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

updated variables in Lambda and LambdaProp

Browse source
This commit is contained in:
wadler 2018-06-24 18:48:47 -03:00
parent 2b01695f50
commit 2786ffb059
2 changed files with 65 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/plta/Lambda.lagda
View file

@ -93,12 +93,8 @@ correspond to introduction rules and deconstructors to eliminators.
Here is the syntax of terms in BNF. Here is the syntax of terms in BNF.
L, M, N ::= L, M, N ::=
⌊ x ⌋ ⌊ x ⌋ | ƛ x ⇒ N | L · M |
ƛ x ⇒ N `zero | `suc M | `case L [zero⇒ M |suc x ⇒ N] |
L · M
`zero
`suc M
`case L [zero⇒ M |suc x ⇒ N]
μ x ⇒ M μ x ⇒ M
And here it is formalised in Agda. And here it is formalised in Agda.
@ -110,7 +106,6 @@ infix 6 ƛ_⇒_
infix 6 μ_⇒_ infix 6 μ_⇒_
infixl 7 _·_ infixl 7 _·_
infix 8 `suc_ infix 8 `suc_
infix 9 ⌊_⌋
data Term : Set where data Term : Set where
⌊_⌋ : Id → Term ⌊_⌋ : Id → Term

125
src/plta/LambdaProp.lagda
View file

