2
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ cross posted at cs.stackexchange.com/questions/165304/… $\endgroup$
    – emesupap
    Jan 30 at 5:34
  • 1
    $\begingroup$ 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)$. $\endgroup$ Jan 30 at 7:36
  • $\begingroup$ @Taroccoesbrocco yes that’s the exact meaning $\endgroup$
    – emesupap
    Jan 30 at 14:06

1 Answer 1

2
$\begingroup$

The proof you wrote for Point 1 is perfect.

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!

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .