Exercise on normalizing Ycombinator for factorial function in Church numerals

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),
	 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.

1 Like

Instead of Y fixpoint combinator, why not primitive recursion
combinator R. You already have church numerals. Shouldn’t be
so difficult to define recursion combinator R? Actually I didn’t try it yet.

But the problem is with Y combinator, you don’t know
whether a recursion terminates. It does for factorial, but
otherwise? On the other hand a a primitive recursion combinator

R always terminates. It produces a function f from two functions
g and h that satisfies this primitive recursion schema:

f(0, x) = g(x)
f(n+1, x) = h(n, x, f(n,x))

If g and h terminate, then f terminates as well, and is unique. This
is the so called Recursion Theorem, the idea was first
expounded by Dedekind in 1888 in the context of arithmetic.

For the simple case when h has no further parameters n,x
and g is the identity function, we have f(n, x) = h^n(x), lets say
we write this as (R h) n x, and use church numerals for n then we have:

/* for church numerals */
R = λh n x.(n x h) 

See also:


Things go well for addition and multiplication:

plus = R succ
mult = λn m.(R (plus n)) m 0

But factorial has not a simple h, it uses the parameter n. So
we need a better recursion combinator R, is this possible?
Maybe juggling with pairs?

I agree, though I missed to use the combinator R. I will try R later.

Thanks for comment. I learned in the literature K. Goedel is the founder of primitive recursive function, who used it as a key to internalize arithmetic to prove the famous incompleteness theorem I of theory which includes arithmetic (induction). It is impressive that Dedekind already noticed the notion about 50 years before K. Goedel used it.

Dedekind wasn’t possibly aware that there is the distinction between
primitive recursive and μ-recursive. Even David Hilbert had the strong
believe that every computable function is primitive recursive, until in 1926

Wilhelm Ackerman proved the contrary. A more down to earth naming instead
of primitive recursive and μ-recursive would be LOOP-programs versus
WHILE-programs. The Ackerman function can be used to show that it can

only be implemented via a WHILE-program and not with a LOOP-program.
But then the R combinator can show that the Ackerman function can be
nevertheless be implemented with a higher order (λ calculus) LOOP-program.

Edit 28.02.2023
BTW: Here is an idea to use the R combinator so as to also do the
factorial example. What if we would iterate pairs of the form:

<0, 0!>, <1, 1!>, <2, 2!>, ..., <n, n!>

We define a step function for the above pair iteration, obtaining the
elimination of parameters. I don’t find the pair constructor in your
def/2 that works with fst and snd of your def/2, so I mention

pair explicitly here for usage in step:

pair = λa b f. (f a) b
step = λx. pair (succ (fst x)) (mult (succ (fst x)) (snd x))

And armed with step we can define:

factorial = λn. snd ((R step) n (pair 0 1))

Yes or No?

But Haskell is not the only language that provides higher order
programming. Prolog can do the same, it is even part of the ISO
core standard now. The predicate call/n made it into a corrigendum:

8.15.4 call/ 2…8
These built-in predicates provide support for higher-order programming.

Here is the Y combinator in Prolog, its just the
Haskell fix translated from functional into relational:

/* Y combinator */
fix(F,N,X) :- call(F,fix(F),N,X).

factorial(_,0,1) :- !.    % attention, not steadfast
factorial(F,N,X) :- M is N-1, call(F,M,Y), X is N*Y.

Works fine:

?- call(fix(factorial),10,X).
X = 3628800.

And here the R combinator in Prolog, not using
church numerals, but the Dedekind form:

/* R combinator */
natrec(_, 0, X, X) :- !.    % attention, not steadfast
natrec(F, N, X, Z) :- M is N-1, natrec(F, M, X, Y), call(F, Y, Z).

step((X,Y),(Z,T)) :- Z is X+1, T is Z*Y.

factorial(X,Y) :- natrec(step,X,(0,1),(_,Y)).

Works also fine:

?- factorial(10,X).
X = 3628800.

Homework: Define a more tail recursion friendly form
of the R combinator using an accumulator.

Actually before I reached to work the ycombinator for factorial, I had tried the macro def for factorial as this

