Binders in Prolog

Question

I know Prolog has no built-in binders to represent e.g. λx (x=1) but I was wondering if it was possible to implement them. In some predicates like setof/3, the behaviour is quite close: the variable X in the answer substitution for the query

?- setof(X, member(X,[a,a,c]), Xs).
Xs = [a, c].

is unbound and we can give it a value to our liking:

?- setof(X, member(X,[a,a,c]), Xs), X = b.
X = b,
Xs = [a, c].

But if we instantiate X earlier, we lose solutions:

?- X = b, setof(X, member(X,[a,a,c]), Xs).
false.

What I would like to happen is that setof binds X, i.e. for the evaluation of setof, X is treated like a fresh variable. To make this a bit more concrete: Is it possible to give an implementation binding_setof such that

?- X = b, binding_setof(X, member(X,[a,a,c]), Xs).
X = b,
Xs = [a, c].

?

P.S.: I am aware of languages like λProlog which were built to solve this issue, but I am interested in a Prolog solution.

Edit: I have tried to solve the problem with library(lambda). I aimed to create an anonymous variable and apply it to \X^setof(X, member(X,[a,c,c], Xs) via call/N. Since the binding of Xs is undone outside of it, the toplevel does not report it. It's still possible to see it by adding format('~w',[Xs]) into the setof but I leave it out for clarity. Again, the call

?- call(\X^setof(X,member(X,[a,c,c]),Xs), _), X=b.
X = b.

succeeds, but

?- X = b, call(\X^setof(X,member(X,[a,c,c]),Xs), _).
false.

fails. This is consistent with the comment in the source that a lambda bound variable must not occur outside the lambda expression.

Answer 1

The Golog interpreter contains a solution to locally scoping variables, they use a pi/2 compound and a sub/4 predicate. We can adapt pi/2 to a predicate, their license precludes distributing their interpreter so you'll need to get sub/4 from them (free), linked above.

pi(V, E) :- 
    sub(V, _, E, E1), 
    call(E1).

?- X = d, pi(x, setof(x, member(x, [a, a, c]), Xs)).
X = d,
Xs = [a, c].

It works "most of the time"; I've had issues when working with CLP libraries.