From 74427956f3c4309424287aefecd7b2c58c478eda Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 27 Apr 2018 16:13:51 -0300 Subject: [PATCH] failed attempt at string ids --- src/Typed.lagda | 123 ++++-- src/extra/Typed-backup.lagda | 280 ++++++------- src/extra/Typed-string.lagda | 788 +++++++++++++++++++++++++++++++++++ 3 files changed, 1008 insertions(+), 183 deletions(-) create mode 100644 src/extra/Typed-string.lagda diff --git a/src/Typed.lagda b/src/Typed.lagda index e201ed2c..37b2cf80 100644 --- a/src/Typed.lagda +++ b/src/Typed.lagda @@ -15,15 +15,45 @@ module Typed where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_) open import Data.Empty using (⊥; ⊥-elim) -open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter) -open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_) +open import Data.List using (List; []; _∷_; _++_; map; foldr; filter) +open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_) open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n) +open import Data.String using (String) open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Function using (_∘_) open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary.Negation using (¬?) open import Collections + +import Data.Nat as Nat +import Data.String as String + +pattern [_] x = x ∷ [] +pattern [_,_] x y = x ∷ y ∷ [] +pattern [_,_,_] x y z = x ∷ y ∷ z ∷ [] +\end{code} + + +## Identifiers + +\begin{code} +data Id : Set where + id : String → ℕ → Id + +_≟_ : ∀ (x y : Id) → Dec (x ≡ y) +id s m ≟ id t n with s String.≟ t | m Nat.≟ n +... | yes refl | yes refl = yes refl +... | yes refl | no m≢n = no (λ {refl → m≢n refl}) +... | no s≢t | _ = no (λ {refl → s≢t refl}) + +{- +_≠_ : ∀ (x y : Id) → x ≢ y +x ≠ y with x ≟ y +... | no x≢y = x≢y +... | yes _ = impossible + where postulate impossible : _ +-} \end{code} @@ -40,9 +70,6 @@ infix 7 `suc_ `pred_ `Y_ infixl 8 _·_ infix 9 `_ -Id : Set -Id = ℕ - data Type : Set where `ℕ : Type _⇒_ : Type → Type → Type @@ -122,11 +149,11 @@ data _⊢_⦂_ : Env → Term → Type → Set where \begin{code} m n s z : Id -p = 0 -m = 1 -n = 2 -s = 3 -z = 4 +p = id "p" 0 -- 0 +m = id "m" 0 -- 1 +n = id "n" 0 -- 2 +s = id "s" 0 -- 3 +z = id "z" 0 -- 4 s≢z : s ≢ z s≢z () @@ -281,15 +308,35 @@ free (`Y M) = free M ### Fresh identifier \begin{code} -fresh : List Id → Id -fresh = foldr _⊔_ 0 ∘ map suc +bump : String → Id → ℕ +bump s (id t n) with s String.≟ t +... | yes refl = suc n +... | no _ = 0 -⊔-lemma : ∀ {w xs} → w ∈ xs → suc w ≤ fresh xs -⊔-lemma {_} {_ ∷ xs} here = m≤m⊔n _ (fresh xs) -⊔-lemma {_} {_ ∷ xs} (there x∈) = ≤-trans (⊔-lemma x∈) (n≤m⊔n _ (fresh xs)) +next : String → List Id → ℕ +next s = foldr _⊔_ 0 ∘ map (bump s) -fresh-lemma : ∀ {x xs} → x ∈ xs → x ≢ fresh xs -fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈) +⊔-lemma : ∀ {s w xs} → w ∈ xs → bump s w ≤ next s xs +⊔-lemma {s} {_} {_ ∷ xs} here = m≤m⊔n _ (next s xs) +⊔-lemma {s} {_} {_ ∷ xs} (there x∈) = ≤-trans (⊔-lemma x∈) (n≤m⊔n _ (next s xs)) + +fresh : Id → List Id → Id +fresh (id s _) xs = id s (next s xs) + +fresh-lemma : ∀ {w x xs} → w ∈ xs → w ≢ fresh x xs +fresh-lemma {w @ (id t n)} {x @ (id s _)} {xs} w∈ w≢fr = {! (⊔-lemma {s} {w} {xs} w∈)!} -- with s String.≟ t +{- +... | yes refl = {! (⊔-lemma {s} {w} {xs} w∈)!} +... | no s≢t = {!!} + + +with s String.≟ t | fresh x xs +... | yes refl | fr = {! (⊔-lemma {s} {w} {xs} w∈)!} +... | no s≢t | _ = s≢t refl + + +next-lemma : ∀ {x xs} → x ∈ xs → x ≢ next xs +next-lemma x∈ refl = 1+n≰n (⊔-lemma x∈) \end{code} ### Identifier maps @@ -326,6 +373,23 @@ _[_:=_] : Term → Id → Term → Term N [ x := M ] = subst (free M ++ (free N \\ x)) (∅ , x ↦ M) N \end{code} +### Testing substitution + +\begin{code} +_ : (` s · ` s · ` z) [ z := `zero ] ≡ (` s · ` s · `zero) +_ = refl + +_ : (` s · ` s · ` z) [ s := (`λ m ⇒ `suc ` m) ] [ z := `zero ] + ≡ ((`λ p ⇒ `suc ` p) · (`λ p ⇒ `suc ` p) · `zero) +_ = refl + +_ : (`λ m ⇒ ` m · ` n) [ n := ` m ] ≡ (`λ n ⇒ ` n · ` m) +_ = refl + +_ : subst [ m , n ] (∅ , m ↦ ` n , n ↦ ` m) (` m · ` n) ≡ (` n · ` m) +_ = refl +\end{code} + ## Values @@ -705,19 +769,20 @@ preservation : ∀ {Γ M N A} → Γ ⊢ N ⦂ A preservation (Ax ⊢x) () preservation (⊢λ ⊢N) () -preservation (⊢L · ⊢M) (ξ-·₁ L⟶L′) = preservation ⊢L L⟶L′ · ⊢M -preservation (⊢V · ⊢M) (ξ-·₂ _ M⟶M′) = ⊢V · preservation ⊢M M⟶M′ -preservation ((⊢λ ⊢N) · ⊢W) (β-⇒ _) = ⊢substitution ⊢N ⊢W +preservation (⊢L · ⊢M) (ξ-·₁ L⟶) = preservation ⊢L L⟶ · ⊢M +preservation (⊢V · ⊢M) (ξ-·₂ _ M⟶) = ⊢V · preservation ⊢M M⟶ +preservation ((⊢λ ⊢N) · ⊢W) (β-⇒ _) = ⊢substitution ⊢N ⊢W preservation (⊢zero) () -preservation (⊢suc ⊢M) (ξ-suc M⟶M′) = ⊢suc (preservation ⊢M M⟶M′) -preservation (⊢pred ⊢M) (ξ-pred M⟶M′) = ⊢pred (preservation ⊢M M⟶M′) -preservation (⊢pred ⊢zero) (β-pred-zero) = ⊢zero -preservation (⊢pred (⊢suc ⊢M)) (β-pred-suc _) = ⊢M -preservation (⊢if0 ⊢L ⊢M ⊢N) (ξ-if0 L⟶L′) = ⊢if0 (preservation ⊢L L⟶L′) ⊢M ⊢N -preservation (⊢if0 ⊢zero ⊢M ⊢N) β-if0-zero = ⊢M -preservation (⊢if0 (⊢suc ⊢V) ⊢M ⊢N) (β-if0-suc _) = ⊢N -preservation (⊢Y ⊢M) (ξ-Y M⟶M′) = ⊢Y (preservation ⊢M M⟶M′) -preservation (⊢Y (⊢λ ⊢N)) (β-Y _ refl) = ⊢substitution ⊢N (⊢Y (⊢λ ⊢N)) +preservation (⊢suc ⊢M) (ξ-suc M⟶) = ⊢suc (preservation ⊢M M⟶) +preservation (⊢pred ⊢M) (ξ-pred M⟶) = ⊢pred (preservation ⊢M M⟶) +preservation (⊢pred ⊢zero) (β-pred-zero) = ⊢zero +preservation (⊢pred (⊢suc ⊢M)) (β-pred-suc _) = ⊢M +preservation (⊢if0 ⊢L ⊢M ⊢N) (ξ-if0 L⟶) = ⊢if0 (preservation ⊢L L⟶) ⊢M ⊢N +preservation (⊢if0 ⊢zero ⊢M ⊢N) β-if0-zero = ⊢M +preservation (⊢if0 (⊢suc ⊢V) ⊢M ⊢N) (β-if0-suc _) = ⊢N +preservation (⊢Y ⊢M) (ξ-Y M⟶) = ⊢Y (preservation ⊢M M⟶) +preservation (⊢Y (⊢λ ⊢N)) (β-Y _ refl) = ⊢substitution ⊢N (⊢Y (⊢λ ⊢N)) +-} \end{code} diff --git a/src/extra/Typed-backup.lagda b/src/extra/Typed-backup.lagda index eb085e72..3e2002a8 100644 --- a/src/extra/Typed-backup.lagda +++ b/src/extra/Typed-backup.lagda @@ -15,33 +15,30 @@ module Typed where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_) open import Data.Empty using (⊥; ⊥-elim) -open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter) -open import Data.List.Any using (Any; here; there) +open import Data.List using (List; []; _∷_; _++_; map; foldr; filter) open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_) open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n) -open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) - renaming (_,_ to ⟨_,_⟩) +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Data.Unit using (⊤; tt) open import Function using (_∘_) -open import Function.Equality using (≡-setoid) -open import Function.Equivalence using (_⇔_; equivalence) open import Relation.Nullary using (¬_; Dec; yes; no) -open import Relation.Nullary.Negation using (contraposition; ¬?) -open import Relation.Nullary.Product using (_×-dec_) -open import Collections using (_↔_) +open import Relation.Nullary.Negation using (¬?) +open import Collections + +pattern [_] x = x ∷ [] +pattern [_,_] x y = x ∷ y ∷ [] +pattern [_,_,_] x y z = x ∷ y ∷ z ∷ [] \end{code} ## Syntax \begin{code} -infixr 5 _⟹_ +infixr 5 _⇒_ infixl 5 _,_⦂_ infix 4 _∋_⦂_ infix 4 _⊢_⦂_ infix 5 `λ_⇒_ -infix 5 `λ_ infixl 6 `if0_then_else_ infix 7 `suc_ `pred_ `Y_ infixl 8 _·_ @@ -52,7 +49,7 @@ Id = ℕ data Type : Set where `ℕ : Type - _⟹_ : Type → Type → Type + _⇒_ : Type → Type → Type data Env : Set where ε : Env @@ -82,45 +79,45 @@ data _∋_⦂_ : Env → Id → Type → Set where data _⊢_⦂_ : Env → Term → Type → Set where - `_ : ∀ {Γ A x} + Ax : ∀ {Γ A x} → Γ ∋ x ⦂ A --------------------- → Γ ⊢ ` x ⦂ A - `λ_ : ∀ {Γ x N A B} + ⊢λ : ∀ {Γ x N A B} → Γ , x ⦂ A ⊢ N ⦂ B ------------------------ - → Γ ⊢ (`λ x ⇒ N) ⦂ A ⟹ B + → Γ ⊢ (`λ x ⇒ N) ⦂ A ⇒ B _·_ : ∀ {Γ L M A B} - → Γ ⊢ L ⦂ A ⟹ B + → Γ ⊢ L ⦂ A ⇒ B → Γ ⊢ M ⦂ A -------------- → Γ ⊢ L · M ⦂ B - `zero : ∀ {Γ} + ⊢zero : ∀ {Γ} -------------- → Γ ⊢ `zero ⦂ `ℕ - `suc_ : ∀ {Γ M} + ⊢suc : ∀ {Γ M} → Γ ⊢ M ⦂ `ℕ --------------- → Γ ⊢ `suc M ⦂ `ℕ - `pred_ : ∀ {Γ M} + ⊢pred : ∀ {Γ M} → Γ ⊢ M ⦂ `ℕ ---------------- → Γ ⊢ `pred M ⦂ `ℕ - `if0 : ∀ {Γ L M N A} + ⊢if0 : ∀ {Γ L M N A} → Γ ⊢ L ⦂ `ℕ → Γ ⊢ M ⦂ A → Γ ⊢ N ⦂ A ---------------------------- → Γ ⊢ `if0 L then M else N ⦂ A - `Y_ : ∀ {Γ M A} - → Γ ⊢ M ⦂ A ⟹ A + ⊢Y : ∀ {Γ M A} + → Γ ⊢ M ⦂ A ⇒ A --------------- → Γ ⊢ `Y M ⦂ A \end{code} @@ -163,13 +160,13 @@ two : Term two = `suc `suc `zero ⊢two : ε ⊢ two ⦂ `ℕ -⊢two = `suc `suc `zero +⊢two = (⊢suc (⊢suc ⊢zero)) plus : Term plus = `Y (`λ p ⇒ `λ m ⇒ `λ n ⇒ `if0 ` m then ` n else ` p · (`pred ` m) · ` n) -⊢plus : ε ⊢ plus ⦂ `ℕ ⟹ `ℕ ⟹ `ℕ -⊢plus = `Y (`λ `λ `λ `if0 (` ⊢m) (` ⊢n) (` ⊢p · (`pred ` ⊢m) · ` ⊢n)) +⊢plus : ε ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ +⊢plus = (⊢Y (⊢λ (⊢λ (⊢λ (⊢if0 (Ax ⊢m) (Ax ⊢n) (Ax ⊢p · (⊢pred (Ax ⊢m)) · Ax ⊢n)))))) where ⊢p = S p≢n (S p≢m Z) ⊢m = S m≢n Z @@ -182,13 +179,13 @@ four = plus · two · two ⊢four = ⊢plus · ⊢two · ⊢two Ch : Type -Ch = (`ℕ ⟹ `ℕ) ⟹ `ℕ ⟹ `ℕ +Ch = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ twoCh : Term twoCh = `λ s ⇒ `λ z ⇒ (` s · (` s · ` z)) ⊢twoCh : ε ⊢ twoCh ⦂ Ch -⊢twoCh = `λ `λ ` ⊢s · (` ⊢s · ` ⊢z) +⊢twoCh = (⊢λ (⊢λ (Ax ⊢s · (Ax ⊢s · Ax ⊢z)))) where ⊢s = S s≢z Z ⊢z = Z @@ -196,8 +193,8 @@ twoCh = `λ s ⇒ `λ z ⇒ (` s · (` s · ` z)) plusCh : Term plusCh = `λ m ⇒ `λ n ⇒ `λ s ⇒ `λ z ⇒ ` m · ` s · (` n · ` s · ` z) -⊢plusCh : ε ⊢ plusCh ⦂ Ch ⟹ Ch ⟹ Ch -⊢plusCh = `λ `λ `λ `λ ` ⊢m · ` ⊢s · (` ⊢n · ` ⊢s · ` ⊢z) +⊢plusCh : ε ⊢ plusCh ⦂ Ch ⇒ Ch ⇒ Ch +⊢plusCh = (⊢λ (⊢λ (⊢λ (⊢λ (Ax ⊢m · Ax ⊢s · (Ax ⊢n · Ax ⊢s · Ax ⊢z)))))) where ⊢m = S m≢z (S m≢s (S m≢n Z)) ⊢n = S n≢z (S n≢s Z) @@ -207,8 +204,8 @@ plusCh = `λ m ⇒ `λ n ⇒ `λ s ⇒ `λ z ⇒ ` m · ` s · (` n · ` s · ` fromCh : Term fromCh = `λ m ⇒ ` m · (`λ s ⇒ `suc ` s) · `zero -⊢fromCh : ε ⊢ fromCh ⦂ Ch ⟹ `ℕ -⊢fromCh = `λ ` ⊢m · (`λ `suc ` ⊢s) · `zero +⊢fromCh : ε ⊢ fromCh ⦂ Ch ⇒ `ℕ +⊢fromCh = (⊢λ (Ax ⊢m · (⊢λ (⊢suc (Ax ⊢s))) · ⊢zero)) where ⊢m = Z ⊢s = Z @@ -221,63 +218,22 @@ fourCh = fromCh · (plusCh · twoCh · twoCh) \end{code} -# Denotational semantics - -\begin{code} -⟦_⟧ᵀ : Type → Set -⟦ `ℕ ⟧ᵀ = ℕ -⟦ A ⟹ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ - -⟦_⟧ᴱ : Env → Set -⟦ ε ⟧ᴱ = ⊤ -⟦ Γ , x ⦂ A ⟧ᴱ = ⟦ Γ ⟧ᴱ × ⟦ A ⟧ᵀ - -⟦_⟧ⱽ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ -⟦ Z ⟧ⱽ ⟨ ρ , v ⟩ = v -⟦ S _ x ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ x ⟧ⱽ ρ - -⟦_⟧ : ∀ {Γ M A} → Γ ⊢ M ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ -⟦ ` x ⟧ ρ = ⟦ x ⟧ⱽ ρ -⟦ `λ ⊢N ⟧ ρ = λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ } -⟦ ⊢L · ⊢M ⟧ ρ = (⟦ ⊢L ⟧ ρ) (⟦ ⊢M ⟧ ρ) -⟦ `zero ⟧ ρ = zero -⟦ `suc ⊢M ⟧ ρ = suc (⟦ ⊢M ⟧ ρ) -⟦ `pred ⊢M ⟧ ρ = pred (⟦ ⊢M ⟧ ρ) - where - pred : ℕ → ℕ - pred zero = zero - pred (suc n) = n -⟦ `if0 ⊢L ⊢M ⊢N ⟧ ρ = if0 ⟦ ⊢L ⟧ ρ then ⟦ ⊢M ⟧ ρ else ⟦ ⊢N ⟧ ρ - where - if0_then_else_ : ∀ {A} → ℕ → A → A → A - if0 zero then m else n = m - if0 suc _ then m else n = n -⟦ `Y ⊢M ⟧ ρ = {!!} - --- _ : ⟦ ⊢four ⟧ tt ≡ 4 --- _ = refl - -_ : ⟦ ⊢fourCh ⟧ tt ≡ 4 -_ = refl -\end{code} - - ## Erasure \begin{code} lookup : ∀ {Γ x A} → Γ ∋ x ⦂ A → Id -lookup {Γ , x ⦂ A} Z = x -lookup {Γ , x ⦂ A} (S _ k) = lookup {Γ} k +lookup {Γ , x ⦂ A} Z = x +lookup {Γ , x ⦂ A} (S _ ⊢w) = lookup {Γ} ⊢w erase : ∀ {Γ M A} → Γ ⊢ M ⦂ A → Term -erase (` k) = ` lookup k -erase (`λ_ {x = x} ⊢N) = `λ x ⇒ erase ⊢N +erase (Ax ⊢w) = ` lookup ⊢w +erase (⊢λ {x = x} ⊢N) = `λ x ⇒ erase ⊢N erase (⊢L · ⊢M) = erase ⊢L · erase ⊢M -erase (`zero) = `zero -erase (`suc ⊢M) = `suc (erase ⊢M) -erase (`pred ⊢M) = `pred (erase ⊢M) -erase (`if0 ⊢L ⊢M ⊢N) = `if0 (erase ⊢L) then (erase ⊢M) else (erase ⊢N) -erase (`Y ⊢M) = `Y (erase ⊢M) +erase (⊢zero) = `zero +erase (⊢suc ⊢M) = `suc (erase ⊢M) +erase (⊢pred ⊢M) = `pred (erase ⊢M) +erase (⊢if0 ⊢L ⊢M ⊢N) = `if0 (erase ⊢L) then (erase ⊢M) else (erase ⊢N) +erase (⊢Y ⊢M) = `Y (erase ⊢M) \end{code} ### Properties of erasure @@ -288,19 +244,19 @@ cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {s t u v x y} → cong₃ f refl refl refl = refl lookup-lemma : ∀ {Γ x A} → (⊢x : Γ ∋ x ⦂ A) → lookup ⊢x ≡ x -lookup-lemma Z = refl -lookup-lemma (S _ k) = lookup-lemma k +lookup-lemma Z = refl +lookup-lemma (S _ ⊢w) = lookup-lemma ⊢w erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M ⦂ A) → erase ⊢M ≡ M -erase-lemma (` ⊢x) = cong `_ (lookup-lemma ⊢x) -erase-lemma (`λ_ {x = x} ⊢N) = cong (`λ x ⇒_) (erase-lemma ⊢N) -erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M) -erase-lemma (`zero) = refl -erase-lemma (`suc ⊢M) = cong `suc_ (erase-lemma ⊢M) -erase-lemma (`pred ⊢M) = cong `pred_ (erase-lemma ⊢M) -erase-lemma (`if0 ⊢L ⊢M ⊢N) = cong₃ `if0_then_else_ - (erase-lemma ⊢L) (erase-lemma ⊢M) (erase-lemma ⊢N) -erase-lemma (`Y ⊢M) = cong `Y_ (erase-lemma ⊢M) +erase-lemma (Ax ⊢x) = cong `_ (lookup-lemma ⊢x) +erase-lemma (⊢λ {x = x} ⊢N) = cong (`λ x ⇒_) (erase-lemma ⊢N) +erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M) +erase-lemma (⊢zero) = refl +erase-lemma (⊢suc ⊢M) = cong `suc_ (erase-lemma ⊢M) +erase-lemma (⊢pred ⊢M) = cong `pred_ (erase-lemma ⊢M) +erase-lemma (⊢if0 ⊢L ⊢M ⊢N) = cong₃ `if0_then_else_ + (erase-lemma ⊢L) (erase-lemma ⊢M) (erase-lemma ⊢N) +erase-lemma (⊢Y ⊢M) = cong `Y_ (erase-lemma ⊢M) \end{code} @@ -374,6 +330,23 @@ _[_:=_] : Term → Id → Term → Term N [ x := M ] = subst (free M ++ (free N \\ x)) (∅ , x ↦ M) N \end{code} +### Testing substitution + +\begin{code} +_ : (` s · ` s · ` z) [ z := `zero ] ≡ (` s · ` s · `zero) +_ = refl + +_ : (` s · ` s · ` z) [ s := (`λ m ⇒ `suc ` m) ] [ z := `zero ] + ≡ ((`λ p ⇒ `suc ` p) · (`λ p ⇒ `suc ` p) · `zero) +_ = refl + +_ : (`λ m ⇒ ` m · ` n) [ n := ` m ] ≡ (`λ n ⇒ ` n · ` m) +_ = refl + +_ : subst [ m , n ] (∅ , m ↦ ` n , n ↦ ` m) (` m · ` n) ≡ (` n · ` m) +_ = refl +\end{code} + ## Values @@ -412,7 +385,7 @@ data _⟶_ : Term → Term → Set where ---------------- → V · M ⟶ V · M′ - β-⟹ : ∀ {x N V} + β-⇒ : ∀ {x N V} → Value V ------------------------------ → (`λ x ⇒ N) · V ⟶ N [ x := V ] @@ -503,7 +476,7 @@ data Canonical : Term → Type → Set where Fun : ∀ {x N A B} → ε , x ⦂ A ⊢ N ⦂ B ------------------------------ - → Canonical (`λ x ⇒ N) (A ⟹ B) + → Canonical (`λ x ⇒ N) (A ⇒ B) \end{code} ## Canonical forms lemma @@ -516,9 +489,9 @@ canonical : ∀ {V A} → Value V ------------- → Canonical V A -canonical `zero Zero = Zero -canonical (`suc ⊢V) (Suc VV) = Suc (canonical ⊢V VV) -canonical (`λ ⊢N) Fun = Fun ⊢N +canonical ⊢zero Zero = Zero +canonical (⊢suc ⊢V) (Suc VV) = Suc (canonical ⊢V VV) +canonical (⊢λ ⊢N) Fun = Fun ⊢N \end{code} Every canonical form has a type and a value. @@ -528,9 +501,9 @@ type : ∀ {V A} → Canonical V A ------------- → ε ⊢ V ⦂ A -type Zero = `zero -type (Suc CV) = `suc (type CV) -type (Fun ⊢N) = `λ ⊢N +type Zero = ⊢zero +type (Suc CV) = ⊢suc (type CV) +type (Fun ⊢N) = ⊢λ ⊢N value : ∀ {V A} → Canonical V A @@ -555,26 +528,26 @@ data Progress (M : Term) (A : Type) : Set where → Progress M A progress : ∀ {M A} → ε ⊢ M ⦂ A → Progress M A -progress (` ()) -progress (`λ ⊢N) = done (Fun ⊢N) +progress (Ax ()) +progress (⊢λ ⊢N) = done (Fun ⊢N) progress (⊢L · ⊢M) with progress ⊢L ... | step L⟶L′ = step (ξ-·₁ L⟶L′) ... | done (Fun _) with progress ⊢M ... | step M⟶M′ = step (ξ-·₂ Fun M⟶M′) -... | done CM = step (β-⟹ (value CM)) -progress `zero = done Zero -progress (`suc ⊢M) with progress ⊢M +... | done CM = step (β-⇒ (value CM)) +progress ⊢zero = done Zero +progress (⊢suc ⊢M) with progress ⊢M ... | step M⟶M′ = step (ξ-suc M⟶M′) ... | done CM = done (Suc CM) -progress (`pred ⊢M) with progress ⊢M +progress (⊢pred ⊢M) with progress ⊢M ... | step M⟶M′ = step (ξ-pred M⟶M′) ... | done Zero = step β-pred-zero ... | done (Suc CM) = step (β-pred-suc (value CM)) -progress (`if0 ⊢L ⊢M ⊢N) with progress ⊢L +progress (⊢if0 ⊢L ⊢M ⊢N) with progress ⊢L ... | step L⟶L′ = step (ξ-if0 L⟶L′) ... | done Zero = step β-if0-zero ... | done (Suc CM) = step (β-if0-suc (value CM)) -progress (`Y ⊢M) with progress ⊢M +progress (⊢Y ⊢M) with progress ⊢M ... | step M⟶M′ = step (ξ-Y M⟶M′) ... | done (Fun _) = step (β-Y Fun refl) \end{code} @@ -594,23 +567,23 @@ dom-lemma Z = here dom-lemma (S x≢y ⊢y) = there (dom-lemma ⊢y) free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ -free-lemma (` ⊢x) w∈ with w∈ -... | here = dom-lemma ⊢x -... | there () -free-lemma {Γ} (`λ_ {N = N} ⊢N) = ∷-to-\\ (free-lemma ⊢N) +free-lemma (Ax ⊢x) w∈ with w∈ +... | here = dom-lemma ⊢x +... | there () +free-lemma {Γ} (⊢λ {N = N} ⊢N) = ∷-to-\\ (free-lemma ⊢N) free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈ ... | inj₁ ∈L = free-lemma ⊢L ∈L ... | inj₂ ∈M = free-lemma ⊢M ∈M -free-lemma `zero () -free-lemma (`suc ⊢M) w∈ = free-lemma ⊢M w∈ -free-lemma (`pred ⊢M) w∈ = free-lemma ⊢M w∈ -free-lemma (`if0 ⊢L ⊢M ⊢N) w∈ +free-lemma ⊢zero () +free-lemma (⊢suc ⊢M) w∈ = free-lemma ⊢M w∈ +free-lemma (⊢pred ⊢M) w∈ = free-lemma ⊢M w∈ +free-lemma (⊢if0 ⊢L ⊢M ⊢N) w∈ with ++-to-⊎ w∈ ... | inj₁ ∈L = free-lemma ⊢L ∈L ... | inj₂ ∈MN with ++-to-⊎ ∈MN ... | inj₁ ∈M = free-lemma ⊢M ∈M ... | inj₂ ∈N = free-lemma ⊢N ∈N -free-lemma (`Y ⊢M) w∈ = free-lemma ⊢M w∈ +free-lemma (⊢Y ⊢M) w∈ = free-lemma ⊢M w∈ \end{code} ### Renaming @@ -620,11 +593,11 @@ free-lemma (`Y ⊢M) w∈ = free-lemma ⊢M w∈ → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) -------------------------------------------------- → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) -⊢rename ⊢σ ⊆xs (` ⊢x) = ` ⊢σ ∈xs ⊢x +⊢rename ⊢σ ⊆xs (Ax ⊢x) = Ax (⊢σ ∈xs ⊢x) where ∈xs = ⊆xs here -⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (`λ_ {x = x} {N = N} {A = A} ⊢N) - = `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) +⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (⊢λ {x = x} {N = N} {A = A} ⊢N) + = ⊢λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) where Γ′ = Γ , x ⦂ A Δ′ = Δ , x ⦂ A @@ -642,16 +615,16 @@ free-lemma (`Y ⊢M) w∈ = free-lemma ⊢M w∈ where L⊆ = trans-⊆ ⊆-++₁ ⊆xs M⊆ = trans-⊆ ⊆-++₂ ⊆xs -⊢rename ⊢σ ⊆xs (`zero) = `zero -⊢rename ⊢σ ⊆xs (`suc ⊢M) = `suc (⊢rename ⊢σ ⊆xs ⊢M) -⊢rename ⊢σ ⊆xs (`pred ⊢M) = `pred (⊢rename ⊢σ ⊆xs ⊢M) -⊢rename ⊢σ ⊆xs (`if0 {L = L} ⊢L ⊢M ⊢N) - = `if0 (⊢rename ⊢σ L⊆ ⊢L) (⊢rename ⊢σ M⊆ ⊢M) (⊢rename ⊢σ N⊆ ⊢N) +⊢rename ⊢σ ⊆xs (⊢zero) = ⊢zero +⊢rename ⊢σ ⊆xs (⊢suc ⊢M) = ⊢suc (⊢rename ⊢σ ⊆xs ⊢M) +⊢rename ⊢σ ⊆xs (⊢pred ⊢M) = ⊢pred (⊢rename ⊢σ ⊆xs ⊢M) +⊢rename ⊢σ ⊆xs (⊢if0 {L = L} ⊢L ⊢M ⊢N) + = ⊢if0 (⊢rename ⊢σ L⊆ ⊢L) (⊢rename ⊢σ M⊆ ⊢M) (⊢rename ⊢σ N⊆ ⊢N) where L⊆ = trans-⊆ ⊆-++₁ ⊆xs M⊆ = trans-⊆ ⊆-++₁ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) N⊆ = trans-⊆ ⊆-++₂ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) -⊢rename ⊢σ ⊆xs (`Y ⊢M) = `Y (⊢rename ⊢σ ⊆xs ⊢M) +⊢rename ⊢σ ⊆xs (⊢Y ⊢M) = ⊢Y (⊢rename ⊢σ ⊆xs ⊢M) \end{code} @@ -664,10 +637,10 @@ free-lemma (`Y ⊢M) w∈ = free-lemma ⊢M w∈ → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) ------------------------------------------------------------- → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ A) -⊢subst Σ ⊢ρ ⊆xs (` ⊢x) +⊢subst Σ ⊢ρ ⊆xs (Ax ⊢x) = ⊢ρ (⊆xs here) ⊢x -⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (`λ_ {x = x} {N = N} {A = A} ⊢N) - = `λ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N) +⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (⊢λ {x = x} {N = N} {A = A} ⊢N) + = ⊢λ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N) where y = fresh ys Γ′ = Γ , x ⦂ A @@ -689,7 +662,7 @@ free-lemma (`Y ⊢M) w∈ = free-lemma ⊢M w∈ ⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C ⊢ρ′ {w} _ Z with w ≟ x - ... | yes _ = ` Z + ... | yes _ = Ax Z ... | no w≢ = ⊥-elim (w≢ refl) ⊢ρ′ {w} w∈′ (S w≢ ⊢w) with w ≟ x ... | yes refl = ⊥-elim (w≢ refl) @@ -702,16 +675,16 @@ free-lemma (`Y ⊢M) w∈ = free-lemma ⊢M w∈ where L⊆ = trans-⊆ ⊆-++₁ ⊆xs M⊆ = trans-⊆ ⊆-++₂ ⊆xs -⊢subst Σ ⊢ρ ⊆xs `zero = `zero -⊢subst Σ ⊢ρ ⊆xs (`suc ⊢M) = `suc (⊢subst Σ ⊢ρ ⊆xs ⊢M) -⊢subst Σ ⊢ρ ⊆xs (`pred ⊢M) = `pred (⊢subst Σ ⊢ρ ⊆xs ⊢M) -⊢subst Σ ⊢ρ ⊆xs (`if0 {L = L} ⊢L ⊢M ⊢N) - = `if0 (⊢subst Σ ⊢ρ L⊆ ⊢L) (⊢subst Σ ⊢ρ M⊆ ⊢M) (⊢subst Σ ⊢ρ N⊆ ⊢N) +⊢subst Σ ⊢ρ ⊆xs ⊢zero = ⊢zero +⊢subst Σ ⊢ρ ⊆xs (⊢suc ⊢M) = ⊢suc (⊢subst Σ ⊢ρ ⊆xs ⊢M) +⊢subst Σ ⊢ρ ⊆xs (⊢pred ⊢M) = ⊢pred (⊢subst Σ ⊢ρ ⊆xs ⊢M) +⊢subst Σ ⊢ρ ⊆xs (⊢if0 {L = L} ⊢L ⊢M ⊢N) + = ⊢if0 (⊢subst Σ ⊢ρ L⊆ ⊢L) (⊢subst Σ ⊢ρ M⊆ ⊢M) (⊢subst Σ ⊢ρ N⊆ ⊢N) where L⊆ = trans-⊆ ⊆-++₁ ⊆xs M⊆ = trans-⊆ ⊆-++₁ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) N⊆ = trans-⊆ ⊆-++₂ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) -⊢subst Σ ⊢ρ ⊆xs (`Y ⊢M) = `Y (⊢subst Σ ⊢ρ ⊆xs ⊢M) +⊢subst Σ ⊢ρ ⊆xs (⊢Y ⊢M) = ⊢Y (⊢subst Σ ⊢ρ ⊆xs ⊢M) ⊢substitution : ∀ {Γ x A N B M} → Γ , x ⦂ A ⊢ N ⦂ B → @@ -737,7 +710,7 @@ free-lemma (`Y ⊢M) w∈ = free-lemma ⊢M w∈ ... | no w≢ = ⊥-elim (w≢ refl) ⊢ρ {w} w∈ (S w≢ ⊢w) with w ≟ x ... | yes refl = ⊥-elim (w≢ refl) - ... | no _ = ` ⊢w + ... | no _ = Ax ⊢w ⊆xs : free N ⊆ xs ⊆xs x∈ = x∈ @@ -751,22 +724,21 @@ preservation : ∀ {Γ M N A} → M ⟶ N --------- → Γ ⊢ N ⦂ A -preservation (` ⊢x) () -preservation (`λ ⊢N) () -preservation (⊢L · ⊢M) (ξ-·₁ L⟶L′) = preservation ⊢L L⟶L′ · ⊢M -preservation (⊢V · ⊢M) (ξ-·₂ _ M⟶M′) = ⊢V · preservation ⊢M M⟶M′ -preservation ((`λ ⊢N) · ⊢W) (β-⟹ _) = ⊢substitution ⊢N ⊢W -preservation (`zero) () -preservation (`suc ⊢M) (ξ-suc M⟶M′) = `suc (preservation ⊢M M⟶M′) -preservation (`pred ⊢M) (ξ-pred M⟶M′) = `pred (preservation ⊢M M⟶M′) -preservation (`pred `zero) (β-pred-zero) = `zero -preservation (`pred (`suc ⊢M)) (β-pred-suc _) = ⊢M -preservation (`if0 ⊢L ⊢M ⊢N) (ξ-if0 L⟶L′) = `if0 (preservation ⊢L L⟶L′) ⊢M ⊢N -preservation (`if0 `zero ⊢M ⊢N) β-if0-zero = ⊢M -preservation (`if0 (`suc ⊢V) ⊢M ⊢N) (β-if0-suc _) = ⊢N -preservation (`Y ⊢M) (ξ-Y M⟶M′) = `Y (preservation ⊢M M⟶M′) -preservation (`Y (`λ ⊢N)) (β-Y _ refl) = ⊢substitution ⊢N (`Y (`λ ⊢N)) +preservation (Ax ⊢x) () +preservation (⊢λ ⊢N) () +preservation (⊢L · ⊢M) (ξ-·₁ L⟶) = preservation ⊢L L⟶ · ⊢M +preservation (⊢V · ⊢M) (ξ-·₂ _ M⟶) = ⊢V · preservation ⊢M M⟶ +preservation ((⊢λ ⊢N) · ⊢W) (β-⇒ _) = ⊢substitution ⊢N ⊢W +preservation (⊢zero) () +preservation (⊢suc ⊢M) (ξ-suc M⟶) = ⊢suc (preservation ⊢M M⟶) +preservation (⊢pred ⊢M) (ξ-pred M⟶) = ⊢pred (preservation ⊢M M⟶) +preservation (⊢pred ⊢zero) (β-pred-zero) = ⊢zero +preservation (⊢pred (⊢suc ⊢M)) (β-pred-suc _) = ⊢M +preservation (⊢if0 ⊢L ⊢M ⊢N) (ξ-if0 L⟶) = ⊢if0 (preservation ⊢L L⟶) ⊢M ⊢N +preservation (⊢if0 ⊢zero ⊢M ⊢N) β-if0-zero = ⊢M +preservation (⊢if0 (⊢suc ⊢V) ⊢M ⊢N) (β-if0-suc _) = ⊢N +preservation (⊢Y ⊢M) (ξ-Y M⟶) = ⊢Y (preservation ⊢M M⟶) +preservation (⊢Y (⊢λ ⊢N)) (β-Y _ refl) = ⊢substitution ⊢N (⊢Y (⊢λ ⊢N)) \end{code} - diff --git a/src/extra/Typed-string.lagda b/src/extra/Typed-string.lagda new file mode 100644 index 00000000..37b2cf80 --- /dev/null +++ b/src/extra/Typed-string.lagda @@ -0,0 +1,788 @@ +--- +title : "Typed: Typed Lambda term representation" +layout : page +permalink : /Typed +--- + + +## Imports + +\begin{code} +module Typed where +\end{code} + +\begin{code} +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.List using (List; []; _∷_; _++_; map; foldr; filter) +open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_) +open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n) +open import Data.String using (String) +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Function using (_∘_) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Nullary.Negation using (¬?) +open import Collections + +import Data.Nat as Nat +import Data.String as String + +pattern [_] x = x ∷ [] +pattern [_,_] x y = x ∷ y ∷ [] +pattern [_,_,_] x y z = x ∷ y ∷ z ∷ [] +\end{code} + + +## Identifiers + +\begin{code} +data Id : Set where + id : String → ℕ → Id + +_≟_ : ∀ (x y : Id) → Dec (x ≡ y) +id s m ≟ id t n with s String.≟ t | m Nat.≟ n +... | yes refl | yes refl = yes refl +... | yes refl | no m≢n = no (λ {refl → m≢n refl}) +... | no s≢t | _ = no (λ {refl → s≢t refl}) + +{- +_≠_ : ∀ (x y : Id) → x ≢ y +x ≠ y with x ≟ y +... | no x≢y = x≢y +... | yes _ = impossible + where postulate impossible : _ +-} +\end{code} + + +## Syntax + +\begin{code} +infixr 5 _⇒_ +infixl 5 _,_⦂_ +infix 4 _∋_⦂_ +infix 4 _⊢_⦂_ +infix 5 `λ_⇒_ +infixl 6 `if0_then_else_ +infix 7 `suc_ `pred_ `Y_ +infixl 8 _·_ +infix 9 `_ + +data Type : Set where + `ℕ : Type + _⇒_ : Type → Type → Type + +data Env : Set where + ε : Env + _,_⦂_ : Env → Id → Type → Env + +data Term : Set where + `_ : Id → Term + `λ_⇒_ : Id → Term → Term + _·_ : Term → Term → Term + `zero : Term + `suc_ : Term → Term + `pred_ : Term → Term + `if0_then_else_ : Term → Term → Term → Term + `Y_ : Term → Term + +data _∋_⦂_ : Env → Id → Type → Set where + + Z : ∀ {Γ A x} + ----------------- + → Γ , x ⦂ A ∋ x ⦂ A + + S : ∀ {Γ A B x w} + → w ≢ x + → Γ ∋ w ⦂ B + ----------------- + → Γ , x ⦂ A ∋ w ⦂ B + +data _⊢_⦂_ : Env → Term → Type → Set where + + Ax : ∀ {Γ A x} + → Γ ∋ x ⦂ A + --------------------- + → Γ ⊢ ` x ⦂ A + + ⊢λ : ∀ {Γ x N A B} + → Γ , x ⦂ A ⊢ N ⦂ B + ------------------------ + → Γ ⊢ (`λ x ⇒ N) ⦂ A ⇒ B + + _·_ : ∀ {Γ L M A B} + → Γ ⊢ L ⦂ A ⇒ B + → Γ ⊢ M ⦂ A + -------------- + → Γ ⊢ L · M ⦂ B + + ⊢zero : ∀ {Γ} + -------------- + → Γ ⊢ `zero ⦂ `ℕ + + ⊢suc : ∀ {Γ M} + → Γ ⊢ M ⦂ `ℕ + --------------- + → Γ ⊢ `suc M ⦂ `ℕ + + ⊢pred : ∀ {Γ M} + → Γ ⊢ M ⦂ `ℕ + ---------------- + → Γ ⊢ `pred M ⦂ `ℕ + + ⊢if0 : ∀ {Γ L M N A} + → Γ ⊢ L ⦂ `ℕ + → Γ ⊢ M ⦂ A + → Γ ⊢ N ⦂ A + ---------------------------- + → Γ ⊢ `if0 L then M else N ⦂ A + + ⊢Y : ∀ {Γ M A} + → Γ ⊢ M ⦂ A ⇒ A + --------------- + → Γ ⊢ `Y M ⦂ A +\end{code} + +## Test examples + +\begin{code} +m n s z : Id +p = id "p" 0 -- 0 +m = id "m" 0 -- 1 +n = id "n" 0 -- 2 +s = id "s" 0 -- 3 +z = id "z" 0 -- 4 + +s≢z : s ≢ z +s≢z () + +n≢z : n ≢ z +n≢z () + +n≢s : n ≢ s +n≢s () + +m≢z : m ≢ z +m≢z () + +m≢s : m ≢ s +m≢s () + +m≢n : m ≢ n +m≢n () + +p≢n : p ≢ n +p≢n () + +p≢m : p ≢ m +p≢m () + +two : Term +two = `suc `suc `zero + +⊢two : ε ⊢ two ⦂ `ℕ +⊢two = (⊢suc (⊢suc ⊢zero)) + +plus : Term +plus = `Y (`λ p ⇒ `λ m ⇒ `λ n ⇒ `if0 ` m then ` n else ` p · (`pred ` m) · ` n) + +⊢plus : ε ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ +⊢plus = (⊢Y (⊢λ (⊢λ (⊢λ (⊢if0 (Ax ⊢m) (Ax ⊢n) (Ax ⊢p · (⊢pred (Ax ⊢m)) · Ax ⊢n)))))) + where + ⊢p = S p≢n (S p≢m Z) + ⊢m = S m≢n Z + ⊢n = Z + +four : Term +four = plus · two · two + +⊢four : ε ⊢ four ⦂ `ℕ +⊢four = ⊢plus · ⊢two · ⊢two + +Ch : Type +Ch = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ + +twoCh : Term +twoCh = `λ s ⇒ `λ z ⇒ (` s · (` s · ` z)) + +⊢twoCh : ε ⊢ twoCh ⦂ Ch +⊢twoCh = (⊢λ (⊢λ (Ax ⊢s · (Ax ⊢s · Ax ⊢z)))) + where + ⊢s = S s≢z Z + ⊢z = Z + +plusCh : Term +plusCh = `λ m ⇒ `λ n ⇒ `λ s ⇒ `λ z ⇒ ` m · ` s · (` n · ` s · ` z) + +⊢plusCh : ε ⊢ plusCh ⦂ Ch ⇒ Ch ⇒ Ch +⊢plusCh = (⊢λ (⊢λ (⊢λ (⊢λ (Ax ⊢m · Ax ⊢s · (Ax ⊢n · Ax ⊢s · Ax ⊢z)))))) + where + ⊢m = S m≢z (S m≢s (S m≢n Z)) + ⊢n = S n≢z (S n≢s Z) + ⊢s = S s≢z Z + ⊢z = Z + +fromCh : Term +fromCh = `λ m ⇒ ` m · (`λ s ⇒ `suc ` s) · `zero + +⊢fromCh : ε ⊢ fromCh ⦂ Ch ⇒ `ℕ +⊢fromCh = (⊢λ (Ax ⊢m · (⊢λ (⊢suc (Ax ⊢s))) · ⊢zero)) + where + ⊢m = Z + ⊢s = Z + +fourCh : Term +fourCh = fromCh · (plusCh · twoCh · twoCh) + +⊢fourCh : ε ⊢ fourCh ⦂ `ℕ +⊢fourCh = ⊢fromCh · (⊢plusCh · ⊢twoCh · ⊢twoCh) +\end{code} + + +## Erasure + +\begin{code} +lookup : ∀ {Γ x A} → Γ ∋ x ⦂ A → Id +lookup {Γ , x ⦂ A} Z = x +lookup {Γ , x ⦂ A} (S _ ⊢w) = lookup {Γ} ⊢w + +erase : ∀ {Γ M A} → Γ ⊢ M ⦂ A → Term +erase (Ax ⊢w) = ` lookup ⊢w +erase (⊢λ {x = x} ⊢N) = `λ x ⇒ erase ⊢N +erase (⊢L · ⊢M) = erase ⊢L · erase ⊢M +erase (⊢zero) = `zero +erase (⊢suc ⊢M) = `suc (erase ⊢M) +erase (⊢pred ⊢M) = `pred (erase ⊢M) +erase (⊢if0 ⊢L ⊢M ⊢N) = `if0 (erase ⊢L) then (erase ⊢M) else (erase ⊢N) +erase (⊢Y ⊢M) = `Y (erase ⊢M) +\end{code} + +### Properties of erasure + +\begin{code} +cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {s t u v x y} → + s ≡ t → u ≡ v → x ≡ y → f s u x ≡ f t v y +cong₃ f refl refl refl = refl + +lookup-lemma : ∀ {Γ x A} → (⊢x : Γ ∋ x ⦂ A) → lookup ⊢x ≡ x +lookup-lemma Z = refl +lookup-lemma (S _ ⊢w) = lookup-lemma ⊢w + +erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M ⦂ A) → erase ⊢M ≡ M +erase-lemma (Ax ⊢x) = cong `_ (lookup-lemma ⊢x) +erase-lemma (⊢λ {x = x} ⊢N) = cong (`λ x ⇒_) (erase-lemma ⊢N) +erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M) +erase-lemma (⊢zero) = refl +erase-lemma (⊢suc ⊢M) = cong `suc_ (erase-lemma ⊢M) +erase-lemma (⊢pred ⊢M) = cong `pred_ (erase-lemma ⊢M) +erase-lemma (⊢if0 ⊢L ⊢M ⊢N) = cong₃ `if0_then_else_ + (erase-lemma ⊢L) (erase-lemma ⊢M) (erase-lemma ⊢N) +erase-lemma (⊢Y ⊢M) = cong `Y_ (erase-lemma ⊢M) +\end{code} + + +## Substitution + +### Lists as sets + +\begin{code} +open Collections.CollectionDec (Id) (_≟_) +\end{code} + +### Free variables + +\begin{code} +free : Term → List Id +free (` x) = [ x ] +free (`λ x ⇒ N) = free N \\ x +free (L · M) = free L ++ free M +free (`zero) = [] +free (`suc M) = free M +free (`pred M) = free M +free (`if0 L then M else N) = free L ++ free M ++ free N +free (`Y M) = free M +\end{code} + +### Fresh identifier + +\begin{code} +bump : String → Id → ℕ +bump s (id t n) with s String.≟ t +... | yes refl = suc n +... | no _ = 0 + +next : String → List Id → ℕ +next s = foldr _⊔_ 0 ∘ map (bump s) + +⊔-lemma : ∀ {s w xs} → w ∈ xs → bump s w ≤ next s xs +⊔-lemma {s} {_} {_ ∷ xs} here = m≤m⊔n _ (next s xs) +⊔-lemma {s} {_} {_ ∷ xs} (there x∈) = ≤-trans (⊔-lemma x∈) (n≤m⊔n _ (next s xs)) + +fresh : Id → List Id → Id +fresh (id s _) xs = id s (next s xs) + +fresh-lemma : ∀ {w x xs} → w ∈ xs → w ≢ fresh x xs +fresh-lemma {w @ (id t n)} {x @ (id s _)} {xs} w∈ w≢fr = {! (⊔-lemma {s} {w} {xs} w∈)!} -- with s String.≟ t +{- +... | yes refl = {! (⊔-lemma {s} {w} {xs} w∈)!} +... | no s≢t = {!!} + + +with s String.≟ t | fresh x xs +... | yes refl | fr = {! (⊔-lemma {s} {w} {xs} w∈)!} +... | no s≢t | _ = s≢t refl + + +next-lemma : ∀ {x xs} → x ∈ xs → x ≢ next xs +next-lemma x∈ refl = 1+n≰n (⊔-lemma x∈) +\end{code} + +### Identifier maps + +\begin{code} +∅ : Id → Term +∅ x = ` x + +infixl 5 _,_↦_ + +_,_↦_ : (Id → Term) → Id → Term → (Id → Term) +(ρ , x ↦ M) w with w ≟ x +... | yes _ = M +... | no _ = ρ w +\end{code} + +### Substitution + +\begin{code} +subst : List Id → (Id → Term) → Term → Term +subst ys ρ (` x) = ρ x +subst ys ρ (`λ x ⇒ N) = `λ y ⇒ subst (y ∷ ys) (ρ , x ↦ ` y) N + where + y = fresh ys +subst ys ρ (L · M) = subst ys ρ L · subst ys ρ M +subst ys ρ (`zero) = `zero +subst ys ρ (`suc M) = `suc (subst ys ρ M) +subst ys ρ (`pred M) = `pred (subst ys ρ M) +subst ys ρ (`if0 L then M else N) + = `if0 (subst ys ρ L) then (subst ys ρ M) else (subst ys ρ N) +subst ys ρ (`Y M) = `Y (subst ys ρ M) + +_[_:=_] : Term → Id → Term → Term +N [ x := M ] = subst (free M ++ (free N \\ x)) (∅ , x ↦ M) N +\end{code} + +### Testing substitution + +\begin{code} +_ : (` s · ` s · ` z) [ z := `zero ] ≡ (` s · ` s · `zero) +_ = refl + +_ : (` s · ` s · ` z) [ s := (`λ m ⇒ `suc ` m) ] [ z := `zero ] + ≡ ((`λ p ⇒ `suc ` p) · (`λ p ⇒ `suc ` p) · `zero) +_ = refl + +_ : (`λ m ⇒ ` m · ` n) [ n := ` m ] ≡ (`λ n ⇒ ` n · ` m) +_ = refl + +_ : subst [ m , n ] (∅ , m ↦ ` n , n ↦ ` m) (` m · ` n) ≡ (` n · ` m) +_ = refl +\end{code} + + +## Values + +\begin{code} +data Value : Term → Set where + + Zero : + ---------- + Value `zero + + Suc : ∀ {V} + → Value V + -------------- + → Value (`suc V) + + Fun : ∀ {x N} + --------------- + → Value (`λ x ⇒ N) +\end{code} + +## Reduction + +\begin{code} +infix 4 _⟶_ + +data _⟶_ : Term → Term → Set where + + ξ-·₁ : ∀ {L L′ M} + → L ⟶ L′ + ---------------- + → L · M ⟶ L′ · M + + ξ-·₂ : ∀ {V M M′} + → Value V + → M ⟶ M′ + ---------------- + → V · M ⟶ V · M′ + + β-⇒ : ∀ {x N V} + → Value V + ------------------------------ + → (`λ x ⇒ N) · V ⟶ N [ x := V ] + + ξ-suc : ∀ {M M′} + → M ⟶ M′ + ------------------ + → `suc M ⟶ `suc M′ + + ξ-pred : ∀ {M M′} + → M ⟶ M′ + -------------------- + → `pred M ⟶ `pred M′ + + β-pred-zero : + --------------------- + `pred `zero ⟶ `zero + + β-pred-suc : ∀ {V} + → Value V + -------------------- + → `pred (`suc V) ⟶ V + + ξ-if0 : ∀ {L L′ M N} + → L ⟶ L′ + ---------------------------------------------- + → `if0 L then M else N ⟶ `if0 L′ then M else N + + β-if0-zero : ∀ {M N} + ------------------------------ + → `if0 `zero then M else N ⟶ M + + β-if0-suc : ∀ {V M N} + → Value V + --------------------------------- + → `if0 (`suc V) then M else N ⟶ N + + ξ-Y : ∀ {M M′} + → M ⟶ M′ + -------------- + → `Y M ⟶ `Y M′ + + β-Y : ∀ {V x N} + → Value V + → V ≡ `λ x ⇒ N + ------------------------ + → `Y V ⟶ N [ x := `Y V ] +\end{code} + +## Reflexive and transitive closure + +\begin{code} +infix 2 _⟶*_ +infix 1 begin_ +infixr 2 _⟶⟨_⟩_ +infix 3 _∎ + +data _⟶*_ : Term → Term → Set where + + _∎ : ∀ {M} + ------------- + → M ⟶* M + + _⟶⟨_⟩_ : ∀ (L : Term) {M N} + → L ⟶ M + → M ⟶* N + --------- + → L ⟶* N + +begin_ : ∀ {M N} → (M ⟶* N) → (M ⟶* N) +begin M⟶*N = M⟶*N +\end{code} + +## Canonical forms + +\begin{code} +data Canonical : Term → Type → Set where + + Zero : + ------------------ + Canonical `zero `ℕ + + Suc : ∀ {V} + → Canonical V `ℕ + --------------------- + → Canonical (`suc V) `ℕ + + Fun : ∀ {x N A B} + → ε , x ⦂ A ⊢ N ⦂ B + ------------------------------ + → Canonical (`λ x ⇒ N) (A ⇒ B) +\end{code} + +## Canonical forms lemma + +Every typed value is canonical. + +\begin{code} +canonical : ∀ {V A} + → ε ⊢ V ⦂ A + → Value V + ------------- + → Canonical V A +canonical ⊢zero Zero = Zero +canonical (⊢suc ⊢V) (Suc VV) = Suc (canonical ⊢V VV) +canonical (⊢λ ⊢N) Fun = Fun ⊢N +\end{code} + +Every canonical form has a type and a value. + +\begin{code} +type : ∀ {V A} + → Canonical V A + ------------- + → ε ⊢ V ⦂ A +type Zero = ⊢zero +type (Suc CV) = ⊢suc (type CV) +type (Fun ⊢N) = ⊢λ ⊢N + +value : ∀ {V A} + → Canonical V A + ------------- + → Value V +value Zero = Zero +value (Suc CV) = Suc (value CV) +value (Fun ⊢N) = Fun +\end{code} + +## Progress + +\begin{code} +data Progress (M : Term) (A : Type) : Set where + step : ∀ {N} + → M ⟶ N + ---------- + → Progress M A + done : + Canonical M A + ------------- + → Progress M A + +progress : ∀ {M A} → ε ⊢ M ⦂ A → Progress M A +progress (Ax ()) +progress (⊢λ ⊢N) = done (Fun ⊢N) +progress (⊢L · ⊢M) with progress ⊢L +... | step L⟶L′ = step (ξ-·₁ L⟶L′) +... | done (Fun _) with progress ⊢M +... | step M⟶M′ = step (ξ-·₂ Fun M⟶M′) +... | done CM = step (β-⇒ (value CM)) +progress ⊢zero = done Zero +progress (⊢suc ⊢M) with progress ⊢M +... | step M⟶M′ = step (ξ-suc M⟶M′) +... | done CM = done (Suc CM) +progress (⊢pred ⊢M) with progress ⊢M +... | step M⟶M′ = step (ξ-pred M⟶M′) +... | done Zero = step β-pred-zero +... | done (Suc CM) = step (β-pred-suc (value CM)) +progress (⊢if0 ⊢L ⊢M ⊢N) with progress ⊢L +... | step L⟶L′ = step (ξ-if0 L⟶L′) +... | done Zero = step β-if0-zero +... | done (Suc CM) = step (β-if0-suc (value CM)) +progress (⊢Y ⊢M) with progress ⊢M +... | step M⟶M′ = step (ξ-Y M⟶M′) +... | done (Fun _) = step (β-Y Fun refl) +\end{code} + + +## Preservation + +### Domain of an environment + +\begin{code} +dom : Env → List Id +dom ε = [] +dom (Γ , x ⦂ A) = x ∷ dom Γ + +dom-lemma : ∀ {Γ y B} → Γ ∋ y ⦂ B → y ∈ dom Γ +dom-lemma Z = here +dom-lemma (S x≢y ⊢y) = there (dom-lemma ⊢y) + +free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ +free-lemma (Ax ⊢x) w∈ with w∈ +... | here = dom-lemma ⊢x +... | there () +free-lemma {Γ} (⊢λ {N = N} ⊢N) = ∷-to-\\ (free-lemma ⊢N) +free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈ +... | inj₁ ∈L = free-lemma ⊢L ∈L +... | inj₂ ∈M = free-lemma ⊢M ∈M +free-lemma ⊢zero () +free-lemma (⊢suc ⊢M) w∈ = free-lemma ⊢M w∈ +free-lemma (⊢pred ⊢M) w∈ = free-lemma ⊢M w∈ +free-lemma (⊢if0 ⊢L ⊢M ⊢N) w∈ + with ++-to-⊎ w∈ +... | inj₁ ∈L = free-lemma ⊢L ∈L +... | inj₂ ∈MN with ++-to-⊎ ∈MN +... | inj₁ ∈M = free-lemma ⊢M ∈M +... | inj₂ ∈N = free-lemma ⊢N ∈N +free-lemma (⊢Y ⊢M) w∈ = free-lemma ⊢M w∈ +\end{code} + +### Renaming + +\begin{code} +⊢rename : ∀ {Γ Δ xs} + → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) + -------------------------------------------------- + → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) +⊢rename ⊢σ ⊆xs (Ax ⊢x) = Ax (⊢σ ∈xs ⊢x) + where + ∈xs = ⊆xs here +⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (⊢λ {x = x} {N = N} {A = A} ⊢N) + = ⊢λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) + where + Γ′ = Γ , x ⦂ A + Δ′ = Δ , x ⦂ A + xs′ = x ∷ xs + + ⊢σ′ : ∀ {w B} → w ∈ xs′ → Γ′ ∋ w ⦂ B → Δ′ ∋ w ⦂ B + ⊢σ′ w∈′ Z = Z + ⊢σ′ w∈′ (S w≢ ⊢w) = S w≢ (⊢σ ∈w ⊢w) + where + ∈w = there⁻¹ w∈′ w≢ + + ⊆xs′ : free N ⊆ xs′ + ⊆xs′ = \\-to-∷ ⊆xs +⊢rename ⊢σ ⊆xs (⊢L · ⊢M) = ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M + where + L⊆ = trans-⊆ ⊆-++₁ ⊆xs + M⊆ = trans-⊆ ⊆-++₂ ⊆xs +⊢rename ⊢σ ⊆xs (⊢zero) = ⊢zero +⊢rename ⊢σ ⊆xs (⊢suc ⊢M) = ⊢suc (⊢rename ⊢σ ⊆xs ⊢M) +⊢rename ⊢σ ⊆xs (⊢pred ⊢M) = ⊢pred (⊢rename ⊢σ ⊆xs ⊢M) +⊢rename ⊢σ ⊆xs (⊢if0 {L = L} ⊢L ⊢M ⊢N) + = ⊢if0 (⊢rename ⊢σ L⊆ ⊢L) (⊢rename ⊢σ M⊆ ⊢M) (⊢rename ⊢σ N⊆ ⊢N) + where + L⊆ = trans-⊆ ⊆-++₁ ⊆xs + M⊆ = trans-⊆ ⊆-++₁ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) + N⊆ = trans-⊆ ⊆-++₂ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) +⊢rename ⊢σ ⊆xs (⊢Y ⊢M) = ⊢Y (⊢rename ⊢σ ⊆xs ⊢M) + +\end{code} + + +### Substitution preserves types + +\begin{code} +⊢subst : ∀ {Γ Δ xs ys ρ} + → (∀ {x} → x ∈ xs → free (ρ x) ⊆ ys) + → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) + ------------------------------------------------------------- + → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ A) +⊢subst Σ ⊢ρ ⊆xs (Ax ⊢x) + = ⊢ρ (⊆xs here) ⊢x +⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (⊢λ {x = x} {N = N} {A = A} ⊢N) + = ⊢λ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N) + where + y = fresh ys + Γ′ = Γ , x ⦂ A + Δ′ = Δ , y ⦂ A + xs′ = x ∷ xs + ys′ = y ∷ ys + ρ′ = ρ , x ↦ ` y + + Σ′ : ∀ {w} → w ∈ xs′ → free (ρ′ w) ⊆ ys′ + Σ′ {w} w∈′ with w ≟ x + ... | yes refl = ⊆-++₁ + ... | no w≢ = ⊆-++₂ ∘ Σ (there⁻¹ w∈′ w≢) + + ⊆xs′ : free N ⊆ xs′ + ⊆xs′ = \\-to-∷ ⊆xs + + ⊢σ : ∀ {w C} → w ∈ ys → Δ ∋ w ⦂ C → Δ′ ∋ w ⦂ C + ⊢σ w∈ ⊢w = S (fresh-lemma w∈) ⊢w + + ⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C + ⊢ρ′ {w} _ Z with w ≟ x + ... | yes _ = Ax Z + ... | no w≢ = ⊥-elim (w≢ refl) + ⊢ρ′ {w} w∈′ (S w≢ ⊢w) with w ≟ x + ... | yes refl = ⊥-elim (w≢ refl) + ... | no _ = ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ w∈) (⊢ρ w∈ ⊢w) + where + w∈ = there⁻¹ w∈′ w≢ + +⊢subst Σ ⊢ρ ⊆xs (⊢L · ⊢M) + = ⊢subst Σ ⊢ρ L⊆ ⊢L · ⊢subst Σ ⊢ρ M⊆ ⊢M + where + L⊆ = trans-⊆ ⊆-++₁ ⊆xs + M⊆ = trans-⊆ ⊆-++₂ ⊆xs +⊢subst Σ ⊢ρ ⊆xs ⊢zero = ⊢zero +⊢subst Σ ⊢ρ ⊆xs (⊢suc ⊢M) = ⊢suc (⊢subst Σ ⊢ρ ⊆xs ⊢M) +⊢subst Σ ⊢ρ ⊆xs (⊢pred ⊢M) = ⊢pred (⊢subst Σ ⊢ρ ⊆xs ⊢M) +⊢subst Σ ⊢ρ ⊆xs (⊢if0 {L = L} ⊢L ⊢M ⊢N) + = ⊢if0 (⊢subst Σ ⊢ρ L⊆ ⊢L) (⊢subst Σ ⊢ρ M⊆ ⊢M) (⊢subst Σ ⊢ρ N⊆ ⊢N) + where + L⊆ = trans-⊆ ⊆-++₁ ⊆xs + M⊆ = trans-⊆ ⊆-++₁ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) + N⊆ = trans-⊆ ⊆-++₂ (trans-⊆ (⊆-++₂ {free L}) ⊆xs) +⊢subst Σ ⊢ρ ⊆xs (⊢Y ⊢M) = ⊢Y (⊢subst Σ ⊢ρ ⊆xs ⊢M) + +⊢substitution : ∀ {Γ x A N B M} → + Γ , x ⦂ A ⊢ N ⦂ B → + Γ ⊢ M ⦂ A → + -------------------- + Γ ⊢ N [ x := M ] ⦂ B +⊢substitution {Γ} {x} {A} {N} {B} {M} ⊢N ⊢M = + ⊢subst {Γ′} {Γ} {xs} {ys} {ρ} Σ ⊢ρ {N} {B} ⊆xs ⊢N + where + Γ′ = Γ , x ⦂ A + xs = free N + ys = free M ++ (free N \\ x) + ρ = ∅ , x ↦ M + + Σ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys + Σ {w} w∈ y∈ with w ≟ x + ... | yes _ = ⊆-++₁ y∈ + ... | no w≢ rewrite ∈-[_] y∈ = ⊆-++₂ (∈-≢-to-\\ w∈ w≢) + + ⊢ρ : ∀ {w B} → w ∈ xs → Γ′ ∋ w ⦂ B → Γ ⊢ ρ w ⦂ B + ⊢ρ {w} w∈ Z with w ≟ x + ... | yes _ = ⊢M + ... | no w≢ = ⊥-elim (w≢ refl) + ⊢ρ {w} w∈ (S w≢ ⊢w) with w ≟ x + ... | yes refl = ⊥-elim (w≢ refl) + ... | no _ = Ax ⊢w + + ⊆xs : free N ⊆ xs + ⊆xs x∈ = x∈ +\end{code} + +### Preservation + +\begin{code} +preservation : ∀ {Γ M N A} + → Γ ⊢ M ⦂ A + → M ⟶ N + --------- + → Γ ⊢ N ⦂ A +preservation (Ax ⊢x) () +preservation (⊢λ ⊢N) () +preservation (⊢L · ⊢M) (ξ-·₁ L⟶) = preservation ⊢L L⟶ · ⊢M +preservation (⊢V · ⊢M) (ξ-·₂ _ M⟶) = ⊢V · preservation ⊢M M⟶ +preservation ((⊢λ ⊢N) · ⊢W) (β-⇒ _) = ⊢substitution ⊢N ⊢W +preservation (⊢zero) () +preservation (⊢suc ⊢M) (ξ-suc M⟶) = ⊢suc (preservation ⊢M M⟶) +preservation (⊢pred ⊢M) (ξ-pred M⟶) = ⊢pred (preservation ⊢M M⟶) +preservation (⊢pred ⊢zero) (β-pred-zero) = ⊢zero +preservation (⊢pred (⊢suc ⊢M)) (β-pred-suc _) = ⊢M +preservation (⊢if0 ⊢L ⊢M ⊢N) (ξ-if0 L⟶) = ⊢if0 (preservation ⊢L L⟶) ⊢M ⊢N +preservation (⊢if0 ⊢zero ⊢M ⊢N) β-if0-zero = ⊢M +preservation (⊢if0 (⊢suc ⊢V) ⊢M ⊢N) (β-if0-suc _) = ⊢N +preservation (⊢Y ⊢M) (ξ-Y M⟶) = ⊢Y (preservation ⊢M M⟶) +preservation (⊢Y (⊢λ ⊢N)) (β-Y _ refl) = ⊢substitution ⊢N (⊢Y (⊢λ ⊢N)) +-} +\end{code} + +