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

Merge pull request #297 from gallais/whitespace

Browse source 
[ fix ] whitespace violations
This commit is contained in:
Philip Wadler 2019-06-19 09:45:34 -03:00 committed by GitHub
commit e5f68a47ac
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
22 changed files with 196 additions and 197 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/plfa/Adequacy.lagda
View file

@ -142,7 +142,7 @@ at least one of them is too.
AboveFun-⊔ : ∀{u u'}
→ AboveFun (u ⊔ u')
→ AboveFun u ⊎ AboveFun u'
AboveFun-⊔{u}{u'} ⟨ v , ⟨ w , v↦w⊑u⊔u' ⟩ ⟩
AboveFun-⊔{u}{u'} ⟨ v , ⟨ w , v↦w⊑u⊔u' ⟩ ⟩
with sub-inv-fun v↦w⊑u⊔u'
... | ⟨ Γ , ⟨ f , ⟨ Γ⊆u⊔u' , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩
with Funs∈ f
@ -364,7 +364,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf
sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf
| no naf2 | yes af3
with vcw' ev1c af3
... | ⟨ clos {Γ'} L γ₁ , ⟨ L⇓c3 , 𝕍w'c ⟩ ⟩
... | ⟨ clos {Γ'} L γ₁ , ⟨ L⇓c3 , 𝕍w'c ⟩ ⟩
with 𝕍→WHNF 𝕍w'c
... | ƛ_ {N = N'} =
let 𝕍wc = not-AboveFun-𝕍{w}{Γ'}{γ₁}{N'} naf2 in
@ -385,7 +385,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨
(v₁' ⊔ v₂') ⊑ v
The induction hypotheses gives us `𝕍 v₁' (clos (ƛ N) γ)`
and `𝕍 v₂' (clos (ƛ N) γ)`, which is all we need for this case.
and `𝕍 v₂' (clos (ƛ N) γ)`, which is all we need for this case.
* Case `ConjR1⊑`.
@ -418,16 +418,16 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨
𝕍 (v ↦ w) (clos (ƛ N) γ)
𝕍 (v ↦ w') (clos (ƛ N) γ)
and need to show that
and need to show that
𝕍 (v ↦ (w ⊔ w')) (clos (ƛ N) γ)
Let `c` be an arbtrary closure such that `𝔼 v c`.
Assume `w ⊔ w'` is greater than a function.
Unfortunately, this does not mean that both `w` and `w'`
are above functions. But thanks to the lemma `AboveFun-⊔`,
we know that at least one of them is greater than a function.
* Suppose both of them are greater than a function. Then we have
`γ ⊢ N ⇓ clos L δ` and `𝕍 w (clos L δ)`. We also have `γ ⊢ N ⇓ c₃` and
`𝕍 w' c₃`. Because the big-step semantics is deterministic, we have
@ -441,7 +441,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨
`L ≡ ƛ N'` for some `N'`. Meanwhile, from `¬ AboveFun w'` we have
`𝕍 w' (clos L γ₁)`. We conclude that
`𝕍 (w ⊔ w') (clos (ƛ N') γ₁)`.
The proof of `sub-𝔼` is direct and explained below.
@ -485,9 +485,9 @@ kth-x{γ' = γ'}{x = x} with γ' x
⟨ c , ⟨ (⇓-var eq M'⇓c) , 𝕍γx ⟩ ⟩
↓→𝔼 {Γ} {γ} {γ'} 𝔾γγ' (↦-elim{L = L}{M = M}{v = v₁}{w = v} d₁ d₂) fv
with ↓→𝔼 𝔾γγ' d₁ ⟨ v₁ , ⟨ v , Refl⊑ ⟩ ⟩
... | ⟨ clos L' δ , ⟨ L⇓L' , 𝕍v₁↦v ⟩ ⟩
... | ⟨ clos L' δ , ⟨ L⇓L' , 𝕍v₁↦v ⟩ ⟩
with 𝕍→WHNF 𝕍v₁↦v
... | ƛ_ {N = N}
... | ƛ_ {N = N}
with 𝕍v₁↦v {clos M γ'} (↓→𝔼 𝔾γγ' d₂) fv
... | ⟨ c' , ⟨ N⇓c' , 𝕍v ⟩ ⟩ =
⟨ c' , ⟨ ⇓-app L⇓L' N⇓c' , 𝕍v ⟩ ⟩
@ -500,12 +500,12 @@ kth-x{γ' = γ'}{x = x} with γ' x
↓→𝔼 𝔾γγ' (⊔-intro{v = v₁}{w = v₂} d₁ d₂) fv12
with AboveFun? v₁ | AboveFun? v₂
... | yes fv1 | yes fv2
with ↓→𝔼 𝔾γγ' d₁ fv1 | ↓→𝔼 𝔾γγ' d₂ fv2
with ↓→𝔼 𝔾γγ' d₁ fv1 | ↓→𝔼 𝔾γγ' d₂ fv2
... | ⟨ c₁ , ⟨ M⇓c₁ , 𝕍v₁ ⟩ ⟩ | ⟨ c₂ , ⟨ M⇓c₂ , 𝕍v₂ ⟩ ⟩
rewrite ⇓-determ M⇓c₂ M⇓c₁ =
⟨ c₁ , ⟨ M⇓c₁ , 𝕍⊔-intro 𝕍v₁ 𝕍v₂ ⟩ ⟩
↓→𝔼 𝔾γγ' (⊔-intro{v = v₁}{w = v₂} d₁ d₂) fv12 | yes fv1 | no nfv2
with ↓→𝔼 𝔾γγ' d₁ fv1
with ↓→𝔼 𝔾γγ' d₁ fv1
... | ⟨ clos {Γ'} M' γ₁ , ⟨ M⇓c₁ , 𝕍v₁ ⟩ ⟩
with 𝕍→WHNF 𝕍v₁
... | ƛ_ {N = N} =
@ -531,7 +531,7 @@ kth-x{γ' = γ'}{x = x} with γ' x
* Case `var`. Looking up `x` in `γ'` yields some closure, `clos M' δ`,
and from `𝔾 γ γ'` we have `𝔼 (γ x) (clos M' δ)`. With the premise
`AboveFun (γ x)`, we obtain a closure `c` such that `δ ⊢ M' ⇓ c`
and `𝕍 (γ x) c`. To conclude `γ' ⊢ x ⇓ c` via `⇓-var`, we
and `𝕍 (γ x) c`. To conclude `γ' ⊢ x ⇓ c` via `⇓-var`, we
need `γ' x ≡ clos M' δ`, which is obvious, but it requires some
Agda shananigans via the `kth-x` lemma to get our hands on it.
@ -574,7 +574,7 @@ kth-x{γ' = γ'}{x = x} with γ' x
and `𝕍 v₁ (clos (ƛ N) γ₁)`.
Then because `v₂` is not greater than a function, we also have
`𝕍 v₂ (clos (ƛ N) γ₁)`. We conclude that `𝕍 (v₁ ⊔ v₂) (clos (ƛ N) γ₁)`.
* Case `sub`. We have `γ ⊢ M ↓ v`, `v' ⊑ v`, and `AboveFun v'`.
We need to show that `γ' ⊢ M ⇓ c` and `𝕍 v' c` for some `c`.
We have `AboveFun v` by `AboveFun-⊑`,
@ -598,7 +598,7 @@ adequacy{M}{N} eq
⟨ ⊥ , ⟨ ⊥ , Refl⊑ ⟩ ⟩
... | ⟨ clos {Γ} M′ γ , ⟨ M⇓c , Vc ⟩ ⟩
with 𝕍→WHNF Vc
... | ƛ_ {N = N′} =
... | ƛ_ {N = N′} =
⟨ Γ , ⟨ N′ , ⟨ γ , M⇓c ⟩ ⟩ ⟩
\end{code}
@ -615,7 +615,7 @@ results about the denotational semantics.
\begin{code}
reduce→cbn : ∀ {M : ∅ ⊢ ★} {N : ∅ , ★ ⊢ ★}
→ M —↠ ƛ N
→ Σ[ Δ ∈ Context ] Σ[ N′ ∈ Δ , ★ ⊢ ★ ] Σ[ δ ∈ ClosEnv Δ ]
→ Σ[ Δ ∈ Context ] Σ[ N′ ∈ Δ , ★ ⊢ ★ ] Σ[ δ ∈ ClosEnv Δ ]
∅' ⊢ M ⇓ clos (ƛ N′) δ
reduce→cbn M—↠ƛN = adequacy (soundness M—↠ƛN)
\end{code}
@ -646,4 +646,4 @@ This chapter uses the following unicode:
𝔼 U+1D53C MATHEMATICAL DOUBLE-STRUCK CAPITAL E (\bE)
𝔾 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL G (\bG)
𝕍 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL V (\bV)

28
src/plfa/Bisimulation.lagda
View file

@ -15,7 +15,7 @@ previous chapter, we saw how _let_ terms can be rewritten as an
application of an abstraction, and how two alternative formulations of
products — one with projections and one with case — can be formulated
in terms of each other. In this chapter, we look at how to formalise
such claims.
such claims.
Given two different systems, with different terms and reduction rules,
we define what it means to claim that one _simulates_ the other.
@ -34,7 +34,7 @@ _Simulation_: For every `M`, `M†`, and `N`:
If `M ~ M†` and `M —→ N`
then `M† —↠ N†` and `N ~ N†`
for some `N†`.
Or, in a diagram:
M --- —→ --- N
@ -70,7 +70,7 @@ reduction step in the source we must show a corresponding reduction
sequence in the target.
For instance, the source might be lambda calculus with _let_
added, and the target the same system with `let` translated out.
added, and the target the same system with `let` translated out.
The key rule defining our relation will be:
M ~ M†
@ -121,8 +121,8 @@ Another exercise is to show the alternative formulations
of products in
Chapter [More][plfa.More]
are in bisimulation.
## Imports
We import our source language from
@ -185,7 +185,7 @@ We need a number of technical results. The first is that simulation
commutes with values. That is, if `M ~ M†` and `M` is a value then
`M†` is also a value:
\begin{code}
~val : ∀ {Γ A} {M M† : Γ ⊢ A}
~val : ∀ {Γ A} {M M† : Γ ⊢ A}
→ M ~ M†
→ Value M
--------
@ -278,7 +278,7 @@ From the general case of substitution, it is also easy to derive
the required special case. If `N ~ N†` and `M ~ M†`, then
`N [ M ] ~ N† [ M† ]`:
\begin{code}
~sub : ∀ {Γ A B} {N N† : Γ , B ⊢ A} {M M† : Γ ⊢ B}
~sub : ∀ {Γ A B} {N N† : Γ , B ⊢ A} {M M† : Γ ⊢ B}
→ N ~ N†
→ M ~ M†
-----------------------
@ -302,7 +302,7 @@ _Lock-step simulation_: For every `M`, `M†`, and `N`:
If `M ~ M†` and `M —→ N`
then `M† —→ N†` and `N ~ N†`
for some `N†`.
Or, in a diagram:
M --- —→ --- N
@ -372,13 +372,13 @@ In its structure, it looks a little bit like a proof of progress:
from which follows:
L · M --- —→ --- L′ · M
| |
| |
| |
~ ~
| |
| |
L† · M† --- —→ --- L′† · M†
- The source term reduces via `ξ-·₂`, in which case the target term does as well.
Recursive invocation gives us
@ -393,7 +393,7 @@ In its structure, it looks a little bit like a proof of progress:
from which follows:
V · M --- —→ --- V · M′
| |
| |
| |
~ ~
| |
@ -404,12 +404,12 @@ In its structure, it looks a little bit like a proof of progress:
- The source term reduces via `β-ƛ`, in which case the target term does as well:
(ƛ x ⇒ N) · V --- —→ --- N [ x := V ]
| |
(ƛ x ⇒ N) · V --- —→ --- N [ x := V ]
| |
| |
~ ~
| |
| |
| |
(ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V† ]
Since simulation commutes with values and `V` is a value, `V†` is also a value.

24
src/plfa/CallByName.lagda
View file

@ -139,7 +139,7 @@ straightforward induction on the two big-step derivations.
with trans (sym eq1) eq2
... | refl = ⇓-determ mc mc'
⇓-determ ⇓-lam ⇓-lam = refl
⇓-determ (⇓-app mc mc₁) (⇓-app mc' mc'')
⇓-determ (⇓-app mc mc₁) (⇓-app mc' mc'')
with ⇓-determ mc mc'
... | refl = ⇓-determ mc₁ mc''
\end{code}
@ -209,7 +209,7 @@ The next lemma states that if you start with an equivalent
environment and substitution `γ ≈ₑ σ`, extending them with
an equivalent closure and term `c ≈ N` produces
an equivalent environment and substitution:
`(γ ,' V) ≈ₑ (ext-subst σ N)`.
`(γ ,' V) ≈ₑ (ext-subst σ N)`.
\begin{code}
≈ₑ-ext : ∀ {Γ} {γ : ClosEnv Γ} {σ : Subst Γ ∅} {V} {N : ∅ ⊢ ★}
@ -280,7 +280,7 @@ to consider.
The premise `γ ≈ₑ σ` tells us that `γ x ≈ σ x`, so `clos L δ ≈ σ x`.
By the definition of `≈`, there exists a `τ` such that
`δ ≈ₑ τ` and `σ x ≡ ⟪ τ ⟫ L `.
Using `δ ⊢ L ⇓ V` and `δ ≈ₑ τ`,
Using `δ ⊢ L ⇓ V` and `δ ≈ₑ τ`,
the induction hypothesis gives us
`⟪ τ ⟫ L —↠ N` and `V ≈ N` for some `N`.
So we have shown that `⟪ σ ⟫ x —↠ N` and `V ≈ N` for some `N`.
@ -290,28 +290,28 @@ to consider.
and `clos (⟪ σ ⟫ (ƛ N)) γ ≈ ⟪ σ ⟫ (ƛ N)`.
* Case `⇓-app`.
Using `γ ⊢ L ⇓ clos N δ` and `γ ≈ₑ σ`,
Using `γ ⊢ L ⇓ clos N δ` and `γ ≈ₑ σ`,
the induction hypothesis gives us
⟪ σ ⟫ L —↠ ƛ ⟪ exts τ ⟫ N (1)
and `δ ≈ₑ τ` for some `τ`.
From `γ≈ₑσ` we have `clos M γ ≈ ⟪ σ ⟫ M`.
Then with `(δ ,' clos M γ) ⊢ N ⇓ V`,
the induction hypothesis gives us `V ≈ N'` and
⟪ exts τ ⨟ subst-zero (⟪ σ ⟫ M) ⟫ N —↠ N' (2)
Meanwhile, by `β`, we have
(ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M —→ ⟪ subst-zero (⟪ σ ⟫ M) ⟫ (⟪ exts τ ⟫ N)
which is the same as the following, by `sub-sub`.
(ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M —→ ⟪ exts τ ⨟ subst-zero (⟪ σ ⟫ M) ⟫ N (3)
Using (3) and (2) we have
(ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M —↠ N' (4)
From (1) we have
@ -338,7 +338,7 @@ cbn→reduce {M}{Δ}{δ}{N′} M⇓c
⟨ ⟪ exts σ ⟫ N′ , rs ⟩
\end{code}
## Beta reduction to a lambda implies big-step evaluation
## Beta reduction to a lambda implies big-step evaluation
The proof of the backward direction, that beta reduction to a lambda
implies that the call-by-name semantics produces a result, is more
@ -401,4 +401,4 @@ This chapter uses the following unicode:
ₑ U+2091 LATIN SUBSCRIPT SMALL LETTER E (\_e)
⊢ U+22A2 RIGHT TACK (\|- or \vdash)
⇓ U+21DB DOWNWARDS DOUBLE ARROW (\d= or \Downarrow)

28
src/plfa/Compositional.lagda
View file

@ -47,7 +47,7 @@ open import Data.Unit using (⊤; tt)
Regarding the first equation
ℰ (ƛ M) ≃ ... ℰ M ...
we need to define a function that maps a `Denotation (Γ , ★)` to a
`Denotation Γ`. This function, let us name it `ℱ`, should mimic the
non-recursive part of the semantics when applied to a lambda term. In
@ -192,9 +192,9 @@ describe the proof below.
→ (ℰ L ● ℰ M) γ v
ℰ·→●ℰ (↦-elim{v = v′} d₁ d₂) = inj₂ ⟨ v′ , ⟨ d₁ , d₂ ⟩ ⟩
ℰ·→●ℰ {v = ⊥} ⊥-intro = inj₁ Bot⊑
ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (⊔-intro{v = v₁}{w = v₂} d₁ d₂)
ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (⊔-intro{v = v₁}{w = v₂} d₁ d₂)
with ℰ·→●ℰ d₁ | ℰ·→●ℰ d₂
... | inj₁ lt1 | inj₁ lt2 = inj₁ (ConjL⊑ lt1 lt2)
... | inj₁ lt1 | inj₁ lt2 = inj₁ (ConjL⊑ lt1 lt2)
... | inj₁ lt1 | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ =
inj₂ ⟨ v₁′ , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩
where lt : v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂
@ -242,13 +242,13 @@ We proceed by induction on the semantics.
`γ ⊢ M ↓ (v₁′ ⊔ v₁′′)`. But this does not yet match
what we need for `ℰ L ● ℰ M` because the result of
`L` must be an `↦` whose input entry is `v₁′ ⊔ v₁′′`.
So we use the `sub` rule to obtain
So we use the `sub` rule to obtain
`γ ⊢ L ↓ (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂)`,
using the `Dist⊔→⊔` lemma (thanks to the `Dist⊑` rule) to
show that
(v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂) ⊑ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁)
So we have proved what is needed for this case.
* In case `sub` we have `Γ ⊢ L · M ↓ v₁` and `v ⊑ v₁`.
@ -258,7 +258,7 @@ We proceed by induction on the semantics.
* Suppose `v₁ ⊑ ⊥`. We conclude that `v ⊑ ⊥`.
* Suppose `Γ ⊢ L ↓ v′ → v₁` and `Γ ⊢ M ↓ v′`.
We conclude with `Γ ⊢ L ↓ v′ → v` by rule `sub`, because
`v′ → v ⊑ v′ → v₁`.
`v′ → v ⊑ v′ → v₁`.
The forward direction is proved by cases on the premise `(ℰ L ● ℰ M) γ v`.
@ -280,7 +280,7 @@ function application, as witnessed by the `●` function.
\begin{code}
app-equiv : ∀{Γ}{L M : Γ ⊢ ★}
→ ℰ (L · M) ≃ (ℰ L) ● (ℰ M)
app-equiv γ v = ⟨ ℰ·→●ℰ , ●ℰ→ℰ· ⟩
app-equiv γ v = ⟨ ℰ·→●ℰ , ●ℰ→ℰ· ⟩
\end{code}
We also need an inversion lemma for variables.
@ -331,7 +331,7 @@ whether `ℱ` is a congruence.
→ ℱ D ≃ ℱ D′
ℱ-cong{Γ} D≃D′ γ v =
⟨ (λ x → ℱ≃{γ}{v} x D≃D′) , (λ x → ℱ≃{γ}{v} x (≃-sym D≃D′)) ⟩
where
where
ℱ≃ : ∀{γ : Env Γ}{v}{D D′ : Denotation (Γ , ★)}
→ ℱ D γ v → D ≃ D′ → ℱ D′ γ v
ℱ≃ {v = ⊥} fd dd′ = tt
@ -403,7 +403,7 @@ app-cong {Γ}{L}{L′}{M}{M′} L≅L′ M≅M′ =
ℰ L ● ℰ M
≃⟨ ●-cong L≅L′ M≅M′ ⟩
ℰ L′ ● ℰ M′
≃⟨ ≃-sym app-equiv ⟩
≃⟨ ≃-sym app-equiv ⟩
ℰ (L′ · M′)
☐
\end{code}
@ -443,7 +443,7 @@ data Ctx : Context → Context → Set where
`CAppR`. The `CAppL` is for when the hole is inside the left-hand
term (the operator) and the later is when the hole is inside the
right-hand term (the operand).
The action of surrounding a term with a context is defined by the
following `plug` function. It is defined by recursion on the context.
@ -472,7 +472,7 @@ compositionality {C = CLam C′} M≃N =
compositionality {C = CAppL C′ L} M≃N =
app-cong (compositionality {C = C′} M≃N) λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩
compositionality {C = CAppR L C′} M≃N =
app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C′} M≃N)
app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C′} M≃N)
\end{code}
The proof is a straightforward induction on the context `C`, using the
@ -502,7 +502,7 @@ with the congruence lemmas for `ℱ` and `●`.
\begin{code}
ℰ≃⟦⟧ : ∀ {Γ} {M : Γ ⊢ ★}
→ ℰ M ≃ ⟦ M ⟧
→ ℰ M ≃ ⟦ M ⟧
ℰ≃⟦⟧ {Γ} {` x} = var-equiv
ℰ≃⟦⟧ {Γ} {ƛ N} =
let ih = ℰ≃⟦⟧ {M = N} in
@ -532,4 +532,4 @@ This chapter uses the following unicode:
ℱ U+2131 SCRIPT CAPITAL F (\McF)
● U+2131 BLACK CIRCLE (\cib)

40
src/plfa/Confluence.lagda
View file

@ -45,7 +45,7 @@ diamond property. Here is a counter example.
(λ x. x x)((λ x. x) a) —→ (λ x. x x) a
(λ x. x x)((λ x. x) a) —→ ((λ x. x) a) ((λ x. x) a)
Both terms can reduce to `a a`, but the second term requires two steps
to get there, not one.
@ -144,7 +144,7 @@ data _⇛*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
## Equivalence between parallel reduction and reduction
Here we prove that for any `M` and `N`, `M ⇛* N` if and only if `M —↠ N`.
Here we prove that for any `M` and `N`, `M ⇛* N` if and only if `M —↠ N`.
The only-if direction is particularly easy. We start by showing
that if `M —→ N`, then `M ⇛ N`. The proof is by induction on
the reduction `M —→ N`.
@ -155,7 +155,7 @@ beta-par : ∀{Γ A}{M N : Γ ⊢ A}
------
→ M ⇛ N
beta-par {Γ} {★} {L · M} (ξ₁ r) = papp (beta-par {M = L} r) par-refl
beta-par {Γ} {★} {L · M} (ξ₂ r) = papp par-refl (beta-par {M = M} r)
beta-par {Γ} {★} {L · M} (ξ₂ r) = papp par-refl (beta-par {M = M} r)
beta-par {Γ} {★} {(ƛ N) · M} β = pbeta par-refl par-refl
beta-par {Γ} {★} {ƛ N} (ζ r) = pabs (beta-par r)
\end{code}
@ -212,13 +212,13 @@ The proof is by induction on `M ⇛ N`.
So `L · M —↠ L′ · M` and then `L′ · M —↠ L′ · M′`
because `—↠` is a congruence. We conclude using the transitity
of `—↠`.
* Suppose `(ƛ N) · M ⇛ N′ [ M′ ]` because `N ⇛ N′` and `M ⇛ M′`.
By similar reasoning, we have
`(ƛ N) · M —↠ (ƛ N′) · M′`.
Of course, `(ƛ N′) · M′ —→ N′ [ M′ ]`, so we can conclude
using the transitivity of `—↠`.
With this lemma in hand, we complete the proof that `M ⇛* N` implies
`M —↠ N` with a simple induction on `M ⇛* N`.
@ -325,7 +325,7 @@ We proceed by induction on `M ⇛ M′`.
which we obtain by `par-subst-exts`.
So we have `subst (exts σ) N ⇛ subst (exts τ) N′`
and conclude by rule `pabs`.
* Suppose `L · M ⇛ L′ · M′` because `L ⇛ L′` and `M ⇛ M′`.
By the induction hypothesis we have
`subst σ L ⇛ subst τ L′` and `subst σ M ⇛ subst τ M′`, so
@ -339,7 +339,7 @@ We proceed by induction on `M ⇛ M′`.
to `subst (exts τ) N′ [ subst τ M′ ]`.
Substitution commutes with itself in the following sense.
For any σ, N, and M, we have
(subst (exts σ) N) [ subst σ M ] ≡ subst σ (N [ M ])
So we have parallel reduction to `subst τ (N′ [ M′ ])`.
@ -376,7 +376,7 @@ diamond! We show that parallel reduction satisfies the diamond
property: that if `M ⇛ N` and `M ⇛ N′`, then `N ⇛ L` and `N′ ⇛ L` for
some `L`. The proof is relatively easy; it is parallel reduction's
_raison d'etre_.
\begin{code}
par-diamond : ∀{Γ A} {M N N′ : Γ ⊢ A}
→ M ⇛ N
@ -391,25 +391,25 @@ par-diamond (pabs p1) (pabs p2)
par-diamond{Γ}{A}{L · M}{N}{N′} (papp{Γ}{L}{L₁}{M}{M₁} p1 p3)
(papp{Γ}{L}{L₂}{M}{M₂} p2 p4)
with par-diamond p1 p2
... | ⟨ L₃ , ⟨ p5 , p6 ⟩ ⟩
... | ⟨ L₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ (L₃ · M₃) , ⟨ (papp p5 p7) , (papp p6 p8) ⟩ ⟩
par-diamond (papp (pabs p1) p3) (pbeta p2 p4)
with par-diamond p1 p2
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ N₃ [ M₃ ] , ⟨ pbeta p5 p7 , sub-par p6 p8 ⟩ ⟩
par-diamond (pbeta p1 p3) (papp (pabs p2) p4)
with par-diamond p1 p2
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ (N₃ [ M₃ ]) , ⟨ sub-par p5 p7 , pbeta p6 p8 ⟩ ⟩
par-diamond {Γ}{A} (pbeta p1 p3) (pbeta p2 p4)
with par-diamond p1 p2
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ N₃ [ M₃ ] , ⟨ sub-par p5 p7 , sub-par p6 p8 ⟩ ⟩
@ -454,14 +454,14 @@ The proof is by induction on both premises.
We have both `(ƛ N₁) · M₁ ⇛ N₃ [ M₃ ]`
and `(ƛ N₂) · M₂ ⇛ N₃ [ M₃ ]`
by rule `pbeta`
## Proof of confluence for parallel reduction
As promised at the beginning, the proof that parallel reduction is
confluent is easy now that we know it satisfies the diamond property.
We just need to prove the strip lemma, which states that
if `M ⇒ N` and `M ⇒* N′`, then
if `M ⇒ N` and `M ⇒* N′`, then
`N ⇒* L` and `N′ ⇒ L` for some `L`.
The proof is a straightforward induction on `M ⇒* N′`,
using the diamond property in the induction step.
@ -504,11 +504,11 @@ The step case may be illustrated as follows:
L
/ \
1 *
1 *
/ \
M₁ (a) M₂
/ \ /
* * 1
* * 1
/ \ /
M₁′(b) N
\ /
@ -519,15 +519,15 @@ The step case may be illustrated as follows:
where downward lines are instances of `⇛` or `⇛*`, depending on how
they are marked. Here `(a)` holds by `strip` and `(b)` holds by
induction.
## Proof of confluence for reduction
Confluence of reduction is a corollary of confluence for parallel
reduction. From
reduction. From
`L —↠ M₁` and `L —↠ M₂` we have
`L ⇛* M₁` and `L ⇛* M₂` by `betas-pars`.
Then by confluence we obtain some `L` such that
Then by confluence we obtain some `L` such that
`M₁ ⇛* N` and `M₂ ⇛* N`, from which we conclude that
`M₁ —↠ N` and `M₂ —↠ N` by `pars-betas`.
@ -566,4 +566,4 @@ Homeier's (TPHOLs 2001).
This chapter uses the following unicode:
⇛ U+3015 RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)

4
src/plfa/Connectives.lagda
View file

@ -48,7 +48,7 @@ declaring a suitable inductive type:
\begin{code}
data _×_ (A B : Set) : Set where
⟨_,_⟩ :
⟨_,_⟩ :
A
→ B
-----
@ -718,7 +718,7 @@ an embedding rather than an isomorphism because the
In the usual approach to logic, both of the distribution laws
are given as equivalences, where each side implies the other:
A × (B ⊎ C) ⇔ (A × B) ⊎ (A × C)
A × (B ⊎ C) ⇔ (A × B) ⊎ (A × C)
A ⊎ (B × C) ⇔ (A ⊎ B) × (A ⊎ C)
But when we consider the functions that provide evidence for these

2
src/plfa/ContextualEquivalence.lagda
View file

@ -92,7 +92,7 @@ From `ℰ M ≃ ℰ N`, compositionality gives us
ℰ (plug C M) ≃ ℰ (plug C N).
Putting these two facts together gives us
Putting these two facts together gives us
ℰ (plug C N) ≃ ℰ (ƛN′).

6
src/plfa/DeBruijn.lagda
View file

@ -128,7 +128,7 @@ the term that adds two naturals:
case ` "m"
[zero⇒ ` "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
of `"m"` in the successor branch must refer to the latter
@ -220,7 +220,7 @@ infixl 7 _·_
infix 8 `suc_
infix 9 `_
infix 9 S_
infix 9 #_
infix 9 #_
\end{code}
Since terms are inherently typed, we must define types and
@ -679,7 +679,7 @@ substitution for one free variable:
\begin{code}
_[_] : ∀ {Γ A B}
→ Γ , B ⊢ A
→ Γ ⊢ B
→ Γ ⊢ B
---------
→ Γ ⊢ A
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N

6
src/plfa/Decidable.lagda
View file

@ -544,17 +544,17 @@ postulate
∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
\end{code}
#### Exercise `iff-erasure` (recommended)
Give analogues of the `_⇔_` operation from
Give analogues of the `_⇔_` operation from
Chapter [Isomorphism][plfa.Isomorphism#iff],
operation on booleans and decidables, and also show the corresponding erasure:
\begin{code}
postulate
_iff_ : Bool → Bool → Bool
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
\end{code}
\begin{code}

54
src/plfa/Denotational.lagda
View file

@ -13,7 +13,7 @@ module plfa.Denotational where
The lambda calculus is a language about _functions_, that is, mappings
from input to output. In computing we often think of such
mappings as being carried out by a sequence of
operations that transform an input into an output. But
operations that transform an input into an output. But
functions can also be represented as data. For example, one
can tabulate a function, that is, create a table where each row has
two entries, an input and the corresponding output for the function.
@ -331,7 +331,7 @@ data _⊢_↓_ : ∀{Γ} → Env Γ → (Γ ⊢ ★) → Value → Set where
→ γ ⊢ M ↓ w
---------------
→ γ ⊢ M ↓ (v ⊔ w)
sub : ∀ {Γ} {γ : Env Γ} {M v w}
→ γ ⊢ M ↓ v
→ w ⊑ v
@ -344,7 +344,7 @@ lambda abstraction results in a single-entry table that maps the input
`v` to the output `w`, provided that evaluating the body in an
environment with `v` bound to its parameter produces the output `w`.
As a simple example of this rule, we can see that the identity function
maps `⊥` to `⊥`.
maps `⊥` to `⊥`.
\begin{code}
id : ∅ ⊢ ★
@ -421,7 +421,7 @@ denot-twoᶜ {u}{v}{w} =
↦-intro (↦-intro (↦-elim (sub var lt1) (↦-elim (sub var lt2) var)))
where lt1 : v ↦ w ⊑ u ↦ v ⊔ v ↦ w
lt1 = ConjR2⊑ (Fun⊑ Refl⊑ Refl⊑)
lt2 : u ↦ v ⊑ u ↦ v ⊔ v ↦ w
lt2 = (ConjR1⊑ (Fun⊑ Refl⊑ Refl⊑))
\end{code}
@ -464,7 +464,7 @@ the result of the application is `⊥`.
Ω = Δ · Δ
denot-Ω : `∅ ⊢ Ω ↓ ⊥
denot-Ω = ↦-elim denot-Δ (⊔-intro (↦-intro ⊥-intro) ⊥-intro)
denot-Ω = ↦-elim denot-Δ (⊔-intro (↦-intro ⊥-intro) ⊥-intro)
\end{code}
A shorter derivation of the same result is by just one use of the
@ -636,7 +636,7 @@ We can also characterize divergence and termination using denotations.
* divergence: `¬ (∅ ⊢ M ↓ v ↦ w)` for any `v` and `w`.
* termination: `∅ ⊢ M ↓ v ↦ w` for some `v` and `w`.
Alternatively, we can use the denotation function `ℰ`.
Alternatively, we can use the denotation function `ℰ`.
* divergence: `¬ (ℰ M ≃ ℰ (ƛ N))` for any term `N`.
* termination: `ℰ M ≃ ℰ (ƛ N)` for some term `N`.
@ -722,7 +722,7 @@ rename-pres : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} {M : Γ ⊢ ★}
→ δ ⊢ (rename ρ M) ↓ v
rename-pres ρ lt (var {x = x}) = sub var (lt x)
rename-pres ρ lt (↦-elim d d₁) =
↦-elim (rename-pres ρ lt d) (rename-pres ρ lt d₁)
↦-elim (rename-pres ρ lt d) (rename-pres ρ lt d₁)
rename-pres ρ lt (↦-intro d) =
↦-intro (rename-pres (ext ρ) (ext-nth ρ lt) d)
rename-pres ρ lt ⊥-intro = ⊥-intro
@ -879,7 +879,7 @@ then `v ↦ w` must be a member of `u`.
→ v ↦ w ⊆ u
---------
→ v ↦ w ∈ u
↦⊆→∈ incl = incl refl
↦⊆→∈ incl = incl refl
\end{code}
@ -1051,21 +1051,21 @@ sub-inv-trans {u₁′ ⊔ u₂′} {u₂} {u} fg u′⊆u IH
premise (the induction hypothesis from `u ⊑ u₂`) to obtain that
`u₁′ ↦ u₂′` factors of `u₂ into u₂′`. This case is complete because
`dom u′ ≡ u₁′` and `cod u′ ≡ u₂′`.
* Suppose `u′ ≡ u₁′ ⊔ u₂′`. Then we have `u₁′ ⊆ u` and `u₂′ ⊆ u`. We also
* Suppose `u′ ≡ u₁′ ⊔ u₂′`. Then we have `u₁′ ⊆ u` and `u₂′ ⊆ u`. We also
have `Funs u₁′` and `Funs u₂′`, so we can apply the induction hypothesis
for both `u₁′` and `u₂′`. So there exists values `u₃₁` and `u₃₂` such that
`(dom u₁′) ↦ (cod u₁′)` factors `u` into `u₃₁` and
`(dom u₂′) ↦ (cod u₂′)` factors `u` into `u₃₂`.
We will show that `(dom u) ↦ (cod u)` factors `u` into `u₃₁ ⊔ u₃₂`.
So we need to show that
dom (u₃₁ ⊔ u₃₂) ⊑ dom (u₁′ ⊔ u₂′)
cod (u₁′ ⊔ u₂′) ⊑ cod (u₃₁ ⊔ u₃₂)
But those both follow directly from the factoring of
`u` into `u₃₁` and `u₃₂`, using the monotonicity of `⊔` with respect to `⊑`.
### Inversion of less-than for functions
@ -1085,19 +1085,19 @@ sub-inv {⊥} {u₂} Bot⊑ {v} {w} ()
sub-inv {u₁₁ ⊔ u₁₂} {u₂} (ConjL⊑ lt1 lt2) {v} {w} (inj₁ x) = sub-inv lt1 x
sub-inv {u₁₁ ⊔ u₁₂} {u₂} (ConjL⊑ lt1 lt2) {v} {w} (inj₂ y) = sub-inv lt2 y
sub-inv {u₁} {u₂₁ ⊔ u₂₂} (ConjR1⊑ lt) {v} {w} m
with sub-inv lt m
with sub-inv lt m
... | ⟨ u₃₁ , ⟨ fu₃₁ , ⟨ u₃₁⊆u₂₁ , ⟨ domu₃₁⊑v , w⊑codu₃₁ ⟩ ⟩ ⟩ ⟩ =
⟨ u₃₁ , ⟨ fu₃₁ , ⟨ (λ {w} z → inj₁ (u₃₁⊆u₂₁ z)) ,
⟨ domu₃₁⊑v , w⊑codu₃₁ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁} {u₂₁ ⊔ u₂₂} (ConjR2⊑ lt) {v} {w} m
with sub-inv lt m
with sub-inv lt m
... | ⟨ u₃₂ , ⟨ fu₃₂ , ⟨ u₃₂⊆u₂₂ , ⟨ domu₃₂⊑v , w⊑codu₃₂ ⟩ ⟩ ⟩ ⟩ =
⟨ u₃₂ , ⟨ fu₃₂ , ⟨ (λ {C} z → inj₂ (u₃₂⊆u₂₂ z)) ,
⟨ domu₃₂⊑v , w⊑codu₃₂ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁} {u₂} (Trans⊑{v = u} u₁⊑u u⊑u₂) {v} {w} v↦w∈u₁
with sub-inv u₁⊑u v↦w∈u₁
... | ⟨ u′ , ⟨ fu′ , ⟨ u′⊆u , ⟨ domu′⊑v , w⊑codu′ ⟩ ⟩ ⟩ ⟩
with sub-inv-trans {u′} fu′ u′⊆u (sub-inv u⊑u₂)
... | ⟨ u′ , ⟨ fu′ , ⟨ u′⊆u , ⟨ domu′⊑v , w⊑codu′ ⟩ ⟩ ⟩ ⟩
with sub-inv-trans {u′} fu′ u′⊆u (sub-inv u⊑u₂)
... | ⟨ u₃ , ⟨ fu₃ , ⟨ u₃⊆u₂ , ⟨ domu₃⊑domu′ , codu′⊑codu₃ ⟩ ⟩ ⟩ ⟩ =
⟨ u₃ , ⟨ fu₃ , ⟨ u₃⊆u₂ , ⟨ Trans⊑ domu₃⊑domu′ domu′⊑v ,
Trans⊑ w⊑codu′ codu′⊑codu₃ ⟩ ⟩ ⟩ ⟩
@ -1128,7 +1128,7 @@ Let `v` and `w` be arbitrary values.
* Subcase `v ↦ w ∈ u₁₁`. We conclude by the induction
hypothesis for `u₁₁ ⊑ u₂`.
* Subcase `v ↦ w ∈ u₁₂`. We conclude by the induction hypothesis
for `u₁₂ ⊑ u₂`.
@ -1147,12 +1147,12 @@ Let `v` and `w` be arbitrary values.
* Case `ConjR2⊑`. This case follows by reasoning similar to
the case for `ConjR1⊑`.
* Case `Trans⊑`.
* Case `Trans⊑`.
u₁ ⊑ u u ⊑ u₂
---------------
u₁ ⊑ u₂
By the induction hypothesis for `u₁ ⊑ u`, we know
that `v ↦ w` factors `u` into `u′`, for some value `u′`,
so we have `Funs u′` and `u′ ⊆ u`.
@ -1217,12 +1217,12 @@ less-than with functions on the left and right-hand sides.
-----------------
→ v′ ⊑ v × w ⊑ w′
↦⊑↦-inv{v}{w}{v′}{w′} lt
with sub-inv-fun lt
with sub-inv-fun lt
... | ⟨ Γ , ⟨ f , ⟨ Γ⊆v34 , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩
with Funs∈ f
... | ⟨ u , ⟨ u′ , u↦u′∈Γ ⟩ ⟩
with Γ⊆v34 u↦u′∈Γ
... | refl =
... | refl =
let codΓ⊆w′ = ⊆↦→cod⊆ Γ⊆v34 in
⟨ lt1 u↦u′∈Γ , Trans⊑ lt2 (⊆→⊑ codΓ⊆w′) ⟩
\end{code}
@ -1257,9 +1257,9 @@ technical report by Gordon Plotkin (1972) and are later described in
an article in Theoretical Computer Science (Plotkin 1993). In that
work, the inductive definition of `Value` is a bit different than the
one we use:
Value = C + ℘f(Value) × ℘f(Value)
where `C` is a set of constants and `℘f` means finite powerset. The
pairs in `℘f(Value) × ℘f(Value)` represent input-output mappings, just
as in this chapter. The finite powersets are used to enable a function
@ -1277,9 +1277,9 @@ version.
Dana Scott's ℘(ω) (1976) and Engeler's B(A) (1981) are two more
examples of graph models. Both use the following inductive definition
of `Value`.
Value = C + ℘f(Value) × Value
The use of `Value` instead of `℘f(Value)` in the output does not restrict
expressiveness compared to Plotkin's model because the semantics use
sets of values and a pair of sets `(V, V′)` can be represented as a set
@ -1333,7 +1333,7 @@ This chapter uses the following unicode:
⊔ U+2294 SQUARE CUP (\lub)
⊑ U+2291 SQUARE IMAGE OF OR EQUAL TO (\sqsubseteq)
⊢ U+22A2 RIGHT TACK (\|- or \vdash)
↓ U+2193 DOWNWARDS ARROW (\d)
↓ U+2193 DOWNWARDS ARROW (\d)
ᶜ U+1D9C MODIFIER LETTER SMALL C (\^c)
ℰ U+2130 SCRIPT CAPITAL E (\McE)
≃ U+2243 ASYMPTOTICALLY EQUAL TO (\~- or \simeq)

8
src/plfa/Fonts.lagda
View file

@ -28,7 +28,7 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
----------|
------------------------|
αβγδεζηθικλμνξοπρστυφχψω|
ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
------------------------|
----|
≠≠≠≠|
@ -36,13 +36,13 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
ΓΓΔΔ|
ΣΣΠΠ|
λλλλ|
ƛƛƛƛ|
ƛƛƛƛ|
····|
××××|
ℓℓℓℓ|
≡≡≡≡|
¬¬¬¬|
≤≤≥≥|
≤≤≥≥|
∅∅∅∅|
————|
††‡‡|
@ -75,7 +75,7 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
∈∈∋∋|
⊢⊢⊣⊣|
⊥⊥⊤⊤|
∷∷∷∷|
∷∷∷∷|
∎∎∎∎|
⦂⦂⦂⦂|
∥∥∥∥|

12
src/plfa/Inference.lagda
View file

@ -11,7 +11,7 @@ module plfa.Inference where
\end{code}
So far in our development, type derivations for the corresponding
term have been provided by fiat.
term have been provided by fiat.
In Chapter [Lambda][plfa.Lambda]
type derivations were given separately from the term, while
in Chapter [DeBruijn][plfa.DeBruijn]
@ -87,7 +87,7 @@ as output. Consider the rules:
Γ ⊢ ` x ⦂ A
Γ , x ⦂ A ⊢ N ⦂ B
---------------------------
---------------------------
Γ ⊢ (ƛ x ⦂ A ⇒ N) ⦂ (A ⇒ B)
Γ ⊢ L ⦂ A ⇒ B
@ -260,7 +260,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
Once we have a type derivation, it will be easy to construct
from it the inherently typed representation. In order that we
can compare with our previous development, we import
module `pfla.DeBruijn`:
module `pfla.DeBruijn`:
\begin{code}
import plfa.DeBruijn as DB
@ -564,7 +564,7 @@ that `A` and `B` must be identical:
uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
uniq-↑ (⊢` ∋x) (⊢` ∋x′) = uniq-∋ ∋x ∋x′
uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′) = rng≡ (uniq-↑ ⊢L ⊢L′)
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′) = refl
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′) = refl
\end{code}
There are three possibilities for the term. If it is a variable,
uniqueness of synthesis follows from uniqueness of lookup.
@ -706,7 +706,7 @@ synthesize Γ (L · M) with synthesize Γ L
... | yes ⟨ `ℕ , ⊢L ⟩ = no (λ{ ⟨ _ , ⊢L′ · _ ⟩ → ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
... | no ¬⊢M = no (¬arg ⊢L ¬⊢M)
... | yes ⊢M = yes ⟨ B , ⊢L · ⊢M ⟩
... | yes ⊢M = yes ⟨ B , ⊢L · ⊢M ⟩
synthesize Γ (M ↓ A) with inherit Γ M A
... | no ¬⊢M = no (λ{ ⟨ _ , ⊢↓ ⊢M ⟩ → ¬⊢M ⊢M })
... | yes ⊢M = yes ⟨ A , ⊢↓ ⊢M ⟩
@ -773,7 +773,7 @@ inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
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) })
... | yes ⟨ _ ⇒ _ , ⊢L ⟩ = no (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
... | yes ⟨ `ℕ , ⊢L ⟩ with inherit Γ M A
... | no ¬⊢M = no (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
... | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A

2
src/plfa/Isomorphism.lagda
View file

@ -431,7 +431,7 @@ postulate
≃-implies-≲ : ∀ {A B : Set}
→ A ≃ B
-----
→ A ≲ B
→ A ≲ B
\end{code}
\begin{code}

4
src/plfa/Lambda.lagda
View file

@ -39,7 +39,7 @@ variables, partly because such terms are easier to read and partly
because the development is more traditional.
The development in this chapter was inspired by the corresponding
development in Chapter _Stlc_ of _Software Foundations_
development in Chapter _Stlc_ of _Software Foundations_
(_Programming Language Foundations_). We differ by
representing contexts explicitly (as lists pairing identifiers with
types) rather than as partial maps (which take identifiers to types),
@ -548,7 +548,7 @@ the rules for reduction of applications are written as follows:
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
quantifications are made explicit, and so are the predicates that indicate

2
src/plfa/Lists.lagda
View file

@ -439,7 +439,7 @@ reverses xs =
shunt xs []
≡⟨ shunt-reverse xs [] ⟩
reverse xs ++ []
≡⟨ ++-identityʳ (reverse xs) ⟩
≡⟨ ++-identityʳ (reverse xs) ⟩
reverse xs
∎
\end{code}

12
src/plfa/More.lagda
View file

@ -160,7 +160,7 @@ construct to a calculus without the construct.
`proj₂ L project second component
V, W ::= ... Values
`⟨ V , W ⟩ pair
`⟨ V , W ⟩ pair
### Typing
@ -226,7 +226,7 @@ and reduction rules:
case× L [⟨ x , y ⟩=> M ] case
V, W ::= Values
`⟨ V , W ⟩ pair
`⟨ V , W ⟩ pair
### Typing
@ -249,7 +249,7 @@ and reduction rules:
Here is a function to swap the components of a pair rewritten in the new notation:
swap×-case : ∅ ⊢ A `× B ⇒ B `× A
swap×-case = ƛ z ⇒ case× z
swap×-case = ƛ z ⇒ case× z
[⟨ x , y ⟩⇒ `⟨ y , x ⟩ ]
### Translation
@ -386,7 +386,7 @@ Here is the isomorphism between `A` and ``A `× `⊤``:
## Alternative formulation of unit type
There is an alternative formulation of the unit type, where in place of
There is an alternative formulation of the unit type, where in place of
no way to eliminate the type we have a case term that binds zero variables.
We repeat the syntax in full, but only give the new type and reduction rules:
@ -614,7 +614,7 @@ data _∋_ : Context → Type → Set where
→ Γ ∋ B
---------
→ Γ , A ∋ B
\end{code}
\end{code}
### Terms and the typing judgment
@ -1131,7 +1131,7 @@ cube : ∅ ⊢ Nat ⇒ Nat
cube = ƛ (# 0 `* # 0 `* # 0)
_ : cube · con 2 —↠ con 8
_ =
_ =
begin
cube · con 2
—→⟨ β-ƛ V-con ⟩

26
src/plfa/Properties.lagda
View file

@ -153,7 +153,7 @@ data Canonical_⦂_ : Term → Type → Set where
→ Canonical V ⦂ `ℕ
---------------------
→ Canonical `suc V ⦂ `ℕ
\end{code}
\end{code}
Every closed, well-typed value is canonical:
\begin{code}
@ -170,7 +170,7 @@ canonical (⊢suc ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV)
canonical (⊢case ⊢L ⊢M ⊢N) ()
canonical (⊢μ ⊢M) ()
\end{code}
There are only three interesting cases to consider:
There are only three interesting cases to consider:
* If the term is a lambda abstraction, then well-typing of the term
guarantees well-typing of the body.
@ -274,7 +274,7 @@ progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
progress (⊢μ ⊢M) = step β-μ
\end{code}
We induct on the evidence that the term is well-typed.
Let's unpack the first three cases:
Let's unpack the first three cases:
* The term cannot be a variable, since no variable is well typed
in the empty context.
@ -411,7 +411,7 @@ to substitution by closed terms in order to avoid the need to
rename bound variables. The term into which we are substituting
is typed in an arbitrary context `Γ`, extended by the variable
`x` for which we are substituting; and the result term is typed
in `Γ`.
in `Γ`.
The lemma establishes that substitution composes well with typing:
typing the components separately guarantees that the result of
@ -446,7 +446,7 @@ and `Γ , x ⦂ A` appears in a hypothesis. Thus:
Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B
for lambda expressions, and similarly for case and fixpoint. To deal
with this situation, we first prove a lemma showing that if one context maps to another,
with this situation, we first prove a lemma showing that if one context maps to another,
this is still true after adding the same variable to
both contexts:
\begin{code}
@ -652,7 +652,7 @@ Now that naming is resolved, let's unpack the first three cases:
where the second hypothesis follows from:
Γ , y ⦂ B ∋ x ⦂ A
There are two subcases, depending on the evidence for this judgment:
+ The lookup judgment is evidenced by rule `Z`:
@ -725,7 +725,7 @@ Now that naming is resolved, let's unpack the first three cases:
-------------------------
Γ , x ⦂ A ⊢ N ⦂ C
The typing rule for abstractions then yields the required conclusion.
The typing rule for abstractions then yields the required conclusion.
+ If the variables are distinct then after simplification we must show:
@ -743,7 +743,7 @@ Now that naming is resolved, let's unpack the first three cases:
The inductive hypothesis gives us:
∅ ⊢ V ⦂ B
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
------------------------------------
Γ , x ⦂ A , y ⦂ B ⊢ N [ y := V ] ⦂ C
@ -810,7 +810,7 @@ preserve ⊢zero ()
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 ⊢zero ⊢M ⊢N) β-zero = ⊢M
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV) = subst ⊢V ⊢N
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV) = subst ⊢V ⊢N
preserve (⊢μ ⊢M) (β-μ) = subst (⊢μ ⊢M) ⊢M
\end{code}
The proof never mentions the types of `M` or `N`,
@ -936,7 +936,7 @@ reduction finished:
data Steps (L : Term) : Set where
steps : ∀ {N}
→ L —↠ N
→ L —↠ N
→ Finished N
----------
→ Steps L
@ -970,7 +970,7 @@ remaining. There are two possibilities:
+ Term `L` is a value, so we are done. We return the
trivial reduction sequence `L —↠ L`, evidence that `L` is
well-typed, and the evidence that `L` is a value.
+ Term `L` steps to another term `M`. Preservation provides
evidence that `M` is also well-typed, and we recursively invoke
`eval` on the remaining gas. The result is evidence that
@ -1425,7 +1425,7 @@ three typical cases:
By induction we have `L′ ≡ L″`, and hence by congruence
`L′ · M ≡ L″ · M`.
* An instance of `ξ-·₁` and an instance of `ξ-·₂`:
Value L
@ -1440,7 +1440,7 @@ three typical cases:
* Two instances of `β-ƛ`:
Value V Value V
Value V Value V
----------------------------- β-ƛ ----------------------------- β-ƛ
(ƛ x ⇒ N) · V —→ N [ x := V ] (ƛ x ⇒ N) · V —→ N [ x := V ]

2
src/plfa/Quantifiers.lagda
View file

@ -36,7 +36,7 @@ proposition `∀ (x : A) → B x` holds if for every term `M` of type
`A` the proposition `B M` holds. Here `B M` stands for
the proposition `B x` with each free occurrence of `x` replaced by
`M`. Variable `x` appears free in `B x` but bound in
`∀ (x : A) → B x`.
`∀ (x : A) → B x`.
Evidence that `∀ (x : A) → B x` holds is of the form

6
src/plfa/Relations.lagda
View file

@ -305,7 +305,7 @@ length obscures the essence of the proof. We will usually opt for
shorter proofs.
The technique of induction on evidence that a property holds (e.g.,
inducting on evidence that `m ≤ n`)---rather than induction on
inducting on evidence that `m ≤ n`)---rather than induction on
values of which the property holds (e.g., inducting on `m`)---will turn
out to be immensely valuable, and one that we use often.
@ -341,7 +341,7 @@ and `suc n ≤ suc m` and must show `suc m ≡ suc n`. The inductive
hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, and our goal
follows by congruence.
#### Exercise `≤-antisym-cases` {#leq-antisym-cases}
#### Exercise `≤-antisym-cases` {#leq-antisym-cases}
The above proof omits cases where one argument is `z≤n` and one
argument is `s≤s`. Why is it ok to omit them?
@ -741,7 +741,7 @@ Show that the sum of two odd numbers is even.
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
Recall that
Recall that
Exercise [Bin][plfa.Naturals#Bin]
defines a datatype `Bin` of bitstrings representing natural numbers.
Representations are not unique due to leading zeros.

44
src/plfa/Soundness.lagda
View file

@ -38,7 +38,7 @@ open import plfa.Untyped
subst; _[_]; subst-zero; ext; rename; exts)
open import plfa.LambdaReduction
using (_—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _[])
open import plfa.Substitution using (Rename; Subst; ids)
open import plfa.Substitution using (Rename; Subst; ids)
open import plfa.Denotational
using (Value; ⊥; Env; _⊢_↓_; _`,_; _⊑_; _`⊑_; `⊥; _`⊔_; init; last; init-last;
Refl⊑; Trans⊑; `Refl⊑; Env⊑; EnvConjR1⊑; EnvConjR2⊑; up-env;
@ -107,7 +107,7 @@ The proof is by cases on the de Bruijn index `x`.
* If it is `Z`, then we need to show that `δ , v ⊢ # 0 ↓ v`,
which we have by rule `var`.
* If it is `S x′`,then we need to show that
* If it is `S x′`,then we need to show that
`δ , v ⊢ rename S_ (σ x′) ↓ nth x′ γ`,
which we obtain by the `rename-pres` lemma.
@ -123,7 +123,7 @@ subst-pres : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} {M : Γ ⊢ ★}
→ δ ⊢ subst σ M ↓ v
subst-pres σ s (var {x = x}) = (s x)
subst-pres σ s (↦-elim d₁ d₂) =
↦-elim (subst-pres σ s d₁) (subst-pres σ s d₂)
↦-elim (subst-pres σ s d₁) (subst-pres σ s d₂)
subst-pres σ s (↦-intro d) =
↦-intro (subst-pres (λ {A} → exts σ) (subst-ext σ s) d)
subst-pres σ s ⊥-intro = ⊥-intro
@ -159,7 +159,7 @@ substitution : ∀ {Γ} {γ : Env Γ} {N M v w}
→ γ `, v ⊢ N ↓ w
→ γ ⊢ M ↓ v
---------------
→ γ ⊢ N [ M ] ↓ w
→ γ ⊢ N [ M ] ↓ w
substitution{Γ}{γ}{N}{M}{v}{w} dn dm =
subst-pres (subst-zero M) sub-z-ok dn
where
@ -193,8 +193,8 @@ preserve : ∀ {Γ} {γ : Env Γ} {M N v}
----------
→ γ ⊢ N ↓ v
preserve (var) ()
preserve (↦-elim d₁ d₂) (ξ₁ r) = ↦-elim (preserve d₁ r) d₂
preserve (↦-elim d₁ d₂) (ξ₂ r) = ↦-elim d₁ (preserve d₂ r)
preserve (↦-elim d₁ d₂) (ξ₁ r) = ↦-elim (preserve d₁ r) d₂
preserve (↦-elim d₁ d₂) (ξ₂ r) = ↦-elim d₁ (preserve d₂ r)
preserve (↦-elim d₁ d₂) β = substitution (lambda-inversion d₁) d₂
preserve (↦-intro d) (ζ r) = ↦-intro (preserve d r)
preserve ⊥-intro r = ⊥-intro
@ -271,7 +271,7 @@ rename-reflect {M = ƛ N} all-n (⊔-intro d₁ d₂) =
rename-reflect {M = ƛ N} all-n (sub d₁ lt) =
sub (rename-reflect all-n d₁) lt
rename-reflect {M = L · M} all-n (↦-elim d₁ d₂) =
↦-elim (rename-reflect all-n d₁) (rename-reflect all-n d₂)
↦-elim (rename-reflect all-n d₁) (rename-reflect all-n d₂)
rename-reflect {M = L · M} all-n ⊥-intro = ⊥-intro
rename-reflect {M = L · M} all-n (⊔-intro d₁ d₂) =
⊔-intro (rename-reflect all-n d₁) (rename-reflect all-n d₂)
@ -419,7 +419,7 @@ subst-⊥ x = ⊥-intro
\end{code}
If a substitution produces terms that evaluate to the values in
both `γ₁` and `γ₂`, then those terms also evaluate to the values in
both `γ₁` and `γ₂`, then those terms also evaluate to the values in
`γ₁ ⊔ γ₂`.
\begin{code}
@ -463,15 +463,15 @@ subst-reflect : ∀ {Γ Δ} {δ : Env Δ} {M : Γ ⊢ ★} {v} {L : Δ ⊢ ★}
---------------------------------------
→ Σ[ γ ∈ Env Γ ] δ `⊢ σ ↓ γ × γ ⊢ M ↓ v
subst-reflect {M = M}{σ = σ} (var {x = y}) eqL with M
subst-reflect {M = M}{σ = σ} (var {x = y}) eqL with M
... | ` x with var {x = y}
... | yv rewrite sym eqL = subst-reflect-var {σ = σ} yv
subst-reflect {M = M} (var {x = y}) () | M₁ · M₂
subst-reflect {M = M} (var {x = y}) () | ƛ M′
subst-reflect {M = M}{σ = σ} (↦-elim d₁ d₂) eqL
with M
... | ` x with ↦-elim d₁ d₂
with M
... | ` x with ↦-elim d₁ d₂
... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′
subst-reflect (↦-elim d₁ d₂) () | ƛ M′
subst-reflect{Γ}{Δ}{γ}{σ = σ} (↦-elim d₁ d₂)
@ -487,10 +487,10 @@ subst-reflect {M = M}{σ = σ} (↦-intro d) eqL with M
... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′
subst-reflect {σ = σ} (↦-intro d) eq | ƛ M′
with subst-reflect {σ = exts σ} d (lambda-inj eq)
... | ⟨ δ′ , ⟨ exts-σ-δ′ , m′ ⟩ ⟩ =
... | ⟨ δ′ , ⟨ exts-σ-δ′ , m′ ⟩ ⟩ =
⟨ init δ′ , ⟨ ((λ x → rename-inc-reflect (exts-σ-δ′ (S x)))) ,
↦-intro (up-env (split m′) (var-inv (exts-σ-δ′ Z))) ⟩ ⟩
subst-reflect (↦-intro d) () | M₁ · M₂
subst-reflect (↦-intro d) () | M₁ · M₂
subst-reflect {σ = σ} ⊥-intro eq =
⟨ `⊥ , ⟨ subst-⊥ {σ = σ} , ⊥-intro ⟩ ⟩
@ -501,7 +501,7 @@ subst-reflect {σ = σ} (⊔-intro d₁ d₂) eq
⟨ δ₁ `⊔ δ₂ , ⟨ subst-⊔ {γ₁ = δ₁}{γ₂ = δ₂}{σ = σ} subst-δ₁ subst-δ₂ ,
⊔-intro (Env⊑ m1 (EnvConjR1⊑ δ₁ δ₂))
(Env⊑ m2 (EnvConjR2⊑ δ₁ δ₂)) ⟩ ⟩
subst-reflect (sub d lt) eq
subst-reflect (sub d lt) eq
with subst-reflect d eq
... | ⟨ δ , ⟨ subst-δ , m ⟩ ⟩ = ⟨ δ , ⟨ subst-δ , sub m lt ⟩ ⟩
\end{code}
@ -544,7 +544,7 @@ subst-reflect (sub d lt) eq
by `Env⊑` with `EnvConjR1⊑` and `EnvConjR2⊑`.
So by `⊔-intro` we have `δ₁ ⊔ δ₂ ⊢ M ↓ v₁ ⊔ v₂`.
By `subst-⊔` we conclude that `δ ⊢ σ ↓ δ₁ ⊔ δ₂`.
### Single substitution reflects denotations
@ -565,7 +565,7 @@ subst-zero-reflect : ∀ {Δ} {δ : Env Δ} {γ : Env (Δ , ★)} {M : Δ ⊢
→ δ `⊢ subst-zero M ↓ γ
----------------------------------------
→ Σ[ w ∈ Value ] γ `⊑ (δ `, w) × δ ⊢ M ↓ w
subst-zero-reflect {δ = δ} {γ = γ} δσγ = ⟨ last γ , ⟨ lemma , δσγ Z ⟩ ⟩
subst-zero-reflect {δ = δ} {γ = γ} δσγ = ⟨ last γ , ⟨ lemma , δσγ Z ⟩ ⟩
where
lemma : γ `⊑ (δ `, last γ)
lemma Z = Refl⊑
@ -609,9 +609,9 @@ easily prove that reduction does too.
reflect-beta : ∀{Γ}{γ : Env Γ}{M N}{v}
→ γ ⊢ (N [ M ]) ↓ v
→ γ ⊢ (ƛ N) · M ↓ v
reflect-beta d
reflect-beta d
with substitution-reflect d
... | ⟨ v₂′ , ⟨ d₁′ , d₂′ ⟩ ⟩ = ↦-elim (↦-intro d₂′) d₁′
... | ⟨ v₂′ , ⟨ d₁′ , d₂′ ⟩ ⟩ = ↦-elim (↦-intro d₂′) d₁′
reflect : ∀ {Γ} {γ : Env Γ} {M M′ N v}
@ -622,10 +622,10 @@ reflect var (ξ₁ r) ()
reflect var (ξ₂ r) ()
reflect{γ = γ} (var{x = x}) β mn
with var{γ = γ}{x = x}
... | d′ rewrite sym mn = reflect-beta d′
... | d′ rewrite sym mn = reflect-beta d′
reflect var (ζ r) ()
reflect (↦-elim d₁ d₂) (ξ₁ r) refl = ↦-elim (reflect d₁ r refl) d₂
reflect (↦-elim d₁ d₂) (ξ₂ r) refl = ↦-elim d₁ (reflect d₂ r refl)
reflect (↦-elim d₁ d₂) (ξ₁ r) refl = ↦-elim (reflect d₁ r refl) d₂
reflect (↦-elim d₁ d₂) (ξ₂ r) refl = ↦-elim d₁ (reflect d₂ r refl)
reflect (↦-elim d₁ d₂) β mn
with ↦-elim d₁ d₂
... | d′ rewrite sym mn = reflect-beta d′
@ -639,7 +639,7 @@ reflect (↦-intro d) (ζ r) refl = ↦-intro (reflect d r refl)
reflect ⊥-intro r mn = ⊥-intro
reflect (⊔-intro d₁ d₂) r mn rewrite sym mn =
⊔-intro (reflect d₁ r refl) (reflect d₂ r refl)
reflect (sub d lt) r mn = sub (reflect d r mn) lt
reflect (sub d lt) r mn = sub (reflect d r mn) lt
\end{code}
## Reduction implies denotational equality

45
src/plfa/Substitution.lagda
View file

@ -16,7 +16,7 @@ module plfa.Substitution where
The primary purpose of this chapter is to prove that substitution
commutes with itself. Barendgredt (1984) refers to this
as the substitution lemma:
M [x:=N] [y:=L] = M [y:=L] [x:= N[y:=L] ]
In our setting, with de Bruijn indices for variables, the statement of
@ -134,7 +134,7 @@ Given two substitutions `σ` and `τ`, the sequencing operation `σ ⨟ τ`
produces the sequence
⟪τ⟫(σ 0), ⟪τ⟫(σ 1), ⟪τ⟫(σ 2), ...
That is, it composes the two substitutions by first applying
`σ` and then applying `τ`.
@ -159,7 +159,7 @@ The σ algebra includes the following equations.
(sub-tail) ↑ ⨟ (M • σ) ≡ σ
(sub-η) (⟪ σ ⟫ (` Z)) • (↑ ⨟ σ) ≡ σ
(Z-shift) (` Z) • ↑ ≡ ids
(sub-id) ⟪ ids ⟫ M ≡ M
(sub-app) ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M)
(sub-abs) ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ σ ⟫ N
@ -217,7 +217,7 @@ When the renaming is the increment function, then it is equivalent to
shift.
ren S_ ≡ ↑ (ren-shift)
rename S_ M ≡ ⟪ ↑ ⟫ M (rename-shift)
Renaming with the identity renaming leaves the term unchanged.
@ -280,10 +280,10 @@ sub-tail = extensionality λ x → refl
\end{code}
\begin{code}
sub-η : ∀{Γ Δ} {A B} {σ : Subst (Γ , A) Δ}
sub-η : ∀{Γ Δ} {A B} {σ : Subst (Γ , A) Δ}
→ (⟪ σ ⟫ (` Z) • (↑ ⨟ σ)) {A = B} ≡ σ
sub-η {Γ}{Δ}{A}{B}{σ} = extensionality λ x → lemma
where
where
lemma : ∀ {x} → ((⟪ σ ⟫ (` Z)) • (↑ ⨟ σ)) x ≡ σ x
lemma {x = Z} = refl
lemma {x = S x} = refl
@ -292,7 +292,7 @@ sub-η {Γ}{Δ}{A}{B}{σ} = extensionality λ x → lemma
\begin{code}
Z-shift : ∀{Γ}{A B}
→ ((` Z) • ↑) ≡ ids {Γ , A} {B}
Z-shift {Γ}{A}{B} = extensionality lemma
Z-shift {Γ}{A}{B} = extensionality lemma
where
lemma : (x : Γ , A ∋ B) → ((` Z) • ↑) x ≡ ids x
lemma Z = refl
@ -319,7 +319,7 @@ sub-dist {Γ}{Δ}{Σ}{A}{B}{σ}{τ}{M} = extensionality λ x → lemma {x = x}
\begin{code}
sub-app : ∀{Γ Δ} {σ : Subst Γ Δ} {L : Γ ⊢ ★}{M : Γ ⊢ ★}
→ ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M)
sub-app = refl
sub-app = refl
\end{code}
@ -378,7 +378,7 @@ cong-sub : ∀{Γ Δ}{σ σ′ : Subst Γ Δ}{A}{M M′ : Γ ⊢ A}
cong-sub {Γ} {Δ} {σ} {σ′} {A} {` x} ss refl = cong-app ss x
cong-sub {Γ} {Δ} {σ} {σ′} {A} {ƛ M} ss refl =
cong ƛ_ (cong-sub {σ = exts σ}{σ′ = exts σ′} {M = M} (cong-exts ss) refl)
cong-sub {Γ} {Δ} {σ} {σ′} {A} {L · M} ss refl =
cong-sub {Γ} {Δ} {σ} {σ′} {A} {L · M} ss refl =
cong₂ _·_ (cong-sub {M = L} ss refl) (cong-sub {M = M} ss refl)
\end{code}
@ -412,7 +412,7 @@ cong-seq {Γ}{Δ}{Σ}{σ}{σ′}{τ}{τ′} ss' tt' {A} = extensionality lemma
lemma : (x : Γ ∋ A) → (σ ⨟ τ) x ≡ (σ′ ⨟ τ′) x
lemma x =
begin
(σ ⨟ τ) x
(σ ⨟ τ) x
≡⟨⟩
subst τ (σ x)
≡⟨ cong (subst τ) (cong-app ss' x) ⟩
@ -420,7 +420,7 @@ cong-seq {Γ}{Δ}{Σ}{σ}{σ′}{τ}{τ′} ss' tt' {A} = extensionality lemma
≡⟨ cong-sub{M = σ′ x} tt' refl ⟩
subst τ′ (σ′ x)
≡⟨⟩
(σ′ ⨟ τ′) x
(σ′ ⨟ τ′) x
∎
\end{code}
@ -434,7 +434,7 @@ in the σ algebra.
The first equation we prove is
rename ρ M ≡ ⟪ ren ρ ⟫ M (rename-subst-ren)
Because `subst` uses the `exts` function, we need the following lemma
which says that `exts` and `ext` do the same thing except that `ext`
works on renamings and `exts` works on substitutions.
@ -517,7 +517,7 @@ exts-cons-shift = extensionality λ x → lemma{x = x}
As a corollary, we have a similar correspondence for `ren (ext ρ)`.
\begin{code}
ext-cons-Z-shift : ∀{Γ Δ} {ρ : Rename Γ Δ}{A}{B}
ext-cons-Z-shift : ∀{Γ Δ} {ρ : Rename Γ Δ}{A}{B}
→ ren (ext ρ {B = B}) ≡ (` Z • (ren ρ ⨟ ↑)) {A}
ext-cons-Z-shift {Γ}{Δ}{ρ}{A}{B} =
begin
@ -582,7 +582,7 @@ using `exts-ids` in the case for `M ≡ ƛ N`.
sub-id : ∀{Γ} {A} {M : Γ ⊢ A}
→ ⟪ ids ⟫ M ≡ M
sub-id {M = ` x} = refl
sub-id {M = ƛ N} =
sub-id {M = ƛ N} =
begin
⟪ ids ⟫ (ƛ N)
≡⟨⟩
@ -598,7 +598,7 @@ sub-id {M = L · M} = cong₂ _·_ sub-id sub-id
The `rename-id` equation is a corollary is `sub-id`.
\begin{code}
rename-id : ∀ {Γ}{A} {M : Γ ⊢ A}
rename-id : ∀ {Γ}{A} {M : Γ ⊢ A}
→ rename (λ {A} x → x) M ≡ M
rename-id {M = M} =
begin
@ -660,7 +660,7 @@ the other using `rename`, we proceed by induction on the term `M`,
using the `compose-ext` lemma in the case for `M ≡ ƛ N`.
\begin{code}
compose-rename : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A}{ρ : Rename Δ Σ}{ρ′ : Rename Γ Δ}
compose-rename : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A}{ρ : Rename Δ Σ}{ρ′ : Rename Γ Δ}
→ rename ρ (rename ρ′ M) ≡ rename (ρ ∘ ρ′) M
compose-rename {M = ` x} = refl
compose-rename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ′} = cong ƛ_ G
@ -673,7 +673,7 @@ compose-rename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ′} = cong ƛ_ G
rename ((ext ρ) ∘ (ext ρ′)) N
≡⟨ cong-rename compose-ext refl ⟩
rename (ext (ρ ∘ ρ′)) N
∎
∎
compose-rename {M = L · M} = cong₂ _·_ compose-rename compose-rename
\end{code}
@ -701,7 +701,7 @@ commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r =
begin
exts (exts σ) (ext ρ (S y))
≡⟨⟩
rename S_ (exts σ (ρ y))
rename S_ (exts σ (ρ y))
≡⟨ cong (rename S_) r ⟩
rename S_ (rename ρ (σ y))
≡⟨ compose-rename ⟩
@ -735,7 +735,7 @@ The proof is by induction on the term `M`.
* If `x = S y`, we obtain the goal by the following equational reasoning.
exts (exts σ) (ext ρ (S y))
≡ rename S_ (exts σ (ρ y))
≡ rename S_ (exts σ (ρ y))
≡ rename S_ (rename S_ (σ (ρ y) (by the premise)
≡ rename (ext ρ) (exts σ (S y)) (by compose-rename)
≡ rename ((ext ρ) ∘ S_) (σ y)
@ -786,7 +786,7 @@ The proof proceed by cases on `x`.
Now we come to the proof of `sub-sub`, which we explain below.
\begin{code}
sub-sub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ}
sub-sub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ}
→ ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ M) ≡ ⟪ σ₁ ⨟ σ₂ ⟫ M
sub-sub {M = ` x} = refl
sub-sub {Γ}{Δ}{Σ}{A}{ƛ N}{σ₁}{σ₂} =
@ -806,7 +806,7 @@ We proceed by induction on the term `M`.
* If `M = x`, then both sides are equal to `σ₂ (σ₁ x)`.
* If `M = ƛ N`, we first use the induction hypothesis to show that
* If `M = ƛ N`, we first use the induction hypothesis to show that
ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N
@ -906,7 +906,7 @@ normal form
⟪ ⟪ σ ⟫ M • σ ⟫ N
We then do the same with the right-hand side, arriving at the same
normal form.
normal form.
\begin{code}
subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{σ : Subst Γ Δ }
@ -1010,4 +1010,3 @@ This chapter uses the following unicode:
〔 U+3014 LEFT TORTOISE SHELL BRACKET (\( option 9 on page 2)
〕 U+3015 RIGHT TORTOISE SHELL BRACKET (\) option 9 on page 2)

6
src/plfa/Untyped.lagda
View file

@ -277,7 +277,7 @@ subst-zero M (S x) = ` x
_[_] : ∀ {Γ A B}
→ Γ , B ⊢ A
→ Γ ⊢ B
→ Γ ⊢ B
---------
→ Γ ⊢ A
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} (subst-zero M) {A} N
@ -356,7 +356,7 @@ data Application : ∀ {Γ A} → Γ ⊢ A → Set where
The reduction rules are altered to switch from call-by-value to
call-by-name and to enable full normalisation:
* In rule `ξ₁`, the function term is required to be an application,
* In rule `ξ₁`, the function term is required to be an application,
to avoid conflict with rule `β`.
* In rule `ξ₂`, the function term is required to be neutral
@ -731,7 +731,7 @@ plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
\end{code}
Because `` `suc `` is now a defined term rather than primitive,
it is no longer the case that `plus · two · two` reduces to `four`,
but they do both reduce to the same normal term.
but they do both reduce to the same normal term.
#### Exercise `plus-eval`