From 31aece11442a4a05d2f32ede369f5d7cc91efedf Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 4 Jul 2017 18:33:27 +0100 Subject: [PATCH] revising Stlc and StlcProp --- src/Maps.lagda | 49 +++++++++++++--------------- src/Stlc.lagda | 79 ++++------------------------------------------ src/StlcProp.lagda | 53 +++++++++++++++++-------------- 3 files changed, 59 insertions(+), 122 deletions(-) diff --git a/src/Maps.lagda b/src/Maps.lagda index e3747980..34194ebf 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -36,7 +36,6 @@ standard library, wherever they overlap. open import Data.Nat using (ℕ) open import Data.Empty using (⊥; ⊥-elim) open import Data.Maybe using (Maybe; just; nothing) --- open import Data.String using (String) open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_; trans; sym) @@ -54,7 +53,7 @@ we repeat its definition here. \begin{code} data Id : Set where - id : ℕ → Id {- String → Id -} + id : ℕ → Id \end{code} We recall a standard fact of logic. @@ -69,7 +68,7 @@ by deciding equality on the underlying strings. \begin{code} _≟_ : (x y : Id) → Dec (x ≡ y) -id x ≟ id y with x Data.Nat.≟ y {- x Data.String.≟ y -} +id x ≟ id y with x Data.Nat.≟ y id x ≟ id y | yes refl = yes refl id x ≟ id y | no x≢y = no (contrapositive id-inj x≢y) where @@ -77,15 +76,6 @@ id x ≟ id y | no x≢y = no (contrapositive id-inj x≢y) id-inj refl = refl \end{code} -We define some identifiers for future use. - -\begin{code} -x y z : Id -x = id 0 -- id "x" -y = id 1 -- id "y" -z = id 2 -- id "z" -\end{code} - ## Total Maps Our main job in this chapter will be to build a definition of @@ -135,8 +125,8 @@ takes `x` to `v` and takes every other key to whatever `ρ` does. _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A (ρ , x ↦ v) y with x ≟ y - ... | yes x=y = v - ... | no x≠y = ρ y + ... | yes x≡y = v + ... | no x≢y = ρ y \end{code} This definition is a nice example of higher-order programming. @@ -147,25 +137,30 @@ For example, we can build a map taking ids to naturals, where `x` maps to 42, `y` maps to 69, and every other key maps to 0, as follows: \begin{code} - ρ₀ : TotalMap ℕ - ρ₀ = always 0 , x ↦ 42 , y ↦ 69 + module example where + + x y z : Id + x = id 0 + y = id 1 + z = id 2 + + ρ₀ : TotalMap ℕ + ρ₀ = always 0 , x ↦ 42 , y ↦ 69 + + test₁ : ρ₀ x ≡ 42 + test₁ = refl + + test₂ : ρ₀ y ≡ 69 + test₂ = refl + + test₃ : ρ₀ z ≡ 0 + test₃ = refl \end{code} This completes the definition of total maps. Note that we don't need to define a `find` operation because it is just function application! -\begin{code} - test₁ : ρ₀ x ≡ 42 - test₁ = refl - - test₂ : ρ₀ y ≡ 69 - test₂ = refl - - test₃ : ρ₀ z ≡ 0 - test₃ = refl -\end{code} - To use maps in later chapters, we'll need several fundamental facts about how they behave. Even if you don't work the following exercises, make sure you understand the statements of diff --git a/src/Stlc.lagda b/src/Stlc.lagda index ac177416..d883ba74 100644 --- a/src/Stlc.lagda +++ b/src/Stlc.lagda @@ -7,10 +7,10 @@ permalink : /Stlc This chapter defines the simply-typed lambda calculus. ## Imports + \begin{code} open import Maps using (Id; id; _≟_; PartialMap; module PartialMap) open PartialMap using (∅) renaming (_,_↦_ to _,_∶_) --- open import Data.String using (String) open import Data.Nat using (ℕ) open import Data.Maybe using (Maybe; just; nothing) open import Relation.Nullary using (Dec; yes; no) @@ -45,8 +45,8 @@ data Term : Set where Example terms. \begin{code} f x : Id -f = id 0 -- id "f" -x = id 1 -- id "x" +f = id 0 +x = id 1 not two : Term not = λ[ x ∶ 𝔹 ] (if var x then false else true) @@ -104,26 +104,6 @@ data _⟹_ : Term → Term → Set where ## Reflexive and transitive closure -\begin{code} -{- -Rel : Set → Set₁ -Rel A = A → A → Set - -infixl 10 _>>_ - -data _* {A : Set} (R : Rel A) : Rel A where - ⟨⟩ : ∀ {x : A} → (R *) x x - ⟨_⟩ : ∀ {x y : A} → R x y → (R *) x y - _>>_ : ∀ {x y z : A} → (R *) x y → (R *) y z → (R *) x z - -infix 10 _⟹*_ - -_⟹*_ : Rel Term -_⟹*_ = (_⟹_) * --} -\end{code} - -## Notation for setting out reductions \begin{code} infix 10 _⟹*_ @@ -164,50 +144,6 @@ reduction₂ = Much of the above, though not all, can be filled in using C-c C-r and C-c C-s. -\begin{code} -{- -infixr 2 _⟹⟨_⟩_ -infix 3 _∎ - -_⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N -L ⟹⟨ L⟹M ⟩ M⟹*N = ⟨ L⟹M ⟩ >> M⟹*N - -_∎ : ∀ M → M ⟹* M -M ∎ = ⟨⟩ --} -\end{code} - -## Example reduction derivations - -\begin{code} -{- -reduction₁ : not · true ⟹* false -reduction₁ = - not · true - ⟹⟨ β⇒ value-true ⟩ - if true then false else true - ⟹⟨ β𝔹₁ ⟩ - false - ∎ - -reduction₂ : two · not · true ⟹* true -reduction₂ = - two · not · true - ⟹⟨ γ⇒₁ (β⇒ value-λ) ⟩ - (λ[ x ∶ 𝔹 ] not · (not · var x)) · true - ⟹⟨ β⇒ value-true ⟩ - not · (not · true) - ⟹⟨ γ⇒₂ value-λ (β⇒ value-true) ⟩ - not · (if true then false else true) - ⟹⟨ γ⇒₂ value-λ β𝔹₁ ⟩ - not · false - ⟹⟨ β⇒ value-false ⟩ - if false then false else true - ⟹⟨ β𝔹₂ ⟩ - true - ∎ --} -\end{code} ## Type rules @@ -255,20 +191,19 @@ We start with the declaration: typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹 typing₁ = ? -Typing C-L (control L) causes Agda to create a hole and tell us its -expected type. +Typing C-l causes Agda to create a hole and tell us its expected type. typing₁ = { }0 ?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹 -Now we fill in the hole by typing C-R (control R). Agda observes that +Now we fill in the hole by typing C-c C-r. Agda observes that the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which Agda leaves as a hole. typing₁ = ⇒-I { }0 ?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹 -Again we fill in the hole by typing C-R. Agda observes that the +Again we fill in the hole by typing C-c C-r. Agda observes that the outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes three arguments, which Agda leaves as holes. @@ -277,7 +212,7 @@ outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The ?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹 ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹 -Again we fill in the three holes by typing C-R in each. Agda observes +Again we fill in the three holes by typing C-c C-r in each. Agda observes that `var x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and `𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a diff --git a/src/StlcProp.lagda b/src/StlcProp.lagda index b997cd4f..def68cac 100644 --- a/src/StlcProp.lagda +++ b/src/StlcProp.lagda @@ -193,16 +193,16 @@ A variable `x` appears _free_ in a term `M` if `M` contains an occurrence of `x` that is not bound in an outer lambda abstraction. For example: - - `x` appears free, but `f` does not, in `λ[ f ∶ (A ⇒ B) ] f · x` - - both `f` and `x` appear free in `(λ[ f ∶ (A ⇒ B) ] f · x) · f`; + - `x` appears free, but `f` does not, in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x` + - both `f` and `x` appear free in `(λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f`; note that `f` appears both bound and free in this term - - no variables appear free in `λ[ f ∶ (A ⇒ B) ] (λ[ x ∶ A ] f · x)` + - no variables appear free in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x` Formally: \begin{code} data _∈_ : Id → Term → Set where - free-var : ∀ {x} → x ∈ (var x) + free-var : ∀ {x} → x ∈ var x free-λ : ∀ {x y A N} → y ≢ x → x ∈ N → x ∈ (λ[ y ∶ A ] N) free-·₁ : ∀ {x L M} → x ∈ L → x ∈ (L · M) free-·₂ : ∀ {x L M} → x ∈ M → x ∈ (L · M) @@ -215,37 +215,44 @@ A term in which no variables appear free is said to be _closed_. \begin{code} _∉_ : Id → Term → Set -x ∉ M = x ∈ M → ⊥ +x ∉ M = ¬ (x ∈ M) closed : Term → Set closed M = ∀ {x} → x ∉ M \end{code} -#### Exercise: 1 star (free-in) -Prove formally the properties listed above. +Here are proofs corresponding to the first two examples above. \begin{code} -{- -example-free₁ : x ∈ (λ[ f ∶ (A ⇒ B) ] f · x) -example-free₁ = ? -example-free₂ : f ∉ (λ[ f ∶ (A ⇒ B) ] f · x) -example-free₂ = ? -example-free₃ : x ∈ (λ[ f ∶ (A ⇒ B) ] f · x) -example-free₃ = ? -example-free₄ : f ∈ (λ[ f ∶ (A ⇒ B) ] f · x) -example-free₄ = ? --} +f≢x : f ≢ x +f≢x () + +example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) +example-free₁ = free-λ f≢x (free-·₂ free-var) + +example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) +example-free₂ (free-λ f≢x (free-·₁ free-var)) = f≢x refl +example-free₂ (free-λ f≢x (free-·₂ ())) \end{code} -If the definition of `_∈_` is not crystal clear to -you, it is a good idea to take a piece of paper and write out the -rules in informal inference-rule notation. (Although it is a -rather low-level, technical definition, understanding it is -crucial to understanding substitution and its properties, which -are really the crux of the lambda-calculus.) +#### Exercise: 1 star (free-in) +Prove formally the remaining examples given above. + +\begin{code} +postulate + example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f) + example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f) + example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x) + example-free₆ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x) +\end{code} + +Although `_∈_` may apperar to be a low-level technical definition, +understanding it is crucial to understanding the properties of +substitution, which are really the crux of the lambda calculus. ### Substitution + To prove that substitution preserves typing, we first need a technical lemma connecting free variables and typing contexts: If a variable `x` appears free in a term `M`, and if we know `M` is