% :- module(lambda,[normalize/2]).

% Term := Var | Atom | Term * Term | lam(X,Term)
%       | f(Term,...,Term) (!)

normalize(Term,Nf) :-
    beta(Term,Red,Tag),
    normalizeLO(Red,Nf,Tag), !.

normalizeLO(T,T,not) :- !.
normalizeLO(T,Nf,chd) :-
    normalize(T,Nf), !.

normalize_seq([T|Ts],[Nf|Nfs]) :-
    normalize(T,Nf),
    normalize_seq(Ts,Nfs).
normalize_seq([],[]).

% Beta-Reduktion beta(+Term,-Reduziert,-geändert?)

beta(X, X, not) :-
    var(X), !.

beta(M*N, M*ConN, Tag) :-
    var(M),
    beta(N,ConN,Tag), !.

beta(lam(X,M)*N, MDup, chd) :-
    alpha(lam(X,M),lam(XDup,MDup)),
    XDup = N, !.

beta(M*N, T, Tag) :-
    beta(M,ConM,TagL),
    wrLO(TagL,M,ConM,N,T,Tag), !.  % s.u.

beta(lam(V,T), lam(V,ConT), Tag) :-
    beta(T,ConT,Tag), !.

beta(T, ConT, not) :- % für f(Term,..,Term) 
    compound(T),      
    !, T =.. [F|Args],
    normalize_seq(Args,Nfs),
    ConT =..[F|Nfs].    

beta(V, V, not) :- !. 

% Schwache leftmost-outermost-Reduktion

wrLO(not, M, _, N, M*ConN, Tag) :-
    beta(N,ConN, Tag), !.

wrLO(chd, _,ConM, N, ConM*N, chd) :- !.

% Alpha-Reduktion: 

alpha(T, TDup) :-
    alpha_list(T,[],TDup), !.

alpha_list(V, L, VDup) :-
    var(V),
    !, rename(V,L,VDup). 

alpha_list(lam(Var,Body), L, lam(New,BodyDup)) :-
    !, alpha_list(Body,[(Var,New)|L],BodyDup).

alpha_list(M*N, L, MDup*NDup) :-
    !, alpha_list(M,L,MDup),
    alpha_list(N,L,NDup).

alpha_list(F,_, F) :-
    atomic(F), !. 

alpha_list(T, L, TDup) :-  % für:  f(Term,...,Term) 
    compound(T),
    !, T =.. [F|Ts],
    alphas(Ts,L,TsDup),
    TDup =.. [F|TsDup].

alphas([T|Ts], L, [TDup|TsDup]) :-
    alpha_list(T,L,TDup),
    alphas(Ts,L,TsDup).
alphas([],_L,[]).

rename(V, [], V).
rename(V, [(Var,Dup)|_], Dup) :-
    V == Var, !. 
rename(V, [_|C], Dup) :-  
    !, rename(V,C,Dup).

