This is an interpreter for the pure untyped lambda calculus.

lambda.pl

% This is an interpreter for the pure untyped lambda calculus.

% We represent lambda terms using De Bruijn indices.

term(var(I)) :- integer(I).
term(abs(M)) :- term(M).
term(app(M, N)) :- term(M), term(N).

% Lambda abstractions are the only values.

valu(abs(M)) :- term(abs(M)).

% A lambda abstraction binds a variable in its subterm. The key idea in
% this implementation is that we can *lift* this binding into the
% metalanguage, and implement substitution in the lambda calculus by
% means of substitution in Prolog.
%
% This is accomplished by taking the subterm of the abstraction and
% replacing all appearances of its bound variable by a free Prolog
% variable. This defines a relation between lambda abstractions and
% Prolog terms with free variables.

lift(abs(MB), MU, X) :- subs(MB, MU, 1, X).

% Examples:
% :- I = abs(var(1)), lift(I, X, X).
% :- K = abs(abs(var(2))), lift(K, abs(X), X).

% Substitution in the subterm is done by traversing it in search of the
% (free) variable with a given index. When such a variable is found it's
% replaced by a Prolog variable which will be shared between all
% appearances.

subs(var(I), X, I, X) :- !.

% Since we're effectively removing a layer of abstraction, we have to
% decrement De Bruijn indices of free variables.

subs(var(J), var(K), I, _) :- J < I -> K is J ; K is J - 1.

% Moreover, we have to increment the searched-for index every time the
% recursion enters an abstraction.

subs(abs(MB), abs(MU), I, X) :- J is I + 1, subs(MB, MU, J, X).

subs(app(MB, NB), app(MU, NU), I, X) :- subs(MB, MU, I, X), subs(NB, NU, I, X).

% So with this in place beta reduction is expressed quite simply: lift
% the abstraction and unify the free variable with the argument.

redu(app(abs(M), N), R) :- lift(abs(M), R, X), X = N.

% Finally, by repeated reduction we express evaluation.

eval(V, V) :- valu(V).

eval(app(M, N), V) :-
  % Evaluate the left term to obtain a lambda abstraction;
  eval(M, MV), MV = abs(_),

  % evaluate the argument (removing this step results in a lazy
  % evaluation strategy);
  eval(N, NV),

  % apply one step of beta reduction;
  redu(app(MV, NV), R),

  % and evaluate the resulting term, to eventually reach a value.
  eval(R, V).