diff --git a/src/plfa/Adequacy.lagda b/src/plfa/Adequacy.lagda index e087e4a4..219b8645 100644 --- a/src/plfa/Adequacy.lagda +++ b/src/plfa/Adequacy.lagda @@ -28,43 +28,57 @@ open import Data.Unit open import Relation.Nullary using (Dec; yes; no) \end{code} +Having proved a preservation property in the last chapter, a natural +next step would be to prove progress. That is, to prove a property +of the form -In this chapter we prove that the denotational semantics is adequate, -that is, if a term M is denotationally equal to a lambda abstraction, -then M multi-step reduces to a lambda abstraction. + If γ ⊢ M ↓ v, then either M is a lambda abstraction or M —→ N for some N. + +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). + +This stronger property, reformulated a bit, is known as _adequacy_. +That is, if a term `M` is denotationally equal to a lambda abstraction, +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 -≃ ℰ (ƛ N) 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 +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 -Recall that ℰ M ≃ ℰ (ƛ N) is equivalent to saying that γ ⊢ M ↓ (v ↦ -v') for some v and v'. We will show that γ ⊢ M ↓ (v ↦ v') implies -that M halts under call-by-name. 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_ 𝕍. +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_ `𝕍`. The rest of this chapter is organized as follows. -* We loosen the requirement that M result in a function value to - instead require that M result in a value that is greater than or +* We 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 define the logical relation `𝕍` that relates values and closures, + and extend it to a relation on terms `𝔼` and environments `𝔾`. * We prove the main lemma, - that if 𝔾 γ γ' and γ ⊢ M ↓ v, then 𝔼 v (clos M γ'). + that if `𝔾 γ γ'` and `γ ⊢ M ↓ v`, then `𝔼 v (clos M γ')`. * We prove adequacy as a corollary to the main lemma. @@ -76,25 +90,25 @@ greather-than or equal to a function value. \begin{code} AboveFun : Value → Set -AboveFun v = Σ[ v₁ ∈ Value ] Σ[ v₂ ∈ Value ] v₁ ↦ v₂ ⊑ v +AboveFun u = Σ[ v ∈ Value ] Σ[ w ∈ Value ] v ↦ w ⊑ u \end{code} -If a value v is greater than a function, then an even greater value v' +If a value `u` is greater than a function, then an even greater value `u'` is too. \begin{code} -AboveFun-⊑ : ∀{v v' : Value} - → AboveFun v → v ⊑ v' +AboveFun-⊑ : ∀{u u' : Value} + → AboveFun u → u ⊑ u' ------------------- - → AboveFun v' -AboveFun-⊑ ⟨ v₁ , ⟨ v₂ , lt' ⟩ ⟩ lt = ⟨ v₁ , ⟨ v₂ , Trans⊑ lt' lt ⟩ ⟩ + → AboveFun u' +AboveFun-⊑ ⟨ v , ⟨ w , lt' ⟩ ⟩ lt = ⟨ v , ⟨ w , Trans⊑ lt' lt ⟩ ⟩ \end{code} -The bottom value ⊥ is not greater than a function. +The bottom value `⊥` is not greater than a function. \begin{code} AboveFun⊥ : ¬ AboveFun ⊥ -AboveFun⊥ ⟨ v₁ , ⟨ v₂ , lt ⟩ ⟩ +AboveFun⊥ ⟨ v , ⟨ w , lt ⟩ ⟩ with sub-inv-fun lt ... | ⟨ Γ , ⟨ f , ⟨ Γ⊆⊥ , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ with Funs∈ f @@ -103,50 +117,50 @@ AboveFun⊥ ⟨ v₁ , ⟨ v₂ , lt ⟩ ⟩ ... | () \end{code} -If the join of two values v₁ and v₂ is greater than a function, then +If the join of two values `u` and `u'` is greater than a function, then at least one of them is too. \begin{code} -AboveFun-⊔ : ∀{v₁ v₂} - → AboveFun (v₁ ⊔ v₂) - → AboveFun v₁ ⊎ AboveFun v₂ -AboveFun-⊔{v₁}{v₂} ⟨ v , ⟨ v' , v↦v'⊑v₁⊔v₂ ⟩ ⟩ - with sub-inv-fun v↦v'⊑v₁⊔v₂ -... | ⟨ Γ , ⟨ f , ⟨ Γ⊆v₁⊔v₂ , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ +AboveFun-⊔ : ∀{u u'} + → AboveFun (u ⊔ u') + → AboveFun u ⊎ AboveFun u' +AboveFun-⊔{u}{u'} ⟨ v , ⟨ w , v↦w⊑u⊔u' ⟩ ⟩ + with sub-inv-fun v↦w⊑u⊔u' +... | ⟨ Γ , ⟨ f , ⟨ Γ⊆u⊔u' , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ with Funs∈ f ... | ⟨ A , ⟨ B , m ⟩ ⟩ - with Γ⊆v₁⊔v₂ m + with Γ⊆u⊔u' m ... | inj₁ x = inj₁ ⟨ A , ⟨ B , (∈→⊑ x) ⟩ ⟩ ... | inj₂ x = inj₂ ⟨ A , ⟨ B , (∈→⊑ x) ⟩ ⟩ \end{code} -On the other hand, if neither of v₁ and v₂ is greater than a function, +On the other hand, if neither of `u` and `u'` is greater than a function, then their join is also not greater than a function. \begin{code} -not-AboveFun-⊔ : ∀{v₁ v₂ : Value} - → ¬ AboveFun v₁ → ¬ AboveFun v₂ - → ¬ AboveFun (v₁ ⊔ v₂) -not-AboveFun-⊔ af1 af2 af12 +not-AboveFun-⊔ : ∀{u u' : Value} + → ¬ AboveFun u → ¬ AboveFun u' + → ¬ AboveFun (u ⊔ u') +not-AboveFun-⊔ naf1 naf2 af12 with AboveFun-⊔ af12 -... | inj₁ x = contradiction x af1 -... | inj₂ x = contradiction x af2 +... | inj₁ af1 = contradiction af1 naf1 +... | inj₂ af2 = contradiction af2 naf2 \end{code} The converse is also true. If the join of two values is not above a function, then neither of them is individually. \begin{code} -not-AboveFun-⊔-inv : ∀{v₁ v₂ : Value} → ¬ AboveFun (v₁ ⊔ v₂) - → ¬ AboveFun v₁ × ¬ AboveFun v₂ +not-AboveFun-⊔-inv : ∀{u u' : Value} → ¬ AboveFun (u ⊔ u') + → ¬ AboveFun u × ¬ AboveFun u' not-AboveFun-⊔-inv af = ⟨ f af , g af ⟩ where - f : ∀{v₁ v₂ : Value} → ¬ AboveFun (v₁ ⊔ v₂) → ¬ AboveFun v₁ - f{v₁}{v₂} af12 ⟨ v , ⟨ v' , lt ⟩ ⟩ = - contradiction ⟨ v , ⟨ v' , ConjR1⊑ lt ⟩ ⟩ af12 - g : ∀{v₁ v₂ : Value} → ¬ AboveFun (v₁ ⊔ v₂) → ¬ AboveFun v₂ - g{v₁}{v₂} af12 ⟨ v , ⟨ v' , lt ⟩ ⟩ = - contradiction ⟨ v , ⟨ v' , ConjR2⊑ lt ⟩ ⟩ af12 + f : ∀{u u' : Value} → ¬ AboveFun (u ⊔ u') → ¬ AboveFun u + f{u}{u'} af12 ⟨ v , ⟨ w , lt ⟩ ⟩ = + contradiction ⟨ v , ⟨ w , ConjR1⊑ lt ⟩ ⟩ af12 + g : ∀{u u' : Value} → ¬ AboveFun (u ⊔ u') → ¬ AboveFun u' + g{u}{u'} af12 ⟨ v , ⟨ w , lt ⟩ ⟩ = + contradiction ⟨ v , ⟨ w , ConjR2⊑ lt ⟩ ⟩ af12 \end{code} The property of being greater than a function value is decidable, as @@ -155,11 +169,11 @@ exhibited by the following function. \begin{code} AboveFun? : (v : Value) → Dec (AboveFun v) AboveFun? ⊥ = no AboveFun⊥ -AboveFun? (v ↦ v') = yes ⟨ v , ⟨ v' , Refl⊑ ⟩ ⟩ -AboveFun? (v₁ ⊔ v₂) - with AboveFun? v₁ | AboveFun? v₂ -... | yes ⟨ v , ⟨ v' , lt ⟩ ⟩ | _ = yes ⟨ v , ⟨ v' , (ConjR1⊑ lt) ⟩ ⟩ -... | no _ | yes ⟨ v , ⟨ v' , lt ⟩ ⟩ = yes ⟨ v , ⟨ v' , (ConjR2⊑ lt) ⟩ ⟩ +AboveFun? (v ↦ w) = yes ⟨ v , ⟨ w , Refl⊑ ⟩ ⟩ +AboveFun? (u ⊔ u') + with AboveFun? u | AboveFun? u' +... | yes ⟨ v , ⟨ w , lt ⟩ ⟩ | _ = yes ⟨ v , ⟨ w , (ConjR1⊑ lt) ⟩ ⟩ +... | no _ | yes ⟨ v , ⟨ w , lt ⟩ ⟩ = yes ⟨ v , ⟨ w , (ConjR2⊑ lt) ⟩ ⟩ ... | no x | no y = no (not-AboveFun-⊔ x y) \end{code} @@ -207,27 +221,27 @@ data _⊢_⇓_ : ∀{Γ} → ClosEnv Γ → (Γ ⊢ ★) → Clos → Set where ⇓-lam : ∀{Γ}{γ : ClosEnv Γ}{M : Γ , ★ ⊢ ★} → γ ⊢ ƛ M ⇓ clos (ƛ M) γ - ⇓-app : ∀{Γ}{γ : ClosEnv Γ}{L M : Γ ⊢ ★}{Δ}{δ : ClosEnv Δ}{L' : Δ , ★ ⊢ ★}{c} - → γ ⊢ L ⇓ clos (ƛ L') δ → (δ ,' clos M γ) ⊢ L' ⇓ c + ⇓-app : ∀{Γ}{γ : ClosEnv Γ}{L M : Γ ⊢ ★}{Δ}{δ : ClosEnv Δ}{N : Δ , ★ ⊢ ★}{c} + → γ ⊢ L ⇓ clos (ƛ N) δ → (δ ,' clos M γ) ⊢ N ⇓ c ---------------------------------------------------- → γ ⊢ L · M ⇓ c \end{code} -* The (⇓-var) rule evaluates a variable by finding the associated +* The `⇓-var` rule evaluates a variable by finding the associated closure in the environment and then evaluating the closure. -* The (⇓-lam) rule turns a lambda abstraction into a closure +* The `⇓-lam` rule turns a lambda abstraction into a closure by packaging it up with its environment. -* The (⇓-app) rule performs function application by first evaluating - the term L in operator position. If that produces a closure containing - a lambda abstraction (ƛ L'), then we evaluate the body L' in an - environment extended with the argument M. Note that M is not - evaluated in rule (⇓-app) because this is call-by-name and not +* The `⇓-app` rule performs function application by first evaluating + the term `L` in operator position. If that produces a closure containing + a lambda abstraction `ƛ N`, then we evaluate the body `N` in an + environment extended with the argument `M`. Note that `M` is not + evaluated in rule `⇓-app` because this is call-by-name and not call-by-value. -If the big-step semantics says that a term M evaluates to both c and -c', then c and c' are identical. In other words, the big-step relation +If the big-step semantics says that a term `M` evaluates to both `c` and +`c'`, then `c` and `c'` are identical. In other words, the big-step relation is a partial function. \begin{code} @@ -246,60 +260,61 @@ is a partial function. ## Relating values to closures -Next we relate semantic values to closures. The relation 𝕍 is for -closures whose term is a lambda abstraction (i.e. in WHNF), whereas -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 according to v. +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, +`𝔼 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 +according to `v`. \begin{code} 𝕍 : Value → Clos → Set 𝔼 : Value → Clos → Set \end{code} -We define 𝕍 as a function from values and closures to Set and not as a -data type because it is mutually recursive with 𝔼 in a negative +We define `𝕍` as a function from values and closures to `Set` and not as a +data type because it is mutually recursive with `𝔼` in a negative position (to the left of an implication). We first perform case analysis on the term in the closure. If the term is a variable or -application, then 𝕍 is false (Bot). If the term is a lambda -abstraction, we define 𝕍 by recursion on the value, which we +application, then `𝕍` is false (`Bot`). If the term is a lambda +abstraction, we define `𝕍` by recursion on the value, which we describe below. \begin{code} 𝕍 v (clos (` x₁) γ) = Bot 𝕍 v (clos (M · M₁) γ) = Bot 𝕍 ⊥ (clos (ƛ M) γ) = ⊤ -𝕍 (v ↦ v') (clos (ƛ M) γ) = - (∀{c : Clos} → 𝔼 v c → AboveFun v' → Σ[ c' ∈ Clos ] - (γ ,' c) ⊢ M ⇓ c' × 𝕍 v' c') -𝕍 (v₁ ⊔ v₂) (clos (ƛ M) γ) = 𝕍 v₁ (clos (ƛ M) γ) × 𝕍 v₂ (clos (ƛ M) γ) +𝕍 (v ↦ w) (clos (ƛ N) γ) = + (∀{c : Clos} → 𝔼 v c → AboveFun w → Σ[ c' ∈ Clos ] + (γ ,' c) ⊢ N ⇓ c' × 𝕍 w c') +𝕍 (u ⊔ v) (clos (ƛ N) γ) = 𝕍 u (clos (ƛ N) γ) × 𝕍 v (clos (ƛ N) γ) \end{code} -* If the value is ⊥, then the result is true (⊤). +* If the value is `⊥`, then the result is true (`⊤`). -* If the value is a join (v₁ ⊔ v₂), then the result is the pair - (conjunction) of 𝕍 is true for both v₁ and v₂. +* If the value is a join (u ⊔ v), then the result is the pair + (conjunction) of 𝕍 is true for both u and v. -* The important case is for a function value (v ↦ v') and closure - (clos (ƛ M) γ). Given any closure c such that 𝔼 v c, if v' is - greater than a function, then M evaluates (with γ extended with c) - to some closure c' and we have 𝕍 v' c'. +* 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 + greater than a function, then `N` evaluates (with `γ` extended with `c`) + to some closure `c'` and we have `𝕍 w c'`. -The definition of 𝔼 is straightforward. If v is a greater than a -function, then M evaluates to a closure related to v. +The definition of `𝔼` is straightforward. If `v` is a greater than a +function, then `M` evaluates to a closure related to `v`. \begin{code} 𝔼 v (clos M γ') = AboveFun v → Σ[ c ∈ Clos ] γ' ⊢ M ⇓ c × 𝕍 v c \end{code} -The proof of the main lemma is by induction on γ ⊢ M ↓ v, so it goes +The proof of the main lemma is by induction on `γ ⊢ M ↓ v`, so it goes underneath lambda abstractions and must therefore reason about open -terms (terms with variables). Thus, we must relate environments of -semantic values to environments of closures. In the following, 𝔾 -relates γ to γ' if the corresponding values and closures are related -by 𝔼. +terms (terms with variables). So we must relate environments of +semantic values to environments of closures. In the following, `𝔾` +relates `γ` to `γ'` if the corresponding values and closures are related +by `𝔼`. \begin{code} 𝔾 : ∀{Γ} → Env Γ → ClosEnv Γ → Set @@ -315,8 +330,8 @@ by 𝔼. \end{code} -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 +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. \begin{code} @@ -331,38 +346,38 @@ The proof goes by cases on the term in the closure. 𝕍→WHNF : ∀{Γ}{γ : ClosEnv Γ}{M : Γ ⊢ ★}{v} → 𝕍 v (clos M γ) → WHNF M 𝕍→WHNF {M = ` x} {v} () -𝕍→WHNF {M = ƛ M} {v} vc = ƛ_ -𝕍→WHNF {M = M · M₁} {v} () +𝕍→WHNF {M = ƛ N} {v} vc = ƛ_ +𝕍→WHNF {M = L · M} {v} () \end{code} -Next we have an introduction rule for 𝕍 that mimics the (⊔-intro) -rule. If both v₁ and v₂ are related to a closure c, then their join is +Next we have an introduction rule for `𝕍` that mimics the `⊔-intro` +rule. If both `u` and `v` are related to a closure `c`, then their join is too. \begin{code} -𝕍⊔-intro : ∀{c v₁ v₂} - → 𝕍 v₁ c → 𝕍 v₂ c +𝕍⊔-intro : ∀{c u v} + → 𝕍 u c → 𝕍 v c --------------- - → 𝕍 (v₁ ⊔ v₂) c -𝕍⊔-intro {clos (` x₁) x} () v2c -𝕍⊔-intro {clos (ƛ M) x} v1c v2c = ⟨ v1c , v2c ⟩ -𝕍⊔-intro {clos (M · M₁) x} () v2c + → 𝕍 (u ⊔ v) c +𝕍⊔-intro {clos (` x) γ} () vc +𝕍⊔-intro {clos (ƛ N) γ} uc vc = ⟨ uc , vc ⟩ +𝕍⊔-intro {clos (L · M) γ} () vc \end{code} -In a moment we prove that 𝕍 is preserved when going from a greater -value to a lesser value: if 𝕍 v c and v' ⊑ v, then 𝕍 v' c. -This property, named 𝕍-sub, is needed by the main lemma in -the case for the (sub) rule. +In a moment we prove that `𝕍` is preserved when going from a greater +value to a lesser value: if `𝕍 v c` and `v' ⊑ v`, then `𝕍 v' c`. +This property, named `𝕍-sub`, is needed by the main lemma in +the case for the `sub` rule. -To prove 𝕍-sub, we in turn need the following property concerning +To prove `𝕍-sub`, we in turn need the following property concerning values that are not greater than a function, that is, values that are -equivalent to ⊥. In such cases, 𝕍 v (clos (ƛ M) γ') is trivially true. +equivalent to `⊥`. In such cases, `𝕍 v (clos (ƛ N) γ')` is trivially true. \begin{code} -not-AboveFun-𝕍 : ∀{v : Value}{Γ}{γ' : ClosEnv Γ}{M : Γ , ★ ⊢ ★ } +not-AboveFun-𝕍 : ∀{v : Value}{Γ}{γ' : ClosEnv Γ}{N : Γ , ★ ⊢ ★ } → ¬ AboveFun v ------------------- - → 𝕍 v (clos (ƛ M) γ') + → 𝕍 v (clos (ƛ N) γ') not-AboveFun-𝕍 {⊥} af = tt not-AboveFun-𝕍 {v ↦ v'} af = ⊥-elim (contradiction ⟨ v , ⟨ v' , Refl⊑ ⟩ ⟩ af) not-AboveFun-𝕍 {v₁ ⊔ v₂} af @@ -370,126 +385,127 @@ not-AboveFun-𝕍 {v₁ ⊔ v₂} af ... | ⟨ af1 , af2 ⟩ = ⟨ not-AboveFun-𝕍 af1 , not-AboveFun-𝕍 af2 ⟩ \end{code} -The proofs of 𝕍-sub and 𝔼-sub are intertwined. +The proofs of `𝕍-sub` and `𝔼-sub` are intertwined. \begin{code} sub-𝕍 : ∀{c : Clos}{v v'} → 𝕍 v c → v' ⊑ v → 𝕍 v' c sub-𝔼 : ∀{c : Clos}{v v'} → 𝔼 v c → v' ⊑ v → 𝔼 v' c \end{code} -We prove 𝕍-sub by case analysis on the closure's term, to dispatch the +We prove `𝕍-sub` by case analysis on the closure's term, to dispatch the cases for variables and application. We then proceed by induction on -v' ⊑ v. We describe each case below. +`v' ⊑ v`. We describe each case below. \begin{code} sub-𝕍 {clos (` x) γ} {v} () lt -sub-𝕍 {clos (M₁ · M₂) γ} () lt -sub-𝕍 {clos (ƛ M) γ} vc Bot⊑ = tt -sub-𝕍 {clos (ƛ M) γ} vc (ConjL⊑ lt1 lt2) = ⟨ (sub-𝕍 vc lt1) , sub-𝕍 vc lt2 ⟩ -sub-𝕍 {clos (ƛ M) γ} ⟨ vv1 , vv2 ⟩ (ConjR1⊑ lt) = sub-𝕍 vv1 lt -sub-𝕍 {clos (ƛ M) γ} ⟨ vv1 , vv2 ⟩ (ConjR2⊑ lt) = sub-𝕍 vv2 lt -sub-𝕍 {clos (ƛ M) γ} vc (Trans⊑{v = v₂} lt1 lt2) = sub-𝕍 (sub-𝕍 vc lt2) lt1 -sub-𝕍 {clos (ƛ M) γ} vc (Fun⊑ lt1 lt2) ev1 sf +sub-𝕍 {clos (L · M) γ} () lt +sub-𝕍 {clos (ƛ N) γ} vc Bot⊑ = tt +sub-𝕍 {clos (ƛ N) γ} vc (ConjL⊑ lt1 lt2) = ⟨ (sub-𝕍 vc lt1) , sub-𝕍 vc lt2 ⟩ +sub-𝕍 {clos (ƛ N) γ} ⟨ vv1 , vv2 ⟩ (ConjR1⊑ lt) = sub-𝕍 vv1 lt +sub-𝕍 {clos (ƛ N) γ} ⟨ vv1 , vv2 ⟩ (ConjR2⊑ lt) = sub-𝕍 vv2 lt +sub-𝕍 {clos (ƛ N) γ} vc (Trans⊑{v = v₂} lt1 lt2) = sub-𝕍 (sub-𝕍 vc lt2) lt1 +sub-𝕍 {clos (ƛ N) γ} vc (Fun⊑ lt1 lt2) ev1 sf with vc (sub-𝔼 ev1 lt1) (AboveFun-⊑ sf lt2) -... | ⟨ c , ⟨ Mc , v4 ⟩ ⟩ = ⟨ c , ⟨ Mc , sub-𝕍 v4 lt2 ⟩ ⟩ -sub-𝕍 {clos (ƛ M) γ} {v₁ ↦ v₂ ⊔ v₁ ↦ v₃} ⟨ vc12 , vc13 ⟩ Dist⊑ ev1c sf - with AboveFun? v₂ | AboveFun? v₃ +... | ⟨ c , ⟨ Nc , v4 ⟩ ⟩ = ⟨ c , ⟨ Nc , sub-𝕍 v4 lt2 ⟩ ⟩ +sub-𝕍 {clos (ƛ N) γ} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf + with AboveFun? w | AboveFun? w' ... | yes af2 | yes af3 - with vc12 ev1c af2 | vc13 ev1c af3 -... | ⟨ clos N δ , ⟨ M⇓c₂ , 𝕍v₂ ⟩ ⟩ - | ⟨ c₃ , ⟨ M⇓c₃ , 𝕍v₃ ⟩ ⟩ rewrite ⇓-determ M⇓c₃ M⇓c₂ with 𝕍→WHNF 𝕍v₂ + with vcw ev1c af2 | vcw' ev1c af3 +... | ⟨ clos L δ , ⟨ L⇓c₂ , 𝕍w ⟩ ⟩ + | ⟨ c₃ , ⟨ L⇓c₃ , 𝕍w' ⟩ ⟩ rewrite ⇓-determ L⇓c₃ L⇓c₂ with 𝕍→WHNF 𝕍w ... | ƛ_ = - ⟨ clos N δ , ⟨ M⇓c₂ , ⟨ 𝕍v₂ , 𝕍v₃ ⟩ ⟩ ⟩ -sub-𝕍 {c} {v₁ ↦ v₂ ⊔ v₁ ↦ v₃} ⟨ vc12 , vc13 ⟩ Dist⊑ ev1c sf + ⟨ clos L δ , ⟨ L⇓c₂ , ⟨ 𝕍w , 𝕍w' ⟩ ⟩ ⟩ +sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf | yes af2 | no naf3 - with vc12 ev1c af2 -... | ⟨ clos {Γ'} N γ₁ , ⟨ M⇓c2 , 𝕍v₂ ⟩ ⟩ - with 𝕍→WHNF 𝕍v₂ + with vcw ev1c af2 +... | ⟨ clos {Γ'} L γ₁ , ⟨ L⇓c2 , 𝕍w ⟩ ⟩ + with 𝕍→WHNF 𝕍w ... | ƛ_ {N = N'} = - let 𝕍v₃ = not-AboveFun-𝕍{v₃}{Γ'}{γ₁}{N'} naf3 in - ⟨ clos (ƛ N') γ₁ , ⟨ M⇓c2 , 𝕍⊔-intro 𝕍v₂ 𝕍v₃ ⟩ ⟩ -sub-𝕍 {c} {v₁ ↦ v₂ ⊔ v₁ ↦ v₃} ⟨ vc12 , vc13 ⟩ Dist⊑ ev1c sf + let 𝕍w' = not-AboveFun-𝕍{w'}{Γ'}{γ₁}{N'} naf3 in + ⟨ clos (ƛ N') γ₁ , ⟨ L⇓c2 , 𝕍⊔-intro 𝕍w 𝕍w' ⟩ ⟩ +sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf | no naf2 | yes af3 - with vc13 ev1c af3 -... | ⟨ clos {Γ'} N γ₁ , ⟨ M⇓c3 , 𝕍3c ⟩ ⟩ - with 𝕍→WHNF 𝕍3c + with vcw' ev1c af3 +... | ⟨ clos {Γ'} L γ₁ , ⟨ L⇓c3 , 𝕍w'c ⟩ ⟩ + with 𝕍→WHNF 𝕍w'c ... | ƛ_ {N = N'} = - let 𝕍2c = not-AboveFun-𝕍{v₂}{Γ'}{γ₁}{N'} naf2 in - ⟨ clos (ƛ N') γ₁ , ⟨ M⇓c3 , 𝕍⊔-intro 𝕍2c 𝕍3c ⟩ ⟩ -sub-𝕍 {c} {v₁ ↦ v₂ ⊔ v₁ ↦ v₃} ⟨ vc12 , vc13 ⟩ Dist⊑ ev1c ⟨ v , ⟨ v' , lt ⟩ ⟩ + let 𝕍wc = not-AboveFun-𝕍{w}{Γ'}{γ₁}{N'} naf2 in + ⟨ clos (ƛ N') γ₁ , ⟨ L⇓c3 , 𝕍⊔-intro 𝕍wc 𝕍w'c ⟩ ⟩ +sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ w'' , lt ⟩ ⟩ | no naf2 | no naf3 - with AboveFun-⊔ ⟨ v , ⟨ v' , lt ⟩ ⟩ + with AboveFun-⊔ ⟨ v' , ⟨ w'' , lt ⟩ ⟩ ... | inj₁ af2 = ⊥-elim (contradiction af2 naf2) ... | inj₂ af3 = ⊥-elim (contradiction af3 naf3) \end{code} -* Case (Bot⊑). We immediately have 𝕍 ⊥ (clos (ƛ M) γ). +* Case `Bot⊑`. We immediately have `𝕍 ⊥ (clos (ƛ N) γ)`. -* Case (ConjL⊑). +* Case `ConjL⊑`. v₁' ⊑ v v₂' ⊑ v ------------------- (v₁' ⊔ v₂') ⊑ v - The induction hypotheses gives us 𝕍 v₁' (clos (ƛ M) γ) - and 𝕍 v₂' (clos (ƛ M) γ), which is all we need for this case. + The induction hypotheses gives us `𝕍 v₁' (clos (ƛ N) γ)` + and `𝕍 v₂' (clos (ƛ N) γ)`, which is all we need for this case. -* Case (ConjR1⊑). +* Case `ConjR1⊑`. v' ⊑ v₁ ------------- v' ⊑ (v₁ ⊔ v₂) - The induction hypothesis gives us 𝕍 v' (clos (ƛ M) γ). + The induction hypothesis gives us `𝕍 v' (clos (ƛ N) γ)`. -* Case (ConjR2⊑). +* Case `ConjR2⊑`. v' ⊑ v₂ ------------- v' ⊑ (v₁ ⊔ v₂) - Again, the induction hypothesis gives us 𝕍 v' (clos (ƛ M) γ). + Again, the induction hypothesis gives us `𝕍 v' (clos (ƛ N) γ)`. -* Case (Trans⊑). +* Case `Trans⊑`. v' ⊑ v₂ v₂ ⊑ v ----------------- v' ⊑ v - The induction hypothesis for v₂ ⊑ v gives us - 𝕍 v₂ (clos (ƛ M) γ). We apply the induction hypothesis - for v' ⊑ v₂ to conclude that 𝕍 v' (clos (ƛ M) γ). + The induction hypothesis for `v₂ ⊑ v` gives us + `𝕍 v₂ (clos (ƛ N) γ)`. We apply the induction hypothesis + for `v' ⊑ v₂` to conclude that `𝕍 v' (clos (ƛ N) γ)`. -* Case (Dist⊑). This case is the most difficult. We have +* Case `Dist⊑`. This case is the most difficult. We have - 𝕍 (v₁ ↦ v₂) (clos (ƛ M) γ) - 𝕍 (v₁ ↦ v₃) (clos (ƛ M) γ) + 𝕍 (v ↦ w) (clos (ƛ N) γ) + 𝕍 (v ↦ w') (clos (ƛ N) γ) and need to show that - 𝕍 (v₁ ↦ (v₂ ⊔ v₃)) (clos (ƛ M) γ) + 𝕍 (v ↦ (w ⊔ w')) (clos (ƛ N) γ) - Let c be an arbtrary closure such that 𝔼 v₁ c. - Assume (v₂ ⊔ v₃) is greater than a function. - Unfortunately, this does not mean that both v₂ and v₃ - are above functions. But thanks to the lemma AboveFun-⊔, + Let `c` be an arbtrary closure such that `𝔼 v c`. + Assume `w ⊔ w'` is greater than a function. + Unfortunately, this does not mean that both `w` and `w'` + are above functions. But thanks to the lemma `AboveFun-⊔`, we know that at least one of them is greater than a function. * Suppose both of them are greater than a function. Then we have - γ ⊢ M ⇓ clos N δ and 𝕍 v₂ (clos N δ). We also have γ ⊢ M ⇓ c₃ and - 𝕍 v₃ c₃. Because the big-step semantics is deterministic, we have - c₃ ≡ clos N δ. Also, from 𝕍 v₂ (clos N δ) we know that N ≡ ƛ N' - for some N'. We conclude that 𝕍 (v₂ ⊔ v₃) (clos (ƛ N') δ). + `γ ⊢ N ⇓ clos L δ` and `𝕍 w (clos L δ)`. We also have `γ ⊢ N ⇓ c₃` and + `𝕍 w' c₃`. Because the big-step semantics is deterministic, we have + `c₃ ≡ clos L δ`. Also, from `𝕍 w (clos L δ)` we know that `L ≡ ƛ N'` + for some `N'`. We conclude that `𝕍 (w ⊔ w') (clos (ƛ N') δ)`. * Suppose one of them is greater than a function and the other is - not: say AboveFun v₂ and ¬ AboveFun v₃. Then from 𝕍 (v₁ ↦ v₂) (clos (ƛ M) γ) - we have γ ⊢ M ⇓ clos N γ₁ and 𝕍 v₂ (clos N γ₁). From this we have - N ≡ ƛ N' for some N'. Meanwhile, from ¬ AboveFun v₃ we have - 𝕍 v₃ (clos N γ₁). We conclude that We conclude that - 𝕍 (v₂ ⊔ v₃) (clos (ƛ N') γ₁). + not: say `AboveFun w` and `¬ AboveFun w'`. Then from + `𝕍 (v ↦ w) (clos (ƛ N) γ)` + we have `γ ⊢ N ⇓ clos L γ₁` and `𝕍 w (clos L γ₁)`. From this we have + `L ≡ ƛ N'` for some `N'`. Meanwhile, from `¬ AboveFun w'` we have + `𝕍 w' (clos L γ₁)`. We conclude that + `𝕍 (w ⊔ w') (clos (ƛ N') γ₁)`. -The proof of sub-𝔼 is direct. +The proof of `sub-𝔼` is direct and explained below. \begin{code} sub-𝔼 {clos M γ} {v} {v'} 𝔼v v'⊑v fv' @@ -498,19 +514,19 @@ sub-𝔼 {clos M γ} {v} {v'} 𝔼v v'⊑v fv' ⟨ c , ⟨ M⇓c , sub-𝕍 𝕍v v'⊑v ⟩ ⟩ \end{code} -From AboveFun v' and v' ⊑ v we have AboveFun v. Then with 𝔼 v c we -obtain a closure c such that γ ⊢ M ⇓ c and 𝕍 v c. We conclude with an -application of sub-𝕍 with v' ⊑ v to show 𝕍 v' c. +From `AboveFun v'` and `v' ⊑ v` we have `AboveFun v`. Then with `𝔼 v c` we +obtain a closure `c` such that `γ ⊢ M ⇓ c` and `𝕍 v c`. We conclude with an +application of `sub-𝕍` with `v' ⊑ v` to show `𝕍 v' c`. ## Programs with function denotation terminate via call-by-name The main lemma proves that if a term has a denotation that is above a -function, then it terminates via call-by-name. In more detail, if γ ⊢ -M ↓ v and 𝔾 γ γ', then 𝔼 v (clos M γ'). The proof is by induction on -the derivation of γ ⊢ M ↓ v we discuss each case below. +function, then it terminates via call-by-name. More formally, if +`γ ⊢ M ↓ v` and `𝔾 γ γ'`, then `𝔼 v (clos M γ')`. The proof is by +induction on the derivation of `γ ⊢ M ↓ v` we discuss each case below. -The following lemma, kth-x, is used in the case for the (var) rule. +The following lemma, kth-x, is used in the case for the `var` rule. \begin{code} kth-x : ∀{Γ}{γ' : ClosEnv Γ}{x : Γ ∋ ★} @@ -523,27 +539,27 @@ kth-x{γ' = γ'}{x = x} with γ' x \begin{code} ↓→𝔼 : ∀{Γ}{γ : Env Γ}{γ' : ClosEnv Γ}{M : Γ ⊢ ★ }{v} → 𝔾 γ γ' → γ ⊢ M ↓ v → 𝔼 v (clos M γ') -↓→𝔼 {Γ} {γ} {γ'} {`_ x} {v} 𝔾γγ' var fγx +↓→𝔼 {Γ} {γ} {γ'} 𝔾γγ' (var{x = x}) fγx with kth-x{Γ}{γ'}{x} | 𝔾γγ'{x = x} -... | ⟨ Δ , ⟨ δ , ⟨ L , eq ⟩ ⟩ ⟩ | 𝔾γγ'x rewrite eq +... | ⟨ Δ , ⟨ δ , ⟨ M' , eq ⟩ ⟩ ⟩ | 𝔾γγ'x rewrite eq with 𝔾γγ'x fγx -... | ⟨ c , ⟨ L⇓c , 𝕍γx ⟩ ⟩ = - ⟨ c , ⟨ (⇓-var eq L⇓c) , 𝕍γx ⟩ ⟩ -↓→𝔼 {Γ} {γ} {γ'} {L · M} {v} 𝔾γγ' (↦-elim{v = v₁} d₁ d₂) fv +... | ⟨ c , ⟨ M'⇓c , 𝕍γx ⟩ ⟩ = + ⟨ c , ⟨ (⇓-var eq M'⇓c) , 𝕍γx ⟩ ⟩ +↓→𝔼 {Γ} {γ} {γ'} 𝔾γγ' (↦-elim{L = L}{M = M}{v = v₁}{w = v} d₁ d₂) fv with ↓→𝔼 𝔾γγ' d₁ ⟨ v₁ , ⟨ v , Refl⊑ ⟩ ⟩ ... | ⟨ clos L' δ , ⟨ L⇓L' , 𝕍v₁↦v ⟩ ⟩ with 𝕍→WHNF 𝕍v₁↦v -... | ƛ_ {N = L''} +... | ƛ_ {N = N} with 𝕍v₁↦v {clos M γ'} (↓→𝔼 𝔾γγ' d₂) fv -... | ⟨ c' , ⟨ L''⇓c' , 𝕍v ⟩ ⟩ = - ⟨ c' , ⟨ ⇓-app L⇓L' L''⇓c' , 𝕍v ⟩ ⟩ -↓→𝔼 {Γ} {γ} {γ'} {ƛ M} {v ↦ v'} 𝔾γγ' (↦-intro d) fv↦v' = - ⟨ (clos (ƛ M) γ') , ⟨ ⇓-lam , E ⟩ ⟩ - where E : {c : Clos} → 𝔼 v c → AboveFun v' - → Σ[ c' ∈ Clos ] (γ' ,' c) ⊢ M ⇓ c' × 𝕍 v' c' - E {c} 𝔼vc fv' = ↓→𝔼 (λ {x} → 𝔾-ext{Γ}{γ}{γ'} 𝔾γγ' 𝔼vc {x}) d fv' -↓→𝔼 {Γ} {γ} {γ'} {M} {⊥} 𝔾γγ' ⊥-intro f⊥ = ⊥-elim (AboveFun⊥ f⊥) -↓→𝔼 {Γ} {γ} {γ'} {M} {v₁ ⊔ v₂} 𝔾γγ' (⊔-intro d₁ d₂) fv12 +... | ⟨ c' , ⟨ N⇓c' , 𝕍v ⟩ ⟩ = + ⟨ c' , ⟨ ⇓-app L⇓L' N⇓c' , 𝕍v ⟩ ⟩ +↓→𝔼 {Γ} {γ} {γ'} 𝔾γγ' (↦-intro{N = N}{v = v}{w = w} d) fv↦w = + ⟨ clos (ƛ N) γ' , ⟨ ⇓-lam , E ⟩ ⟩ + where E : {c : Clos} → 𝔼 v c → AboveFun w + → Σ[ c' ∈ Clos ] (γ' ,' c) ⊢ N ⇓ c' × 𝕍 w c' + E {c} 𝔼vc fw = ↓→𝔼 (λ {x} → 𝔾-ext{Γ}{γ}{γ'} 𝔾γγ' 𝔼vc {x}) d fw +↓→𝔼 𝔾γγ' ⊥-intro f⊥ = ⊥-elim (AboveFun⊥ f⊥) +↓→𝔼 𝔾γγ' (⊔-intro{v = v₁}{w = v₂} d₁ d₂) fv12 with AboveFun? v₁ | AboveFun? v₂ ... | yes fv1 | yes fv2 with ↓→𝔼 𝔾γγ' d₁ fv1 | ↓→𝔼 𝔾γγ' d₂ fv2 @@ -554,16 +570,16 @@ kth-x{γ' = γ'}{x = x} with γ' x with ↓→𝔼 𝔾γγ' d₁ fv1 ... | ⟨ clos {Γ'} M' γ₁ , ⟨ M⇓c₁ , 𝕍v₁ ⟩ ⟩ with 𝕍→WHNF 𝕍v₁ -... | ƛ_ {N = M''} = - let 𝕍v₂ = not-AboveFun-𝕍{v₂}{Γ'}{γ₁}{M''} nfv2 in - ⟨ clos (ƛ M'') γ₁ , ⟨ M⇓c₁ , 𝕍⊔-intro 𝕍v₁ 𝕍v₂ ⟩ ⟩ +... | ƛ_ {N = N} = + let 𝕍v₂ = not-AboveFun-𝕍{v₂}{Γ'}{γ₁}{N} nfv2 in + ⟨ clos (ƛ N) γ₁ , ⟨ M⇓c₁ , 𝕍⊔-intro 𝕍v₁ 𝕍v₂ ⟩ ⟩ ↓→𝔼 𝔾γγ' (⊔-intro{v = v₁}{w = v₂} d₁ d₂) fv12 | no nfv1 | yes fv2 with ↓→𝔼 𝔾γγ' d₂ fv2 -... | ⟨ clos {Γ'} M' γ₁ , ⟨ M⇓c₂ , 𝕍2c ⟩ ⟩ +... | ⟨ clos {Γ'} M' γ₁ , ⟨ M'⇓c₂ , 𝕍2c ⟩ ⟩ with 𝕍→WHNF 𝕍2c -... | ƛ_ {N = M} = - let 𝕍1c = not-AboveFun-𝕍{v₁}{Γ'}{γ₁}{M} nfv1 in - ⟨ clos (ƛ M) γ₁ , ⟨ M⇓c₂ , 𝕍⊔-intro 𝕍1c 𝕍2c ⟩ ⟩ +... | ƛ_ {N = N} = + let 𝕍1c = not-AboveFun-𝕍{v₁}{Γ'}{γ₁}{N} nfv1 in + ⟨ clos (ƛ N) γ₁ , ⟨ M'⇓c₂ , 𝕍⊔-intro 𝕍1c 𝕍2c ⟩ ⟩ ↓→𝔼 𝔾γγ' (⊔-intro d₁ d₂) fv12 | no nfv1 | no nfv2 with AboveFun-⊔ fv12 ... | inj₁ fv1 = ⊥-elim (contradiction fv1 nfv1) @@ -574,64 +590,66 @@ kth-x{γ' = γ'}{x = x} with γ' x ⟨ c , ⟨ M⇓c , sub-𝕍 𝕍v v'⊑v ⟩ ⟩ \end{code} -* Case (var). Looking up x in γ' yields some closure, clos L δ, - and from 𝔾 γ γ' we have 𝔼 (γ x) (clos L δ). With the premise - AboveFun (γ x), we obtain a closure c such that δ ⊢ L ⇓ c - and 𝕍 (γ x) c. To conclude γ' ⊢ ` x ⇓ c via (⇓-var), we - need γ' x ≡ clos L δ, which is obvious, but it requires some - Agda shananigans via the kth-x lemma to get our hands on it. +* Case `var`. Looking up `x` in `γ'` yields some closure, `clos M' δ`, + and from `𝔾 γ γ'` we have `𝔼 (γ x) (clos M' δ)`. With the premise + `AboveFun (γ x)`, we obtain a closure `c` such that `δ ⊢ M' ⇓ c` + 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' δ). - Of course, L' ≡ ƛ L'' for some L''. - By the induction hypothesis for γ ⊢ M ↓ v₁, - we have 𝔼 v₁ (clos M γ'). - Together with the premise AboveFun v and 𝕍 v (clos L' δ), - we obtain a closure c' such that δ ⊢ L'' ⇓ c' and 𝕍 v c'. - We conclude that γ' ⊢ L · M ⇓ c' by rule (⇓-app). +* Case `↦-elim`. We have `γ ⊢ L · M ↓ v`. + The induction hypothesis for `γ ⊢ L ↓ v₁ ↦ v` + gives us `γ' ⊢ L ⇓ clos L' δ` and `𝕍 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 `AboveFun v` and `𝕍 v (clos L' δ)`, + we obtain a closure `c'` such that `δ ⊢ N ⇓ c'` and `𝕍 v c'`. + We conclude that `γ' ⊢ L · M ⇓ c'` by rule `⇓-app`. -* Case (↦-intro). We have γ ⊢ ƛ M ↓ v ↦ v'. - We immediately have γ' ⊢ ƛ M ⇓ clos (ƛ M) γ' by rule (⇓-lam). - But we also need to prove 𝕍 (v ↦ v') (clos (ƛ M) γ'). - Let c by an arbitrary closure such that 𝔼 v c. - Suppose v' is greater than a function value. - We need to show that γ' , c ⊢ M ⇓ c' and 𝕍 v' c' for some c'. - We prove this by the induction hypothesis for γ , v ⊢ M ↓ v' - but we must first show that 𝔾 (γ , v) (γ' , c). We prove - that by the lemma 𝔾-ext, using facts 𝔾 γ γ' and 𝔼 v c. +* Case `↦-intro`. We have `γ ⊢ ƛ N ↓ v ↦ w`. + We immediately have `γ' ⊢ ƛ M ⇓ clos (ƛ M) γ'` 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'`. + 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`. -* Case (⊥-intro). We have the premise AboveFun ⊥, but that's impossible. +* Case `⊥-intro`. We have the premise `AboveFun ⊥`, but that's impossible. -* Case (⊔-intro). We have γ ⊢ M ↓ (v₁ ⊔ v₂) and AboveFun (v₁ ⊔ v₂) - and need to show γ' ⊢ M ↓ c and 𝕍 (v₁ ⊔ v₂) c for some c. - Again, by AboveFun-⊔, at least one of v₁ or v₂ is greater than a function. +* Case `⊔-intro`. We have `γ ⊢ M ↓ (v₁ ⊔ v₂)` and `AboveFun (v₁ ⊔ v₂)` + and need to show `γ' ⊢ M ↓ c` and `𝕍 (v₁ ⊔ v₂) c` for some `c`. + Again, by `AboveFun-⊔`, at least one of `v₁` or `v₂` is greater than + a function. - * Suppose both v₁ and v₂ are greater than a function value. - By the induction hypotheses for γ ⊢ M ↓ v₁ and γ ⊢ M ↓ v₂ - we have γ' ⊢ M ⇓ c₁, 𝕍 v₁ c₁, γ' ⊢ M ⇓ c₂, and 𝕍 v₂ c₂ for some c₁ and c₂. - Because ⇓ is deterministic, we have c₂ ≡ c₁. - Then by 𝕍⊔-intro we conclude that 𝕍 (v₁ ⊔ v₂) c₁. + * Suppose both `v₁` and `v₂` are greater than a function value. + By the induction hypotheses for `γ ⊢ M ↓ v₁` and `γ ⊢ M ↓ v₂` + we have `γ' ⊢ M ⇓ c₁`, `𝕍 v₁ c₁`, `γ' ⊢ M ⇓ c₂`, and `𝕍 v₂ c₂` + for some `c₁` and `c₂`. Because `⇓` is deterministic, we have `c₂ ≡ c₁`. + Then by `𝕍⊔-intro` we conclude that `𝕍 (v₁ ⊔ v₂) c₁`. - * Without loss of generality, suppose v₁ is greater than a function - value but v₂ is not. By the induction hypotheses for γ ⊢ M ↓ v₁, - and using 𝕍→WHNF, we have γ' ⊢ M ⇓ clos (ƛ M'') γ₁ - and 𝕍 v₁ (clos (ƛ M'') γ₁). - Then because v₂ is not greater than a function, we also have - 𝕍 v₂ (clos (ƛ M'') γ₁). We conclude that 𝕍 (v₁ ⊔ v₂) (clos (ƛ M'') γ₁). + * Without loss of generality, suppose `v₁` is greater than a function + value but `v₂` is not. By the induction hypotheses for `γ ⊢ M ↓ v₁`, + and using `𝕍→WHNF`, we have `γ' ⊢ M ⇓ clos (ƛ N) γ₁` + and `𝕍 v₁ (clos (ƛ N) γ₁)`. + Then because `v₂` is not greater than a function, we also have + `𝕍 v₂ (clos (ƛ N) γ₁)`. We conclude that `𝕍 (v₁ ⊔ v₂) (clos (ƛ N) γ₁)`. -* Case (sub). We have γ ⊢ M ↓ v, v' ⊑ v, and AboveFun v'. - We need to show that γ' ⊢ M ⇓ c and 𝕍 v' c for some c. - We have AboveFun v by AboveFun-⊑, - so the induction hypothesis for γ ⊢ M ↓ v gives us a closure c - such that γ' ⊢ M ⇓ c and 𝕍 v c. We conclude that 𝕍 v' c by sub-𝕍. +* Case `sub`. We have `γ ⊢ M ↓ v`, `v' ⊑ v`, and `AboveFun v'`. + We need to show that `γ' ⊢ M ⇓ c` and `𝕍 v' c` for some `c`. + We have `AboveFun v` by `AboveFun-⊑`, + so the induction hypothesis for `γ ⊢ M ↓ v` gives us a closure `c` + such that `γ' ⊢ M ⇓ c` and `𝕍 v c`. We conclude that `𝕍 v' c` by `sub-𝕍`. ## 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 ⇓ c for some c. +We have `∅ ⊢ ƛ N ↓ ⊥ ↦ ⊥`, so `ℰ M ≃ ℰ (ƛ N)` +gives us `∅ ⊢ M ↓ ⊥ ↦ ⊥`. Then the main lemma gives us +`∅ ⊢ M ⇓ c` for some `c`. \begin{code} adequacy : ∀{M : ∅ ⊢ ★}{N : ∅ , ★ ⊢ ★} → ℰ M ≃ ℰ (ƛ N) diff --git a/src/plfa/Soundness.lagda b/src/plfa/Soundness.lagda index 04087af3..63b68da5 100644 --- a/src/plfa/Soundness.lagda +++ b/src/plfa/Soundness.lagda @@ -34,20 +34,20 @@ open import Function using (_∘_) In this chapter we prove that the reduction semantics is sound with -respect to the denotational semantics, i.e., +respect to the denotational semantics, i.e., for any term L L —↠ ƛ N implies ℰ L ≃ ℰ (ƛ N) The proof is by induction on the reduction sequence, so the main lemma -concerns a single reduction step. We prove that if a term `M` steps to -`N`, then `M` and `N` are denotationally equal. We shall prove each -direction of this if-and-only-if separately. One direction will look -just like a type preservation proof. The other direction is like -proving type preservation for reduction going in reverse. Recall that -type preservation is sometimes called subject reduction. Preservation -in reverse is a well-known property and is called _subject -expansion_. It is also well-known that subject expansion is false for -most typed lambda calculi! +concerns a single reduction step. We prove that if any term `M` steps +to a term `N`, then `M` and `N` are denotationally equal. We shall +prove each direction of this if-and-only-if separately. One direction +will look just like a type preservation proof. The other direction is +like proving type preservation for reduction going in reverse. Recall +that type preservation is sometimes called subject +reduction. Preservation in reverse is a well-known property and is +called _subject expansion_. It is also well-known that subject +expansion is false for most typed lambda calculi! ## Forward reduction preserves denotations @@ -154,30 +154,30 @@ So we need to show that `γ ⊢ M [ N ] ↓ w`, or equivalently, that `γ ⊢ subst (subst-zero N) M ↓ w`. \begin{code} -substitution : ∀ {Γ} {γ : Env Γ} {M N v w} - → γ `, v ⊢ M ↓ w - → γ ⊢ N ↓ v +substitution : ∀ {Γ} {γ : Env Γ} {N M v w} + → γ `, v ⊢ N ↓ w + → γ ⊢ M ↓ v --------------- - → γ ⊢ M [ N ] ↓ w -substitution{Γ}{γ}{M}{N}{v}{w} dm dn = - subst-pres (subst-zero N) sub-z-ok dm + → γ ⊢ N [ M ] ↓ w +substitution{Γ}{γ}{N}{M}{v}{w} dn dm = + subst-pres (subst-zero M) sub-z-ok dn where - sub-z-ok : γ `⊢ subst-zero N ↓ (γ `, v) - sub-z-ok Z = dn + sub-z-ok : γ `⊢ subst-zero M ↓ (γ `, v) + sub-z-ok Z = dm sub-z-ok (S x) = var \end{code} This result is a corollary of the lemma for simultaneous substitution. -To use the lemma, we just need to show that `subst-zero N` maps +To use the lemma, we just need to show that `subst-zero M` maps variables to terms that produces the same values as those in `γ , v`. Let `y` be an arbitrary variable (de Bruijn index). -* If it is `Z`, then `(subst-zero N) y = N` and `nth y (γ , v) = v`. - By the premise we conclude that `γ ⊢ N ↓ v`. +* If it is `Z`, then `(subst-zero M) y = M` and `nth y (γ , v) = v`. + By the premise we conclude that `γ ⊢ M ↓ v`. -* If it is `S y'`, then `(subst-zero N) (S y') = y'` and - `nth (S y') (γ , v) = nth y' γ`. So we conclude that - `γ ⊢ y' ↓ nth y' γ` by rule `var`. +* If it is `S x`, then `(subst-zero M) (S x) = x` and + `nth (S x) (γ , v) = nth x γ`. So we conclude that + `γ ⊢ x ↓ nth x γ` by rule `var`. ### Reduction preserves denotations @@ -563,29 +563,29 @@ Most of the work is now behind us. We have proved that simultaneous substitution reflects denotations. Of course, β reduction uses single substitution, so we need a corollary that proves that single substitution reflects denotations. That is, -give terms `M : (Γ , ★ ⊢ ★)` and `N : (Γ ⊢ ★)`, -if `γ ⊢ M [ N ] ↓ v`, then `γ ⊢ N ↓ v₂` and `(γ , v₂) ⊢ M ↓ v` -for some value `v₂`. We have `M [ N ] = subst (subst-zero N) M`. +give terms `N : (Γ , ★ ⊢ ★)` and `M : (Γ ⊢ ★)`, +if `γ ⊢ N [ M ] ↓ w`, then `γ ⊢ M ↓ v` and `(γ , v) ⊢ N ↓ w` +for some value `v`. We have `N [ M ] = subst (subst-zero M) N`. We apply the `subst-reflect` lemma to obtain -`γ ⊢ subst-zero N ↓ (δ' , v')` and `(δ' , v') ⊢ M ↓ v` +`γ ⊢ subst-zero M ↓ (δ' , v')` and `(δ' , v') ⊢ N ↓ w` for some `δ'` and `v'`. -Instantiating `γ ⊢ subst-zero N ↓ (δ' , v')` at `k = 0` -gives us `γ ⊢ N ↓ v'`. We choose `v₂ = v'`, so the first +Instantiating `γ ⊢ subst-zero M ↓ (δ' , v')` at `k = 0` +gives us `γ ⊢ M ↓ v'`. We choose `w = v'`, so the first part of our conclusion is complete. -It remains to prove `(γ , v') ⊢ M ↓ v`. First, we obtain -`(γ , v') ⊢ rename var-id M ↓ v` by the `rename-pres` lemma -applied to `(δ' , v') ⊢ M ↓ v`, with the `var-id` renaming, +It remains to prove `(γ , v') ⊢ N ↓ v`. First, we obtain +`(γ , v') ⊢ rename var-id N ↓ v` by the `rename-pres` lemma +applied to `(δ' , v') ⊢ N ↓ v`, with the `var-id` renaming, `γ = (δ' , v')`, and `δ = (γ , v')`. To apply this lemma, we need to show that `nth n (δ' , v') ⊑ nth (var-id n) (γ , v')` for any `n`. This is accomplished by the following lemma, which -makes use of `γ ⊢ subst-zero N ↓ (δ' , v')`. +makes use of `γ ⊢ subst-zero M ↓ (δ' , v')`. \begin{code} -nth-id-le : ∀{Γ}{δ'}{v'}{γ}{N} - → γ `⊢ subst-zero N ↓ (δ' `, v') +nth-id-le : ∀{Γ}{δ'}{v'}{γ}{M} + → γ `⊢ subst-zero M ↓ (δ' `, v') ----------------------------------------------------- → (x : Γ , ★ ∋ ★) → (δ' `, v') x ⊑ (γ `, v') (var-id x) nth-id-le γ-sz-δ'v' Z = Refl⊑ @@ -603,32 +603,32 @@ The above lemma proceeds by induction on `n`. Returning to the proof that single substitution reflects denotations, we have just proved that - (γ `, v') ⊢ rename var-id M ↓ v + (γ `, v') ⊢ rename var-id N ↓ v -but we need to show `(γ `, v') ⊢ M ↓ v`. +but we need to show `(γ `, v') ⊢ N ↓ v`. So we apply the `rename-id` lemma to obtain -`rename var-id M ≡ M`. +`rename var-id N ≡ N`. The following is the formal version of this proof. \begin{code} -subst-zero-reflect : ∀ {Δ} {δ : Env Δ} {γ : Env (Δ , ★)} {N : Δ ⊢ ★} - → δ `⊢ subst-zero N ↓ γ +subst-zero-reflect : ∀ {Δ} {δ : Env Δ} {γ : Env (Δ , ★)} {M : Δ ⊢ ★} + → δ `⊢ subst-zero M ↓ γ ---------------------------------------- - → Σ[ w ∈ Value ] γ `⊑ (δ `, w) × δ ⊢ N ↓ w + → Σ[ w ∈ Value ] γ `⊑ (δ `, w) × δ ⊢ M ↓ w subst-zero-reflect {δ = δ} {γ = γ} δσγ = ⟨ last γ , ⟨ lemma , δσγ Z ⟩ ⟩ where lemma : γ `⊑ (δ `, last γ) lemma Z = Refl⊑ lemma (S x) = var-inv (δσγ (S x)) -substitution-reflect : ∀ {Δ} {δ : Env Δ} {M : Δ , ★ ⊢ ★} {N : Δ ⊢ ★} {v} - → δ ⊢ M [ N ] ↓ v +substitution-reflect : ∀ {Δ} {δ : Env Δ} {N : Δ , ★ ⊢ ★} {M : Δ ⊢ ★} {v} + → δ ⊢ N [ M ] ↓ v ------------------------------------------------ - → Σ[ w ∈ Value ] δ ⊢ N ↓ w × (δ `, w) ⊢ M ↓ v + → Σ[ w ∈ Value ] δ ⊢ M ↓ w × (δ `, w) ⊢ N ↓ v substitution-reflect d with subst-reflect d refl -... | ⟨ γ , ⟨ δσγ , γMv ⟩ ⟩ with subst-zero-reflect δσγ -... | ⟨ w , ⟨ ineq , δNw ⟩ ⟩ = ⟨ w , ⟨ δNw , Env⊑ γMv ineq ⟩ ⟩ +... | ⟨ γ , ⟨ δσγ , γNv ⟩ ⟩ with subst-zero-reflect δσγ +... | ⟨ w , ⟨ ineq , δMw ⟩ ⟩ = ⟨ w , ⟨ δMw , Env⊑ γNv ineq ⟩ ⟩ \end{code} @@ -688,8 +688,9 @@ reduce-equal {Γ}{M}{N} r γ v = ⟨ (λ m → preserve m r) , (λ n → reflect n r refl) ⟩ \end{code} -We conclude that multi-step reduction to a lambda abstraction implies -denotational equivalence to a lambda abstraction. +We conclude with the _soundness property_, that multi-step reduction +to a lambda abstraction implies denotational equivalence with a lambda +abstraction. \begin{code} soundness : ∀{Γ} {M : Γ ⊢ ★} {N : Γ , ★ ⊢ ★}