[Prev][Next][Index][Thread]
Is the PER model fully abstract?
Consider System F with a distinguished base type B of Booleans and two
constants tt,ff of type B. Define observational equivalence between
two closed terms s,t of type A as C(s) = C(t) for all closed terms C
of type A->Bool. The well-known PER interpretation of System F
interprets types as partial equivalence relations on the natural
numbers, universal quantification as intersection, and B as (for
example) the PER {(0,0),(1,1)}.
This model is easily seen to be computationally adequate, in the sense
that [[s]] = [[t]] implies that s and t are observationally
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
name two closed terms of some type A that are observationally
equivalent yet receive different interpretations in the PER model?)
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
H = [[ All(X) (X->U) -> X -> V ]].
Show that
s H (\t. \x (s (\y.y) (t x))).
In other words, show that s can use its arguments only by applying the
first to the second and then further processing the result.
What we don't know is whether a similar characterization can be given
in the case of the PER
H' = [[ All(X) (X->U) -> (X->X) -> X -> V ]].
Is there some general theorem that allows arguments using
parametricity to be transferred to the PER model in some cases?
Martin Hofmann and Benjamin Pierce