1:- module(ptq, []).
9
10:- use_module(pac(reduce)). 11:- use_module(util(misc)). 12:- use_module(util(models)). 13:- use_module(util('emacs-handler')). 14:- use_module(util(beta)). 15:- use_module(util(langsem)). 16:- use_module(pac(op)). 17:- use_module(pac(basic)). 18
19
20:- op(670, xfy, \). 25
26
27demo(A,B):-demo_sentence(A), once(ptq(A, B)).
28
30demo_sentence([john,walk]).
31demo_sentence([john,find, a, unicorn]).
32demo_sentence([john,seek, a, unicorn]).
33demo_sentence([every, unicorn, walk]).
34demo_sentence([a, unicorn, find, john]).
37debrujin(T0, T) :- debrujin(T0, T, _).
39debrujin(T, T1, N):- debrujin([], 1, T, N, T1).
41debrujin(N, T, N1, T1):- debrujin([], N, T, N1, T1).
43debrujin(Assoc, N, T, N, T1):- assocq(Assoc, T, T1), !.
44debrujin(Assoc, N, X, N1, Y):- scope(X, V, B, Y, #(N), B1), !,
45 N2 is N+1,
46 debrujin([(V, #(N))|Assoc], N2, B, N1, B1).
47debrujin(Assoc, N, T, N1, T1):- eh:termrec(ptq:debrujin_(Assoc), T, T1, N, N1).
49debrujin_(A, X, Y, Z, U):- debrujin(A, X, Z, Y, U).
50
51scope(\(V,B), V, B, \(V0,B0), V0, B0).
52scope(iota(V, B), V, B, iota(V0, B0), V0, B0).
53scope(forall(V, B), V, B, forall(V0, B0), V0, B0).
54scope(exists(V, B), V, B, exists(V0, B0), V0, B0).
55
56shift(N, #(M), #(M1)):- !, M1 is M + N.
57shift(N, T, T1) :- mapterm(shift(N), T, T1).
58
59alpha_equiv(X, Y):- debrujin(X, Z, N), debrujin(Y, Z, N).
60
65
66ptq_set(X, S):- ptq_set(s, X, S).
68ptq_set(C, X, S):- ptq_all_(C, X, S0),
69 term_smash0(["<font color=\"red\">", S0, "</font>"], S).
70
71ptq_all_(C, X, S):- setof(Y, ptq(C, X, Y), S1), !,
72 maplist(term_smash0,S1,S2), insert("<br>",S2,S).
73ptq_all_(_, _, "** Category mismatch ?").
74
75
81
82ptq --> ptq(s).
83
84ptq(C) --> parse(C), !,
85 simplify, !,
86 sharp_to_print_name, !,
87 pretty_print_html, !.
88
89webchurch --> simplify,
90 sharp_to_print_name, !,
91 pretty_print_html, !.
92
93
96parse(C, X, Y):- call(C, Y, X, []), normal(Y).
97
98normal(error(_,_,_)):- !, fail.
99normal(_).
100
102
103s(@(NP2,int(\(X,@(NP1,int(VP)))))) --> np(NP1), vp(VP,X,NP2).
105s(@(NP, int(VP))) --> np(NP), vp(VP).
107
108np(@(A, int(CN))) --> determiner(A), cn(CN).
109np(PN) --> pn(PN).
110
111vp(ITV) --> itv(ITV).
112vp(@(TV, int(NP))) --> tv(TV), np(NP).
113
114vp(@(TV, int(\(P, @@(P,X)))), X, NP) --> tv(TV), np(NP).
115
116itv(walk)-->[walk].
117
118tv(find_star) --> [find].
119tv(seek) --> [seek].
120tv(\(P, \(X, @@(P, int(\(Y, X=Y)))))) --> [is].
121
122pn(\(P, @@(P, j))) --> [john].
123pn(\(P, @@(P, b))) --> [bill].
124
125cn(unicorn) --> [unicorn].
126cn(man) --> [man].
127
129determiner(X\ (Y\ (exists(Z, @@(X,Z) & @@(Y,Z)))))-->[a].
130determiner(X\ (Y\ (forall(Z, @@(X,Z)-> @@(Y,Z)))))-->[every].
131
133
138
142variable(#(_)).
144signature( \+ ((#)/1) ).
145
146:- meta_predicate ptq_reduce(:,?,?). 147ptq_reduce(R) --> {signature(S)}, reduce:reduce(R, subtree(S)).
148
150
153
154simplify --> {b_setval(brujin_index, 0)},
155 ptq_reduce(expand_lambda_macro),
156 debrujin,
157 ptq_reduce(ptq_rule),
158 ptq_reduce(redex_to_term),
159 ptq_reduce(elim_redundant),
160 ptq_reduce(paramodulation),
161 ptq_reduce(identity),
162 ptq_reduce(elim_redundant),
163 ptq_reduce(boole),
164 debrujin.
165%
166ptq_rule(@@(P,X), ext(P)@X).
167ptq_rule(ext(int(X)), X).
168ptq_rule((X\Y)@Z, U):- b_getval(brujin_index, I),
169 debrujin(I, X\Y, J, X0\Y0),
170 b_setval(brujin_index, J),
171 beta_subst([(X0, Z)], Y0, U).
172ptq_rule(X, Y):- ptq_postulate(X,Y).
173
174% PTQ表示è¦ç´ f@a= f(a). (f@y)@x = f(x, y)
175% ?- redex_to_term(f@y, E).
176% ?- reduce(ptq:redex_to_term, (f@y)@x, E).
177
178redex_to_term(X@Y, Z):-
179 L = [exists(_,_), forall(_,_), #(_), ext(_), int(_),
180 @@(_,_), @(_,_)],
181 \+ member(X, L),
182 X=..[F|X0],
183 Z=..[F,Y|X0].
184
186paramodulation(exists(X, B), exists(X, B0)):-
187 select_eq_conj(B, X=R, B1),
188 beta:beta_subst([(X,R)], B1, B0).
190select_eq_conj(L=R, L=R, true):- variable(L).
191select_eq_conj(L=R, R=L, true):- variable(R).
192select_eq_conj(A&B, E, A0&B):- select_eq_conj(A, E, A0).
193select_eq_conj(A&B, E, A&B0):- select_eq_conj(B, E, B0).
194
195identity(X = Y, true):- X == Y.
196
202
203boole((A&B)&C, A&(B&C)).
204boole(true&A, A).
205boole(A&true, A).
206boole(_&false, false).
207boole(false&_, false).
208boole(not(not(X)), X).
209boole(or(_,true), true).
210boole(or(true,_), true).
211boole(or(false,A), A).
212boole(or(A, false), A).
213boole(not(true), false).
214boole(not(false), true).
215
216elim_redundant(exists(X, Y), Y):- \+ appear(X, Y).
217elim_redundant(forall(X, Y), Y):- \+ appear(X, Y).
218
220appear(X, X).
221appear(X, Y):- Y=..[_|Y0], member(Z, Y0), appear(X, Z).
222
224expand_ptq_macro(X, X):- var(X), !.
225expand_ptq_macro(X, Y):- def(X, Def), !, expand_ptq_macro(Def, Y).
226expand_ptq_macro(X, Y):- X=..[F|Xs],
227 ( def(F, D)
228 -> expand_ptq_macro(D, E),
229 maplist(expand_ptq_macro, Xs, Ys),
230 beta:lambda_application(E, Ys, Y)
231 ; maplist(expand_ptq_macro, Xs, Ys),
232 Y =..[F|Ys]
233 ).
234
238
239sharp_to_print_name(X, X):- var(X), !.
240sharp_to_print_name(#(I), X):-
241 nth1(I, [x,y,z,u,v,w,l,m,n,p,q,r,s,t,u,a,b,c,d,e,f,g,h,i,j,k], X),
242 !.
243sharp_to_print_name(#(I), #(J)):- !, number_codes(I,J).
244sharp_to_print_name(T, T0):- T=..[F|A],
245 maplist(sharp_to_print_name, A, A0),
246 T0 =.. [F|A0].
247
248% ?- num_num(3, C).
249% num_num(I, J) :- format(codes(C), "~w", [I]), number_codes(J,C).
250
251% Meaning postulate 4 (æå³å
¬æº)
252
253ptq_postulate(find_star@P@X, @@(P, int(Y\ find@Y@X))).
254
262expand_lambda_macro(M, D):-
263 ( def(M, E) -> debrujin(E, D)
264 ; M=..[F|As],
265 def(F, M0),
266 debrujin(M0, M1),
267 beta_redex(M1, As, D)
268 ).
269
271beta_redex(M, [], M).
272beta_redex(M, [A|As], N):- beta_redex(M@A, As, N).
273
275def(cn(X), M):- church_numeral(X, M).
276def(p, x\y\x).
277def(q, x\y\ y).
278def(pi1, x\y\ x).
279def(qi2, x\y\ y).
280def(true, x\y\ x).
281def(false, x\y\ y).
282def(and, x\y\ (x @ y @ false)).
283def(not, x\ (x @ false @ true)).
284def(if, x\y\z\ (x @ y @ z)).
285def(succ, n\f\x\ (f @ (n @ f @ x))).
286def(pred, n\f\x\ (n @ (g \ h \ ( h @ (g @ f))) @ (u \ x) @ (u \ u))).
287def(plus, m\n\f\x\ ( m @ f @ (n @ f @ x))).
288def(mult, m\n\ (m @ (plus @n) @ cn(0))).
289def(iszero, n\ (n@ (x \ false) @ true)).
290def(zero, cn(0)).
291def(one, cn(1)).
292def(two, cn(2)).
293def(three, cn(3)).
294def(cons, f\s\b\ (b @ f @s)).
295def(car, p\ (p @ true)).
296def(cdr, p\ (p @ false)).
297def(ycombinator, f\ ((x\ (f @ (x @ x))) @ (x\ (f @ (x @ x))))).
298def(factorial, f\n\ if(iszero(n), cn(1), mult(n, f @ pred(n)))).
299def(test, f\n\ cn(0)).
300
303
307
308church_numeral(N, CN) :- church_numeral(N, CN0, f, x),
309 fresh_bind(CN0, CN).
310
312church_numeral(0, F\X\ X, F, X).
313church_numeral(N, F\X\ (F @ M), F, X):- N > 0, N0 is N-1, church_numeral(N0, F\X\ M, F, X).
322
323pretty_print_html(A, [A]):- atomic(A), !.
324pretty_print_html(X, Y):- X=..[F|A],
325 length(A, N),
326 maplist(pretty_print_html, A, B),
327 pretty_print_html0(F, N, B, Y).
328
329pretty_print_html0(exists, 2, [A, B], ["∃", A, B]).
330pretty_print_html0(forall, 2, [A, B], ["∀", A, B]).
331pretty_print_html0((\), 2, [A, B], ["λ", A, B]).
332pretty_print_html0((&), 2, [A, B], ["(", A, "∧", B,")"]).
333pretty_print_html0((or), 2, [A, B], ["(", A, "∨", B,")"]).
334pretty_print_html0((not), 1, [A], ["(","¬", A, ")"]).
335pretty_print_html0((->), 2, [A,B], ["(",A, "→", B, ")"]).
336pretty_print_html0(F, 2, [A, B], ["(", A, F, B, ")"]):- declared_op(F, 2).
337pretty_print_html0(F, 1, [A], ["(", F, A, ")"]):- declared_op(F, 1).
338pretty_print_html0(F, _, L0, [F, "(", L , ")" ]):- insert(",", L0, L).
339
341declared_op(X,N):- current_op(_,T,X),
342 ( N=2, memberchk(T, [xfx,xfy,yfx,yfy])
343 ; N=1, memberchk(T, [fx, fy])
344 )