merge

src/plfa/part3/Adequacy.lagda.md

@@ -22,7 +22,7 @@ Such a property would tell us that having a denotation implies either
 reduction to normal form or divergence. This is indeed true, but we
 can prove a much stronger property! In fact, having a denotation that
 is a function value (not `⊥`) implies reduction to a lambda
-abstraction (no divergence).
+abstraction.
 
 This stronger property, reformulated a bit, is known as _adequacy_.
 That is, if a term `M` is denotationally equal to a lambda abstraction,
@@ -30,36 +30,34 @@ then `M` reduces to a lambda abstraction.
 
     ℰ M ≃ ℰ (ƛ N)  implies M —↠ ƛ N' for some N'
 
-Recall that `ℰ M ≃ ℰ (ƛ N)` is equivalent to saying that
+Recall that `ℰ M ≃ ℰ (ƛ N)` is equivalent to saying that `γ ⊢ M ↓ (v ↦
-`γ ⊢ M ↓ (v ↦ w)` for some `v` and `w`. We will show that
+w)` for some `v` and `w`. We will show that `γ ⊢ M ↓ (v ↦ w)` implies
-`γ ⊢ M ↓ (v ↦ w)` implies reduction a lambda abstraction.
+multi-step reduction a lambda abstraction.  The recursive structure of
-
+the derivations for `γ ⊢ M ↓ (v ↦ w)` are completely different from
-It is well known that a term can reduce to a lambda abstraction using
+the structure of multi-step reductions, so a direct proof would be
-full β reduction if and only if it can reduce to a lambda abstraction
+challenging. However, The structure of `γ ⊢ M ↓ (v ↦ w)` closer to
-using the call-by-name reduction strategy. So we shall prove that
+that of [BigStep]({{ site.baseurl }}/BigStep/) call-by-name
-`γ ⊢ M ↓ (v ↦ w)` implies that `M` halts under call-by-name evaluation,
+evaluation. Further, we already proved that big-step evaluation
-which we define with a big-step semantics written `γ' ⊢ M ⇓ c`, where
+implies multi-step reduction to a lambda (`cbn→reduce`). So we shall
-`c` is a closure (a term paired with an environment) and `γ'` is an
+prove that `γ ⊢ M ↓ (v ↦ w)` implies that `γ' ⊢ M ⇓ c`, where `c` is a
-environment that maps variables to closures
+closure (a term paired with an environment), `γ'` is an environment
-
+that maps variables to closures, and `γ` and `γ'` are appropriate
-So we will show that `γ ⊢ M ↓ (v ↦ w)` implies `γ' ⊢ M ⇓ c`,
+related.  The proof will be an induction on the derivation of
-provided `γ` and `γ'` are appropriate related.  The proof will
+`γ ⊢ M ↓ v`, and to strengthen the induction hypothesis, we will relate
-be an induction on the derivation of `γ ⊢ M ↓ v`, and to
+semantic values to closures using a _logical relation_ `𝕍`.
-strengthen the induction hypothesis, we will relate semantic values to
-closures using a _logical relation_ `𝕍`.
 
 The rest of this chapter is organized as follows.
 
-* We loosen the requirement that `M` result in a function value and
+* To make the `𝕍` relation down-closed with respect to `⊑`,
+  we must loosen the requirement that `M` result in a function value and
   instead require that `M` result in a value that is greater than or
   equal to a function value. We establish several properties about
   being ``greater than a function''.
 
-* We define the call-by-name big-step semantics of the lambda calculus
-  and prove that it is deterministic.
-
 * We define the logical relation `𝕍` that relates values and closures,
   and extend it to a relation on terms `𝔼` and environments `𝔾`.
+  We prove several lemmas that culminate in the property that
+  if `𝕍 v c` and `v′ ⊑ v`, then `𝕍 v′ c`.
 
 * We prove the main lemma,
   that if `𝔾 γ γ'` and `γ ⊢ M ↓ v`, then `𝔼 v (clos M γ')`.
