added type derivations to Lambda

This commit is contained in:
wadler 2018-05-21 15:28:55 -03:00
parent f9e21d7ecf
commit 78a1163f0a
2 changed files with 136 additions and 31 deletions

View file

@ -116,14 +116,20 @@ Here are some example terms: the naturals two and four, the recursive
definition of a function to naturals, and a term that computes
two plus two.
\begin{code}
tm2 tm4 tm+ tm2+2 : Term
tm2 = `suc `suc `zero
tm4 = `suc `suc `suc `suc `zero
tm+ = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case # "m"
[zero⇒ # "n"
|suc "m" ⇒ `suc (# "+" · # "m" · # "n") ]
tm2+2 = tm+ · tm2 · tm2
tm2 : Term
tm2 = `suc `suc `zero
tm4 : Term
tm4 = `suc `suc `suc `suc `zero
tm+ : Term
tm+ = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
`case # "m"
[zero⇒ # "n"
|suc "m" ⇒ `suc (# "+" · # "m" · # "n") ]
tm2+2 : Term
tm2+2 = tm+ · tm2 · tm2
\end{code}
The recursive definition of addition is similar to our original
definition of `_+_` for naturals, as given in Chapter [Natural](Naturals).
@ -136,13 +142,21 @@ naturals. Similar to before, we define: the numerals two and four, a
function to add numerals, a function to convert numerals to naturals,
and a term that computes two plus two.
\begin{code}
ch2 ch4 ch+ ch ch2+2 : Term
ch2 = ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · # "z")
ch4 = ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · (# "s" · (# "s" · # "z")))
ch+ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
# "m" · # "s" · (# "n" · # "s" · # "z")
ch = ƛ "n" ⇒ # "n" · (ƛ "m" ⇒ `suc (# "m")) · `zero
ch2+2 = ch+ · ch2 · ch2
ch2 : Term
ch2 = ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · # "z")
ch4 : Term
ch4 = ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · (# "s" · (# "s" · # "z")))
ch+ : Term
ch+ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
# "m" · # "s" · (# "n" · # "s" · # "z")
ch : Term
ch = ƛ "m" ⇒ # "m" · (ƛ "n" ⇒ `suc (# "n")) · `zero
ch2+2 : Term
ch2+2 = ch · (ch+ · ch2 · ch2)
\end{code}
Two takes two arguments `s` and `z`, and applies `s` twice to `z`;
similarly for four. Addition takes two numerals `m` and `n`, a
@ -840,14 +854,68 @@ Here is the above derivation formalised in Agda.
\begin{code}
⊢ch2 : ∅ ⊢ ch2 ⦂ (` ⇒ `) ⇒ ` ⇒ `
⊢ch2 = ⇒-I (⇒-I (⇒-E (Ax ⊢s) (⇒-E (Ax ⊢s) (Ax ⊢z))))
⊢ch2 = ⇒-I (⇒-I (⇒-E (Ax ∋s) (⇒-E (Ax ∋s) (Ax ∋z))))
where
s≢z : "s" ≢ "z"
s≢z ()
⊢s = S s≢z Z
⊢z = Z
∋s = S s≢z Z
∋z = Z
\end{code}
\begin{code}
⊢tm2 : ∅ ⊢ tm2 ⦂ `
⊢tm2 = -I₂ (-I₂ -I₁)
⊢tm4 : ∅ ⊢ tm4 ⦂ `
⊢tm4 = -I₂ (-I₂ (-I₂ (-I₂ -I₁)))
⊢tm+ : ∅ ⊢ tm+ ⦂ ` ⇒ ` ⇒ `
⊢tm+ = Fix (⇒-I (⇒-I (-E (Ax ∋m) (Ax ∋n)
(-I₂ (⇒-E (⇒-E (Ax ∋+) (Ax ∋m)) (Ax ∋n))))))
where
∋+ = (S (λ()) (S (λ()) (S (λ()) Z)))
∋m = (S (λ()) Z)
∋n = Z
∋m = Z
∋n = (S (λ()) Z)
⊢tm2+2 : ∅ ⊢ tm2+2 ⦂ `
⊢tm2+2 = ⇒-E (⇒-E ⊢tm+ ⊢tm2) ⊢tm2
\end{code}
Typing for the rest of the Church terms.
\begin{code}
Ch : Type → Type
Ch A = (A ⇒ A) ⇒ A ⇒ A
⊢ch4 : ∀ {A} → (∅ ⊢ ch4 ⦂ (Ch A))
⊢ch4 = ⇒-I (⇒-I (⇒-E (Ax ∋s) (⇒-E (Ax ∋s)
(⇒-E (Ax ∋s) (⇒-E (Ax ∋s) (Ax ∋z))))))
where
∋s = S (λ()) Z
∋z = Z
⊢ch+ : ∀ {A} → ∅ ⊢ ch+ ⦂ Ch A ⇒ Ch A ⇒ Ch A
⊢ch+ = ⇒-I (⇒-I (⇒-I (⇒-I (⇒-E (⇒-E (Ax ∋m) (Ax ∋s))
(⇒-E (⇒-E (Ax ∋n) (Ax ∋s)) (Ax ∋z))))))
where
∋m = S (λ()) (S (λ()) (S (λ()) Z))
∋n = S (λ()) (S (λ()) Z)
∋s = S (λ()) Z
∋z = Z
⊢ch : ∅ ⊢ ch ⦂ Ch ` ⇒ `
⊢ch = ⇒-I (⇒-E (⇒-E (Ax ∋m) (⇒-I (-I₂ (Ax ∋n)))) -I₁)
where
∋m = Z
∋n = Z
⊢ch2+2 : ∅ ⊢ ch2+2 ⦂ `
⊢ch2+2 = ⇒-E (⊢ch) (⇒-E (⇒-E ⊢ch+ ⊢ch2) ⊢ch2)
\end{code}

View file

@ -14,6 +14,7 @@ module LambdaProp where
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Data.String using (String; _≟_)
open import Data.Nat using (; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product
using (_×_; proj₁; proj₂; ∃; ∃-syntax)
@ -81,7 +82,7 @@ step or it is a value.
\begin{code}
data Progress (M : Term) : Set where
steps : ∀ {N}
step : ∀ {N}
→ M ⟹ N
----------
→ Progress M
@ -98,29 +99,29 @@ progress : ∀ {M A}
progress (Ax ())
progress (⇒-I ⊢N) = done V-ƛ
progress (⇒-E ⊢L ⊢M) with progress ⊢L
... | steps L⟹L = steps (ξ-·₁ L⟹L)
... | step L⟹L = step (ξ-·₁ L⟹L)
... | done VL with progress ⊢M
... | steps M⟹M = steps (ξ-·₂ VL M⟹M)
... | step M⟹M = step (ξ-·₂ VL M⟹M)
... | done VM with canonical ⊢L VL
... | C-ƛ = steps (β-ƛ· VM)
... | C-ƛ = step (β-ƛ· VM)
progress -I₁ = done V-zero
progress (-I₂ ⊢M) with progress ⊢M
... | steps M⟹M = steps (ξ-suc M⟹M)
... | step M⟹M = step (ξ-suc M⟹M)
... | done VM = done (V-suc VM)
progress (-E ⊢L ⊢M ⊢N) with progress ⊢L
... | steps L⟹L = steps (ξ-case L⟹L)
... | step L⟹L = step (ξ-case L⟹L)
... | done VL with canonical ⊢L VL
... | C-zero = steps β-case-zero
... | C-suc CL = steps (β-case-suc (value CL))
progress (Fix ⊢M) = steps β-μ
... | C-zero = step β-case-zero
... | C-suc CL = step (β-case-suc (value CL))
progress (Fix ⊢M) = step β-μ
\end{code}
This code reads neatly in part because we consider the
`steps` option before the `done` option. We could, of course,
`step` option before the `done` option. We could, of course,
do it the other way around, but then the `...` abbreviation
no longer works, and we will need to write out all the arguments
in full. In general, the rule of thumb is to consider the easy case
(here `steps`) before the hard case (here `done`).
(here `step`) before the hard case (here `done`).
If you have two hard cases, you will have to expand out `...`
or introduce subsidiary functions.
@ -341,6 +342,42 @@ preserve (-E (-I₂ ⊢V) ⊢M ⊢N) (β-case-suc VV) = subst ⊢N ⊢V
preserve (Fix ⊢M) (β-μ) = subst ⊢M (Fix ⊢M)
\end{code}
## Normalisation
\begin{code}
Gas : Set
Gas =
data Normalise (M : Term) : Set where
out-of-gas : ∀ {N A}
→ M ⟹* N
→ ∅ ⊢ N ⦂ A
-------------
→ Normalise M
normal : ∀ {V}
→ Gas
→ M ⟹* V
→ Value V
--------------
→ Normalise M
normalise : ∀ {M A}
→ ∅ ⊢ M ⦂ A
-----------
→ Normalise M
normalise {L} zero ⊢L = out-of-gas (L ∎) ⊢L
normalise {L} (suc m) ⊢L with progress ⊢L
... | done VL = normal (suc m) (L ∎) VL
... | step L⟹M with normalise m (preserve ⊢L L⟹M)
... | out-of-gas M⟹*N ⊢N = out-of-gas (L ⟹⟨ L⟹M ⟩ M⟹*N) ⊢N
... | normal n M⟹*V VV = normal n (L ⟹⟨ L⟹M ⟩ M⟹*V) VV
\end{code}
#### Exercise: 2 stars, recommended (subject_expansion_stlc)
@ -390,8 +427,8 @@ Soundness : ∀ {M N A}
-----------
→ ¬ (Stuck N)
Soundness ⊢M (M ∎) ⟨ ¬M⟹N , ¬VM ⟩ with progress ⊢M
... | steps M⟹N = ¬M⟹N M⟹N
... | done VM = ¬VM VM
... | step M⟹N = ¬M⟹N M⟹N
... | done VM = ¬VM VM
Soundness ⊢L (L ⟹⟨ L⟹M ⟩ M⟹*N) = Soundness (preserve ⊢L L⟹M) M⟹*N
\end{code}
</div>