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

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

normalize(T,Nf) :-
    beta(T,ConT,Tag),     % Einen Vereinfachungsschritt
    ( Tag = chd           % machen; falls der zu ConT =/= T
    -> normalize(ConT,Nf) % fuehrt, das weiter vereinfachen,
    ; Nf = ConT ).        % sonst ist ConT = T die Normalform

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(T*S, T*ConS, Tag) :-
    var(T),
    !, beta(S,ConS,Tag).

beta(lam(X,R)*S, RDup, chd) :-
    !, alpha(lam(X,R),lam(XDup,RDup)),
    XDup = S.         % simuliert R[X/S]

beta(T*S, U, Tag) :-
    !, beta(T,ConT,TagT),
    ( TagT = chd -> U = ConT*S, Tag = chd
    ; beta(S,ConS,Tag), U = T*ConS ).

beta(lam(X,R), lam(X,ConR), Tag) :-
    !, beta(R,ConR,Tag).

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

beta(T, T, not) :- !. % Konstante

% Alpha-Reduktion: alpha(+Term,-Umbenannt)

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

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

alpha_list(lam(V,R), L, lam(New,RDup)) :-
    !, alpha_list(R,[(V,New)|L],RDup).

alpha_list(ex(V,R), L, ex(New,RDup)) :-
    !, alpha_list(R,[(V,New)|L],RDup). 

alpha_list(all(V,R), L, all(New,RDup)) :-
    !, alpha_list(R,[(V,New)|L],RDup). 

alpha_list(T*S, L, TDup*SDup) :-
    !, alpha_list(T,L,TDup),
    alpha_list(S,L,SDup).

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

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(+Var, +Variablenpaare, -VarUmbenannt)

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