# Mitchell Foundations for PL 2.3.4 (observational equivalence)

Background.

• The language is PCF, with observable types $$\text{bool}$$ and $$\text{nat}$$.
• $$\text{eval}$$ is the partial function on PCF terms such that $$\text{eval}(M) = N$$ iff $$N$$ is the unique normal form of $$M$$.
• observational equivalence: for all contexts $$C[ ]$$ such that $$C[M]$$ and $$C[N]$$ are closed terms of observable type, we have that $$\text{eval}(C[M]) \simeq \text{eval}(C[N]$$.

Questions.

1. Show that if programs (closed terms of observable type) $$M$$ and $$N$$ are operationally equivalence, $$\text{eval}(M) \simeq \text{eval}(N)$$.
2. Assuming that all programs with no normal form are observationally (aka operationally) equivalent, show that if $$M$$,$$N$$ are programs such that $$\text{eval}(M) \simeq \text{eval}(N)$$, $$M$$ and $$N$$ are observationally equivalent.

Attempts.

1. Suppose that $$M$$, $$N$$ are operationally equivalent and consider the empty context. Pasting in $$M$$, $$N$$ we have that $$\text{eval}(M) \simeq \text{eval}(N)$$ by definition.

2. Let $$C[]$$ be such that $$C[M]$$, $$C[N]$$ are programs. (a) If $$\text{eval}(M)$$ is defined, ie $$M$$ has a normal form $$K$$, then $$N$$ has the same normal form. Non-deterministic reduction is the same as deterministic reduction for \text{eval} function (by his statement on p. 75), hence we choose to reduce the $$M$$ and $$N$$ portions of $$C[M]$$, $$C[N]$$ to $$C[K]$$ first. This leaves us with $$C[M]$$ and $$C[N]$$ both stepping to $$C[K]$$. Then if $$C[K]$$ has a normal form $$Z$$, $$C[M]$$ and $$C[N]$$ both step to $$Z$$ and we are done. Else, $$C[K]$$ has no normal form, and hence neither $$C[M]$$ nor $$C[N]$$ do (for suppose that $$C[M]$$ has a normal form, by confluence, so does $$C[K]$$). (b) given that $$M$$, $$N$$ have no normal forms, $$C[M]$$ and $$C[N]$$ do not have normal forms either.

Problem: I don't think (b) is true: since pcf is Turing-complete, we can write $$Y$$ combinator. We can also write a function $$t:$$ that takes arbitrarily many arguments and returns $$1$$. So $$Y$$ combinator has no nf, but $$C[] = t([])$$ does have a normal form. Is there a better way to go about completeing this problem?

• cross posted at cs.stackexchange.com/questions/165304/… Jan 30 at 5:34
• What does it mean that $\text{eval}(M) \simeq \text{eval}(N)$? Does it mean the following disjunction? Either $\text{eval}$ is defined neither in $M$ nor in $N$, or $\text{eval}$ is defined in both $M$ and $N$ and $\text{eval}(M) = \text{eval}(N)$. Jan 30 at 7:36
• @Taroccoesbrocco yes that’s the exact meaning Jan 30 at 14:06

The proof you wrote for Point 2 correctly distinguishes the two cases, and it is correct in case (a) but not in case (b) exactly because of what you already said. The fact that $$M$$ has no normal form does not imply that $$C[M]$$ has no normal form. Take for instance the fixed point combinator $$Y : (\tau \to \tau) \to \tau$$ (which has no normal form) and $$F = \lambda x^{\sigma \to \sigma}. \lambda y^\sigma. y : (\sigma \to \sigma) \to (\sigma \to \sigma)$$ (which is normal) with $$\tau = \sigma \to \sigma$$. Then, $$YF$$ reduces to $$F(YF)$$ (by definition of fixed point combinator), which in turn reduces to $$F$$ (by definition of $$F$$), which is normal, hence $$YF$$ (that is, $$C[Y]$$ with $$C[] = [\,]F$$) has a normal form.
The proof in case (b) is easy to fix. Remember that case (b) is when $$\text{eval}(M) \simeq \text{eval}(N)$$ because the partial function $$\text{eval}$$ is defined neither in $$M$$ nor in $$N$$, since $$M$$ and $$N$$ have no normal forms. According to the assumptions of Point 2, we already know that $$M$$ and $$N$$ are not observationally equivalent programs. So, there is nothing to do!