completed draft of PandP
This commit is contained in:
wadler
parent
ec55c30779
commit
2c570407e4
1 changed files with 141 additions and 182 deletions
|
|
@ -853,28 +853,28 @@ data Gas : Set where
|
|||
When our evaluator returns a term `N`, it will either give evidence that
|
||||
`N` is a value or indicate that it ran out of gas.
|
||||
\begin{code}
|
||||
data Done? (N : Term) : Set where
|
||||
data Finished (N : Term) : Set where
|
||||
done :
|
||||
Value N
|
||||
-------
|
||||
→ Done? N
|
||||
----------
|
||||
→ Finished N
|
||||
|
||||
out-of-gas :
|
||||
-------
|
||||
Done? N
|
||||
----------
|
||||
Finished N
|
||||
\end{code}
|
||||
Given a term `M` of type `A`, the evaluator will, for some `N`, return
|
||||
a reduction sequence from `M` to `N` along with evidence that `N` is
|
||||
well-typed and an indication of whether reduction completed.
|
||||
Given a term `L` of type `A`, the evaluator will, for some `N`, return
|
||||
a reduction sequence from `L` to `N` along with evidence that `N` is
|
||||
well-typed and an indication of whether reduction finished.
|
||||
\begin{code}
|
||||
data Eval (M : Term) (A : Type) : Set where
|
||||
data Steps (L : Term) (A : Type) : Set where
|
||||
|
||||
steps : ∀ {N}
|
||||
→ M ⟶* N
|
||||
→ L ⟶* N
|
||||
→ ∅ ⊢ N ⦂ A
|
||||
→ Done? N
|
||||
--------
|
||||
→ Eval M A
|
||||
→ Finished N
|
||||
----------
|
||||
→ Steps L A
|
||||
\end{code}
|
||||
The evaluator takes gas and evidence that a term is well-typed,
|
||||
and returns the result of evaluating that term for a number of
|
||||
|
|
@ -884,12 +884,12 @@ eval : ∀ {L A}
|
|||
→ Gas
|
||||
→ ∅ ⊢ L ⦂ A
|
||||
---------
|
||||
→ Eval L A
|
||||
eval {L} (gas zero) ⊢L = steps (L ∎) ⊢L out-of-gas
|
||||
→ Steps L A
|
||||
eval {L} (gas zero) ⊢L = steps (L ∎) ⊢L out-of-gas
|
||||
eval {L} (gas (suc m)) ⊢L with progress ⊢L
|
||||
... | done VL = steps (L ∎) ⊢L (done VL)
|
||||
... | step L⟶M with normalise (gas m) (preserve ⊢L L⟶M)
|
||||
... | steps M⟶*N ⊢N done? = steps (L ⟶⟨ L⟶M ⟩ M⟶*N) ⊢N done?
|
||||
... | done VL = steps (L ∎) ⊢L (done VL)
|
||||
... | step L⟶M with eval (gas m) (preserve ⊢L L⟶M)
|
||||
... | steps M⟶*N ⊢N fin = steps (L ⟶⟨ L⟶M ⟩ M⟶*N) ⊢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
|
||||
|
|
@ -909,51 +909,20 @@ remaining. There are two possibilities.
|
|||
|
||||
+ Term `L` steps to another term `M`. Preservation provides
|
||||
evidence that `M` is also well-typed, and we recursively invoke
|
||||
`eval` on the remaining gas. The result will be another term
|
||||
`N` such that `M ⟶* N` and `N` is well-typed plus an indication
|
||||
of how reduction terminated. We combine the evidence that `L ⟶ M`
|
||||
and `M ⟶* N` to return evidence that `L ⟶* N`, together with
|
||||
the evidence that `N` is well-typed and the indication of how
|
||||
reduction termination.
|
||||
`eval` on the remaining gas. The result is evidence that
|
||||
`M ⟶* N`, together with evidence that `N` is well-typed and an
|
||||
indication of whether reduction finished. We combine the evidence
|
||||
that `L ⟶ M` and `M ⟶* N` to return evidence that `L ⟶* N`,
|
||||
together with the other relevant evidence.
|
||||
|
||||
|
||||
\begin{code}
|
||||
{-
|
||||
data Normalise (M : Term) : Set where
|
||||
|
||||
out-of-gas : ∀ {N A}
|
||||
→ M ⟶* N
|
||||
→ ∅ ⊢ N ⦂ A
|
||||
-------------
|
||||
→ Normalise M
|
||||
|
||||
normal : ∀ {V}
|
||||
→ Gas
|
||||
→ M ⟶* V
|
||||
→ Value V
|
||||
--------------
|
||||
→ Normalise M
|
||||
|
||||
normalise : ∀ {M A}
|
||||
→ Gas
|
||||
→ ∅ ⊢ M ⦂ A
|
||||
-----------
|
||||
→ Normalise M
|
||||
normalise {L} zero ⊢L = out-of-gas (L ∎) ⊢L
|
||||
normalise {L} (suc m) ⊢L with progress ⊢L
|
||||
... | done VL = normal (suc m) (L ∎) VL
|
||||
... | step L⟶M with normalise m (preserve ⊢L L⟶M)
|
||||
... | out-of-gas M⟶*N ⊢N = out-of-gas (L ⟶⟨ L⟶M ⟩ M⟶*N) ⊢N
|
||||
... | normal n M⟶*V VV = normal n (L ⟶⟨ L⟶M ⟩ M⟶*V) VV
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
### Examples
|
||||
|
||||
We can now use Agda to compute the reduction sequence for two plus two
|
||||
given in the preceding chapter.
|
||||
\begin{code}
|
||||
{-
|
||||
_ : normalise 100 ⊢four ≡
|
||||
normal 88
|
||||
_ : eval (gas 100) ⊢four ≡
|
||||
steps
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
|
|
@ -1107,13 +1076,20 @@ _ : normalise 100 ⊢four ≡
|
|||
· `suc (`suc `zero))
|
||||
])
|
||||
⟶⟨ ξ-suc (ξ-suc β-case-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎)
|
||||
(V-suc (V-suc (V-suc (V-suc V-zero))))
|
||||
(⊢suc (⊢suc (⊢suc (⊢suc ⊢zero))))
|
||||
(done (V-suc (V-suc (V-suc (V-suc V-zero)))))
|
||||
_ = refl
|
||||
\end{code}
|
||||
The example above was generated by using ^C ^N to normalise the
|
||||
left-hand side of the equation and pasting in the result as the
|
||||
right-hand side of the equation. The result was then edited to give
|
||||
the example reduction of the previous chapter, by writing `plus`
|
||||
and `two` in place of the corresponding terms and reformatting.
|
||||
|
||||
Similarly, can evaluate the corresponding term for Church numerals.
|
||||
\begin{code}
|
||||
_ : normalise 100 ⊢fourᶜ ≡
|
||||
normal 88
|
||||
_ : eval (gas 100) ⊢fourᶜ ≡
|
||||
steps
|
||||
((ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
(ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "m" ⌋ · ⌊ "s" ⌋ · (⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋)))))
|
||||
|
|
@ -1172,89 +1148,126 @@ _ : normalise 100 ⊢fourᶜ ≡
|
|||
(ƛ "n" ⇒ `suc ⌊ "n" ⌋) · `suc (`suc (`suc `zero)) ⟶⟨
|
||||
β-ƛ· (V-suc (V-suc (V-suc V-zero))) ⟩
|
||||
`suc (`suc (`suc (`suc `zero))) ∎)
|
||||
(V-suc (V-suc (V-suc (V-suc V-zero))))
|
||||
(⊢suc (⊢suc (⊢suc (⊢suc ⊢zero))))
|
||||
(done (V-suc (V-suc (V-suc (V-suc V-zero)))))
|
||||
_ = refl
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
We can also derive the non-terminating example.
|
||||
\begin{code}
|
||||
⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ⌊ "x" ⌋ ⦂ `ℕ
|
||||
⊢sucμ = ⊢μ (⊢suc (Ax ∋x))
|
||||
where
|
||||
∋x = Z
|
||||
|
||||
_ : eval (gas 3) ⊢sucμ ≡
|
||||
steps
|
||||
(μ "x" ⇒ `suc ⌊ "x" ⌋ Chain.⟶⟨ β-μ ⟩
|
||||
`suc (μ "x" ⇒ `suc ⌊ "x" ⌋) Chain.⟶⟨ ξ-suc β-μ ⟩
|
||||
`suc (`suc (μ "x" ⇒ `suc ⌊ "x" ⌋)) Chain.⟶⟨ ξ-suc (ξ-suc β-μ) ⟩
|
||||
`suc (`suc (`suc (μ "x" ⇒ `suc ⌊ "x" ⌋))) Chain.∎)
|
||||
(⊢suc (⊢suc (⊢suc (⊢μ (⊢suc (Ax Z)))))) out-of-gas
|
||||
_ = refl
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise: 2 stars, recommended (subject_expansion_stlc)
|
||||
|
||||
<!--
|
||||
An exercise in the [Types]({{ "Types" | relative_url }}) chapter asked about the
|
||||
subject expansion property for the simple language of arithmetic and boolean
|
||||
expressions. Does this property hold for STLC? That is, is it always the case
|
||||
that, if `M ==> N` and `∅ ⊢ N ⦂ A`, then `∅ ⊢ M ⦂ A`? It is easy to find a
|
||||
counter-example with conditionals, find one not involving conditionals.
|
||||
-->
|
||||
#### Exercise `subject_expansion`
|
||||
|
||||
We say that `M` _reduces_ to `N` if `M ⟶ N`,
|
||||
and that `M` _expands_ to `N` if `N ⟶ M`.
|
||||
and conversely that `M` _expands_ to `N` if `N ⟶ M`.
|
||||
The preservation property is sometimes called _subject reduction_.
|
||||
Its opposite is _subject expansion_, which holds if
|
||||
`M ==> N` and `∅ ⊢ N ⦂ A`, then `∅ ⊢ M ⦂ A`.
|
||||
`M ==> N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
|
||||
Find two counter-examples to subject expansion, one
|
||||
with case expressions and one not involving case expressions.
|
||||
|
||||
## Type Soundness
|
||||
|
||||
#### Exercise: 2 stars, optional (type_soundness)
|
||||
|
||||
Put progress and preservation together and show that a well-typed
|
||||
term can _never_ reach a stuck state.
|
||||
## Well-typed terms don't get stuck
|
||||
|
||||
A term is _normal_ if it cannot reduce.
|
||||
\begin{code}
|
||||
Normal : Term → Set
|
||||
Normal M = ∀ {N} → ¬ (M ⟶ N)
|
||||
Normal M = ∀ {N} → ¬ (M ⟶ N)
|
||||
\end{code}
|
||||
|
||||
A term is _stuck_ if it is normal yet not a value.
|
||||
\begin{code}
|
||||
Stuck : Term → Set
|
||||
Stuck M = Normal M × ¬ Value M
|
||||
Stuck M = Normal M × ¬ Value M
|
||||
\end{code}
|
||||
|
||||
Using progress and preservation, it is easy to show that well-typed terms don't get stuck.
|
||||
\begin{code}
|
||||
postulate
|
||||
Soundness : ∀ {M N A}
|
||||
wttdgs : ∀ {M N A}
|
||||
→ ∅ ⊢ M ⦂ A
|
||||
→ M ⟶* N
|
||||
-----------
|
||||
→ ¬ (Stuck N)
|
||||
→ ¬ (Stuck M)
|
||||
\end{code}
|
||||
|
||||
#### Exercise `stuck`
|
||||
|
||||
Give an example of a not well-typed term that does get stuck.
|
||||
|
||||
#### Exercise `wttdgs`
|
||||
|
||||
Show that if a term is well-typed it is not stuck,
|
||||
and that any descendant of a well-typed term is also well-typed.
|
||||
Combine these results to show `wttdgs`.
|
||||
|
||||
<div class="hidden">
|
||||
If a term is well-typed, it does not get stuck.
|
||||
\begin{code}
|
||||
Soundness′ : ∀ {M N A}
|
||||
unstuck : ∀ {M A}
|
||||
→ ∅ ⊢ M ⦂ A
|
||||
-----------
|
||||
→ ¬ (Stuck M)
|
||||
unstuck ⊢M ⟨ ¬M⟶N , ¬VM ⟩ with progress ⊢M
|
||||
... | step M⟶N = ¬M⟶N M⟶N
|
||||
... | done VM = ¬VM VM
|
||||
\end{code}
|
||||
|
||||
Any descendant of a well-typed term is well-typed.
|
||||
\begin{code}
|
||||
preserve* : ∀ {M N A}
|
||||
→ ∅ ⊢ M ⦂ A
|
||||
→ M ⟶* N
|
||||
---------
|
||||
→ ∅ ⊢ N ⦂ A
|
||||
preserve* ⊢M (M ∎) = ⊢M
|
||||
preserve* ⊢L (L ⟶⟨ L⟶M ⟩ M⟶*N) = preserve* (preserve ⊢L L⟶M) M⟶*N
|
||||
\end{code}
|
||||
|
||||
Combining the above gives us the desired result.
|
||||
\begin{code}
|
||||
wttdgs′ : ∀ {M N A}
|
||||
→ ∅ ⊢ M ⦂ A
|
||||
→ M ⟶* N
|
||||
-----------
|
||||
→ ¬ (Stuck N)
|
||||
Soundness′ ⊢M (M ∎) ⟨ ¬M⟶N , ¬VM ⟩ with progress ⊢M
|
||||
... | step M⟶N = ¬M⟶N M⟶N
|
||||
... | done VM = ¬VM VM
|
||||
Soundness′ ⊢L (L ⟶⟨ L⟶M ⟩ M⟶*N) = Soundness′ (preserve ⊢L L⟶M) M⟶*N
|
||||
wttdgs′ ⊢M M⟶*N = unstuck (preserve* ⊢M M⟶*N)
|
||||
\end{code}
|
||||
</div>
|
||||
|
||||
|
||||
## Additional Exercises
|
||||
|
||||
#### Exercise: 1 star (progress_preservation_statement)
|
||||
#### Exercise: `progress-preservation`
|
||||
|
||||
Without peeking at their statements above, write down the progress
|
||||
and preservation theorems for the simply typed lambda-calculus.
|
||||
|
||||
#### Exercise: 2 stars (stlc_variation1)
|
||||
|
||||
#### Quiz
|
||||
|
||||
Suppose we add a new term `zap` with the following reduction rule
|
||||
|
||||
--------- (ST_Zap)
|
||||
M ⟶ zap
|
||||
--------- β-zap
|
||||
M ⟶ zap
|
||||
|
||||
and the following typing rule:
|
||||
|
||||
----------- (T_Zap)
|
||||
Γ ⊢ zap : A
|
||||
----------- ⊢zap
|
||||
Γ ⊢ zap ⦂ A
|
||||
|
||||
Which of the following properties of the STLC remain true in
|
||||
Which of the following properties remain true in
|
||||
the presence of these rules? For each property, write either
|
||||
"remains true" or "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
|
@ -1266,18 +1279,18 @@ false, give a counterexample.
|
|||
- Preservation
|
||||
|
||||
|
||||
#### Exercise: 2 stars (stlc_variation2)
|
||||
#### Quiz
|
||||
|
||||
Suppose instead that we add a new term `foo` with the following
|
||||
reduction rules:
|
||||
|
||||
------------------- (Foo₁)
|
||||
(λ x ⇒ ⌊ x ⌋) ⟶ foo
|
||||
--------------------- β-foo₁
|
||||
(λ x ⇒ ⌊ x ⌋) ⟶ foo
|
||||
|
||||
------------ (Foo₂)
|
||||
foo ⟶ true
|
||||
------------ β-foo₂
|
||||
foo ⟶ zero
|
||||
|
||||
Which of the following properties of the STLC remain true in
|
||||
Which of the following properties remain true in
|
||||
the presence of this rule? For each one, write either
|
||||
"remains true" or else "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
|
@ -1288,10 +1301,11 @@ false, give a counterexample.
|
|||
|
||||
- Preservation
|
||||
|
||||
#### Exercise: 2 stars (stlc_variation3)
|
||||
|
||||
#### Quiz
|
||||
|
||||
Suppose instead that we remove the rule `ξ·₁` from the `⟶`
|
||||
relation. Which of the following properties of the STLC remain
|
||||
relation. Which of the following properties remain
|
||||
true in the absence of this rule? For each one, write either
|
||||
"remains true" or else "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
|
@ -1302,14 +1316,28 @@ false, give a counterexample.
|
|||
|
||||
- Preservation
|
||||
|
||||
#### Exercise: 2 stars, optional (stlc_variation4)
|
||||
Suppose instead that we add the following new rule to the
|
||||
reduction relation:
|
||||
|
||||
---------------------------------------- (FunnyCaseZero)
|
||||
case zero [zero⇒ M |suc x ⇒ N ] ⟶ true
|
||||
#### Quiz
|
||||
|
||||
Which of the following properties of the STLC remain true in
|
||||
We can enumerate all the computable function from naturals to
|
||||
naturals, by writing out all programs of type `ℕ ⇒ `ℕ in
|
||||
lexical order. Write `fᵢ` for the `i`'th function in this list.
|
||||
|
||||
Say we add a typing rule that applies the above enumeration
|
||||
to interpret a natural as a function from naturals to naturals.
|
||||
|
||||
Γ ⊢ L ⦂ `ℕ
|
||||
Γ ⊢ M ⦂ `ℕ
|
||||
-------------- ⊢ℕ⇒ℕ
|
||||
Γ ⊢ L · M ⦂ `ℕ
|
||||
|
||||
And that we add the corresponding reduction rule.
|
||||
|
||||
fᵢ(m) → n
|
||||
--------- δ-ℕ⇒ℕ
|
||||
i · m → n
|
||||
|
||||
Which of the following properties remain true in
|
||||
the presence of this rule? For each one, write either
|
||||
"remains true" or else "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
|
@ -1320,72 +1348,3 @@ false, give a counterexample.
|
|||
|
||||
- Preservation
|
||||
|
||||
|
||||
#### Exercise: 2 stars, optional (stlc_variation5)
|
||||
|
||||
Suppose instead that we add the following new rule to the typing
|
||||
relation:
|
||||
|
||||
Γ ⊢ L ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
Γ ⊢ M ⦂ `ℕ
|
||||
------------------------------ (FunnyApp)
|
||||
Γ ⊢ L · M ⦂ `ℕ
|
||||
|
||||
Which of the following properties of the STLC remain true in
|
||||
the presence of this rule? For each one, write either
|
||||
"remains true" or else "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
|
||||
#### Exercise: 2 stars, optional (stlc_variation6)
|
||||
|
||||
Suppose instead that we add the following new rule to the typing
|
||||
relation:
|
||||
|
||||
Γ ⊢ L ⦂ `ℕ
|
||||
Γ ⊢ M ⦂ `ℕ
|
||||
--------------------- (FunnyApp')
|
||||
Γ ⊢ L · M ⦂ `ℕ
|
||||
|
||||
Which of the following properties of the STLC remain true in
|
||||
the presence of this rule? For each one, write either
|
||||
"remains true" or else "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
|
||||
#### Exercise : 2 stars, optional (stlc_variation7)
|
||||
|
||||
Suppose we add the following new rule to the typing relation
|
||||
of the STLC:
|
||||
|
||||
-------------------- (T_FunnyAbs)
|
||||
∅ ⊢ ƛ x ⇒ N ⦂ `ℕ
|
||||
|
||||
Which of the following properties of the STLC remain true in
|
||||
the presence of this rule? For each one, write either
|
||||
"remains true" or else "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue