diff --git a/out/StlcProp.md b/out/StlcProp.md index 45a6b18f..15722646 100644 --- a/out/StlcProp.md +++ b/out/StlcProp.md @@ -4,795 +4,793 @@ layout : page permalink : /StlcProp --- -
- -open import Function using (_∘_) -open import Data.Empty using (⊥; ⊥-elim) -open import Data.Bool using (Bool; true; false) -open import Data.Maybe using (Maybe; just; nothing) -open import Data.Product using (∃; ∃₂; _,_; ,_) -open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Relation.Nullary using (¬_; Dec; yes; no) -open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym) -open import Maps -open Maps.PartialMap -open import Stlc - -- In this chapter, we develop the fundamental theory of the Simply Typed Lambda Calculus---in particular, the type safety theorem. +## Imports + +
{% raw %} +open import Function using (_∘_) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Bool using (Bool; true; false) +open import Data.Maybe using (Maybe; just; nothing) +open import Data.Product using (∃; ∃₂; _,_; ,_) +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym) +open import Maps +open Maps.PartialMap +open import Stlc +{% endraw %}+ ## Canonical Forms -As we saw for the simple calculus in the [Stlc]({{ "Stlc" | relative_url }}) +As we saw for the simple calculus in the [Stlc] chapter, the first step in establishing basic properties of reduction and types is to identify the possible _canonical forms_ (i.e., well-typed closed values) belonging to each type. For `bool`, these are the boolean values `true` and `false`. For arrow types, the canonical forms are lambda-abstractions. -
- -{% raw %} +data canonical_for_ : canonical_for_ : Term → Type → Set where canonical-λᵀ : ∀ {x A N B} → canonical N B} → canonical (λᵀ x ∈ A ⇒ N) for (A ⇒ B) canonical-trueᵀ : canonical trueᵀ for 𝔹 canonical-falseᵀ : canonical falseᵀ canonical falseᵀ for 𝔹 -- canonical_for_ : Term → Type → Set -- canonical L for 𝔹 = L ≡ trueᵀ ⊎ L ≡ falseᵀ -- canonical L for (A ⇒ B) = ∃₂ λ x N → L ≡ λᵀ x ∈ A ⇒ N canonicalFormsLemma : ∀ {L A} → ∅ ⊢ L ∈ A → A} → ∅ ⊢ L ∈ A → value L → canonical L for A canonicalFormsLemma (Ax ⊢x) () canonicalFormsLemma (⇒-I ⊢N) value-λᵀ = canonical-λᵀ -- _ , _ , refl canonicalFormsLemma (⇒-E ⊢L ⊢M) () canonicalFormsLemma 𝔹-I₁ value-trueᵀ 𝔹-I₁ value-trueᵀ = canonical-trueᵀ -- inj₁ refl canonicalFormsLemma 𝔹-I₂ value-falseᵀ = canonical-falseᵀ -- inj₂ refl canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) () - -+{% endraw %} ## Progress @@ -803,101 +801,99 @@ straightforward extension of the progress proof we saw in the [Stlc]({{ "Stlc" | relative_url }}) chapter. We'll give the proof in English first, then the formal version. -
- -{% raw %} +progress : ∀ {M A} → ∅ ⊢ M ∈ A → A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N - -+{% endraw %} _Proof_: By induction on the derivation of `\vdash t : A`. @@ -937,830 +933,826 @@ _Proof_: By induction on the derivation of `\vdash t : A`. - Otherwise, `t_1` takes a step, and therefore so does `t` (by `if`). -
- -{% raw %} +progress (Ax ()) +progress (Ax ()) -progress (⇒-I ⊢N) = inj₁ value-λᵀ progress (⇒-E {Γ} {L} {M} (⇒-E {Γ} {L} {M} {A} {B} ⊢L ⊢M) with progress ⊢L ... | inj₂ (L′ , L⟹L′) = inj₂ (L′ , L⟹L′) = inj₂ (L′ ·ᵀ M , γ⇒₁ L⟹L′) +... | inj₁ L⟹L′) -...valueL |with inj₁ valueL with progress ⊢M ... | inj₂ (M′ , M⟹M′) inj₂ (M′ , M⟹M′) = inj₂ (L ·ᵀ M′ , γ⇒₂ valueL M⟹M′) +... valueL| inj₁ M⟹M′) -...valueM |with inj₁ valueM with canonicalFormsLemma ⊢L valueL ... | canonical-λᵀ {x} canonical-λᵀ {x} {.A} {N} {.B} = inj₂ ((N [ x := M ]) , β⇒ [ x := M ]valueM) , β⇒ +progress valueM) -progress 𝔹-I₁ = inj₁ value-trueᵀ progress 𝔹-I₂ = inj₁ value-falseᵀ progress (𝔹-E {Γ} {L} {M} (𝔹-E {Γ} {L} {M} {N} {A} ⊢L ⊢M ⊢N) with progress ⊢L ... | inj₂ (L′ , L⟹L′) inj₂ (L′ , L⟹L′) = inj₂ ((ifᵀ L′ then M else N) , thenγ𝔹 M else NL⟹L′) +... | , γ𝔹inj₁ L⟹L′) -...valueL |with inj₁ valueL with canonicalFormsLemma ⊢L valueL ... | canonical-trueᵀ = inj₂ (M , β𝔹₁) ... | canonical-falseᵀ canonical-falseᵀ = inj₂ (N , β𝔹₂) - -+{% endraw %} #### Exercise: 3 stars, optional (progress_from_term_ind) Show that progress can also be proved by induction on terms instead of induction on typing derivations. -
- -{% raw %} +postulate progress′ : ∀ {M A} → ∅ ⊢ M ∈ A → A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N - -+{% endraw %} ## Preservation @@ -1816,683 +1808,679 @@ For example: Formally: -
- -{% raw %} +data _FreeIn_ : Id → Term → Set where free-varᵀ : ∀ {x} → x FreeIn ∀ {x}(varᵀ → x FreeIn (varᵀ x) free-λᵀ : ∀ {x y A N} → y ≢ x → yx A N} →FreeIn yN ≢→ x → x FreeIn (λᵀ Ny →∈ xA FreeIn (λᵀ y ∈ A ⇒ N) free-·ᵀ₁ : ∀ {x L M} → x FreeIn L → x → x FreeIn (L ·ᵀ → x FreeIn (LM) + free-·ᵀ₂ ·ᵀ M) - free-·ᵀ₂ : ∀ {x L M} → x FreeIn M → x → x FreeIn M(L ·ᵀ →M) + free-ifᵀ₁ x FreeIn (L ·ᵀ: M) - free-ifᵀ₁ : ∀ {x L M N} → x FreeIn L → x → x FreeIn L → x FreeIn (ifᵀ L then M else N) + free-ifᵀ₂ : N) - free-ifᵀ₂ : ∀ {x L M N} → x FreeIn M → x → x FreeIn M → x FreeIn (ifᵀ L then M else N) free-ifᵀ₃ : ∀ {x L M N} → x FreeIn N → x → x FreeIn N → x FreeIn (ifᵀ L then M else N) - -+{% endraw %} A term in which no variables appear free is said to be _closed_. -
- -{% raw %} +closed : Term → Set +closed M = →∀ Set{x} -closed → ¬ (x M = ∀ {x} → ¬ (x FreeIn M) - -+{% endraw %} #### Exercise: 1 star (free-in) If the definition of `_FreeIn_` is not crystal clear to @@ -2509,121 +2497,119 @@ a variable `x` appears free in a term `M`, and if we know `M` is well typed in context `Γ`, then it must be the case that `Γ` assigns a type to `x`. -
- -{% raw %} +freeLemma : ∀ {x M A Γ} → x FreeIn M → Γ →⊢ xM FreeIn M → Γ ⊢ M ∈ A → ∃ λ B → Γ x ≡ just λ B → Γ x ≡ just B - -+{% endraw %} _Proof_: We show, by induction on the proof that `x` appears free in `P`, that, for all contexts `Γ`, if `P` is well @@ -2654,460 +2640,458 @@ _Proof_: We show, by induction on the proof that `x` appears assigns a type to `x`, we appeal the decidable equality for names `_≟_`, noting that `x` and `y` are different variables. -
- -{% raw %} +freeLemma free-varᵀ (Ax Γx≡justA) = (_ , Γx≡justA) = (_ , Γx≡justA) freeLemma (free-·ᵀ₁ x∈L) (⇒-E ⊢L ⊢M) x∈L) (⇒-E ⊢L ⊢M) = freeLemma x∈L ⊢L +freeLemma x∈L ⊢L -freeLemma (free-·ᵀ₂ x∈M) (⇒-E ⊢L ⊢M) x∈M) (⇒-E ⊢L ⊢M) = freeLemma x∈M ⊢M +freeLemma x∈M ⊢M -freeLemma (free-ifᵀ₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) = (𝔹-EfreeLemma x∈L ⊢L ⊢M ⊢N) = +freeLemma x∈L ⊢L -freeLemma (free-ifᵀ₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = (𝔹-EfreeLemma ⊢Lx∈M ⊢M ⊢N) = +freeLemma x∈M ⊢M -freeLemma (free-ifᵀ₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = (𝔹-EfreeLemma ⊢Lx∈N ⊢M ⊢N) = +freeLemma x∈N(free-λᵀ ⊢N -freeLemma{x} {y} (free-λᵀy≢x x∈N) {x} {y} y≢x x∈N) (⇒-I ⊢N) with freeLemma x∈N ⊢N ... | Γx=justC with y ≟ x +... | withyes yy≡x ≟= x -... |⊥-elim yes y≡x = ⊥-elim (y≢x y≡x) ... | no _ = Γx=justC - -+{% endraw %} [A subtle point: if the first argument of `free-λᵀ` was of type `x ≢ y` rather than of type `y ≢ x`, then the type of the @@ -3118,370 +3102,366 @@ the empty context is closed (it has no free variables). #### Exercise: 2 stars, optional (∅⊢-closed) -
- -{% raw %} +postulate ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∈ A → A} → ∅closed ⊢ M ∈ A → closed M - -+{% endraw %}
- -{% raw %} +contradiction : ∀ {X : Set} → ∀ {x {X : X} Set} → ∀¬ (_≡_ {xA := Maybe X} → ¬ (_≡_} {A(just = Maybe X} (just x) nothing) contradiction () + +∅⊢-closed′ : () - -∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ∈ A → A} → ∅closed ⊢ M +∅⊢-closed′ ∈ A → closed{M} M -∅⊢-closed′ {M} {A} ⊢M {x} x∈M with freeLemma x∈M ⊢M ... | (B , ∅x≡justB) |= (B , ∅x≡justB) = contradiction (trans (sym ∅x≡justB) (apply-∅ x)) - -+{% endraw %}
- -{% raw %} +weaken : ∀ {Γ Γ′ M A} + → (∀ {x} - → (∀→ x FreeIn M {x}→ Γ →x x≡ FreeIn M → Γ x ≡ Γ′ x) → Γ ⊢ M ∈ A + → Γ′ ∈⊢ A - → Γ′ ⊢ M ∈ A - -+{% endraw %} _Proof_: By induction on the derivation of `Γ ⊢ M ∈ A`. @@ -3678,202 +3656,233 @@ _Proof_: By induction on the derivation of `t_1` are also free in `t_1\;t_2`, and similarly for `t_2`; hence the desired result follows from the induction hypotheses. -
- -{% raw %} +weaken Γ~Γ′ (Ax Γx≡justA) rewrite (Γ~Γ′ free-varᵀ) (Γ~Γ′ free-varᵀ) = Ax Γx≡justA weaken {Γ} {Γ′} {λᵀ x ∈ {Γ}A ⇒ {Γ′N} {λᵀΓ~Γ′ x ∈(⇒-I A ⇒⊢N) N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (weaken Γx~Γ′x ⊢N) where Γx~Γ′x : ∀ {y} → y FreeIn ∀N {y→ } → y FreeIn N → (Γ , x ↦ A) y ≡ (Γ′ , x ↦ A) y ≡ (Γ′ , x ↦ A) y Γx~Γ′x {y} y∈N with x ≟ {y} y∈N + ... with x ≟ y - ... | yes refl = refl ... | no x≢y = Γ~Γ′ (free-λᵀ x≢y y∈N) +weaken Γ~Γ′ y∈N)(⇒-E -weaken ⊢L ⊢M) Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (weaken (Γ~Γ′ ∘ free-·ᵀ₁) ⊢L) ∘ free-·ᵀ₁) ⊢L) (weaken (Γ~Γ′ ∘ free-·ᵀ₂) ⊢M) weaken Γ~Γ′ 𝔹-I₁ = 𝔹-I₁ +weaken Γ~Γ′ 𝔹-I₁𝔹-I₂ = 𝔹-I₂ weaken Γ~Γ′ 𝔹-I₂ = 𝔹-I₂ -weaken Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (weaken (Γ~Γ′ ∘ free-ifᵀ₁) ⊢L) ∘ free-ifᵀ₁) ⊢L) (weaken (Γ~Γ′ ∘ free-ifᵀ₂) ⊢M) ∘ free-ifᵀ₂) ⊢M) (weaken (Γ~Γ′ ∘ free-ifᵀ₃) ⊢N) {- replaceCtxt f (var x x∶A ) rewrite f var = var x x∶A @@ -4298,8 +4275,7 @@ replaceCtxt f (if t₁∶bool then t₂∶A else t₃∶ else replaceCtxt (f ∘ if3) t₃∶A -} - -+{% endraw %} Now we come to the conceptual heart of the proof that reduction @@ -4318,168 +4294,166 @@ and obtain a new term that still has type `B`. _Lemma_: If `Γ , x ↦ A ⊢ N ∈ B` and `∅ ⊢ V ∈ A`, then `Γ ⊢ (N [ x := V ]) ∈ B`. -
- -{% raw %} +preservation-[:=] : ∀ {Γ x A N B V} → (Γ , x ↦ A) ⊢ N ∈ B → ∅ ⊢ V ∈ A → Γ ⊢ (N [ x := V ]) ⊢∈ (N [ x := V ]) ∈ B - -+{% endraw %} One technical subtlety in the statement of the lemma is that we assign `V` the type `A` in the _empty_ context---in other @@ -4545,1345 +4519,1341 @@ _Proof_: We show, by induction on `N`, that for all `A` and - The remaining cases are similar to the application case. We need a couple of lemmas. A closed term can be weakened to any context, and just is injective. -
- -{% raw %} +weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∈ A A→ Γ} → ∅ ⊢ V ∈ A → Γ ⊢ V ∈ A weaken-closed {V} {A} {Γ} ⊢V = {V}weaken {A} {Γ}Γ~Γ′ ⊢V = weaken Γ~Γ′ ⊢V where Γ~Γ′ : ∀ {x} → x FreeIn ∀V {x}→ ∅ →x x≡ FreeIn V → ∅ x ≡ Γ x Γ~Γ′ {x} x∈V = ⊥-elim {x}(x∉V x∈V =) ⊥-elim (x∉V x∈V) where x∉V : ¬ (x FreeIn V) x∉V = ∅⊢-closed ⊢V {x} just-injective : ∀ {X : Set} {x :y ∀: {X} :→ Set}_≡_ {xA y= : X}Maybe →X} _≡_ {A(just = Maybe X} (just x) (just y) → x ≡ y +just-injective y -just-injective refl = refl +{% endraw %}- - -
- -{% raw %} +preservation-[:=] {_} {x} (Ax {_} {x′} {x} (Ax {_} {x′} [Γ,x↦A]x′≡B) ⊢V with x ≟ x′ +...| withyes x ≟x≡x′ x′ -...|rewrite yes x≡x′ rewrite just-injective [Γ,x↦A]x′≡B = weaken-closed ⊢V ...| no x≢x′ = Ax [Γ,x↦A]x′≡B preservation-[:=] {Γ} {x} {A} {λᵀ x′ ∈ {x} {A} {λᵀ x′ ∈ A′ ⇒ N′} {.A′ ⇒ B′} ⇒ N′} {.A′ ⇒ B′V} (⇒-I ⊢N′) ⊢V {V}with (⇒-Ix ≟ ⊢N′) ⊢V with x ≟ x′ ...| yes x≡x′ rewrite yes x≡x′ rewrite x≡x′ = weaken Γ′~Γ (⇒-I weaken Γ′~Γ (⇒-I ⊢N′) where Γ′~Γ : ∀ {y} → y FreeIn ∀ {y} → y FreeIn (λᵀ x′ ∈ A′ ⇒ N′) → (Γ , x′ ↦ A) y →≡ (Γ , x′ ↦ A) y + Γ′~Γ {y} ≡ Γ y - Γ′~Γ {y} (free-λᵀ x′≢y y∈N′) with x′ ≟ y ...| yes x′≡y = ⊥-elim (x′≢y x′≡y) ...| no _ = refl ...| no x≢x′ = ⇒-I ⊢N′V where x′x⊢N′ : Γ , x′ ↦ A′ , x ↦ A ⊢ N′ ∈ B′ + x′x⊢N′ N′ ∈ B′ - x′x⊢N′ rewrite update-permute Γ update-permutex A x′ A′ x≢x′ Γ= x A x′ A′ x≢x′ = ⊢N′ ⊢N′V : (Γ , x′ ↦ A′) ⊢ N′ [ x := V ] ∈ B′ ⊢N′V = preservation-[:=] x′x⊢N′ ⊢V preservation-[:=] (⇒-E ⊢L ⊢M) ⊢V = (⇒-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M) ⊢V = ⇒-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V) preservation-[:=] 𝔹-I₁ ⊢V = 𝔹-I₁ preservation-[:=] 𝔹-I₂ ⊢V = 𝔹-I₂ preservation-[:=] (𝔹-E ⊢L ⊢M ⊢N) ⊢V = 𝔹-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V) (preservation-[:=] ⊢N ⊢V) - -+{% endraw %} ### Main Theorem @@ -5893,101 +5863,99 @@ term `M` has type `A` and takes a step to `N`, then `N` is also a closed term with type `A`. In other words, small-step reduction preserves types. -
- -{% raw %} +preservation : ∀ {M N A} → ∅ ⊢ M ∈ A N→ A} → ∅ ⊢ M ∈ A → M ⟹ N → ∅ ⊢ N ∈ A - -+{% endraw %} _Proof_: By induction on the derivation of `\vdash t : T`. @@ -6020,457 +5988,455 @@ _Proof_: By induction on the derivation of `\vdash t : T`. - Otherwise, `t` steps by `Sif`, and the desired conclusion follows directly from the induction hypothesis. -
- -{% raw %} +preservation (Ax x₁) () preservation (⇒-I ⊢N) () preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒ (⇒-I ⊢N) ⊢V) (β⇒ valueV) = preservation-[:=] ⊢N ⊢V preservation (⇒-E ⊢L ⊢M) (γ⇒₁ (⇒-E ⊢L ⊢M) (γ⇒₁ L⟹L′) with preservation ⊢L L⟹L′ +...| ⊢L′ ⊢L L⟹L′ -...| ⊢L′ = ⇒-E ⊢L′ ⊢M preservation (⇒-E ⊢L ⊢M) (γ⇒₂ (⇒-E ⊢L ⊢M) (γ⇒₂ valueL M⟹M′) with preservation ⊢M M⟹M′ +...| ⊢M′ ⊢M= M⟹M′⇒-E ⊢L ⊢M′ ...| ⊢M′ = ⇒-E ⊢Lpreservation ⊢M′ -preservation 𝔹-I₁ () preservation 𝔹-I₂ () preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) (𝔹-E 𝔹-I₁ ⊢M ⊢N) β𝔹₁ = ⊢M preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) (𝔹-E 𝔹-I₂ ⊢M ⊢N) β𝔹₂ = ⊢N preservation (𝔹-E ⊢L ⊢M ⊢N) (γ𝔹 L⟹L′) ⊢M ⊢N) (γ𝔹 L⟹L′) with preservation ⊢L L⟹L′ +...| ⊢L′ ⊢L= L⟹L′ -...|𝔹-E ⊢L′ ⊢M ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N -- Writing out implicit parameters in full -- preservation (⇒-E {Γ} {λᵀ x ∈ A ⇒ N} {M} {.A} {B} (⇒-I {.Γ} {.x} {.N} {.A} {.B} ⊢N) ⊢M) (β⇒ {.x} {.A} {.N} {.M} valueM) -- = preservation-[:=] {Γ} {x} {A} {M} {N} {B} ⊢M ⊢N - -+{% endraw %} Proof with eauto. remember (@empty ty) as Gamma. diff --git a/src/Maps.lagda b/src/Maps.lagda index a8d8040d..08b2d397 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -131,7 +131,7 @@ a map `ρ`, a key `x`, and a value `v` and returns a new map that takes `x` to `v` and takes every other key to whatever `ρ` does. \begin{code} - infixl 100 _,_↦_ + infixl 15 _,_↦_ _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A (ρ , x ↦ v) y with x ≟ y @@ -335,7 +335,7 @@ module PartialMap where \end{code} \begin{code} - infixl 100 _,_↦_ + infixl 15 _,_↦_ _,_↦_ : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) → PartialMap A ρ , x ↦ v = TotalMap._,_↦_ ρ x (just v) diff --git a/src/Stlc.lagda b/src/Stlc.lagda index 66dd686b..effbcf7d 100644 --- a/src/Stlc.lagda +++ b/src/Stlc.lagda @@ -14,7 +14,6 @@ open import Data.String using (String) open import Data.Empty using (⊥; ⊥-elim) open import Data.Maybe using (Maybe; just; nothing) open import Data.Nat using (ℕ; suc; zero; _+_) -open import Data.Bool using (Bool; true; false; if_then_else_) open import Relation.Nullary using (Dec; yes; no) open import Relation.Nullary.Decidable using (⌊_⌋) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl) @@ -28,23 +27,26 @@ import Relation.Binary.PreorderReasoning as PreorderReasoning ## Syntax -Syntax of types and terms. All source terms are labeled with $ᵀ$. +Syntax of types and terms. \begin{code} -infixr 100 _⇒_ -infixl 100 _·ᵀ_ +infixr 20 _⇒_ data Type : Set where 𝔹 : Type _⇒_ : Type → Type → Type +infixl 20 _·_ +infix 15 λ[_∶_]_ +infix 15 if_then_else_ + data Term : Set where - varᵀ : Id → Term - λᵀ_∈_⇒_ : Id → Type → Term → Term - _·ᵀ_ : Term → Term → Term - trueᵀ : Term - falseᵀ : Term - ifᵀ_then_else_ : Term → Term → Term → Term + var : Id → Term + λ[_∶_]_ : Id → Type → Term → Term + _·_ : Term → Term → Term + true : Term + false : Term + if_then_else_ : Term → Term → Term → Term \end{code} Some examples. @@ -54,58 +56,63 @@ f = id "f" x = id "x" y = id "y" -I[𝔹] I[𝔹⇒𝔹] K[𝔹][𝔹] not[𝔹] : Term -I[𝔹] = (λᵀ x ∈ 𝔹 ⇒ (varᵀ x)) -I[𝔹⇒𝔹] = (λᵀ f ∈ (𝔹 ⇒ 𝔹) ⇒ (λᵀ x ∈ 𝔹 ⇒ ((varᵀ f) ·ᵀ (varᵀ x)))) -K[𝔹][𝔹] = (λᵀ x ∈ 𝔹 ⇒ (λᵀ y ∈ 𝔹 ⇒ (varᵀ x))) -not[𝔹] = (λᵀ x ∈ 𝔹 ⇒ (ifᵀ (varᵀ x) then falseᵀ else trueᵀ)) +I I² K not : Term +I = λ[ x ∶ 𝔹 ] var x +I² = λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] var f · var x +K = λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] var x +not = λ[ x ∶ 𝔹 ] (if var x then false else true) + +check : not ≡ λ[ x ∶ 𝔹 ] (if var x then false else true) +check = refl \end{code} ## Values \begin{code} -data value : Term → Set where - value-λᵀ : ∀ {x A N} → value (λᵀ x ∈ A ⇒ N) - value-trueᵀ : value (trueᵀ) - value-falseᵀ : value (falseᵀ) +data Value : Term → Set where + value-λ : ∀ {x A N} → Value (λ[ x ∶ A ] N) + value-true : Value true + value-false : Value false \end{code} ## Substitution \begin{code} -_[_:=_] : Term → Id → Term → Term -(varᵀ x′) [ x := V ] with x ≟ x′ +_[_∶=_] : Term → Id → Term → Term +(var x′) [ x ∶= V ] with x ≟ x′ ... | yes _ = V -... | no _ = varᵀ x′ -(λᵀ x′ ∈ A′ ⇒ N′) [ x := V ] with x ≟ x′ -... | yes _ = λᵀ x′ ∈ A′ ⇒ N′ -... | no _ = λᵀ x′ ∈ A′ ⇒ (N′ [ x := V ]) -(L′ ·ᵀ M′) [ x := V ] = (L′ [ x := V ]) ·ᵀ (M′ [ x := V ]) -(trueᵀ) [ x := V ] = trueᵀ -(falseᵀ) [ x := V ] = falseᵀ -(ifᵀ L′ then M′ else N′) [ x := V ] = ifᵀ (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ]) +... | no _ = var x′ +(λ[ x′ ∶ A′ ] N′) [ x ∶= V ] with x ≟ x′ +... | yes _ = λ[ x′ ∶ A′ ] N′ +... | no _ = λ[ x′ ∶ A′ ] (N′ [ x ∶= V ]) +(L′ · M′) [ x ∶= V ] = (L′ [ x ∶= V ]) · (M′ [ x ∶= V ]) +(true) [ x ∶= V ] = true +(false) [ x ∶= V ] = false +(if L′ then M′ else N′) [ x ∶= V ] = if (L′ [ x ∶= V ]) then (M′ [ x ∶= V ]) else (N′ [ x ∶= V ]) \end{code} ## Reduction rules \begin{code} +infix 10 _⟹_ + data _⟹_ : Term → Term → Set where - β⇒ : ∀ {x A N V} → value V → - ((λᵀ x ∈ A ⇒ N) ·ᵀ V) ⟹ (N [ x := V ]) + β⇒ : ∀ {x A N V} → Value V → + (λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ] γ⇒₁ : ∀ {L L' M} → L ⟹ L' → - (L ·ᵀ M) ⟹ (L' ·ᵀ M) + L · M ⟹ L' · M γ⇒₂ : ∀ {V M M'} → - value V → + Value V → M ⟹ M' → - (V ·ᵀ M) ⟹ (V ·ᵀ M') + V · M ⟹ V · M' β𝔹₁ : ∀ {M N} → - (ifᵀ trueᵀ then M else N) ⟹ M + if true then M else N ⟹ M β𝔹₂ : ∀ {M N} → - (ifᵀ falseᵀ then M else N) ⟹ N + if false then M else N ⟹ N γ𝔹 : ∀ {L L' M N} → L ⟹ L' → - (ifᵀ L then M else N) ⟹ (ifᵀ L' then M else N) + if L then M else N ⟹ if L' then M else N \end{code} ## Reflexive and transitive closure of a relation @@ -114,7 +121,7 @@ data _⟹_ : Term → Term → Set where Rel : Set → Set₁ Rel A = A → A → Set -infixl 100 _>>_ +infixl 10 _>>_ data _* {A : Set} (R : Rel A) : Rel A where ⟨⟩ : ∀ {x : A} → (R *) x x @@ -123,9 +130,9 @@ data _* {A : Set} (R : Rel A) : Rel A where \end{code} \begin{code} -infix 80 _⟹*_ +infix 10 _⟹*_ -_⟹*_ : Term → Term → Set +_⟹*_ : Rel Term _⟹*_ = (_⟹_) * \end{code} @@ -143,54 +150,42 @@ _⟹*_ = (_⟹_) * } open PreorderReasoning ⟹*-Preorder - using (begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_) + using (_IsRelatedTo_; begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_) + +infixr 2 _⟹*⟪_⟫_ + +_⟹*⟪_⟫_ : ∀ x {y z} → x ⟹ y → y IsRelatedTo z → x IsRelatedTo z +x ⟹*⟪ x⟹y ⟫ yz = x ⟹*⟨ ⟨ x⟹y ⟩ ⟩ yz \end{code} Example evaluation. \begin{code} -example₀′ : not[𝔹] ·ᵀ trueᵀ ⟹* falseᵀ -example₀′ = +example₀ : not · true ⟹* false +example₀ = begin - not[𝔹] ·ᵀ trueᵀ - ⟹*⟨ ⟨ β⇒ value-trueᵀ ⟩ ⟩ - ifᵀ trueᵀ then falseᵀ else trueᵀ - ⟹*⟨ ⟨ β𝔹₁ ⟩ ⟩ - falseᵀ + not · true + ⟹*⟪ β⇒ value-true ⟫ + if true then false else true + ⟹*⟪ β𝔹₁ ⟫ + false ∎ -example₀ : (not[𝔹] ·ᵀ trueᵀ) ⟹* falseᵀ -example₀ = ⟨ step₀ ⟩ >> ⟨ step₁ ⟩ - where - M₀ M₁ M₂ : Term - M₀ = (not[𝔹] ·ᵀ trueᵀ) - M₁ = (ifᵀ trueᵀ then falseᵀ else trueᵀ) - M₂ = falseᵀ - step₀ : M₀ ⟹ M₁ - step₀ = β⇒ value-trueᵀ - step₁ : M₁ ⟹ M₂ - step₁ = β𝔹₁ - -example₁ : (I[𝔹⇒𝔹] ·ᵀ I[𝔹] ·ᵀ (not[𝔹] ·ᵀ falseᵀ)) ⟹* trueᵀ -example₁ = ⟨ step₀ ⟩ >> ⟨ step₁ ⟩ >> ⟨ step₂ ⟩ >> ⟨ step₃ ⟩ >> ⟨ step₄ ⟩ - where - M₀ M₁ M₂ M₃ M₄ M₅ : Term - M₀ = (I[𝔹⇒𝔹] ·ᵀ I[𝔹] ·ᵀ (not[𝔹] ·ᵀ falseᵀ)) - M₁ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ (not[𝔹] ·ᵀ falseᵀ)) - M₂ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ (ifᵀ falseᵀ then falseᵀ else trueᵀ)) - M₃ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ trueᵀ) - M₄ = I[𝔹] ·ᵀ trueᵀ - M₅ = trueᵀ - step₀ : M₀ ⟹ M₁ - step₀ = γ⇒₁ (β⇒ value-λᵀ) - step₁ : M₁ ⟹ M₂ - step₁ = γ⇒₂ value-λᵀ (β⇒ value-falseᵀ) - step₂ : M₂ ⟹ M₃ - step₂ = γ⇒₂ value-λᵀ β𝔹₂ - step₃ : M₃ ⟹ M₄ - step₃ = β⇒ value-trueᵀ - step₄ : M₄ ⟹ M₅ - step₄ = β⇒ value-trueᵀ +example₁ : I² · I · (not · false) ⟹* true +example₁ = + begin + I² · I · (not · false) + ⟹*⟪ γ⇒₁ (β⇒ value-λ) ⟫ + (λ[ x ∶ 𝔹 ] I · var x) · (not · false) + ⟹*⟪ γ⇒₂ value-λ (β⇒ value-false) ⟫ + (λ[ x ∶ 𝔹 ] I · var x) · (if false then false else true) + ⟹*⟪ γ⇒₂ value-λ β𝔹₂ ⟫ + (λ[ x ∶ 𝔹 ] I · var x) · true + ⟹*⟪ β⇒ value-true ⟫ + I · true + ⟹*⟪ β⇒ value-true ⟫ + true + ∎ \end{code} ## Type rules @@ -199,26 +194,26 @@ example₁ = ⟨ step₀ ⟩ >> ⟨ step₁ ⟩ >> ⟨ step₂ ⟩ >> ⟨ step Context : Set Context = PartialMap Type -infix 50 _⊢_∈_ +infix 10 _⊢_∶_ -data _⊢_∈_ : Context → Term → Type → Set where +data _⊢_∶_ : Context → Term → Type → Set where Ax : ∀ {Γ x A} → Γ x ≡ just A → - Γ ⊢ varᵀ x ∈ A + Γ ⊢ var x ∶ A ⇒-I : ∀ {Γ x N A B} → - (Γ , x ↦ A) ⊢ N ∈ B → - Γ ⊢ (λᵀ x ∈ A ⇒ N) ∈ (A ⇒ B) + Γ , x ↦ A ⊢ N ∶ B → + Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B ⇒-E : ∀ {Γ L M A B} → - Γ ⊢ L ∈ (A ⇒ B) → - Γ ⊢ M ∈ A → - Γ ⊢ L ·ᵀ M ∈ B + Γ ⊢ L ∶ A ⇒ B → + Γ ⊢ M ∶ A → + Γ ⊢ L · M ∶ B 𝔹-I₁ : ∀ {Γ} → - Γ ⊢ trueᵀ ∈ 𝔹 + Γ ⊢ true ∶ 𝔹 𝔹-I₂ : ∀ {Γ} → - Γ ⊢ falseᵀ ∈ 𝔹 + Γ ⊢ false ∶ 𝔹 𝔹-E : ∀ {Γ L M N A} → - Γ ⊢ L ∈ 𝔹 → - Γ ⊢ M ∈ A → - Γ ⊢ N ∈ A → - Γ ⊢ (ifᵀ L then M else N) ∈ A + Γ ⊢ L ∶ 𝔹 → + Γ ⊢ M ∶ A → + Γ ⊢ N ∶ A → + Γ ⊢ if L then M else N ∶ A \end{code} diff --git a/src/StlcProp.lagda b/src/StlcProp.lagda index 14ba4032..4d2f503b 100644 --- a/src/StlcProp.lagda +++ b/src/StlcProp.lagda @@ -4,6 +4,12 @@ layout : page permalink : /StlcProp --- +In this chapter, we develop the fundamental theory of the Simply +Typed Lambda Calculus---in particular, the type safety +theorem. + +## Imports + \begin{code} open import Function using (_∘_) open import Data.Empty using (⊥; ⊥-elim) @@ -18,10 +24,6 @@ open Maps.PartialMap open import Stlc \end{code} -In this chapter, we develop the fundamental theory of the Simply -Typed Lambda Calculus---in particular, the type safety -theorem. - ## Canonical Forms @@ -54,16 +56,19 @@ canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) () As before, the _progress_ theorem tells us that closed, well-typed terms are not stuck: either a well-typed term is a value, or it -can take a reduction step. The proof is a relatively -straightforward extension of the progress proof we saw in the -[Stlc]({{ "Stlc" | relative_url }}) chapter. We'll give the proof in English -first, then the formal version. +can take a reduction step. \begin{code} progress : ∀ {M A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N \end{code} -_Proof_: By induction on the derivation of `\vdash t : A`. +The proof is a relatively +straightforward extension of the progress proof we saw in the +[Types]({{ "Types" | relative_url }}) chapter. +We'll give the proof in English +first, then the formal version. + +_Proof_: By induction on the derivation of `∅ ⊢ M ∈ A`. - The last rule of the derivation cannot be `var`, since a variable is never well typed in an empty context.