[TYPES] logical relations and ctx equivalence

[Dimitrios Vytiniotis]

Dear TYPES readers,

    Consider the simplest syntactic relational interpretation of
System-F types as sets of pairs of closed values.  Quantification is
over arbitrary value relations. The semantics is call by value and
terminating. [Definitions can be found at the end of this message]

First, I think it is an easy corollary of the fundamental theorem that
the logical relation is contained in ctx equivalence (I am using
ground equivalence, actually), i.e. that:

Proposition: If (e1,e2) in (interp[t] nil nil)
              then forall contexts C : t -> Int,
              C[e1] and C[e2] evaluate to the same literal.

What I am asking is whether we know that it is complete:

Question: If forall C : t -> Int,
              C[e1] and C[e2] evaluate to the same literal
           then (e1,e2) in (interp[t] nil nil).

It seems that an important step towards completeness is showing that
the logical relation is an equivalence-respecting one. Then, for
example, Pitts' work [ATTAPL clapter] uses TT-closures, and Harper &
Birkedal's paper [Relational interpetation for recursive types in an
Operational Setting] builds the logical relation between equivalence
classes of expressions alltogether (and does not handle polymorphism,
but this probably does not matter). Are all these constructions
necessary? Is there a negative result or an easy counterexample that
the plain-old definition does not give a big enough relation, or do we
not have a direct proof method, or do we not know? Any pointers to
related work would be very useful.

Thank you,
--Dimitrios Vytiniotis


Informal Definitions
=====================

Types:   t ::= a | t -> t | Int | forall a.t
Terms:   e ::= x | \(x:t).e | e e | e [t] | int_literal

Type envs:  m : TyVar -> (Value,Value)
             d : TyVar -> (Type,Type)
	    d1(a) = fst (d(a))
             d2(a) = snd (d(a))

VRel(t1,t2) = set of relations between pairs of
               closed values of types t1 and t2

interp[a] m d  = m(a)
interp[Int] m d = identity on integer literals
interp[t1->t2] m d =
    { (v1,v2) | v1 : d1(t1->t2) and
                v2 : d2(t1->t2) and
      forall x1 x2. (x1,x2) in (interp[t1] m d) =>
       (v1 x1, v2 x2) evaluate to (w1,w2) in (interp[t2] m d) }
interp[forall a.t] m d =
    { (v1,v2) | v1: d1(forall a.t) and
                v2: d2(forall a.t) and
      forall t1 t2 r. r in VRel(t1,t2) =>
       (v1 [t1], v2 [t2]) evaluate to (w1,w2)
                            in (interp[t] (m,a->r) (d,a->(t1,t2)))}