Anonymous recursion
A fixed-point combinator is a higher-order function fix
that by definition satisfies the equivalence
forall f. fix f = f (fix f)
fix f
represents a solution x
to the fixed-point equation
x = f x
The factorial of a natural number can be proved by
fact 0 = 1
fact n = n * fact (n - 1)
Using fix
, arbitrary constructive proofs over general/μ-recursive functions can be derived without nonymous self-referentiality.
fact n = (fix fact') n
where
fact' rec n = if n == 0
then 1
else n * rec (n - 1)
such that
fact 3
= (fix fact') 3
= fact' (fix fact') 3
= if 3 == 0 then 1 else 3 * (fix fact') (3 - 1)
= 3 * (fix fact') 2
= 3 * fact' (fix fact') 2
= 3 * if 2 == 0 then 1 else 2 * (fix fact') (2 - 1)
= 3 * 2 * (fix fact') 1
= 3 * 2 * fact' (fix fact') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (fix fact') (1 - 1)
= 3 * 2 * 1 * (fix fact') 0
= 3 * 2 * 1 * fact' (fix fact') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (fix fact') (0 - 1)
= 3 * 2 * 1 * 1
= 6
This formal proof that
fact 3 = 6
methodically uses the fixed-point combinator equivalence for rewrites
fix fact' -> fact' (fix fact')
Lambda calculus
The untyped lambda calculus formalism consists in a context-free grammar
E ::= v Variable
| λ v. E Abstraction
| E E Application
where v
ranges over variables, together with the beta and eta reduction rules
(λ x. B) E -> B[x := E] Beta
λ x. E x -> E if x doesn’t occur free in E Eta
Beta reduction substitutes all free occurrences of the variable x
in the abstraction (“function”) body B
by the expression (“argument”) E
. Eta reduction eliminates redundant abstraction. It is sometimes omitted from the formalism. An irreducible expression, to which no reduction rule applies, is in normal or canonical form.
λ x y. E
is shorthand for
λ x. λ y. E
(abstraction multiarity),
E F G
is shorthand for
(E F) G
(application left-associativity),
λ x. x
and
λ y. y
are alpha-equivalent.
Abstraction and application are the two only “language primitives” of the lambda calculus, but they allow encoding of arbitrarily complex data and operations.
The Church numerals are an encoding of the natural numbers similar to the Peano-axiomatic naturals.
0 = λ f x. x No application
1 = λ f x. f x One application
2 = λ f x. f (f x) Twofold
3 = λ f x. f (f (f x)) Threefold
. . .
SUCC = λ n f x. f (n f x) Successor
ADD = λ n m f x. n f (m f x) Addition
MULT = λ n m f x. n (m f) x Multiplication
. . .
A formal proof that
1 + 2 = 3
using the rewrite rule of beta reduction:
ADD 1 2
= (λ n m f x. n f (m f x)) (λ g y. g y) (λ h z. h (h z))
= (λ m f x. (λ g y. g y) f (m f x)) (λ h z. h (h z))
= (λ m f x. (λ y. f y) (m f x)) (λ h z. h (h z))
= (λ m f x. f (m f x)) (λ h z. h (h z))
= λ f x. f ((λ h z. h (h z)) f x)
= λ f x. f ((λ z. f (f z)) x)
= λ f x. f (f (f x)) Normal form
= 3
Combinators
In lambda calculus, combinators are abstractions that contain no free variables. Most simply: I
, the identity combinator
λ x. x
isomorphic to the identity function
id x = x
Such combinators are the primitive operators of combinator calculi like the SKI system.
S = λ x y z. x z (y z)
K = λ x y. x
I = λ x. x
Beta reduction is not strongly normalizing; not all reducible expressions, “redexes”, converge to normal form under beta reduction. A simple example is divergent application of the omega ω
combinator
λ x. x x
to itself:
(λ x. x x) (λ y. y y)
= (λ y. y y) (λ y. y y)
. . .
= _|_ Bottom
Reduction of leftmost subexpressions (“heads”) is prioritized. Applicative order normalizes arguments before substitution, normal order does not. The two strategies are analogous to eager evaluation, e.g. C, and lazy evaluation, e.g. Haskell.
K (I a) (ω ω)
= (λ k l. k) ((λ i. i) a) ((λ x. x x) (λ y. y y))
diverges under eager applicative-order beta reduction
= (λ k l. k) a ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ y. y y) (λ y. y y))
. . .
= _|_
since in strict semantics
forall f. f _|_ = _|_
but converges under lazy normal-order beta reduction
= (λ l. ((λ i. i) a)) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= a
If an expression has a normal form, normal-order beta reduction will find it.
Y
The essential property of the Y
fixed-point combinator
λ f. (λ x. f (x x)) (λ x. f (x x))
is given by
Y g
= (λ f. (λ x. f (x x)) (λ x. f (x x))) g
= (λ x. g (x x)) (λ x. g (x x)) = Y g
= g ((λ x. g (x x)) (λ x. g (x x))) = g (Y g)
= g (g ((λ x. g (x x)) (λ x. g (x x)))) = g (g (Y g))
. . . . . .
The equivalence
Y g = g (Y g)
is isomorphic to
fix f = f (fix f)
The untyped lambda calculus can encode arbitrary constructive proofs over general/μ-recursive functions.
FACT = λ n. Y FACT' n
FACT' = λ rec n. if n == 0 then 1 else n * rec (n - 1)
FACT 3
= (λ n. Y FACT' n) 3
= Y FACT' 3
= FACT' (Y FACT') 3
= if 3 == 0 then 1 else 3 * (Y FACT') (3 - 1)
= 3 * (Y FACT') (3 - 1)
= 3 * FACT' (Y FACT') 2
= 3 * if 2 == 0 then 1 else 2 * (Y FACT') (2 - 1)
= 3 * 2 * (Y FACT') 1
= 3 * 2 * FACT' (Y FACT') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (Y FACT') (1 - 1)
= 3 * 2 * 1 * (Y FACT') 0
= 3 * 2 * 1 * FACT' (Y FACT') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (Y FACT') (0 - 1)
= 3 * 2 * 1 * 1
= 6
(Multiplication delayed, confluence)
For Churchian untyped lambda calculus, there has been shown to exist a recursively enumerable infinity of fixed-point combinators besides Y
.
X = λ f. (λ x. x x) (λ x. f (x x))
Y' = (λ x y. x y x) (λ y x. y (x y x))
Z = λ f. (λ x. f (λ v. x x v)) (λ x. f (λ v. x x v))
Θ = (λ x y. y (x x y)) (λ x y. y (x x y))
. . .
Normal-order beta reduction makes the unextended untyped lambda calculus a Turing-complete rewrite system.
In Haskell, the fixed-point combinator can be elegantly implemented
fix :: forall t. (t -> t) -> t
fix f = f (fix f)
Haskell’s laziness normalizes to a finity before all subexpressions have been evaluated.
primes :: Integral t => [t]
primes = sieve [2 ..]
where
sieve = fix (\ rec (p : ns) ->
p : rec [n | n <- ns
, n `rem` p /= 0])