[Prev][Next][Index][Thread]
Re: Is the PER model fully abstract?

To: pierce@cs.indiana.edu

Subject: Re: Is the PER model fully abstract?

From: Ralph Loader <loader@mc46.merton.ox.ac.uk>

Date: Tue, 11 Mar 1997 08:39:47 GMT

Cc: types@cs.indiana.edu

DeliveryDate: Tue, 11 Mar 1997 03:39:56 0500

InReplyTo: <199703110429.XAA23632@school.cs.indiana.edu>

References: <199703110429.XAA23632@school.cs.indiana.edu>
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.