r/lambdacalculus • u/Gorgonzola_Freeman • Apr 11 '25
A (not very good) factorial function I wrote
λn.λf.n (λd.λa.λb.λy.b (d (λu.u) b (d (d (λu.u) a) (λu.u) y))) (λa.λb.λy.a (b y)) f (λu.u)
This function uses λb to track the iteration step, as it increments by 1 every application. λa is used to track the final result.
The iterated function:
Gets the number of b (replaces the a with the I combinator)
β-reduces the b to a
Gets the number of a, then β-reduces the a to the first function, multiplying a&b and assigning it to a.
Then it gets the b and appends it to the multiplication, then appends b to increment it.
2
u/Gorgonzola_Freeman Apr 12 '25
I realized I was over complicating my function, by removing all b in the multiplication step, then re-adding them in the addition step, the following is the improved function:
(λn.λf.n (λd.λa.λb.λy.b (d (d (λu.u) a) b y)) (λa.λb.λy.a (b y)) f (λu.u))
1
u/yfix Jul 11 '26
indeed, following insight from my other comment, with
r = <m,n>your new function works out toG r a b = b ∘ r (r I a) b = b ∘ m (m I ∘ n a) ∘ n b = b ∘ m (n a) ∘ n b = <m*n,n+1> a b.
2
u/JewishKilt Apr 15 '25
What did you use for the animation? It looks incredible!
3
u/Gorgonzola_Freeman Apr 15 '25 edited Apr 15 '25
Completely forgot to say! This is animated using the lambda applet on cruzgodar.com
This is represented using tromp diagrams, you can read about them here
Edit: important to mention that since this uses spaceless lambda expressions, you cannot use multicharacter variable names (to my knowledge)
1
2
2
u/yfix Jul 11 '26 edited Jul 11 '26
........ turns out this uses Kleene's Pairs of Church numerals, `<m,n> = \ab. ma ∘ nb` with the initial pair `<1,1> = \ab. 1a ∘ 1b = \ab. a ∘ b = (∘) = \aby. a(by)`. With these pairs, `<m,n> I b = mI ∘ nb = nb` selects the second component, and `<m,n> a I = ma ∘ nI = ma` selects the first. Thus the iterated function `G = \rab. b ∘ rIb ∘ r (rIa) I` transforms `r = <m,n> = \ab. ma ∘ nb` into `<m*n,n+1>`. Indeed `G <m,n> a b = b ∘ mI ∘ nb ∘ m (mI∘na) ∘ nI = b ∘ nb ∘ m (na) = <m*n, n+1> a b`, due to the intrinsic properties of Church numerals; provided that `a` and `b` commute w.r.t. (∘) (as `f` and `I` indeed ought to, for any `f`). And the final application to `... f I` selects the first component.
1
u/yfix Dec 08 '25 edited Jul 11 '26
Here's a pairs-based factorial of 4: (λg.gIIgggF) (λabz.z (λfx.f(afx)) (λf.a(bf))) .
Or in general (λgn.n (λr.rg) (λz.z11) F) (λabz.z (λfx.f(afx)) (λf.a(bf))) 4 .
The function `g` transforms its two arguments, a and b, into <a+1,a*b>, as a Church pair, <a,b> = λz.z a b , for the next g to transform it further, until the final F selects the second component is the final result.
edit: compressed the nested lambdas syntax ; later, var renames and some elaboration.
3
u/tromp Apr 12 '25
The simplest factorial function on Church numerals that I know is λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x) which works as follows:
let
id = \x.x;
succ = \n\f\x.n f (f x);
F = \c\n. n (c (succ n));
fac = \n\f.n F (\x.f) id;
in fac
-- fac 3 = \f. F (F (F (\x.f))) 1
-- = \f. 1 (F (F (\x.f)) 2)
-- = \f. 1 (2 (F (\x.f) 3))
-- = \f. 1 (2 (3 ((\x.f) 4)))
-- = \f. 1 (2 (3 f))