From 3ba45ceb62c4f087c16fe94506eafb4932daca01 Mon Sep 17 00:00:00 2001 From: wadler Date: Sun, 24 Jun 2018 19:45:51 -0300 Subject: [PATCH] changed rule names in Lambda, Prop to match Inference --- src/plta/Inference.lagda | 29 +++++------ src/plta/Lambda.lagda | 49 +++++++++--------- src/plta/LambdaProp.lagda | 103 ++++++++++++++++++++++---------------- 3 files changed, 100 insertions(+), 81 deletions(-) diff --git a/src/plta/Inference.lagda b/src/plta/Inference.lagda index 5e6959ac..7e7e2055 100644 --- a/src/plta/Inference.lagda +++ b/src/plta/Inference.lagda @@ -149,7 +149,7 @@ data _⊢_↑_ where data _⊢_↓_ where - ⊢λ : ∀ {Γ x N A B} + ⊢ƛ : ∀ {Γ x N A B} → Γ , x ⦂ A ⊢ N ↓ B ----------------------- → Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B @@ -246,7 +246,7 @@ synthesize Γ (M ↓ A) = inherit Γ (ƛ x ⇒ N) (A ⇒ B) = do ⊢N ← inherit (Γ , x ⦂ A) N B - return (⊢λ ⊢N) + return (⊢ƛ ⊢N) inherit Γ (ƛ x ⇒ N) `ℕ = error⁻ "lambda cannot be of type natural" (ƛ x ⇒ N) [] inherit Γ `zero `ℕ = @@ -289,8 +289,8 @@ x ≠ y with x ≟ y ⊢four = (⊢↓ (⊢μ - (⊢λ - (⊢λ + (⊢ƛ + (⊢ƛ (⊢case (Ax (S (_≠_ "m" "n") Z)) (⊢↑ (Ax Z) refl) (⊢suc (⊢↑ @@ -309,13 +309,13 @@ _ = refl ⊢fourCh : ε ⊢ fourCh ↑ `ℕ ⊢fourCh = - (⊢↓ (⊢λ (⊢↑ (Ax Z · ⊢λ (⊢suc (⊢↑ (Ax Z) refl)) · ⊢zero) refl)) · + (⊢↓ (⊢ƛ (⊢↑ (Ax Z · ⊢ƛ (⊢suc (⊢↑ (Ax Z) refl)) · ⊢zero) refl)) · ⊢↑ (⊢↓ - (⊢λ - (⊢λ - (⊢λ - (⊢λ + (⊢ƛ + (⊢ƛ + (⊢ƛ + (⊢ƛ (⊢↑ (Ax (S (_≠_ "m" "z") @@ -332,16 +332,16 @@ _ = refl refl) refl))))) · - ⊢λ - (⊢λ + ⊢ƛ + (⊢ƛ (⊢↑ (Ax (S (_≠_ "s" "z") Z) · ⊢↑ (Ax (S (_≠_ "s" "z") Z) · ⊢↑ (Ax Z) refl) refl) refl)) · - ⊢λ - (⊢λ + ⊢ƛ + (⊢ƛ (⊢↑ (Ax (S (_≠_ "s" "z") Z) · ⊢↑ (Ax (S (_≠_ "s" "z") Z) · ⊢↑ (Ax Z) refl) @@ -391,6 +391,7 @@ _ : synthesize ε (((ƛ "x" ⇒ ⌊ "x" ⌋ ↑) ↓ `ℕ ⇒ (`ℕ ⇒ `ℕ))) _ = refl \end{code} + ## Erasure \begin{code} @@ -409,7 +410,7 @@ _ = refl ∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻ ∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻ -∥ ⊢λ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻ +∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻ ∥ ⊢zero ∥⁻ = DB.`zero ∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻ ∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.`caseℕ ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻ diff --git a/src/plta/Lambda.lagda b/src/plta/Lambda.lagda index f0526170..b92835ed 100644 --- a/src/plta/Lambda.lagda +++ b/src/plta/Lambda.lagda @@ -905,38 +905,38 @@ data _⊢_⦂_ : Context → Term → Type → Set where → Γ ⊢ ⌊ x ⌋ ⦂ A -- ⇒-I - ⇒-I : ∀ {Γ x N A B} + ⊢ƛ : ∀ {Γ x N A B} → Γ , x ⦂ A ⊢ N ⦂ B ------------------- → Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B -- ⇒-E - ⇒-E : ∀ {Γ L M A B} + _·_ : ∀ {Γ L M A B} → Γ ⊢ L ⦂ A ⇒ B → Γ ⊢ M ⦂ A ------------- → Γ ⊢ L · M ⦂ B -- ℕ-I₁ - ℕ-I₁ : ∀ {Γ} + ⊢zero : ∀ {Γ} -------------- → Γ ⊢ `zero ⦂ `ℕ -- ℕ-I₂ - ℕ-I₂ : ∀ {Γ M} + ⊢suc : ∀ {Γ M} → Γ ⊢ M ⦂ `ℕ --------------- → Γ ⊢ `suc M ⦂ `ℕ -- ℕ-E - ℕ-E : ∀ {Γ L M x N A} + ⊢case : ∀ {Γ L M x N A} → Γ ⊢ L ⦂ `ℕ → Γ ⊢ M ⦂ A → Γ , x ⦂ `ℕ ⊢ N ⦂ A ------------------------------------- → Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ⦂ A - Fix : ∀ {Γ x M A} + ⊢μ : ∀ {Γ x M A} → Γ , x ⦂ A ⊢ M ⦂ A ----------------- → Γ ⊢ μ x ⇒ M ⦂ A @@ -1002,9 +1002,9 @@ is a type derivation for the Church numberal two: Γ₂ ⊢ ⌊ "s" ⌋ ⦂ A ⇒ A Γ₂ ⊢ ⌊ "s" ⌋ · ⌊ "z" ⌋ ⦂ A -------------------------------------------------- _·_ Γ₂ ⊢ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A - ---------------------------------------------- ƛ_ + ---------------------------------------------- ⊢ƛ Γ₁ ⊢ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A ⇒ A - ---------------------------------------------------------- ƛ_ + ---------------------------------------------------------- ⊢ƛ ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A ⇒ A where `∋s` and `∋z` abbreviate the two derivations: @@ -1022,7 +1022,7 @@ Ch : Type → Type Ch A = (A ⇒ A) ⇒ A ⇒ A ⊢twoᶜ : ∀ {A} → ∅ ⊢ twoᶜ ⦂ Ch A -⊢twoᶜ = ⇒-I (⇒-I (⇒-E (Ax ∋s) (⇒-E (Ax ∋s) (Ax ∋z)))) +⊢twoᶜ = ⊢ƛ (⊢ƛ (Ax ∋s · (Ax ∋s · Ax ∋z))) where ∋s = S ("s" ≠ "z") Z @@ -1032,11 +1032,11 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A Here are the typings corresponding to our first example. \begin{code} ⊢two : ∅ ⊢ two ⦂ `ℕ -⊢two = ℕ-I₂ (ℕ-I₂ ℕ-I₁) +⊢two = ⊢suc (⊢suc ⊢zero) ⊢plus : ∅ ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ -⊢plus = Fix (⇒-I (⇒-I (ℕ-E (Ax ∋m) (Ax ∋n) - (ℕ-I₂ (⇒-E (⇒-E (Ax ∋+) (Ax ∋m′)) (Ax ∋n′)))))) +⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (Ax ∋m) (Ax ∋n) + (⊢suc (Ax ∋+ · Ax ∋m′ · Ax ∋n′))))) where ∋+ = (S ("+" ≠ "m") (S ("+" ≠ "n") (S ("+" ≠ "m") Z))) ∋m = (S ("m" ≠ "n") Z) @@ -1045,7 +1045,7 @@ Here are the typings corresponding to our first example. ∋n′ = (S ("n" ≠ "m") Z) ⊢four : ∅ ⊢ four ⦂ `ℕ -⊢four = ⇒-E (⇒-E ⊢plus ⊢two) ⊢two +⊢four = ⊢plus · ⊢two · ⊢two \end{code} The two occcurrences of variable `"n"` in the original term appear in different contexts, and correspond here to the two different @@ -1057,8 +1057,7 @@ branch of the case expression. Here are typings for the remainder of the Church example. \begin{code} ⊢plusᶜ : ∀ {A} → ∅ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A -⊢plusᶜ = ⇒-I (⇒-I (⇒-I (⇒-I (⇒-E (⇒-E (Ax ∋m) (Ax ∋s)) - (⇒-E (⇒-E (Ax ∋n) (Ax ∋s)) (Ax ∋z)))))) +⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (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) @@ -1066,12 +1065,12 @@ Here are typings for the remainder of the Church example. ∋z = Z ⊢sucᶜ : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ -⊢sucᶜ = ⇒-I (ℕ-I₂ (Ax ∋n)) +⊢sucᶜ = ⊢ƛ (⊢suc (Ax ∋n)) where ∋n = Z ⊢fourᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ -⊢fourᶜ = ⇒-E (⇒-E (⇒-E (⇒-E ⊢plusᶜ ⊢twoᶜ) ⊢twoᶜ) ⊢sucᶜ) ℕ-I₁ +⊢fourᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero \end{code} @@ -1089,20 +1088,20 @@ Typing C-l causes Agda to create a hole and tell us its expected type. ?0 : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ Now we fill in the hole by typing C-c C-r. Agda observes that -the outermost term in `sucᶜ` in `ƛ`, which is typed using `⇒-I`. The -`⇒-I` rule in turn takes one argument, which Agda leaves as a hole. +the outermost term in `sucᶜ` in `⊢ƛ`, which is typed using `ƛ`. The +`ƛ` rule in turn takes one argument, which Agda leaves as a hole. - ⊢sucᶜ = ⇒-I { }1 + ⊢sucᶜ = ⊢ƛ { }1 ?1 : ∅ , "n" ⦂ `ℕ ⊢ `suc ⌊ "n" ⌋ ⦂ `ℕ We can fill in the hole by type C-c C-r again. - ⊢sucᶜ = ⇒-I (`ℕ-I₂ { }2) + ⊢sucᶜ = ⊢ƛ (⊢suc { }2) ?2 : ∅ , "n" ⦂ `ℕ ⊢ ⌊ "n" ⌋ ⦂ `ℕ And again. - ⊢suc′ = ⇒-I (ℕ-I₂ (Ax { }3)) + ⊢suc′ = ⊢ƛ (⊢suc (Ax { }3)) ?3 : ∅ , "n" ⦂ `ℕ ∋ "n" ⦂ `ℕ A further attempt with C-c C-r yields the message: @@ -1111,7 +1110,7 @@ A further attempt with C-c C-r yields the message: We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are done. - ⊢suc′ = ⇒-I (ℕ-I₂ (Ax Z)) + ⊢suc′ = ⊢ƛ (⊢suc (Ax Z)) The entire process can be automated using Agsy, invoked with C-c C-a. @@ -1144,7 +1143,7 @@ application is both a natural and a function. \begin{code} nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A) -nope₁ (⇒-E () _) +nope₁ (() · _) \end{code} As a second example, here is a formal proof that it is not possible to @@ -1153,7 +1152,7 @@ doing so requires types `A` and `B` such that `A ⇒ B ≡ A`. \begin{code} nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ⌊ "x" ⌋ · ⌊ "x" ⌋ ⦂ A) -nope₂ (⇒-I (⇒-E (Ax ∋x) (Ax ∋x′))) = contradiction (∋-injective ∋x ∋x′) +nope₂ (⊢ƛ (Ax ∋x · Ax ∋x′)) = contradiction (∋-injective ∋x ∋x′) where contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A) contradiction () diff --git a/src/plta/LambdaProp.lagda b/src/plta/LambdaProp.lagda index 1c52eb19..c116994e 100644 --- a/src/plta/LambdaProp.lagda +++ b/src/plta/LambdaProp.lagda @@ -75,13 +75,13 @@ canonical : ∀ {M A} → Value M --------------- → Canonical M ⦂ A -canonical (Ax ()) () -canonical (⇒-I ⊢N) V-ƛ = C-ƛ -canonical (⇒-E ⊢L ⊢M) () -canonical ℕ-I₁ V-zero = C-zero -canonical (ℕ-I₂ ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV) -canonical (ℕ-E ⊢L ⊢M ⊢N) () -canonical (Fix ⊢M) () +canonical (Ax ()) () +canonical (⊢ƛ ⊢N) V-ƛ = C-ƛ +canonical (⊢L · ⊢M) () +canonical ⊢zero V-zero = C-zero +canonical (⊢suc ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV) +canonical (⊢case ⊢L ⊢M ⊢N) () +canonical (⊢μ ⊢M) () value : ∀ {M A} → Canonical M ⦂ A @@ -116,23 +116,23 @@ progress : ∀ {M A} ---------- → Progress M progress (Ax ()) -progress (⇒-I ⊢N) = done V-ƛ -progress (⇒-E ⊢L ⊢M) with progress ⊢L +progress (⊢ƛ ⊢N) = done V-ƛ +progress (⊢L · ⊢M) with progress ⊢L ... | step L⟶L′ = step (ξ-·₁ L⟶L′) ... | done VL with progress ⊢M ... | step M⟶M′ = step (ξ-·₂ VL M⟶M′) ... | done VM with canonical ⊢L VL ... | C-ƛ = step (β-ƛ· VM) -progress ℕ-I₁ = done V-zero -progress (ℕ-I₂ ⊢M) with progress ⊢M +progress ⊢zero = done V-zero +progress (⊢suc ⊢M) with progress ⊢M ... | step M⟶M′ = step (ξ-suc M⟶M′) ... | done VM = done (V-suc VM) -progress (ℕ-E ⊢L ⊢M ⊢N) with progress ⊢L +progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L ... | step L⟶L′ = step (ξ-case L⟶L′) ... | done VL with canonical ⊢L VL ... | C-zero = step β-case-zero ... | C-suc CL = step (β-case-suc (value CL)) -progress (Fix ⊢M) = step β-μ +progress (⊢μ ⊢M) = step β-μ \end{code} This code reads neatly in part because we consider the @@ -204,13 +204,13 @@ rename : ∀ {Γ Δ} → (∀ {w B} → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B) ---------------------------------- → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) -rename σ (Ax ∋w) = Ax (σ ∋w) -rename σ (⇒-I ⊢N) = ⇒-I (rename (ext σ) ⊢N) -rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M) -rename σ ℕ-I₁ = ℕ-I₁ -rename σ (ℕ-I₂ ⊢M) = ℕ-I₂ (rename σ ⊢M) -rename σ (ℕ-E ⊢L ⊢M ⊢N) = ℕ-E (rename σ ⊢L) (rename σ ⊢M) (rename (ext σ) ⊢N) -rename σ (Fix ⊢M) = Fix (rename (ext σ) ⊢M) +rename σ (Ax ∋w) = Ax (σ ∋w) +rename σ (⊢ƛ ⊢N) = ⊢ƛ (rename (ext σ) ⊢N) +rename σ (⊢L · ⊢M) = (rename σ ⊢L) · (rename σ ⊢M) +rename σ ⊢zero = ⊢zero +rename σ (⊢suc ⊢M) = ⊢suc (rename σ ⊢M) +rename σ (⊢case ⊢L ⊢M ⊢N) = ⊢case (rename σ ⊢L) (rename σ ⊢M) (rename (ext σ) ⊢N) +rename σ (⊢μ ⊢M) = ⊢μ (rename (ext σ) ⊢M) \end{code} We have three important corollaries. First, @@ -316,18 +316,18 @@ subst {x = y} (Ax {x = x} Z) ⊢V with x ≟ y subst {x = y} (Ax {x = x} (S x≢y ∋x)) ⊢V with x ≟ y ... | yes refl = ⊥-elim (x≢y refl) ... | no _ = Ax ∋x -subst {x = y} (⇒-I {x = x} ⊢N) ⊢V with x ≟ y -... | yes refl = ⇒-I (rename-≡ ⊢N) -... | no x≢y = ⇒-I (subst (rename-≢ x≢y ⊢N) ⊢V) -subst (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) -subst ℕ-I₁ ⊢V = ℕ-I₁ -subst (ℕ-I₂ ⊢M) ⊢V = ℕ-I₂ (subst ⊢M ⊢V) -subst {x = y} (ℕ-E {x = x} ⊢L ⊢M ⊢N) ⊢V with x ≟ y -... | yes refl = ℕ-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (rename-≡ ⊢N) -... | no x≢y = ℕ-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (subst (rename-≢ x≢y ⊢N) ⊢V) -subst {x = y} (Fix {x = x} ⊢M) ⊢V with x ≟ y -... | yes refl = Fix (rename-≡ ⊢M) -... | no x≢y = Fix (subst (rename-≢ x≢y ⊢M) ⊢V) +subst {x = y} (⊢ƛ {x = x} ⊢N) ⊢V with x ≟ y +... | yes refl = ⊢ƛ (rename-≡ ⊢N) +... | no x≢y = ⊢ƛ (subst (rename-≢ x≢y ⊢N) ⊢V) +subst (⊢L · ⊢M) ⊢V = (subst ⊢L ⊢V) · (subst ⊢M ⊢V) +subst ⊢zero ⊢V = ⊢zero +subst (⊢suc ⊢M) ⊢V = ⊢suc (subst ⊢M ⊢V) +subst {x = y} (⊢case {x = x} ⊢L ⊢M ⊢N) ⊢V with x ≟ y +... | yes refl = ⊢case (subst ⊢L ⊢V) (subst ⊢M ⊢V) (rename-≡ ⊢N) +... | no x≢y = ⊢case (subst ⊢L ⊢V) (subst ⊢M ⊢V) (subst (rename-≢ x≢y ⊢N) ⊢V) +subst {x = y} (⊢μ {x = x} ⊢M) ⊢V with x ≟ y +... | yes refl = ⊢μ (rename-≡ ⊢M) +... | no x≢y = ⊢μ (subst (rename-≢ x≢y ⊢M) ⊢V) \end{code} @@ -345,18 +345,37 @@ preserve : ∀ {M N A} ---------- → ∅ ⊢ N ⦂ A preserve (Ax ()) -preserve (⇒-I ⊢N) () -preserve (⇒-E ⊢L ⊢M) (ξ-·₁ L⟶L′) = ⇒-E (preserve ⊢L L⟶L′) ⊢M -preserve (⇒-E ⊢L ⊢M) (ξ-·₂ VL M⟶M′) = ⇒-E ⊢L (preserve ⊢M M⟶M′) -preserve (⇒-E (⇒-I ⊢N) ⊢V) (β-ƛ· VV) = subst ⊢N ⊢V -preserve ℕ-I₁ () -preserve (ℕ-I₂ ⊢M) (ξ-suc M⟶M′) = ℕ-I₂ (preserve ⊢M M⟶M′) -preserve (ℕ-E ⊢L ⊢M ⊢N) (ξ-case L⟶L′) = ℕ-E (preserve ⊢L L⟶L′) ⊢M ⊢N -preserve (ℕ-E ℕ-I₁ ⊢M ⊢N) β-case-zero = ⊢M -preserve (ℕ-E (ℕ-I₂ ⊢V) ⊢M ⊢N) (β-case-suc VV) = subst ⊢N ⊢V -preserve (Fix ⊢M) (β-μ) = subst ⊢M (Fix ⊢M) +preserve (⊢ƛ ⊢N) () +preserve (⊢L · ⊢M) (ξ-·₁ L⟶L′) = (preserve ⊢L L⟶L′) · ⊢M +preserve (⊢L · ⊢M) (ξ-·₂ VL M⟶M′) = ⊢L · (preserve ⊢M M⟶M′) +preserve ((⊢ƛ ⊢N) · ⊢V) (β-ƛ· VV) = subst ⊢N ⊢V +preserve ⊢zero () +preserve (⊢suc ⊢M) (ξ-suc M⟶M′) = ⊢suc (preserve ⊢M M⟶M′) +preserve (⊢case ⊢L ⊢M ⊢N) (ξ-case L⟶L′) = ⊢case (preserve ⊢L L⟶L′) ⊢M ⊢N +preserve (⊢case ⊢zero ⊢M ⊢N) β-case-zero = ⊢M +preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-case-suc VV) = subst ⊢N ⊢V +preserve (⊢μ ⊢M) (β-μ) = subst ⊢M (⊢μ ⊢M) \end{code} + +## Normalisation with streams + +codata Lift (A : Set) where + lift : A → Lift A + +data _↠_ : Term → Term → Set where + + _∎ : ∀ (M : Term) + ----- + → M ↠ M + + _↦⟨_⟩_ : ∀ (L : Term) {M N : Term} + → L ⟶ M + → Lift (M ↠ N) + ------------ + → L ↠ N + + ## Normalisation \begin{code}