Lambda calculus alpha equivalence and beta reduction in Prolog (basic attempt, not complete)

lambda.pl

%%%%%%%%%%%%%%%
% Sets and maps
%%%%%%%%%%%%%%%

% Sets: http://kti.ms.mff.cuni.cz/~bartak/prolog/sets.html
% Maps: sets of pairs.

list([]).
list([_|_]).

lt(X, Y) :- var(X); var(Y).
lt(X, Y) :- nonvar(X), nonvar(Y), not(list(X)), not(list(Y)), X < Y.
lt([], [_]).
lt([X], [Y]) :- lt(X, Y).
lt([X|XT], [Y|YT]) :- lt(X, Y), lt(XT, YT).

% Set union
union(S, [], S).
union([], S, S).
union([X|TX], [X|TY], [X|TZ]) :- union(TX, TY, TZ).
union([X|TX], [Y|TY], [X|TZ]) :- lt(X,Y), union(TX, [Y|TY], TZ).
union([X|TX], [Y|TY], [Y|TZ]) :- lt(Y,X), union([X|TX], TY, TZ).

% Subtract set Y from X.
subtract(S, [], S).
subtract([], _, []).
subtract([X|TX], [X|TY], TZ) :- subtract(TX, TY, TZ).
subtract([X|TX], [Y|TY], [X|TZ]) :- lt(X,Y), subtract(TX, [Y|TY], TZ).
subtract([X|TX], [Y|TY], TZ) :- lt(Y,X), subtract([X|TX], TY, TZ).

% Inverse map (set of pairs).
invmap([], []).
invmap([[K,V]|M1], [[V,K]|M2]) :- invmap(M1, M2).

% Check if X maps to Y in map M.
mapsto([[K, V]|_], X, Y) :- X = K, Y = V.
mapsto([[K, _]|M], X, Y) :- X \= K, mapsto(M, X, Y).

% Delete a map key.
delkey([], _, []).
delkey([[K,_]|M], K, M).
delkey([[K1,V1]|M1], K, [[K1,V1]|M2]) :- K \= K1, delkey(M1, K, M2).

% Set a map key.
setkey(M1, K, V, M2) :- delkey(M1, K, M3), union(M3, [[K,V]], M2).

% Check map domain assuming an ordered domain.
mapdom([], []).
mapdom([[K,_]|M], [K|TK]) :- mapdom(M, TK).

% ?- setkey([], "x", "y", U1),
%    setkey(U1, "v", "w", U2),
%    setkey(U2, "x", "z", U3),
%    invmap(U3, U4),
%    mapsto(U4, "z", X).

%%%%%%%%%%%%%%%%%
% Lambda calculus
%%%%%%%%%%%%%%%%%

% Variables are represented as strings.
variable(X) :- string(X).

% FV(x) = {x}
fv(X, [X]) :- variable(X).

% FV((M1, M2)) = FV(M1) union FV(M2)
fv(app(M1, M2), FV) :- fv(M1, FV1), fv(M2, FV2), union(FV1, FV2, FV).

% FV(\x.M) = FV(M) - x
fv(lambda(X, M), FV) :- variable(X), fv(M, FV1), subtract(FV1, [X], FV).

% Alpha conversion on a variable.
alpha(X, Y, U) :- variable(X), variable(Y), mapsto(U, X, Y).

% Alpha conversion on append.
alpha(app(M1, M2), app(M3, M4), U) :- alpha(M1, M3, U), alpha(M2, M4, U).

% Alpha conversion on abstraction.
alpha(lambda(X, M1), lambda(Y, M2), U) :-
    variable(X), variable(Y),
    alpha(M1, M2, V),
    delkey(V, X, U).

% Alpha equivalence needs to go both ways.
alphaeq(M, N, U) :-
    alpha(M, N, U),
    fv(M, FV),
    mapdom(U, FV),
    invmap(U, V),
    alpha(N, M, V).

% x[x -> M] = M
subst(X, M, X, M) :- variable(X).

% (M1 M2)[x -> M] = (N1, N2) s.t. M1[x -> M] = N1, M2[x -> M] = N2
subst(X, M, app(M1, M2), app(N1, N2)) :- subst(X, M, M1, N1), subst(X, M, M2, N2).

% (\x.N)[x -> M] = (\x.N) by shadowing
subst(X, _, lambda(X, N), lambda(X, N)) :- variable(X).

% (\y.M1)[x -> M] = (\y.N) s.t. M1[x -> M] = N
% TODO: Pick fresh Y not in fv(M) for the beta reduced form.
subst(X, M, lambda(Y, M1), lambda(Y, N)) :-
    variable(X), variable(Y),
    X \= Y, subst(X, M, M1, N).

% A variable cannot be beta reduced.
beta(X, X) :- variable(X).

% A lambda cannot be beta reduced.
beta(lambda(X, M), lambda(X, M)) :- variable(X).

% An application of a lambda can be beta reduced.
beta(app(M1, M2), N) :-
    % Beta reduce M1 to a lambda.
    beta(M1, lambda(X, M3)),
    % Apply lambda and beta reduce the result.
    subst(X, M2, M3, M4), beta(M4, N).