michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

saved old substitution in extra

Browse source
This commit is contained in:
wadler 2018-07-02 19:18:44 -03:00
parent 83975bc8e1
commit fb2c3ab076
4 changed files with 85 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
extra/extra/OldSubstitution.lagda Normal file
View file

@ -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))

44
src/plta/DeBruijn.lagda
View file

@ -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

29
src/plta/Lambda.lagda
View file

@ -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.

54
src/plta/Properties.lagda
View file

@ -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}