Slide 12.14: Recursive functions

Slide 12.13: Declarations
Slide 12.15: Recursive functions (cont.)
Home

Recursive Functions

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 )