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 16
17
18 21
24
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
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].
49beta_one_list([X|Xs], [Y|Xs]):- beta_one(X, Y).
50beta_one_list([X|Xs], [X|Ys]):- beta_one_list(Xs, Ys).
51
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
70
72
75
76lambda_application(E, [], E).
77lambda_application(E, [A|As], E0):- lambda_application(E@A, As, E0).
78
80
87
88:- meta_predicate fresh_bind(6, ?, ?). 89
90fresh_bind(T0, T) :- fresh_bind(protected, T0, T).
92fresh_bind(P, T0, T) :- fresh_bind(P, [], T0, T).
93
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
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
118copy_term(X, B, C):- copy_term((X,B), (Y,C)), X=Y.
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
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
139
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
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
170
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
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