COMPSCI 3MI3 : Assignment 8
Fall 2021
Nicholas Moore
1. Proof of Sequencing as a Derived Form
In topic 9, slides 26-32, we discuss the sequencing operator ; in two ways, as a separate term of the
language, and as a term derived from an inner language. In these slides, we stated the following theorem.
THEOREM [Sequencing is a Derived Form]
Define λE as the external calculus. This language will be composed of simply typed λ-Calculus, en-
riched with the Unit type and term, and with the term ;, E-Seq, E-SeqNext, and T-Seq.
Define λI as the internal calculus. This language will be composed of the simply typed λ-Calculus
and Unit type and term only.
Define e ∈ λE → λI as an elaboration function, which translates from the external language to the
internal language. It does so by replacing all instances of t1; t2 with (λx : Unit.t2) t1. For each term t of
λE , we have:
t
E−→ t′ ⇐⇒ e(t) I−→ e(t′) (1)
Γ `E t : T ⇐⇒ Γ `I e(t) : T (2)
The proof of these statements proceeds by structural induction over t.
Because these are “if and only if” statements, both directions must be proven independently.
(a) (6 points) Prove t
E−→ t′ =⇒ e(t) I−→ e(t′)
(b) (6 points) Prove e(t)
I−→ e(t′) =⇒ t E−→ t′
(c) (6 points) Prove Γ `E t : T =⇒ Γ `I e(t) : T
(d) (6 points) Prove Γ `I e(t) : T =⇒ Γ `E t : T

























学霸联盟