def(factorial, n\ (if@(iszero@n)@cn(1)@ (mult@n @ (rec(factorial) @ (pred@n))))).

And I saw it works with modifying beta_one rule to expand rec(factorial) according to the def rule for factorial. However I felt it was not an exercise on pure lambda calculus because of non pure construct rec(_) .

I am not sure for now that your recursion term ‘R’ works for pure lambda calculus on factorial in church numerals without using impure construct like call/rec. I need time to learn again lambda calculus.

Suppose def/2 for factorial, ycombinator, and your ‘R’ I guess.

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))))).
def('R', h\n\x\ (n@x@h)).

Then, this is just query log that you would like to see.

% ?- normalize(('R'@factorial)@cn(3), R), pp(R).
%@ A\A@(A@(A@(B\C\C@(D\E\F\F)@(G\H\G)@(I\J\I@J)@(C@(K\L\M\B@(N\O\C@(P\Q\Q@(P@N))@(R\O)@(S\S))@L@(K@L@M))@(T\U\U)))))
%@ R = (_A\_A@(_A@(_A@(_B\_C\ ... @ ... @ (... \ ...)@(_F\ ... \ ...)@(_C@(... \ ...)@(_\ ... \ ...)))))).

while ycombinator instead of ‘R’ works as posted.

% ?- normalize((ycombinator@factorial)@cn(3), R), pp(R).
%@ A\B\A@(A@(A@(A@(A@(A@B)))))
%@ R = (_A\_B\_A@(_A@(_A@(_A@(_A@(_A@_B)))))).

I may be missing your points. Could you show an exact query you would like to run to see the result ?

I see. So, adding these

def(pair, a\b\f\ f@ a @ b).
def(step, x\ pair @ (succ @ (fst @x)) @ (mult@(succ@ (fst@ x))@ (snd@ x))).
def(jfactorial, n\ snd @ (('R'@ step)@ n @(pair @ cn(0) @ cn(1)))).
def('R', h\n\x\ n@x@h).


% ?- write_canonical(h\n\x\ n@x@h).
%@ \(h,\(n,\(x,@(@(n,x),h))))

I ran the query without thought, to get the result, which
is something wrong.

% ?- normalize(('R'@jfactorial)@cn(3), R), pp(R).
%@ A\A@(A@(A@(B\C\C)))
%@ R = (_A\_A@(_A@(_A@(_\_B\_B)))).

Anyway, your pair, step, (j)factorial and R seems pretty pure, I agree. I would like to see them in details.

I got expected result as you said. Thanks.

I added macros first and second as this,

def(first, p\p@fst).  
def(second, p\p@snd). 

and modified step to use them instead of fst and snd:

def(step, x\ (pair @ (succ @ (first @x)) @ (mult@(succ@ (first@ x))@ (second@ x)))).
% ?- time(normalize(cn(3) @ step @ (pair@cn(0)@cn(1))@snd, R)), pp(R).
%@ % 7,662,777 inferences, 0.629 CPU in 0.630 seconds (100% CPU, 12176165 Lips)
%@ A\B\A@(A@(A@(A@(A@(A@B)))))

% ?- time(normalize(cn(4) @ step @ (pair@cn(0)@cn(1))@snd, R)), pp(R).
%@ % 66,319,760 inferences, 5.548 CPU in 5.551 seconds (100% CPU, 11952754 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)))))))))))))))))))))))

Church numerals are power of function f, indeed : f^n(x) = f(f(...(x)...))

1 Like

Thanks for comments on my macro definition def/2. In fact
I share similar questions with you. Some of these macros are used in my old Prolog CGI on fragment of R. Montague’s PTQ, which I found recently broken. It is time for me to review
the cgi codes from scratch including the macros definition. In particular, I am interested in the macro pair, which was missed in the list of mine.

Yes. subterm/4, 5 is for general purpose simplifier , based on Prolog backtracking. It is convenient for trying experimental converter easily. Also slowness comes from rename_bound_vars/2, which is debrujin indexing (renaming bound variables). I found it is necessary for each beta-reduction. For example, when substituting lambda term to a large church-numeral !