From d1f628ceae435e47158c799348e54f5582d0be47 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Tue, 31 Mar 2020 16:07:45 -0400 Subject: [PATCH 1/7] changed the denot-church exercise --- src/plfa/part3/Denotational.lagda.md | 63 +++++++++++++++++++--------- 1 file changed, 44 insertions(+), 19 deletions(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index fe4ddaf7..202652b7 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/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 From 3ab180ad8d4719b9c5e2039bf680b0a4c67879e4 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Wed, 1 Apr 2020 09:30:52 -0400 Subject: [PATCH 2/7] tweak --- src/plfa/part3/Denotational.lagda.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 202652b7..7cd28762 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -515,13 +515,13 @@ 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ˢᵘᶜ` (for denotation of successor) constructs +The following function `D^suc` (for denotation of successor) constructs a table whose entries are all the edges in the path. ``` -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) +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 @@ -541,7 +541,7 @@ 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] + (D^suc (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 @@ -551,11 +551,11 @@ Dᶜ (suc n) (a[n+1] ∷ a[n] ∷ ls) = ⊥ ↦ a[0] ↦ a[0] * The Church numeral for `suc n` takes two arguments: - a successor function whose denotation is given by `Dˢᵘᶜ`, + 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 n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1] + (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`. From 2dc431121e91bb3bc544ab8c65d07835ce47b353 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Tue, 7 Apr 2020 08:19:03 -0400 Subject: [PATCH 3/7] simplified D^c --- src/plfa/part3/Denotational.lagda.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 7cd28762..6d3f1185 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -539,9 +539,7 @@ 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 (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1] +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 From 2afe5706a1b8509f68c33ddd67a98b95f6940afb Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Thu, 9 Apr 2020 09:15:25 -0400 Subject: [PATCH 4/7] some edits --- src/plfa/part3/Adequacy.lagda.md | 82 ++++++++++++++++++-------------- 1 file changed, 47 insertions(+), 35 deletions(-) diff --git a/src/plfa/part3/Adequacy.lagda.md b/src/plfa/part3/Adequacy.lagda.md index 21300022..26c6838b 100644 --- a/src/plfa/part3/Adequacy.lagda.md +++ b/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,23 +30,21 @@ then `M` reduces to a lambda abstraction. ℰ M ≃ ℰ (ƛ N) implies M —↠ ƛ N' for some N' -Recall that `ℰ M ≃ ℰ (ƛ N)` is equivalent to saying that -`γ ⊢ M ↓ (v ↦ w)` for some `v` and `w`. We will show that -`γ ⊢ M ↓ (v ↦ w)` implies reduction a lambda abstraction. - -It is well known that a term can reduce to a lambda abstraction using -full β reduction if and only if it can reduce to a lambda abstraction -using the call-by-name reduction strategy. So we shall prove that -`γ ⊢ M ↓ (v ↦ w)` implies that `M` halts under call-by-name evaluation, -which we define with a big-step semantics written `γ' ⊢ M ⇓ c`, where -`c` is a closure (a term paired with an environment) and `γ'` is an -environment that maps variables to closures - -So we will show that `γ ⊢ M ↓ (v ↦ w)` implies `γ' ⊢ M ⇓ c`, -provided `γ` and `γ'` are appropriate related. The proof will -be an induction on the derivation of `γ ⊢ M ↓ v`, and to -strengthen the induction hypothesis, we will relate semantic values to -closures using a _logical relation_ `𝕍`. +Recall that `ℰ M ≃ ℰ (ƛ N)` is equivalent to saying that `γ ⊢ M ↓ (v ↦ +w)` for some `v` and `w`. We will show that `γ ⊢ M ↓ (v ↦ w)` implies +multi-step reduction a lambda abstraction. The recursive structure of +the derivations for `γ ⊢ M ↓ (v ↦ w)` are completely different from +the structure of multi-step reductions, so a direct proof would be +challenging. However, The structure of `γ ⊢ M ↓ (v ↦ w)` closer to +that of the [BigStep](../part2/BigStep.lagda.md) call-by-name +evaluation. Further, we already proved that big-step evaluation +implies multi-step reduction to a lambda (`cbn→reduce`). So we shall +prove that `γ ⊢ M ↓ (v ↦ w)` implies that `γ' ⊢ M ⇓ c`, where `c` is a +closure (a term paired with an environment), `γ'` is an environment +that maps variables to closures, and `γ` and `γ'` are appropriate +related. The proof will be an induction on the derivation of +`γ ⊢ M ↓ v`, and to strengthen the induction hypothesis, we will relate +semantic values to closures using a _logical relation_ `𝕍`. The rest of this chapter is organized as follows. @@ -55,9 +53,6 @@ The rest of this chapter is organized as follows. 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 `𝔾`. @@ -265,7 +260,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 +576,14 @@ kth-x{γ' = γ'}{x = x} with γ' x ## Proof of denotational adequacy -The adequacy property is a corollary of the main lemma. -We have `∅ ⊢ ƛ N ↓ ⊥ ↦ ⊥`, so `ℰ M ≃ ℰ (ƛ N)` -gives us `∅ ⊢ M ↓ ⊥ ↦ ⊥`. Then the main lemma gives us -`∅ ⊢ M ⇓ clos (ƛ N′) γ` for some `N′` and `γ`. +From the main lemma we can directly show that `ℰ M ≃ ℰ (ƛ N)` implies +that `M` big-steps to a lambda, i.e., `∅ ⊢ M ⇓ clos (ƛ N′) γ`. ``` -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 +592,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 -we established the forward direction: that if call-by-name produces a -result, then the program beta reduces to a lambda abstraction. We now -prove the backward direction of the if-and-only-if, leveraging our -results about the denotational semantics. +evaluation is equivalent to beta reduction. In chapter +[BigStep](../part2/BigStep.lagda.md) we established the forward +direction: that if call-by-name produces a result, then the program +beta reduces to a lambda abstraction (`cbn→reduce`). We now prove the backward +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 From 433587bc6125a7af6518b562ea0e2331c30b29fa Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Thu, 9 Apr 2020 09:18:30 -0400 Subject: [PATCH 5/7] more edits --- src/plfa/part3/ContextualEquivalence.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/plfa/part3/ContextualEquivalence.lagda.md b/src/plfa/part3/ContextualEquivalence.lagda.md index 748c2b98..c1b0d9f7 100644 --- a/src/plfa/part3/ContextualEquivalence.lagda.md +++ b/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](../Adequacy.lagda.md) to deduce ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ). From 09a91451b284a6f2a3a9f5d39818d027d5797da7 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Thu, 9 Apr 2020 09:27:24 -0400 Subject: [PATCH 6/7] fix links --- src/plfa/part3/Adequacy.lagda.md | 9 ++++++--- src/plfa/part3/ContextualEquivalence.lagda.md | 2 +- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/plfa/part3/Adequacy.lagda.md b/src/plfa/part3/Adequacy.lagda.md index 26c6838b..b764b985 100644 --- a/src/plfa/part3/Adequacy.lagda.md +++ b/src/plfa/part3/Adequacy.lagda.md @@ -36,7 +36,7 @@ multi-step reduction a lambda abstraction. The recursive structure of the derivations for `γ ⊢ M ↓ (v ↦ w)` are completely different from the structure of multi-step reductions, so a direct proof would be challenging. However, The structure of `γ ⊢ M ↓ (v ↦ w)` closer to -that of the [BigStep](../part2/BigStep.lagda.md) call-by-name +that of [BigStep]({{ site.baseurl }}/BigStep/) call-by-name evaluation. Further, we already proved that big-step evaluation implies multi-step reduction to a lambda (`cbn→reduce`). So we shall prove that `γ ⊢ M ↓ (v ↦ w)` implies that `γ' ⊢ M ⇓ c`, where `c` is a @@ -48,13 +48,16 @@ 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 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 γ')`. @@ -616,7 +619,7 @@ adequacy{M}{N} eq As promised, we return to the question of whether call-by-name evaluation is equivalent to beta reduction. In chapter -[BigStep](../part2/BigStep.lagda.md) we established the forward +[BigStep]({{ site.baseurl }}/BigStep/) we established the forward direction: that if call-by-name produces a result, then the program beta reduces to a lambda abstraction (`cbn→reduce`). We now prove the backward direction of the if-and-only-if, leveraging our results about the diff --git a/src/plfa/part3/ContextualEquivalence.lagda.md b/src/plfa/part3/ContextualEquivalence.lagda.md index c1b0d9f7..91496570 100644 --- a/src/plfa/part3/ContextualEquivalence.lagda.md +++ b/src/plfa/part3/ContextualEquivalence.lagda.md @@ -94,7 +94,7 @@ Putting these two facts together gives us ℰ (plug C N) ≃ ℰ (ƛN′). -We then apply `↓→⇓` from Chapter [Adequacy](../Adequacy.lagda.md) to deduce +We then apply `↓→⇓` from Chapter [Adequacy]({{ site.baseurl }}/Adequacy/) to deduce ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ). From 963fc985b0668224e3b681a1f8604b7e63d8a152 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Fri, 10 Apr 2020 13:55:52 -0400 Subject: [PATCH 7/7] moved exercise to come later --- src/plfa/part3/Denotational.lagda.md | 141 ++++++++++++++------------- 1 file changed, 71 insertions(+), 70 deletions(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 6d3f1185..bb05e64f 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -509,76 +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. 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 -``` ## Denotations and denotational equality @@ -881,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