COMPSCI 3MI3 – Principles of Programming Languages
J. Carette
McMaster University
Adapted from “Types and Programming Languages” by Benjamin C. Pierce and Nick Moore’s material.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 1 / 30
The Lambda Calculus
Computation my Friends! Computation!
In the 1960s, Peter Landin observed that complex programming languages can be understood by capturing their essential mechanisms as a small core calculus.
The core language used by Landin was λ-Calculus
▶ Developed in the 1920s by Alonzo Church.
▶ Reduces all computation to function definition and application.
The strength of λ-Calculus comes from it’s simplicity and its capacity for formal reasoning.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 2 / 30
λ-Calculus Syntax
Untyped λ-Calculus is comprised of only 3 terms! ……………………………………………………………….
⟨t⟩ ::= ⟨x⟩
| λ⟨x⟩.⟨t⟩ | ⟨t⟩ ⟨t⟩
………………………………………………………………. These terms are:
λ abstraction application.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 3 / 30
Kinds of Syntax
Concrete Syntax
▶ The “surface syntax” used by programmers Abstract Syntax
▶ Often a tree, sometimes a Directed Acyclic Graph (DAG)
▶ The “internal representation” that’s nicer for programs to compute with.
Concrete to Abstract:
Nice-to-have but redundant constructs removed (aka desugaring) Missing information is added (type inference and elaboration)
J. Carette (McMaster University) The Lambda Calculus Fall 2023 4 / 30
Abstract syntax is an excellent way of visualizing a program’s structure, especially in resolving operator precedence.
For example, under BEDMAS, the expression 1 + 2 ∗ 3 would be the left diagram, not the right diagram:
BEDMAS trees are evaluated leaf-first, however λ expressions may be evaluated using a number of different strategies.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 5 / 30
ASTs of λ-Calculus
To reduce redundant parentheses in our concrete syntax for λ-Calculus: Application will be left-associative. That is, s t u is interpretted as:
i.e. (s t) u
J. Carette (McMaster University) The Lambda Calculus Fall 2023 6 / 30
Scope of λ Operator
The abstraction operator λ is taken to extend to the right as far as possible.
For the following expression:
λx.λy.x y x, aka λx.(λy.(x y) x), aka
We would construct an AST:
J. Carette (McMaster University) The Lambda Calculus Fall 2023 7 / 30
Free vs Bound Variables
In predicate calculus, distinction between free and bound variables. ∃x | x ̸= y
x is bound by the existential quantifier.
y is not bound by a quantifier and is therefore free
(λx.x y) x The first occurance of x is bound.
Both y and the second occurrance of x are free.
J. Carette (McMaster University) The Lambda Calculus
Only One Evaluation Rule
These terms reduce by substituting the abstracted variable with the term applied to the function. In other words:
(λx.t1) t2 → [x 7→ t2] t1
A λ expression which may be simplified is known as a redex, or
reducible expression. Calledbeta-reduction, aka β-reduction.
J. Carette (McMaster University) The Lambda Calculus Fall 2023
Programming Help
Using All our Substitutions
[x 7→ t2] t1 stands for “the term obtained by the replacement of all free occurances of x in t1 by t2. Examples:
(λx.x) y → y
(λx.x (λx.x)) (u r) → u r (λx.x)
J. Carette (McMaster University) The Lambda Calculus
Our Test Expression
To examine strategies, we will use a running example expression:
(λx.x) ((λx.x) (λz.(λx.x) z)) (6)
λx.x is effectively an identity function, so we write it as id. id (id (λz.id z))
The above expression has three redexes:
id (id (λz.id z)) id (id (λz.id z))
id (id (λz.id z)) J. Carette (McMaster University) The Lambda Calculus
The Worst Strategy Ever
Under Full Beta-Reduction, the redexes may be reduced in any order. not deterministic.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 12 / 30
Normal Order
Normal order begins with the leftmost, outermost redex, and proceeds until there are no more redexes to evaluate.
id (id (λz.id z)) → id (λz.id z)
→ λz.idz → λz.z ↛
J. Carette
(McMaster University)
The Lambda Calculus
Call By Name
The call by name strategy is more restrictive than normal order. You can’t evaluate anything under a lambda.
id (id (λz.id z)) → id (λz.id z)
→ λz.idz ↛
In this case, λz.id z is considered a normal form.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 14 / 30
程序代写 CS代考 加微信: cstutorcs
Haskell uses call by need, which is an optimization of call by name. To avoid re-evaluation, expressions are kept as a graph that joins
identical expressions,
Further, once an expression is evaluated, the expression is replaced by its value in the AST.
thus only need to be evaluated once.
is a reduction relation on syntax graphs, rather than syntax trees.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 15 / 30
Call By Value
Most languages use call by value, where only the outermost redexes are reduced, and a redex is only reduced when the right-hand-side has already been reduced to a value.
Here, as elsewhere, a value is a term in normal form.
id (id (λz.id z)) → id (λz.id z)
→ λz.idz ↛
J. Carette (McMaster University)
The Lambda Calculus
Can we even do Booleans? (Want to reconstruct UAE). tru = λt.λf .t
fls = λt.λf .f
J. Carette (McMaster University) The Lambda Calculus
Bool as 2-argument functions?!?
This will make more sense once we consider if then else:
ifte = λc.λth.λel. c th el (13)
With c = tru (λc.λth.λel. c th el) tru u v
→ (λth.λel. tru th el) u v
→ (λel. tru u el) v
→ (λt.λf .t) u v
→ (λf .u) v
→u →v ↛↛
With c = fls (λc.λth.λel. c th el) fls u v
→ (λth.λel. fls th el) u v → (λel. fls u el) v
→ (λt.λf.f)uv
J. Carette (McMaster University) The Lambda Calculus Fall 2023 18 / 30
Boolean Operators
Extending the λ-Calculus vs UAE:
UAE: add additional terms and evaluation rules.
▶ Makes recursion and induction longer λ-Calculus: define terms in the language
▶ tru and fls are not terms, but labels for λ expressions that were already valid terms!
J. Carette (McMaster University) The Lambda Calculus Fall 2023 19 / 30
Conservative Extension
Consider two theories, T1 and T2. We say that T2 is a conservative extension of T1 if:
Every theorem of T1 is a theorem of T2
Any theorem of T2 in the language of T1 is already a theorem of T1. i.e. Booleans are a conservative extension of the λ-Calculus Why useful? All
properties of the λ-Calculus remain true of conservative extensions.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 20 / 30
Boolean And I
More operations.
With input tru tru
(λb.λc. b c fls) tru tru
→ (λc . tru c fls) tru →
→ tru tru fls →
→ (λt .λf .t ) tru fls →
With input tru fls (λb.λc. b c fls) tru fls
(λc . tru c fls) fls tru fls fls
(λt .λf .t ) fls fls
→ (λf .tru) fls
→ tru ↛↛
and = λb.λc. b c fls (14)
→ (λf .fls) fls
J. Carette (McMaster University) The Lambda Calculus
Boolean And II
With input fls tru
(λb.λc. b c fls) fls tru
→ (λc . fls c fls) tru
→ fls tru fls
→ (λt .λf .f ) tru fls
→ (λf.f)fls
→ fls ↛↛
With input fls fls
(λb.λc. b c fls) fls fls → (λc . fls c fls) fls
→ fls fls fls
→ (λt .λf .f ) fls fls
→ (λf.f)fls
J. Carette (McMaster University) The Lambda Calculus
pair = λf .λs.λb. b f s (15) fst = λp. p tru (16) snd = λp. p fls (17)
b is used to select between f and s
fst and snd merely apply tru and fls respectively.
Since tru selects the first argument, it also selects the first term in the pair.
Likewise for fls Let’s code it in Haskell!
J. Carette (McMaster University) The Lambda Calculus Fall 2023 23 / 30
Church Numerals
Natural numbers are quite similar to Peano arithmetic:
c0 = λs.λz. z
c1 = λs.λz. s z
c2 = λs.λz. s (s z)
c3 = λs.λz. s (s (s z))
Church numerals take two arguments, a successor s and a zero term z
representation.
(18) (19) (20) (21)
J. Carette (McMaster University) The Lambda Calculus Fall 2023
You might have noticed that c0 has the same definition as fls. This is sometimes called a pun in computer science.
The same thing occurs in lower level languages, where the interpretation of a sequence of bits is context dependant.
In C, the bit arrangement 0x00000000 corresponds to:
▶ Zero (Integer)
▶ False (Boolean)
▶ ”\0\0\0\0” (Character Array)
This is not a good thing.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 25 / 30
Adding one:
succ = λn.λs.λz. s (n s z)
Successor of Two
→ (λn.λs.λz. s (n s z)) c2
→ λs.λz.s(c2sz)
→ λs.λz. s ((λs.λz. s (s z)) s z)
→ λs.λz. s ((λz. s (s z)) z)
→ λs.λz. s (s (s z))
J. Carette
(McMaster University)
The Lambda Calculus
plus = λm.λn.λs.λz. m s(n s z)
plus c2 c2
→ (λm.λn.λs.λz. m s (n s z))c2c2
→ (λn.λs.λz. c2 s (n s z))c2
→ λs.λz.c2s(c2sz)
→ λs.λz. (λs.λz. s (s z)) s ((λs.λz. s (s z)) s z)
→ λs.λz. (λz. s (s z)) ((λs.λz. s (s z)) s z)
→ λs.λz. (s (s ((λs.λz. s (s z)) s z)))
→ λs.λz. (s (s ((λz. s (s z)) z)))
→ λs.λz. (s (s (s (s z))))
J. Carette
(McMaster University) The Lambda Calculus Fall 2023
Times Have Changed
Finally, let’s define a multiplication operator.
times = λm.λn. m (plus n) c0
3 × 2 =? times c3 c2
(λm.λn. m (plus n) c0) c3 c2
(λn. c3 (plus n) c0) c2
(λs.λz. s (s (s z))) (plus c2) c0 (plus c2 ) ((plus c2 ) ((plus c2 ) c0 ))
J. Carette
(McMaster University)
The Lambda Calculus
Sub-Derivation
Technically this is cheating, since we don’t have a rule for this type of substitution in the semantic, and it violates our evaluation strategy.
→ (λm.λn.λs.λz. m s (n s z)) (λs.λz. s (s z))
→ (λn.λs.λz. (λs.λz. s (s z)) s (n s z))
→ (λn.λs.λz. (λz. s (s z)) (n s z))
→ (λn.λs.λz. (s (s (n s z))))
(It saves a lot of time though)
J. Carette (McMaster University) The Lambda Calculus Fall 2023 29 / 30
Computer Science Tutoring
→ → ⇝ → → → → → → ↛
(plus c2) ((plus c2) ((plus c2) c0))
(λn.λs.λz. (s (s (n s z)))) ((plus c2) ((plus c2) c0))
λs.λz. (s (s (((plus c2) ((plus c2) c0)) s z)))
λs.λz. (s (s (((λn.λs.λz. (s (s (n s z)))) ((plus c2) c0)) s z))) λs.λz. (s (s ((λz. (s (s (((plus c2) c0) s z)))) z)))
λs.λz. (s (s (s (s (((plus c2) c0) s z)))))
λs.λz. (s (s (s (s (((λn.λs.λz. (s (s (n s z)))) c0) s z))))) λs.λz. (s (s (s (s ((λs.λz. (s (s (c0 s z)))) s z)))))
λs.λz. (s (s (s (s ((λz. (s (s (c0 s z)))) z)))))
λs.λz. (s (s (s (s (s (s (c0 s z)))))))
λs.λz. (s (s (s (s (s (s ((λs.λz. z) s z)))))))
λs.λz. (s (s (s (s (s (s ((λz. z) z)))))))
λs.λz. (s (s (s (s (s (s z))))))
J. Carette
(McMaster University) The Lambda Calculus Fall 2023 30 / 30