Let’s say you build a function for factorial, using applied lambda calculus (extra functions). For factorial — if x is 0, return 1, otherwise return x × factorial (n-1)
Basic function:
factorial := λx.(iszero x) c₁ (mult x (factorial (n-1)))
The problem is, it has factorial in its definition. It can’t. So abstract it.
factorial := (λa.λx.(iszero x) c₁ (mult x (a (n-1))) ) factorial
We can then divide it into two parts:
F := λa.λx.(iszero x) c₁ (mult x (a (n-1))) factorial := F factorial
Then use a fixed point combinator.
factorial := Y F