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

changed rule names in Lambda, Prop to match Inference

Browse source
This commit is contained in:
wadler 2018-06-24 19:45:51 -03:00
parent 2786ffb059
commit 3ba45ceb62
3 changed files with 100 additions and 81 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/plta/Inference.lagda
View file

@ -149,7 +149,7 @@ data _⊢_↑_ where
data _⊢_↓_ where
⊢λ : ∀ {Γ x N A B}
⊢ƛ : ∀ {Γ x N A B}
→ Γ , x ⦂ A ⊢ N ↓ B
-----------------------
→ Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B
@ -246,7 +246,7 @@ synthesize Γ (M ↓ A) =
inherit Γ (ƛ x ⇒ N) (A ⇒ B) =
do ⊢N ← inherit (Γ , x ⦂ A) N B
return (⊢λ ⊢N)
return (⊢ƛ ⊢N)
inherit Γ (ƛ x ⇒ N) `ℕ =
error⁻ "lambda cannot be of type natural" (ƛ x ⇒ N) []
inherit Γ `zero `ℕ =
@ -289,8 +289,8 @@ x ≠ y with x ≟ y
⊢four =
(⊢↓
(⊢μ
(⊢λ
(⊢λ
(⊢ƛ
(⊢ƛ
(⊢case (Ax (S (_≠_ "m" "n") Z)) (⊢↑ (Ax Z) refl)
(⊢suc
(⊢↑
@ -309,13 +309,13 @@ _ = refl
⊢fourCh : ε ⊢ fourCh ↑ `ℕ
⊢fourCh =
(⊢↓ (⊢λ (⊢↑ (Ax Z · ⊢λ (⊢suc (⊢↑ (Ax Z) refl)) · ⊢zero) refl)) ·
(⊢↓ (⊢ƛ (⊢↑ (Ax Z · ⊢ƛ (⊢suc (⊢↑ (Ax Z) refl)) · ⊢zero) refl)) ·
⊢↑
(⊢↓
(⊢λ
(⊢λ
(⊢λ
(⊢λ
(⊢ƛ
(⊢ƛ
(⊢ƛ
(⊢ƛ
(⊢↑
(Ax
(S (_≠_ "m" "z")
@ -332,16 +332,16 @@ _ = refl
refl)
refl)))))
·
⊢λ
(⊢λ
⊢ƛ
(⊢ƛ
(⊢↑
(Ax (S (_≠_ "s" "z") Z) ·
⊢↑ (Ax (S (_≠_ "s" "z") Z) · ⊢↑ (Ax Z) refl)
refl)
refl))
·
⊢λ
(⊢λ
⊢ƛ
(⊢ƛ
(⊢↑
(Ax (S (_≠_ "s" "z") Z) ·
⊢↑ (Ax (S (_≠_ "s" "z") Z) · ⊢↑ (Ax Z) refl)
@ -391,6 +391,7 @@ _ : synthesize ε (((ƛ "x" ⇒ ⌊ "x" ⌋ ↑) ↓ `ℕ ⇒ (`ℕ ⇒ `ℕ)))
_ = refl
\end{code}
## Erasure
\begin{code}
@ -409,7 +410,7 @@ _ = refl
∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻
∥ ⊢λ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻
∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻
∥ ⊢zero ∥⁻ = DB.`zero
∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻
∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.`caseℕ ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻

49
src/plta/Lambda.lagda
View file

@ -905,38 +905,38 @@ data _⊢_⦂_ : Context → Term → Type → Set where
→ Γ ⊢ ⌊ x ⌋ ⦂ A
-- ⇒-I
⇒-I : ∀ {Γ x N A B}
⊢ƛ : ∀ {Γ x N A B}
→ Γ , x ⦂ A ⊢ N ⦂ B
-------------------
→ Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B
-- ⇒-E
⇒-E : ∀ {Γ L M A B}
_·_ : ∀ {Γ L M A B}
→ Γ ⊢ L ⦂ A ⇒ B
→ Γ ⊢ M ⦂ A
-------------
→ Γ ⊢ L · M ⦂ B
-- ℕ-I₁
ℕ-I₁ : ∀ {Γ}
⊢zero : ∀ {Γ}
--------------
→ Γ ⊢ `zero ⦂ `ℕ
-- ℕ-I₂
ℕ-I₂ : ∀ {Γ M}
⊢suc : ∀ {Γ M}
→ Γ ⊢ M ⦂ `ℕ
---------------
→ Γ ⊢ `suc M ⦂ `ℕ
-- ℕ-E
ℕ-E : ∀ {Γ L M x N A}
⊢case : ∀ {Γ L M x N A}
→ Γ ⊢ L ⦂ `ℕ
→ Γ ⊢ M ⦂ A
→ Γ , x ⦂ `ℕ ⊢ N ⦂ A
-------------------------------------
→ Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ⦂ A
Fix : ∀ {Γ x M A}
⊢μ : ∀ {Γ x M A}
→ Γ , x ⦂ A ⊢ M ⦂ A
-----------------
→ Γ ⊢ μ x ⇒ M ⦂ A
@ -1002,9 +1002,9 @@ is a type derivation for the Church numberal two:
Γ₂ ⊢ ⌊ "s" ⌋ ⦂ A ⇒ A Γ₂ ⊢ ⌊ "s" ⌋ · ⌊ "z" ⌋ ⦂ A
-------------------------------------------------- _·_
Γ₂ ⊢ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A
---------------------------------------------- ƛ_
---------------------------------------------- ⊢ƛ
Γ₁ ⊢ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A ⇒ A
---------------------------------------------------------- ƛ_
---------------------------------------------------------- ⊢ƛ
∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋) ⦂ A ⇒ A
where `∋s` and `∋z` abbreviate the two derivations:
@ -1022,7 +1022,7 @@ Ch : Type → Type
Ch A = (A ⇒ A) ⇒ A ⇒ A
⊢twoᶜ : ∀ {A} → ∅ ⊢ twoᶜ ⦂ Ch A
⊢twoᶜ = ⇒-I (⇒-I (⇒-E (Ax ∋s) (⇒-E (Ax ∋s) (Ax ∋z))))
⊢twoᶜ = ⊢ƛ (⊢ƛ (Ax ∋s · (Ax ∋s · Ax ∋z)))
where
∋s = S ("s" ≠ "z") Z
@ -1032,11 +1032,11 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A
Here are the typings corresponding to our first example.
\begin{code}
⊢two : ∅ ⊢ two ⦂ `ℕ
⊢two = ℕ-I₂ (ℕ-I₂ ℕ-I₁)
⊢two = ⊢suc (⊢suc ⊢zero)
⊢plus : ∅ ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
⊢plus = Fix (⇒-I (⇒-I (ℕ-E (Ax ∋m) (Ax ∋n)
(ℕ-I₂ (⇒-E (⇒-E (Ax ∋+) (Ax ∋m′)) (Ax ∋n′))))))
⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (Ax ∋m) (Ax ∋n)
(⊢suc (Ax ∋+ · Ax ∋m′ · Ax ∋n′)))))
where
∋+ = (S ("+" ≠ "m") (S ("+" ≠ "n") (S ("+" ≠ "m") Z)))
∋m = (S ("m" ≠ "n") Z)
@ -1045,7 +1045,7 @@ Here are the typings corresponding to our first example.
∋n′ = (S ("n" ≠ "m") Z)
⊢four : ∅ ⊢ four ⦂ `ℕ
⊢four = ⇒-E (⇒-E ⊢plus ⊢two) ⊢two
⊢four = ⊢plus · ⊢two · ⊢two
\end{code}
The two occcurrences of variable `"n"` in the original term appear
in different contexts, and correspond here to the two different
@ -1057,8 +1057,7 @@ branch of the case expression.
Here are typings for the remainder of the Church example.
\begin{code}
⊢plusᶜ : ∀ {A} → ∅ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
⊢plusᶜ = ⇒-I (⇒-I (⇒-I (⇒-I (⇒-E (⇒-E (Ax ∋m) (Ax ∋s))
(⇒-E (⇒-E (Ax ∋n) (Ax ∋s)) (Ax ∋z))))))
⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (Ax ∋m · Ax ∋s · (Ax ∋n · Ax ∋s · Ax ∋z)))))
where
∋m = S ("m" ≠ "z") (S ("m" ≠ "s") (S ("m" ≠ "n") Z))
∋n = S ("n" ≠ "z") (S ("n" ≠ "s") Z)
@ -1066,12 +1065,12 @@ Here are typings for the remainder of the Church example.
∋z = Z
⊢sucᶜ : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ
⊢sucᶜ = ⇒-I (ℕ-I₂ (Ax ∋n))
⊢sucᶜ = ⊢ƛ (⊢suc (Ax ∋n))
where
∋n = Z
⊢fourᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ
⊢fourᶜ = ⇒-E (⇒-E (⇒-E (⇒-E ⊢plusᶜ ⊢twoᶜ) ⊢twoᶜ) ⊢sucᶜ) ℕ-I₁
⊢fourᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero
\end{code}
@ -1089,20 +1088,20 @@ Typing 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ᶜ` in `ƛ`, which is typed using `⇒-I`. The
`⇒-I` rule in turn takes one argument, which Agda leaves as a hole.
the outermost term in `sucᶜ` in `⊢ƛ`, which is typed using `ƛ`. The
`ƛ` rule in turn takes one argument, which Agda leaves as a hole.
⊢sucᶜ = ⇒-I { }1
⊢sucᶜ = ⊢ƛ { }1
?1 : ∅ , "n" ⦂ `ℕ ⊢ `suc ⌊ "n" ⌋ ⦂ `ℕ
We can fill in the hole by type C-c C-r again.
⊢sucᶜ = ⇒-I (`ℕ-I₂ { }2)
⊢sucᶜ = ⊢ƛ (⊢suc { }2)
?2 : ∅ , "n" ⦂ `ℕ ⊢ ⌊ "n" ⌋ ⦂ `ℕ
And again.
⊢suc′ = ⇒-I (ℕ-I₂ (Ax { }3))
⊢suc′ = ⊢ƛ (⊢suc (Ax { }3))
?3 : ∅ , "n" ⦂ `ℕ ∋ "n" ⦂ `ℕ
A further attempt with C-c C-r yields the message:
@ -1111,7 +1110,7 @@ A further attempt with C-c C-r yields the message:
We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are done.
⊢suc′ = ⇒-I (ℕ-I₂ (Ax Z))
⊢suc′ = ⊢ƛ (⊢suc (Ax Z))
The entire process can be automated using Agsy, invoked with C-c C-a.
@ -1144,7 +1143,7 @@ application is both a natural and a function.
\begin{code}
nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A)
nope₁ (⇒-E () _)
nope₁ (() · _)
\end{code}
As a second example, here is a formal proof that it is not possible to
@ -1153,7 +1152,7 @@ doing so requires types `A` and `B` such that `A ⇒ B ≡ A`.
\begin{code}
nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ⌊ "x" ⌋ · ⌊ "x" ⌋ ⦂ A)
nope₂ (⇒-I (⇒-E (Ax ∋x) (Ax ∋x′))) = contradiction (∋-injective ∋x ∋x′)
nope₂ (⊢ƛ (Ax ∋x · Ax ∋x′)) = contradiction (∋-injective ∋x ∋x′)
where
contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A)
contradiction ()

103
src/plta/LambdaProp.lagda
View file

@ -75,13 +75,13 @@ canonical : ∀ {M A}
→ Value M
---------------
→ Canonical M ⦂ A
canonical (Ax ()) ()
canonical (⇒-I ⊢N) V-ƛ = C-ƛ
canonical (⇒-E ⊢L ⊢M) ()
canonical ℕ-I₁ V-zero = C-zero
canonical (ℕ-I₂ ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV)
canonical (ℕ-E ⊢L ⊢M ⊢N) ()
canonical (Fix ⊢M) ()
canonical (Ax ()) ()
canonical (⊢ƛ ⊢N) V-ƛ = C-ƛ
canonical (⊢L · ⊢M) ()
canonical ⊢zero V-zero = C-zero
canonical (⊢suc ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV)
canonical (⊢case ⊢L ⊢M ⊢N) ()
canonical (⊢μ ⊢M) ()
value : ∀ {M A}
→ Canonical M ⦂ A
@ -116,23 +116,23 @@ progress : ∀ {M A}
----------
→ Progress M
progress (Ax ())
progress (⇒-I ⊢N) = done V-ƛ
progress (⇒-E ⊢L ⊢M) with progress ⊢L
progress (⊢ƛ ⊢N) = done V-ƛ
progress (⊢L · ⊢M) with progress ⊢L
... | step L⟶L′ = step (ξ-·₁ L⟶L′)
... | done VL with progress ⊢M
... | step M⟶M′ = step (ξ-·₂ VL M⟶M′)
... | done VM with canonical ⊢L VL
... | C-ƛ = step (β-ƛ· VM)
progress ℕ-I₁ = done V-zero
progress (ℕ-I₂ ⊢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 (ℕ-E ⊢L ⊢M ⊢N) with progress ⊢L
progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
... | step L⟶L′ = step (ξ-case L⟶L′)
... | done VL with canonical ⊢L VL
... | C-zero = step β-case-zero
... | C-suc CL = step (β-case-suc (value CL))
progress (Fix ⊢M) = step β-μ
progress (⊢μ ⊢M) = step β-μ
\end{code}
This code reads neatly in part because we consider the
@ -204,13 +204,13 @@ rename : ∀ {Γ Δ}
→ (∀ {w B} → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B)
----------------------------------
→ (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename σ (Ax ∋w) = Ax (σ ∋w)
rename σ (⇒-I ⊢N) = ⇒-I (rename (ext σ) ⊢N)
rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M)
rename σ ℕ-I₁ = ℕ-I₁
rename σ (ℕ-I₂ ⊢M) = ℕ-I₂ (rename σ ⊢M)
rename σ (ℕ-E ⊢L ⊢M ⊢N) = ℕ-E (rename σ ⊢L) (rename σ ⊢M) (rename (ext σ) ⊢N)
rename σ (Fix ⊢M) = Fix (rename (ext σ) ⊢M)
rename σ (Ax ∋w) = Ax (σ ∋w)
rename σ (⊢ƛ ⊢N) = ⊢ƛ (rename (ext σ) ⊢N)
rename σ (⊢L · ⊢M) = (rename σ ⊢L) · (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 σ (⊢μ ⊢M) = ⊢μ (rename (ext σ) ⊢M)
\end{code}
We have three important corollaries. First,
@ -316,18 +316,18 @@ subst {x = y} (Ax {x = x} Z) ⊢V with x ≟ y
subst {x = y} (Ax {x = x} (S x≢y ∋x)) ⊢V with x ≟ y
... | yes refl = ⊥-elim (x≢y refl)
... | no _ = Ax ∋x
subst {x = y} (⇒-I {x = x} ⊢N) ⊢V with x ≟ y
... | yes refl = ⇒-I (rename-≡ ⊢N)
... | no x≢y = ⇒-I (subst (rename-≢ x≢y ⊢N) ⊢V)
subst (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (subst ⊢L ⊢V) (subst ⊢M ⊢V)
subst ℕ-I₁ ⊢V = ℕ-I₁
subst (ℕ-I₂ ⊢M) ⊢V = ℕ-I₂ (subst ⊢M ⊢V)
subst {x = y} (ℕ-E {x = x} ⊢L ⊢M ⊢N) ⊢V with x ≟ y
... | yes refl = ℕ-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (rename-≡ ⊢N)
... | no x≢y = ℕ-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (subst (rename-≢ x≢y ⊢N) ⊢V)
subst {x = y} (Fix {x = x} ⊢M) ⊢V with x ≟ y
... | yes refl = Fix (rename-≡ ⊢M)
... | no x≢y = Fix (subst (rename-≢ x≢y ⊢M) ⊢V)
subst {x = y} (⊢ƛ {x = x} ⊢N) ⊢V with x ≟ y
... | yes refl = ⊢ƛ (rename-≡ ⊢N)
... | no x≢y = ⊢ƛ (subst (rename-≢ x≢y ⊢N) ⊢V)
subst (⊢L · ⊢M) ⊢V = (subst ⊢L ⊢V) · (subst ⊢M ⊢V)
subst ⊢zero ⊢V = ⊢zero
subst (⊢suc ⊢M) ⊢V = ⊢suc (subst ⊢M ⊢V)
subst {x = y} (⊢case {x = x} ⊢L ⊢M ⊢N) ⊢V with x ≟ y
... | yes refl = ⊢case (subst ⊢L ⊢V) (subst ⊢M ⊢V) (rename-≡ ⊢N)
... | no x≢y = ⊢case (subst ⊢L ⊢V) (subst ⊢M ⊢V) (subst (rename-≢ x≢y ⊢N) ⊢V)
subst {x = y} (⊢μ {x = x} ⊢M) ⊢V with x ≟ y
... | yes refl = ⊢μ (rename-≡ ⊢M)
... | no x≢y = ⊢μ (subst (rename-≢ x≢y ⊢M) ⊢V)
\end{code}
@ -345,18 +345,37 @@ preserve : ∀ {M N A}
----------
→ ∅ ⊢ N ⦂ A
preserve (Ax ())
preserve (⇒-I ⊢N) ()
preserve (⇒-E ⊢L ⊢M) (ξ-·₁ L⟶L′) = ⇒-E (preserve ⊢L L⟶L′) ⊢M
preserve (⇒-E ⊢L ⊢M) (ξ-·₂ VL M⟶M′) = ⇒-E ⊢L (preserve ⊢M M⟶M′)
preserve (⇒-E (⇒-I ⊢N) ⊢V) (β-ƛ· VV) = subst ⊢N ⊢V
preserve ℕ-I₁ ()
preserve (ℕ-I₂ ⊢M) (ξ-suc M⟶M′) = ℕ-I₂ (preserve ⊢M M⟶M′)
preserve (ℕ-E ⊢L ⊢M ⊢N) (ξ-case L⟶L′) = ℕ-E (preserve ⊢L L⟶L′) ⊢M ⊢N
preserve (ℕ-E ℕ-I₁ ⊢M ⊢N) β-case-zero = ⊢M
preserve (ℕ-E (ℕ-I₂ ⊢V) ⊢M ⊢N) (β-case-suc VV) = subst ⊢N ⊢V
preserve (Fix ⊢M) (β-μ) = subst ⊢M (Fix ⊢M)
preserve (⊢ƛ ⊢N) ()
preserve (⊢L · ⊢M) (ξ-·₁ L⟶L′) = (preserve ⊢L L⟶L′) · ⊢M
preserve (⊢L · ⊢M) (ξ-·₂ VL M⟶M′) = ⊢L · (preserve ⊢M M⟶M′)
preserve ((⊢ƛ ⊢N) · ⊢V) (β-ƛ· VV) = subst ⊢N ⊢V
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) β-case-zero = ⊢M
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-case-suc VV) = subst ⊢N ⊢V
preserve (⊢μ ⊢M) (β-μ) = subst ⊢M (⊢μ ⊢M)
\end{code}
## Normalisation with streams
codata Lift (A : Set) where
lift : A → Lift A
data _↠_ : Term → Term → Set where
_∎ : ∀ (M : Term)
-----
→ M ↠ M
_↦⟨_⟩_ : ∀ (L : Term) {M N : Term}
→ L ⟶ M
→ Lift (M ↠ N)
------------
→ L ↠ N
## Normalisation
\begin{code}