Topic

Introduction to Lambda Calculus

Introduction and motivations

The lambda calculus is a useful tool in Computer Science

it constitutes the foundation for functional programming

it is the meta-language of denotational semantics (the “best-bet” standard for specifying programming language semantics)

it provides (one version of) a theory of computation (the more traditional version is via Turing Machines)

Lambda calculus comes from logic and mathematics

it provides a generalized notion of function (untyped, higher-order functions)

it provides a generalization of algebraic and logical notations

it can be used as a foundation for constructive mathematics

What is lambda calculus?

it is “the” formal theory of functions (i.e., it formalizes functions first, rather than encoding them in other terms, as in set theory)

it is “just” a better (more direct) notation for functions

How does lambda calculus differ from traditional mathematical treatments of functions?

in traditional math, functions are usually first-order and usually typed; in (pure) lambda calculus, functions are higher-order and untyped

in set theory, functions are coded as their graphs (i.e., sets of pairs); in lambda calculus, functions are viewed operationally, in terms of rules or algorithms

allows us to distinguish different algorithms and thus different running times, styles of expression, etc.

allows us to connect to the functions via concrete language: this is how we define and use them, not just what they are

Variations on lambda calculus

the pure, untyped calculus (what we will study here)

applied calculi with extra constants (e.g., for logic or arithmetic)

combinatory logic: no bound variables ("points-free")

deBruijn numbers: another way of eliminating variables

typed calculi: a rich family of calculi which model typed programming languages, higher-order logics, etc.

Syntax of the lambda calculus

Notational conventions

M, N, P, … range over lambda terms (the main syntactic category)

x,y,z, … range over variable names; actual variables may be drawn from any (countably infinite) set of symbols

Context-free grammar of expressions

M ::= x | λx.M | M N

the first form of term is just an occurrence of a variable

the second form of term is called a lambda abstraction: its meaning is a function

the variable in an abstraction is bound by the construct; the body term is the scope of the binding

the third form is (function) application; the left part is called the operator, the right part the argument

Abbreviations, precedence and other syntactic conveniences

function application associates to the left

M N P ≣ (M N) P ≢ M (N P)

the scope of lambda extends as far as possible to the right (up to the end, or a closing parenthesis)

λx.M N ≣ (λx.(M N)) ≢ (λx.M) N

multiple successive abstractions are often abbreviated with a single lambda (if variables are multi-symbol, then use commas or spaces to separate)

λxyz. M ≣ λx. (λy. (λz.M))

Some sample terms

the identity function

(λx. x)

a polynomial in x

(λx. x^2 + 2x +3)