@@ -265,7 +263,6 @@ by `𝔼`.
 𝔾-ext {Γ} {γ} {γ'} g e {S x} = g
 ```
 
-
 We need a few properties of the `𝕍` and `𝔼` relations.  The first is that
 a closure in the `𝕍` relation must be in weak-head normal form.  We
 define WHNF has follows.
@@ -582,16 +579,14 @@ kth-x{γ' = γ'}{x = x} with γ' x
 
 ## Proof of denotational adequacy
 
-The adequacy property is a corollary of the main lemma.
+From the main lemma we can directly show that `ℰ M ≃ ℰ (ƛ N)` implies
-We have `∅ ⊢ ƛ N ↓ ⊥ ↦ ⊥`, so `ℰ M ≃ ℰ (ƛ N)`
+that `M` big-steps to a lambda, i.e., `∅ ⊢ M ⇓ clos (ƛ N′) γ`.
-gives us `∅ ⊢ M ↓ ⊥ ↦ ⊥`. Then the main lemma gives us
-`∅ ⊢ M ⇓ clos (ƛ N′) γ` for some `N′` and `γ`.
 
 ```
-adequacy : ∀{M : ∅ ⊢ ★}{N : ∅ , ★ ⊢ ★}  →  ℰ M ≃ ℰ (ƛ N)
+↓→⇓ : ∀{M : ∅ ⊢ ★}{N : ∅ , ★ ⊢ ★}  →  ℰ M ≃ ℰ (ƛ N)
          →  Σ[ Γ ∈ Context ] Σ[ N′ ∈ (Γ , ★ ⊢ ★) ] Σ[ γ ∈ ClosEnv Γ ]
             ∅' ⊢ M ⇓ clos (ƛ N′) γ
-adequacy{M}{N} eq
+↓→⇓{M}{N} eq
     with ↓→𝔼 𝔾-∅ ((proj₂ (eq `∅ (⊥ ↦ ⊥))) (↦-intro ⊥-intro))
                  ⟨ ⊥ , ⟨ ⊥ , ⊑-refl ⟩ ⟩
 ... | ⟨ clos {Γ} M′ γ , ⟨ M⇓c , Vc ⟩ ⟩
@@ -600,26 +595,46 @@ adequacy{M}{N} eq
     ⟨ Γ , ⟨ N′ , ⟨ γ , M⇓c ⟩  ⟩ ⟩
 ```
 
+The proof goes as follows. We derive `∅ ⊢ ƛ N ↓ ⊥ ↦ ⊥` and
+then `ℰ M ≃ ℰ (ƛ N)` gives us `∅ ⊢ M ↓ ⊥ ↦ ⊥`. We conclude
+by applying the main lemma to obtain `∅ ⊢ M ⇓ clos (ƛ N′) γ`
+for some `N′` and `γ`.
+
+Now to prove the adequacy property. We apply the above
+lemma to obtain `∅ ⊢ M ⇓ clos (ƛ N′) γ` and then
+apply `cbn→reduce` to conclude.
+
+```
+adequacy : ∀{M : ∅ ⊢ ★}{N : ∅ , ★ ⊢ ★}
+   →  ℰ M ≃ ℰ (ƛ N)
+   → Σ[ N′ ∈ (∅ , ★ ⊢ ★) ]
+     (M —↠ ƛ N′)
+adequacy{M}{N} eq
+    with ↓→⇓ eq
+... | ⟨ Γ , ⟨ N′ , ⟨ γ , M⇓ ⟩ ⟩ ⟩ =
+    cbn→reduce M⇓
+```
 
 ## Call-by-name is equivalent to beta reduction
 
 As promised, we return to the question of whether call-by-name
-evaluation is equivalent to beta reduction. In the chapter CallByName
+evaluation is equivalent to beta reduction. In chapter
-we established the forward direction: that if call-by-name produces a
+[BigStep]({{ site.baseurl }}/BigStep/) we established the forward
-result, then the program beta reduces to a lambda abstraction.  We now
+direction: that if call-by-name produces a result, then the program
-prove the backward direction of the if-and-only-if, leveraging our
+beta reduces to a lambda abstraction (`cbn→reduce`).  We now prove the backward
-results about the denotational semantics.
+direction of the if-and-only-if, leveraging our results about the
+denotational semantics.
 
 ```
 reduce→cbn : ∀ {M : ∅ ⊢ ★} {N : ∅ , ★ ⊢ ★}
            → M —↠ ƛ N
            → Σ[ Δ ∈ Context ] Σ[ N′ ∈ Δ , ★ ⊢ ★ ] Σ[ δ ∈ ClosEnv Δ ]
              ∅' ⊢ M ⇓ clos (ƛ N′) δ
-reduce→cbn M—↠ƛN = adequacy (soundness M—↠ƛN)
+reduce→cbn M—↠ƛN = ↓→⇓ (soundness M—↠ƛN)
 ```
 
 Suppose `M —↠ ƛ N`. Soundness of the denotational semantics gives us
-`ℰ M ≃ ℰ (ƛ N)`. Then by adequacy we conclude that
+`ℰ M ≃ ℰ (ƛ N)`. Then by `↓→⇓` we conclude that
 `∅' ⊢ M ⇓ clos (ƛ N′) δ` for some `N′` and `δ`.
 
 Putting the two directions of the if-and-only-if together, we

src/plfa/part3/ContextualEquivalence.lagda.md

@@ -20,7 +20,7 @@ open import plfa.part2.BigStep using (_⊢_⇓_; cbn→reduce)
 open import plfa.part3.Denotational using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_)
 open import plfa.part3.Compositional using (Ctx; plug; compositionality)
 open import plfa.part3.Soundness using (soundness)
-open import plfa.part3.Adequacy using (adequacy)
+open import plfa.part3.Adequacy using (↓→⇓)
 ```
 
 ## Contextual Equivalence
@@ -78,7 +78,7 @@ denot-equal-terminates {Γ}{M}{N}{C} ℰM≃ℰN ⟨ N′ , CM—↠ƛN′ ⟩ =
   let ℰCM≃ℰƛN′ = soundness CM—↠ƛN′ in
   let ℰCM≃ℰCN = compositionality{Γ = Γ}{Δ = ∅}{C = C} ℰM≃ℰN in
   let ℰCN≃ℰƛN′ = ≃-trans (≃-sym ℰCM≃ℰCN) ℰCM≃ℰƛN′ in
-    cbn→reduce (proj₂ (proj₂ (proj₂ (adequacy ℰCN≃ℰƛN′))))
+    cbn→reduce (proj₂ (proj₂ (proj₂ (↓→⇓ ℰCN≃ℰƛN′))))
 ```
 
 The proof is direct. Because `plug C —↠ plug C (ƛN′)`,
@@ -94,7 +94,7 @@ Putting these two facts together gives us
 
     ℰ (plug C N) ≃ ℰ (ƛN′).
 
-We then apply adequacy to deduce
+We then apply `↓→⇓` from Chapter [Adequacy]({{ site.baseurl }}/Adequacy/) to deduce
 
     ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ).
 

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 (¬_)
@@ -508,54 +509,6 @@ 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 the 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
 
@@ -858,6 +811,77 @@ up-env d lt = ⊑-env d (ext-le lt)
   ext-le lt (S n) = ⊑-refl
 ```
 
+#### Exercise `denot-church` (recommended)
+
+Church numerals are more general than natural numbers in that they
+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^suc` (for denotation of successor) constructs
+a table whose entries are all the edges in the path.
+
+```
+D^suc : (n : ℕ) → Vec Value (suc n) → Value
+D^suc zero (a[0] ∷ []) = ⊥
+D^suc (suc i) (a[i+1] ∷ a[i] ∷ ls) =  a[i] ↦ a[i+1]  ⊔  D^suc i (a[i] ∷ ls)
+```
+
+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.)
+
+```
+vec-last : ∀{n : ℕ} → Vec Value (suc n) → Value
+vec-last {0} (a ∷ []) = a
+vec-last {suc n} (a ∷ b ∷ ls) = vec-last (b ∷ ls)
+```
+
+The function `Dᶜ` computes the denotation of the nth Church numeral
+for a given path.
+
+```
+Dᶜ : (n : ℕ) → Vec Value (suc n) → Value
+Dᶜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n]
+```
+
+* 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^suc`,
+  and the start of the path (last of the vector).
+  It returns the `n + 1` vertex in the path.
+  
+        (D^suc (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,
+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 : ℕ}{ls : Vec Value (suc n)}
+       → `∅ ⊢ church n ↓ Dᶜ n ls
+
+```
+-- Your code goes here
+```
+
 
 ## Inversion of the less-than relation for functions