From 2cf5421261b9ee04ddde63885fabc02555c96f10 Mon Sep 17 00:00:00 2001 From: wadler Date: Thu, 29 Jun 2017 14:01:44 +0100 Subject: [PATCH] updated derivations in Stlc --- src/Stlc.lagda | 141 +++++++++++++++++++++++++++---------------------- 1 file changed, 79 insertions(+), 62 deletions(-) diff --git a/src/Stlc.lagda b/src/Stlc.lagda index 16eb8867..66f6738f 100644 --- a/src/Stlc.lagda +++ b/src/Stlc.lagda @@ -11,17 +11,9 @@ This chapter defines the simply-typed lambda calculus. open import Maps using (Id; id; _≟_; PartialMap; module PartialMap) open PartialMap using (∅) renaming (_,_↦_ to _,_∶_) 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 Relation.Nullary using (Dec; yes; no) -open import Relation.Nullary.Decidable using (⌊_⌋) -open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl) -open import Relation.Binary using (Preorder) -import Relation.Binary.PreorderReasoning as PreorderReasoning --- open import Relation.Binary.Core using (Rel) --- open import Data.Product using (∃; ∄; _,_) --- open import Function using (_∘_; _$_) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) \end{code} @@ -49,21 +41,15 @@ data Term : Set where if_then_else_ : Term → Term → Term → Term \end{code} -Some examples. +Example terms. \begin{code} -f x y : Id +f x : Id 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 two : Term not = λ[ x ∶ 𝔹 ] (if var x then false else true) - -check : not ≡ λ[ x ∶ 𝔹 ] (if var x then false else true) -check = refl +two = λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] var f · (var f · var x) \end{code} ## Values @@ -99,23 +85,23 @@ infix 10 _⟹_ data _⟹_ : Term → Term → Set where β⇒ : ∀ {x A N V} → Value V → (λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ] - γ⇒₁ : ∀ {L L' M} → + γ⇒₀ : ∀ {L L' M} → L ⟹ L' → L · M ⟹ L' · M - γ⇒₂ : ∀ {V M M'} → + γ⇒₁ : ∀ {V M M'} → Value V → M ⟹ M' → V · M ⟹ V · M' - β𝔹₁ : ∀ {M N} → + β𝔹₀ : ∀ {M N} → if true then M else N ⟹ M - β𝔹₂ : ∀ {M N} → + β𝔹₁ : ∀ {M 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 \end{code} -## Reflexive and transitive closure of a relation +## Reflexive and transitive closure \begin{code} Rel : Set → Set₁ @@ -127,65 +113,54 @@ 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 -\end{code} -\begin{code} infix 10 _⟹*_ _⟹*_ : Rel Term _⟹*_ = (_⟹_) * \end{code} +## Notation for setting out reductions + \begin{code} -⟹*-Preorder : Preorder _ _ _ -⟹*-Preorder = record - { Carrier = Term - ; _≈_ = _≡_ - ; _∼_ = _⟹*_ - ; isPreorder = record - { isEquivalence = P.isEquivalence - ; reflexive = λ {refl → ⟨⟩} - ; trans = _>>_ - } - } +infixr 2 _⟹⟨_⟩_ +infix 3 _∎ -open PreorderReasoning ⟹*-Preorder - using (_IsRelatedTo_; begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_) +_⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N +L ⟹⟨ L⟹M ⟩ M⟹*N = ⟨ L⟹M ⟩ >> M⟹*N -infixr 2 _⟹*⟪_⟫_ - -_⟹*⟪_⟫_ : ∀ x {y z} → x ⟹ y → y IsRelatedTo z → x IsRelatedTo z -x ⟹*⟪ x⟹y ⟫ yz = x ⟹*⟨ ⟨ x⟹y ⟩ ⟩ yz +_∎ : ∀ M → M ⟹* M +M ∎ = ⟨⟩ \end{code} -Example evaluation. +## Example reductions \begin{code} example₀ : not · true ⟹* false example₀ = - begin not · true - ⟹*⟪ β⇒ value-true ⟫ + ⟹⟨ β⇒ value-true ⟩ if true then false else true - ⟹*⟪ β𝔹₁ ⟫ + ⟹⟨ β𝔹₀ ⟩ false ∎ -example₁ : I² · I · (not · false) ⟹* true +example₁ : two · not · true ⟹* 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 ⟫ + 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 @@ -207,9 +182,9 @@ data _⊢_∶_ : Context → Term → Type → Set where Γ ⊢ L ∶ A ⇒ B → Γ ⊢ M ∶ A → Γ ⊢ L · M ∶ B - 𝔹-I₁ : ∀ {Γ} → + 𝔹-I₀ : ∀ {Γ} → Γ ⊢ true ∶ 𝔹 - 𝔹-I₂ : ∀ {Γ} → + 𝔹-I₁ : ∀ {Γ} → Γ ⊢ false ∶ 𝔹 𝔹-E : ∀ {Γ L M N A} → Γ ⊢ L ∶ 𝔹 → @@ -217,3 +192,45 @@ data _⊢_∶_ : Context → Term → Type → Set where Γ ⊢ N ∶ A → Γ ⊢ if L then M else N ∶ A \end{code} + +## Example type derivations + +\begin{code} +example₂ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹 +example₂ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₁ 𝔹-I₀) + +example₃ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 +example₃ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl)))) +\end{code} + +Construction of a type derivation is best done interactively. +We start with the declaration: + + `example₂ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` + `example₂ = ?` + +Typing control-L causes Agda to create a hole and tell us its expected type. + + `example₂ = { }0` + `?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` + +Now we fill in the hole, observing that the outermost term in `not` in a `λ`, +which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which +we again specify with a hole. + + `example₂ = ⇒-I { }0` + `?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹` + +Again we fill in the hole, observing that the outermost term is now +`if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes +three arguments, which we again specify with holes. + + `example₂ = ⇒-I (𝔹-E { }0 { }1 { }2)` + `?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ 𝔹` + `?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹` + `?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹` + +Filling in the three holes gives the derivation above. + + +