Lambda Calculus and Combinators

Connections

Related to: Functions, functional programming
Prerequisite:
Requisite for:

Functions

The classical idea of a function that of an optional name, 0 or more parameters, and a rule for computing a value from the parameters. For example, f n = if (n == 0) then 1 else n*(f (n-1)) This is in contrast to the modern definition of a function as a set of ordered pairs. The classical idea is used as a foundation for computing. The lambda calculus is an elegant formulation of the classical idea.

Why should we be interested in the lambda calculus?

The lambda calculus was introduced as a notation for representing and studying functions.

As a model of computation, it is equivalent to the Turing machine.

It provides the theoretical foundations for functional programming languages (Lisp is syntacticaly similar) and is used to provide the denotational semantics for programming languages.

In it, functions are first class objects. They may be assigned to a variable, passed as an argument, or returned as a result.

It is the source of inspiration for lexical scope rules and lazy evaluation.

What are the key ideas of the lambda calculus?

Simple syntax

Execution (expression evaluation) is by reduction to a normal form.

Syntax

**The Syntax of the Lambda Calculus**

formula	::=	term = term
term	::=	identifier \| application \| abstraction
identifier	::=	x₀ \| x₁ \| x₂ \| ...
application	::=	( term term )
abstraction	::=	( λ identifier . term )

Parentheses may be omitted according to the following conventions:

Associate to the left: A B C = ((A B) C)
The scope of λx. extends as far a possible: λx.yxλz.xz = (λx.yx (λz.xz))
Consecutive λ's may be collapsed to a single λ: λxy.M = λx.λy.M

**Substitution rules:**[e⁄x] - e replaces x

[e⁄x]x	`→`	e
[e⁄x]y	`→`	y	x ≠ y
[e⁄x]( M N )	`→`	( [e⁄x]M [e⁄x]N )
[e⁄x]λx.M	`→`	λx.M
[e`/`x]λy.M	`→`	λz.[e⁄x][z`⁄y`]M	x ≠ y & z does not occur in either e or M

The Theory

Axioms and rules of inference

**= is an equivalence relation**

	M = M
	M = N then N = M
	M = N, N = L then M = L

**= is substitutive**

	if N = N' then M N = M N'
	if M = M' then M N = M' N
	if M = N then λx.M = λx.N

**Axioms - the conversion rules**
	Expansion		Reduction
alpha	λx.M	=	λy.[y⁄x]M	(y does not occur in M)
beta	(λx.M) N	=	[N⁄x]M
eta	λx.M x	=	M

Reduction

Definition: A reduction is the application of 0 or more alpha, beta or eta reductions.

M is reduceable to N (M red N) if there is a sequence of alpha, beta, and/or eta reductions from M to N.
M is convertable to N ( M cnv N) if M = N is a theorem of the lambda calculus.
A term containing no free variables is called a combinator.

Definition: A term M is said to be in normal form if it does not contain a (beta or eta) redux as a subterm. If M cnv N and N is a normal form, then N is said to be the normal form of M.

The key questions include

If two or more reductions are possible, does the order in which they are done matter? Some possibilities include left to right, right to left, parallel.
- Left to right reductions correspond to lazy evaluation with significant overhead for copying but permit infinite data structures.
- Right to left reductions correspond to passing by value.
Do reduction sequences terminate?
Do all functions reduce to a cononical form?

The following expressions do not have normal forms:

(λx.x x) (λx. x x)
Y = λf. (λx. f ( x x )) (λx. f ( x x ))

The order of reduction is important: (λw.z) ((λx.x x) (λx. x x))

Reducing the argument first is known as applicative order evaluation and corresponds to call by value. Performing the substitution first is known as normal order reduction and corresponds to call by name. Applicative order is desireable when a function is sure to use its arguments as the arguments are evaluated just once and may be used several times. Normal order reduction requires that the arguments be evaluated each time they are needed however, it is possible that the value of an argument may not be needed.

The following theorem assures us that any two reduction sequences that terminate will do so with the same result.

THEOREM (Church-Rosser) If X cnv Y then there is a Z such that X red Z and Y red Z.

The Semantics

Combinators (variable-free expressions)

Haskell B. Curry

Combinatorial Logic

S = λf ( λg ( λx f x ( g x ) ) )

K = λx λy x

I = λx x

Y = λf λx ( f(x x)) λx (f (x x))

C [ s ] → s

C [ (E₁ E₂)] → (C [ E₁] C [ E₂ ])

C [ λx E] → A [ (x, C [ E] ) ]

A [ (x, s) ] → if (s=x) then I else (K s)

A [ (x, (E₁ E₂))] → ((S A [ (x, E₁)] ) A [ (x, E₂) ] )

S f g x → f x (g x)

K c x → c

I x → x

Y e → e (Y e)

(A B) → A B

(A B C) → A B C