<p>Got the answer, thanks to jonsterling on reddit for the insight. </p>

<p>The error is that both <code>M</code> and <code>N</code> written as full judgements, must be weakened to have the same environment, and one that fits <code>C[-]</code>. So the question becomes whether  <code>⟦M⟧ = ⟦x,y ⊢ x⟧</code> and <code>⟦N⟧ = ⟦x,y ⊢ y⟧</code> are observationally equivalent.  And the contradiction above disappears. </p>

CC BY-SA 3.0
2016-04-08T22:52:30.103Z
2016-04-08T22:52:30.103Z
Adribar
<p>The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms. </p>

<p>Lets consider the simple case where  the terms <code>M</code> and <code>N</code> are free variables, <code>M = x</code> and <code>N = y</code>. Choosing the program context <code>C[-] = (λxy.[-]) v w</code> we have,<br>
<code>C[M] = (λxy.x) v w →* v</code><br>
<code>C[N] = (λxy.y) v w →* w</code><br>
So by definition <code>M</code> and <code>N</code> wouldn't be observationally equivalent.        </p>

<p>However, consider any <em>adequate</em> denotational semantics of PCF. Then by definition of adequacy, <code>⟦M⟧ = ⟦N⟧</code> implies <code>M</code> and <code>N</code> observationally equivalent. The denotations of both (open) terms are,<br>
<code>⟦M⟧ = ⟦x ⊢ x⟧ = id</code><br>
<code>⟦N⟧ = ⟦y ⊢ y⟧ = id</code><br>
From what we conclude <code>M</code> and <code>N</code>  to be observationally equivalent. </p>

<p>So, surely I must be going wrong somewhere, and I suspect it to be some trivial mistake. But where?</p>

<pl.programming-languages><functional-programming><semantics><denotational-semantics><typed-lambda-calculus>
Observational Equivalence of open terms in PCF
Adribar
# Observational Equivalence of open terms in PCF

(Asked by: username_0 on 2016-04-08)

The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms.

Lets consider the simple case where the terms `M` and `N` are free variables, `M = x` and `N = y`. Choosing the program context `C[-] = (λxy.[-]) v w` we have,  
`C[M] = (λxy.x) v w →* v`  
`C[N] = (λxy.y) v w →* w`  
So by definition `M` and `N` wouldn't be observationally equivalent.

However, consider any *adequate* denotational semantics of PCF. Then by definition of adequacy, `⟦M⟧ = ⟦N⟧` implies `M` and `N` observationally equivalent. The denotations of both (open) terms are,  
`⟦M⟧ = ⟦x ⊢ x⟧ = id`  
`⟦N⟧ = ⟦y ⊢ y⟧ = id`  
From what we conclude `M` and `N` to be observationally equivalent.

So, surely I must be going wrong somewhere, and I suspect it to be some trivial mistake. But where?

**Tags:** pl.programming-languages, functional-programming, semantics, denotational-semantics, typed-lambda-calculus

---

## 1 answers

### Answer by username_0 on 2016-04-08. Score: 2

Got the answer, thanks to jonsterling on reddit for the insight.

The error is that both `M` and `N` written as full judgements, must be weakened to have the same environment, and one that fits `C[-]`. So the question becomes whether `⟦M⟧ = ⟦x,y ⊢ x⟧` and `⟦N⟧ = ⟦x,y ⊢ y⟧` are observationally equivalent. And the contradiction above disappears.


---

