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) Towards the Lambda Calculus Fall 2023 1 / 36
Towards the Lambda Calculus
Language Safety
“Informally […], safe languages can be defined as ones that make it impossible to shoot yourself in the foot while programming.” (Pierce, 2002)
Safety refers to whether or not a language protects its own abstractions.
▶ In Haskell, lists can only be accessed in the normal way.
▶ In C, pointer manipulation can be used to violate the bounds of arrays to
read adjacent data.
Language safety can be enforced either statically or dynamically, though often a combined approach is used.
▶ Haskell, for example, checks array bounds dynamically.
Statically Checked
Dynamically Checked
ML, Haskell, Java
Lisp, Scheme, Perl, Postscript
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 2 / 36
Programming Help, Add QQ: 749389476
From the ground up
“In modern languages, the type system is often taken as the foundation of the language’s design, and the organizing principle, in light of which every other aspect of the design is considered.” (Pierce, 2002)
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 3 / 36
EBNF Examples
The following grammar describes how we write the integers. ……………………………………………………………….
⟨Integer⟩ ::= [-]⟨digit⟩{⟨digit⟩}
⟨digit⟩::= 0|1|2|3|4|5|6|7|8|9 ……………………………………………………………….
Here, we have two rules. The top level rule,
“|” denotes a set of options. For example,
“[]” denote something which is optional. For example, the negative sign denoting a negative integer may be absent.
“{}” denote zero or more repetitions of the contents. For example, zero or more digits may follow the first.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 4 / 36
EBNF Examples
The following grammar is for writing hexadecimal integers. ……………………………………………………………….
⟨Hex Integer⟩ ::= [-]⟨hex digit⟩{⟨hex digit⟩}
⟨hexdigit⟩::= 0|1|2|3|4|5|6|7|8|9|A|B|C|D|E|F
………………………………………………………………. Note that the grammar describing decimal integers is a subset of the grammar for hexadecimal integers.
Although every Integer is also a Hex Integer, this does not imply anything about how either group would be interpretted.
EBNF describes syntax, not semantics!
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 5 / 36
Computer Science Tutoring
Death and Syntaxes!
Here are a few more example grammars:
A Python list. Items in quotes are taken literally.
………………………………………………………………. ⟨List⟩ ::= ‘[’ ⟨Object List⟩ ‘]’
⟨Object List⟩ ::= ⟨Object⟩, ⟨Object List⟩ | ⟨Object⟩ ……………………………………………………………….
A Python function. ……………………………………………………………….
⟨Function⟩ ::= def ⟨Identfier⟩ (⟨Argument List⟩) : ‘\n\t’ ⟨Statement List⟩ ……………………………………………………………….
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 6 / 36
Untyped Arithemetic Expressions (UAE) – Syntax
………………………………………………………………. ⟨t⟩ ::= true
| if ⟨t⟩ then ⟨t⟩ else ⟨t⟩ |0
| succ ⟨t ⟩
| pred ⟨t⟩
| iszero ⟨t ⟩
………………………………………………………………. t is a metavariable.
EBNF is a metalanguage (a language which describes languages), and t is a variable of that language.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 7 / 36
Define Your Terms!
Equivalent descriptions formalisms: Defining Terms Inductively
Defining Terms Using Inference Rules Defining Terms Using Set Theory
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 8 / 36
Inductive Definition
The set of terms is the smallest set T such that: {true, false, 0} ⊆ T
t1 ∈ T , =⇒ {succ t1,pred t1,iszero t1} ⊆ T t1,t2,t3 ∈T =⇒ {ift1 thent2 elset3}⊆T
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023
程序代写 CS代考 加微信: cstutorcs
Terms By Rules of Inference
Similar to rules of natural deduction used in the presentation of logical systems.
T shall be the set of terms defined by the following rules:
false ∈ T t∈T
predt ∈T t2 ∈ T
iszerot ∈T t3 ∈ T
ift1 thent2 elset3 ∈ T
J. Carette
(McMaster University) Towards the Lambda Calculus Fall 2023 10 / 36
Terms, Set-Theoretically
For each natural number i, define the set Si as follows:
Si+1 = {true,false,0}
∪{t ∈Si |succt,predt,iszerot} ∪{t1,t2,t3 ∈Si|ift1 thent2 elset3}
S = [ Si i
J. Carette
(McMaster University)
Towards the Lambda Calculus Fall 2023 11 / 36
Yes. By induction – prove T ⊆ S and also S ⊆ T .
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 12 / 36
Size of a Term
The size of a term t, written size(t) is written as follows:
size (true)
size (false)
size(succ t1)
size(pred t1)
size(iszero t1)
size(if t1 then t2 else t3)
= size(t1) + 1
= size(t1) + 1
= size(t1) + 1
= size(t1) + size(t2) + size(t3) + 1
J. Carette (McMaster University)
Towards the Lambda Calculus Fall 2023 13 / 36
Depth of a Term
The depth of a term t, written depth(t) is written as follows:
depth(true) = depth(false) = depth(0) = depth(succ t1) = depth(pred t1) = depth(iszero t1) = depth(if t1 then t2 else t3) =
depth(t1) + 1
depth(t1) + 1
depth(t1) + 1 max(depth(t1), depth(t2),
depth(t3)) + 1
J. Carette (McMaster University)
Towards the Lambda Calculus Fall 2023 14 / 36
Induction on Size and Depth
With these new definitions, we can now introduce three exciting new forms of induction!
[Induction on Size]
If, for s ∈ T
▶ Given P(r) for all r such that
size(r) < size(s)
▶ we can show P(s)
Wemayconclude∀s∈T |P(s)
These two forms of induction are derived from Complete Induction over N
[Induction on depth]
If, for s ∈ T
▶ Given P(r) for all r such that
depth(r) < depth(s) ▶ we can show P(s)
Wemayconclude∀s∈T |P(s)
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 15 / 36
Structural Induction over Terms
[Structural Induction Over Terms]
If, for s ∈ T
We can show P(c) for the language constants, and
▶ Given P(r) for all immediate subterms of r of s
▶ we can show P(s)
We may conclude ∀s ∈ T | P(s)
These methods of induction are equivalent to each other, but using one or
the other can simplify our proofs.
Formally, these three forms of induction are interderivable.
As a matter of style, we will often use structural induction:
Because it is a bit more intuitive.
To avoid having to detour into numbers.
J. Carette
(McMaster University) Towards the Lambda Calculus Fall 2023 16 / 36
Semantics Styles
Once we have syntax, by specifying the semantics of our Untyped Arithmetic Expressions language, we will have a complete and working model of a programming language that’s ready for implementation1!
In general there are three major semantic styles: Operational Semantics
▶ Small-Step ▶ Big-Step
Denotational Semantics Axiomatic Semantics
1By you! During an assignment!
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 17 / 36
Operational Semantics
Under operational semantics, we define how a language behaves by specifying an abstract machine for it.
An abstract machine is abstract because it operates on the terms of the language themselves.
▶ This is in contrast to a regular machine, which must first translate the terms to instructions in the computer processor’s instruction set.
For simple languages (such as UAE), the state of this abstract machine is simply a term of the language.
The machine’s behaviour is specified by a transition function.
The meaning of a term is the final state of the abstract machine at the
point of halting.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 18 / 36
Operational Semantics (cont.)
Small Step
For each state, gives either the results A single transition within the abstract
of a single simplification, or indicates the machine has halted.
machine evaluates the term to its final result.
Sometimes, we will use two different operational semantics for the same language. For example:
One might be abstract, on the terms of the language as used by the programmer.
Another might represent the structures used by the compiler/interpreter.
In the above case, proving correspondance between these two machines is proving the correctness of an implementation of the language, i.e., proving the correctness of the compiler itself.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 19 / 36
Denotational Semantics
Meaning of a term is a mathematical object.
Semantic Domains → A collection of sets of mathematical objects
which we can map terms to.
Interpretation Function → A mapping between the terms of our language and the elements of our semantic domains.
For example:
writing succ(succ(succ0)) as 3.
N is the semantic domain.
The interpretation function maps terms of UAE to N.
⋆ How? By counting the number of succ invokations.
J. Carette
(McMaster University) Towards the Lambda Calculus Fall 2023 20 / 36
Axiomatic Semantics
Axiomatic Semantics give laws of behaviour of terms.
This means that the meaning of a term is precisely that which can be
proved about it.
This normally takes the form of assertions about the modification of
program states made by program instructions. This approach is closely related to Hoare Logic.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 21 / 36
Operational Semantics of Booleans
Small step semantics of the boolean elements of UAE.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 22 / 36
The One-Step Evaluation Relation
Our evaluation relation → is defined as the smallest binary relation on terms satisfying the three rules given.
When a pair (t,t′) is in our evaluation relation, we say that “the evaluation statement t → t′ is derivable.”
By smallest, we mean that the relation contains no pairs other than those derived from instances of our inference rules.
▶ Since there are an infinite number of terms, there are also an infinite number of instances of the inference rules, and an infinite number of pairs in our evaluation relation.
Demonstrate the derivability of a given pair using formal derivation.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 23 / 36
Example Evaluation
Consider the following expression in UAE:
if true then (if false then false else false) else true (4)
Let’s set t to the inner if expression so the derivation tree fits on the page:
t = if false then false else false (5)
(See evaluation on board)
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 24 / 36
Example Evaluation 2
if (if true then false else true) then true else false t = if true then false else true
(rest also on board)
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023
Induction on Derivations
Fact: t → t′ is derivable iff there is a derivation with t → t′ as its conclusion.
This fact can be used to reason about the properties of the evaluation relation.
[Induction on Derivations]
If we can show that
▶ Given that the same property holds for all sub-derivations,
▶ The property must necessarily hold for the super-derivation,
We may conclude that the property holds for all possible derivations.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 26 / 36
Determinacy
[Determinacy of One-Step Evaluation]
t→t′∧t→t′′ =⇒t′=t′′ (8)
That is to say, if a term t evaluates to t′, and the same term evaluates to t′′, t′ and t′′ must be the same term.
By induction on the derivation of t → t′.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 27 / 36
Normal Form
Language designers care a lot about how an expression is evaluated. Programmers care more about what it evaluates to.
A term t is in Normal Form if no evaluation rule applies to it.
For untyped booleans, the normal form of all terms is true or false. THEOREM : [Every Value is in Normal Form]
true and false are in normal form. Become highly non-trivial later!
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 28 / 36
If It’s In Normal Form... It’s a Value!
[If t is in Normal Form, t is a Value] Proof:
Suppose t is in Normal Form but not a value.
IH: Subterms of t that are not a value are not in normal form. t not a value, must be of form
if t1 then t2 else t3 (9)
Whether it can be evaluated depends on what t1 is. There are three possibilities:
▶ t1 is true. E-IfTrue applies.
▶ Similarly for t1 = false and E-IfFalse.
▶ Thus t1 is not a value, and by IH, not in normal form. But this means
E-If applies, to t is not normal.
We will see later on that this isn’t necessarily the case for all languages.
succ 0 cannot be evaluated, but is also not a value.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 29 / 36
Termination
evaluation terminates when it reaches some normal form.
in a finite number of steps,
without repeating “states” (which would cause non-termination).
But what about the the halting problem ? Rough answer: it’s easy to use types to keep it at bay.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 30 / 36
Multi-step Evaluation (→∗) multi-step evalution relation →∗:
the reflexive, transitive closure of one-step evaluation. In other words, the smallest relation such that:
t→t′ =⇒t→∗t′ ∀t ∈ T | t →∗ t
t→∗t′∧t′→∗t′′ =⇒t→∗t′′ i.e. contains →, is reflexive and is transitive.
J. Carette (McMaster University) Towards the Lambda Calculus
Uniqueness of Normal Form
THEOREM : [Uniqueness of Normal Forms]
Consider t, u, u′ ∈ T , where u and u′ are normal forms.
t→∗u∧t→∗u′ =⇒u=u′ (13)
Proof idea:
single-step is unique
can’t have multiple normal forms in a path of →∗ (by definition, normal forms don’t evaluate).
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 32 / 36
Termination of Evaluation
THEOREM : [Termination of Evaluation] (for Booleans)
∀t ∈ T ∃t′ ∈ N|t →∗ t′ (14)
Where N is the set of normal forms of T . Useful: LEMMA :
s → s′ =⇒ size(s) > size(s′). (15) So single-step evaluation reduces size, and there are no infinite descending
chains of naturals.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 33 / 36
Extended UAE Semantics
When a term is in normal form but not a value, it is stuck.
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 34 / 36
Why are Numeric Values Necessary?
Consider the following expression in UAE:
iszero succ pred succ 0
Which rule applies?
1 E-IsZeroSucc
2 E-IsZero
Those rules again…
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 35 / 36
To Resolve Ambiguity!
We can’t use E-IsZeroSucc, because succ pred succ 0 is not a value.
If E-IsZeroSucc did not require a numeric value, the rule would also apply to evaluatable succ terms.
This would cause a rather nasty ambiguity, destroying our language’s determinacy! Basically…
t→t′∧t→t′′ nolongerimpliest′ =t′′ (16) This is bad language design, even if multi-step semantics might still turn out
J. Carette (McMaster University) Towards the Lambda Calculus Fall 2023 36 / 36