From fe1b959e328fe49e0927a73b942e613f4d637ecb Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Thu, 15 Oct 2026 18:12:53 +0800 Subject: [PATCH 1/3] fix typos --- src/plfa/part3/Soundness.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/plfa/part3/Soundness.lagda.md b/src/plfa/part3/Soundness.lagda.md index d9512a41a..db8affe95 100644 --- a/src/plfa/part3/Soundness.lagda.md +++ b/src/plfa/part3/Soundness.lagda.md @@ -280,7 +280,7 @@ We cannot prove this lemma by induction on the derivation of `δ (ρ x) ⊑ γ x`, so we conclude by the `var` rule. * If it is a lambda abstraction `ƛ N`, we have - rename `ρ (ƛ N) = ƛ (rename (ext ρ) N)`. + `rename ρ (ƛ N) = ƛ (rename (ext ρ) N)`. We proceed by cases on `δ ⊢ ƛ (rename (ext ρ) N) ↓ v`. * Rule `↦-intro`: To satisfy the premise of the induction @@ -515,11 +515,11 @@ subst-reflect (sub d lt) eq by the `subst-⊔` lemma. * Case `↦-intro`: We have `subst σ M ≡ ƛ L′`. We proceed by cases on `M`. - * Case `M ≡ x`: We apply the `subst-reflect-var` lemma. + * Case `` M ≡ ` x ``: We apply the `subst-reflect-var` lemma. * Case `M ≡ ƛ M′`: By the induction hypothesis, we have `(δ′ , v′) ⊢ M′ ↓ v₂` and `(δ , v₁) ⊢ exts σ ↓ (δ′ , v′)`. - From the later we have `(δ , v₁) ⊢ # 0 ↓ v′`. + From the latter we have `(δ , v₁) ⊢ # 0 ↓ v′`. By the lemma `var-inv` we have `v′ ⊑ v₁`, so by the `up-env` lemma we have `(δ′ , v₁) ⊢ M′ ↓ v₂` and therefore `δ′ ⊢ ƛ M′ ↓ v₁ → v₂`. We also need to show that `δ ⊢ σ ↓ δ′`. Fix `k`. We have From 64a293fd19914d9ac9a07a8c28e7b9adb1a0db2d Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Fri, 16 Oct 2026 20:04:17 +0800 Subject: [PATCH 2/3] fix typos --- src/plfa/part3/Adequacy.lagda.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/plfa/part3/Adequacy.lagda.md b/src/plfa/part3/Adequacy.lagda.md index 7e0abd09a..c72a02226 100644 --- a/src/plfa/part3/Adequacy.lagda.md +++ b/src/plfa/part3/Adequacy.lagda.md @@ -38,7 +38,7 @@ 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 +that maps variables to closures, and `γ` and `γ'` are appropriately 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_ `𝕍`. @@ -49,7 +49,7 @@ The rest of this chapter is organized as follows. 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''. + 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 `𝔾`. @@ -191,7 +191,7 @@ above-fun? (u ⊔ u') Next we relate semantic values to closures. The relation `𝕍` is for closures whose term is a lambda abstraction, i.e., in weak-head normal -form (WHNF). The relation 𝔼 is for any closure. Roughly speaking, +form (WHNF). The relation `𝔼` is for any closure. Roughly speaking, `𝔼 v c` will hold if, when `v` is greater than a function value, `c` evaluates to a closure `c'` in WHNF and `𝕍 v c'`. Regarding `𝕍 v c`, it will hold when `c` is in WHNF, and if `v` is a function, the body of `c` evaluates @@ -222,8 +222,8 @@ describe below. * If the value is `⊥`, then the result is true (`⊤`). -* If the value is a join (u ⊔ v), then the result is the pair - (conjunction) of 𝕍 is true for both u and v. +* If the value is a join (`u ⊔ v`), then the result is the pair + (conjunction) of `𝕍` being true for both `u` and `v`. * The important case is for a function value `v ↦ w` and closure `clos (ƛ N) γ`. Given any closure `c` such that `𝔼 v c`, if `w` is @@ -521,26 +521,26 @@ kth-x{γ' = γ'}{x = x} with γ' x * Case `var`. Looking up `x` in `γ'` yields some closure, `clos M' δ`, and from `𝔾 γ γ'` we have `𝔼 (γ x) (clos M' δ)`. With the premise `above-fun (γ x)`, we obtain a closure `c` such that `δ ⊢ M' ⇓ c` - and `𝕍 (γ x) c`. To conclude `γ' ⊢ x ⇓ c` via `⇓-var`, we + and `𝕍 (γ x) c`. To conclude ``γ' ⊢ ` x ⇓ c`` via `⇓-var`, we need `γ' x ≡ clos M' δ`, which is obvious, but it requires some Agda shananigans via the `kth-x` lemma to get our hands on it. * Case `↦-elim`. We have `γ ⊢ L · M ↓ v`. The induction hypothesis for `γ ⊢ L ↓ v₁ ↦ v` - gives us `γ' ⊢ L ⇓ clos L' δ` and `𝕍 v (clos L' δ)`. + gives us `γ' ⊢ L ⇓ clos L' δ` and `𝕍 (v₁ ↦ v) (clos L' δ)`. Of course, `L' ≡ ƛ N` for some `N`. By the induction hypothesis for `γ ⊢ M ↓ v₁`, we have `𝔼 v₁ (clos M γ')`. - Together with the premise `above-fun v` and `𝕍 v (clos L' δ)`, - we obtain a closure `c'` such that `δ ⊢ N ⇓ c'` and `𝕍 v c'`. + Together with the premise `above-fun v` and `𝕍 (v₁ ↦ v) (clos L' δ)`, + we obtain a closure `c'` such that `(δ ,' clos M γ') ⊢ N ⇓ c'` and `𝕍 v c'`. We conclude that `γ' ⊢ L · M ⇓ c'` by rule `⇓-app`. * Case `↦-intro`. We have `γ ⊢ ƛ N ↓ v ↦ w`. - We immediately have `γ' ⊢ ƛ M ⇓ clos (ƛ M) γ'` by rule `⇓-lam`. + We immediately have `γ' ⊢ ƛ N ⇓ clos (ƛ N) γ'` by rule `⇓-lam`. But we also need to prove `𝕍 (v ↦ w) (clos (ƛ N) γ')`. Let `c` by an arbitrary closure such that `𝔼 v c`. - Suppose `v'` is greater than a function value. - We need to show that `γ' , c ⊢ N ⇓ c'` and `𝕍 v' c'` for some `c'`. + Suppose `w` is greater than a function value. + We need to show that `γ' , c ⊢ N ⇓ c'` and `𝕍 w c'` for some `c'`. We prove this by the induction hypothesis for `γ , v ⊢ N ↓ v'` but we must first show that `𝔾 (γ , v) (γ' , c)`. We prove that by the lemma `𝔾-ext`, using facts `𝔾 γ γ'` and `𝔼 v c`. From 4d306322357fce4fbb10647c0ecaa93997cfcdab Mon Sep 17 00:00:00 2001 From: Hillosanation <88579655+Hillosanation@users.noreply.github.com> Date: Fri, 16 Oct 2026 20:47:42 +0800 Subject: [PATCH 3/3] fix typos --- src/plfa/part3/ContextualEquivalence.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part3/ContextualEquivalence.lagda.md b/src/plfa/part3/ContextualEquivalence.lagda.md index 787110dff..5312ee770 100644 --- a/src/plfa/part3/ContextualEquivalence.lagda.md +++ b/src/plfa/part3/ContextualEquivalence.lagda.md @@ -78,7 +78,7 @@ denot-equal-terminates {Γ}{M}{N}{C} ℰM≃ℰN ⟨ N′ , CM—↠ƛN′ ⟩ = cbn→reduce (proj₂ (proj₂ (proj₂ (↓→⇓ ℰCN≃ℰƛN′)))) ``` -The proof is direct. Because `plug C —↠ plug C (ƛ N′)`, +The proof is direct. Because `plug C M —↠ ƛ N′`, we can apply soundness to obtain ℰ (plug C M) ≃ ℰ (ƛ N′) @@ -93,7 +93,7 @@ Putting these two facts together gives us We then apply `↓→⇓` from Chapter [Adequacy](/Adequacy/) to deduce - ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ). + ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ. Call-by-name evaluation implies reduction to a lambda abstraction, so we conclude that