michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

more edits

Browse source
This commit is contained in:
Jeremy Siek 2020-04-09 09:18:30 -04:00
parent 2afe5706a1
commit 433587bc61
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/plfa/part3/ContextualEquivalence.lagda.md
View file

@ -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.Denotational using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_)
open import plfa.part3.Compositional using (Ctx; plug; compositionality) open import plfa.part3.Compositional using (Ctx; plug; compositionality)
open import plfa.part3.Soundness using (soundness) open import plfa.part3.Soundness using (soundness)
open import plfa.part3.Adequacy using (adequacy) open import plfa.part3.Adequacy using (↓→⇓)
``` ```
## Contextual Equivalence ## 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≃ℰƛN′ = soundness CM—↠ƛN′ in
let ℰCM≃ℰCN = compositionality{Γ = Γ}{Δ = ∅}{C = C} ℰM≃ℰN in let ℰCM≃ℰCN = compositionality{Γ = Γ}{Δ = ∅}{C = C} ℰM≃ℰN in
let ℰCN≃ℰƛN′ = ≃-trans (≃-sym ℰCM≃ℰCN) ℰCM≃ℰƛ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′)`, 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′). ℰ (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′′) δ). ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ).