1:- module(beta,
    2	  [beta_subst/3, normal_form/2,
    3	  fresh_bind/2, fresh_goal/3, fresh_call/2
    4	   ]).    5
    6:- use_module(pac(basic)).    7:- use_pac('emacs-handler').    8:- include(pac(op)).    9
   10		/********************************************************
   11		*     Note: This very old codes is currently broken.    *
   12		*     No plan to review and rewrite.                    *
   13		********************************************************/
   14
   15
   16        /********************************
   17		*     Lambda-beta conversion    *
   18		********************************/
   19% ?- pac_beta:normal_form(f((x\x)@a, (y\y)@b), X).
   20% X = f(a, b).
   21% ?- beta_one(f(x\x@a, y\y@b), X).
   22% X = f(a, y\y@b)
   23% ?- beta(x\x@a, X).
   24% X = a.
   25
   26normal_form(X, Y):-  beta_one(X, X0), !,
   27	normal_form(X0, Y).
   28normal_form(X, X).
   29
   30beta(E, M0):- is_beta_redex(E),
   31	E = @(\(X, M), N),
   32	fresh_bind(\(X,M), \(X0,M0)),
   33	X0 = N.
   34
   35is_beta_redex(M):- nonvar(M), M=(F@_), nonvar(F), F=(_\_).
   36
   37beta_one(M, M0):- beta(M, M0).
   38beta_one(X, Y):- compound(X), X=..[F|Xs],
   39	beta_one_list(Xs, Ys),
   40	Y=..[F|Ys].
   41
   42beta_one_list([X|Xs], [Y|Xs]):- beta_one(X, Y).
   43beta_one_list([X|Xs], [X|Ys]):- beta_one_list(Xs, Ys).
   44
   45%%%
   46outer_most_first(X, Y):- var(X), !, Y=X.
   47outer_most_first(F@A, Y):- !, outer_most_first(A, A0),
   48	outer_most_first(F, F0),
   49	beta_outer_most_first(F0, A0, Y).
   50outer_most_first(X, X).
   51
   52beta_outer_most_first(F, A, F@A):- var(F), !.
   53beta_outer_most_first(X\M, A, Y):- !, fresh_bind(X\M, X0\Y), X0=A.
   54% beta_outer_most_first(X\M, A, Y):- !, fresh_bind(X\M, X0\Y0), X0=A,
   55%	outer_most_first(Y0, Y).
   56beta_outer_most_first(F, A, F@A).
   57
   58% ?- church(ycombinator @ factorial@ cn(2), X).
   59% ?- church(ycombinator @ factorial@ cn(3), X), numbervars(X, 0, _), write_canonical(X).
   60% ?- macro_expansion(if(true, succ(zero), one), X).
   61% X = (x\y\z\ (x@y@z)@f\x\ (f@x)@ (n\f\x\ (f@ (n@f@x))@f\x\x)@x\y\x).
   62
   63% church(X, Y):- macro_expansion(X, X0), normal_form(X0, Y).
   64
   65% church_outer_most(X, Y):- macro_expansion(X, X0),
   66%	outer_most_first(X0, Y).
   67
   68lambda_application(E, [], E).
   69lambda_application(E, [A|As], E0):- lambda_application(E@A, As, E0).
   70
   71%%%%  Yet Another deBrujin-ing
   72% ?- fresh_bind([x,x]\a(x,x), P), numbervars(P, 0, _).
   73% P = [A, B]\a(B, B).
   74
   75fresh_bind(T0, T) :- fresh_bind(protected, T0, T).
   76fresh_bind(P, T0, T) :- fresh_bind(P, [], T0, T).
   77
   78:- meta_predicate fresh_bind(6, ?, ?).   79
   80fresh_bind(_, Assoc, X, Y):- (var(X); atom(X)), !,
   81	(assocq(Assoc, X, Y) -> true;  Y = X).
   82fresh_bind(P, Assoc, X, X0):- call(P, X, V, B, X0, V0, B0), !,
   83	fresh_vars(P, V, V0, Assoc, Assoc0),
   84	fresh_bind(P, Assoc0, B, B0).
   85fresh_bind(P, Assoc, X, Y):- mapterm(fresh_bind(P, Assoc), X, Y).
   86
   87fresh_vars(P, V, V0, Assoc, Assoc0):- (var(V); atom(V))
   88	-> Assoc0=[(V,V0)|Assoc]
   89	;  fresh_bind_(V, V0, Assoc, Assoc0, P).
   90
   91fresh_bind_([], [], Assoc, Assoc, _):- !.
   92fresh_bind_([X|Y], [X0|Y0], Assoc, Assoc0, P):-
   93	fresh_bind_(Y, Y0, [(X,X0)|Assoc], Assoc0, P).
   94
   95copy_term(X, B, C):- copy_term((X,B), (Y,C)), X=Y.
   96
   97protected(st(E, V, B), V, a(B, E), st(E0, V0, B0), V0, a(B0, E0)).
   98protected(#(E, V, B), V, a(B, E), #(E0, V0, B0), V0, a(B0, E0)).
   99protected(^(V, B), V, B, ^(V0, B0), V0, B0).
  100protected(\(V,B), V, B, \(V0,B0), V0, B0).
  101protected(\\(V,B), V, B, \\(V0,B0), V0, B0).
  102protected(forall(V, B), V, B, forall(V0, B0), V0, B0).
  103protected(exists(V, B), V, B, exists(V0, B0), V0, B0).
  104protected(every(V, B), V, B, every(V0, B0), V0, B0).
  105protected(some(V, B), V, B, some(V0, B0), V0, B0).
  106
  107%%%% test alpha equivalence between closed terms.
  108% ?- alpha_equiv(x\x@(x\x), y\y@(z\z)).
  109
  110alpha_equiv(X,Y):- fresh_bind(X, X0), fresh_bind(Y, Y0),
  111	numbervars(X0, 0, N), numbervars(Y0, 0, N),
  112	X0==Y0.
  113
  114% Beta conversion for Lambda Calculus.
  115% ?- beta_star((x\x)@a, X).
  116% ?- var_beta_star((_x\_x)@a, X).
  117% ?- beta_star((x\forall(x,x=x))@a, X).
  118% X = forall(x, x=x).
  119% ?- var_beta_star((x\forall(x,x=x))@a, X).
  120% X = forall(_G271, _G271=_G271).
  121
  122beta_star(X, Y):- reduce:term_rewrite(beta_star_, [], X, Y).
  123
  124beta_star_(X, _):- var(X), !, fail.
  125beta_star_(@(\(X,Y), Z), Y0):- fresh_bind(\(X,Y), \(X0, Y0)), X0=Z.
  126
  127var_beta_star(X, Y):- reduce:term_rewrite(beta_star_, [], X, Y).
  128
  129var_beta_star_(X, _):- var(X), !, fail.
  130var_beta_star_(@(\(X,Y), Z), U):- beta_subst([(X,Z)], Y, U).
  131
  132%%%%
  133% Not obsolete ! ; being used by ptq module
  134beta_subst(X, Y, Z):- once(beta_subst([], X, Y, Z)).
  135
  136beta_subst(Vs, _, A, A) :- memq(A, Vs).
  137beta_subst(_, Ps, A, B) :- assocq(Ps, A, B).
  138beta_subst(_, Ps, A, A) :- (Ps==[]; var(A)).
  139beta_subst(Vs, Ps, \(X,A), \(X,B)) :- beta_subst([X|Vs], Ps, A, B).
  140beta_subst(Vs, Ps, A, B) :-
  141	atomic(A) -> B=A ; mapterm(beta_subst(Vs, Ps), A, B).
  142
  143% fresh_goal/3
  144% ?- fresh_goal([X]:-a(X), A, G).
  145% A = [_G506],
  146% G = a(_G506).
  147
  148fresh_goal(H:-G, A, G0):- !, fresh_goal(H, G, A, G0).
  149fresh_goal(:-G, [], G0):- !, copy_term(G, G0).
  150fresh_goal(^(F, X), A, true):- !, copy_term((F, X), (F, A)).
  151fresh_goal(fix(X, E), A, G):- !, fresh_goal_fix(X, E, A, G).
  152fresh_goal([],[], true):-!.
  153fresh_goal([A|B], C, true):-!, copy_term([A|B],C).
  154
  155% fresh_goal/4
  156fresh_goal(H, G, A, G0):- var(H), !, copy_term((H, G), (A, G0)).
  157fresh_goal(F^X, G, A, G0):- !, copy_term((F, X, G), (F, A, G0)).
  158fresh_goal(^(F), G, [], G0):- !, copy_term((F, G), (F, G0)).
  159fresh_goal(X, G, A, G0):- copy_term((X, G), (A, G0)).
  160
  161fresh_goal_fix(X, E, A, app(E0, A)):- var(X), !,
  162	copy_term(fix(X, E), fix(X0, E0)),
  163	X0 = fix(X,E).
  164fresh_goal_fix(V^X, E, A, app(E0, A)):- !,
  165	copy_term(fix(V, X, E), fix(V, X0, E0)),
  166	X0 = fix(V^X,E).
  167
  168%
  169%
  170fresh_call(X, A):- fresh_bind(X