@ -41,6 +41,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_) open import Function using (_∘_)
open import plta.Lambda open import plta.Lambda
open Chain (Term) (_⟶_)
\end{code} \end{code}
@ -398,36 +399,36 @@ _ : normalise 100 ⊢four ≡
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· `suc (`suc `zero) · `suc (`suc `zero)
· `suc (`suc `zero) · `suc (`suc `zero)
⟶⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩ ⟶⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· # "n") · ⌊ "n" ⌋)
])) ]))
· `suc (`suc `zero) · `suc (`suc `zero)
· `suc (`suc `zero) · `suc (`suc `zero)
⟶⟨ ξ-·₁ (β-ƛ· (V-suc (V-suc V-zero))) ⟩ ⟶⟨ ξ-·₁ (β-ƛ· (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒ (ƛ "n" ⇒
`case `suc (`suc `zero) [zero⇒ # "n" |suc "m" ⇒ `case `suc (`suc `zero) [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· # "n") · ⌊ "n" ⌋)
]) ])
· `suc (`suc `zero) · `suc (`suc `zero)
⟶⟨ β-ƛ· (V-suc (V-suc V-zero)) ⟩ ⟶⟨ β-ƛ· (V-suc (V-suc V-zero)) ⟩
@ -436,9 +437,9 @@ _ : normalise 100 ⊢four ≡
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· `suc (`suc `zero)) · `suc (`suc `zero))
] ]
⟶⟨ β-case-suc (V-suc V-zero) ⟩ ⟶⟨ β-case-suc (V-suc V-zero) ⟩
@ -446,7 +447,7 @@ _ : normalise 100 ⊢four ≡
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· `suc `zero · `suc `zero
· `suc (`suc `zero)) · `suc (`suc `zero))
@ -454,30 +455,30 @@ _ : normalise 100 ⊢four ≡
`suc `suc
((ƛ "m" ⇒ ((ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· # "n") · ⌊ "n" ⌋)
])) ]))
· `suc `zero · `suc `zero
· `suc (`suc `zero)) · `suc (`suc `zero))
⟶⟨ ξ-suc (ξ-·₁ (β-ƛ· (V-suc V-zero))) ⟩ ⟶⟨ ξ-suc (ξ-·₁ (β-ƛ· (V-suc V-zero))) ⟩
`suc `suc
((ƛ "n" ⇒ ((ƛ "n" ⇒
`case `suc `zero [zero⇒ # "n" |suc "m" ⇒ `case `suc `zero [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· # "n") · ⌊ "n" ⌋)
]) ])
· `suc (`suc `zero)) · `suc (`suc `zero))
⟶⟨ ξ-suc (β-ƛ· (V-suc (V-suc V-zero))) ⟩ ⟶⟨ ξ-suc (β-ƛ· (V-suc (V-suc V-zero))) ⟩
@ -487,9 +488,9 @@ _ : normalise 100 ⊢four ≡
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· `suc (`suc `zero)) · `suc (`suc `zero))
] ]
⟶⟨ ξ-suc (β-case-suc V-zero) ⟩ ⟶⟨ ξ-suc (β-case-suc V-zero) ⟩
@ -498,7 +499,7 @@ _ : normalise 100 ⊢four ≡
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· `zero · `zero
· `suc (`suc `zero))) · `suc (`suc `zero)))
@ -507,15 +508,15 @@ _ : normalise 100 ⊢four ≡
(`suc (`suc
((ƛ "m" ⇒ ((ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· # "n") · ⌊ "n" ⌋)
])) ]))
· `zero · `zero
· `suc (`suc `zero))) · `suc (`suc `zero)))
@ -523,15 +524,15 @@ _ : normalise 100 ⊢four ≡
`suc `suc
(`suc (`suc
((ƛ "n" ⇒ ((ƛ "n" ⇒
`case `zero [zero⇒ # "n" |suc "m" ⇒ `case `zero [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒
`suc `suc
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· # "n") · ⌊ "n" ⌋)
]) ])
· `suc (`suc `zero))) · `suc (`suc `zero)))
⟶⟨ ξ-suc (ξ-suc (β-ƛ· (V-suc (V-suc V-zero)))) ⟩ ⟶⟨ ξ-suc (ξ-suc (β-ƛ· (V-suc (V-suc V-zero)))) ⟩
@ -542,9 +543,9 @@ _ : normalise 100 ⊢four ≡
((μ "+" ⇒ ((μ "+" ⇒
(ƛ "m" ⇒ (ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (# "+" · # "m" · # "n") `case ⌊ "m" ⌋ [zero⇒ ⌊ "n" ⌋ |suc "m" ⇒ `suc (⌊ "+" ⌋ · ⌊ "m" ⌋ · ⌊ "n" ⌋)
]))) ])))
· # "m" · ⌊ "m" ⌋
· `suc (`suc `zero)) · `suc (`suc `zero))
]) ])
⟶⟨ ξ-suc (ξ-suc β-case-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎) ⟶⟨ ξ-suc (ξ-suc β-case-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎)
@ -557,60 +558,60 @@ _ : normalise 100 ⊢fourᶜ ≡
normal 88 normal 88
((ƛ "m" ⇒ ((ƛ "m" ⇒
(ƛ "n" ⇒ (ƛ "n" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ # "m" · # "s" · (# "n" · # "s" · # "z"))))) (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "m" ⌋ · ⌊ "s" ⌋ · (⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋)))))
· (ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)))
· (ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)))
· (ƛ "n" ⇒ `suc # "n") · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· `zero · `zero
⟶⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ· V-ƛ))) ⟩ ⟶⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ· V-ƛ))) ⟩
(ƛ "n" ⇒ (ƛ "n" ⇒
(ƛ "s" ⇒ (ƛ "s" ⇒
(ƛ "z" ⇒ (ƛ "z" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · # "s" · (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · ⌊ "s" ⌋ ·
(# "n" · # "s" · # "z")))) (⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋))))
· (ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)))
· (ƛ "n" ⇒ `suc # "n") · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· `zero · `zero
⟶⟨ ξ-·₁ (ξ-·₁ (β-ƛ· V-ƛ)) ⟩ ⟶⟨ ξ-·₁ (ξ-·₁ (β-ƛ· V-ƛ)) ⟩
(ƛ "s" ⇒ (ƛ "s" ⇒
(ƛ "z" ⇒ (ƛ "z" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · # "s" · (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · ⌊ "s" ⌋ ·
((ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · # "s" · # "z"))) ((ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · ⌊ "s" ⌋ · ⌊ "z" ⌋)))
· (ƛ "n" ⇒ `suc # "n") · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· `zero · `zero
⟶⟨ ξ-·₁ (β-ƛ· V-ƛ) ⟩ ⟶⟨ ξ-·₁ (β-ƛ· V-ƛ) ⟩
(ƛ "z" ⇒ (ƛ "z" ⇒
(ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "n" ⇒ `suc # "n") (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· ·
((ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "n" ⇒ `suc # "n") ((ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· # "z")) · ⌊ "z" ⌋))
· `zero · `zero
⟶⟨ β-ƛ· V-zero ⟩ ⟶⟨ β-ƛ· V-zero ⟩
(ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "n" ⇒ `suc # "n") (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· ·
((ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "n" ⇒ `suc # "n") ((ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· `zero) · `zero)
⟶⟨ ξ-·₁ (β-ƛ· V-ƛ) ⟩ ⟶⟨ ξ-·₁ (β-ƛ· V-ƛ) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · # "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ⌊ "z" ⌋)) ·
((ƛ "s" ⇒ (ƛ "z" ⇒ # "s" · (# "s" · # "z"))) · (ƛ "n" ⇒ `suc # "n") ((ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋))) · (ƛ "n" ⇒ `suc ⌊ "n" ⌋)
· `zero) · `zero)
⟶⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ· V-ƛ)) ⟩ ⟶⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ· V-ƛ)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · # "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ⌊ "z" ⌋)) ·
((ƛ "z" ⇒ (ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · # "z")) · ((ƛ "z" ⇒ (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ⌊ "z" ⌋)) ·
`zero) `zero)
⟶⟨ ξ-·₂ V-ƛ (β-ƛ· V-zero) ⟩ ⟶⟨ ξ-·₂ V-ƛ (β-ƛ· V-zero) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · # "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ⌊ "z" ⌋)) ·
((ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · `zero)) ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · `zero))
⟶⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ· V-zero)) ⟩ ⟶⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ· V-zero)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · # "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ⌊ "z" ⌋)) ·
((ƛ "n" ⇒ `suc # "n") · `suc `zero) ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · `suc `zero)
⟶⟨ ξ-·₂ V-ƛ (β-ƛ· (V-suc V-zero)) ⟩ ⟶⟨ ξ-·₂ V-ƛ (β-ƛ· (V-suc V-zero)) ⟩
(ƛ "z" ⇒ (ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · # "z")) · (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ⌊ "z" ⌋)) ·
`suc (`suc `zero) `suc (`suc `zero)
⟶⟨ β-ƛ· (V-suc (V-suc V-zero)) ⟩ ⟶⟨ β-ƛ· (V-suc (V-suc V-zero)) ⟩
(ƛ "n" ⇒ `suc # "n") · ((ƛ "n" ⇒ `suc # "n") · `suc (`suc `zero)) (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · ((ƛ "n" ⇒ `suc ⌊ "n" ⌋) · `suc (`suc `zero))
⟶⟨ ξ-·₂ V-ƛ (β-ƛ· (V-suc (V-suc V-zero))) ⟩ ⟶⟨ ξ-·₂ V-ƛ (β-ƛ· (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒ `suc # "n") · `suc (`suc (`suc `zero)) ⟶⟨ (ƛ "n" ⇒ `suc ⌊ "n" ⌋) · `suc (`suc (`suc `zero)) ⟶⟨
β-ƛ· (V-suc (V-suc (V-suc V-zero))) ⟩ β-ƛ· (V-suc (V-suc (V-suc V-zero))) ⟩
`suc (`suc (`suc (`suc `zero))) ∎) `suc (`suc (`suc (`suc `zero))) ∎)
(V-suc (V-suc (V-suc (V-suc V-zero)))) (V-suc (V-suc (V-suc (V-suc V-zero))))
@ -712,7 +713,7 @@ Suppose instead that we add a new term `foo` with the following
reduction rules: reduction rules:
------------------- (Foo₁) ------------------- (Foo₁)
(λ x ⇒ # x) ⟶ foo (λ x ⇒ ⌊ x ⌋) ⟶ foo
------------ (Foo₂) ------------ (Foo₂)
foo ⟶ true foo ⟶ true
@ -807,7 +808,7 @@ false, give a counterexample.
#### Exercise: 2 stars, optional (stlc_variation7) #### Exercise : 2 stars, optional (stlc_variation7)
Suppose we add the following new rule to the typing relation Suppose we add the following new rule to the typing relation
of the STLC: of the STLC: