From fb2c3ab076156736cc362069211882989287019e Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 2 Jul 2018 19:18:44 -0300 Subject: [PATCH] saved old substitution in extra --- extra/extra/OldSubstitution.lagda | 49 ++++++++++++++++++++++++++++ src/plta/DeBruijn.lagda | 44 ++++++++++++++++--------- src/plta/Lambda.lagda | 29 ----------------- src/plta/Properties.lagda | 54 +++++-------------------------- 4 files changed, 85 insertions(+), 91 deletions(-) create mode 100644 extra/extra/OldSubstitution.lagda diff --git a/extra/extra/OldSubstitution.lagda b/extra/extra/OldSubstitution.lagda new file mode 100644 index 00000000..ea195cb4 --- /dev/null +++ b/extra/extra/OldSubstitution.lagda @@ -0,0 +1,49 @@ +infix 9 _[_:=_] + +_[_:=_] : Term → Id → Term → Term +(` x) [ y := V ] with x ≟ y +... | yes _ = V +... | no _ = ` x +(ƛ x ⇒ N) [ y := V ] with x ≟ y +... | yes _ = ƛ x ⇒ N +... | no _ = ƛ x ⇒ (N [ y := V ]) +(L · M) [ y := V ] = (L [ y := V ]) · (M [ y := V ]) +(`zero) [ y := V ] = `zero +(`suc M) [ y := V ] = `suc (M [ y := V ]) +(`case L + [zero⇒ M + |suc x ⇒ N ]) + [ y := V ] with x ≟ y +... | yes _ = `case L [ y := V ] + [zero⇒ M [ y := V ] + |suc x ⇒ N ] +... | no _ = `case L [ y := V ] + [zero⇒ M [ y := V ] + |suc x ⇒ N [ y := V ] ] +(μ x ⇒ N) [ y := V ] with x ≟ y +... | yes _ = μ x ⇒ N +... | no _ = μ x ⇒ (N [ y := V ]) + +subst : ∀ {Γ x N V A B} + → ∅ ⊢ V ⦂ A + → Γ , x ⦂ A ⊢ N ⦂ B + -------------------- + → Γ ⊢ N [ x := V ] ⦂ B +subst {x = y} ⊢V (⊢` {x = x} Z) with x ≟ y +... | yes refl = weaken ⊢V +... | no x≢y = ⊥-elim (x≢y refl) +subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∋x)) with x ≟ y +... | yes refl = ⊥-elim (x≢y refl) +... | no _ = ⊢` ∋x +subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y +... | yes refl = ⊢ƛ (drop ⊢N) +... | no x≢y = ⊢ƛ (subst ⊢V (swap x≢y ⊢N)) +subst ⊢V (⊢L · ⊢M) = subst ⊢V ⊢L · subst ⊢V ⊢M +subst ⊢V ⊢zero = ⊢zero +subst ⊢V (⊢suc ⊢M) = ⊢suc (subst ⊢V ⊢M) +subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y +... | yes refl = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N) +... | no x≢y = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N)) +subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y +... | yes refl = ⊢μ (drop ⊢M) +... | no x≢y = ⊢μ (subst ⊢V (swap x≢y ⊢M)) diff --git a/src/plta/DeBruijn.lagda b/src/plta/DeBruijn.lagda index 9be25b3e..96b3fe22 100644 --- a/src/plta/DeBruijn.lagda +++ b/src/plta/DeBruijn.lagda @@ -1016,6 +1016,9 @@ V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N ## Progress +As before, every term that is well-typed and closed is either +a value or takes a reduction step. The formulation of progress +is just as before, but annotated with types. \begin{code} data Progress {A} (M : ∅ ⊢ A) : Set where step : ∀ {N : ∅ ⊢ A} @@ -1026,31 +1029,40 @@ data Progress {A} (M : ∅ ⊢ A) : Set where Value M ---------- → Progress M +\end{code} +The statement and proof of progress is much as before. +Again, we must add a type annotation. We no longer need +to explicitly refer to the Canonical Forms lemma, since it +is built-in to the definition of value. +\begin{code} progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M progress (` ()) -progress (ƛ N) = done V-ƛ +progress (ƛ N) = done V-ƛ progress (L · M) with progress L -... | step L—→L′ = step (ξ-·₁ L—→L′) +... | step L—→L′ = step (ξ-·₁ L—→L′) ... | done V-ƛ with progress M -... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′) -... | done VM = step (β-ƛ VM) -progress (`zero) = done V-zero +... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′) +... | done VM = step (β-ƛ VM) +progress (`zero) = done V-zero progress (`suc M) with progress M -... | step M—→M′ = step (ξ-suc M—→M′) -... | done VM = done (V-suc VM) +... | step M—→M′ = step (ξ-suc M—→M′) +... | done VM = done (V-suc VM) progress (`case L M N) with progress L -... | step L—→L′ = step (ξ-case L—→L′) -... | done V-zero = step (β-zero) -... | done (V-suc VL) = step (β-suc VL) -progress (μ N) = step (β-μ) +... | step L—→L′ = step (ξ-case L—→L′) +... | done V-zero = step (β-zero) +... | done (V-suc VL) = step (β-suc VL) +progress (μ N) = step (β-μ) \end{code} ## Evaluation -By analogy, we will use the name _gas_ for the parameter which puts a -bound on the number of reduction steps. Gas is specified by a natural number. +Before, we combined progress and preservation to evaluate a term. +We can do much the same here, but we no longer need to explicitly +refer to preservation, since it is built-in to the definition of reduction. + +As previously, gas is specified by a natural number. \begin{code} data Gas : Set where gas : ℕ → Gas @@ -1081,8 +1093,7 @@ data Steps : ∀ {A} → ∅ ⊢ A → Set where ---------- → Steps L \end{code} -The evaluator takes gas and evidence that a term is well-typed, -and returns the corresponding steps. +The evaluator takes gas and a term and returns the corresponding steps. \begin{code} eval : ∀ {A} → Gas @@ -1093,8 +1104,9 @@ eval (gas zero) L = steps (L ∎) out-of-gas eval (gas (suc m)) L with progress L ... | done VL = steps (L ∎) (done VL) ... | step {M} L—→M with eval (gas m) M -... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin +... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin \end{code} +The definition is mu ## Examples diff --git a/src/plta/Lambda.lagda b/src/plta/Lambda.lagda index 0ee7bbdc..51fb2dc7 100644 --- a/src/plta/Lambda.lagda +++ b/src/plta/Lambda.lagda @@ -422,35 +422,6 @@ N ⟨ x ⟩[ y := V ] with x ≟ y [zero⇒ M [ y := V ] |suc x ⇒ N ⟨ x ⟩[ y := V ] ] (μ x ⇒ N) [ y := V ] = μ x ⇒ (N ⟨ x ⟩[ y := V ]) - - -{- -infix 9 _[_:=_] - -_[_:=_] : Term → Id → Term → Term -(` x) [ y := V ] with x ≟ y -... | yes _ = V -... | no _ = ` x -(ƛ x ⇒ N) [ y := V ] with x ≟ y -... | yes _ = ƛ x ⇒ N -... | no _ = ƛ x ⇒ (N [ y := V ]) -(L · M) [ y := V ] = (L [ y := V ]) · (M [ y := V ]) -(`zero) [ y := V ] = `zero -(`suc M) [ y := V ] = `suc (M [ y := V ]) -(`case L - [zero⇒ M - |suc x ⇒ N ]) - [ y := V ] with x ≟ y -... | yes _ = `case L [ y := V ] - [zero⇒ M [ y := V ] - |suc x ⇒ N ] -... | no _ = `case L [ y := V ] - [zero⇒ M [ y := V ] - |suc x ⇒ N [ y := V ] ] -(μ x ⇒ N) [ y := V ] with x ≟ y -... | yes _ = μ x ⇒ N -... | no _ = μ x ⇒ (N [ y := V ]) --} \end{code} Let's unpack the first three cases. diff --git a/src/plta/Properties.lagda b/src/plta/Properties.lagda index 4a02bc98..a8f723bb 100644 --- a/src/plta/Properties.lagda +++ b/src/plta/Properties.lagda @@ -243,7 +243,7 @@ A term `M` makes progress if either it can take a step, meaning there exists a term `N` such that `M —→ N`, or if it is done, meaning that `M` is a value. -If a term is well-typed in the empty context then it is a value. +If a term is well-typed in the empty context then it satisfies progress. \begin{code} progress : ∀ {M A} → ∅ ⊢ M ⦂ A @@ -580,6 +580,7 @@ we require an arbitrary context `Γ`, as in the statement of the lemma. Here is the formal statement and proof that substitution preserves types. \begin{code} subst : ∀ {Γ y N V A B} + → ∅ ⊢ V ⦂ B → Γ , y ⦂ B ⊢ N ⦂ A -------------------- → Γ ⊢ N [ y := V ] ⦂ A @@ -614,45 +615,6 @@ substvar {x = x} {y = y} ⊢V (S x≢y ∋x) with x ≟ y substbind {x = x} {y = y} ⊢V ⊢N with x ≟ y ... | yes refl = drop ⊢N ... | no x≢y = subst ⊢V (swap x≢y ⊢N) - -{- -subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y -... | yes refl = ⊢ƛ (drop ⊢N) -... | no x≢y = ⊢ƛ (subst ⊢V (swap x≢y ⊢N)) -subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y -... | yes refl = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N) -... | no x≢y = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N)) -subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y -... | yes refl = ⊢μ (drop ⊢M) -... | no x≢y = ⊢μ (subst ⊢V (swap x≢y ⊢M)) --} - - -{- -subst : ∀ {Γ x N V A B} - → ∅ ⊢ V ⦂ A - → Γ , x ⦂ A ⊢ N ⦂ B - -------------------- - → Γ ⊢ N [ x := V ] ⦂ B -subst {x = y} ⊢V (⊢` {x = x} Z) with x ≟ y -... | yes refl = weaken ⊢V -... | no x≢y = ⊥-elim (x≢y refl) -subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∋x)) with x ≟ y -... | yes refl = ⊥-elim (x≢y refl) -... | no _ = ⊢` ∋x -subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y -... | yes refl = ⊢ƛ (drop ⊢N) -... | no x≢y = ⊢ƛ (subst ⊢V (swap x≢y ⊢N)) -subst ⊢V (⊢L · ⊢M) = subst ⊢V ⊢L · subst ⊢V ⊢M -subst ⊢V ⊢zero = ⊢zero -subst ⊢V (⊢suc ⊢M) = ⊢suc (subst ⊢V ⊢M) -subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y -... | yes refl = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N) -... | no x≢y = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N)) -subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y -... | yes refl = ⊢μ (drop ⊢M) -... | no x≢y = ⊢μ (subst ⊢V (swap x≢y ⊢M)) --} \end{code} We induct on the evidence that `N` is well-typed in the context `Γ` extended by `x`. @@ -966,11 +928,11 @@ eval : ∀ {L A} → ∅ ⊢ L ⦂ A --------- → Steps L -eval {L} (gas zero) ⊢L = steps (L ∎) out-of-gas +eval {L} (gas zero) ⊢L = steps (L ∎) out-of-gas eval {L} (gas (suc m)) ⊢L with progress ⊢L -... | done VL = steps (L ∎) (done VL) +... | done VL = steps (L ∎) (done VL) ... | step L—→M with eval (gas m) (preserve ⊢L L—→M) -... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin +... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin \end{code} Let `L` be the name of the term we are reducing, and `⊢L` be the evidence that `L` is well-typed. We consider the amount of gas @@ -1367,11 +1329,11 @@ wttdgs′ ⊢M M—↠N = unstuck′ (preserves′ ⊢M M—↠N) ## Reduction is deterministic -When we introduced reduction, we claimed it was deterministic: -for any term, there is at most one other term to which it reduces. +When we introduced reduction, we claimed it was deterministic. +For completeness, we present a formal proof here. A case term takes four arguments (three subterms and a bound -variable), and to complete our proof we will need a variant +variable), and our proof will need a variant of congruence to deal with functions of four arguments. It is exactly analogous to `cong` and `cong₂` as defined previously. \begin{code}