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

revised notation for Lambda, PandP

Browse source
This commit is contained in:
wadler 2018-06-29 12:11:41 -03:00
parent 62b25bad76
commit ba4dd3e84b
2 changed files with 408 additions and 405 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

448
src/plta/Lambda.lagda
View file

@ -11,7 +11,7 @@ module plta.Lambda where
[This chapter was originally based on Chapter _Stlc_ [This chapter was originally based on Chapter _Stlc_
of _Software Foundations_ (_Programming Language Foundations_). of _Software Foundations_ (_Programming Language Foundations_).
It has now been updated, but if you spot any plagiarism It has now been updated, but if you spot any plagiarism
please let me know. -- P] please let me know. – P]
The _lambda-calculus_, first published by the logician Alonzo Church in The _lambda-calculus_, first published by the logician Alonzo Church in
1932, is a core calculus with only three syntactic constructs: 1932, is a core calculus with only three syntactic constructs:
@ -67,7 +67,7 @@ open import Relation.Nullary.Negation using (¬?)
Terms have seven constructs. Three are for the core lambda calculus: Terms have seven constructs. Three are for the core lambda calculus:
* Variables `⌊ x ⌋` * Variables `` x`
* Abstractions `ƛ x ⇒ N` * Abstractions `ƛ x ⇒ N`
* Applications `L · M` * Applications `L · M`
@ -94,7 +94,7 @@ correspond to introduction rules and deconstructors to eliminators.
Here is the syntax of terms in BNF. Here is the syntax of terms in BNF.
L, M, N ::= L, M, N ::=
⌊ x ⌋ | ƛ x ⇒ N | L · M | ` x | ƛ x ⇒ N | L · M |
`zero | `suc M | `case L [zero⇒ M |suc x ⇒ N] | `zero | `suc M | `case L [zero⇒ M |suc x ⇒ N] |
μ x ⇒ M μ x ⇒ M
@ -107,9 +107,10 @@ infix 6 ƛ_⇒_
infix 6 μ_⇒_ infix 6 μ_⇒_
infixl 7 _·_ infixl 7 _·_
infix 8 `suc_ infix 8 `suc_
infix 9 `_
data Term : Set where data Term : Set where
⌊_⌋ : Id → Term `_ : Id → Term
ƛ_⇒_ : Id → Term → Term ƛ_⇒_ : Id → Term → Term
_·_ : Term → Term → Term _·_ : Term → Term → Term
`zero : Term `zero : Term
@ -134,9 +135,9 @@ two = `suc `suc `zero
plus : Term plus : Term
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case ⌊ "m" ⌋ `case ` "m"
[zero⇒ ⌊ "n" ⌋ [zero⇒ ` "n"
|suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) ] |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
four : Term four : Term
four = plus · two · two four = plus · two · two
@ -160,14 +161,14 @@ function that adds Church numerals, a function to compute successor,
and a term that computes two plus two. and a term that computes two plus two.
\begin{code} \begin{code}
twoᶜ : Term twoᶜ : Term
twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")
plusᶜ : Term plusᶜ : Term
plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
⌊ "m" ⌋ · ⌊ "s" ⌋ · (⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋) ` "m" · ` "s" · (` "n" · ` "s" · ` "z")
sucᶜ : Term sucᶜ : Term
sucᶜ = ƛ "n" ⇒ `suc (⌊ "n" ⌋) sucᶜ = ƛ "n" ⇒ `suc (` "n")
fourᶜ : Term fourᶜ : Term
fourᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero fourᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
@ -198,7 +199,7 @@ two natural numbers.
### Formal vs informal ### Formal vs informal
In informal presentation of formal semantics, one uses choice of In informal presentation of formal semantics, one uses choice of
variable name to disambiguate and writes `x` rather than `⌊ x ⌋` variable name to disambiguate and writes `x` rather than `` x`
for a term that is a variable. Agda requires we distinguish. for a term that is a variable. Agda requires we distinguish.
Similarly, informal presentation often use the same notation for Similarly, informal presentation often use the same notation for
@ -218,10 +219,10 @@ and `N` the _body_ of the abstraction. A central feature
of lambda calculus is that consistent renaming of bound variables of lambda calculus is that consistent renaming of bound variables
leaves the meaning of a term unchanged. Thus the five terms leaves the meaning of a term unchanged. Thus the five terms
* `` ƛ "s" ⇒ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) `` * `` ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ``
* `` ƛ "f" ⇒ ƛ "x" ⇒ ⌊ "f" ⌋ · (⌊ "f" ⌋ · ⌊ "x" ⌋) `` * `` ƛ "f" ⇒ ƛ "x" ⇒ ` "f" · (` "f" · ` "x") ``
* `` ƛ "sam" ⇒ ƛ "zelda" ⇒ ⌊ "sam" ⌋ · (⌊ "sam" ⌋ · ⌊ "zelda" ⌋) `` * `` ƛ "sam" ⇒ ƛ "zelda" ⇒ ` "sam" · (` "sam" · ` "zelda") ``
* `` ƛ "z" ⇒ ƛ "s" ⇒ ⌊ "z" ⌋ · (⌊ "z" ⌋ · ⌊ "s" ⌋) `` * `` ƛ "z" ⇒ ƛ "s" ⇒ ` "z" · (` "z" · ` "s") ``
* `` ƛ "😇" ⇒ ƛ "😈" ⇒ # "😇" · (# "😇" · # "😈" ) `` * `` ƛ "😇" ⇒ ƛ "😈" ⇒ # "😇" · (# "😇" · # "😈" ) ``
are all considered equivalent. Following the convention introduced are all considered equivalent. Following the convention introduced
@ -231,13 +232,13 @@ this equivalence relation is called _alpha renaming_.
As we descend from a term into its subterms, variables As we descend from a term into its subterms, variables
that are bound may become free. Consider the following terms. that are bound may become free. Consider the following terms.
* `` ƛ "s" ⇒ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) `` * `` ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ``
has both `s` and `z` as bound variables. has both `s` and `z` as bound variables.
* `` ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) `` * `` ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ``
has `s` bound and `z` free. has `s` bound and `z` free.
* `` ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) `` * `` ` "s" · (` "s" · ` "z") ``
has both `s` and `z` as free variables. has both `s` and `z` as free variables.
We say that a term with no free variables is _closed_; otherwise it is We say that a term with no free variables is _closed_; otherwise it is
@ -247,12 +248,12 @@ two are open.
Different occurrences of a variable may be bound and free. Different occurrences of a variable may be bound and free.
In the term In the term
(ƛ "x" ⇒ ⌊ "x" ⌋) · ⌊ "x" ⌋ (ƛ "x" ⇒ ` "x") · ` "x"
the inner occurrence of `x` is bound while the outer occurrence is free. the inner occurrence of `x` is bound while the outer occurrence is free.
By alpha renaming, the term above is equivalent to By alpha renaming, the term above is equivalent to
(ƛ "y" ⇒ ⌊ "y" ⌋) · ⌊ "x" ⌋ (ƛ "y" ⇒ ` "y") · ` "x"
in which `y` is bound and `x` is free. A common convention, called the in which `y` is bound and `x` is free. A common convention, called the
_Barendregt convention_, is to use alpha renaming to ensure that the bound _Barendregt convention_, is to use alpha renaming to ensure that the bound
@ -264,17 +265,17 @@ Case and recursion also introduce bound variables, which are also subject
to alpha renaming. In the term to alpha renaming. In the term
μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case ⌊ "m" ⌋ `case ` "m"
[zero⇒ ⌊ "n" ⌋ [zero⇒ ` "n"
|suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) ] |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
notice that there are two binding occurrences of `m`, one in the first notice that there are two binding occurrences of `m`, one in the first
line and one in the last line. It is equivalent to the following term, line and one in the last line. It is equivalent to the following term,
μ "plus" ⇒ ƛ "x" ⇒ ƛ "y" ⇒ μ "plus" ⇒ ƛ "x" ⇒ ƛ "y" ⇒
`case ⌊ "x" ⌋ `case ` "x"
[zero⇒ ⌊ "y" ⌋ [zero⇒ ` "y"
|suc "x′" ⇒ `suc (⌊ "plus" ⌋ · ⌊ "x′" ⌋ · ⌊ "y" ⌋) ] |suc "x′" ⇒ `suc (` "plus" · ` "x′" · ` "y") ]
where the two binding occurrences corresponding to `m` now have distinct where the two binding occurrences corresponding to `m` now have distinct
names, `x` and `x′`. names, `x` and `x′`.
@ -342,13 +343,13 @@ Substitution plays a key role in defining the
operational semantics of function application. 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" ``
in the body of the function abstraction. in the body of the function abstraction.
We write substitution as `N [ x := V ]`, meaning We write substitution as `N [ x := V ]`, meaning
@ -360,19 +361,19 @@ usually substitute values.
Here are some examples: Here are some examples:
* `` (sucᶜ · (sucᶜ · ⌊ "z" ⌋)) [ "z" := `zero ] `` yields * `` (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] `` yields
`` sucᶜ · (sucᶜ · `zero) `` `` sucᶜ · (sucᶜ · `zero) ``
* `` (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)) [ "s" := sucᶜ ] `` yields * `` (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] `` yields
ƛ "z" ⇒ sucᶜ · (sucᶜ · ⌊ "z" ⌋) `` ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") ``
* `` (ƛ "x" ⇒ ⌊ "y" ⌋) [ "y" := `zero ] `` yields `` ƛ "x" ⇒ `zero `` * `` (ƛ "x" ⇒ ` "y") [ "y" := `zero ] `` yields `` ƛ "x" ⇒ `zero ``
* `` (ƛ "x" ⇒ ⌊ "x" ⌋) [ "x" := `zero ] `` yields `` ƛ "x" ⇒ ⌊ "x" ⌋ `` * `` (ƛ "x" ⇒ ` "x") [ "x" := `zero ] `` yields `` ƛ "x" ⇒ ` "x" ``
* `` (ƛ "y" ⇒ ⌊ "y" ⌋) [ "x" := `zero ] `` yields `` ƛ "x" ⇒ ⌊ "x" ⌋ `` * `` (ƛ "y" ⇒ ` "y") [ "x" := `zero ] `` yields `` ƛ "x" ⇒ ` "x" ``
In the last but one example, substituting `` `zero `` for `x` in In the last but one example, substituting `` `zero `` for `x` in
`` ƛ "x" ⇒ ⌊ "x" ⌋ `` does _not_ yield `` ƛ "x" ⇒ `zero ``, `` ƛ "x" ⇒ ` "x" `` does _not_ yield `` ƛ "x" ⇒ `zero ``,
since `x` is bound in the lambda abstraction. since `x` is bound in the lambda abstraction.
The choice of bound names is irrelevant: both The choice of bound names is irrelevant: both
`` ƛ "x" ⇒ ⌊ "x" ⌋ `` and `` ƛ "y" ⇒ ⌊ "y" ⌋ `` stand for the `` ƛ "x" ⇒ ` "x" `` and `` ƛ "y" ⇒ ` "y" `` stand for the
identity function. One way to think of this is that `x` within identity function. One way to think of this is that `x` within
the body of the abstraction stands for a _different_ variable than the body of the abstraction stands for a _different_ variable than
`x` outside the abstraction, they just happen to have the same name. `x` outside the abstraction, they just happen to have the same name.
@ -382,13 +383,13 @@ when term substituted for the variable is closed. This is because
substitution by terms that are _not_ closed may require renaming substitution by terms that are _not_ closed may require renaming
of bound variables. For example: of bound variables. For example:
* `` (ƛ "x" ⇒ ⌊ "x" ⌋ · ⌊ "y" ⌋) [ "y" := ⌊ "x" ⌋ · ⌊ "y" ⌋ ] `` should not yield * `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · ` "y" ] `` should not yield
`` ƛ "x" ⇒ ⌊ "x" ⌋ · (⌊ "x" ⌋ · ⌊ "y" ⌋) `` `` ƛ "x" ⇒ ` "x" · (` "x" · ` "y") ``
Instead, we should rename the variables to avoid capture. Instead, we should rename the variables to avoid capture.
* `` (ƛ "x" ⇒ ⌊ "x" ⌋ · ⌊ "y" ⌋) [ "y" := ⌊ "x" ⌋ · ⌊ "y" ⌋ ] `` should yield * `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · ` "y" ] `` should yield
`` ƛ "z" ⇒ ⌊ "z" ⌋ · (⌊ "x" ⌋ · ⌊ "y" ⌋) `` `` ƛ "z" ⇒ ` "z" · (` "x" · ` "y") ``
Formal definition of substitution with suitable renaming is considerably Formal definition of substitution with suitable renaming is considerably
more complex, so we avoid it by restricting to substitution by closed terms, more complex, so we avoid it by restricting to substitution by closed terms,
@ -400,9 +401,9 @@ Here is the formal definition of substitution by closed terms in Agda.
infix 9 _[_:=_] infix 9 _[_:=_]
_[_:=_] : Term → Id → Term → Term _[_:=_] : Term → Id → Term → Term
⌊ x ⌋ [ y := V ] with x ≟ y (` x) [ y := V ] with x ≟ y
... | yes _ = V ... | yes _ = V
... | no _ = ⌊ x ⌋ ... | no _ = ` x
(ƛ x ⇒ N) [ y := V ] with x ≟ y (ƛ x ⇒ N) [ y := V ] with x ≟ y
... | yes _ = ƛ x ⇒ N ... | yes _ = ƛ x ⇒ N
... | no _ = ƛ x ⇒ (N [ y := V ]) ... | no _ = ƛ x ⇒ (N [ y := V ])
@ -440,19 +441,19 @@ simply push substitution recursively into the subterms.
Here is confirmation that the examples above are correct. Here is confirmation that the examples above are correct.
\begin{code} \begin{code}
_ : (sucᶜ · sucᶜ · ⌊ "z" ⌋) [ "z" := `zero ] ≡ sucᶜ · sucᶜ · `zero _ : (sucᶜ · sucᶜ · ` "z") [ "z" := `zero ] ≡ sucᶜ · sucᶜ · `zero
_ = refl _ = refl
_ : (ƛ "z" ⇒ ⌊ "s" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · sucᶜ · ⌊ "z" ⌋ _ : (ƛ "z" ⇒ ` "s" · ` "s" · ` "z") [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · sucᶜ · ` "z"
_ = refl _ = refl
_ : (ƛ "x" ⇒ ⌊ "y" ⌋) [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero _ : (ƛ "x" ⇒ ` "y") [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero
_ = refl _ = refl
_ : (ƛ "x" ⇒ ⌊ "x" ⌋) [ "x" := `zero ] ≡ ƛ "x" ⇒ ⌊ "x" ⌋ _ : (ƛ "x" ⇒ ` "x") [ "x" := `zero ] ≡ ƛ "x" ⇒ ` "x"
_ = refl _ = refl
_ : (ƛ "y" ⇒ ⌊ "y" ⌋) [ "x" := `zero ] ≡ ƛ "y" ⇒ ⌊ "y" ⌋ _ : (ƛ "y" ⇒ ` "y") [ "x" := `zero ] ≡ ƛ "y" ⇒ ` "y"
_ = refl _ = refl
\end{code} \end{code}
@ -460,11 +461,11 @@ _ = refl
What is the result of the following substitution? What is the result of the following substitution?
(ƛ "y" ⇒ ⌊ "x" ⌋ · (ƛ "x" ⇒ ⌊ "x" ⌋)) [ "x" := `zero ] (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ ` "x")) [ "x" := `zero ]
1. `` (ƛ "y" ⇒ ⌊ "x" ⌋ · (ƛ "x" ⇒ ⌊ "x" ⌋)) `` 1. `` (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ ` "x")) ``
2. `` (ƛ "y" ⇒ ⌊ "x" ⌋ · (ƛ "x" ⇒ `zero)) `` 2. `` (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ `zero)) ``
3. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ ⌊ "x" ⌋)) `` 3. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ ` "x")) ``
4. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ `zero)) `` 4. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ `zero)) ``
@ -479,16 +480,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
@ -513,75 +514,84 @@ 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 ]
β-case-zero : ∀ {x M N} β-zero : ∀ {x M N}
---------------------------------------- ----------------------------------------
→ `case `zero [zero⇒ M |suc x ⇒ N ] ⟶ M → `case `zero [zero⇒ M |suc x ⇒ N ] ↦ M
β-case-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
of a term are reduced to values before the whole term is reduced.
This is referred to as _call by value_ reduction.
Further, we have arranged that subterms are reduced in a
left-to-right order. This means that reduction is _deterministic_:
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.
#### 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") ``
3. `` (ƛ "x" ⇒ ⌊ "x" ⌋) · (ƛ "x" ⇒ ⌊ "x" ⌋) · (ƛ "x" ⇒ ⌊ "x" ⌋) `` 3. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
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") ``
3. `` (ƛ "x" ⇒ ⌊ "x" ⌋) · (ƛ "x" ⇒ ⌊ "x" ⌋) · (ƛ "x" ⇒ ⌊ "x" ⌋) `` 3. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
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 ``
3. `` `zero `` 3. `` `zero ``
@ -589,170 +599,155 @@ 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 function `⟶`. the reflexive and transitive closure `↠` of the step relation `↦`.
The reflexive and transitive closure `⟶*` of an arbitrary relation `⟶` We define reflexive and transitive closure as a sequence of zero or
is the smallest relation that includes `⟶` and is also reflexive more steps of the underlying relation, along lines similar to that for
and transitive. We could define this directly, as follows. reasoning about chains of equalities
\begin{code}
module Closure (A : Set) (_⟶_ : A → A → Set) where
data _⟶*_ : A → A → Set where
refl : ∀ {M}
--------
→ M ⟶* M
trans : ∀ {L M N}
→ L ⟶* M
→ M ⟶* N
--------
→ L ⟶* N
inc : ∀ {M N}
→ M ⟶ N
--------
→ M ⟶* N
\end{code}
Here we use a module to define the reflexive and transitive
closure of an arbitrary relation.
The three clauses specify that `⟶*` is reflexive and transitive,
and that `⟶` implies `⟶*`.
However, it will prove more convenient to define the transitive
closure as a sequence of zero or more steps of the underlying
relation, along lines similar to that for 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}
module Chain (A : Set) (_⟶_ : A → A → Set) where infix 2 _↠_
infix 1 begin_
infixr 2 _↦⟨_⟩_
infix 3 _∎
infix 2 _⟶*_ data _↠_ : Term → Term → Set where
infix 1 begin_ _∎ : ∀ M
infixr 2 _⟶⟨_⟩_ ---------
infix 3 _∎ → M ↠ M
data _⟶*_ : A → A → Set where _↦⟨_⟩_ : ∀ L {M N}
_∎ : ∀ M → L ↦ M
--------- → M ↠ N
→ M ⟶* M ---------
→ L ↠ N
_⟶⟨_⟩_ : ∀ L {M N} begin_ : ∀ {M N} → (M ↠ N) → (M ↠ N)
→ L ⟶ M begin M↠N = M↠N
→ M ⟶* N
---------
→ L ⟶* N
begin_ : ∀ {M N} → (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, * From term `M`, we can take no steps, giving a step of type `M ↠ M`.
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` * From term `L` we can take a single of type `L ↦ M` followed by zero
followed by zero or more steps of type `M ⟶* N`, or more steps of type `M ↠ N`, giving a step of type `L ↠ N`. It is
giving a step of type `L ⟶* N`, written `L ↦⟨ L↦M ⟩ M↠N`, where `L↦M` and `M↠N` are steps of the
It is written `L ⟨ L⟶M ⟩ M⟶*N`, appropriate type.
where `L⟶M` and `M⟶*N` are steps of the appropriate type.
The notation is chosen to allow us to lay The notation is chosen to allow us to lay out example reductions in an
out example reductions in an appealing way, appealing way, as we will see in the next section.
as we will see in the next section.
We then instantiate the second module to our specific notion As alternative is to define reflexive and transitive closure directly,
of reduction step. as the smallest relation that includes `↦` and is also reflexive
and transitive. We could do so as follows.
\begin{code} \begin{code}
open Chain (Term) (_⟶_) data _↠′_ : Term → Term → Set where
step : ∀ {M N}
→ M ↦ N
------
→ M ↠′ N
refl : ∀ {M}
------
→ M ↠′ M
trans : ∀ {L M N}
→ L ↠′ M
→ M ↠′ N
------
→ L ↠′ N
\end{code} \end{code}
The three constructors specify, respectively, that `↠` includes `↦`
and is reflexive and transitive.
It is a straightforward exercise to show the two are equivalent.
#### Exercise (`closure-equivalent`) #### Exercise (`↠≃↠′`)
Show that the two notions of reflexive and transitive closure Show that the two notions of reflexive and transitive closure
above are equivalent. above are isomorphic.
## Examples ## Examples
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}
_ : four ⟶* `suc `suc `suc `suc `zero _ : four ↠ `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) ]
⟶⟨ β-case-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 (β-case-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 β-case-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}
@ -803,7 +798,7 @@ Thus,
* What is the type of the following term? * What is the type of the following term?
ƛ "s" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · `zero) ƛ "s" ⇒ ` "s" · (` "s" · `zero)
1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) `` 1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) ``
2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ `` 2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ ``
@ -816,7 +811,7 @@ Thus,
* What is the type of the following term? * What is the type of the following term?
(ƛ "s" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · `zero)) · sucᵐ (ƛ "s" ⇒ ` "s" · (` "s" · `zero)) · sucᵐ
1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) `` 1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) ``
2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ `` 2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ ``
@ -910,9 +905,9 @@ and indicates in context `Γ` that term `M` has type `A`.
Context `Γ` provides types for all the free variables in `M`. Context `Γ` provides types for all the free variables in `M`.
For example For example
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · (` "s" · ` "z") ⦂ `ℕ ``
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)) ⦂ `ℕ ⇒ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ `ℕ ⇒ `ℕ ``
* `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)) ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` * `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ ``
Typing is formalised as follows. Typing is formalised as follows.
\begin{code} \begin{code}
@ -923,7 +918,7 @@ data _⊢_⦂_ : Context → Term → Type → Set where
Ax : ∀ {Γ x A} Ax : ∀ {Γ x A}
→ Γ ∋ x ⦂ A → Γ ∋ x ⦂ A
------------- -------------
→ Γ ⊢ ⌊ x ⌋ ⦂ A → Γ ⊢ ` x ⦂ A
-- ⇒-I -- ⇒-I
⊢ƛ : ∀ {Γ x N A B} ⊢ƛ : ∀ {Γ x N A B}
@ -998,7 +993,7 @@ Here `_≟_` is the function that tests two identifiers for equality.
We intend to apply the function only when the We intend to apply the function only when the
two arguments are indeed unequal, and indicate that the second two arguments are indeed unequal, and indicate that the second
case should never arise by postulating a term `impossible` of case should never arise by postulating a term `impossible` of
with the empty type `⊥`. If we use ^C ^N to normalise the term with the empty type `⊥`. If we use `C `N to normalise the term
"a" ≠ "a" "a" ≠ "a"
@ -1016,17 +1011,17 @@ evidence of _any_ proposition whatsoever, regardless of its truth.
Type derivations correspond to trees. In informal notation, here Type derivations correspond to trees. In informal notation, here
is a type derivation for the Church numberal two: is a type derivation for the Church numberal two:
∋s ∋s ∋z ∋s ∋s ∋z
------------------- ⌊_⌋ ------------------- ⌊_⌋ --------------- ⌊_⌋ ------------------- `_ ------------------- `_ --------------- `_
Γ₂ ⊢ ⌊ "s" ⌋ ⦂ A ⇒ A Γ₂ ⊢ ⌊ "s" ⌋ ⦂ A ⇒ A Γ₂ ⊢ ⌊ "z" ⌋ ⦂ A Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "z" ⦂ A
------------------- ⌊_⌋ ------------------------------------------ _·_ ------------------- `_ ------------------------------------------ _·_
Γ₂ ⊢ ⌊ "s" ⌋ ⦂ A ⇒ A Γ₂ ⊢ ⌊ "s" ⌋ · ⌊ "z" ⌋ ⦂ A Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "s" · ` "z" ⦂ A
-------------------------------------------------- _·_ -------------------------------------------------- _·_
Γ₂ ⊢ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A Γ₂ ⊢ ` "s" · (` "s" · ` "z") ⦂ A
---------------------------------------------- ⊢ƛ ---------------------------------------------- ⊢ƛ
Γ₁ ⊢ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A ⇒ A Γ₁ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A
---------------------------------------------------------- ⊢ƛ ---------------------------------------------------------- ⊢ƛ
∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A ⇒ A ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A
where `∋s` and `∋z` abbreviate the two derivations: where `∋s` and `∋z` abbreviate the two derivations:
@ -1113,12 +1108,12 @@ the outermost term in `sucᶜ` in `⊢ƛ`, which is typed using `ƛ`. The
`ƛ` rule in turn takes one argument, which Agda leaves as a hole. `ƛ` rule in turn takes one argument, which Agda leaves as a hole.
⊢sucᶜ = ⊢ƛ { }1 ⊢sucᶜ = ⊢ƛ { }1
?1 : ∅ , "n" ⦂ `ℕ ⊢ `suc ⌊ "n" ⌋ ⦂ `ℕ ?1 : ∅ , "n" ⦂ `ℕ ⊢ `suc ` "n" ⦂ `ℕ
We can fill in the hole by type C-c C-r again. We can fill in the hole by type C-c C-r again.
⊢sucᶜ = ⊢ƛ (⊢suc { }2) ⊢sucᶜ = ⊢ƛ (⊢suc { }2)
?2 : ∅ , "n" ⦂ `ℕ ⊢ ⌊ "n" ⌋ ⦂ `ℕ ?2 : ∅ , "n" ⦂ `ℕ ⊢ ` "n" ⦂ `ℕ
And again. And again.
@ -1157,10 +1152,10 @@ the term `ƛ "x" ⇒ "x"` has type `A ⇒ A` for any type `A`.
### Non-examples ### Non-examples
We can also show that terms are _not_ typeable. For example, here is We can also show that terms are _not_ typeable. For example, here is
a formal proof that it is not possible to type the term `` `zero · a formal proof that it is not possible to type the term
`suc `zero ``. In other words, no type `A` is the type of this term. It `` `zero · `suc `zero ``. It cannot be typed, because doing so
cannot be typed, because doing so requires that the first term in the requires that the first term in the application is both a natural and
application is both a natural and a function. a function.
\begin{code} \begin{code}
nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A) nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A)
@ -1168,11 +1163,11 @@ nope₁ (() · _)
\end{code} \end{code}
As a second example, here is a formal proof that it is not possible to As a second example, here is a formal proof that it is not possible to
type `` ƛ "x" ⇒ ⌊ "x" ⌋ · ⌊ "x" ⌋ `` It cannot be typed, because type `` ƛ "x" ⇒ ` "x" · ` "x" `` It cannot be typed, because
doing so requires types `A` and `B` such that `A ⇒ B ≡ A`. doing so requires types `A` and `B` such that `A ⇒ B ≡ A`.
\begin{code} \begin{code}
nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ⌊ "x" ⌋ · ⌊ "x" ⌋ ⦂ A) nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A)
nope₂ (⊢ƛ (Ax ∋x · Ax ∋x′)) = contradiction (∋-injective ∋x ∋x′) nope₂ (⊢ƛ (Ax ∋x · Ax ∋x′)) = contradiction (∋-injective ∋x ∋x′)
where where
contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A) contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A)
@ -1185,15 +1180,15 @@ nope₂ (⊢ƛ (Ax ∋x · Ax ∋x′)) = contradiction (∋-injective ∋x
For each of the following, given a type `A` for which it is derivable, For each of the following, given a type `A` for which it is derivable,
or explain why there is no such `A`. or explain why there is no such `A`.
1. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ⌊ "y" ⌋ · ⌊ "x" ⌋ ⦂ A `` 1. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ` "y" · ` "x" ⦂ A ``
2. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ⌊ "x" ⌋ · ⌊ "y" ⌋ ⦂ A `` 2. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ` "x" · ` "y" ⦂ A ``
3. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ ⊢ ƛ "x" ⇒ ⌊ "y" ⌋ · ⌊ "x" ⌋ ⦂ A `` 3. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ ⊢ ƛ "x" ⇒ ` "y" · ` "x" ⦂ A ``
For each of the following, give type `A`, `B`, and `C` for which it is derivable, For each of the following, give type `A`, `B`, and `C` for which it is derivable,
or explain why there are no such types. or explain why there are no such types.
1. `` ∅ , "x" ⦂ A ⊢ ⌊ "x" ⌋ · ⌊ "x" ⌋ ⦂ B `` 1. `` ∅ , "x" ⦂ A ⊢ ` "x" · ` "x" ⦂ B ``
2. `` ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ⌊ "x" ⌋ · (⌊ "y" ⌋ · ⌊ "z" ⌋) ⦂ C `` 2. `` ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ` "x" · (` "y" · ` "z") ⦂ C ``
#### Exercise (`mul-type`) #### Exercise (`mul-type`)
@ -1211,7 +1206,8 @@ This chapter uses the following unicode
· 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+27F9: LONG RIGHTWARDS ARROW (\r5, \-->) ↦ U+21A6: RIGHTWARDS ARROW FROM BAR (\mapsto, \r-|)
↠ 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)

365
src/plta/PandP.lagda
View file

@ -15,7 +15,7 @@ Those parts will be revised.]
The last chapter formalised simply-typed lambda calculus and The last chapter formalised simply-typed lambda calculus and
introduced several important relations over it. introduced several important relations over it.
We write `Value M` if term `M` is a value. We write `Value M` if term `M` is a value.
We write `M ⟶ N` if term `M` reduces to term `N`. We write `M ↦ N` if term `M` reduces to term `N`.
And we write `Γ ⊢ M ⦂ A` if in context `Γ` the term `M` has type `A`. And we write `Γ ⊢ M ⦂ A` if in context `Γ` the term `M` has type `A`.
We are particularly concerned with terms typed in the empty context We are particularly concerned with terms typed in the empty context
`∅`, which must be _closed_ (that is, have no _free variables_). `∅`, which must be _closed_ (that is, have no _free variables_).
@ -40,7 +40,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 first we need In the latter case, we would like to apply progress again. But first we need
@ -48,7 +48,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 evaluation. Start with a closed and well-typed term. This gives us a recipe for evaluation. Start with a closed and well-typed term.
By progress, it is either a value, in which case we are done, or it reduces By progress, it is either a value, in which case we are done, or it reduces
@ -87,7 +87,6 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_) open import Function using (_∘_)
open import plta.Isomorphism open import plta.Isomorphism
open import plta.Lambda open import plta.Lambda
open Chain (Term) (_⟶_)
\end{code} \end{code}
@ -192,7 +191,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.
@ -200,7 +199,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
@ -210,7 +209,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.
@ -220,23 +219,23 @@ progress : ∀ {M A}
---------- ----------
→ Progress M → Progress M
progress (Ax ()) progress (Ax ())
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 β-case-zero ... | C-zero = step β-zero
... | C-suc CL = step (β-case-suc (value CL)) ... | C-suc CL = step (β-suc (value CL))
progress (⊢μ ⊢M) = step β-μ progress (⊢μ ⊢M) = step β-μ
\end{code} \end{code}
We induct on the evidence that `M` is well-typed. We induct on the evidence that `M` is well-typed.
Let's unpack the first three cases. Let's unpack the first three cases.
@ -249,7 +248,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`
@ -257,7 +256,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
@ -269,7 +268,7 @@ Let's unpack the first three cases.
since we are in an application leads to the since we are in an application leads to the
conclusion that `L` must be a lambda conclusion that `L` must be a lambda
abstraction. We also have evidence that `M` is abstraction. We also have evidence that `M` is
a value, so our original term steps by `β-ƛ·`. a value, so our original term steps by `β-ƛ`.
The remaining cases are similar. If by induction we have a The remaining cases are similar. If by induction we have a
`step` case we apply a `ξ` rule, and if we have a `done` case `step` case we apply a `ξ` rule, and if we have a `done` case
@ -289,11 +288,11 @@ 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
implicit and so must be written out in full. In the case for `β-ƛ·` implicit and so must be written out in full. In the case for `β-ƛ`
this requires that we match against the lambda expression `L` to this requires that we match against the lambda expression `L` to
determine its bound variable and body, `ƛ x ⇒ N`, so we can show that determine its bound variable and body, `ƛ x ⇒ N`, so we can show that
`L · M` reduces to `N [ x := M ]`. `L · M` reduces to `N [ x := M ]`.
@ -305,7 +304,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
@ -370,7 +369,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
@ -404,7 +403,6 @@ ext : ∀ {Γ Δ}
→ (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
----------------------------------------------------- -----------------------------------------------------
→ (∀ {x y A B} → Γ , y ⦂ B ∋ x ⦂ A → Δ , y ⦂ B ∋ x ⦂ A) → (∀ {x y A B} → Γ , y ⦂ B ∋ x ⦂ A → Δ , y ⦂ B ∋ x ⦂ A)
ext ρ Z = Z ext ρ Z = Z
ext ρ (S x≢y ∋x) = S x≢y (ρ ∋x) ext ρ (S x≢y ∋x) = S x≢y (ρ ∋x)
\end{code} \end{code}
@ -595,9 +593,9 @@ Now that naming is resolved, let's unpack the first three cases.
* In the variable case, we must show * In the variable case, we must show
∅ ⊢ V ⦂ B ∅ ⊢ V ⦂ B
Γ , y ⦂ B ⊢ ⌊ x ⌋ ⦂ A Γ , y ⦂ B ⊢ ` x ⦂ A
------------------------ ------------------------
Γ ⊢ ⌊ x ⌋ [ y := V ] ⦂ A Γ ⊢ ` x [ y := V ] ⦂ A
where the second hypothesis follows from: where the second hypothesis follows from:
@ -645,7 +643,7 @@ Now that naming is resolved, let's unpack the first three cases.
x ≢ y x ≢ y
Γ ∋ x ⦂ A Γ ∋ x ⦂ A
------------- -------------
Γ ⊢ ⌊ x ⌋ ⦂ A Γ ⊢ ` x ⦂ A
which follows by the typing rule for variables. which follows by the typing rule for variables.
@ -735,20 +733,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 (Ax ()) preserve (Ax ())
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) β-case-zero = ⊢M preserve (⊢case ⊢zero ⊢M ⊢N) β-zero = ⊢M
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-case-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.
@ -757,9 +755,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
@ -771,13 +769,13 @@ 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
from which the typing of the right-hand side follows immediately. from which the typing of the right-hand side follows immediately.
* Rule `β-ƛ·`. We have * Rule `β-ƛ`. We have
Value V Value V
---------------------------- ----------------------------
@ -813,15 +811,17 @@ well-typed term to its value, if it has one.
Some terms may reduce forever. Here is a simple example. Some terms may reduce forever. Here is a simple example.
\begin{code} \begin{code}
sucμ = μ "x" ⇒ `suc (` "x")
_ = _ =
begin begin
μ "x" ⇒ `suc ⌊ "x" ⌋ sucμ
⟶⟨ β-μ ⟩ ↦⟨ β-μ ⟩
`suc (μ "x" ⇒ `suc ⌊ "x" ⌋) `suc sucμ
⟶⟨ ξ-suc β-μ ⟩ ↦⟨ ξ-suc β-μ ⟩
`suc `suc (μ "x" ⇒ `suc ⌊ "x" ⌋) `suc `suc sucμ
⟶⟨ ξ-suc (ξ-suc β-μ) ⟩ ↦⟨ ξ-suc (ξ-suc β-μ) ⟩
`suc `suc `suc (μ "x" ⇒ `suc ⌊ "x" ⌋) `suc `suc `suc sucμ
-- ... -- ...
∎ ∎
\end{code} \end{code}
@ -871,7 +871,7 @@ well-typed and an indication of whether reduction finished.
data Steps (L : Term) (A : Type) : Set where data Steps (L : Term) (A : Type) : Set where
steps : ∀ {N} steps : ∀ {N}
→ L ⟶* N → L ↠ N
→ ∅ ⊢ N ⦂ A → ∅ ⊢ N ⦂ A
→ Finished N → Finished N
---------- ----------
@ -886,18 +886,18 @@ eval : ∀ {L A}
→ ∅ ⊢ L ⦂ A → ∅ ⊢ L ⦂ A
--------- ---------
→ Steps L A → Steps L A
eval {L} (gas zero) ⊢L = steps (L ∎) ⊢L out-of-gas eval {L} (gas zero) ⊢L = steps (L ∎) ⊢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 ∎) ⊢L (done VL) ... | done VL = steps (L ∎) ⊢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 ⊢N fin = steps (L ⟶⟨ L⟶M ⟩ M⟶*N) ⊢N fin ... | steps M↠N ⊢N fin = steps (L ↦⟨ L↦M ⟩ M↠N) ⊢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.
@ -905,165 +905,187 @@ 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.
### Examples ### Examples
We can now use Agda to compute the reduction sequence for two plus two We can now use Agda to compute the non-terminating reduction
given in the preceding chapter. sequence given earlier. First, we show that the term `sucμ`
is well-typed.
\begin{code}
⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ` "x" ⦂ `ℕ
⊢sucμ = ⊢μ (⊢suc (Ax ∋x))
where
∋x = Z
\end{code}
To show the first three steps of the infinite reduction
sequence, we evaluate with three steps worth of gas.
\begin{code}
_ : eval (gas 3) ⊢sucμ ≡
steps
(μ "x" ⇒ `suc ` "x" ↦⟨ β-μ ⟩
`suc (μ "x" ⇒ `suc ` "x") ↦⟨ ξ-suc β-μ ⟩
`suc (`suc (μ "x" ⇒ `suc ` "x")) ↦⟨ ξ-suc (ξ-suc β-μ) ⟩
`suc (`suc (`suc (μ "x" ⇒ `suc ` "x"))) ∎)
(⊢suc (⊢suc (⊢suc (⊢μ (⊢suc (Ax Z)))))) out-of-gas
_ = refl
\end{code}
Similarly, we can use Agda to compute the reduction sequence for two plus two
given in the preceding chapter. Supplying 100 steps of gas is more than enough.
\begin{code} \begin{code}
_ : eval (gas 100) ⊢four ≡ _ : eval (gas 100) ⊢four ≡
steps steps
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· `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" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· ⌊ "n" ⌋) · ` "n")
])) ]))
· `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
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· ⌊ "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
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· `suc (`suc `zero)) · `suc (`suc `zero))
] ]
⟶⟨ β-case-suc (V-suc V-zero) ⟩ ↦⟨ β-suc (V-suc V-zero) ⟩
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· `suc `zero · `suc `zero
· `suc (`suc `zero)) · `suc (`suc `zero))
⟶⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩ ↦⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc `suc
((ƛ "m" ⇒ ((ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `case ` "m" [zero⇒ ` "n" |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· ⌊ "n" ⌋) · ` "n")
])) ]))
· `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" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· ⌊ "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
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· `suc (`suc `zero)) · `suc (`suc `zero))
] ]
⟶⟨ ξ-suc (β-case-suc V-zero) ⟩ ↦⟨ ξ-suc (β-suc V-zero) ⟩
`suc `suc
(`suc (`suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· `zero · `zero
· `suc (`suc `zero))) · `suc (`suc `zero)))
⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩ ↦⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc `suc
(`suc (`suc
((ƛ "m" ⇒ ((ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `case ` "m" [zero⇒ ` "n" |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· ⌊ "n" ⌋) · ` "n")
])) ]))
· `zero · `zero
· `suc (`suc `zero))) · `suc (`suc `zero)))
⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ· V-zero))) ⟩ ↦⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc `suc
(`suc (`suc
((ƛ "n" ⇒ ((ƛ "n" ⇒
`case `zero [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `case `zero [zero⇒ ` "n" |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· ⌊ "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" ⇒
@ -1071,21 +1093,21 @@ _ : eval (gas 100) ⊢four ≡
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋) `case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
]))) ])))
· ⌊ "m" ⌋ · ` "m"
· `suc (`suc `zero)) · `suc (`suc `zero))
]) ])
⟶⟨ ξ-suc (ξ-suc β-case-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎) ↦⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `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)))))
_ = refl _ = refl
\end{code} \end{code}
The example above was generated by using ^C ^N to normalise the 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 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 right-hand side of the equation. The example reduction of the
the example reduction of the previous chapter, by writing `plus` previous chapter was derived from this result, by writing `plus` and
and `two` in place of the corresponding terms and reformatting. `two` in place of their corresponding expansions and reformatting.
Similarly, can evaluate the corresponding term for Church numerals. Similarly, can evaluate the corresponding term for Church numerals.
\begin{code} \begin{code}
@ -1093,88 +1115,73 @@ _ : eval (gas 100) ⊢fourᶜ ≡
steps steps
((ƛ "m" ⇒ ((ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "m" ⌋ · ⌊ "s" ⌋ · (⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋))))) (ƛ "s" ⇒ (ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z")))))
· (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
· (ƛ "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" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · ⌊ "s" ⌋ · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" ·
(⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋)))) (` "n" · ` "s" · ` "z"))))
· (ƛ "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))) ∎)
(⊢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)))))
_ = refl _ = refl
\end{code} \end{code}
Again, the example in the previous section was derived by editing the
We can also derive the non-terminating example. above.
\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 `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`.
@ -1186,7 +1193,7 @@ with case expressions and one not involving case expressions.
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.
@ -1200,7 +1207,7 @@ Using progress and preservation, it is easy to show that well-typed terms don't
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}
@ -1223,8 +1230,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}
@ -1232,21 +1239,21 @@ Any descendant of a well-typed term is well-typed.
\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* ⊢M (M ∎) = ⊢M preserve* ⊢M (M ∎) = ⊢M
preserve* ⊢L (L ⟶⟨ L⟶M ⟩ M⟶*N) = preserve* (preserve ⊢L L⟶M) M⟶*N preserve* ⊢L (L ↦⟨ L↦M ⟩ M↠N) = preserve* (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 (preserve* ⊢M M⟶*N) wttdgs′ ⊢M M↠N = unstuck (preserve* ⊢M M↠N)
\end{code} \end{code}
@ -1261,7 +1268,7 @@ and preservation theorems for the simply typed lambda-calculus.
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:
@ -1286,10 +1293,10 @@ 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
@ -1305,7 +1312,7 @@ false, give a counterexample.
#### Quiz #### Quiz
Suppose instead that we remove the rule `ξ·₁` from the `⟶` Suppose instead that we remove the rule `ξ·₁` from the step
relation. Which of the following properties remain relation. Which of the following properties remain
true in the absence of this rule? For each one, write either true in the absence of this rule? For each one, write either
"remains true" or else "becomes false." If a property becomes "remains true" or else "becomes false." If a property becomes