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

doh! got Church and Scott mixed up, unfixing

Browse source
This commit is contained in:
Jeremy Siek 2020-03-29 16:51:25 -04:00
parent 6dc437bce7
commit 2486155f3f
1 changed files with 7 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -681,7 +681,7 @@ Here is the representation of naturals encoded with de Bruijn indexes:
`zero = ƛ ƛ (# 0) `zero = ƛ ƛ (# 0)
`suc_ : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★) `suc_ : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★)
`suc_ M = (ƛ ƛ ƛ (# 1 · (# 2 · # 1 · # 0))) · M `suc_ M = (ƛ ƛ ƛ (# 1 · # 2)) · M
case : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★) → (Γ , ★ ⊢ ★) → (Γ ⊢ ★) case : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★) → (Γ , ★ ⊢ ★) → (Γ ⊢ ★)
case L M N = L · (ƛ N) · M case L M N = L · (ƛ N) · M
@ -691,21 +691,17 @@ definitions. The successor branch expects an additional variable to
be in scope (as indicated by its type), so it is converted to an be in scope (as indicated by its type), so it is converted to an
ordinary term using lambda abstraction. ordinary term using lambda abstraction.
Applying successor to the zero indeed reduces to the Church numeral Applying successor to the zero indeed reduces to the Scott numeral
for one. for one.
``` ```
_ : eval (gas 100) (`suc_ {∅} `zero) ≡ _ : eval (gas 100) (`suc_ {∅} `zero) ≡
steps steps
((ƛ (ƛ (ƛ (` (S Z)) · ((` (S (S Z))) · (` (S Z)) · (` Z))))) · (ƛ (ƛ (` Z))) ((ƛ (ƛ (ƛ # 1 · # 2))) · (ƛ (ƛ # 0))
—→⟨ β ⟩ —→⟨ β ⟩
ƛ (ƛ (` (S Z)) · ((ƛ (ƛ (` Z))) · (` (S Z)) · (` Z))) ƛ (ƛ # 1 · (ƛ (ƛ # 0)))
—→⟨ ζ (ζ (ξ₂ (ξ₁ β))) ⟩ ∎)
ƛ (ƛ (` (S Z)) · ((ƛ (` Z)) · (` Z))) (done (ƛ (ƛ (′ (` (S Z)) · (ƛ (ƛ (′ (` Z))))))))
—→⟨ ζ (ζ (ξ₂ β)) ⟩
ƛ (ƛ (` (S Z)) · (` Z))
∎)
(done (ƛ (ƛ (′ (` (S Z)) · (′ (` Z))))))
_ = refl _ = refl
``` ```