[Prev][Next][Index][Thread]

Re: Is the PER model fully abstract?

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.

Ralph.