Uses of quasi-PERs/difunctional relations/zig-zag relations?
Makoto Takeyama and I sent the following to data-refinement@etl.go.jp on Jan 5, 1996:


  Subject: what is a data refinement relation?
  
  Dear all:  anyone still interested in data refinement?
  
  Recently Mak and I have been looking again at an idea we considered
   many months ago.  The motivation is to characterize
   the logical relations relevant to showing data refinement.
   This was stimulated by the realization that logical relations can
   be used to show "safety" of abstract interpretations
   (see Section 2.8 of the chapter by Jones and Nielson in
   volume 4 of the Handbook of Logic in CS), but such relations
   are more general than those used to show data refinement.
  
  My reasoning goes as follows.  If a relation R is establishing a data
   refinement between (among) sets, then it must be inducing 
   (partial) equivalence relations on each of the sets, with 
   these equivalence classes in one-to-one correspondence,
   and every element of an equivalence class must be related
   to all elements of the corresponding equivalence classes in
   the other domains of interpretation.  The idea is that each 
   equivalence class represents an "abstract" value; in a fully
   abstract interpretation the equivalence classes are singletons.
  
  We can give a simple condition to ensure that an n-ary relation R induces 
   this structure.  Define v ~ v' in domain V iff there exists a value
   x in some other domain X (and arbitrary values ... in the
   other domains) such that R(...,v,...,x,...) and R(...,v',...,x,...).
   This defines symmetric relations on each of the domains.  Imposing
   local transitivity would then give us pers on each domain, but
   this would not suffice because we want to ensure transitivity
   across interpretations.  The following condition achieves this:
   if v_i ~ v'_i for all i, then R(...,v_i,...) iff R(...,v'_i,...)
   I call this "zig-zag completeness"; in the case n=2, it says
   that if R(a,c) &amp; R(a',c') then R(a,c') iff R(a',c).
  
  Proposition. If R and S are zig-zag complete relations, so
   are R x S and R -> S.  
  
  Proposition.  Suppose t and t' are terms of type th in context pi,
   and R is a zig-zag complete logical relation; 
   then, if the equivalence judgement t=t' is interpreted as follows:
  
  for all u_i in V_i[[pi]],
      R^{pi}(...,u_i,...) implies that, for all i, V_i[[t]]u_i ~ V_i[[t']]u_i
  
  this interpretation satisfies the usual axioms and rules
   for equational logic.
  
  The intuition here is that the terms are to be "equivalent" both
    within a single interpretation (V_i) and across interepretations;
    i.e., the meanings of t and t' are in the same R-induced 
    equivalence class, no matter which interpretation is used.
  
  Questions:
  
  
  Has anyone seen this kind of structure before?
  What are the natural generalizations of these ideas to 
    other propositions and "arbitrary" semantic categories? 
  
  
  Bob Tennent
  rdt@cs.queensu.ca