changed the denot-church exercise

src/plfa/part3/Denotational.lagda.md

@@ -64,6 +64,7 @@ open import Data.Nat using (ℕ; zero; suc)
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum
+open import Data.Vec using (Vec; []; _∷_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; refl; sym; cong; cong₂; cong-app)
 open import Relation.Nullary using (¬_)
@@ -511,27 +512,53 @@ for your choice of `v`.
 #### 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`.
+represent paths. A path consists of `n` edges and `n + 1` vertices.
+We store the vertices in a vector of length `n + 1` in reverse
+order. The edges in the path map the ith vertex to the `i + 1` vertex.
+The following function `Dˢᵘᶜ` (for denotation of successor) constructs
+a table whose entries are all the edges in the path.
 
 ```
-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)
+Dˢᵘᶜ : (n : ℕ) → Vec Value (suc n) → Value
+Dˢᵘᶜ zero (a[0] ∷ []) = ⊥
+Dˢᵘᶜ (suc i) (a[i+1] ∷ a[i] ∷ ls) =  a[i] ↦ a[i+1]  ⊔  Dˢᵘᶜ i (a[i] ∷ ls)
 ```
 
-* A singleton path is of the form `f ↦ a ↦ a`.
+We use the following auxilliary function to obtain the last element of
+a non-empty vector. (This formulation is more convenient for our
+purposes than the one in the Agda standard library.)
 
-* If there is a path from `a` to `b` and
-  an edge from `b` to `c` in the graph of `f`,
-  then there is a path from `a` to `c`.
+```
+vec-last : ∀{n : ℕ} → Vec Value (suc n) → Value
+vec-last {0} (a ∷ []) = a
+vec-last {suc n} (a ∷ b ∷ ls) = vec-last (b ∷ ls)
+```
 
-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`.
+The function `Dᶜ` computes the denotation of the nth Church numeral
+for a given path.
+
+```
+Dᶜ : (n : ℕ) → Vec Value (suc n) → Value
+Dᶜ zero (a[0] ∷ []) = ⊥ ↦ a[0] ↦ a[0]
+Dᶜ (suc n) (a[n+1] ∷ a[n] ∷ ls) =
+  (Dˢᵘᶜ (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]
+```
+
+* The Church numeral for 0 ignores its first argument and returns
+  its second argument, so for the singleton path consisting of
+  just `a[0]`, its denotation is
+
+        ⊥ ↦ a[0] ↦ a[0]
+
+* The Church numeral for `suc n` takes two arguments:
+  a successor function whose denotation is given by `Dˢᵘᶜ`,
+  and the start of the path (last of the vector).
+  It returns the `n + 1` vertex in the path.
+  
+        (Dˢᵘᶜ (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]
+
+The exercise is to prove that for any path `ls`, the meaning of the
+Church numeral `n` is `Dᶜ n ls`.
 
 To fascilitate talking about arbitrary Church numerals, the following
 `church` function builds the term for the nth Church numeral,
@@ -548,10 +575,8 @@ church n = ƛ ƛ apply-n n
 
 Prove the following theorem.
 
-    denot-church : ∀{n v}
-       → Path n v
-         -----------------
-       → `∅ ⊢ church n ↓ v
+    denot-church : ∀{n : ℕ}{ls : Vec Value (suc n)}
+       → `∅ ⊢ church n ↓ Dᶜ n ls
 
 ```
 -- Your code goes here