I left memo on macros for simple lambda calculus at one of my codes in library(pac) as the future work. In fact, I remember I was not successful to calculate the popular recursive factorial
n! = 1 x 2 x ... x n using ycombinator. So I have challanged again here. Fortunately this time it is successful, which is also a surprise for me. I did not expect it works, though based on my very limited knowledge about ycombinator.
This is that memo with fixing typos. The macros factorial and ycombinator are at the last two lines of the def/2 predicate.
:- op(670, xfy, \).
% macros
def(cn(N), CN):- church_numeral(N, CN).
def(fst, x\y\x).
def(snd, x\y\y).
def(true, x\y\x).
def(false, x\y\y).
def(and, x\y\ (x @ y @ false)).
def(or, x\y\ (x @ true @ y)).
def(not, x\ (x @ false @ true)).
def(if, x\y\z\ (x @ y @ z)).
def(succ, n\f\x\ (f @ (n @ f @ x))).
def(pred, n\f\x\ (n @ (g \ h \ ( h @ (g @ f))) @ (u \ x) @ (u \ u))).
def(plus, m\n\f\x\ ( m @ f @ (n @ f @ x))).
def(mult, m\n\ (m @ (plus @n) @ cn(0))).
def(iszero, n\ (n@ (x \ false) @ true)).
def(zero, cn(0)).
def(one, cn(1)).
def(two, cn(2)).
def(three, cn(3)).
def(cons, f\s\b\ (b @ f @s)).
def(car, p\ (p @ true)).
def(cdr, p\ (p @ false)).
def(factorial, f\n\ (if@(iszero@n)@cn(1)@ (mult@n @ (f @ (pred@n))))).
def(ycombinator, f\ ((x\ (f @ (x @ x))) @ (x\ (f @ (x @ x))))).
Queries on ycombinator(factorial).
% Recursive factorial by ycombinator.
% For 0! = 1.
% ?- normalize((ycombinator@factorial)@cn(0), R), pp(R).
%@ A\B\A@B
% For 1! = 1.
% ?- normalize((ycombinator@factorial)@cn(1), R), pp(R).
%@ A\B\A@B
% For 2! = 2.
% ?- normalize((ycombinator@factorial)@cn(2), R), pp(R).
%@ A\B\A@(A@B)
% For 3! = 1 x 2 x 3 = 6.
% ?- normalize((ycombinator@factorial)@cn(3), R), pp(R).
%@ A\B\A@(A@(A@(A@(A@(A@B)))))
% For 4! = 1 x 2 x 3 x 4 = 24.
% ?- time(normalize((ycombinator@factorial)@cn(4), R)), pp(R).
%@ % 498,812,621 inferences, 42.238 CPU in 42.255 seconds (100% CPU, 11809528 Lips)
%@ 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)))))))))))))))))))))))
Here is main codes for this exersise post. Predicates not listed
here (e.g. subterm/4, rename_bound_vars/2) are defined in library(pac) with different names, which are independent of lambda calculus.
%
normalize(X, Y):- expand_macro(X, Z),
beta_normal_form(Z, Y).
%
beta_normal_form(X, Y):- beta_one(X, X0), !,
beta_normal_form(X0, Y).
beta_normal_form(X, X).
%
ssu(X, Y):- subsumes_term(X, Y), X = Y.
%
beta_one(X, Y):- subterm(X, Y, X0, Y0),
ssu((U\V) @ W, X0),
U = W,
rename_bound_vars(V, Y0).
%
expand_macro(X, Y):- subterm(X, Z, A, B),
nonvar(A),
def(A, B0),
!,
rename_bound_vars(B0, B),
expand_macro(Z, Y).
expand_macro(X, Y):- rename_bound_vars(X, Y).
%
pp(X):- \+ (\+ (numbervars(X), writeln(X))).
% ?- church_numeral(0, CN).
% ?- church_numeral(1, CN).
% ?- church_numeral(2, CN), pp(CN).
church_numeral(N, CN) :- church_numeral(N, CN, _, _).
%
church_numeral(0, F\X\X, F, X).
church_numeral(N, F\X\(F@M), F, X):- N > 0,
N0 is N-1,
church_numeral(N0, F\X\M, F, X).
I enjoyed this exercise, but I believe there are many similar codes on the net for calculating ycombinator(factorial) even in Prolog.
