%% Version:  1.0  -  Date: 10 May 2007  -  File: lambda.pl
%%
%% Purpose: Evaluating Lambda Terms
%%
%% Author:  Jens Otten
%%
%% Usage:   lam(L,Y).
%%          % where L is a lambda term and Y the result returned; a
%%          % lambda term L has the following form (X is a variable
%%          % written with SMALL LETTERS; L1,L2 are lambda terms):
%%          %  X:L1              - abstraction (lambda X.L1)
%%          %  L1*L2             - application (L1 L2)
%%          %
%%          % Example: [lambda].
%%          %          lam( (m:n:f:x:m*f*(n*f*x))*3*5 ,Y).
%%          %          lam(add*3*5,Y). % add is defined below
%%          %          lam(add*3*5,Y), num(N,Y). % returns natural
%%          %
%%          % Loads program and evaluates the given lambda term,
%%          % e.g. the sum of 3 and 5 is returned
%%
%% License: GPL

:- op(600,xfy,:).  :- op(500,yfx,*).

%% These are some examples of lambda terms; once they are
%% defined they can be used within other lambda terms

lam(add,m:n:f:x:m*f*(n*f*x)).
lam(mul,m:n:f:x:m*(n*f)*x).
lam(exp,m:n:f:x:(m*n)*f*x).

%% Do not change anything below this line except you know
%% what you are actually doing ...
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
lam((X:L1)*L2,L3) :- !, lam(L1,L4), subs(L4,X,L2,L5), lam(L5,L3).
lam(X:L,X:L1) :- !, lam(L,L1).
lam(L1*L2,L3) :- lam(L1,L4), L1\=L4, !, lam(L4*L2,L3).
lam(L1*L2,L3) :- lam(L2,L4), L2\=L4, !, lam(L1*L4,L3).
lam(L,L1) :- number(L), !, num(L,L1).
lam(L,L).
num(0,(f:x:x)) :- !.
num(N,(f:x:f*L1)) :- var(N) -> num(N1,f:x:L1), N is N1+1 ;
                     N1 is N-1, num(N1,f:x:L1).
subs(X,X,L,L) :- !.
subs(X,_,_,X) :- (atomic(X);X==[[]]), !.
subs(L,X,L2,L1) :- L=..[F,L3|L4], subs(L3,X,L2,L5), subs(L4,X,L2,L6),
                   L1=..[F,L5|L6].