1:- module(ptq, []).    2
    3%  run lisp for this s-expression, and type "jj" to get a qcompling query,
    4%  then run the query.
    5
    6:- use_module(pac(reduce)).    7:- use_module(util(misc)).    8:- use_module(util(models)).    9:- use_module(util('emacs-handler')).   10:- use_module(util(beta)).   11:- use_module(util(langsem)).   12:- use_module(pac(op)).   13:- use_module(pac(basic)).   14
   15:- op(670, xfy, \).   16
   17% ?- demo(A,B), smash(B).
   18% ?- ptq_set(s, [john,walk], V), smash(V).
   19
   20% ?- parse(np, [a, unicorn], R), ptq_normalize(R).
   21
   22% ?- trace.
   23% ?- ptq(np, [a, unicorn], R).
   24
   25demo(A,B):-demo_sentence(A), once(ptq(A, B)).
   26
   27test_ptq :- forall(demo_sentence(S),
   28				   (	parse(s, S, X),
   29						(	ptq_normalize(X, Y) ->
   30							writeln(S=>Y)
   31						;	writeln(error(S))
   32						)
   33				   )).
   34% ?- test_ptq.
   35%@ [john,walk]=>walk(j)
   36%@ [john,is,a,man]=>some(x,man@x&j=x)
   37%@ [john,is,bill]=>j=b
   38%@ [a,unicorn,walk]=>some(x,unicorn@x&walk(x))
   39%@ [john,find,a,unicorn]=>some(x,unicorn@x&find(x,j))
   40%@ [john,seek,a,unicorn]=>some(x,unicorn@x&seek(int((y\ext(y@x))),j))
   41%@ [every,unicorn,walk]=>all(x,(unicorn@x->walk(x)))
   42%@ [every,unicorn,seek,john]=>all(x,(unicorn@x->seek(int((y\ext(y@j))),x)))
   43%@ [a,man,find,every,unicorn]=>all(x,(unicorn@x->some(y,man@y&find(x,y))))
   44%@ [some,man,find,every,unicorn]=>all(x,(unicorn@x->some(y,man@y&find(x,y))))
   45%@ true.
   46
   47% ?- parse(s, [john,walk], X),	ptq_normalize(X, Y).
   48%
   49demo_sentence([john, walk]).
   50demo_sentence([john, is, a, man]).
   51demo_sentence([john, is, bill]).
   52demo_sentence([a, unicorn, walk]).
   53demo_sentence([john, find, a, unicorn]).
   54demo_sentence([john, seek, a, unicorn]).
   55demo_sentence([every, unicorn, walk]).
   56demo_sentence([every, unicorn, seek, john]).
   57demo_sentence([a, man, find, every, unicorn]).
   58demo_sentence([some, man, find, every, unicorn]).
   59
   60% ?- gensymvars(X\Y\X\U@V@W).
   61gensymvars(P):- gensymvars([x,y,z], P).
   62%
   63gensymvars(As, P):- term_variables(P, Q),
   64		  length(Q, N),
   65		  gensyms(N, As, U),
   66		  maplist(=, Q, U).
   67
   68
   69% ?- gensyms(3, [a,b,c], U).
   70% ?- gensyms(4, [a,b,c], U).
   71% ?- gensyms(100, [a], U), length(U, L).
   72%
   73gensyms(N, A, U):- gensyms(N, A, A, U, []).
   74%
   75gensyms(0, _, _, U, U):-!.
   76gensyms(N, [], A, U, V):-!, gensyms(N, 1, A, A, U, V).
   77gensyms(N, [X|Xs], A, [X|U], V):- N0 is N-1,
   78	gensyms(N0, Xs, A, U, V).
   79%
   80gensyms(0,_, _, _, U, U):-!.
   81gensyms(N, I, [], A, U, V):-!,  J is I + 1,
   82	gensyms(N, J, A, A, U, V).
   83gensyms(N, I, [X|Xs], A, [Y|U], V):-!,  atom_concat(X, I, Y),
   84	N0 is N -1,
   85	gensyms(N0, I, Xs, A, U, V).
   86
   87% de Brujin indexing
   88% ?- debrujin(x\x, R), writeln(R).
   89% ?- debrujin(X\X, Y), writeln(Y), writeln(Y).
   90% ?- debrujin(x\x, Y), debrujin(x\x, Z), writeln(Y),writeln(Z).
   91% ?- debrujin(x\x\x, Y), writeln(Y).
   92% ?- debrujin(V\x\x\x\V, Y), writeln(Y).
   93% ?- debrujin(x\forall(y, f(x, y)), Y), writeln(Y).
   94% ?- debrujin(x\forall(y, f(x, y)+g(y, x)), Y), writeln(Y).
   95% ?- debrujin( x\(x=y), Y), writeln(Y).
   96% ?- debrujin( x\y, Y), writeln(Y).
   97% ?- debrujin( x\U, Y), writeln(Y).
   98% ?- debrujin( x\(x=y), Y), writeln(Y).
   99
  100%
  101debrujin(X, Y):- b_setval(scope_count, 0),
  102	debrujin(X, Y, []).
  103%
  104debrujin(X, Y, A):- compound(X),
  105	scope(X, V, Body, Y, #(K0), Body0), !,
  106	b_getval(scope_count, K),
  107	K0 is K + 1,
  108	b_setval(scope_count, K0),
  109	debrujin(Body, Body0, [V- #(K0)|A]).
  110debrujin(X, Y, A):- (	var(X); atomic(X)), !,
  111	(	assocq(A, X, Y) -> true
  112	;	Y = X
  113	).
  114debrujin(#(K), #(K), _):-!.
  115debrujin(X, Y, A):-
  116	functor(X, F, N),
  117	functor(Y, F, N),
  118	debrujin_args(1, X, Y, A).
  119%
  120debrujin_args(I, X, Y, A):- arg(I, X, U), !,
  121	debrujin(U, V, A),
  122	arg(I, Y, V),
  123	J is I + 1,
  124	debrujin_args(J, X, Y, A).
  125debrujin_args(_, _, _, _).
  126
  127% Scope
  128scope(\(V,B), V, B, \(V0,B0), V0, B0).
  129scope(iota(V, B), V, B, iota(V0, B0), V0, B0).
  130scope(forall(V, B), V, B, all(V0, B0), V0, B0).
  131scope(every(V, B), V, B, all(V0, B0), V0, B0).
  132scope(all(V, B), V, B, all(V0, B0), V0, B0).
  133scope(exists(V, B), V, B, some(V0, B0), V0, B0).
  134scope(some(V, B), V, B, some(V0, B0), V0, B0).
  135
  136%
  137shift(N, #(M), #(M1)):- !, M1 is M + N.
  138shift(N, T, T1) :- mapterm(shift(N), T, T1).
  139
  140% ?- alpha_equiv(x\x, y\y).
  141% ?- alpha_equiv(x\x, y\z).  % false.
  142alpha_equiv(X, Y):- debrujin(X, A), debrujin(Y, B), variant(A, B).
  143
  144% ?- rename_bound_vars(x\x, Y).
  145% ?- rename_bound_vars(forall(x, (x\x) = f(x)), Y).
  146% ?- rename_bound_vars(forall(X, (X\X) = f(X)), Y).
  147% ?- rename_bound_vars(forall(x, (x\x) = f(x)), U),
  148%	rename_bound_vars(forall(X, (X\X) = f(X)), V),
  149%	alpha_equiv(U, V).
  150% ?- rename_bound_vars(f(A,B,A),  X).
  151rename_bound_vars(X, Y):- debrujin(X, Z),
  152	b_getval(scope_count, N),
  153	debrujin_vars(N, MVs),
  154	qsubst(MVs, Z, Y).
L is unified with a list [#(V1), #(V2), ..., #(VN)] of fresh variabls Vi (i = 1,..., N). This list is used to substitute Debrujin idicies for renaming bounded varaibles to a unique fresh variables without the name conflict.
  163% ?- debrujin_vars(100, R), writeln(R).
  164debrujin_vars(0, []):-!.
  165debrujin_vars(N, MVs):-
  166	numlist(1, N, Ns),
  167	maplist(debrujin_var, Ns, Ms),
  168	length(Vs, N),
  169	zip(Ms, Vs, MVs).
  170%
  171debrujin_var(I, #(I)).
  172
  173% ptq_sgn([(\)/2, (\\)/2, iota/2, forall/2, exists/2
  174% ?- ptq_set(s, [john,walk], X), smash(X).
  175% ?- ptq_set(s, [john,walk], X).
  176% ?- ptq_set([john,walk], X), smash(X).
  177
  178ptq_set_cgi([C, X], S):-!, ptq_set(C, X, S).
  179
  180ptq_set(X, S):- ptq_set(s, X, S).
  181%
  182ptq_set(C, X, S):- ptq_all_(C, X, S0),
  183	term_smash0(["<font color=\"red\">", S0, "</font>"], S).
  184
  185ptq_all_(C, X, S):- setof(Y, ptq(C, X, Y), S1), !,
  186	maplist(term_smash0,S1,S2), insert("<br>",S2,S).
  187ptq_all_(_, _, "** Category  mismatch ?").
  188
  189%%% for cgi  %%%
  190% ?- ptq([john, walk], X).
  191% ?- ptq(s, [john, find, a, unicorn], X).
  192% ?- ptq_all(s, [john, find, a, unicorn], All).
  193
  194% ?- webchurch(p(a, b), X), smash(X).
  195ptq --> ptq(s).
  196
  197ptq_all --> ptq_all(s).
  198%
  199
  200ptq(C, X, Y):- parse(C, X, Z), ptq_normalize(Z, U),
  201			   ptq_simplify(U, Y).
  202%
  203ptq_all(C, X, Y):- findall(V,
  204					(	parse(C, X, Z),
  205						ptq_normalize(Z, U),
  206						ptq_simplify(U, V)
  207					),
  208					Y).
  209
  210
  211ptq_orig(C) -->  parse(C), !,
  212	simplify, !,
  213	sharp_to_print_name, !,
  214	pretty_print_html, !.
  215%
  216% ?- webchurch(plus@cn(1)@cn(2), R).
  217%@ R = ["&lambda;", [x], ["&lambda;", [y], ["(", [x], @|...]]] .
  218
  219webchurch(X, Y):- ptq_normalize(X, Z),
  220				  ptq_simplify(Z, U),
  221				  pretty_print_html(U, Y).
  222
  223% %
  224% webchurch_orig --> simplify,
  225% 	sharp_to_print_name, !,
  226% 	pretty_print_html, !.
  227
  228% ?- all_parse(s, [john, find, a, unicorn], X), maplist(writeln, X).
  229% ?- all_parse(s, [some, man, find, every, unicorn], X), maplist(writeln, X).
  230
  231all_parse(C, X, V):- findall(U, (	parse(C, X, Y),
  232									ptq_normalize(Y, Z),
  233									ptq_simplify(Z, U)
  234								),
  235								V).
  236
  237% ?- parse(np, [a, unicorn], X), ptq_normalize(X, R).
  238% ?- parse(s, [john,walk], X),	ptq_normalize(X, Y).
  239parse(C, X, Y):- call(C, Y, X, []), chk_normal(Y).
  240%
  241chk_normal(error(_,_,_)):- !, fail.
  242chk_normal(_).
  243
  244% DCG for a fragment of PTQ  (Lambda version)
  245
  246s(@(NP2,int(\(X,@(NP1,int(VP)))))) --> np(NP1), vp(VP,X,NP2).
  247% for 'specific' reading: Rule S14, T14
  248s(@(NP, int(VP))) --> np(NP), vp(VP).
  249% Rule S5, T5
  250
  251np(@(A, int(CN))) --> determiner(A), cn(CN).
  252np(PN) --> pn(PN).
  253
  254vp(ITV)  --> itv(ITV).
  255vp(@(TV, int(NP))) --> tv(TV), np(NP).
  256
  257vp(@(TV, int(\(P, @@(P,X)))), X, NP) --> tv(TV), np(NP).
  258
  259itv(walk)-->[walk].
  260
  261tv(find_star) --> [find].
  262tv(seek) --> [seek].
  263tv(\(P, \(X, @@(P, int(\(Y, X=Y)))))) --> [is].
  264
  265pn(\(P, @@(P, j))) --> [john].
  266pn(\(P, @@(P, b))) --> [bill].
  267
  268cn(unicorn) --> [unicorn].
  269cn(man) --> [man].
  270%
  271determiner(X\ (Y\ (exists(Z, @@(X,Z) & @@(Y,Z)))))-->[a].
  272determiner(X\ (Y\ (exists(Z, @@(X,Z) & @@(Y,Z)))))-->[some].
  273determiner(X\ (Y\ (forall(Z, @@(X,Z)-> @@(Y,Z)))))-->[every].
  274
  275%%% simplify expressions
  276% ?- simplify(exists(#1, man(#1) & (#1=john)), E), writeln(E).
  277% ?- simplify(true(first, second), E), writeln(E).
  278% ?- simplify(true, E), writeln(E).
  279variable(#(_)).
  280%
  281signature( \+ ((#)/1) ).
  282
  283%
  284ptq_normalize(X, Y):- expand_macro(X, Z),  % macros defined by def/2.
  285	ptq_reduce(Z, U),
  286	gensymvars([x,y,z], U),   % ala numbervars/1,3
  287	elim_redundant(U, Y).
  288%
  289ptq_reduce(X, Y):- elim_atmark_one(X, Z), !,  % completingt args.
  290	ptq_reduce(Z, Y).
  291ptq_reduce(X, Y):- ptq_macro_one(X, Z), !,
  292	ptq_reduce(Z, Y).
  293ptq_reduce(X, Y):- beta_one(X, Z), !,	% beta reduction.
  294	ptq_reduce(Z, Y).
  295ptq_reduce(X, X).
  296
  297%
  298elim_redundant(X, Y):- subterm(X, Y, Z, Z0),
  299	(	ssu(every(A, B), Z),
  300		\+ appear(A, B)
  301	;   ssu(some(A, B), Z),
  302		\+ appear(A, B)
  303	),
  304	!,
  305	Z0 = B.
  306elim_redundant(X, X).
  307
  308% ?- appear( a, f(a, b)).
  309appear(X, X).
  310appear(X, Y):- Y=..[_|Y0], member(Z, Y0), appear(X, Z).
  311
  312
  313
  314
  315%
  316ptq_macro_one(X, Y):- subterm(X, Y, A, B),
  317	 (	ptq_macro(A0, B0)
  318	 ;	meaning_postulate(A0, B0)
  319	 ),
  320	 ssu(A0, A),
  321	 B = B0.
  322%
  323completing_args(X, Y):- subterm(X, X0, Z, Z0),
  324	elim_atmark(A, B),
  325	ssu(A, Z),
  326	Z0 = B,
  327	!,
  328	completing_args(X0, Y).
  329completing_args(X, Y):- subterm(X, X0, Z, Z0),
  330	ssu(A@B, Z),
  331	!,
  332	complete_args(A, [B], Z0),
  333	completing_args(X0, Y).
  334completing_args(X, X).
  335
  336% PTQ marcros.
  337% ?- expand_ptq_macro(@@(int(p(a)),  x), R).
  338ptq_macro(@@(P, X), ext(P)@X).
  339ptq_macro(ext(int(X)), X).
  340
  341% Meaning postulate 4 (意味公準)
  342meaning_postulate(find_star@P@X, @@(P, int(Y\ find@Y@X))).
  343
  344% simplify -->
  345% 	ptq_reduce(expand_lambda_macro),
  346% 	debrujin,
  347% 	ptq_reduce(ptq_rule),
  348% 	ptq_reduce(redex_to_term),
  349% 	ptq_reduce(elim_redundant),
  350% 	ptq_reduce(paramodulation),
  351% 	ptq_reduce(identity),
  352% 	ptq_reduce(elim_redundant),
  353% 	ptq_reduce(boole).
  354
  355
  356ptq_simplify(X, Y):- subterm(X, U, Z, Z0),
  357	boole(A, B),
  358	ssu(A, Z),
  359	Z0 = B,
  360	!,
  361	ptq_simplify(U, Y).
  362ptq_simplify(X, Y):- subterm(X, U, Z, Z0),
  363	ssu(_=_, Z),
  364	Z = (A = B),
  365	A == B,
  366	!,
  367	Z0 = true,
  368	!,
  369	ptq_simplify(U, Y).
  370ptq_simplify(X, X).
  371
  372% ?- qsubst([a-1, b-2], f(a,b,a), R).
  373qsubst(M, X, Y):-
  374	(	member(P, M), arg(1, P, A), A==X ->
  375		arg(2, P, Y)
  376	;	compound(X)	->
  377		functor(X, F, N),
  378		functor(Y, F, N),
  379		qsubst_args(1, M, X, Y)
  380	;	Y = X
  381	),
  382	!.
  383%
  384qsubst_args(I, M, X, Y):- arg(I, X, A), !,
  385	arg(I, Y, B),
  386	qsubst(M, A, B),
  387	J is I + 1,
  388	qsubst_args(J, M, X, Y).
  389qsubst_args(_, _, _, _).
  390
  391% PTQ表示規約 f@a= f(a).   (f@y)@x = f(x, y)
  392% ?- redex_to_term(f@y, E).
  393%@ E = f(y).
  394% ?- redex_to_term(f@y@z, E).
  395
  396% ?- reduce(ptq:redex_to_term, (f@y)@x, E).
  397
  398% redex_to_term(X@Y, Z):-
  399% 	L = [exists(_,_), forall(_,_), #(_), ext(_), int(_),
  400% 	     @@(_,_), @(_,_)],
  401% 	\+ member(X, L),
  402% 	X=..[F|X0],
  403% 	Z=..[F,Y|X0].
  404% ?- listing(variable).
  405%
  406paramodulation(exists(X, B), exists(X, B0)):-
  407	select_eq_conj(B, X=R, B1),
  408	beta:beta_subst([(X,R)], B1, B0).
  409%
  410select_eq_conj(L=R, L=R, true):- variable(L).
  411select_eq_conj(L=R, R=L, true):- variable(R).
  412select_eq_conj(A&B, E, A0&B):- select_eq_conj(A, E, A0).
  413select_eq_conj(A&B, E, A&B0):- select_eq_conj(B, E, B0).
  414%
  415identity(X = Y, true):- X == Y.
  416%
  417% ?-  reduce(boole, true & false, X).
  418% ?-  reduce(boole, true & true, X).
  419% ?-  reduce(boole, or(true, false), X).
  420boole((A&B)&C, A&(B&C)).
  421boole(true&A, A).
  422boole(A&true, A).
  423boole(_&false, false).
  424boole(false&_, false).
  425boole(not(not(X)), X).
  426boole(or(_,true), true).
  427boole(or(true,_), true).
  428boole(or(false,A), A).
  429boole(or(A, false), A).
  430boole(not(true), false).
  431boole(not(false), true).
  432%
  433% #(1) -> x; #(2) -> y; ....
  434% ?- sharp_to_print_name(f(#1, #3), X).
  435sharp_to_print_name(X, X):- var(X), !.
  436sharp_to_print_name(#(I), X):-
  437	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),
  438	!.
  439sharp_to_print_name(#(I), #(J)):- !, number_codes(I,J).
  440sharp_to_print_name(T, T0):- T=..[F|A],
  441	maplist(sharp_to_print_name, A, A0),
  442	T0 =.. [F|A0].
  443%
  444elim_atmark(exists(X, P)@Y, exists(X, P@Y)).
  445elim_atmark(forall(X, P)@Y, forall(X, P@Y)).
  446elim_atmark(ext(X)@Y, ext(X@Y)).
  447elim_atmark(int(X)@Y, int(X@Y)).
  448elim_atmark(@@(X)@Y, @@(X@Y)).
  449%
  450elim_atmark_one(X, Y):- subterm(X, Y, Z, Z0),
  451	(	elim_atmark(A, B),
  452		ssu(A, Z),
  453		Z0 = B
  454	;	ssu(A@B, Z),
  455		nonvar(A),
  456		functor(A, F, _),
  457		dict_v(F),
  458		complete_args(A, [B], Z0)
  459	).
  460% ?- normalize(first@(pair@a@b), Y).
  461% ?- normalize(second@(pair@a@b), Y).
  462% ?- normalize((x\x)@a, Y).
  463% ?- normalize(succ@cn(1), Y), pp(Y).
  464% ?- normalize(succ@cn(2), Y), pp(Y).
  465% ?- normalize(succ@cn(10), Y), pp(Y).
  466% ?- normalize(plus@cn(1)@cn(1), Y).
  467% ?- normalize(plus@cn(2)@cn(3), Y).
  468% ?- normalize(plus@cn(3)@cn(4), Y).
  469% ?- normalize(plus@ (f\x\ f@f@x)@(f\x\ f@x), Y).
  470% ?- normalize(plus@ (f\x\ f@f@x)@(g\y\ g@g@y), Y).
  471% ?- normalize(mult@cn(1)@cn(2), Y).
  472% ?- normalize(mult@cn(1)@cn(1), Y).
  473% ?- normalize(one, Y).
  474% ?- normalize(mult, Y).
  475% ?- normalize(three, Y).
  476% ?- normalize(mult@cn(1)@cn(2), Y).
  477% ?- normalize(mult@(cn(2)@cn(1)), Y).
  478% ?- normalize(mult@(cn(3)@cn(1)), Y).
  479% ?- normalize(mult@(cn(4)@cn(3)), Y).
  480% ?- normalize(cn(2), R), normalize(f\x\ (((R@R)@f)@x), A).
  481% ?- normalize((mult(3, cn(3))), Y).
  482% ?- normalize((mult@(cn(1)@cn(2)))@cn(0), Y).
  483% ?- normalize((mult@(cn(1)@cn(2))), Y).
  484% ?- normalize(g\((f\x\f@f@x)@(g@g)), R).
  485% ?- normalize(g\((f\x\f@f@x)@(g@g@g)), R).
  486% ?- normalize(mul, R), church_numeral(1, One), church_numeral(2, Two),
  487%	normalize(R@One@Two, U).
  488% ?- X=1, Y=2, normalize(mul, R), church_numeral(X, One),
  489%	church_numeral(Y, Two), normalize(R@One@Two, U).
  490% ?- X=100, Y=100, normalize(mul, R),
  491%  church_numeral(X, One), church_numeral(Y, Two),normalize(R@One@Two, U).
  492% ?- normalize(X\(Y\X), R).
  493% ?- normalize(X\ ((Y\ (X@Y)@1)), R), normalize(R, S).
  494% ?- normalize((X\ (Y\X))@1, R).
  495% ?- normalize((X\X)@1, R).
  496
  497% Example. Recursive factorial by ycombinator.
  498
  499%	For  0! = 1.
  500% ?- normalize((ycombinator@factorial)@cn(0), R), pp(R).
  501%@ A\B\A@B
  502%	For  1! = 1.
  503% ?- normalize((ycombinator@factorial)@cn(1), R), pp(R).
  504%@ A\B\A@B
  505%	For  2! = 2.
  506% ?- normalize((ycombinator@factorial)@cn(2), R), pp(R).
  507%@ A\B\A@(A@B)
  508%	For 3! = 1 x 2 x 3 = 6.
  509% ?- normalize((ycombinator@factorial)@cn(3), R), pp(R).
  510%@ A\B\A@(A@(A@(A@(A@(A@B)))))
  511%	For 4! = 1 x 2 x 3 x 4 = 24.
  512% ?- time(normalize((ycombinator@factorial)@cn(4), R)), pp(R).
  513%@ % 498,812,621 inferences, 42.238 CPU in 42.255 seconds (100% CPU, 11809528 Lips)
  514%@ A\B\A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@B)))))))))))))))))))))))
  515
  516%
  517normalize(X, Y):- expand_macro(X, Z),
  518	beta_normal_form(Z, Y).
  519
  520expand_macro(X, Y):- subterm(X, Z, A, B),
  521	 nonvar(A),
  522	 def(A, B0),
  523	 !,
  524	 rename_bound_vars(B0, B),
  525	 expand_macro(Z, Y).
  526expand_macro(X, Y):- rename_bound_vars(X, Y).
  527
  528
  529%
  530beta_normal_form(X, Y):- beta_one(X, X0), !,
  531	beta_normal_form(X0, Y).
  532beta_normal_form(X, X).
  533%
  534ssu(X, Y):- subsumes_term(X, Y), X = Y.
  535%
  536beta_one(X, Y):- subterm(X, Y, X0, Y0),
  537	  	ssu((U\V) @ W, X0),
  538		U = W,
  539		rename_bound_vars(V, Y0).
  540%
  541dict_v(walk).
  542dict_v(find).
  543dict_v(seek).
  544dict_v(man).
  545dict_v(unicorn).
  546
  547% ?- ssu(f(X, Y),f(U, U)).
  548% ?- ssu(f(U,U),f(X, Y)). % false
  549% ?- normalize(mul@cn(2)@cn(1), X), pp(X).
  550% ?- normalize(mul@cn(2)@cn(2), X), pp(X).
  551% ?- normalize(mul@cn(3)@cn(2), X), pp(X).
  552% ?- normalize(mul@cn(3)@cn(3), X), pp(X).
  553% ?- expand_macro(mul@cn(3)@cn(3), X), pp(X).
  554% ?- normalize((mul@cn(4))@cn(3), X), pp(X).
  555% ?- E= (a\b\c\d\a@b@c@d)@(e\f\e@(e@(e@(e@f))))@(g\h\g@(g@(g@h))),
  556%	normalize(E, R).
  557% ?- expand_macro(mul@cn(3)@cn(3), X), rename_bound_vars(X, X0),
  558%	pp(X0),  normalize(X0, Y), pp(Y).
  559%@ (A\B\C\D\A@B@C@D)@(E\F\E@(E@(E@F)))@(G\H\G@(G@(G@H)))
  560% ?- Exp = ((A\B\C\D\A@B@C@D)@(E\F\E@(E@(E@F)))@(G\H\G@(G@(G@H)))),
  561%	normalize(Exp, R).
  562%@ Exp = R, R = (A\B\C\D\A@B@C@D)@(E\F\E@(E@(E@F)))@(G\H\G@(G@(G@H))).
  563% ?- trace.
  564% ?- normalize((x\y\z\u) @ a @ b @ c, R).
  565%@ R = u.
  566% ?- write_canonical((x\y\z\u) @ a @ b @ c).
  567%@ @(@(@(\(x,\(y,\(z,u))),a),b),c)
  568
  569
  570% ?- normalize(iszero@cn(0), R), normalize(true, S), alpha_equiv(R, S).
  571% ?- normalize(pred@cn(2), R), normalize(cn(1), S), alpha_equiv(R, S).
  572% ?- N=10000, between(1, N, I), J is I +1, once(equal(succ@cn(I), cn(J))).
  573% ?- N=10000, between(1, N, I), J is I +1, once(equal(succ@cn(I), cn(I))).
  574
  575% ?- normalize(fst@cn(1)@cn(2), R).
  576% ?- normalize(snd@cn(1)@cn(2), R).
  577% ?- normalize(if@true@cn(1)@cn(2), R).
  578% ?- normalize(if@false@cn(1)@cn(2), R).
  579% ?- normalize(and@true@true, R).
  580% ?- normalize(and@false@true, R).
  581% ?- normalize(and@true@true, R).
  582% ?- normalize(and@false@false, R).
  583% ?- normalize(or@true@true, R).
  584% ?- normalize(or@true@false, R).
  585% ?- normalize(or@false@true, R).
  586% ?- normalize(or@false@false, R).
  587% ?- normalize(not@true, R).
  588% ?- normalize(not@false, R).
  589% ?- normalize(succ@cn(1), R).
  590% ?- normalize(plus@cn(1)@cn(2), R).
  591% ?- normalize(pred@cn(2)@cn(1), R).
  592% ?- normalize(mult@cn(2)@cn(3), R).
  593% ?- normalize(mult@cn(3)@cn(2), R), pp(R).
  594% ?- normalize(mult@cn(3)@cn(3), R), pp(R).
  595% ?- normalize(mult@cn(7)@cn(5), R), pp(R).
  596% ?- normalize(pred@cn(2), R), pp(R).
  597% ?- normalize(pred@cn(1), R), pp(R).
  598% ?- normalize(pred@cn(0), R), pp(R).
  599% ?- normalize(pred@cn(5), R), pp(R).
  600% ?- rename_bound_vars(x\ ((x\x)@x), R).
  601% ?- rename_bound_vars(f(x\ ((x\ (x@x))@x), x\ ((x\ (x@x))@x)) , R).
  602% ?- rename_bound_vars(forall(x, f(x, x\ ((x\ (x@x))@x), x\ ((x\ (x@x))@x))) , R), pp(R), pp(R).
  603
  604% ?- time(normalize(cn(3) @ step @ (pair@cn(0)@cn(1))@snd, R)), pp(R).
  605% ?- time(normalize(cn(4) @ step @ (pair@cn(0)@cn(1))@snd, R)), pp(R).
  606%@ A\B\A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@(A@B)))))))))))))))))))))))
  607
  608pp(X):- \+ (\+ (numbervars(X), writeln(X))).
  609%
  610equal(X, Y):- normalize(X, U), normalize(Y, V), alpha_equiv(U, V).
  611%
  612% 関数定義 (将来拡張用)
  613def(cn(N), CN):- church_numeral(N, CN).
  614def(fst, x\y\x).
  615def(snd, x\y\y).
  616def(first, p\p@fst).
  617def(second, p\p@snd).
  618def(true, x\y\x).
  619def(false, x\y\y).
  620def(and, x\y\ (x @ y @ false)).
  621def(or, x\y\ (x @ true @ y)).
  622def(not, x\ (x @ false @ true)).
  623def(if, x\y\z\ (x @ y @ z)).
  624def(succ, n\f\x\ (f @ (n @ f @ x))).
  625def(pred, n\f\x\ (n @ (g \ h \ ( h @ (g @ f))) @ (u \ x) @ (u \ u))).
  626def(plus, m\n\f\x\ ( m @ f @ (n @ f @ x))).
  627def(mult, m\n\ (m @ (plus @n) @ cn(0))).
  628def(iszero, n\ (n@ (x \ false) @ true)).
  629def(zero, cn(0)).
  630def(one, cn(1)).
  631def(two, cn(2)).
  632def(three, cn(3)).
  633def(cons, f\s\b\ (b @ f @s)).
  634def(car, p\ (p @ true)).
  635def(cdr, p\ (p @ false)).
  636def(factorial, f\n\ (if@(iszero@n)@cn(1)@ (mult@n @ (f @ (pred@n))))).
  637def(ycombinator,  f\ ((x\ (f @ (x @ x))) @ (x\ (f @ (x @ x))))).
  638def(pair, a\b\f\ f @ a @ b).
  639def(step, x\ (pair @ (succ @ (first @x)) @ (mult@(succ@ (first@ x))@ (second@ x)))).  % by J. Burse
  640
  641% ?- normalize(cn(2) @ (x\ mult @x @x) @ch(1), R), pp(R).
  642% ?- normalize(cn(2) @ (x\ succ@ x) @cn(1), R), pp(R).
  643% ?- normalize(cn(3) @ (x\ plus@ x@ x) @cn(1), R), pp(R).
  644% ?- normalize(cn(4) @ (x\ plus@ x@ x) @cn(1), R), pp(R).
  645% ?- normalize(cn(4) @ (x\ mult @ x@ x) @cn(2), R), pp(R).
  646% ?- normalize(cn(2) @ (x\ mult @ x@ x) @cn(2), R), pp(R).
  647% ?- time(normalize(cn(3) @ (x\ mult @ x@ x) @cn(2), R)), pp(R).
  648
  649% ?- church_numeral(0, CN).
  650% ?- church_numeral(1, CN).
  651% ?- church_numeral(2, CN), pp(CN).
  652church_numeral(N, CN) :- church_numeral(N, CN, _, _).
  653
  654% ?- church_numeral(20, CN, F, X).
  655church_numeral(0, F\X\X, F, X).
  656church_numeral(N, F\X\(F@M), F, X):- N > 0,	N0 is N-1,	church_numeral(N0, F\X\M, F, X).
