Uses of quasi-PERs/difunctional relations/zig-zag relations? Given sets $A$ and $B$, a difunctional relation $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property:


  If $a \sim b$ and $a' \sim b'$ and $a \sim b'$, then $a' \sim b$.  


Difunctional relations are a generalization of the concept of partial equivalence relations which permit one to define a notion of equality from different sets. As a result, they are also known as quasi-PERs (QPERs), and they are also known as zig-zag relations, due to the following picture:

I'm writing a paper that uses them, but I've had trouble tracking down good references for their use in semantics. 


Martin Hoffman uses them in Correctness of Effect-Based Program Transformations.
I have seen mentions (but no good references) claiming that Tennant and Takeyama have proposed their use as well. 


They are such a pretty idea that I have trouble believing my particular use of them is original. I would really appreciate any further references.
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