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?


1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy