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

Remove tick from constructors

Browse source
This commit is contained in:
wadler 2019-09-02 19:15:50 +01:00
parent f68782dccb
commit 07894d0d79
6 changed files with 535 additions and 550 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

407
src/plfa/part2/DeBruijn.lagda.md
View file

@ -116,7 +116,7 @@ that it is _intrinsically typed_. In the previous two chapters,
the definition of terms and the definition of types are
completely separate. All terms have type `Term`, and nothing
in Agda prevents one from writing a nonsense term such as
`` `zero · `suc `zero `` which has no type. Such terms that
`` zero · suc zero `` which has no type. Such terms that
exist independent of types are sometimes called _preterms_ or
_raw terms_. Here we are going to replace the type `Term` of
raw terms by the type `Γ ⊢ A` of intrinsically-typed terms
@ -140,7 +140,7 @@ the term that adds two naturals:
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
case ` "m"
[zero⇒ ` "n"
|suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
|suc "m" ⇒ suc (` "+" · ` "m" · ` "n") ]
Note variable `"m"` is bound twice, once in a lambda abstraction
and once in the successor branch of the case. Any appearance
@ -162,8 +162,8 @@ Here is its corresponding type derivation:
The two definitions are in close correspondence, where in
addition to the previous correspondences we have:
* `` `zero `` corresponds to `⊢zero`
* `` `suc_ `` corresponds to `⊢suc`
* `` zero `` corresponds to `⊢zero`
* `` suc `` corresponds to `⊢suc`
* `` case_[zero⇒_|suc_⇒_] `` corresponds to `⊢case`
* `μ_⇒_` corresponds to `⊢μ`
@ -177,7 +177,7 @@ of `"n"` but accessed in different contexts, the first where
Here is the term and its type derivation in the notation of this chapter:
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
plus = μ ƛ ƛ case (# 1) (# 0) (`suc (# 3 · # 0 · # 1))
plus = μ ƛ ƛ case (# 1) (# 0) (suc (# 3 · # 0 · # 1))
Reading from left to right, each de Bruijn index corresponds
to a lookup derivation:
@ -230,7 +230,6 @@ infixr 7 _⇒_
infix 5 ƛ_
infix 5 μ_
infixl 7 _·_
infix 8 `suc_
infix 9 `_
infix 9 S_
infix 9 #_
@ -300,7 +299,7 @@ Constructor `S` no longer requires an additional parameter,
since without names shadowing is no longer an issue. Now
constructors `Z` and `S` correspond even more closely to the
constructors `here` and `there` for the element-of relation
`_∈_` on lists, as well as to constructors `zero` and `suc`
`_∈_` on lists, as well as to constructors zero` and suc`
for natural numbers.
For example, consider the following old-style lookup
@ -353,11 +352,11 @@ data _⊢_ : Context → Type → Set where
---------
→ Γ ⊢ B
`zero : ∀ {Γ}
zero : ∀ {Γ}
---------
→ Γ ⊢ `ℕ
`suc_ : ∀ {Γ}
suc : ∀ {Γ}
→ Γ ⊢ `ℕ
------
→ Γ ⊢ `ℕ
@ -460,10 +459,10 @@ for comparison.
First, computing two plus two on naturals:
```
two : ∀ {Γ} → Γ ⊢ `ℕ
two = `suc `suc `zero
two = suc (suc zero)
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
plus = μ ƛ ƛ (case (# 1) (# 0) (suc (# 3 · # 0 · # 1)))
2+2 : ∀ {Γ} → Γ ⊢ `ℕ
2+2 = plus · two · two
@ -483,10 +482,10 @@ plusᶜ : ∀ {Γ A} → Γ ⊢ Ch A ⇒ Ch A ⇒ Ch A
plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ
sucᶜ = ƛ `suc (# 0)
sucᶜ = ƛ suc (# 0)
2+2ᶜ : ∀ {Γ} → Γ ⊢ `ℕ
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero
```
As before we generalise everything to arbitrary
contexts. While we are at it, we also generalise `twoᶜ` and
@ -550,8 +549,8 @@ rename : ∀ {Γ Δ}
rename ρ (` x) = ` (ρ x)
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
rename ρ (`zero) = `zero
rename ρ (`suc M) = `suc (rename ρ M)
rename ρ (zero) = zero
rename ρ (suc M) = suc (rename ρ M)
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
rename ρ (μ N) = μ (rename (ext ρ) N)
```
@ -664,8 +663,8 @@ subst : ∀ {Γ Δ}
subst σ (` k) = σ k
subst σ (ƛ N) = ƛ (subst (exts σ) N)
subst σ (L · M) = (subst σ L) · (subst σ M)
subst σ (`zero) = `zero
subst σ (`suc M) = `suc (subst σ M)
subst σ (zero) = zero
subst σ (suc M) = suc (subst σ M)
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
subst σ (μ N) = μ (subst (exts σ) N)
```
@ -719,10 +718,10 @@ M₂ : ∅ , `ℕ ⇒ `ℕ ⊢ `ℕ ⇒ `ℕ
M₂ = ƛ # 1 · (# 1 · # 0)
M₃ : ∅ ⊢ `ℕ ⇒ `ℕ
M₃ = ƛ `suc # 0
M₃ = ƛ suc (# 0)
M₄ : ∅ ⊢ `ℕ ⇒ `ℕ
M₄ = ƛ (ƛ `suc # 0) · ((ƛ `suc # 0) · # 0)
M₄ = ƛ (ƛ suc (# 0)) · ((ƛ suc (# 0)) · # 0)
_ : M₂ [ M₃ ] ≡ M₄
_ = refl
@ -732,8 +731,8 @@ Previously, we presented an example of substitution that we
did not implement, since it needed to rename the bound
variable to avoid capture:
* `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · `zero ] `` should yield
`` ƛ "z" ⇒ ` "z" · (` "x" · `zero) ``
* `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · zero ] `` should yield
`` ƛ "z" ⇒ ` "z" · (` "x" · zero) ``
Say the bound `"x"` has type `` `ℕ ⇒ `ℕ ``, the substituted
`"y"` has type `` `ℕ ``, and the free `"x"` also has type ``
@ -743,10 +742,10 @@ M₅ : ∅ , `ℕ ⇒ `ℕ , `ℕ ⊢ (`ℕ ⇒ `ℕ) ⇒ `ℕ
M₅ = ƛ # 0 · # 1
M₆ : ∅ , `ℕ ⇒ `ℕ ⊢ `ℕ
M₆ = # 0 · `zero
M₆ = # 0 · zero
M₇ : ∅ , `ℕ ⇒ `ℕ ⊢ (`ℕ ⇒ `ℕ) ⇒ `ℕ
M₇ = ƛ (# 0 · (# 1 · `zero))
M₇ = ƛ (# 0 · (# 1 · zero))
_ : M₅ [ M₆ ] ≡ M₇
_ = refl
@ -777,15 +776,15 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
V-zero : ∀ {Γ}
-----------------
→ Value (`zero {Γ})
→ Value (zero {Γ})
V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
→ Value V
--------------
→ Value (`suc V)
→ Value (suc V)
```
Here `zero` requires an implicit parameter to aid inference,
Here zero` requires an implicit parameter to aid inference,
much in the same way that `[]` did in
[Lists]({{ site.baseurl }}/Lists/).
@ -822,7 +821,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
→ M —→ M′
-----------------
→ `suc M —→ `suc M′
→ suc M —→ suc M′
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ L —→ L′
@ -831,12 +830,12 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
-------------------
→ case `zero M N —→ M
→ case zero M N —→ M
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ Value V
----------------------------
→ case (`suc V) M N —→ N [ V ]
→ case (suc V) M N —→ N [ V ]
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
----------------
@ -889,86 +888,86 @@ We reiterate each of our previous examples. First, the Church
numeral two applied to the successor function and zero yields
the natural number two:
```
_ : twoᶜ · sucᶜ · `zero {∅} —↠ `suc `suc `zero
_ : twoᶜ · sucᶜ · zero {∅} —↠ suc (suc zero)
_ =
begin
twoᶜ · sucᶜ · `zero
twoᶜ · sucᶜ · zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ (sucᶜ · (sucᶜ · # 0))) · `zero
(ƛ (sucᶜ · (sucᶜ · # 0))) · zero
—→⟨ β-ƛ V-zero ⟩
sucᶜ · (sucᶜ · `zero)
sucᶜ · (sucᶜ · zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
sucᶜ · `suc `zero
sucᶜ · suc zero
—→⟨ β-ƛ (V-suc V-zero) ⟩
`suc (`suc `zero)
suc (suc zero)
∎
```
As before, we need to supply an explicit context to `` `zero ``.
As before, we need to supply an explicit context to `` zero ``.
Next, a sample reduction demonstrating that two plus two is four:
```
_ : plus {∅} · two · two —↠ `suc `suc `suc `suc `zero
_ : plus {∅} · two · two —↠ suc (suc (suc (suc zero)))
_ =
plus · two · two
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · two · two
(ƛ ƛ case (` S Z) (` Z) (suc (plus · ` Z · ` S Z))) · two · two
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ case two (` Z) (`suc (plus · ` Z · ` S Z))) · two
(ƛ case two (` Z) (suc (plus · ` Z · ` S Z))) · two
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
case two two (`suc (plus · ` Z · two))
case two two (suc (plus · ` Z · two))
—→⟨ β-suc (V-suc V-zero) ⟩
`suc (plus · `suc `zero · two)
suc (plus · suc zero · two)
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
· `suc `zero · two)
suc ((ƛ ƛ case (` S Z) (` Z) (suc (plus · ` Z · ` S Z)))
· suc zero · two)
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc ((ƛ case (`suc `zero) (` Z) (`suc (plus · ` Z · ` S Z))) · two)
suc ((ƛ case (suc zero) (` Z) (suc (plus · ` Z · ` S Z))) · two)
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
`suc (case (`suc `zero) (two) (`suc (plus · ` Z · two)))
suc (case (suc zero) (two) (suc (plus · ` Z · two)))
—→⟨ ξ-suc (β-suc V-zero) ⟩
`suc (`suc (plus · `zero · two))
suc (suc (plus · zero · two))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc (`suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
· `zero · two))
suc (suc ((ƛ ƛ case (` S Z) (` Z) (suc (plus · ` Z · ` S Z)))
· zero · two))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc (`suc ((ƛ case `zero (` Z) (`suc (plus · ` Z · ` S Z))) · two))
suc (suc ((ƛ case zero (` Z) (suc (plus · ` Z · ` S Z))) · two))
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
`suc (`suc (case `zero (two) (`suc (plus · ` Z · two))))
suc (suc (case zero (two) (suc (plus · ` Z · two))))
—→⟨ ξ-suc (ξ-suc β-zero) ⟩
`suc (`suc (`suc (`suc `zero)))
suc (suc (suc (suc zero)))
∎
```
And finally, a similar sample reduction for Church numerals:
```
_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero {∅}
_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero —↠ suc (suc (suc (suc (zero {∅}))))
_ =
begin
plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero
—→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
(ƛ ƛ ƛ twoᶜ · ` S Z · (` S S Z · ` S Z · ` Z)) · twoᶜ · sucᶜ · `zero
(ƛ ƛ ƛ twoᶜ · ` S Z · (` S S Z · ` S Z · ` Z)) · twoᶜ · sucᶜ · zero
—→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ ƛ twoᶜ · ` S Z · (twoᶜ · ` S Z · ` Z)) · sucᶜ · `zero
(ƛ ƛ twoᶜ · ` S Z · (twoᶜ · ` S Z · ` Z)) · sucᶜ · zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` Z)) · `zero
(ƛ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` Z)) · zero
—→⟨ β-ƛ V-zero ⟩
twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero)
twoᶜ · sucᶜ · (twoᶜ · sucᶜ · zero)
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ sucᶜ · (sucᶜ · ` Z)) · (twoᶜ · sucᶜ · `zero)
(ƛ sucᶜ · (sucᶜ · ` Z)) · (twoᶜ · sucᶜ · zero)
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ sucᶜ · (sucᶜ · ` Z)) · ((ƛ sucᶜ · (sucᶜ · ` Z)) · `zero)
(ƛ sucᶜ · (sucᶜ · ` Z)) · ((ƛ sucᶜ · (sucᶜ · ` Z)) · zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ sucᶜ · (sucᶜ · ` Z)) · (sucᶜ · (sucᶜ · `zero))
(ƛ sucᶜ · (sucᶜ · ` Z)) · (sucᶜ · (sucᶜ · zero))
—→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
(ƛ sucᶜ · (sucᶜ · ` Z)) · (sucᶜ · `suc `zero)
(ƛ sucᶜ · (sucᶜ · ` Z)) · (sucᶜ · suc zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
(ƛ sucᶜ · (sucᶜ · ` Z)) · `suc (`suc `zero)
(ƛ sucᶜ · (sucᶜ · ` Z)) · suc (suc zero)
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
sucᶜ · (sucᶜ · `suc (`suc `zero))
sucᶜ · (sucᶜ · suc (suc 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))) ⟩
`suc (`suc (`suc (`suc `zero)))
suc (suc (suc (suc zero)))
∎
```
@ -1023,8 +1022,8 @@ progress (L · M) with progress L
... | done V-ƛ with progress M
... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′)
... | done VM = step (β-ƛ VM)
progress (`zero) = done V-zero
progress (`suc M) with progress M
progress (zero) = done V-zero
progress (suc M) with progress M
... | step M—→M′ = step (ξ-suc M—→M′)
... | done VM = done (V-suc VM)
progress (case L M N) with progress L
@ -1091,23 +1090,23 @@ to invoke preservation.
## Examples
We reiterate each of our previous examples. We re-define the term
`sucμ` that loops forever:
sucμ` that loops forever:
```
sucμ : ∅ ⊢ `ℕ
sucμ = μ (`suc (# 0))
sucμ = μ (suc (# 0))
```
To compute the first three steps of the infinite reduction sequence,
we evaluate with three steps worth of gas:
```
_ : eval (gas 3) sucμ ≡
steps
(μ `suc ` Z
(μ suc (` Z)
—→⟨ β-μ ⟩
`suc (μ `suc ` Z)
suc (μ suc (` Z))
—→⟨ ξ-suc β-μ ⟩
`suc (`suc (μ `suc ` Z))
suc (suc (μ suc (` Z)))
—→⟨ ξ-suc (ξ-suc β-μ) ⟩
`suc (`suc (`suc (μ `suc ` Z)))
suc (suc (suc (μ suc (` Z))))
∎)
out-of-gas
_ = refl
@ -1115,17 +1114,17 @@ _ = refl
The Church numeral two applied to successor and zero:
```
_ : eval (gas 100) (twoᶜ · sucᶜ · `zero) ≡
_ : eval (gas 100) (twoᶜ · sucᶜ · zero) ≡
steps
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) · `zero
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ suc (` Z)) · zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) · `zero
(ƛ (ƛ suc (` Z)) · ((ƛ suc (` Z)) · ` Z)) · zero
—→⟨ β-ƛ V-zero ⟩
(ƛ `suc ` Z) · ((ƛ `suc ` Z) · `zero)
(ƛ suc (` Z)) · ((ƛ suc (` Z)) · zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ `suc ` Z) · `suc `zero
(ƛ suc (` Z)) · suc zero
—→⟨ β-ƛ (V-suc V-zero) ⟩
`suc (`suc `zero)
suc (suc zero)
∎)
(done (V-suc (V-suc V-zero)))
_ = refl
@ -1135,155 +1134,141 @@ Two plus two is four:
```
_ : eval (gas 100) (plus · two · two) ≡
steps
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· `suc (`suc `zero)
· `suc (`suc `zero)
((μ
(ƛ
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· suc (suc zero)
· suc (suc zero)
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ
(ƛ
(ƛ
case (` (S Z)) (` Z)
(`suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z)))))
· `suc (`suc `zero)
· `suc (`suc `zero)
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ
case (`suc (`suc `zero)) (` Z)
(`suc
case (` (S Z)) (` Z)
(suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z))))
· `suc (`suc `zero)
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
case (`suc (`suc `zero)) (`suc (`suc `zero))
(`suc
· ` (S Z)))))
· suc (suc zero)
· suc (suc zero)
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ
case (suc (suc zero)) (` Z)
(suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· `suc (`suc `zero)))
—→⟨ β-suc (V-suc V-zero) ⟩
`suc
· ` (S Z))))
· suc (suc zero)
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
case (suc (suc zero)) (suc (suc zero))
(suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· `suc `zero
· `suc (`suc `zero))
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· suc (suc zero)))
—→⟨ β-suc (V-suc V-zero) ⟩
suc
((μ
(ƛ
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· suc zero
· suc (suc zero))
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc
suc
((ƛ
(ƛ
case (` (S Z)) (` Z)
(suc
((μ
(ƛ
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z)))))
· suc zero
· suc (suc zero))
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
suc
((ƛ
case (suc zero) (` Z)
(suc
((μ
(ƛ
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z))))
· suc (suc zero))
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
suc
(case (suc zero) (suc (suc zero))
(suc
((μ
(ƛ
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· suc (suc zero))))
—→⟨ ξ-suc (β-suc V-zero) ⟩
suc
(suc
((μ
(ƛ
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· zero
· suc (suc zero)))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
suc
(suc
((ƛ
(ƛ
case (` (S Z)) (` Z)
(`suc
(suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z)))))
· `suc `zero
· `suc (`suc `zero))
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc
· zero
· suc (suc zero)))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
suc
(suc
((ƛ
case (`suc `zero) (` Z)
(`suc
case zero (` Z)
(suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z))))
· `suc (`suc `zero))
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
`suc
case (`suc `zero) (`suc (`suc `zero))
(`suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· `suc (`suc `zero)))
—→⟨ ξ-suc (β-suc V-zero) ⟩
`suc
(`suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· `zero
· `suc (`suc `zero)))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc
(`suc
((ƛ
(ƛ
case (` (S Z)) (` Z)
(`suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z)))))
· `zero
· `suc (`suc `zero)))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc
(`suc
((ƛ
case `zero (` Z)
(`suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· ` (S Z))))
· `suc (`suc `zero)))
· suc (suc zero)))
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
`suc
(`suc
case `zero (`suc (`suc `zero))
(`suc
suc
(suc
(case zero (suc (suc zero))
(suc
((μ
(ƛ
(ƛ
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
(ƛ case (` (S Z)) (` Z) (suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
· ` Z
· `suc (`suc `zero))))
—→⟨ ξ-suc (ξ-suc β-zero) ⟩
`suc (`suc (`suc (`suc `zero)))
∎)
(done (V-suc (V-suc (V-suc (V-suc V-zero)))))
· suc (suc zero)))))
—→⟨ ξ-suc (ξ-suc β-zero) ⟩ suc (suc (suc (suc zero))) ∎)
(done (V-suc (V-suc (V-suc (V-suc V-zero)))))
_ = refl
```
And the corresponding term for Church numerals:
```
_ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
_ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero) ≡
steps
((ƛ
(ƛ
(ƛ (ƛ ` (S (S (S Z))) · ` (S Z) · (` (S (S Z)) · ` (S Z) · ` Z)))))
· (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z)))
· (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z)))
· (ƛ `suc ` Z)
· `zero
· (ƛ suc (` Z))
· zero
—→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
(ƛ
(ƛ
@ -1291,43 +1276,43 @@ _ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
(ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · ` (S Z) ·
(` (S (S Z)) · ` (S Z) · ` Z))))
· (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z)))
· (ƛ `suc ` Z)
· `zero
· (ƛ suc (` Z))
· zero
—→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ
(ƛ
(ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · ` (S Z) ·
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · ` (S Z) · ` Z)))
· (ƛ `suc ` Z)
· `zero
· (ƛ suc (` Z))
· zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ
(ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) ·
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) · ` Z))
· `zero
(ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ suc (` Z)) ·
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ suc (` Z)) · ` Z))
· zero
—→⟨ β-ƛ V-zero ⟩
(ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) ·
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) · `zero)
(ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ suc (` Z)) ·
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ suc (` Z)) · zero)
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) ·
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) · `zero)
(ƛ (ƛ suc (` Z)) · ((ƛ suc (` Z)) · ` Z)) ·
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ suc (` Z)) · zero)
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) ·
((ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) · `zero)
(ƛ (ƛ suc (` Z)) · ((ƛ suc (` Z)) · ` Z)) ·
((ƛ (ƛ suc (` Z)) · ((ƛ suc (` Z)) · ` Z)) · zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) ·
((ƛ `suc ` Z) · ((ƛ `suc ` Z) · `zero))
(ƛ (ƛ suc (` Z)) · ((ƛ suc (` Z)) · ` Z)) ·
((ƛ suc (` Z)) · ((ƛ suc (` Z)) · zero))
—→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
(ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) ·
((ƛ `suc ` Z) · `suc `zero)
(ƛ (ƛ suc (` Z)) · ((ƛ suc (` Z)) · ` Z)) ·
((ƛ suc (` Z)) · suc zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
(ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) · `suc (`suc `zero)
(ƛ (ƛ suc (` Z)) · ((ƛ suc (` Z)) · ` Z)) · suc (suc zero)
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
(ƛ `suc ` Z) · ((ƛ `suc ` Z) · `suc (`suc `zero))
(ƛ suc (` Z)) · ((ƛ suc (` Z)) · suc (suc zero))
—→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ `suc ` Z) · `suc (`suc (`suc `zero))
(ƛ suc (` Z)) · suc (suc (suc 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)))))
_ = refl

41
src/plfa/part2/Inference.lagda.md
View file

@ -192,8 +192,8 @@ We can extract the grammar for terms from the above:
L⁻, M⁻, N⁻ ::= terms with inherited type
ƛ x ⇒ N abstraction
`zero zero
`suc M⁻ successor
zero zero
suc M⁻ successor
case L⁺ [zero⇒ M⁻ |suc x ⇒ N⁻ ] case
μ x ⇒ N fixpoint
M ↑ switch to synthesized
@ -290,7 +290,6 @@ infix 5 μ_⇒_
infix 6 _↑
infix 6 _↓_
infixl 7 _·_
infix 8 `suc_
infix 9 `_
```
@ -324,8 +323,8 @@ data Term⁺ where
data Term⁻ where
ƛ_⇒_ : Id → Term⁻ → Term⁻
`zero : Term⁻
`suc_ : Term⁻ → Term⁻
zero : Term⁻
suc : Term⁻ → Term⁻
`case_[zero⇒_|suc_⇒_] : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
μ_⇒_ : Id → Term⁻ → Term⁻
_↑ : Term⁺ → Term⁻
@ -342,12 +341,12 @@ We can recreate the examples from preceding chapters.
First, computing two plus two on naturals:
```
two : Term⁻
two = `suc (`suc `zero)
two = suc (suc zero)
plus : Term⁺
plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case (` "m") [zero⇒ ` "n" ↑
|suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
|suc "m" ⇒ suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
↓ (`ℕ ⇒ `ℕ ⇒ `ℕ)
2+2 : Term⁺
@ -370,10 +369,10 @@ plusᶜ = (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
↓ (Ch ⇒ Ch ⇒ Ch)
sucᶜ : Term⁻
sucᶜ = ƛ "x" ⇒ `suc (` "x" ↑)
sucᶜ = ƛ "x" ⇒ suc (` "x" ↑)
2+2ᶜ : Term⁺
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero
```
The only type decoration required is for `plusᶜ`. One is not even
required for `sucᶜ`, which inherits its type as an argument of `plusᶜ`.
@ -429,12 +428,12 @@ data _⊢_↓_ where
⊢zero : ∀ {Γ}
--------------
→ Γ ⊢ `zero ↓ `ℕ
→ Γ ⊢ zero ↓ `ℕ
⊢suc : ∀ {Γ M}
→ Γ ⊢ M ↓ `ℕ
---------------
→ Γ ⊢ `suc M ↓ `ℕ
→ Γ ⊢ suc M ↓ `ℕ
⊢case : ∀ {Γ L M x N A}
→ Γ ⊢ L ↑ `ℕ
@ -763,12 +762,12 @@ inherit Γ (ƛ x ⇒ N) `ℕ = no (λ())
inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
... | no ¬⊢N = no (λ{ (⊢ƛ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N = yes (⊢ƛ ⊢N)
inherit Γ `zero `ℕ = yes ⊢zero
inherit Γ `zero (A ⇒ B) = no (λ())
inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
inherit Γ zero `ℕ = yes ⊢zero
inherit Γ zero (A ⇒ B) = no (λ())
inherit Γ (suc M) `ℕ with inherit Γ M `ℕ
... | no ¬⊢M = no (λ{ (⊢suc ⊢M) → ¬⊢M ⊢M })
... | yes ⊢M = yes (⊢suc ⊢M)
inherit Γ (`suc M) (A ⇒ B) = no (λ())
inherit Γ (suc M) (A ⇒ B) = no (λ())
inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
... | no ¬∃ = no (λ{ (⊢case ⊢L _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
... | yes ⟨ _ ⇒ _ , ⊢L ⟩ = no (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
@ -961,7 +960,7 @@ _ = refl
Zero inherits a function type:
```
_ : synthesize ∅ (`zero ↓ `ℕ ⇒ `ℕ) ≡ no _
_ : synthesize ∅ (zero ↓ `ℕ ⇒ `ℕ) ≡ no _
_ = refl
```
@ -973,21 +972,21 @@ _ = refl
Successor of an ill-typed term:
```
_ : synthesize ∅ (`suc twoᶜ ↓ `ℕ) ≡ no _
_ : synthesize ∅ (suc twoᶜ ↓ `ℕ) ≡ no _
_ = refl
```
Case of a term with a function type:
```
_ : synthesize ∅
((`case (twoᶜ ↓ Ch) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
((`case (twoᶜ ↓ Ch) [zero⇒ zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl
```
Case of an ill-typed term:
```
_ : synthesize ∅
((`case (twoᶜ ↓ `ℕ) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
((`case (twoᶜ ↓ `ℕ) [zero⇒ zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl
```
@ -1043,8 +1042,8 @@ there are two mutually recursive erasure functions:
∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻
∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻
∥ ⊢zero ∥⁻ = DB.`zero
∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻
∥ ⊢zero ∥⁻ = DB.zero
∥ ⊢suc ⊢M ∥⁻ = DB.suc ∥ ⊢M ∥⁻
∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
∥ ⊢μ ⊢M ∥⁻ = DB.μ ∥ ⊢M ∥⁻
∥ ⊢↑ ⊢M refl ∥⁻ = ∥ ⊢M ∥⁺

273
src/plfa/part2/Lambda.lagda.md
View file

@ -71,8 +71,8 @@ Terms have seven constructs. Three are for the core lambda calculus:
Three are for the naturals:
* Zero `` `zero ``
* Successor `` `suc ``
* Zero `` zero ``
* Successor `` suc ``
* Case `` case L [zero⇒ M |suc x ⇒ N ] ``
And one is for recursion:
@ -93,7 +93,7 @@ Here is the syntax of terms in Backus-Naur Form (BNF):
L, M, N ::=
` 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
And here it is formalised in Agda:
@ -104,15 +104,14 @@ Id = String
infix 5 ƛ_⇒_
infix 5 μ_⇒_
infixl 7 _·_
infix 8 `suc_
infix 9 `_
data Term : Set where
`_ : Id → Term
ƛ_⇒_ : Id → Term → Term
_·_ : Term → Term → Term
`zero : Term
`suc_ : Term → Term
zero : Term
suc : Term → Term
case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term
μ_⇒_ : Id → Term → Term
```
@ -129,13 +128,13 @@ a function that adds naturals,
and a term that computes two plus two:
```
two : Term
two = `suc `suc `zero
two = suc (suc zero)
plus : Term
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
case ` "m"
[zero⇒ ` "n"
|suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
|suc "m" ⇒ suc (` "+" · ` "m" · ` "n") ]
```
The recursive definition of addition is similar to our original
definition of `_+_` for naturals, as given in
@ -149,7 +148,7 @@ the term
plus · two · two
reduces to `` `suc `suc `suc `suc `zero ``.
reduces to `` suc (suc (suc (suc zero))) ``.
As a second example, we use higher-order functions to represent
natural numbers. In particular, the number _n_ is represented by a
@ -167,7 +166,7 @@ plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
` "m" · ` "s" · (` "n" · ` "s" · ` "z")
sucᶜ : Term
sucᶜ = ƛ "n" ⇒ `suc (` "n")
sucᶜ = ƛ "n" ⇒ suc (` "n")
```
The Church numeral for two takes two arguments `s` and `z`
and applies `s` twice to `z`.
@ -177,13 +176,13 @@ result of using `n` to apply `s` to `z`; hence `s` is applied `m` plus
`n` times to `z`, yielding the Church numeral for the sum of `m` and
`n`. For convenience, we define a function that computes successor.
To convert a Church numeral to the corresponding natural, we apply
it to the `sucᶜ` function and the natural number zero.
it to the sucᶜ` function and the natural number zero.
Again, later we will confirm that two plus two is four,
in other words that the term
plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero
reduces to `` `suc `suc `suc `suc `zero ``.
reduces to `` suc (suc (suc (suc zero))) ``.
#### Exercise `mul` (recommended)
@ -236,7 +235,7 @@ plus′ : Term
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
case′ m
[zero⇒ n
|suc m ⇒ `suc (+ · m · n) ]
|suc m ⇒ suc (+ · m · n) ]
where
+ = ` "+"
m = ` "m"
@ -258,7 +257,9 @@ _meta-language_ (the language in which the description is written),
trusting readers can use context to distinguish the two. Agda is
not quite so forgiving, so here we use `ƛ x ⇒ N` and `L · M` for the
object language, as compared to `λ x → N` and `L M` in our
meta-language, Agda.
meta-language, Agda. We use `zero` and `suc` for both the object
language and the meta-language, using Agda's ability to overload
constructors to distinguish the two.
### Bound and free variables
@ -316,7 +317,7 @@ to alpha renaming. In the term
μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
case ` "m"
[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
line and one in the last line. It is equivalent to the following term,
@ -324,7 +325,7 @@ line and one in the last line. It is equivalent to the following term,
μ "plus" ⇒ ƛ "x" ⇒ ƛ "y" ⇒
case ` "x"
[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
names, `x` and `x′`.
@ -333,7 +334,7 @@ names, `x` and `x′`.
## Values
A _value_ is a term that corresponds to an answer.
Thus, `` `suc `suc `suc `suc `zero `` is a value,
Thus, `` suc (suc (suc (suc zero))) `` is a value,
while `` plus · two · two `` is not.
Following convention, we treat all function abstractions
as values; thus, `` plus `` by itself is considered a value.
@ -349,12 +350,12 @@ data Value : Term → Set where
V-zero :
-----------
Value `zero
Value zero
V-suc : ∀ {V}
→ Value V
--------------
→ Value (`suc V)
→ Value (suc V)
```
In what follows, we let `V` and `W` range over values.
@ -385,13 +386,13 @@ Substitution plays a key role in defining the
operational semantics of function application.
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.
We write substitution as `N [ x := V ]`, meaning
@ -406,14 +407,14 @@ Here are some examples:
* `` (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] `` yields
`` ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") ``.
* `` (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] `` yields
`` sucᶜ · (sucᶜ · `zero) ``.
* `` (ƛ "x" ⇒ ` "y") [ "y" := `zero ] `` yields `` ƛ "x" ⇒ `zero ``.
* `` (ƛ "x" ⇒ ` "x") [ "x" := `zero ] `` yields `` ƛ "x" ⇒ ` "x" ``.
* `` (ƛ "y" ⇒ ` "y") [ "x" := `zero ] `` yields `` ƛ "y" ⇒ ` "y" ``.
* `` (sucᶜ · (sucᶜ · ` "z")) [ "z" := zero ] `` yields
`` sucᶜ · (sucᶜ · zero) ``.
* `` (ƛ "x" ⇒ ` "y") [ "y" := zero ] `` yields `` ƛ "x" ⇒ zero ``.
* `` (ƛ "x" ⇒ ` "x") [ "x" := zero ] `` yields `` ƛ "x" ⇒ ` "x" ``.
* `` (ƛ "y" ⇒ ` "y") [ "x" := zero ] `` yields `` ƛ "y" ⇒ ` "y" ``.
In the last but one example, substituting `` `zero `` for `x` in
`` ƛ "x" ⇒ ` "x" `` does _not_ yield `` ƛ "x" ⇒ `zero ``,
In the last but one example, substituting `` zero `` for `x` in
`` ƛ "x" ⇒ ` "x" `` does _not_ yield `` ƛ "x" ⇒ zero ``,
since `x` is bound in the lambda abstraction.
The choice of bound names is irrelevant: both
`` ƛ "x" ⇒ ` "x" `` and `` ƛ "y" ⇒ ` "y" `` stand for the
@ -426,13 +427,13 @@ when term substituted for the variable is closed. This is because
substitution by terms that are _not_ closed may require renaming
of bound variables. For example:
* `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · `zero] `` should not yield <br/>
`` (ƛ "x" ⇒ ` "x" · (` "x" · `zero)) ``.
* `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · zero] `` should not yield <br/>
`` (ƛ "x" ⇒ ` "x" · (` "x" · zero)) ``.
Instead, we should rename the bound variable to avoid capture:
* `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · `zero ] `` should yield <br/>
`` ƛ "x′" ⇒ ` "x′" · (` "x" · `zero) ``.
* `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · zero ] `` should yield <br/>
`` ƛ "x′" ⇒ ` "x′" · (` "x" · zero) ``.
Here `x′` is a fresh variable distinct from `x`.
Formal definition of substitution with suitable renaming is considerably
@ -450,13 +451,13 @@ _[_:=_] : Term → Id → Term → Term
... | no _ = ` x
(ƛ x ⇒ N) [ y := V ] with x ≟ y
... | yes _ = ƛ x ⇒ N
... | no _ = ƛ x ⇒ N [ y := V ]
(L · M) [ y := V ] = L [ y := V ] · M [ y := V ]
(`zero) [ y := V ] = `zero
(`suc M) [ y := V ] = `suc M [ y := V ]
... | no _ = ƛ x ⇒ (N [ y := V ])
(L · M) [ y := V ] = (L [ y := V ]) · (M [ y := V ])
(zero) [ y := V ] = zero
(suc M) [ y := V ] = suc (M [ y := V ])
(case L [zero⇒ M |suc x ⇒ N ]) [ y := V ] with x ≟ y
... | yes _ = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N ]
... | no _ = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N [ y := V ] ]
... | yes _ = case (L [ y := V ]) [zero⇒ (M [ y := V ]) |suc x ⇒ N ]
... | no _ = case (L [ y := V ]) [zero⇒ (M [ y := V ]) |suc x ⇒ (N [ y := V ]) ]
(μ x ⇒ N) [ y := V ] with x ≟ y
... | yes _ = μ x ⇒ N
... | no _ = μ x ⇒ N [ y := V ]
@ -488,16 +489,16 @@ Here is confirmation that the examples above are correct:
_ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")
_ = refl
_ : (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] ≡ sucᶜ · (sucᶜ · `zero)
_ : (sucᶜ · (sucᶜ · ` "z")) [ "z" := zero ] ≡ sucᶜ · (sucᶜ · zero)
_ = refl
_ : (ƛ "x" ⇒ ` "y") [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero
_ : (ƛ "x" ⇒ ` "y") [ "y" := zero ] ≡ ƛ "x" ⇒ zero
_ = refl
_ : (ƛ "x" ⇒ ` "x") [ "x" := `zero ] ≡ ƛ "x" ⇒ ` "x"
_ : (ƛ "x" ⇒ ` "x") [ "x" := zero ] ≡ ƛ "x" ⇒ ` "x"
_ = refl
_ : (ƛ "y" ⇒ ` "y") [ "x" := `zero ] ≡ ƛ "y" ⇒ ` "y"
_ : (ƛ "y" ⇒ ` "y") [ "x" := zero ] ≡ ƛ "y" ⇒ ` "y"
_ = refl
```
@ -506,12 +507,12 @@ _ = refl
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")) ``
2. `` (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ `zero)) ``
3. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ ` "x")) ``
4. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ `zero)) ``
2. `` (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ zero)) ``
3. `` (ƛ "y" ⇒ zero · (ƛ "x" ⇒ ` "x")) ``
4. `` (ƛ "y" ⇒ zero · (ƛ "x" ⇒ zero)) ``
#### Exercise `_[_:=_]′` (stretch)
@ -604,7 +605,7 @@ data _—→_ : Term → Term → Set where
ξ-suc : ∀ {M M′}
→ M —→ M′
------------------
→ `suc M —→ `suc M′
→ suc M —→ suc M′
ξ-case : ∀ {x L L′ M N}
→ L —→ L′
@ -613,12 +614,12 @@ data _—→_ : Term → Term → Set where
β-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}
→ 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}
------------------------------
@ -660,14 +661,14 @@ What does the following term step to?
2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
3. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
What does the following term step to? (Where `twoᶜ` and `sucᶜ` are as
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) ``
2. `` (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero ``
3. `` `zero ``
1. `` sucᶜ · (sucᶜ · zero) ``
2. `` (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · zero ``
3. `` zero ``
## Reflexive and transitive closure
@ -804,98 +805,98 @@ systems studied in this text are trivially confluent.
We start with a simple example. The Church numeral two applied to the
successor function and zero yields the natural number two:
```
_ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero
_ : twoᶜ · sucᶜ · zero —↠ suc (suc zero)
_ =
begin
twoᶜ · sucᶜ · `zero
twoᶜ · sucᶜ · zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · zero
—→⟨ β-ƛ V-zero ⟩
sucᶜ · (sucᶜ · `zero)
sucᶜ · (sucᶜ · zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
sucᶜ · `suc `zero
sucᶜ · suc zero
—→⟨ β-ƛ (V-suc V-zero) ⟩
`suc (`suc `zero)
suc (suc zero)
∎
```
Here is a sample reduction demonstrating that two plus two is four:
```
_ : plus · two · two —↠ `suc `suc `suc `suc `zero
_ : plus · two · two —↠ suc (suc (suc (suc zero)))
_ =
begin
plus · two · two
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (plus · ` "m" · ` "n") ])
· two · two
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒
case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
case two [zero⇒ ` "n" |suc "m" ⇒ suc (plus · ` "m" · ` "n") ])
· two
—→⟨ β-ƛ (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 (plus · `suc `zero · two)
suc (plus · suc zero · two)
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc ((ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· `suc `zero · two)
suc ((ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (plus · ` "m" · ` "n") ])
· suc zero · two)
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc ((ƛ "n" ⇒
case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
suc ((ƛ "n" ⇒
case suc zero [zero⇒ ` "n" |suc "m" ⇒ suc (plus · ` "m" · ` "n") ])
· two)
—→⟨ ξ-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 (plus · `zero · two)
suc (suc (plus · zero · two))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· `zero · two)
suc (suc ((ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (plus · ` "m" · ` "n") ])
· zero · two))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc `suc ((ƛ "n" ⇒
case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two)
suc (suc ((ƛ "n" ⇒
case zero [zero⇒ ` "n" |suc "m" ⇒ suc (plus · ` "m" · ` "n") ])
· two))
—→⟨ ξ-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 (`suc (`suc `zero)))
suc (suc (suc (suc zero)))
∎
```
And here is a similar sample reduction for Church numerals:
```
_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero
_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero —↠ suc (suc (suc (suc zero)))
_ =
begin
(ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z"))
· twoᶜ · twoᶜ · sucᶜ · `zero
· twoᶜ · twoᶜ · sucᶜ · zero
—→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
(ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (` "n" · ` "s" · ` "z"))
· twoᶜ · sucᶜ · `zero
· twoᶜ · sucᶜ · zero
—→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (twoᶜ · ` "s" · ` "z")) · sucᶜ · `zero
(ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (twoᶜ · ` "s" · ` "z")) · sucᶜ · zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` "z")) · `zero
(ƛ "z" ⇒ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` "z")) · zero
—→⟨ β-ƛ V-zero ⟩
twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero)
twoᶜ · sucᶜ · (twoᶜ · sucᶜ · zero)
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (twoᶜ · sucᶜ · `zero)
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (twoᶜ · sucᶜ · zero)
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · ((ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero)
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · ((ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (sucᶜ · `zero))
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (sucᶜ · zero))
—→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (`suc `zero))
(ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · suc 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)) ⟩
sucᶜ · (sucᶜ · `suc `suc `zero)
sucᶜ · (sucᶜ · suc (suc 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))) ⟩
`suc (`suc (`suc (`suc `zero)))
suc (suc (suc (suc zero)))
∎
```
@ -916,13 +917,13 @@ Write out the reduction sequence demonstrating that one plus one is two.
We have just two types:
* Functions, `A ⇒ B`
* Naturals, `` `ℕ ``
* Naturals, `` ℕ ``
As before, to avoid overlap we use variants of the names used by Agda.
Here is the syntax of types in BNF:
A, B, C ::= A ⇒ B | `ℕ
A, B, C ::= A ⇒ B | ℕ
And here it is formalised in Agda:
@ -941,34 +942,34 @@ currying. This is made more convenient by declaring `_⇒_` to
associate to the right and `_·_` to associate to the left.
Thus:
* ``(`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ`` stands for ``((`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ))``.
* ``(ℕ ⇒ ℕ) ⇒ ℕ ⇒ ℕ`` stands for ``((ℕ ⇒ ℕ) ⇒ (ℕ ⇒ ℕ))``.
* `plus · two · two` stands for `(plus · two) · two`.
### Quiz
* What is the type of the following term?
`` ƛ "s" ⇒ ` "s" · (` "s" · `zero) ``
`` ƛ "s" ⇒ ` "s" · (` "s" · zero) ``
1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) ``
2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ ``
3. `` `ℕ ⇒ (`ℕ ⇒ `ℕ) ``
4. `` `ℕ ⇒ `ℕ ⇒ `ℕ ``
5. `` `ℕ ⇒ `ℕ ``
6. `` `ℕ ``
1. `` (ℕ ⇒ ℕ) ⇒ (ℕ ⇒ ℕ) ``
2. `` (ℕ ⇒ ℕ) ⇒ ℕ ``
3. `` ℕ ⇒ (ℕ ⇒ ℕ) ``
4. `` ℕ ⇒ ℕ ⇒ ℕ ``
5. `` ℕ ⇒ ℕ ``
6. `` ℕ ``
Give more than one answer if appropriate.
* What is the type of the following term?
`` (ƛ "s" ⇒ ` "s" · (` "s" · `zero)) · sucᶜ ``
`` (ƛ "s" ⇒ ` "s" · (` "s" · zero)) · sucᶜ ``
1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) ``
2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ ``
3. `` `ℕ ⇒ (`ℕ ⇒ `ℕ) ``
4. `` `ℕ ⇒ `ℕ ⇒ `ℕ ``
5. `` `ℕ ⇒ `ℕ ``
6. `` `ℕ ``
1. `` (ℕ ⇒ ℕ) ⇒ (ℕ ⇒ ℕ) ``
2. `` (ℕ ⇒ ℕ) ⇒ ℕ ``
3. `` ℕ ⇒ (ℕ ⇒ ℕ) ``
4. `` ℕ ⇒ ℕ ⇒ ℕ ``
5. `` ℕ ⇒ ℕ ``
6. `` ℕ ``
Give more than one answer if appropriate.
@ -987,10 +988,10 @@ over contexts. We write `∅` for the empty context, and `Γ , x ⦂ A`
for the context that extends `Γ` by mapping variable `x` to type `A`.
For example,
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ ``
is the context that associates variable `` "s" `` with type `` `ℕ ⇒ `ℕ ``,
and variable `` "z" `` with type `` `ℕ ``.
is the context that associates variable `` "s" `` with type `` ℕ ⇒ ℕ ``,
and variable `` "z" `` with type `` ℕ ``.
Contexts are formalised as follows:
@ -1008,11 +1009,11 @@ data Context : Set where
Show that `Context` is isomorphic to `List (Id × Type)`.
For instance, the isomorphism relates the context
∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ
∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ
to the list
[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
[ ⟨ "z" , ℕ ⟩ , ⟨ "s" , ℕ ⇒ ℕ ⟩ ]
```
-- Your code goes here
@ -1028,8 +1029,8 @@ and indicates in context `Γ` that variable `x` has type `A`.
It is called _lookup_.
For example,
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "z" ⦂ `ℕ ``
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ ∋ "z" ⦂ ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ ∋ "s" ⦂ ℕ ⇒ ℕ ``
give us the types associated with variables `` "z" `` and `` "s" ``,
respectively. The symbol `∋` (pronounced "ni", for "in"
@ -1040,9 +1041,9 @@ If two variables in a context have the same name, then lookup
should return the most recently bound variable, which _shadows_
the other variables. For example,
* `` ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ∋ "x" ⦂ `ℕ ``.
* `` ∅ , "x" ⦂ ℕ ⇒ ℕ , "x" ⦂ ℕ ∋ "x" ⦂ ℕ ``.
Here `` "x" ⦂ `ℕ ⇒ `ℕ `` is shadowed by `` "x" ⦂ `ℕ ``.
Here `` "x" ⦂ ℕ ⇒ ℕ `` is shadowed by `` "x" ⦂ ℕ ``.
Lookup is formalised as follows:
```
@ -1077,12 +1078,12 @@ and indicates in context `Γ` that term `M` has type `A`.
Context `Γ` provides types for all the free variables in `M`.
For example:
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "z" ⦂ `ℕ ``
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ ``
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · ` "z" ⦂ `ℕ ``
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · (` "s" · ` "z") ⦂ `ℕ ``
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ `ℕ ⇒ `ℕ ``
* `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ ⊢ ` "z" ⦂ ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ ⊢ ` "s" ⦂ ℕ ⇒ ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ ⊢ ` "s" · ` "z" ⦂ ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ , "z" ⦂ ℕ ⊢ ` "s" · (` "s" · ` "z") ⦂ ℕ ``
* `` ∅ , "s" ⦂ ℕ ⇒ ℕ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ ℕ ⇒ ℕ ``
* `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (ℕ ⇒ ℕ) ⇒ ℕ ⇒ ℕ ``
Typing is formalised as follows:
```
@ -1112,13 +1113,13 @@ data _⊢_⦂_ : Context → Term → Type → Set where
-- ℕ-I₁
⊢zero : ∀ {Γ}
--------------
→ Γ ⊢ `zero ⦂ `ℕ
→ Γ ⊢ zero ⦂ `ℕ
-- ℕ-I₂
⊢suc : ∀ {Γ M}
→ Γ ⊢ M ⦂ `ℕ
---------------
→ Γ ⊢ `suc M ⦂ `ℕ
→ Γ ⊢ suc M ⦂ `ℕ
-- ℕ-E
⊢case : ∀ {Γ L M x N A}
@ -1267,7 +1268,7 @@ And here are typings for the remainder of the Church example:
where
∋n = Z
⊢2+2ᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ
⊢2+2ᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero ⦂ `ℕ
⊢2+2ᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero
```
@ -1285,11 +1286,11 @@ Typing C-c C-l causes Agda to create a hole and tell us its expected type:
?0 : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ
Now we fill in the hole by typing C-c C-r. Agda observes that
the outermost term in `sucᶜ` is `ƛ`, which is typed using `⊢ƛ`. The
the outermost term in sucᶜ` is `ƛ`, which is typed using `⊢ƛ`. The
`⊢ƛ` rule in turn takes one argument, which Agda leaves as a hole:
⊢sucᶜ = ⊢ƛ { }1
?1 : ∅ , "n" ⦂ `ℕ ⊢ `suc ` "n" ⦂ `ℕ
?1 : ∅ , "n" ⦂ `ℕ ⊢ suc ` "n" ⦂ `ℕ
We can fill in the hole by typing C-c C-r again:
@ -1334,12 +1335,12 @@ the term `ƛ "x" ⇒ "x"` has type `A ⇒ A` for any type `A`.
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 · `suc `zero ``. It cannot be typed, because doing so
`` zero · suc zero ``. It cannot be typed, because doing so
requires that the first term in the application is both a natural and
a function:
```
nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A)
nope₁ : ∀ {A} → ¬ (∅ ⊢ zero · suc zero ⦂ A)
nope₁ (() · _)
```

141
src/plfa/part2/More.lagda.md
View file

@ -155,19 +155,19 @@ construct to a calculus without the construct.
A `× B product type
L, M, N ::= ... Terms
`⟨ M , N ⟩ pair
⟨ M , N ⟩ pair
`proj₁ L project first component
`proj₂ L project second component
V, W ::= ... Values
`⟨ V , W ⟩ pair
⟨ V , W ⟩ pair
### Typing
Γ ⊢ M ⦂ A
Γ ⊢ N ⦂ B
----------------------- `⟨_,_⟩ or `×-I
Γ ⊢ `⟨ M , N ⟩ ⦂ A `× B
----------------------- ⟨_,_⟩ or `×-I
Γ ⊢ ⟨ M , N ⟩ ⦂ A `× B
Γ ⊢ L ⦂ A `× B
---------------- `proj₁ or `×-E₁
@ -181,11 +181,11 @@ construct to a calculus without the construct.
M —→ M′
------------------------- ξ-⟨,⟩₁
`⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
⟨ M , N ⟩ —→ ⟨ M′ , N ⟩
N —→ N′
------------------------- ξ-⟨,⟩₂
`⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
⟨ V , N ⟩ —→ ⟨ V , N′ ⟩
L —→ L′
--------------------- ξ-proj₁
@ -196,17 +196,17 @@ construct to a calculus without the construct.
`proj₂ L —→ `proj₂ L′
---------------------- β-proj₁
`proj₁ `⟨ V , W ⟩ —→ V
`proj₁ ⟨ V , W ⟩ —→ V
---------------------- β-proj₂
`proj₂ `⟨ V , W ⟩ —→ W
`proj₂ ⟨ V , W ⟩ —→ W
### Example
Here is a function to swap the components of a pair:
swap× : ∅ ⊢ A `× B ⇒ B `× A
swap× = ƛ z ⇒ `⟨ proj₂ z , proj₁ z ⟩
swap× = ƛ z ⇒ ⟨ proj₂ z , proj₁ z ⟩
## Alternative formulation of products
@ -222,11 +222,11 @@ and reduction rules:
A `× B product type
L, M, N ::= ... Terms
`⟨ M , N ⟩ pair
⟨ M , N ⟩ pair
case× L [⟨ x , y ⟩⇒ M ] case
V, W ::= Values
`⟨ V , W ⟩ pair
⟨ V , W ⟩ pair
### Typing
@ -242,7 +242,7 @@ and reduction rules:
case× L [⟨ x , y ⟩⇒ N ] —→ case× L′ [⟨ x , y ⟩⇒ N ]
--------------------------------------------------------- β-case×
case× `⟨ V , W ⟩ [⟨ x , y ⟩⇒ N ] —→ N [ x := V ][ y := W ]
case× ⟨ V , W ⟩ [⟨ x , y ⟩⇒ N ] —→ N [ x := V ][ y := W ]
### Example
@ -250,7 +250,7 @@ Here is a function to swap the components of a pair rewritten in the new notatio
swap×-case : ∅ ⊢ A `× B ⇒ B `× A
swap×-case = ƛ z ⇒ case× z
[⟨ x , y ⟩⇒ `⟨ y , x ⟩ ]
[⟨ x , y ⟩⇒ ⟨ y , x ⟩ ]
### Translation
@ -293,23 +293,23 @@ We can also translate back the other way:
A `⊎ B sum type
L, M, N ::= ... Terms
`inj₁ M inject first component
`inj₂ N inject second component
inj₁ M inject first component
inj₂ N inject second component
case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ] case
V, W ::= ... Values
`inj₁ V inject first component
`inj₂ W inject second component
inj₁ V inject first component
inj₂ W inject second component
### Typing
Γ ⊢ M ⦂ A
-------------------- `inj₁ or ⊎-I₁
Γ ⊢ `inj₁ M ⦂ A `⊎ B
-------------------- inj₁ or ⊎-I₁
Γ ⊢ inj₁ M ⦂ A `⊎ B
Γ ⊢ N ⦂ B
-------------------- `inj₂ or ⊎-I₂
Γ ⊢ `inj₂ N ⦂ A `⊎ B
-------------------- inj₂ or ⊎-I₂
Γ ⊢ inj₂ N ⦂ A `⊎ B
Γ ⊢ L ⦂ A `⊎ B
Γ , x ⦂ A ⊢ M ⦂ C
@ -321,21 +321,21 @@ We can also translate back the other way:
M —→ M′
------------------- ξ-inj₁
`inj₁ M —→ `inj₁ M′
inj₁ M —→ inj₁ M′
N —→ N′
------------------- ξ-inj₂
`inj₂ N —→ `inj₂ N′
inj₂ N —→ inj₂ N′
L —→ L′
---------------------------------------------------------------------- ξ-case⊎
case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ case⊎ L′ [inj₁ x ⇒ M |inj₂ y ⇒ N ]
--------------------------------------------------------- β-inj₁
case⊎ (`inj₁ V) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ M [ x := V ]
case⊎ (inj₁ V) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ M [ x := V ]
--------------------------------------------------------- β-inj₂
case⊎ (`inj₂ W) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ N [ y := W ]
case⊎ (inj₂ W) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ N [ y := W ]
### Example
@ -343,8 +343,8 @@ Here is a function to swap the components of a sum:
swap⊎ : ∅ ⊢ A `⊎ B ⇒ B `⊎ A
swap⊎ = ƛ z ⇒ case⊎ z
[inj₁ x ⇒ `inj₂ x
|inj₂ y ⇒ `inj₁ y ]
[inj₁ x ⇒ inj₂ x
|inj₂ y ⇒ inj₁ y ]
## Unit type
@ -359,15 +359,15 @@ There are no reduction rules.
`⊤ unit type
L, M, N ::= ... Terms
`tt unit value
tt unit value
V, W ::= ... Values
`tt unit value
tt unit value
### Typing
------------ `tt or ⊤-I
Γ ⊢ `tt ⦂ `⊤
----------- tt or ⊤-I
Γ ⊢ tt ⦂ `⊤
### Reduction
@ -378,7 +378,7 @@ There are no reduction rules.
Here is the isomorphism between `A` and ``A `× `⊤``:
to×⊤ : ∅ ⊢ A ⇒ A `× `⊤
to×⊤ = ƛ x ⇒ `⟨ x , `tt ⟩
to×⊤ = ƛ x ⇒ ⟨ x , tt ⟩
from×⊤ : ∅ ⊢ A `× `⊤ ⇒ A
from×⊤ = ƛ z ⇒ proj₁ z
@ -396,11 +396,11 @@ We repeat the syntax in full, but only give the new type and reduction rules:
`⊤ unit type
L, M, N ::= ... Terms
`tt unit value
tt unit value
`case⊤ L [tt⇒ N ] case
V, W ::= ... Values
`tt unit value
tt unit value
### Typing
@ -416,7 +416,7 @@ We repeat the syntax in full, but only give the new type and reduction rules:
case⊤ L [tt⇒ M ] —→ case⊤ L′ [tt⇒ M ]
----------------------- β-case⊤
case⊤ `tt [tt⇒ M ] —→ M
case⊤ tt [tt⇒ M ] —→ M
### Example
@ -469,7 +469,7 @@ construct plays a role similar to `⊥-elim` in Agda:
Here is the isomorphism between `A` and ``A `⊎ `⊥``:
to⊎⊥ : ∅ ⊢ A ⇒ A `⊎ `⊥
to⊎⊥ = ƛ x ⇒ `inj₁ x
to⊎⊥ = ƛ x ⇒ inj₁ x
from⊎⊥ : ∅ ⊢ A `⊎ `⊥ ⇒ A
from⊎⊥ = ƛ z ⇒ case⊎ z
@ -577,7 +577,6 @@ infix 5 ƛ_
infix 5 μ_
infixl 7 _·_
infixl 8 _`*_
infix 8 `suc_
infix 9 `_
infix 9 S_
infix 9 #_
@ -643,11 +642,11 @@ data _⊢_ : Context → Type → Set where
-- naturals
`zero : ∀ {Γ}
zero : ∀ {Γ}
------
→ Γ ⊢ `ℕ
`suc_ : ∀ {Γ}
suc : ∀ {Γ}
→ Γ ⊢ `ℕ
------
→ Γ ⊢ `ℕ
@ -689,7 +688,7 @@ data _⊢_ : Context → Type → Set where
-- products
`⟨_,_⟩ : ∀ {Γ A B}
⟨_,_⟩ : ∀ {Γ A B}
→ Γ ⊢ A
→ Γ ⊢ B
-----------
@ -745,14 +744,14 @@ rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ
rename ρ (` x) = ` (ρ x)
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
rename ρ (`zero) = `zero
rename ρ (`suc M) = `suc (rename ρ M)
rename ρ (zero) = zero
rename ρ (suc M) = suc (rename ρ M)
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
rename ρ (μ N) = μ (rename (ext ρ) N)
rename ρ (con n) = con n
rename ρ (M `* N) = rename ρ M `* rename ρ N
rename ρ (`let M N) = `let (rename ρ M) (rename (ext ρ) N)
rename ρ `⟨ M , N ⟩ = `⟨ rename ρ M , rename ρ N ⟩
rename ρ ⟨ M , N ⟩ = ⟨ rename ρ M , rename ρ N ⟩
rename ρ (`proj₁ L) = `proj₁ (rename ρ L)
rename ρ (`proj₂ L) = `proj₂ (rename ρ L)
rename ρ (case× L M) = case× (rename ρ L) (rename (ext (ext ρ)) M)
@ -769,14 +768,14 @@ subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ
subst σ (` k) = σ k
subst σ (ƛ N) = ƛ (subst (exts σ) N)
subst σ (L · M) = (subst σ L) · (subst σ M)
subst σ (`zero) = `zero
subst σ (`suc M) = `suc (subst σ M)
subst σ (zero) = zero
subst σ (suc M) = suc (subst σ M)
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
subst σ (μ N) = μ (subst (exts σ) N)
subst σ (con n) = con n
subst σ (M `* N) = subst σ M `* subst σ N
subst σ (`let M N) = `let (subst σ M) (subst (exts σ) N)
subst σ `⟨ M , N ⟩ = `⟨ subst σ M , subst σ N ⟩
subst σ ⟨ M , N ⟩ = ⟨ subst σ M , subst σ N ⟩
subst σ (`proj₁ L) = `proj₁ (subst σ L)
subst σ (`proj₂ L) = `proj₂ (subst σ L)
subst σ (case× L M) = case× (subst σ L) (subst (exts (exts σ)) M)
@ -825,12 +824,12 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
V-zero : ∀ {Γ}
-----------------
→ Value (`zero {Γ})
→ Value (zero {Γ})
V-suc_ : ∀ {Γ} {V : Γ ⊢ `ℕ}
→ Value V
--------------
→ Value (`suc V)
→ Value (suc V)
-- primitives
@ -844,7 +843,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
→ Value V
→ Value W
----------------
→ Value `⟨ V , W ⟩
→ Value ⟨ V , W ⟩
```
Implicit arguments need to be supplied when they are
@ -880,7 +879,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
→ M —→ M′
-----------------
→ `suc M —→ `suc M′
→ suc M —→ suc M′
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ L —→ L′
@ -889,12 +888,12 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
-------------------
→ case `zero M N —→ M
→ case zero M N —→ M
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ Value V
----------------------------
→ case (`suc V) M N —→ N [ V ]
→ case (suc V) M N —→ N [ V ]
-- fixpoint
@ -936,13 +935,13 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
→ M —→ M′
-------------------------
→ `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
→ ⟨ M , N ⟩ —→ ⟨ M′ , N ⟩
ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
→ Value V
→ N —→ N′
-------------------------
→ `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
→ ⟨ V , N ⟩ —→ ⟨ V , N′ ⟩
ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
→ L —→ L′
@ -958,13 +957,13 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
→ Value V
→ Value W
----------------------
→ `proj₁ `⟨ V , W ⟩ —→ V
→ `proj₁ ⟨ V , W ⟩ —→ V
β-proj₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
→ Value V
→ Value W
----------------------
→ `proj₂ `⟨ V , W ⟩ —→ W
→ `proj₂ ⟨ V , W ⟩ —→ W
-- alternative formulation of products
@ -977,7 +976,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
→ Value V
→ Value W
----------------------------------
→ case× `⟨ V , W ⟩ M —→ M [ V ][ W ]
→ case× ⟨ V , W ⟩ M —→ M [ V ][ W ]
```
@ -1051,8 +1050,8 @@ progress (L · M) with progress L
... | done V-ƛ with progress M
... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′)
... | done VM = step (β-ƛ VM)
progress (`zero) = done V-zero
progress (`suc M) with progress M
progress (zero) = done V-zero
progress (suc M) with progress M
... | step M—→M′ = step (ξ-suc M—→M′)
... | done VM = done (V-suc VM)
progress (case L M N) with progress L
@ -1069,7 +1068,7 @@ progress (L `* M) with progress L
progress (`let M N) with progress M
... | step M—→M′ = step (ξ-let M—→M′)
... | done VM = step (β-let VM)
progress `⟨ M , N ⟩ with progress M
progress ⟨ M , N ⟩ with progress M
... | step M—→M′ = step (ξ-⟨,⟩₁ M—→M′)
... | done VM with progress N
... | step N—→N′ = step (ξ-⟨,⟩₂ VM N—→N′)
@ -1171,31 +1170,31 @@ _ =
∎
swap× : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
swap× = ƛ `⟨ `proj₂ (# 0) , `proj₁ (# 0) ⟩
swap× = ƛ ⟨ `proj₂ (# 0) , `proj₁ (# 0) ⟩
_ : swap× · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
_ : swap× · ⟨ con 42 , zero ⟩ —↠ ⟨ zero , con 42 ⟩
_ =
begin
swap× · `⟨ con 42 , `zero ⟩
swap× · ⟨ con 42 , zero ⟩
—→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
`⟨ `proj₂ `⟨ con 42 , `zero ⟩ , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
⟨ `proj₂ ⟨ con 42 , zero ⟩ , `proj₁ ⟨ con 42 , zero ⟩ ⟩
—→⟨ ξ-⟨,⟩₁ (β-proj₂ V-con V-zero) ⟩
`⟨ `zero , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
⟨ zero , `proj₁ ⟨ con 42 , zero ⟩ ⟩
—→⟨ ξ-⟨,⟩₂ V-zero (β-proj₁ V-con V-zero) ⟩
`⟨ `zero , con 42 ⟩
⟨ zero , con 42 ⟩
∎
swap×-case : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
swap×-case = ƛ case× (# 0) `⟨ # 0 , # 1 ⟩
swap×-case = ƛ case× (# 0) ⟨ # 0 , # 1 ⟩
_ : swap×-case · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
_ : swap×-case · ⟨ con 42 , zero ⟩ —↠ ⟨ zero , con 42 ⟩
_ =
begin
swap×-case · `⟨ con 42 , `zero ⟩
swap×-case · ⟨ con 42 , zero ⟩
—→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
case× `⟨ con 42 , `zero ⟩ `⟨ # 0 , # 1 ⟩
case× ⟨ con 42 , zero ⟩ ⟨ # 0 , # 1 ⟩
—→⟨ β-case× V-con V-zero ⟩
`⟨ `zero , con 42 ⟩
⟨ zero , con 42 ⟩
∎
```

216
src/plfa/part2/Properties.lagda.md
View file

@ -46,7 +46,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
that two plus 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
on the right. Every term in the chain had the same type, `` `ℕ ``.
@ -146,12 +146,12 @@ data Canonical_⦂_ : Term → Type → Set where
C-zero :
--------------------
Canonical `zero ⦂ `ℕ
Canonical zero ⦂ `ℕ
C-suc : ∀ {V}
→ Canonical V ⦂ `ℕ
---------------------
→ Canonical `suc V ⦂ `ℕ
→ Canonical (suc V) ⦂ `ℕ
```
Every closed, well-typed value is canonical:
@ -213,7 +213,7 @@ case of successor.
We would like to show that every term is either a value or takes a
reduction step. However, this is not true in general. The term
`zero · `suc `zero
`zero · suc `zero
is neither a value nor can take a reduction step. And if `` s ⦂ `ℕ ⇒ `ℕ ``
then the term
@ -874,17 +874,17 @@ well-typed term to its value, if it has one.
Some terms may reduce forever. Here is a simple example:
```
sucμ = μ "x" ⇒ `suc (` "x")
sucμ = μ "x" ⇒ suc (` "x")
_ =
begin
sucμ
—→⟨ β-μ ⟩
`suc sucμ
suc sucμ
—→⟨ ξ-suc β-μ ⟩
`suc `suc sucμ
suc (suc sucμ)
—→⟨ ξ-suc (ξ-suc β-μ) ⟩
`suc `suc `suc sucμ
suc (suc (suc sucμ))
-- ...
∎
```
@ -981,10 +981,10 @@ remaining. There are two possibilities:
### Examples
We can now use Agda to compute the non-terminating reduction
sequence given earlier. First, we show that the term `sucμ`
sequence given earlier. First, we show that the term sucμ`
is well typed:
```
⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ` "x" ⦂ `ℕ
⊢sucμ : ∅ ⊢ μ "x" ⇒ suc (` "x") ⦂ `ℕ
⊢sucμ = ⊢μ (⊢suc (⊢` ∋x))
where
∋x = Z
@ -994,13 +994,13 @@ sequence, we evaluate with three steps worth of gas:
```
_ : eval (gas 3) ⊢sucμ ≡
steps
(μ "x" ⇒ `suc ` "x"
(μ "x" ⇒ suc (` "x")
—→⟨ β-μ ⟩
`suc (μ "x" ⇒ `suc ` "x")
suc (μ "x" ⇒ suc (` "x"))
—→⟨ ξ-suc β-μ ⟩
`suc (`suc (μ "x" ⇒ `suc ` "x"))
suc (suc (μ "x" ⇒ suc (` "x")))
—→⟨ ξ-suc (ξ-suc β-μ) ⟩
`suc (`suc (`suc (μ "x" ⇒ `suc ` "x")))
suc (suc (suc (μ "x" ⇒ suc (` "x"))))
∎)
out-of-gas
_ = refl
@ -1012,17 +1012,17 @@ applied to successor and zero. Supplying 100 steps of gas is more than enough:
```
_ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡
steps
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· `zero
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ suc (` "n"))
· zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
`zero
(ƛ "z" ⇒ (ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · ` "z")) ·
zero
—→⟨ β-ƛ V-zero ⟩
(ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero)
(ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ "n" ⇒ `suc ` "n") · `suc `zero
(ƛ "n" ⇒ suc (` "n")) · suc zero
—→⟨ β-ƛ (V-suc V-zero) ⟩
`suc (`suc `zero)
suc (suc zero)
∎)
(done (V-suc (V-suc V-zero)))
_ = refl
@ -1031,7 +1031,7 @@ The example above was generated by using `C-c C-n` to normalise the
left-hand side of the equation and pasting in the result as the
right-hand side of the equation. The example reduction of the
previous chapter was derived from this result, reformatting and
writing `twoᶜ` and `sucᶜ` in place of their expansions.
writing `twoᶜ` and sucᶜ` in place of their expansions.
Next, we show two plus two is four:
```
@ -1040,157 +1040,157 @@ _ : eval (gas 100) ⊢2+2 ≡
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "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" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒
`suc
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· ` "n")
]))
· `suc (`suc `zero)
· `suc (`suc `zero)
· suc (suc zero)
· suc (suc zero)
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒
case `suc (`suc `zero) [zero⇒ ` "n" |suc "m" ⇒
`suc
case suc (suc zero) [zero⇒ ` "n" |suc "m" ⇒
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· ` "n")
])
· `suc (`suc `zero)
· suc (suc zero)
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
case `suc (`suc `zero) [zero⇒ `suc (`suc `zero) |suc "m" ⇒
`suc
case suc (suc zero) [zero⇒ suc (suc zero) |suc "m" ⇒
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· `suc (`suc `zero))
· suc (suc zero))
]
—→⟨ β-suc (V-suc V-zero) ⟩
`suc
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· `suc `zero
· `suc (`suc `zero))
· suc zero
· suc (suc zero))
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc
suc
((ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒
`suc
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· ` "n")
]))
· `suc `zero
· `suc (`suc `zero))
· suc zero
· suc (suc zero))
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc
suc
((ƛ "n" ⇒
case `suc `zero [zero⇒ ` "n" |suc "m" ⇒
`suc
case suc zero [zero⇒ ` "n" |suc "m" ⇒
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· ` "n")
])
· `suc (`suc `zero))
· suc (suc zero))
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
`suc
case `suc `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
`suc
suc
case suc zero [zero⇒ suc (suc zero) |suc "m" ⇒
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· `suc (`suc `zero))
· suc (suc zero))
]
—→⟨ ξ-suc (β-suc V-zero) ⟩
`suc
(`suc
suc
(suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· `zero
· `suc (`suc `zero)))
· zero
· suc (suc zero)))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc
(`suc
suc
(suc
((ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒
`suc
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· ` "n")
]))
· `zero
· `suc (`suc `zero)))
· zero
· suc (suc zero)))
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc
(`suc
suc
(suc
((ƛ "n" ⇒
case `zero [zero⇒ ` "n" |suc "m" ⇒
`suc
case zero [zero⇒ ` "n" |suc "m" ⇒
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· ` "n")
])
· `suc (`suc `zero)))
· suc (suc zero)))
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
`suc
(`suc
case `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
`suc
suc
(suc
case zero [zero⇒ suc (suc zero) |suc "m" ⇒
suc
((μ "+" ⇒
(ƛ "m" ⇒
(ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ suc (` "+" · ` "m" · ` "n")
])))
· ` "m"
· `suc (`suc `zero))
· suc (suc zero))
])
—→⟨ ξ-suc (ξ-suc β-zero) ⟩
`suc (`suc (`suc (`suc `zero)))
suc (suc (suc (suc zero)))
∎)
(done (V-suc (V-suc (V-suc (V-suc V-zero)))))
_ = refl
@ -1207,8 +1207,8 @@ _ : eval (gas 100) ⊢2+2ᶜ ≡
(ƛ "s" ⇒ (ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z")))))
· (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
· (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
· (ƛ "n" ⇒ `suc ` "n")
· `zero
· (ƛ "n" ⇒ suc (` "n"))
· zero
—→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
(ƛ "n" ⇒
(ƛ "s" ⇒
@ -1216,50 +1216,50 @@ _ : eval (gas 100) ⊢2+2ᶜ ≡
(ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" ·
(` "n" · ` "s" · ` "z"))))
· (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
· (ƛ "n" ⇒ `suc ` "n")
· `zero
· (ƛ "n" ⇒ suc (` "n"))
· zero
—→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "s" ⇒
(ƛ "z" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" ·
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" · ` "z")))
· (ƛ "n" ⇒ `suc ` "n")
· `zero
· (ƛ "n" ⇒ suc (` "n"))
· zero
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "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"))
· `zero
· 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")
· `zero)
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ suc (` "n"))
· zero)
—→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
· `zero)
(ƛ "z" ⇒ (ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · ` "z")) ·
((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ suc (` "n"))
· zero)
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
`zero)
(ƛ "z" ⇒ (ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · ` "z")) ·
((ƛ "z" ⇒ (ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · ` "z")) ·
zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero))
(ƛ "z" ⇒ (ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · ` "z")) ·
((ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · zero))
—→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
((ƛ "n" ⇒ `suc ` "n") · `suc `zero)
(ƛ "z" ⇒ (ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · ` "z")) ·
((ƛ "n" ⇒ suc (` "n")) · suc zero)
—→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
`suc (`suc `zero)
(ƛ "z" ⇒ (ƛ "n" ⇒ suc (` "n")) · ((ƛ "n" ⇒ suc (` "n")) · ` "z")) ·
suc (suc 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))) ⟩
(ƛ "n" ⇒ `suc ` "n") · `suc (`suc (`suc `zero))
(ƛ "n" ⇒ suc (` "n")) · suc (suc (suc 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)))))
_ = refl
@ -1401,7 +1401,7 @@ det (ξ-·₂ _ M—→M′) (β-ƛ VM) = ⊥-elim (V¬—→ VM M—
det (β-ƛ _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ V-ƛ L—→L″)
det (β-ƛ VM) (ξ-·₂ _ M—→M″) = ⊥-elim (V¬—→ VM M—→M″)
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 L—→L′ L—→L″) refl refl refl
det (ξ-case L—→L′) β-zero = ⊥-elim (V¬—→ V-zero L—→L′)

7
src/plfa/part2/Untyped.lagda.md
View file

@ -216,7 +216,7 @@ plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ
```
Before, reduction stopped when we reached a lambda term, so we had to
compute `` plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero `` to ensure we reduced
compute `` plusᶜ · twoᶜ · twoᶜ · sucᶜ · zero `` to ensure we reduced
to a representation of the natural four. Now, reduction continues
under lambda, so we don't need the extra arguments. It is convenient
to define a term to represent four as a Church numeral, as well as
@ -487,7 +487,7 @@ form or takes a reduction step.
Previously, progress only applied to closed, well-typed terms. We had
to rule out terms where we apply something other than a function (such
as `` `zero ``) or terms with a free variable. Now we can demonstrate
as `` zero ``) or terms with a free variable. Now we can demonstrate
it for open, well-scoped terms. The definition of normal form permits
free variables, and we have no terms that are not functions.
@ -698,7 +698,8 @@ case L M N = L · (ƛ N) · M
Here we have been careful to retain the exact form of our previous
definitions. The successor branch expects an additional variable to
be in scope (as indicated by its type), so it is converted to an
ordinary term using lambda abstraction.
ordinary term using lambda abstraction. We use names `` `zero `` and
`` `suc ``, since we are defining terms rather than constructors.
We can also define fixpoint. Using named terms, we define: