Re: Is the PER model fully abstract?
Subject: Re: Is the PER model fully abstract?
From: Ralph Loader <firstname.lastname@example.org>
Date: Tue, 11 Mar 1997 08:39:47 GMT
Delivery-Date: Tue, 11 Mar 1997 03:39:56 -0500
Benjamin Pierce writes:
>equivalent. The converse property, i.e. full abstraction, is probably
>not valid. On the other hand, we have not been able to construct an
>explicit counterexample. Does someone know one? (I.e., can someone
My paper "Equational Theories for Inductive Types"
(http://mc46.merton.ox.ac.uk/~loader/) provides an answer for a lambda
calculus with (strictly positive) inductive types. (This is all specific
to the PER given by Kleene application on the natural numbers). I don't
know of much else in this vein; the question for F seems difficult.
>In a similar vein, we have tried to rephrase some arguments that are
>usually performed using parametricity by arguing directly from the PER
>model. For example, here is an exercise: Suppose that s is in the
>domain of the PER
There is a paper "Algebraic Types in PER models" by Hyland, Robinson and
Rosolini that does some things like this.