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