-postulate
progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
@@ -1616,598 +1661,598 @@ Formally:
-data _∈_ : Id → Term → Set where
- free-` : ∀ {x} → x ∈ ` x
- free-λ :_∈_ ∀: Id → Term {x y A N} → Set where y ≢ x → x ∈
+ free-` : N∀ → {x} ∈→ (λ[x ∈ y` ∶x A ] N)
free-·₁free-λ : ∀ {x :y ∀A {xN} L→ M}y →≢ x ∈ L → x ∈ (LN → x ∈ ·(λ[ My ∶ A ] N)
free-·₂free-·₁ : ∀ {x L M}: →∀ {x ∈L M →} x→ ∈x (∈ L ·→ M)x ∈ (L · M)
free-if₁ : ∀ {x Lfree-·₂ M: N}∀ →{x xL ∈ L → x ∈ (if L then M} else→ Nx ∈ M → x ∈ (L · M)
free-if₂free-if₁ : ∀ {x L M N} → x ∈ →L x→ ∈x M∈ → x(if ∈L (if L then M else N)
free-if₃free-if₂ : ∀ {x L M N} → x ∈ →M x→ ∈x N∈ → x(if ∈L (if L then M else N)
+ free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
@@ -2217,131 +2262,131 @@ A term in which no variables appear free is said to be _closed_.
-_∉_ : Id → Term → Set
-x ∉ M = ¬ (x ∈ M)
-
-closed : Term → Set
-closed M =→ ∀ {Set
+x} →∉ xM ∉= ¬ (x ∈ M)
+
+closed : Term → Set
+closed M = ∀ {x} → x ∉ M
@@ -2351,240 +2396,240 @@ Here are proofs corresponding to the first two examples above.
-f≢x : f ≢ x
-f≢x ()
-
-example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] `: f ·≢ ` x)
example-free₁ = free-λ f≢x (free-·₂ free-`)()
example-free₂example-free₁ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
example-free₂example-free₁ (= free-λ f≢ff≢x _)(free-·₂ free-`)
+
+example-free₂ : f ∉ (λ[ =f f≢f∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
+example-free₂ (free-λ f≢f _) = f≢f refl
@@ -2596,367 +2641,367 @@ Prove formally the remaining examples given above.
-postulate
- example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
example-free₄example-free₃ : fx ∈ ((λ[ ((λ[ f ∶ (𝔹 ∶⇒ (𝔹) ⇒] 𝔹) ] ` f · ` x) `· x) · ` f)
example-free₅example-free₄ : xf ∉∈ ((λ[ (λ[f ∶ f ∶ (𝔹 ⇒ 𝔹) ] ` ]f λ[· ` x ∶) 𝔹· ]` ` f · ` x)
example-free₆example-free₅ : x ∉ (λ[ f ∉∶ (λ[𝔹 f⇒ ∶𝔹) (𝔹] ⇒λ[ x ∶ 𝔹) ] λ[ x` ∶f 𝔹· ]` ` f · ` x)
+ example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
@@ -2975,115 +3020,115 @@ then `Γ` must assign a type to `x`.
-free-lemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
@@ -3119,454 +3164,454 @@ _Proof_: We show, by induction on the proof that `x` appears
-free-lemma free-` (Ax Γx≡A) = (_ , Γx≡A)
-free-lemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = free-lemma x∈L ⊢L
free-lemma (free-·₂free-·₁ x∈Mx∈L) (⇒-E ⊢L ⊢L ⊢M) = free-lemma x∈Mx∈L ⊢L ⊢M
free-lemma (free-if₁free-·₂ x∈Lx∈M) (𝔹-E⇒-E ⊢L ⊢M) ⊢M ⊢N) = free-lemma x∈M ⊢M x∈L ⊢L
free-lemma (free-if₂free-if₁ x∈Mx∈L) (𝔹-E ⊢L ⊢M ⊢N) ⊢M ⊢N) = free-lemma x∈L ⊢L x∈M ⊢M
free-lemma (free-if₃free-if₂ x∈Nx∈M) (𝔹-E ⊢L ⊢M ⊢N) ⊢M ⊢N) = free-lemma x∈M ⊢M x∈N ⊢N
free-lemma (free-λfree-if₃ x∈N) {x}(𝔹-E {y}⊢L y≢x⊢M x∈N⊢N) = (⇒-I ⊢N) with free-lemma x∈N ⊢N
+free-lemma ⊢N
-... |(free-λ {Γx≡C with y ≟ x} {y} y≢x x∈N)
- ...(⇒-I |⊢N) yes y≡xwith =free-lemma ⊥-elimx∈N (y≢x y≡x)⊢N
... | no _ Γx≡C with y ≟ x
+... | yes y≡x = ⊥-elim (y≢x y≡x)
+... | no _ = Γx≡C
@@ -3584,68 +3629,68 @@ typed in the empty context is closed (has no free variables).
-postulate
∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
@@ -3654,294 +3699,294 @@ typed in the empty context is closed (has no free variables).
-contradiction : ∀ {X : Set} → ∀ {x : X} → ¬ (_≡_ {A = Maybe X} (just x)∀ nothing{X : Set} → ∀ {x : X} → ¬ (_≡_ {A = Maybe X} (just x) nothing)
contradiction ()
∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
-∅⊢-closed′ {M} {A} ⊢M {x} x∈MM withA} → ∅ free-lemma⊢ x∈MM ⊢M∶ A → closed M
...∅⊢-closed′ |{M} (B{A} ,⊢M ∅x≡B){x} =x∈M contradictionwith (transfree-lemma (sym ∅x≡B)x∈M (apply-∅⊢M
+... | (B , ∅x≡B) = contradiction (trans (sym ∅x≡B) (apply-∅ x))
@@ -3957,144 +4002,144 @@ exchanged for the other.
-context-lemma : ∀ {Γ Γ′ M A}
- → (∀ {x} → x ∈ M → Γ x ≡ Γ′ x)
- → : ∀ {Γ Γ′ Γ ⊢ M ∶ A}
→ Γ′(∀ {x} → ⊢x M∈ ∶M → Γ x ≡ Γ′ x)
+ → Γ ⊢ M ∶ A
+ → Γ′ ⊢ M ∶ A
@@ -4146,252 +4191,159 @@ _Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`.
-context-lemma Γ~Γ′ (Ax Γx≡A) rewrite (Γ~Γ′ free-`) = Ax Γx≡A
context-lemma {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (context-lemma Γx~Γ′x ⊢N)
- where Γ~Γ′ (⇒-I ⊢N) = ⇒-I (context-lemma Γx~Γ′x ⊢N)
where
+ Γx~Γ′x : ∀ {y} → y ∈ N → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y
- Γx~Γ′x } y∈N→ y with∈ xN ≟→ (Γ y,
- ... |x yes∶ reflA) y ≡ (Γ′ , =x refl∶ A) y
... | noΓx~Γ′x {x≢y =y} y∈N Γ~Γ′with (free-λx x≢y≟ y
+ ... y∈N)
-context-lemma| Γ~Γ′yes refl = refl
+ ... (⇒-E| no ⊢L ⊢M) x≢y = ⇒-EΓ~Γ′ (context-lemmafree-λ x≢y y∈N()
+context-lemma Γ~Γ′ ∘(⇒-E free-·₁) ⊢L ⊢M) = ⇒-E (context-lemma (Γ~Γ′ ∘ free-·₁) ⊢L)
(context-lemma (Γ~Γ′ ∘ free-·₂) ⊢M)
context-lemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
context-lemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
context-lemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (context-lemma (Γ~Γ′ ∘ free-if₁) (𝔹-E ⊢L)
- (context-lemma (Γ~Γ′ ∘ free-if₂) ⊢M ⊢N) = 𝔹-E (context-lemma (Γ~Γ′ ∘ free-if₁) ⊢L)
(context-lemma (Γ~Γ′ ∘ free-if₃free-if₂) ⊢M)
+ (context-lemma (Γ~Γ′ ∘ free-if₃) ⊢N)
@@ -4764,162 +4809,162 @@ _Lemma_: If `Γ , x ∶ A ⊢ N ∶ B` and `∅ ⊢ V ∶ A`, then
-preservation-[:=] : ∀ {Γ x A N B V}
→ (Γ , x ∶ A) ⊢ N ∶ B
- → ∅ ⊢ V ∶ A
- → ΓN ⊢∶ (NB
+ → [∅ x⊢ := V ]) ∶ A
+ → Γ ⊢ (N [ x := V ]) ∶ B
@@ -4993,425 +5038,425 @@ we show that if `∅ ⊢ V ∶ A` then `Γ ⊢ N [ x := V ] ∶ B`.
We need a couple of lemmas. A closed term can be weakened to any context, and `just` is injective.
-weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∶ A → Γ ⊢ V ∶ A
-weaken-closed {V} {A: }∀ {V A Γ} ⊢V→ =∅ context-lemma⊢ Γ~Γ′V ∶ A → Γ ⊢ V ⊢V∶ A
- where
- Γ~Γ′weaken-closed : {V∀} {xA} → x{Γ} ∈⊢V V= →context-lemma ∅Γ~Γ′ x ≡ Γ x⊢V
Γ~Γ′ {x} x∈V = ⊥-elim (x∉V x∈V)
- where
- x∉VΓ~Γ′ : ∀ {x} → x ∈ V → ∅ x ≡ Γ : ¬ (x ∈
+ Γ~Γ′ V{x} x∈V = ⊥-elim (x∉V x∈V)
x∉V = ∅⊢-closed ⊢V {x}where
-
-just-injectivex∉V : ∀¬ {X : Set} {(x y∈ V)
+ x∉V := X}∅⊢-closed →⊢V _≡_ {A = Maybe Xx}
+
+just-injective (just: x)∀ (just{X y): → x ≡Set} {x y : X} → _≡_ {A = Maybe X} (just x) (just y) → x ≡ y
just-injective refl = refl
@@ -5419,937 +5464,937 @@ We need a couple of lemmas. A closed term can be weakened to any context, and `j
-preservation-[:=] {Γ} {x} {A} (Ax {Γ,x∶A} {x′} {B} [Γ,x∶A]x′≡B) ⊢V with x ≟{Γ} x′
-...|{x} {A} yes(Ax x≡x′{Γ,x∶A} rewrite{x′} just-injective{B} [Γ,x∶A]x′≡B = weaken-closed) ⊢V with x ≟ x′
...| no x≢x′ = Axyes x≡x′ rewrite just-injective [Γ,x∶A]x′≡B
-preservation-[:=] = weaken-closed {Γ} {x} {A} {λ[ x′ ∶ A′ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with x ≟ x′
...| no x≢x′ = Ax [Γ,x∶A]x′≡B
+preservation-[:=] {Γ} {x} {A} {λ[ x′ ∶ yesA′ x≡x′] N′} rewrite{.A′ x≡x′⇒ B′} {V=} context-lemma Γ′~Γ (⇒-I ⊢N′) ⊢V with x ≟ x′
- where
- Γ′~Γ...| :yes ∀x≡x′ {y}rewrite x≡x′ →= ycontext-lemma ∈Γ′~Γ (λ[ x′ ∶ A′ ] N′) →⇒-I (Γ , x′ ∶ A⊢N′) y ≡ Γ y
where
+ Γ′~Γ : ∀ {y} {→ y} ∈ (free-λλ[ x′≢y y∈N′) with x′ ∶ A′ ] N′) → (Γ , ≟x′ ∶ A) y ≡ Γ y
...| yes x′≡y =Γ′~Γ ⊥-elim{y} (x′≢yfree-λ x′≡yx′≢y y∈N′) with x′ ≟ y
...| no _ =yes refl
-...| nox′≡y x≢x′ = ⇒-I⊥-elim ⊢N′V(x′≢y x′≡y)
where...| no _ = refl
- x′x⊢N′...| : Γ , x′ ∶ A′ , x ∶no x≢x′ A= ⊢ N′ ∶ B′⇒-I ⊢N′V
where
+ x′x⊢N′ rewrite: update-permute Γ x, x′ ∶ A′ A, x′x A′∶ A x≢x′⊢ N′ =∶ ⊢N′B′
⊢N′Vx′x⊢N′ :rewrite (update-permute Γ , x′ ∶ A′) ⊢ N′ [ x := VA ]x′ ∶A′ B′x≢x′ = ⊢N′
⊢N′V =: preservation-[:=](Γ , x′ x′x⊢N′∶ ⊢V
-preservation-[:=] (⇒-E ⊢L ⊢MA′) ⊢V⊢ =N′ ⇒-E[ (preservation-[:=]x ⊢L:= ⊢V)V (preservation-[:=]] ⊢M∶ ⊢V)
-preservation-[:=] 𝔹-I₁ ⊢V = 𝔹-I₁
-preservation-[:=] 𝔹-I₂ ⊢V = 𝔹-I₂
-preservation-[:=] (𝔹-E ⊢L ⊢M ⊢N) ⊢V =B′
𝔹-E⊢N′V = preservation-[:=] x′x⊢N′ ⊢V
+preservation-[:=] (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V)
+preservation-[:=] 𝔹-I₁ ⊢V = 𝔹-I₁
+preservation-[:=] 𝔹-I₂ (preservation-[:=]⊢V = 𝔹-I₂
+preservation-[:=] (𝔹-E ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V) (preservation-[:=] ⊢N) ⊢V =
+ 𝔹-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V) (preservation-[:=] ⊢N ⊢V)
@@ -6365,95 +6410,95 @@ reduction preserves types.
-preservation : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹ N → ∅ ⊢ N ∶ A
@@ -6491,435 +6536,435 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
-preservation (Ax Γx≡A) ()
preservation (⇒-I ⊢N) ()
-preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV)(⇒-I = preservation-[:=] ⊢N) ()
+preservation ⊢V
-preservation (⇒-E ⊢L ⊢M) (ξ·₁⇒-I ⊢N) ⊢V) (βλ· valueV) = L⟹L′)preservation-[:=] with⊢N preservation⊢V ⊢L L⟹L′
...|preservation ⊢L′ = (⇒-E ⊢L′⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L′
preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL...| M⟹M′⊢L′ )= with⇒-E preservation⊢L′ ⊢M M⟹M′
...|preservation ⊢M′ = (⇒-E ⊢L ⊢M) (ξ·₂ ⊢L ⊢M′valueL
-preservation 𝔹-I₁ ()
-preservation 𝔹-I₂ ()
-preservation (𝔹-E 𝔹-I₁ ⊢M ⊢NM⟹M′) with preservation ⊢M M⟹M′
+...| ⊢M′ = ⇒-E ⊢L ⊢M′
+preservation 𝔹-I₁ βif-true = ⊢M()
preservation (𝔹-E 𝔹-I₂ ()
+preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) βif-false =βif-true ⊢N= ⊢M
preservation (𝔹-E ⊢L𝔹-I₂ ⊢M ⊢N) (ξif L⟹L′) withβif-false preservation= ⊢L L⟹L′⊢N
...|preservation ⊢L′ = (𝔹-E ⊢L′⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
+...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
@@ -6943,226 +6988,226 @@ term can _never_ reach a stuck state.
-Normal : Term → Set
-Normal M = ∀ {N} → ¬ (M ⟹ N)
-
-Stuck : Term →Term → Set
Stuck M = Normal M ×= ∀ {N} → ¬ Value(M M⟹ N)
Stuck : Term → Set
+Stuck M = Normal M × ¬ Value M
+
+postulate
Soundness : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹* N → ¬ (Stuck N)
@@ -7171,342 +7216,342 @@ term can _never_ reach a stuck state.
-Soundness′ : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹* N → ¬ (Stuck N)
-Soundness′ ⊢M{M (N A} → ∅ ⊢ M ∎)∶ (¬M⟹NA ,→ ¬ValueM)M with⟹* N → progress¬ (Stuck ⊢MN)
... | steps M⟹N = ¬M⟹N M⟹N
-... | done ValueM = ¬ValueM ValueM
-Soundness′ {L}⊢M {N} {A} ⊢L (_⟹⟨_⟩_ .L {M} {.N} L⟹M M⟹*N∎) (¬M⟹N , ¬ValueM) with progress ⊢M
+... | steps M⟹N = ¬M⟹N M⟹N
+... | done ValueM = ¬ValueM ValueM
+Soundness′ {L} ⊢M{N} M⟹*N{A}
- where
- ⊢M :⊢L ∅(_⟹⟨_⟩_ ⊢.L {M} ∶{.N} AL⟹M M⟹*N) = Soundness′ ⊢M M⟹*N
where
+ ⊢M : ∅ ⊢ M ∶ A
+ ⊢M = preservation ⊢L L⟹M
@@ -7517,6 +7562,7 @@ term can _never_ reach a stuck state.
## Uniqueness of Types
#### Exercise: 3 stars (types_unique)
+
Another nice property of the STLC is that types are unique: a
given term (in a given context) has at most one type.
Formalize this statement and prove it.
@@ -7525,20 +7571,21 @@ Formalize this statement and prove it.
## Additional Exercises
#### Exercise: 1 star (progress_preservation_statement)
+
Without peeking at their statements above, write down the progress
and preservation theorems for the simply typed lambda-calculus.
-``
#### Exercise: 2 stars (stlc_variation1)
+
Suppose we add a new term `zap` with the following reduction rule
--------- (ST_Zap)
- t ==> zap
+ M ⟹ zap
and the following typing rule:
- ---------------- (T_Zap)
- Gamma \vdash zap : T
+ ----------- (T_Zap)
+ Γ ⊢ zap : A
Which of the following properties of the STLC remain true in
the presence of these rules? For each property, write either
@@ -7553,14 +7600,15 @@ false, give a counterexample.
#### Exercise: 2 stars (stlc_variation2)
+
Suppose instead that we add a new term `foo` with the following
reduction rules:
- ----------------- (ST_Foo1)
- (\lambda x:A. x) ==> foo
+ ---------------------- (ST_Foo1)
+ (λ[ x ∶ A ] ` x) ⟹ foo
- ------------ (ST_Foo2)
- foo ==> true
+ ----------- (ST_Foo2)
+ foo ⟹ true
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@@ -7574,9 +7622,10 @@ false, give a counterexample.
- Preservation
#### Exercise: 2 stars (stlc_variation3)
-Suppose instead that we remove the rule `Sapp1` from the `step`
+
+Suppose instead that we remove the rule `ξ·₁` from the `⟹`
relation. Which of the following properties of the STLC remain
-true in the presence of this rule? For each one, write either
+true in the absence of this rule? For each one, write either
"remains true" or else "becomes false." If a property becomes
false, give a counterexample.
@@ -7591,7 +7640,7 @@ Suppose instead that we add the following new rule to the
reduction relation:
---------------------------------- (ST_FunnyIfTrue)
- (if true then t_1 else t_2) ==> true
+ (if true then t_1 else t_2) ⟹ true
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@@ -7605,15 +7654,15 @@ false, give a counterexample.
- Preservation
-
#### Exercise: 2 stars, optional (stlc_variation5)
+
Suppose instead that we add the following new rule to the typing
relation:
- Gamma \vdash t_1 : bool→bool→bool
- Gamma \vdash t_2 : bool
+ Γ ⊢ L ∶ 𝔹 ⇒ 𝔹 ⇒ 𝔹
+ Γ ⊢ M ∶ 𝔹
------------------------------ (T_FunnyApp)
- Gamma \vdash t_1 t_2 : bool
+ Γ ⊢ L · M ∶ 𝔹
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@@ -7632,10 +7681,10 @@ false, give a counterexample.
Suppose instead that we add the following new rule to the typing
relation:
- Gamma \vdash t_1 : bool
- Gamma \vdash t_2 : bool
+ Γ ⊢ L ∶ 𝔹
+ Γ ⊢ M ∶ 𝔹
--------------------- (T_FunnyApp')
- Gamma \vdash t_1 t_2 : bool
+ Γ ⊢ L · M ∶ 𝔹
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@@ -7651,11 +7700,12 @@ false, give a counterexample.
#### Exercise: 2 stars, optional (stlc_variation7)
+
Suppose we add the following new rule to the typing relation
of the STLC:
- ------------------- (T_FunnyAbs)
- \vdash \lambda x:bool.t : bool
+ -------------------- (T_FunnyAbs)
+ ∅ ⊢ λ[ x ∶ 𝔹 ] N ∶ 𝔹
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@@ -7676,27 +7726,309 @@ programming language, let's extend it with a concrete base
type of numbers and some constants and primitive
operators.
-To types, we add a base type of natural numbers (and remove
+To types, we add a base type of numbers (and remove
booleans, for brevity).
-Inductive ty : Type :=
- | TArrow : ty → ty → ty
- | TNat : ty.
+
+
+data Type′ : Set where
+ _⇒_ : Type′ → Type′ → Type′
+ ℕ : Type′
+
+
To terms, we add natural number constants, along with
-successor, predecessor, multiplication, and zero-testing.
+plus, minus, and testing for zero.
-Inductive tm : Type :=
- | tvar : id → tm
- | tapp : tm → tm → tm
- | tabs : id → ty → tm → tm
- | tnat : nat → tm
- | tsucc : tm → tm
- | tpred : tm → tm
- | tmult : tm → tm → tm
- | tif0 : tm → tm → tm → tm.
+
+
+data Term′ : Set where
+ `_ : Id → Term′
+ λ[_∶_]_ : Id → Type′ → Term′ → Term′
+ _·_ : Term′ → Term′ → Term′
+ ‶_ : Data.Nat.ℕ → Term′
+ _+_ : Term′ → Term′ → Term′
+ _-_ : Term′ → Term′ → Term′
+ if0_then_else_ : Term′ → Term′ → Term′ → Term′
+
+
+
+(Assume that `m - n` returns `0` if `m` is less than `n`.)
#### Exercise: 4 stars (stlc_arith)
+
Finish formalizing the definition and properties of the STLC extended
with arithmetic. Specifically:
diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index 827ce723..10ea0dcf 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -4,7 +4,35 @@ layout : page
permalink : /Stlc
---
-This chapter defines the simply-typed lambda calculus.
+The _lambda-calculus_, first published by the logician Alonzo Church in
+1932, is a core calculus with only three syntactic constructs:
+variables, abstraction, and application. It embodies the concept of
+_functional abstraction_, which shows up in almsot every programming
+language in some form (as functions, procedures, or methods).
+The _simply-typed lambda calculus_ (or STLC) is a variant of the
+lambda calculus published by Church in 1940. It has just the three
+constructs above for function types, plus whatever else is required
+for base types. Church had a minimal base type with no operations;
+we will be slightly more pragmatic and choose booleans as our base type.
+
+This chapter formalises the STLC (syntax, small-step semantics, and typing rules),
+and the next chapter reviews its main properties (progress and preservation).
+The new technical challenges arise from the mechanisms of
+_variable binding_ and _substitution_.
+
+We've already seen how to formalize a language with
+variables ([Imp]({{ "Imp" | relative_url }})).
+There, however, the variables were all global.
+In the STLC, we need to handle the variables that name the
+parameters to functions, and these are _bound_ variables.
+Moreover, instead of just looking up variables in a global store,
+we'll need to reduce function applications by _substituting_
+arguments for parameters in function bodies.
+
+We choose booleans as our base type for simplicity. At the end of the
+chapter we'll see how to add naturals as a base type, and in later
+chapters we'll enrich STLC with useful constructs like pairs, sums,
+lists, records, subtyping, and mutable state.
## Imports
@@ -17,10 +45,9 @@ open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
\end{code}
-
## Syntax
-Syntax of types and terms.
+We have just two types, function types and booleans.
\begin{code}
infixr 20 _⇒_
@@ -28,7 +55,15 @@ infixr 20 _⇒_
data Type : Set where
_⇒_ : Type → Type → Type
𝔹 : Type
+\end{code}
+Each type introduces its own constructs, which come in pairs,
+one to introduce (or construct) values of the type, and one to eliminate
+(or deconstruct) them.
+
+CONTINUE FROM HERE
+
+\begin{code}
infixl 20 _·_
infix 15 λ[_∶_]_
infix 15 if_then_else_