?- sharp_to_print_name(exists(#1, man(#1)), X), pretty_print_html(X, Y), smash(Y). pretty_print_html --> eval(#m(ev, pretty_print_html, ptq)). pretty_print_html(X, Y):- once(eval([ptq:pretty_print_html], X, Y)).
  665pretty_print_html(A, [A]):- atomic(A), !.
  666pretty_print_html(X, Y):- X=..[F|A],
  667			length(A, N),
  668			maplist(pretty_print_html, A, B),
  669			pretty_print_html0(F, N, B, Y).
  670
  671pretty_print_html0(exists, 2, [A, B], ["&exist;", A, B]).
  672pretty_print_html0(forall, 2, [A, B], ["&forall;", A, B]).
  673pretty_print_html0((\), 2, [A, B], ["&lambda;", A, B]).
  674pretty_print_html0((&), 2, [A, B], ["(", A, "&and;", B,")"]).
  675pretty_print_html0((or), 2, [A, B], ["(", A, "&or;", B,")"]).
  676pretty_print_html0((not), 1, [A], ["(","&not;", A, ")"]).
  677pretty_print_html0((->), 2, [A,B], ["(",A, "&rarr;", B, ")"]).
  678pretty_print_html0(F, 2, [A, B], ["(", A, F, B, ")"]):- declared_op(F, 2).
  679pretty_print_html0(F, 1, [A], ["(", F, A, ")"]):- declared_op(F, 1).
  680pretty_print_html0(F, _, L0, [F, "(", L , ")" ]):- insert(",", L0, L).
  681
  682%
  683declared_op(X,N):- current_op(_,T,X),
  684	( N=2, memberchk(T, [xfx,xfy,yfx,yfy])
  685	; N=1, memberchk(T, [fx, fy])
  686	)