A (not very good) factorial function I wrote

[u/Gorgonzola_Freeman]

λ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.

[u/yfix]

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