From e51e255d8d30f7da6b029c99c1ccff00e0fdd227 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Fri, 27 Mar 2020 11:35:26 -0400 Subject: [PATCH] fixed suc_ --- src/plfa/part2/Untyped.lagda.md | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index 88d7ecc9..be787cf2 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -681,7 +681,7 @@ Here is the representation of naturals encoded with de Bruijn indexes: `zero = ƛ ƛ (# 0) `suc_ : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★) -`suc_ M = (ƛ ƛ ƛ (# 1 · # 2)) · M +`suc_ M = (ƛ ƛ ƛ (# 1 · (# 2 · # 1 · # 0))) · M case : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★) → (Γ , ★ ⊢ ★) → (Γ ⊢ ★) case L M N = L · (ƛ N) · M @@ -691,6 +691,24 @@ definitions. The successor branch expects an additional variable to be in scope (as indicated by its type), so it is converted to an ordinary term using lambda abstraction. +Applying successor to the zero indeed reduces to the Church numeral +for one. + +``` +_ : eval (gas 100) (`suc_ {∅} `zero) ≡ + steps + ((ƛ (ƛ (ƛ (` (S Z)) · ((` (S (S Z))) · (` (S Z)) · (` Z))))) · (ƛ (ƛ (` Z))) + —→⟨ β ⟩ + ƛ (ƛ (` (S Z)) · ((ƛ (ƛ (` Z))) · (` (S Z)) · (` Z))) + —→⟨ ζ (ζ (ξ₂ (ξ₁ β))) ⟩ + ƛ (ƛ (` (S Z)) · ((ƛ (` Z)) · (` Z))) + —→⟨ ζ (ζ (ξ₂ β)) ⟩ + ƛ (ƛ (` (S Z)) · (` Z)) + ∎) + (done (ƛ (ƛ (′ (` (S Z)) · (′ (` Z)))))) +_ = refl +``` + We can also define fixpoint. Using named terms, we define: μ f = (ƛ x ⇒ f · (x · x)) · (ƛ x ⇒ f · (x · x)) @@ -729,6 +747,7 @@ 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. + #### Exercise `plus-eval` (practice) Use the evaluator to confirm that `plus · two · two` and `four`