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?