3
$\begingroup$

(a) Show that the relation of observational equivalence remains the same when changing the observable types of pcf from nat, bool to nat. (b) Further show that changing from nat,bool to nat, bool, product, where product is the product of two observable types, does not change the relation of observational equivalence.

Terminology: let $=_n, =_p$ represent the equivalence relation whose observable types are nat, and nat, bool, prod resp. let = be the standard equivlanece, ie the one whose observables include nat and bool. The values of pcf are the boolean and natural constants, as well as lambda abstractions.

(a): Given m $=_n$ n. If c[] is such that c[m], c[n] are closed of type nat, we are done by hypothesis. So let c[] be such that c[m], c[n] are closed of type bool. WTS that eval(c[m]) $\simeq$ eval(c[n]). Let d[] be the context formed by "if c[] then 1 else 0". We have that d[m], d[n] are closed of type nat, by hypothesis eval(d[m]) $\simeq$ eval(d[n]). Suppose that d[m] has a normal form, henceforth nf. since closed nf of observable type are values, d[m] must be either 0 or 1. by inversion, c[m] must thus be true or false, hence c[m] has a normal form. Further c[m], c[n] must have the same nf, else d[m], d[n] do not. On the other hand, if d[m] does not have a nf, then c[m] cannot either. for if c[m] has a nf such as true or false, d[m] clearly does by apply reduction rule for conditional. Hence proved.

(b): very similar, but we construct d[] by induction on the depth of the product types. for example, suppose c[m], c[n] are of type (nat x bool) x nat. We can code $\land$ in pcf, so we allow d[] = if $p_1(p_1(c[]))= 0 \land p_1(p_2(c[]) \land p_2(c[])$ then 0 else 1. Then d[m], d[n] have type nat, and we can proceed as in part (a).

Q: doe this seem right? crucially for part a, do we have closed nf of observable type are values? I think so, likely via a progress theorem. Alternatively, is there another way to go about this?

$\endgroup$

1 Answer 1

1
$\begingroup$

In fact, we have something stronger: closed nf of observable type are either numerals or boolean constants.

Pf: We can induct on the typing derivation. The base cases for the numbers and booleans are clearly true. Suppose we have $H \vdash eq? (x) (y) : bool$, and $eq (x) (y)$ is a closed nf of type bool. In particular, no reduction rule can apply to x or y, by inversion and then inductive hypothesis this means that x, y are numerals. But then we have that $eq (x)(y)$ steps to true or false, ie is not in nf. Here is another case: Suppose $H \vdash M(N): t$ is closed of ground type. By inversion, M is of function type, ie a lambda term, and hence beta-reduction applies so that M(N) is not in nf. On the other hand, our term cannot be a fix term since fix terms can always be reduced. The other cases are similar.

$\endgroup$

You must log in to answer this question.

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