Lambda calculus simplifier and interpreter in SWI prolog

Lambda.pro

/*
 * AST definition
 */

:- op(100, fx , (:)).
:- op(200, yfx, ($)).
:- op(300, xfy, (->)).

isName(N) :- N =.. [_].

isExpr(:N    ) :- isName(N).
isExpr(N -> E) :- isName(N), isExpr(E).
isExpr(A $ B ) :- isExpr(A), isExpr(B).

/*
 * Parser
 *
 * We use the prolog functor syntax and transform it into curried function application.
 * We also accept lists, since the function to apply may not be a simple named term.
 *
 * For instance:
 *
 * | Traditional λ-calculus | Internal AST   | "Functor syntax" | "List syntax" |
 * ------------------------------------------------------------------------------
 * | term                   | :term          | term             | term          |
 * | f x                    | f $ x          | f(x)             | [f, x]        |
 * | f x y <=> (f x) y      | f $ x $ y      | f(x, y)          | [f, x, y]     |
 * | λx. e                  | x -> e         | x -> e           | x -> e        |
 * | (λx. x) y              | (x -> :x) $ :y | Not expressible  | [x -> x, y]   |
 * ...
 */

% parse(RawExpr, AST).
parse(N -> E, N -> EAST) :- !, isName(N), parse(E, EAST).
parse(N, :N)             :- isName(N), !.
parse([N | Args], AST)   :- !, uncurry([N | Args], nil, AST).
parse(F, AST)            :- F =.. Apps, !, uncurry(Apps, nil, AST).

% uncurry(NonEmptyList RawExpr, Maybe Accum, AST).
uncurry([E]    , nil      , AST)       :- !, parse(E, AST).
uncurry([E]    , some(Acc), Acc $ AST) :- !, parse(E, AST).
uncurry([E | A], nil      , AST)       :- !, parse(E, EAST), uncurry(A, some(EAST), AST).
uncurry([E | A], some(Acc), AST)       :- !, parse(E, EAST), uncurry(A, some(Acc $ EAST), AST).

/*
 * Base definitions
 */

% subst(InputExpr, Name, Value, OutputExpr).
subst(:X    , X, V, V      ) :- !.
subst(:X    , _, _, :X     ).
subst(X -> E, X, _, X -> E ) :- !. % Shadowing rule
subst(Y -> E, X, V, Y -> S ) :- subst(E, X, V, S).
subst(A $ B , X, V, SA $ SB) :- subst(A, X, V, SA), subst(B, X, V, SB).

% appears(Expr, Name).
appears(:X    , X).
appears(N -> E, X) :- N \= X, appears(E, X).
appears(A $ B , X) :- appears(A, X) ; appears(B, X).

% appearsAtMostOnce(Expr, Name).
appearsAtMostOnce(:_    , _).
appearsAtMostOnce(N -> E, X) :- N = X, ! ; appearsAtMostOnce(E, X).
appearsAtMostOnce(A $ B , X) :- \+ appears(A, X), appearsAtMostOnce(B, X), !
                             ;  \+ appears(B, X), appearsAtMostOnce(A, X).

/*
 * Lambda calculus substitution rules
 */

% alpha(In, Name, Out).
%alpha(X -> E, Y, Y -> S) :- \+ appears(E, Y), subst(E, X, :Y, S).
%
% Edit: There is a bug in the above definition. It does not take into
% account scenarii such as the following :
%   (λx. λy. x) ≠ (λy. λy. y)
% (the presence of `y` in binders is not checked)

% beta(In, Out).
beta((X -> Body) $ Arg, S) :- subst(Body, X, Arg, S).

% eta(In, Out).
eta(X -> E $ :X, E) :- \+ appears(E, X).

/*
 * Evaluation
 */

% simplify(In, Out). Guaranteed to terminate
% (Proof hint: Introduce a function that measures the relative size of expressions;
%              What can you tell about the simplification operations ?)
simplify(:X, :X).
simplify(N -> B, R) :- simplify(B, SB), simplifyNonRec(N -> SB, S)
                    ,  ( N -> SB = S, !, S = R % Fixpoint reached
                       ; simplify(S, R)        % Otherwise, keep going
                       ).
simplify(A $ B, R)  :- simplify(A, SA), simplify(B, SB), simplifyNonRec(SA $ SB, S)
                    ,  ( SA $ SB = S, !, S = R
                       ; simplify(S, R)
                       ).

simplifyNonRec((X -> Body) $ Arg, S)
	:- appearsAtMostOnce(Body, X), !
	,  beta((X -> Body) $ Arg, S).

simplifyNonRec(X, S)
	:- eta(X, S), !.

simplifyNonRec((X -> Body) $ :N, S)
	:- !, beta((X -> Body) $ :N, S).

simplifyNonRec(X, X).

% deepEval(In, Out). May diverge though it will detect some loops and stop evaluating.
deepEval(:X, :X).
deepEval(N -> B, N -> R) :- deepEval(B, R).
deepEval(A $ B, R)       :- deepEval(A, RA), deepEval(B, RB), evalNonRec(RA $ RB, S)
                         , ( RA $ RB = S, !, S = R % Fixpoint reached
                           ; deepEval(S, R)        % Otherwise, keep going
                           ).

evalNonRec(E, R) :- beta(E, R), !.
evalNonRec(E, E).

% safeEval(Limit, In, Out). May time out.
safeEval(Lim, I, O) :-
    catch(
        call_with_time_limit(Lim, deepEval(I, O)),
        time_limit_exceeded,
        O = timed_out
        ).

/*
 * Utility REPL testing predicates
 */

% test(Expr, Simp, Eval).
test(Expr, Simp, Eval) :- ( parse(Expr, AST), isExpr(AST) ; writeln("Syntax error or parser crash"), fail ),
                          ( simplify(AST, Simp), ! ; Simp = crashed ),
                          ( safeEval(5, AST, Eval), ! ; Eval = crashed ).

/* examples

% simplifier test.
test(
    [a -> b -> a(x -> a(x)), x(y)],
    Simp, Eval).

% Omega. deepEval detects the divergence.
test(
    [x -> x(x), x -> x(x)],
    Simp, Eval).

% Some variant of omega. deepEval does not detect the divergence.
test(
	[x -> x(x, x), x -> x(x, x)],
    Simp, Eval).

% For my Sum Type Ménagerie.
Left  = x -> l -> r -> l(x),
Right = x -> l -> r -> r(x),
Id    = x -> x,
Const = a -> b -> a,

Main = [Right, "lol", [Const, ""], Id],

test(Main, Simp, Eval).

% Church arithmetic
Zero =            z -> s -> z,
Succ = n ->       z -> s -> s(n(z, s)),
Plus = n -> m ->  z -> s -> n(m(z, s), s),
Times= n -> m ->  z -> s -> n(z, acc -> m(acc, s)),

Three= [Succ, [Succ, [Succ, Zero]]],

test([Times, Three, Three], Simp, Eval).

*/