# ContextualEquivalence: Denotational equality implies contextual equivalence 🚧

module plfa.part3.ContextualEquivalence where

## Imports

open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import plfa.part2.Untyped using (_⊢_; ★; ∅; _,_; ƛ_; _—↠_) 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 (↓→⇓)

## Contextual Equivalence

The notion of *contextual equivalence* is an important one for
programming languages because it is the sufficient condition for
changing a subterm of a program while maintaining the program’s
overall behavior. Two terms `M`

and `N`

are contextually equivalent
if they can plugged into any context `C`

and produce equivalent
results. As discuss in the Denotational chapter, the result of
a program in the lambda calculus is to terminate or not.
We characterize termination with the reduction semantics as follows.

terminates : ∀{Γ} → (M : Γ ⊢ ★) → Set terminates {Γ} M = Σ[ N ∈ (Γ , ★ ⊢ ★) ] (M —↠ ƛ N)

So two terms are contextually equivalent if plugging them into the same context produces two programs that either terminate or diverge together.

_≅_ : ∀{Γ} → (M N : Γ ⊢ ★) → Set (_≅_ {Γ} M N) = ∀ {C : Ctx Γ ∅} → (terminates (plug C M)) iff (terminates (plug C N))

The contextual equivalence of two terms is difficult to prove directly
based on the above definition because of the universal quantification
of the context `C`

. One of the main motivations for developing
denotational semantics is to have an alternative way to prove
contextual equivalence that instead only requires reasoning about the
two terms.

## Denotational equivalence implies contextual equivalence

Thankfully, the proof that denotational equality implies contextual equivalence is an easy corollary of the results that we have already established. Furthermore, the two directions of the if-and-only-if are symmetric, so we can prove one lemma and then use it twice in the theorem.

The lemma states that if `M`

and `N`

are denotationally equal
and if `M`

plugged into `C`

terminates, then so does
`N`

plugged into `C`

.

denot-equal-terminates : ∀{Γ} {M N : Γ ⊢ ★} {C : Ctx Γ ∅} → ℰ M ≃ ℰ N → terminates (plug C M) ----------------------------------- → terminates (plug C N) 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₂ (↓→⇓ ℰCN≃ℰƛN′))))

The proof is direct. Because `plug C —↠ plug C (ƛN′)`

,
we can apply soundness to obtain

```
ℰ (plug C M) ≃ ℰ (ƛN′)
```

From `ℰ M ≃ ℰ N`

, compositionality gives us

```
ℰ (plug C M) ≃ ℰ (plug C N).
```

Putting these two facts together gives us

```
ℰ (plug C N) ≃ ℰ (ƛN′).
```

We then apply `↓→⇓`

from Chapter Adequacy to deduce

```
∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ).
```

Call-by-name evaluation implies reduction to a lambda abstraction, so we conclude that

```
terminates (plug C N).
```

The main theorem follows by two applications of the lemma.

denot-equal-contex-equal : ∀{Γ} {M N : Γ ⊢ ★} → ℰ M ≃ ℰ N --------- → M ≅ N denot-equal-contex-equal{Γ}{M}{N} eq {C} = ⟨ (λ tm → denot-equal-terminates eq tm) , (λ tn → denot-equal-terminates (≃-sym eq) tn) ⟩

## Unicode

This chapter uses the following unicode:

```
≅ U+2245 APPROXIMATELY EQUAL TO (\~= or \cong)
```