Implementation of call-by-name lambda calculus in Prolog using logic variables as lambda variables

lambda.pl

% Implementation of call-by-name lambda calculus in Prolog using logic variables as lambda variables
%
% The grammar is:
% Term ::= Term-Term % abstraction: LHS is function body; RHS is parameter (Y-X instead of λX.Y)
%        | Term+Term % application: LHS is function; RHS is argument (F+X instead of (F X))

eval(Y-X, Y-X). % abstractions are left as-is
eval(F+X, Y) :-
    copy_term(F,B), % copy before destructive unification of parameter in case F appears elsewhere
    eval(B, Y0-X), % eval into what must be an abstraction and unify X with parameter
    eval(Y0, Y). % fully eval resulting term so we aren't left with an application

%% example terms
s(X+Z+(Y+Z) - Z - Y - X).
k(X - _ - X).
i(X - X).
reverse(S + (K + (S + I)) + K) :- s(S), k(K), i(I).
if(P+A+B - B - A - P).
omega(Omega) :- self_apply(X+X - X, Omega).
y(FXXFXX - F) :- self_apply(F+(X+X) - X, FXXFXX).

self_apply(X, X+X).


% tests
test_sksk :-
    s(S),
    k(K),
    eval(S+K+S+K, Res),
    Res =@= K.
test_reverse :-
    s(S),
    k(K),
    reverse(Rev),
    eval(Rev+K+S+S+K, Res),
    Res =@= K.
all_tests :- test_sksk, test_reverse.