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