Recursive or self-referential definitions are not needed to write a recursive function in lambda calculus!
The function Y gives the effect of recursion.
Y is known as the paradoxical operator or as the fixed-point operator.
Y = λG.(λg.G(g g))(λg.G(g g))
For example, a factorial program can be written with no recursive declarations, in fact with no declarations at all.
A fixed-point operator is a higher-order function that computes a fixed point of other functions.
It allows the implementation of recursion in the form of a rewrite rule, without explicit support from the language's runtime engine.
where
- A higher-order function, which is a function which does at least one of the following: (i) take one or more functions as an input, and (ii) output a function.
- A fixed point of a function, which is a point that is mapped to itself by the function.
That is to say,
x is a fixed point of the function f if and only if f(x)=x.
First note that YF=F(YF); YF is a fixed-point of F.
Y F
= ( λG.(λg.G(g g))(λg.G(g g)) ) F
⇒β (λg.F(g g)) (λg.F(g g))
⇒β F( (λg.F(g g))(λg.F(g g)) )
= F( Y F )