From 7b4eb3baa5bcd187eb70fed154ba7a676c71f2ed Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Thu, 1 Oct 2026 18:07:04 +0800 Subject: [PATCH 1/6] fix formatting of exposition --- src/plfa/part3/Denotational.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 018327cd8..c01362c31 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -402,8 +402,8 @@ we'll name `v`. Then for the second application, `f` must map `v` to some value. Let's name it `w`. So the function's table must include two entries, both `u ↦ v` and `v ↦ w`. For each application of the table, we extract the appropriate entry from it -using the `sub` rule. In particular, we use the ⊑-conj-R1 and -⊑-conj-R2 to select `u ↦ v` and `v ↦ w`, respectively, from the table +using the `sub` rule. In particular, we use `the ⊑-conj-R1` and +`⊑-conj-R2` to select `u ↦ v` and `v ↦ w`, respectively, from the table `u ↦ v ⊔ v ↦ w`. So the meaning of twoᶜ is that it takes this table and parameter `u`, and it returns `w`. Indeed we derive this as follows. From 3c5f4e38d33b0a4f42028694630458be10184dae Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Thu, 1 Oct 2026 18:08:27 +0800 Subject: [PATCH 2/6] oops --- src/plfa/part3/Denotational.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index c01362c31..0d093ac44 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -402,7 +402,7 @@ we'll name `v`. Then for the second application, `f` must map `v` to some value. Let's name it `w`. So the function's table must include two entries, both `u ↦ v` and `v ↦ w`. For each application of the table, we extract the appropriate entry from it -using the `sub` rule. In particular, we use `the ⊑-conj-R1` and +using the `sub` rule. In particular, we use the `⊑-conj-R1` and `⊑-conj-R2` to select `u ↦ v` and `v ↦ w`, respectively, from the table `u ↦ v ⊔ v ↦ w`. So the meaning of twoᶜ is that it takes this table and parameter `u`, and it returns `w`. Indeed we derive this as From c4b71afdfea5614bb1cc9e40a5d452d88d56b9d8 Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Thu, 1 Oct 2026 18:09:56 +0800 Subject: [PATCH 3/6] one more --- src/plfa/part3/Denotational.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 0d093ac44..77a677e85 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -404,7 +404,7 @@ table must include two entries, both `u ↦ v` and `v ↦ w`. For each application of the table, we extract the appropriate entry from it using the `sub` rule. In particular, we use the `⊑-conj-R1` and `⊑-conj-R2` to select `u ↦ v` and `v ↦ w`, respectively, from the table -`u ↦ v ⊔ v ↦ w`. So the meaning of twoᶜ is that it takes this table +`u ↦ v ⊔ v ↦ w`. So the meaning of `twoᶜ` is that it takes this table and parameter `u`, and it returns `w`. Indeed we derive this as follows. From 91e9c8c12b7755c3620291f5379ec43b60886ec2 Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Fri, 2 Oct 2026 01:17:30 +0800 Subject: [PATCH 4/6] fix typo --- src/plfa/part3/Denotational.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 77a677e85..fe585aa26 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -563,7 +563,7 @@ Denotational equality is an equivalence relation. (λ z → proj₂ (eq1 γ v) (proj₂ (eq2 γ v) z)) ⟩ ``` -Two terms `M` and `N` are denotational equal when their denotations are +Two terms `M` and `N` are denotationally equal when their denotations are equal, that is, `ℰ M ≃ ℰ N`. The following submodule introduces equational reasoning for the `≃` From 8989f4feedd436a5abc57e3ec5cdadffe3100b1c Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Fri, 2 Oct 2026 16:44:02 +0800 Subject: [PATCH 5/6] fix typos --- src/plfa/part3/Denotational.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index fe585aa26..5133333e7 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -1093,7 +1093,7 @@ The crux of the proof is the case for `⊑-trans`. u₁ ⊑ u₂ By the induction hypothesis for `u₁ ⊑ u`, we know -that `v ↦ w factors u into u′`, for some value `u′`, +that `v ↦ w` factors `u` into `u′`, for some value `u′`, so we have `all-funs u′` and `u′ ⊆ u`. By the induction hypothesis for `u ⊑ u₂`, we know that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂` into `u₃`. From a63768d13a23a0faf75e318d097ea3023f438b4a Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Thu, 8 Oct 2026 18:11:33 +0800 Subject: [PATCH 6/6] fix typo --- src/plfa/part3/Compositional.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md index c8f559270..66f17f8c8 100644 --- a/src/plfa/part3/Compositional.lagda.md +++ b/src/plfa/part3/Compositional.lagda.md @@ -230,7 +230,7 @@ We proceed by induction on the semantics. * Suppose `γ ⊢ L ↓ v₁′ ↦ v₁`, `γ ⊢ M ↓ v₁′`, and `v₂ ⊑ ⊥`. We have `γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)` by rule `sub` because `v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁`. - * Suppose `γ ⊢ L ↓ v₁′′ ↦ v₁, γ ⊢ M ↓ v₁′′`, + * Suppose `γ ⊢ L ↓ v₁′′ ↦ v₁`, `γ ⊢ M ↓ v₁′′`, `γ ⊢ L ↓ v₁′ ↦ v₂`, and `γ ⊢ M ↓ v₁′`. This case is the most interesting. By two uses of the rule `⊔-intro` we have