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

fixed reduction arrows

Browse source
This commit is contained in:
wadler 2018-07-01 19:04:45 -03:00
parent 46fd91b60c
commit 41f5efe8ed
2 changed files with 219 additions and 216 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

182
src/plta/Lambda.lagda
View file

@ -345,9 +345,9 @@ operational semantics of function application.
For instance, we have For instance, we have
(ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) · sucᶜ · `zero (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) · sucᶜ · `zero
↦ —→
(ƛ "z" ⇒ sucᶜ · (sucᶜ · "z")) · `zero (ƛ "z" ⇒ sucᶜ · (sucᶜ · "z")) · `zero
↦ —→
sucᶜ · (sucᶜ · `zero) sucᶜ · (sucᶜ · `zero)
where we substitute `sucᶜ` for `` ` "s" `` and `` `zero `` for `` ` "z" `` where we substitute `sucᶜ` for `` ` "s" `` and `` `zero `` for `` ` "z" ``
@ -515,16 +515,16 @@ the argument for the variable in the abstraction.
In an informal presentation of the operational semantics, In an informal presentation of the operational semantics,
the rules for reduction of applications are written as follows. the rules for reduction of applications are written as follows.
L ↦ L′ L —→ L′
-------------- ξ-·₁ -------------- ξ-·₁
L · M ↦ L′ · M L · M —→ L′ · M
M ↦ M′ M —→ M′
-------------- ξ-·₂ -------------- ξ-·₂
V · M ↦ V · M′ V · M —→ V · M′
---------------------------- β-ƛ ---------------------------- β-ƛ
(ƛ x ⇒ N) · V ↦ N [ x := V ] (ƛ x ⇒ N) · V —→ N [ x := V ]
The Agda version of the rules below will be similar, except that universal The Agda version of the rules below will be similar, except that universal
quantifications are made explicit, and so are the predicates that indicate quantifications are made explicit, and so are the predicates that indicate
@ -549,48 +549,48 @@ the bound variable by the entire fixpoint term.
Here are the rules formalised in Agda. Here are the rules formalised in Agda.
\begin{code} \begin{code}
infix 4 _↦_ infix 4 _—→_
data _↦_ : Term → Term → Set where data _—→_ : Term → Term → Set where
ξ-·₁ : ∀ {L L′ M} ξ-·₁ : ∀ {L L′ M}
→ L ↦ L′ → L —→ L′
----------------- -----------------
→ L · M ↦ L′ · M → L · M —→ L′ · M
ξ-·₂ : ∀ {V M M′} ξ-·₂ : ∀ {V M M′}
→ Value V → Value V
→ M ↦ M′ → M —→ M′
----------------- -----------------
→ V · M ↦ V · M′ → V · M —→ V · M′
β-ƛ : ∀ {x N V} β-ƛ : ∀ {x N V}
→ Value V → Value V
------------------------------ ------------------------------
→ (ƛ x ⇒ N) · V ↦ N [ x := V ] → (ƛ x ⇒ N) · V —→ N [ x := V ]
ξ-suc : ∀ {M M′} ξ-suc : ∀ {M M′}
→ M ↦ M′ → M —→ M′
------------------ ------------------
→ `suc M ↦ `suc M′ → `suc M —→ `suc M′
ξ-case : ∀ {x L L′ M N} ξ-case : ∀ {x L L′ M N}
→ L ↦ L′ → L —→ L′
----------------------------------------------------------------- -----------------------------------------------------------------
→ `case L [zero⇒ M |suc x ⇒ N ] ↦ `case L′ [zero⇒ M |suc x ⇒ N ] → `case L [zero⇒ M |suc x ⇒ N ] —→ `case L′ [zero⇒ M |suc x ⇒ N ]
β-zero : ∀ {x M N} β-zero : ∀ {x M N}
---------------------------------------- ----------------------------------------
→ `case `zero [zero⇒ M |suc x ⇒ N ] ↦ M → `case `zero [zero⇒ M |suc x ⇒ N ] —→ M
β-suc : ∀ {x V M N} β-suc : ∀ {x V M N}
→ Value V → Value V
--------------------------------------------------- ---------------------------------------------------
→ `case `suc V [zero⇒ M |suc x ⇒ N ] ↦ N [ x := V ] → `case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ]
β-μ : ∀ {x M} β-μ : ∀ {x M}
------------------------------ ------------------------------
→ μ x ⇒ M ↦ M [ x := μ x ⇒ M ] → μ x ⇒ M —→ M [ x := μ x ⇒ M ]
\end{code} \end{code}
The reduction rules are carefully designed to ensure that subterms The reduction rules are carefully designed to ensure that subterms
@ -600,14 +600,14 @@ This is referred to as _call by value_ reduction.
Further, we have arranged that subterms are reduced in a Further, we have arranged that subterms are reduced in a
left-to-right order. This means that reduction is _deterministic_: left-to-right order. This means that reduction is _deterministic_:
for any term, there is at most one other term to which it reduces. for any term, there is at most one other term to which it reduces.
Put another way, our reduction relation `↦` is in fact a function. Put another way, our reduction relation `—→` is in fact a function.
#### Quiz #### Quiz
What does the following term step to? What does the following term step to?
(ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ↦ ??? (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") —→ ???
1. `` (ƛ "x" ⇒ ` "x") `` 1. `` (ƛ "x" ⇒ ` "x") ``
2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") `` 2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
@ -615,7 +615,7 @@ What does the following term step to?
What does the following term step to? What does the following term step to?
(ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ↦ ??? (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") —→ ???
1. `` (ƛ "x" ⇒ ` "x") `` 1. `` (ƛ "x" ⇒ ` "x") ``
2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") `` 2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
@ -623,7 +623,7 @@ What does the following term step to?
What does the following term step to? (Where `two` and `sucᶜ` are as defined above.) What does the following term step to? (Where `two` and `sucᶜ` are as defined above.)
two · sucᶜ · `zero ↦ ??? two · sucᶜ · `zero —→ ???
1. `` sucᶜ · (sucᶜ · `zero) `` 1. `` sucᶜ · (sucᶜ · `zero) ``
2. `` (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero `` 2. `` (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero ``
@ -634,72 +634,72 @@ What does the following term step to? (Where `two` and `sucᶜ` are as defined
A single step is only part of the story. In general, we wish to repeatedly A single step is only part of the story. In general, we wish to repeatedly
step a closed term until it reduces to a value. We do this by defining step a closed term until it reduces to a value. We do this by defining
the reflexive and transitive closure `↠` of the step relation `↦`. the reflexive and transitive closure `—↠` of the step relation `—→`.
We define reflexive and transitive closure as a sequence of zero or We define reflexive and transitive closure as a sequence of zero or
more steps of the underlying relation, along lines similar to that for more steps of the underlying relation, along lines similar to that for
reasoning about chains of equalities reasoning about chains of equalities
Chapter [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}). Chapter [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}).
\begin{code} \begin{code}
infix 2 _↠_ infix 2 _—↠_
infix 1 begin_ infix 1 begin_
infixr 2 _↦⟨_⟩_ infixr 2 _—→⟨_⟩_
infix 3 _∎ infix 3 _∎
data _↠_ : Term → Term → Set where data _—↠_ : Term → Term → Set where
_∎ : ∀ M _∎ : ∀ M
--------- ---------
→ M ↠ M → M —↠ M
_↦⟨_⟩_ : ∀ L {M N} _—→⟨_⟩_ : ∀ L {M N}
→ L ↦ M → L —→ M
→ M ↠ N → M —↠ N
--------- ---------
→ L ↠ N → L —↠ N
begin_ : ∀ {M N} → (M ↠ N) → (M ↠ N) begin_ : ∀ {M N} → (M —↠ N) → (M —↠ N)
begin M↠N = M↠N begin M—↠N = M—↠N
\end{code} \end{code}
We can read this as follows. We can read this as follows.
* From term `M`, we can take no steps, giving a step of type `M ↠ M`. * From term `M`, we can take no steps, giving a step of type `M —↠ M`.
It is written `M ∎`. It is written `M ∎`.
* From term `L` we can take a single of type `L ↦ M` followed by zero * From term `L` we can take a single of type `L —→ M` followed by zero
or more steps of type `M ↠ N`, giving a step of type `L ↠ N`. It is or more steps of type `M —↠ N`, giving a step of type `L —↠ N`. It is
written `L ↦⟨ L↦M ⟩ M↠N`, where `L↦M` and `M↠N` are steps of the written `L —→⟨ L—→M ⟩ M—↠N`, where `L—→M` and `M—↠N` are steps of the
appropriate type. appropriate type.
The notation is chosen to allow us to lay out example reductions in an The notation is chosen to allow us to lay out example reductions in an
appealing way, as we will see in the next section. appealing way, as we will see in the next section.
As alternative is to define reflexive and transitive closure directly, As alternative is to define reflexive and transitive closure directly,
as the smallest relation that includes `↦` and is also reflexive as the smallest relation that includes `—→` and is also reflexive
and transitive. We could do so as follows. and transitive. We could do so as follows.
\begin{code} \begin{code}
data _↠′_ : Term → Term → Set where data _—↠′_ : Term → Term → Set where
step : ∀ {M N} step : ∀ {M N}
→ M ↦ N → M —→ N
------ ------
→ M ↠′ N → M —↠′ N
refl : ∀ {M} refl : ∀ {M}
------ ------
→ M ↠′ M → M —↠′ M
trans : ∀ {L M N} trans : ∀ {L M N}
→ L ↠′ M → L —↠′ M
→ M ↠′ N → M —↠′ N
------ ------
→ L ↠′ N → L —↠′ N
\end{code} \end{code}
The three constructors specify, respectively, that `↠` includes `↦` The three constructors specify, respectively, that `—↠` includes `—→`
and is reflexive and transitive. and is reflexive and transitive.
It is a straightforward exercise to show the two are equivalent. It is a straightforward exercise to show the two are equivalent.
#### Exercise (`↠≃↠′`) #### Exercise (`—↠≃—↠′`)
Show that the two notions of reflexive and transitive closure Show that the two notions of reflexive and transitive closure
above are isomorphic. above are isomorphic.
@ -710,97 +710,97 @@ above are isomorphic.
We start with a simple example. The Church numeral two applied to the We start with a simple example. The Church numeral two applied to the
successor function and zero yields the natural number two. successor function and zero yields the natural number two.
\begin{code} \begin{code}
_ : twoᶜ · sucᶜ · `zero ↠ `suc `suc `zero _ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero
_ = _ =
begin begin
twoᶜ · sucᶜ · `zero twoᶜ · sucᶜ · `zero
↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
↦⟨ β-ƛ V-zero ⟩ —→⟨ β-ƛ V-zero ⟩
sucᶜ · (sucᶜ · `zero) sucᶜ · (sucᶜ · `zero)
↦⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩ —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
sucᶜ · `suc `zero sucᶜ · `suc `zero
↦⟨ β-ƛ (V-suc V-zero) ⟩ —→⟨ β-ƛ (V-suc V-zero) ⟩
`suc (`suc `zero) `suc (`suc `zero)
∎ ∎
\end{code} \end{code}
Here is a sample reduction demonstrating that two plus two is four. Here is a sample reduction demonstrating that two plus two is four.
\begin{code} \begin{code}
_ : plus · two · two ↠ `suc `suc `suc `suc `zero _ : plus · two · two —↠ `suc `suc `suc `suc `zero
_ = _ =
begin begin
plus · two · two plus · two · two
↦⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩ —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ "m" ⇒ ƛ "n" ⇒ (ƛ "m" ⇒ ƛ "n" ⇒
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two · two · two · two
↦⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩ —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒ (ƛ "n" ⇒
`case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) `case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two · two
↦⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩ —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
`case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ] `case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]
↦⟨ β-suc (V-suc V-zero) ⟩ —→⟨ β-suc (V-suc V-zero) ⟩
`suc (plus · `suc `zero · two) `suc (plus · `suc `zero · two)
↦⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩ —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc ((ƛ "m" ⇒ ƛ "n" ⇒ `suc ((ƛ "m" ⇒ ƛ "n" ⇒
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· `suc `zero · two) · `suc `zero · two)
↦⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩ —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc ((ƛ "n" ⇒ `suc ((ƛ "n" ⇒
`case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) `case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two) · two)
↦⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩ —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
`suc (`case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]) `suc (`case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
↦⟨ ξ-suc (β-suc V-zero) ⟩ —→⟨ ξ-suc (β-suc V-zero) ⟩
`suc `suc (plus · `zero · two) `suc `suc (plus · `zero · two)
↦⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩ —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒ `suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· `zero · two) · `zero · two)
↦⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩ —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc `suc ((ƛ "n" ⇒ `suc `suc ((ƛ "n" ⇒
`case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) `case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two) · two)
↦⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩ —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
`suc `suc (`case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]) `suc `suc (`case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
↦⟨ ξ-suc (ξ-suc β-zero) ⟩ —→⟨ ξ-suc (ξ-suc β-zero) ⟩
`suc (`suc (`suc (`suc `zero))) `suc (`suc (`suc (`suc `zero)))
∎ ∎
\end{code} \end{code}
And here is a similar sample reduction for Church numerals. And here is a similar sample reduction for Church numerals.
\begin{code} \begin{code}
_ : fourᶜ ↠ `suc `suc `suc `suc `zero _ : fourᶜ —↠ `suc `suc `suc `suc `zero
_ = _ =
begin begin
(ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z")) (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z"))
· twoᶜ · twoᶜ · sucᶜ · `zero · twoᶜ · twoᶜ · sucᶜ · `zero
↦⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩ —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
(ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (` "n" · ` "s" · ` "z")) (ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (` "n" · ` "s" · ` "z"))
· twoᶜ · sucᶜ · `zero · twoᶜ · sucᶜ · `zero
↦⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩ —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (twoᶜ · ` "s" · ` "z")) · sucᶜ · `zero (ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (twoᶜ · ` "s" · ` "z")) · sucᶜ · `zero
↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` "z")) · `zero (ƛ "z" ⇒ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` "z")) · `zero
↦⟨ β-ƛ V-zero ⟩ —→⟨ β-ƛ V-zero ⟩
twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero) twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero)
↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (twoᶜ · sucᶜ · `zero) (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (twoᶜ · sucᶜ · `zero)
↦⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩ —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · ((ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero) (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · ((ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero)
↦⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩ —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (sucᶜ · `zero)) (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (sucᶜ · `zero))
↦⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩ —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (`suc `zero)) (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (`suc `zero))
↦⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩ —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (`suc `suc `zero) (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (`suc `suc `zero)
↦⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩ —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
sucᶜ · (sucᶜ · `suc `suc `zero) sucᶜ · (sucᶜ · `suc `suc `zero)
↦⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩ —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
sucᶜ · (`suc `suc `suc `zero) sucᶜ · (`suc `suc `suc `zero)
↦⟨ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩ —→⟨ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
`suc (`suc (`suc (`suc `zero))) `suc (`suc (`suc (`suc `zero)))
∎ ∎
\end{code} \end{code}
@ -1267,16 +1267,16 @@ showing that it is well-typed.
This chapter uses the following unicode This chapter uses the following unicode
⇒ U+21D2: RIGHTWARDS DOUBLE ARROW (\=>) ⇒ U+21D2: RIGHTWARDS DOUBLE ARROW (\=>)
ƛ U+019B: LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-) ƛ U+019B: LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-)
· U+00B7: MIDDLE DOT (\cdot) · U+00B7: MIDDLE DOT (\cdot)
😇 U+1F607: SMILING FACE WITH HALO 😇 U+1F607: SMILING FACE WITH HALO
😈 U+1F608: SMILING FACE WITH HORNS 😈 U+1F608: SMILING FACE WITH HORNS
↦ U+21A6: RIGHTWARDS ARROW FROM BAR (\mapsto, \r-|) — U+2014: EM DASH (\em)
↠ U+21A0: RIGHTWARDS TWO HEADED ARROW (\rr-) ↠ U+21A0: RIGHTWARDS TWO HEADED ARROW (\rr-)
ξ U+03BE: GREEK SMALL LETTER XI (\Gx or \xi) ξ U+03BE: GREEK SMALL LETTER XI (\Gx or \xi)
β U+03B2: GREEK SMALL LETTER BETA (\Gb or \beta) β U+03B2: GREEK SMALL LETTER BETA (\Gb or \beta)
∋ U+220B: CONTAINS AS MEMBER (\ni) ∋ U+220B: CONTAINS AS MEMBER (\ni)
⊢ U+22A2: RIGHT TACK (\vdash or \|-) ⊢ U+22A2: RIGHT TACK (\vdash or \|-)
⦂ U+2982: Z NOTATION TYPE COLON (\:) ⦂ U+2982: Z NOTATION TYPE COLON (\:)

253
src/plta/Properties.lagda
View file

@ -48,7 +48,7 @@ Ultimately, we would like to show that we can keep reducing a term
until we reach a value. For instance, in the last chapter we showed until we reach a value. For instance, in the last chapter we showed
that two plust two is four, that two plust two is four,
plus · two · two ↠ `suc `suc `suc `suc `zero plus · two · two —↠ `suc `suc `suc `suc `zero
which was proved by a long chain of reductions, ending in the value which was proved by a long chain of reductions, ending in the value
on the right. Every term in the chain had the same type, `` `ℕ ``. on the right. Every term in the chain had the same type, `` `ℕ ``.
@ -59,7 +59,7 @@ a reduction step. As we will see, this property does _not_ hold for
every term, but it does hold for every closed, well-typed term. every term, but it does hold for every closed, well-typed term.
_Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such _Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
that `M ↦ N`. that `M —→ N`.
So, either we have a value, and we are done, or we can take a reduction step. So, either we have a value, and we are done, or we can take a reduction step.
In the latter case, we would like to apply progress again. But to do so we need In the latter case, we would like to apply progress again. But to do so we need
@ -67,7 +67,7 @@ to know that the term yielded by the reduction is itself closed and well-typed.
It turns out that this property holds whenever we start with a closed, It turns out that this property holds whenever we start with a closed,
well-typed term. well-typed term.
_Preservation_: If `∅ ⊢ M ⦂ A` and `M ↦ N` then `∅ ⊢ N ⦂ A`. _Preservation_: If `∅ ⊢ M ⦂ A` and `M —→ N` then `∅ ⊢ N ⦂ A`.
This gives us a recipe for automating evaluation. Start with a closed This gives us a recipe for automating evaluation. Start with a closed
and well-typed term. By progress, it is either a value, in which case and well-typed term. By progress, it is either a value, in which case
@ -93,10 +93,10 @@ types without needing to develop a separate inductive definition of the
We start with any easy observation. Values do not reduce. We start with any easy observation. Values do not reduce.
\begin{code} \begin{code}
V¬↦ : ∀ {M N} → Value M → ¬ (M ↦ N) V¬—→ : ∀ {M N} → Value M → ¬ (M —→ N)
V¬↦ V-ƛ () V¬—→ V-ƛ ()
V¬↦ V-zero () V¬—→ V-zero ()
V¬↦ (V-suc VM) (ξ-suc M↦N) = V¬↦ VM M↦N V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N
\end{code} \end{code}
We consider the three possibilities for values. We consider the three possibilities for values.
@ -110,13 +110,13 @@ We consider the three possibilities for values.
As a corollary, terms that reduce are not values. As a corollary, terms that reduce are not values.
\begin{code} \begin{code}
↦¬V : ∀ {M N} → (M ↦ N) → ¬ Value M —→¬V : ∀ {M N} → (M —→ N) → ¬ Value M
↦¬V M↦N VM = V¬↦ VM M↦N —→¬V M—→N VM = V¬—→ VM M—→N
\end{code} \end{code}
If we expand out the negations, we have If we expand out the negations, we have
V¬↦ : ∀ {M N} → Value M → M ↦ N → ⊥ V¬—→ : ∀ {M N} → Value M → M —→ N → ⊥
↦¬V : ∀ {M N} → M ↦ N → Value M → ⊥ —→¬V : ∀ {M N} → M —→ N → Value M → ⊥
which are the same function with the arguments swapped. which are the same function with the arguments swapped.
@ -139,38 +139,38 @@ cong₄ f refl refl refl refl = refl
It is now straightforward to show that reduction is deterministic. It is now straightforward to show that reduction is deterministic.
\begin{code} \begin{code}
det : ∀ {M M′ M″} det : ∀ {M M′ M″}
→ (M ↦ M′) → (M —→ M′)
→ (M ↦ M″) → (M —→ M″)
-------- --------
→ M′ ≡ M″ → M′ ≡ M″
det (ξ-·₁ L↦L′) (ξ-·₁ L↦L″) = cong₂ _·_ (det L↦L′ L↦L″) refl det (ξ-·₁ L—→L′) (ξ-·₁ L—→L″) = cong₂ _·_ (det L—→L′ L—→L″) refl
det (ξ-·₁ L↦L′) (ξ-·₂ VL M↦M″) = ⊥-elim (V¬↦ VL L↦L′) det (ξ-·₁ L—→L′) (ξ-·₂ VL M—→M″) = ⊥-elim (V¬—→ VL L—→L′)
det (ξ-·₁ L↦L′) (β-ƛ _) = ⊥-elim (V¬↦ V-ƛ L↦L′) det (ξ-·₁ L—→L′) (β-ƛ _) = ⊥-elim (V¬—→ V-ƛ L—→L′)
det (ξ-·₂ VL _) (ξ-·₁ L↦L″) = ⊥-elim (V¬↦ VL L↦L″) det (ξ-·₂ VL _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ VL L—→L″)
det (ξ-·₂ _ M↦M′) (ξ-·₂ _ M↦M″) = cong₂ _·_ refl (det M↦M′ M↦M″) det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″) = cong₂ _·_ refl (det M—→M′ M—→M″)
det (ξ-·₂ _ M↦M′) (β-ƛ VM) = ⊥-elim (V¬↦ VM M↦M′) det (ξ-·₂ _ M—→M′) (β-ƛ VM) = ⊥-elim (V¬—→ VM M—→M′)
det (β-ƛ _) (ξ-·₁ L↦L″) = ⊥-elim (V¬↦ V-ƛ L↦L″) det (β-ƛ _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ V-ƛ L—→L″)
det (β-ƛ VM) (ξ-·₂ _ M↦M″) = ⊥-elim (V¬↦ VM M↦M″) det (β-ƛ VM) (ξ-·₂ _ M—→M″) = ⊥-elim (V¬—→ VM M—→M″)
det (β-ƛ _) (β-ƛ _) = refl det (β-ƛ _) (β-ƛ _) = refl
det (ξ-suc M↦M′) (ξ-suc M↦M″) = cong `suc_ (det M↦M′ M↦M″) det (ξ-suc M—→M′) (ξ-suc M—→M″) = cong `suc_ (det M—→M′ M—→M″)
det (ξ-case L↦L′) (ξ-case L↦L″) = cong₄ `case_[zero⇒_|suc_⇒_] det (ξ-case L—→L′) (ξ-case L—→L″) = cong₄ `case_[zero⇒_|suc_⇒_]
(det L↦L′ L↦L″) refl refl refl (det L—→L′ L—→L″) refl refl refl
det (ξ-case L↦L′) β-zero = ⊥-elim (V¬↦ V-zero L↦L′) det (ξ-case L—→L′) β-zero = ⊥-elim (V¬—→ V-zero L—→L′)
det (ξ-case L↦L′) (β-suc VL) = ⊥-elim (V¬↦ (V-suc VL) L↦L′) det (ξ-case L—→L′) (β-suc VL) = ⊥-elim (V¬—→ (V-suc VL) L—→L′)
det β-zero (ξ-case M↦M″) = ⊥-elim (V¬↦ V-zero M↦M″) det β-zero (ξ-case M—→M″) = ⊥-elim (V¬—→ V-zero M—→M″)
det β-zero β-zero = refl det β-zero β-zero = refl
det (β-suc VL) (ξ-case L↦L″) = ⊥-elim (V¬↦ (V-suc VL) L↦L″) det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″)
det (β-suc _) (β-suc _) = refl det (β-suc _) (β-suc _) = refl
det β-μ β-μ = refl det β-μ β-μ = refl
\end{code} \end{code}
The proof is by induction over possible reductions. We consider The proof is by induction over possible reductions. We consider
three typical cases. three typical cases.
* Two instances of `ξ-·₁`. * Two instances of `ξ-·₁`.
L ↦ L′ L ↦ L″ L —→ L′ L —→ L″
-------------- ξ-·₁ -------------- ξ-·₁ -------------- ξ-·₁ -------------- ξ-·₁
L · M ↦ L′ · M L · M ↦ L″ · M L · M —→ L′ · M L · M —→ L″ · M
By induction we have `L′ ≡ L″`, and hence by congruence By induction we have `L′ ≡ L″`, and hence by congruence
`L′ · M ≡ L″ · M`. `L′ · M ≡ L″ · M`.
@ -178,9 +178,9 @@ three typical cases.
* An instance of `ξ-·₁` and an instance of `ξ-·₂`. * An instance of `ξ-·₁` and an instance of `ξ-·₂`.
Value L Value L
L ↦ L′ M ↦ M″ L —→ L′ M —→ M″
-------------- ξ-·₁ -------------- ξ-·₂ -------------- ξ-·₁ -------------- ξ-·₂
L · M ↦ L′ · M L · M ↦ L · M″ L · M —→ L′ · M L · M —→ L · M″
The rule on the left requires `L` to reduce, but the rule on the right The rule on the left requires `L` to reduce, but the rule on the right
requires `L` to be a value. This is a contradiction since values do requires `L` to be a value. This is a contradiction since values do
@ -191,7 +191,7 @@ three typical cases.
Value V Value V Value V Value V
---------------------------- β-ƛ ---------------------------- β-ƛ ---------------------------- β-ƛ ---------------------------- β-ƛ
(ƛ x ⇒ N) · V ↦ N [ x := V ] (ƛ x ⇒ N) · V ↦ N [ x := V ] (ƛ x ⇒ N) · V —→ N [ x := V ] (ƛ x ⇒ N) · V —→ N [ x := V ]
Since the left-hand sides are identical, the right-hand sides are Since the left-hand sides are identical, the right-hand sides are
also identical. also identical.
@ -202,7 +202,7 @@ once with `ξ-·₁` first and `ξ-·₂` second, and the other time with the
two swapped. What we might like to do is delete the redundant lines two swapped. What we might like to do is delete the redundant lines
and add and add
det M↦M′ M↦M″ = sym (det M↦M″ M↦M′) det M—→M′ M—→M″ = sym (det M—→M″ M—→M′)
to the bottom of the proof. But this does not work. The termination to the bottom of the proof. But this does not work. The termination
checker complains, because the arguments have merely switched order checker complains, because the arguments have merely switched order
@ -310,7 +310,7 @@ second has a free variable. Every term that is well-typed and closed
has the desired property. has the desired property.
_Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such _Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
that `M ↦ N`. that `M —→ N`.
To formulate this property, we first introduce a relation that To formulate this property, we first introduce a relation that
captures what it means for a term `M` to make progess. captures what it means for a term `M` to make progess.
@ -318,7 +318,7 @@ captures what it means for a term `M` to make progess.
data Progress (M : Term) : Set where data Progress (M : Term) : Set where
step : ∀ {N} step : ∀ {N}
→ M ↦ N → M —→ N
---------- ----------
→ Progress M → Progress M
@ -328,7 +328,7 @@ data Progress (M : Term) : Set where
→ Progress M → Progress M
\end{code} \end{code}
A term `M` makes progress if either it can take a step, meaning there 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 exists a term `N` such that `M —→ N`, or if it is done, meaning that
`M` is a value. `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 is a value.
@ -340,17 +340,17 @@ progress : ∀ {M A}
progress (⊢` ()) progress (⊢` ())
progress (⊢ƛ ⊢N) = done V-ƛ progress (⊢ƛ ⊢N) = done V-ƛ
progress (⊢L · ⊢M) with progress ⊢L progress (⊢L · ⊢M) with progress ⊢L
... | step L↦L′ = step (ξ-·₁ L↦L′) ... | step L—→L′ = step (ξ-·₁ L—→L′)
... | done VL with progress ⊢M ... | done VL with progress ⊢M
... | step M↦M′ = step (ξ-·₂ VL M↦M′) ... | step M—→M′ = step (ξ-·₂ VL M—→M′)
... | done VM with canonical ⊢L VL ... | done VM with canonical ⊢L VL
... | C-ƛ _ = step (β-ƛ VM) ... | C-ƛ _ = step (β-ƛ VM)
progress ⊢zero = done V-zero progress ⊢zero = done V-zero
progress (⊢suc ⊢M) with progress ⊢M progress (⊢suc ⊢M) with progress ⊢M
... | step M↦M′ = step (ξ-suc M↦M′) ... | step M—→M′ = step (ξ-suc M—→M′)
... | done VM = done (V-suc VM) ... | done VM = done (V-suc VM)
progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
... | step L↦L′ = step (ξ-case L↦L′) ... | step L—→L′ = step (ξ-case L—→L′)
... | done VL with canonical ⊢L VL ... | done VL with canonical ⊢L VL
... | C-zero = step β-zero ... | C-zero = step β-zero
... | C-suc CL = step (β-suc (value CL)) ... | C-suc CL = step (β-suc (value CL))
@ -367,7 +367,7 @@ Let's unpack the first three cases.
* If the term is an application `L · M`, recursively apply * If the term is an application `L · M`, recursively apply
progress to the derivation that `L` is well-typed. progress to the derivation that `L` is well-typed.
+ If the term steps, we have evidence that `L ↦ L′`, + If the term steps, we have evidence that `L —→ L′`,
which by `ξ-·₁` means that our original term steps which by `ξ-·₁` means that our original term steps
to `L′ · M` to `L′ · M`
@ -375,7 +375,7 @@ Let's unpack the first three cases.
a value. Recursively apply progress to the derivation a value. Recursively apply progress to the derivation
that `M` is well-typed. that `M` is well-typed.
- If the term steps, we have evidence that `M ↦ M′`, - If the term steps, we have evidence that `M —→ M′`,
which by `ξ-·₂` means that our original term steps which by `ξ-·₂` means that our original term steps
to `L · M′`. Step `ξ-·₂` applies only if we have to `L · M′`. Step `ξ-·₂` applies only if we have
evidence that `L` is a value, but progress on that evidence that `L` is a value, but progress on that
@ -407,7 +407,7 @@ Instead of defining a data type for `Progress M`, we could
have formulated progress using disjunction and existentials: have formulated progress using disjunction and existentials:
\begin{code} \begin{code}
postulate postulate
progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M ↦ N) progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N)
\end{code} \end{code}
This leads to a less perspicous proof. Instead of the mnemonic `done` This leads to a less perspicous proof. Instead of the mnemonic `done`
and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer
@ -423,7 +423,7 @@ proof of `progress` above.
#### Exercise (`Progress-iso`) #### Exercise (`Progress-iso`)
Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M ↦ N)`. Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
## Prelude to preservation ## Prelude to preservation
@ -488,7 +488,7 @@ the same result as if we first substitute and then type the result.
The third step is to show preservation. The third step is to show preservation.
_Preservation_: _Preservation_:
If `∅ ⊢ M ⦂ A` and `M ↦ N` then `∅ ⊢ N ⦂ A`. If `∅ ⊢ M ⦂ A` and `M —→ N` then `∅ ⊢ N ⦂ A`.
The proof is by induction over the possible reductions, and The proof is by induction over the possible reductions, and
the substitution lemma is crucial in showing that each of the the substitution lemma is crucial in showing that each of the
@ -904,20 +904,20 @@ that reduction preserves types is straightforward.
\begin{code} \begin{code}
preserve : ∀ {M N A} preserve : ∀ {M N A}
→ ∅ ⊢ M ⦂ A → ∅ ⊢ M ⦂ A
→ M ↦ N → M —→ N
---------- ----------
→ ∅ ⊢ N ⦂ A → ∅ ⊢ N ⦂ A
preserve (⊢` ()) preserve (⊢` ())
preserve (⊢ƛ ⊢N) () preserve (⊢ƛ ⊢N) ()
preserve (⊢L · ⊢M) (ξ-·₁ L↦L′) = (preserve ⊢L L↦L′) · ⊢M preserve (⊢L · ⊢M) (ξ-·₁ L—→L′) = (preserve ⊢L L—→L′) · ⊢M
preserve (⊢L · ⊢M) (ξ-·₂ VL M↦M′) = ⊢L · (preserve ⊢M M↦M′) preserve (⊢L · ⊢M) (ξ-·₂ VL M—→M′) = ⊢L · (preserve ⊢M M—→M′)
preserve ((⊢ƛ ⊢N) · ⊢V) (β-ƛ VV) = subst ⊢V ⊢N preserve ((⊢ƛ ⊢N) · ⊢V) (β-ƛ VV) = subst ⊢V ⊢N
preserve ⊢zero () preserve ⊢zero ()
preserve (⊢suc ⊢M) (ξ-suc M↦M′) = ⊢suc (preserve ⊢M M↦M′) 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 ⊢L ⊢M ⊢N) (ξ-case L—→L′) = ⊢case (preserve ⊢L L—→L′) ⊢M ⊢N
preserve (⊢case ⊢zero ⊢M ⊢N) β-zero = ⊢M preserve (⊢case ⊢zero ⊢M ⊢N) β-zero = ⊢M
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV) = subst ⊢V ⊢N preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV) = subst ⊢V ⊢N
preserve (⊢μ ⊢M) (β-μ) = subst (⊢μ ⊢M) ⊢M preserve (⊢μ ⊢M) (β-μ) = subst (⊢μ ⊢M) ⊢M
\end{code} \end{code}
The proof never mentions the types of `M` or `N`, The proof never mentions the types of `M` or `N`,
so in what follows we choose type name as convenient. so in what follows we choose type name as convenient.
@ -926,9 +926,9 @@ Let's unpack the cases for two of the reduction rules.
* Rule `ξ-·₁`. We have * Rule `ξ-·₁`. We have
L ↦ L′ L —→ L′
---------------- ----------------
L · M ↦ L′ · M L · M —→ L′ · M
where the left-hand side is typed by where the left-hand side is typed by
@ -940,7 +940,7 @@ Let's unpack the cases for two of the reduction rules.
By induction, we have By induction, we have
Γ ⊢ L ⦂ A ⇒ B Γ ⊢ L ⦂ A ⇒ B
L ↦ L′ L —→ L′
-------------- --------------
Γ ⊢ L′ ⦂ A ⇒ B Γ ⊢ L′ ⦂ A ⇒ B
@ -987,11 +987,11 @@ sucμ = μ "x" ⇒ `suc (` "x")
_ = _ =
begin begin
sucμ sucμ
↦⟨ β-μ ⟩ —→⟨ β-μ ⟩
`suc sucμ `suc sucμ
↦⟨ ξ-suc β-μ ⟩ —→⟨ ξ-suc β-μ ⟩
`suc `suc sucμ `suc `suc sucμ
↦⟨ ξ-suc (ξ-suc β-μ) ⟩ —→⟨ ξ-suc (ξ-suc β-μ) ⟩
`suc `suc `suc sucμ `suc `suc `suc sucμ
-- ... -- ...
∎ ∎
@ -1042,7 +1042,7 @@ reduction finished.
data Steps (L : Term) : Set where data Steps (L : Term) : Set where
steps : ∀ {N} steps : ∀ {N}
→ L ↠ N → L —↠ N
→ Finished N → Finished N
---------- ----------
→ Steps L → Steps L
@ -1058,15 +1058,15 @@ eval : ∀ {L A}
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 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) ... | 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} \end{code}
Let `L` be the name of the term we are reducing, and `⊢L` be the 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 evidence that `L` is well-typed. We consider the amount of gas
remaining. There are two possibilities. remaining. There are two possibilities.
* It is zero, so we stop early. We return the trivial reduction * It is zero, so we stop early. We return the trivial reduction
sequence `L ↠ L`, evidence that `L` is well-typed, and an sequence `L —↠ L`, evidence that `L` is well-typed, and an
indication that we are out of gas. indication that we are out of gas.
* It is non-zero and after the next step we have `m` gas remaining. * It is non-zero and after the next step we have `m` gas remaining.
@ -1074,15 +1074,15 @@ remaining. There are two possibilities.
are two possibilities. are two possibilities.
+ Term `L` is a value, so we are done. We return the + Term `L` is a value, so we are done. We return the
trivial reduction sequence `L ↠ L`, evidence that `L` is trivial reduction sequence `L —↠ L`, evidence that `L` is
well-typed, and the evidence that `L` is a value. well-typed, and the evidence that `L` is a value.
+ Term `L` steps to another term `M`. Preservation provides + Term `L` steps to another term `M`. Preservation provides
evidence that `M` is also well-typed, and we recursively invoke evidence that `M` is also well-typed, and we recursively invoke
`eval` on the remaining gas. The result is evidence that `eval` on the remaining gas. The result is evidence that
`M ↠ N`, together with evidence that `N` is well-typed and an `M —↠ N`, together with evidence that `N` is well-typed and an
indication of whether reduction finished. We combine the evidence indication of whether reduction finished. We combine the evidence
that `L ↦ M` and `M ↠ N` to return evidence that `L ↠ N`, that `L —→ M` and `M —↠ N` to return evidence that `L —↠ N`,
together with the other relevant evidence. together with the other relevant evidence.
@ -1102,9 +1102,9 @@ sequence, we evaluate with three steps worth of gas.
\begin{code} \begin{code}
_ : eval (gas 3) ⊢sucμ ≡ _ : eval (gas 3) ⊢sucμ ≡
steps steps
(μ "x" ⇒ `suc ` "x" ↦⟨ β-μ ⟩ (μ "x" ⇒ `suc ` "x" —→⟨ β-μ ⟩
`suc (μ "x" ⇒ `suc ` "x") ↦⟨ ξ-suc β-μ ⟩ `suc (μ "x" ⇒ `suc ` "x") —→⟨ ξ-suc β-μ ⟩
`suc (`suc (μ "x" ⇒ `suc ` "x")) ↦⟨ ξ-suc (ξ-suc β-μ) ⟩ `suc (`suc (μ "x" ⇒ `suc ` "x")) —→⟨ ξ-suc (ξ-suc β-μ) ⟩
`suc (`suc (`suc (μ "x" ⇒ `suc ` "x"))) ∎) `suc (`suc (`suc (μ "x" ⇒ `suc ` "x"))) ∎)
out-of-gas out-of-gas
_ = refl _ = refl
@ -1118,13 +1118,13 @@ _ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡
steps steps
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· `zero · `zero
↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
`zero `zero
↦⟨ β-ƛ V-zero ⟩ —→⟨ β-ƛ V-zero ⟩
(ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero) ↦⟨ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero) —→⟨
ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ "n" ⇒ `suc ` "n") · `suc `zero ↦⟨ β-ƛ (V-suc V-zero) ⟩ (ƛ "n" ⇒ `suc ` "n") · `suc `zero —→⟨ β-ƛ (V-suc V-zero) ⟩
`suc (`suc `zero) ∎) `suc (`suc `zero) ∎)
(done (V-suc (V-suc V-zero))) (done (V-suc (V-suc V-zero)))
_ = refl _ = refl
@ -1146,7 +1146,7 @@ _ : eval (gas 100) ⊢2+2 ≡
]))) ])))
· `suc (`suc `zero) · `suc (`suc `zero)
· `suc (`suc `zero) · `suc (`suc `zero)
↦⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩ —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `case ` "m" [zero⇒ ` "n" |suc "m" ⇒
@ -1161,7 +1161,7 @@ _ : eval (gas 100) ⊢2+2 ≡
])) ]))
· `suc (`suc `zero) · `suc (`suc `zero)
· `suc (`suc `zero) · `suc (`suc `zero)
↦⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩ —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒ (ƛ "n" ⇒
`case `suc (`suc `zero) [zero⇒ ` "n" |suc "m" ⇒ `case `suc (`suc `zero) [zero⇒ ` "n" |suc "m" ⇒
`suc `suc
@ -1174,7 +1174,7 @@ _ : eval (gas 100) ⊢2+2 ≡
· ` "n") · ` "n")
]) ])
· `suc (`suc `zero) · `suc (`suc `zero)
↦⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩ —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
`case `suc (`suc `zero) [zero⇒ `suc (`suc `zero) |suc "m" ⇒ `case `suc (`suc `zero) [zero⇒ `suc (`suc `zero) |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
@ -1185,7 +1185,7 @@ _ : eval (gas 100) ⊢2+2 ≡
· ` "m" · ` "m"
· `suc (`suc `zero)) · `suc (`suc `zero))
] ]
↦⟨ β-suc (V-suc V-zero) ⟩ —→⟨ β-suc (V-suc V-zero) ⟩
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
@ -1194,7 +1194,7 @@ _ : eval (gas 100) ⊢2+2 ≡
]))) ])))
· `suc `zero · `suc `zero
· `suc (`suc `zero)) · `suc (`suc `zero))
↦⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩ —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc `suc
((ƛ "m" ⇒ ((ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
@ -1210,7 +1210,7 @@ _ : eval (gas 100) ⊢2+2 ≡
])) ]))
· `suc `zero · `suc `zero
· `suc (`suc `zero)) · `suc (`suc `zero))
↦⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩ —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc `suc
((ƛ "n" ⇒ ((ƛ "n" ⇒
`case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `case `suc `zero [zero⇒ ` "n" |suc "m" ⇒
@ -1224,7 +1224,7 @@ _ : eval (gas 100) ⊢2+2 ≡
· ` "n") · ` "n")
]) ])
· `suc (`suc `zero)) · `suc (`suc `zero))
↦⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩ —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
`suc `suc
`case `suc `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒ `case `suc `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
`suc `suc
@ -1236,7 +1236,7 @@ _ : eval (gas 100) ⊢2+2 ≡
· ` "m" · ` "m"
· `suc (`suc `zero)) · `suc (`suc `zero))
] ]
↦⟨ ξ-suc (β-suc V-zero) ⟩ —→⟨ ξ-suc (β-suc V-zero) ⟩
`suc `suc
(`suc (`suc
((μ "+" ⇒ ((μ "+" ⇒
@ -1246,7 +1246,7 @@ _ : eval (gas 100) ⊢2+2 ≡
]))) ])))
· `zero · `zero
· `suc (`suc `zero))) · `suc (`suc `zero)))
↦⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩ —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc `suc
(`suc (`suc
((ƛ "m" ⇒ ((ƛ "m" ⇒
@ -1263,7 +1263,7 @@ _ : eval (gas 100) ⊢2+2 ≡
])) ]))
· `zero · `zero
· `suc (`suc `zero))) · `suc (`suc `zero)))
↦⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩ —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc `suc
(`suc (`suc
((ƛ "n" ⇒ ((ƛ "n" ⇒
@ -1278,7 +1278,7 @@ _ : eval (gas 100) ⊢2+2 ≡
· ` "n") · ` "n")
]) ])
· `suc (`suc `zero))) · `suc (`suc `zero)))
↦⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩ —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
`suc `suc
(`suc (`suc
`case `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒ `case `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
@ -1291,7 +1291,7 @@ _ : eval (gas 100) ⊢2+2 ≡
· ` "m" · ` "m"
· `suc (`suc `zero)) · `suc (`suc `zero))
]) ])
↦⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎) —→⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎)
(done (V-suc (V-suc (V-suc (V-suc V-zero))))) (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
_ = refl _ = refl
\end{code} \end{code}
@ -1309,7 +1309,7 @@ _ : eval (gas 100) ⊢2+2ᶜ ≡
· (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
· (ƛ "n" ⇒ `suc ` "n") · (ƛ "n" ⇒ `suc ` "n")
· `zero · `zero
↦⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩ —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
(ƛ "n" ⇒ (ƛ "n" ⇒
(ƛ "s" ⇒ (ƛ "s" ⇒
(ƛ "z" ⇒ (ƛ "z" ⇒
@ -1318,46 +1318,46 @@ _ : eval (gas 100) ⊢2+2ᶜ ≡
· (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
· (ƛ "n" ⇒ `suc ` "n") · (ƛ "n" ⇒ `suc ` "n")
· `zero · `zero
↦⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩ —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "s" ⇒ (ƛ "s" ⇒
(ƛ "z" ⇒ (ƛ "z" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" ·
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" · ` "z"))) ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" · ` "z")))
· (ƛ "n" ⇒ `suc ` "n") · (ƛ "n" ⇒ `suc ` "n")
· `zero · `zero
↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ (ƛ "z" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· ·
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· ` "z")) · ` "z"))
· `zero · `zero
↦⟨ β-ƛ V-zero ⟩ —→⟨ β-ƛ V-zero ⟩
(ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· ·
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· `zero) · `zero)
↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· `zero) · `zero)
↦⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩ —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · ((ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
`zero) `zero)
↦⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩ —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero)) ((ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero))
↦⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩ —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "n" ⇒ `suc ` "n") · `suc `zero) ((ƛ "n" ⇒ `suc ` "n") · `suc `zero)
↦⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩ —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
`suc (`suc `zero) `suc (`suc `zero)
↦⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩ —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
(ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `suc (`suc `zero)) (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `suc (`suc `zero))
↦⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩ —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒ `suc ` "n") · `suc (`suc (`suc `zero)) ↦⟨ (ƛ "n" ⇒ `suc ` "n") · `suc (`suc (`suc `zero)) —→⟨
β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
`suc (`suc (`suc (`suc `zero))) ∎) `suc (`suc (`suc (`suc `zero))) ∎)
(done (V-suc (V-suc (V-suc (V-suc V-zero))))) (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
@ -1371,7 +1371,7 @@ above.
A term is _normal_ if it cannot reduce. A term is _normal_ if it cannot reduce.
\begin{code} \begin{code}
Normal : Term → Set Normal : Term → Set
Normal M = ∀ {N} → ¬ (M ↦ N) Normal M = ∀ {N} → ¬ (M —→ N)
\end{code} \end{code}
A term is _stuck_ if it is normal yet not a value. A term is _stuck_ if it is normal yet not a value.
@ -1394,7 +1394,7 @@ Using preservation, it is easy to show that after any number of steps, a well-ty
postulate postulate
preserves : ∀ {M N A} preserves : ∀ {M N A}
→ ∅ ⊢ M ⦂ A → ∅ ⊢ M ⦂ A
→ M ↠ N → M —↠ N
--------- ---------
→ ∅ ⊢ N ⦂ A → ∅ ⊢ N ⦂ A
\end{code} \end{code}
@ -1406,7 +1406,7 @@ result with the slogan _well-typed terms don't get stuck_.
postulate postulate
wttdgs : ∀ {M N A} wttdgs : ∀ {M N A}
→ ∅ ⊢ M ⦂ A → ∅ ⊢ M ⦂ A
→ M ↠ N → M —↠ N
----------- -----------
→ ¬ (Stuck M) → ¬ (Stuck M)
\end{code} \end{code}
@ -1427,8 +1427,8 @@ unstuck′ : ∀ {M A}
→ ∅ ⊢ M ⦂ A → ∅ ⊢ M ⦂ A
----------- -----------
→ ¬ (Stuck M) → ¬ (Stuck M)
unstuck′ ⊢M ⟨ ¬M↦N , ¬VM ⟩ with progress ⊢M unstuck′ ⊢M ⟨ ¬M—→N , ¬VM ⟩ with progress ⊢M
... | step M↦N = ¬M↦N M↦N ... | step M—→N = ¬M—→N M—→N
... | done VM = ¬VM VM ... | done VM = ¬VM VM
\end{code} \end{code}
@ -1436,21 +1436,21 @@ Any descendant of a well-typed term is well-typed.
\begin{code} \begin{code}
preserves′ : ∀ {M N A} preserves′ : ∀ {M N A}
→ ∅ ⊢ M ⦂ A → ∅ ⊢ M ⦂ A
→ M ↠ N → M —↠ N
--------- ---------
→ ∅ ⊢ N ⦂ A → ∅ ⊢ N ⦂ A
preserves′ ⊢M (M ∎) = ⊢M preserves′ ⊢M (M ∎) = ⊢M
preserves′ ⊢L (L ↦⟨ L↦M ⟩ M↠N) = preserves′ (preserve ⊢L L↦M) M↠N preserves′ ⊢L (L —→⟨ L—→M ⟩ M—↠N) = preserves′ (preserve ⊢L L—→M) M—↠N
\end{code} \end{code}
Combining the above gives us the desired result. Combining the above gives us the desired result.
\begin{code} \begin{code}
wttdgs′ : ∀ {M N A} wttdgs′ : ∀ {M N A}
→ ∅ ⊢ M ⦂ A → ∅ ⊢ M ⦂ A
→ M ↠ N → M —↠ N
----------- -----------
→ ¬ (Stuck N) → ¬ (Stuck N)
wttdgs′ ⊢M M↠N = unstuck′ (preserves′ ⊢M M↠N) wttdgs′ ⊢M M—↠N = unstuck′ (preserves′ ⊢M M—↠N)
\end{code} \end{code}
@ -1462,20 +1462,21 @@ and preservation theorems for the simply typed lambda-calculus.
#### Exercise `subject_expansion` #### Exercise `subject_expansion`
We say that `M` _reduces_ to `N` if `M ↦ N`, We say that `M` _reduces_ to `N` if `M —→ N`,
and conversely 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_. The preservation property is sometimes called _subject reduction_.
Its opposite is _subject expansion_, which holds if Its opposite is _subject expansion_, which holds if
`M ↦ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`. `M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
Find two counter-examples to subject expansion, one Find two counter-examples to subject expansion, one
with case expressions and one not involving case expressions. with case expressions and one not involving case expressions.
#### Quiz #### Quiz
Suppose we add a new term `zap` with the following reduction rule Suppose we add a new term `zap` with the following reduction rule
--------- β-zap -------- β-zap
M ↦ zap M —→ zap
and the following typing rule: and the following typing rule:
@ -1499,11 +1500,11 @@ false, give a counterexample.
Suppose instead that we add a new term `foo` with the following Suppose instead that we add a new term `foo` with the following
reduction rules: reduction rules:
--------------------- β-foo₁ ------------------ β-foo₁
(λ x ⇒ ` x) ↦ foo (λ x ⇒ ` x) —→ foo
------------ β-foo₂ ----------- β-foo₂
foo ↦ zero foo —→ zero
Which of the following properties remain true in Which of the following properties remain true in
the presence of this rule? For each one, write either the presence of this rule? For each one, write either
@ -1543,14 +1544,14 @@ to interpret a natural as a function from naturals to naturals.
Γ ⊢ L ⦂ `ℕ Γ ⊢ L ⦂ `ℕ
Γ ⊢ M ⦂ `ℕ Γ ⊢ M ⦂ `ℕ
-------------- ⊢ℕ⇒ℕ -------------- _·ℕ_
Γ ⊢ L · M ⦂ `ℕ Γ ⊢ L · M ⦂ `ℕ
And that we add the corresponding reduction rule. And that we add the corresponding reduction rule.
fᵢ(m) → n fᵢ(m) —→ n
--------- δ ---------- δ
i · m → n i · m —→ n
Which of the following properties remain true in Which of the following properties remain true in
the presence of this rule? For each one, write either the presence of this rule? For each one, write either
@ -1563,3 +1564,5 @@ false, give a counterexample.
- Preservation - Preservation
Are all properties preserved in this case? Are there any
other alterations we would wish to make to the system?