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

inductive data type for progress

Browse source
This commit is contained in:
wadler 2017-06-29 23:05:23 +01:00
parent 5c02a1a5cb
commit ec46d635c0
4 changed files with 3995 additions and 4195 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
out/Stlc.md
View file

@ -4100,36 +4100,35 @@ Example terms.
Construction of a type derivation is best done interactively. Construction of a type derivation is best done interactively.
We start with the declaration: We start with the declaration:
`typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
`typing₁ = ?` typing₁ = ?
Typing control-L causes Agda to create a hole and tell us its expected type. Typing C-L (control L) causes Agda to create a hole and tell us its
expected type.
`typing₁ = { }0` typing₁ = { }0
`?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` ?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
Now we fill in the hole, observing that the outermost term in `not` in a `λ`, Now we fill in the hole by typing C-R (control R). Agda observes that
which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The
we again specify with a hole. `⇒-I` rule in turn takes one argument, which Agda leaves as a hole.
`typing₁ = ⇒-I { }0` typing₁ = ⇒-I { }0
`?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹` ?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹
Again we fill in the hole, observing that the outermost term is now Again we fill in the hole by typing C-R. Agda observes that the
`if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
three arguments, which we again specify with holes. `𝔹-E` rule in turn takes three arguments, which Agda leaves as holes.
`typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2)` typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2)
`?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ 𝔹` ?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶
`?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹` ?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹
`?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹` ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹
Again we fill in the three holes, observing that `var x`, `false`, and `true`
are typed using `Ax`, `𝔹-I₂`, and `𝔹-I₁` respectively. The `Ax` rule in turn
takes an argument, to show that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn
be computed with a hole.
Filling in the three holes gives the derivation above.
Again we fill in the three holes by typing C-R in each. Agda observes
that `var x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a
hole. After filling in all holes, the term is as above.

8012
out/StlcProp.md
View file

File diff suppressed because it is too large Load diff

47
src/Stlc.lagda
View file

@ -206,36 +206,35 @@ typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
Construction of a type derivation is best done interactively. Construction of a type derivation is best done interactively.
We start with the declaration: We start with the declaration:
`typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
`typing₁ = ?` typing₁ = ?
Typing control-L causes Agda to create a hole and tell us its expected type. Typing C-L (control L) causes Agda to create a hole and tell us its
expected type.
`typing₁ = { }0` typing₁ = { }0
`?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` ?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
Now we fill in the hole, observing that the outermost term in `not` in a `λ`, Now we fill in the hole by typing C-R (control R). Agda observes that
which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The
we again specify with a hole. `⇒-I` rule in turn takes one argument, which Agda leaves as a hole.
`typing₁ = ⇒-I { }0` typing₁ = ⇒-I { }0
`?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹` ?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹
Again we fill in the hole, observing that the outermost term is now Again we fill in the hole by typing C-R. Agda observes that the
`if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
three arguments, which we again specify with holes. `𝔹-E` rule in turn takes three arguments, which Agda leaves as holes.
`typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2)` typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2)
`?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ 𝔹` ?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶
`?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹` ?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹
`?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹` ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹
Again we fill in the three holes, observing that `var x`, `false`, and `true`
are typed using `Ax`, `𝔹-I₂`, and `𝔹-I₁` respectively. The `Ax` rule in turn
takes an argument, to show that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn
be computed with a hole.
Filling in the three holes gives the derivation above.
Again we fill in the three holes by typing C-R in each. Agda observes
that `var x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a
hole. After filling in all holes, the term is as above.

84
src/StlcProp.lagda
View file

@ -39,7 +39,7 @@ data canonical_for_ : Term → Type → Set where
canonical-false : canonical false for 𝔹 canonical-false : canonical false for 𝔹
canonicalFormsLemma : ∀ {L A} → ∅ ⊢ L ∶ A → Value L → canonical L for A canonicalFormsLemma : ∀ {L A} → ∅ ⊢ L ∶ A → Value L → canonical L for A
canonicalFormsLemma (Ax ⊢x) () canonicalFormsLemma (Ax ()) ()
canonicalFormsLemma (⇒-I ⊢N) value-λ = canonical-λ canonicalFormsLemma (⇒-I ⊢N) value-λ = canonical-λ
canonicalFormsLemma (⇒-E ⊢L ⊢M) () canonicalFormsLemma (⇒-E ⊢L ⊢M) ()
canonicalFormsLemma 𝔹-I₁ value-true = canonical-true canonicalFormsLemma 𝔹-I₁ value-true = canonical-true
@ -50,11 +50,15 @@ canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) ()
## Progress ## Progress
As before, the _progress_ theorem tells us that closed, well-typed As before, the _progress_ theorem tells us that closed, well-typed
terms are not stuck: either a well-typed term is a value, or it terms are not stuck: either a well-typed term can take a reduction
can take a reduction step. step or it is a value.
\begin{code} \begin{code}
progress : ∀ {M A} → ∅ ⊢ M ∶ A → Value M ⊎ ∃ λ N → M ⟹ N data Progress : Term → Set where
steps : ∀ {M N} → M ⟹ N → Progress M
done : ∀ {M} → Value M → Progress M
progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M
\end{code} \end{code}
The proof is a relatively The proof is a relatively
@ -74,52 +78,54 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
- If the last rule of the derivation is `⇒-E`, then the term has the - If the last rule of the derivation is `⇒-E`, then the term has the
form `L · M` for some `L` and `M`, where we know that `L` and `M` form `L · M` for some `L` and `M`, where we know that `L` and `M`
are also well typed in the empty context, giving us two induction are also well typed in the empty context, giving us two induction
hypotheses. By the first induction hypothesis, either `L` is a hypotheses. By the first induction hypothesis, either `L`
value or it can take a step. can take a step or is a value.
- If `L` is a value then consider `M`. By the second induction
hypothesis, either `M` is a value or it can take a step.
- If `M` is a value, then since `L` is a value with a
function type we know it must be a lambda abstraction,
and hence `L · M` can take a step by `β⇒`.
- If `M` can take a step, then so can `L · M` by `γ⇒₂`.
- If `L` can take a step, then so can `L · M` by `γ⇒₁`. - If `L` can take a step, then so can `L · M` by `γ⇒₁`.
- If `L` is a value then consider `M`. By the second induction
hypothesis, either `M` can take a step or is a value.
- If `M` can take a step, then so can `L · M` by `γ⇒₂`.
- If `M` is a value, then since `L` is a value with a
function type we know from the canonical forms lemma
that it must be a lambda abstraction,
and hence `L · M` can take a step by `β⇒`.
- If the last rule of the derivation is `𝔹-E`, then the term has - If the last rule of the derivation is `𝔹-E`, then the term has
the form `if L then M else N` where `L` has type `𝔹`. the form `if L then M else N` where `L` has type `𝔹`.
By the induction hypothesis, either `L` is a value or it can By the induction hypothesis, either `L` can take a step or is
take a step. a value.
- If `L` is a value, then since it has type boolean it must be
either `true` or `false`.
- If `L` is `true`, then then term steps by `β𝔹₁`
- If `L` is `false`, then then term steps by `β𝔹₂`
- If `L` can take a step, then so can `if L then M else N` by `γ𝔹`. - If `L` can take a step, then so can `if L then M else N` by `γ𝔹`.
- If `L` is a value, then since it has type boolean we know from
the canonical forms lemma that it must be either `true` or
`false`.
- If `L` is `true`, then `if L then M else N` steps by `β𝔹₁`
- If `L` is `false`, then `if L then M else N` steps by `β𝔹₂`
This completes the proof. This completes the proof.
\begin{code} \begin{code}
progress (Ax ()) progress (Ax ())
progress (⇒-I ⊢N) = inj₁ value-λ progress (⇒-I ⊢N) = done value-λ
progress (⇒-E {Γ} {L} {M} {A} {B} ⊢L ⊢M) with progress ⊢L progress (⇒-E ⊢L ⊢M) with progress ⊢L
... | inj₂ (L′ , L⟹L′) = inj₂ (L′ · M , γ⇒₁ L⟹L′) ... | steps L⟹L′ = steps (γ⇒₁ L⟹L′)
... | inj₁ valueL with progress ⊢M ... | done valueL with progress ⊢M
... | inj₂ (M′ , M⟹M′) = inj₂ (L · M′ , γ⇒₂ valueL M⟹M′) ... | steps M⟹M′ = steps (γ⇒₂ valueL M⟹M′)
... | inj₁ valueM with canonicalFormsLemma ⊢L valueL ... | done valueM with canonicalFormsLemma ⊢L valueL
... | canonical-λ {x} {.A} {N} {.B} = inj₂ ((N [ x ∶= M ]) , β⇒ valueM) ... | canonical-λ = steps (β⇒ valueM)
progress 𝔹-I₁ = inj₁ value-true progress 𝔹-I₁ = done value-true
progress 𝔹-I₂ = inj₁ value-false progress 𝔹-I₂ = done value-false
progress (𝔹-E {Γ} {L} {M} {N} {A} ⊢L ⊢M ⊢N) with progress ⊢L progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
... | inj₂ (L′ , L⟹L′) = inj₂ ((if L′ then M else N) , γ𝔹 L⟹L′) ... | steps L⟹L′ = steps (γ𝔹 L⟹L′)
... | inj₁ valueL with canonicalFormsLemma ⊢L valueL ... | done valueL with canonicalFormsLemma ⊢L valueL
... | canonical-true = inj₂ (M , β𝔹₁) ... | canonical-true = steps β𝔹₁
... | canonical-false = inj₂ (N , β𝔹₂) ... | canonical-false = steps β𝔹₂
\end{code} \end{code}
#### Exercise: 3 stars, optional (progress_from_term_ind) #### Exercise: 3 stars, optional (progress_from_term_ind)
@ -128,7 +134,7 @@ instead of induction on typing derivations.
\begin{code} \begin{code}
postulate postulate
progress′ : ∀ {M A} → ∅ ⊢ M ∶ A → Value M ⊎ ∃ λ N → M ⟹ N progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
\end{code} \end{code}
## Preservation ## Preservation