the ‘constant-function producing function’ (Haskell's const)

(λxy. x)

function composition

(λfgx. f (g x))

the ‘twice’ function

(λfx. f (f x))

Lambda calculus as a direct means of defining functions

lambda abstractions stand for (denote) functions directly, so that no separate mechanism for parametric definitions is needed

normally, we define functions only indirectly, by way of application to a parameter

f x = x+3

we wouldn’t accept such an indirect definition if we were defining, say, negative numbers in terms of positive ones

x+4 = 1

we would prefer to define negative numbers directly, using a separate notation unique to them; this notation liberates our thinking and allows us to focus on the new concept

x = -3

similarly, lambda calculus allows us to define functions directly, and therefore to focus on them as separate entities

f = (λx.x+3)

here the lambda abstraction appearing on the right is a kind of inverse of function application, just as subtraction is a kind of inverse of addition

Syntactic operations

Some intuitions

intuitively, bound variables can be changed without changing meaning

(λx.x) = (λy.y) = the identity function

intuitively, application substitutes the argument for the bound variable in the function's body

(λx.x+3*x) 17 = 17+3*17

although pure lambda calculus contains no constants (such as + or 3), these can be added to the language for more practical applications

Notions of free and bound variables

the bound variables of a term are those bound by some abstraction

BV(x) = {}

BV(λx.M) = {x}

BV(M N) = BV(M) ∪ BV(N)

the free variables of a term are those not bound by some abstraction

FV(x) = {x}

FV(λx.M) = FV(M) \ {x}

FV(M N) = FV(M) ∪ FV(N)

when substituting terms or variables for bound variables, we need to take some care to avoid confusing one bound variable for another

(λxy.x) y = (λx.(λy.x)) y = (λy.x) [y/x] =? (λy.y)

Substitution formally defined

we define a formal notion of substitution which respects bound variables

M [N/x]: the term M with the term N substituted for all free occurrences of x

x [N/x] = N

y [N/x] = y (for y≢x)

(λx.M) [N/x] = λx.M

(λy.M) [N/x] = λy. (M [N/x]) (for y≢x and if y∉FV(N))

(λy.M) [N/x] = λz. ((M [z/y]) [N/x]) (for y≢x, y∈FV(N), z fresh)

M P [N/x] = (M [N/x]) (P [N/x])

Theory and operational semantics of the lambda calculus

Basic notions of reduction

Beta reduction

(λx.M) N →β M [N/x]

Eta reduction (or expansion)

(λx.M x) →η M (when x∉FV(M))

Alpha reduction (or equivalence)

(λx. M) →α (λy. M[y/x])

Delta reductions (for applied calculi)

2+3 →δ 5

Of these various rules, alpha reduction is the most innocuous; we normally ignore it by considering terms modulo their “alpha-equivalence classes” and by adopting some convention to avoid any clash of variables

Extended notion of reduction

the basic notions of reduction determine relations on terms; we take the reflexive, transitive and compatible closure of these basic notions to get a (full) notion of reduction on terms (compatible closure just says that if a sub-term reduces, so does the term that contains it)

Different reduction orders

since reductions might apply to various sub-terms, there may be several ways in which we can reduce a given term; in fact, some might terminate whereas others might not

(λxy.x) I Ω where Ω = (λx.xx) (λx.xx) and I = λx.x

Normal form

when a term can be reduced no more, we say it is in normal form

some terms may have no normal form

Ω = (λx.xx) (λx.xx)

some terms without normal form may still yield information (e.g., a term representing the list of all digits of π)

Equality on terms

symmetric and transitive closure of reduction; gives us the primitive notion of equality on terms

equality on terms is in general undecidable

Church-Rosser theorem

if two terms are equal, then they reduce to a common term

Normal-order reduction

if a term reduces in finitely-many steps to a normal form, then reducing by the strategy “left-most/outer-most first” will yield that normal form

Expressive power of the lambda calculus

We can encode all the usual mathematical and logical notions in terms of lambda calculus

this is similar to the way in which these notions are encoded in pure set theory

“pure” theories are good for theoretical studies; applied theories usually categorize entities by some kind of types

Booleans

we can encode True, False and if-then-else as follows:

True ≣ λxy. x

False ≣ λxy. y

if M then N else P ≣ M N P

i.e., if-then-else = λxyz. x y z

Natural numbers

we can encode a natural number n as the n-fold self-composition operator

Zero ≣ λfx. x

One ≣ λfx. f x

n ≣ λfx. f (f … (f x) … ) (n occurrences of f)

we can then encode addition, multiplication and exponentiation

+ ≣ λmnfx. m f (n f x)

* ≣ λmnf. m (n f)

^ ≣ λmn. n m

Pairing

we can encode pairs and projection function as follows

(M,N) ≣ λz. z M N

fst ≣ λp. p True

snd ≣ λp. p False

Defining recursion

we can define λ-terms which implement general recursion

Y ≣ λf. (λx. f(x x)) (λx. f(x x))

Y F = F(Y F)

Θ ≣ (λxy. y(xxy)) (λxy. y(xxy))

Θ F ↠ F(Θ F)

we can define factorial this way

fact = Y (λfn. if n=0 then 1 else n * f (n-1))

Combinators

Definition of a combinator

a combinator is any closed lambda term ; i.e., a term without free variables

Combinatory logic as a separate theory

rather than defining combinators as certain lambda terms, we can devise a calculus with combinators alone

in Combinatory Logic, each combinator has a rule which shows its behavior under reduction

S f g x → f x (g x)

K x y → x

I x → x

All terms with variables can be translated into combinatory terms which behave like lambda abstractions

abs x (x) = I

abs x (y) = K x (for y≢x)

abs x (M N) = S (abs x M) (abs x N)

the translation for lambda abstractions just substitutes abs x M for λx.M