merge

src/plfa/part2/Untyped.lagda.md

@@ -675,7 +675,7 @@ the predecessor of the current argument) and one corresponding to the
 zero branch of the case.  (The cases could be in either order.
 We put the successor case first to ease comparison with Church numerals.)
 
-Here is the representation of naturals encoded with de Bruijn indexes:
+Here is the Scott representation of naturals encoded with de Bruijn indexes:
 ```
 `zero : ∀ {Γ} → (Γ ⊢ ★)
 `zero = ƛ ƛ (# 0)
@@ -691,6 +691,20 @@ 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 Scott numeral
+for one.
+
+```
+_ : eval (gas 100) (`suc_ {∅} `zero) ≡
+    steps
+        ((ƛ (ƛ (ƛ # 1 · # 2))) · (ƛ (ƛ # 0))
+    —→⟨ β ⟩
+         ƛ (ƛ # 1 · (ƛ (ƛ # 0)))
+    ∎)
+    (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 +743,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`

src/plfa/part3/Denotational.lagda.md

@@ -60,6 +60,7 @@ open import Relation.Binary using (Setoid)
 ```
 open import Agda.Primitive using (lzero; lsuc)
 open import Data.Empty using (⊥-elim)
+open import Data.Nat using (ℕ; zero; suc)
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum
@@ -507,6 +508,55 @@ for your choice of `v`.
 -- Your code goes here
 ```
 
+#### Exercise `denot-church` (recommended)
+
+Church numerals are more general than natural numbers in that they
+represent paths in a graph. The following `Path` predicate specifies
+when a value of the form `f ↦ a ↦ b` represents a path from the
+starting point `a` to the end point `b` in the graph of the function `f`.
+
+```
+data Path : (n : ℕ) → Value → Set where
+  singleton : ∀{f a} → Path 0 (f ↦ a ↦ a)
+  edge : ∀{n f a b c}
+     → Path n (f ↦ a ↦ b)
+     → b ↦ c ⊑ f
+     → Path (suc n) (f ↦ a ↦ c)
+```
+
+* A singleton path is of the form `f ↦ a ↦ a`.
+
+* If there is a path from `a` to `b` and
+  an edge from `b` to `c` in graph of `f`,
+  then there is a path from `a` to `c`.
+
+This exercise is to prove that if `f ↦ a ↦ b` is a path of length `n`,
+then `f ↦ a ↦ b` is a meaning of the Church numeral `n`.
+
+To fascilitate talking about arbitrary Church numerals, the following
+`church` function builds the term for the nth Church numeral,
+using the auxilliary function `apply-n`.
+
+```
+apply-n : (n : ℕ) → ∅ , ★ , ★ ⊢ ★
+apply-n zero = # 0
+apply-n (suc n) = # 1 · apply-n n
+
+church : (n : ℕ) → ∅ ⊢ ★
+church n = ƛ ƛ apply-n n 
+```
+
+Prove the following theorem.
+
+    denot-church : ∀{n v}
+       → Path n v
+         -----------------
+       → `∅ ⊢ church n ↓ v
+
+```
+-- Your code goes here
+```
+
 ## Denotations and denotational equality
 
 Next we define a notion of denotational equality based on the above