Module abstract

Jekejeke Prolog also provides a simple denotation for lambda abstraction. We use the operator (\)/2 to denote abstracted terms and the operator (^)/2 to denote local terms. We can describe the lambda abstraction via the following syntax:

abstraction      --> binder "\" body_with_local.
body_with_local  --> local "^" body_with_local.
                   | body.
binder           --> term.
local            --> term.

It is possible to abstract goals and closures. The result is a new closure with an incremented closure index. The binder can be an arbitrary term, which allows pattern matching. The local can be an arbitrary term as well, which allows combining multiple local variables. The global variables of a lambda abstraction are aliased along invocations.

?- map(X\Y\(H is X+1, Y is H*H),[1,2,3],R).
No                           % Aliasing prevents success.
?- map(X\Y\H^(H is X+1, Y is H*H),[1,2,3],R).
R = [4,9,16]                 % Now everything is fine.

When a lambda abstraction is invoked the binder is replaced by the argument. In normal lambda calculus the global variables of the argument can clash with further binders in the body. In our implementation it can also happen that binders, local variables and global variables can clash. Local variables can be used to prevent clashes by renaming variables:

?- K=X\Y\ =(X), call(K,Y,B,R).
K = X\Y\ =(X),
B = R                       % Clash gives wrong result.
?- K=X\Y^Y\ =(X), call(K,Y,B,R).
K = X\Y^Y\ =(X),
R = Y                       % Now everything is fine.

The following abstract predicates are provided:

\(X, A, Y1, .., Yn):
The predicate is defined for 1 ≤ n ≤ 7. The goal \(X, A, Y1, .., Yn) succeeds whenever the goal call(A[X/Y1], Y2, ..., Yn) succeeds.