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.