<p>I don't know about the field of semantics, but the concept you mention is crucial in the complexity of counting.</p>

<p>I have not seen a relation $R$ called a <em>difunctional relation</em> before, but it is equivalent to $R$ having some Mal'tsev operation as a polymorphism, a concept from <a href="http://en.wikipedia.org/wiki/Universal_algebra" rel="nofollow">universal algebra</a>. An operation $m$ is a Mal'tsev operation if $m(x,y,y) = m(y,y,x) = x$ for all $x$ and $y$.</p>

<p>The complexity of counting constraint satisfaction problems for a set of weighted constraints $\mathcal{F}$ is #P-complete unless the unweighted versions of the constraints in $\mathcal{F}$ all have a Mal'tsev polymorphism (<a href="http://arxiv.org/abs/1111.2384" rel="nofollow">Cai, Chen</a>). For the unweighted version, this property is also sufficient for tractability (<a href="http://www.sciencedirect.com/science/article/pii/S089054010600109X" rel="nofollow">Bulatov, Dalmau</a>).</p>

<p>It is also <a href="http://rads.stackoverflow.com/amzn/click/1584882549" rel="nofollow">known</a> that a set of relations $\Gamma$ has a Mal'tesv polymorphism iff $\Gamma$ is congruence permutable, another definition from universal algebra. In order to simplify the Bulatov-Dalmau proof by removing much the dependence with deep results from universal algebra, <a href="http://dl.acm.org/citation.cfm?id=1806789" rel="nofollow">Dyer and Richerby</a> further show that $\Gamma$ has a Mal'tsev polymorphism iff $\Gamma$ is (strongly) rectangular (a definition that is new to their paper) and use this to give an "elementary" proof of the same result.</p>

CC BY-SA 3.0
2014-11-14T15:40:59.993Z
More precisely, the concept is equivalent to having a Mal'tsev polymorphism for binary relations, but having a Mal'tsev polymorphism naturally can be applied to any arity whereas this formulation is specific to binary relations.  Also, just to emphasise: this doesn't just apply to counting, but to any algebraic study of classes of relations.  For instance, Mal'tsev polymorphisms are crucial in the study of tractable constraint languages (which are classes of relations) even in the absence of counting considerations.
András Salamon
CC BY-SA 3.0
2014-11-14T16:16:20.683Z
@AndrásSalamon My answer is about ternary relations, not binary ones. How do you define a Mal'tsev polymorphism for relations other than ternary?
Tyson Williams
CC BY-SA 3.0
2014-11-14T16:23:00.980Z
A polymorphism is applied componentwise.  The arity of the tuples does not matter.
András Salamon
CC BY-SA 3.0
2014-11-14T19:16:02.633Z
@AndrásSalamon Of course the definition of a polymorphism exists for every arity. You said that "a Mal'tsev polymorphism naturally can be applied to any arity". I am asking you: what is the definition of a Mal'tsev polymorphism for relations of arity $k \ne 3$?
Tyson Williams
CC BY-SA 3.0
2014-11-17T13:12:26.197Z
I'm not sure what you are objecting to, but I said that "_having_ a Mal'tsev polymorphism" can be applied to any arity.
András Salamon
CC BY-SA 3.0
2014-11-17T14:47:01.147Z
@AndrásSalamon Oh, I see.  I thought you were saying that the Mal'sev property, which I expressed using a ternary function, can be extended/generalized to functions of other arties.
Tyson Williams
CC BY-SA 3.0
2015-04-18T17:36:20.703Z
A Maltsev variety can be (equivalently) characterized as a variety in which any homomorphic relation is difunctional. This is a pretty old result of Lambek (IIRC), but it's nicely presented in a more recent paper of his titled ["The Butterfly and The Serpent"](https://books.google.com/books?id=T2ekTUiuqxMC&pg=PA161).
got trolled too much this week
CC BY-SA 3.0
2012-07-04T16:01:10.197Z
2014-11-14T15:35:24.160Z
2014-11-14T15:35:24.160Z
Tyson Williams
<p>Makoto Takeyama and I sent the following to data-refinement@etl.go.jp on Jan 5, 1996:</p>

<blockquote>
  <p>Subject: what is a data refinement relation?</p>
  
  <p>Dear all:  anyone still interested in data refinement?</p>
  
  <p>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.</p>
  
  <p>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.</p>
  
  <p>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).</p>
  
  <p>Proposition. If R and S are zig-zag complete relations, so
   are R x S and R -> S.  </p>
  
  <p>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:</p>
  
  <p>for all u_i in V_i[[pi]],<br>
      R^{pi}(...,u_i,...) implies that, for all i, V_i[[t]]u_i ~ V_i[[t']]u_i</p>
  
  <p>this interpretation satisfies the usual axioms and rules
   for equational logic.</p>
  
  <p>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.</p>
  
  <p>Questions:</p>
  
  <ol>
  <li><p>Has anyone seen this kind of structure before?</p></li>
  <li><p>What are the natural generalizations of these ideas to 
    other propositions and "arbitrary" semantic categories? </p></li>
  </ol>
  
  <p>Bob Tennent
  rdt@cs.queensu.ca</p>
</blockquote>

CC BY-SA 3.0
2014-11-13T21:45:54.667Z
2015-02-04T16:37:45.007Z
2015-02-04T16:37:45.007Z
Bob Tennent
<p>Given sets $A$ and $B$, a <em>difunctional relation</em> $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property:</p>

<blockquote>
  <p>If $a \sim b$ and $a' \sim b'$ and $a \sim b'$, then $a' \sim b$.  </p>
</blockquote>

<p>Difunctional relations are a generalization of the concept of <a href="http://en.wikipedia.org/wiki/Partial_equivalence_relation" rel="noreferrer">partial equivalence relations</a> which permit one to define a notion of equality from <em>different</em> 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:<img src="https://i.sstatic.net/o4Xdi.png" alt="picture of a zigzag"></p>

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

<ol>
<li>Martin Hoffman uses them in <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.154.7893&amp;rep=rep1&amp;type=pdf" rel="noreferrer"><em>Correctness of Effect-Based Program Transformations</em></a>.</li>
<li>I have seen mentions (but no good references) claiming that Tennant and Takeyama have proposed their use as well. </li>
</ol>

<p>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.  </p>

CC BY-SA 3.0
2012-07-03T16:49:19.307Z
Johan van Benthem used the term zig-zag relations in his dissertation for a different notion similar to bisimulation.
Vijay D
CC BY-SA 3.0
2017-06-12T23:46:21.073Z
Those who wonder how Neel used QPERs (like me) might want to look at "Internalizing Relational Parametricity in the Extensional Calculus of Constructions" from him and Dreyer.
Blaisorblade
<reference-request><pl.programming-languages><denotational-semantics><logical-relations>
Uses of quasi-PERs/difunctional relations/zig-zag relations?
Neel Krishnaswami
# Uses of quasi-PERs/difunctional relations/zig-zag relations?

(Asked by: username_0 on 2012-07-03)

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](http://en.wikipedia.org/wiki/Partial_equivalence_relation) 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:![picture of a zigzag](https://i.sstatic.net/o4Xdi.png)

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

1. Martin Hoffman uses them in [*Correctness of Effect-Based Program Transformations*](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.154.7893&rep=rep1&type=pdf).
2. 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.

**Tags:** reference-request, pl.programming-languages, denotational-semantics, logical-relations
> **Comments:**
> **username_1**: Johan van Benthem used the term zig-zag relations in his dissertation for a different notion similar to bisimulation.  
> **username_2**: Those who wonder how Neel used QPERs (like me) might want to look at "Internalizing Relational Parametricity in the Extensional Calculus of Constructions" from him and Dreyer.  

---

## 2 answers

### Answer by username_6 on 2014-11-13. Score: 9 | Accepted answer

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) & 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:
>
> 1. Has anyone seen this kind of structure before?
> 2. What are the natural generalizations of these ideas to
>    other propositions and "arbitrary" semantic categories?
>
> Bob Tennent
> rdt@cs.queensu.ca


---

### Answer by username_3 on 2012-07-04. Score: 7

I don't know about the field of semantics, but the concept you mention is crucial in the complexity of counting.

I have not seen a relation $R$ called a *difunctional relation* before, but it is equivalent to $R$ having some Mal'tsev operation as a polymorphism, a concept from [universal algebra](http://en.wikipedia.org/wiki/Universal_algebra). An operation $m$ is a Mal'tsev operation if $m(x,y,y) = m(y,y,x) = x$ for all $x$ and $y$.

The complexity of counting constraint satisfaction problems for a set of weighted constraints $\mathcal{F}$ is #P-complete unless the unweighted versions of the constraints in $\mathcal{F}$ all have a Mal'tsev polymorphism ([Cai, Chen](http://arxiv.org/abs/1111.2384)). For the unweighted version, this property is also sufficient for tractability ([Bulatov, Dalmau](http://www.sciencedirect.com/science/article/pii/S089054010600109X)).

It is also [known](http://rads.stackoverflow.com/amzn/click/1584882549) that a set of relations $\Gamma$ has a Mal'tesv polymorphism iff $\Gamma$ is congruence permutable, another definition from universal algebra. In order to simplify the Bulatov-Dalmau proof by removing much the dependence with deep results from universal algebra, [Dyer and Richerby](http://dl.acm.org/citation.cfm?id=1806789) further show that $\Gamma$ has a Mal'tsev polymorphism iff $\Gamma$ is (strongly) rectangular (a definition that is new to their paper) and use this to give an "elementary" proof of the same result.

> **Comments:**
> **username_4**: More precisely, the concept is equivalent to having a Mal'tsev polymorphism for binary relations, but having a Mal'tsev polymorphism naturally can be applied to any arity whereas this formulation is specific to binary relations.  Also, just to emphasise: this doesn't just apply to counting, but to any algebraic study of classes of relations.  For instance, Mal'tsev polymorphisms are crucial in the study of tractable constraint languages (which are classes of relations) even in the absence of counting considerations.  
> **username_3**: @AndrásSalamon My answer is about ternary relations, not binary ones. How do you define a Mal'tsev polymorphism for relations other than ternary?  
> **username_4**: A polymorphism is applied componentwise.  The arity of the tuples does not matter.  
> **username_3**: @AndrásSalamon Of course the definition of a polymorphism exists for every arity. You said that "a Mal'tsev polymorphism naturally can be applied to any arity". I am asking you: what is the definition of a Mal'tsev polymorphism for relations of arity $k \ne 3$?  
> **username_4**: I'm not sure what you are objecting to, but I said that "_having_ a Mal'tsev polymorphism" can be applied to any arity.  
> **username_3**: @AndrásSalamon Oh, I see.  I thought you were saying that the Mal'sev property, which I expressed using a ternary function, can be extended/generalized to functions of other arties.  
> **username_5**: A Maltsev variety can be (equivalently) characterized as a variety in which any homomorphic relation is difunctional. This is a pretty old result of Lambek (IIRC), but it's nicely presented in a more recent paper of his titled ["The Butterfly and The Serpent"](https://books.google.com/books?id=T2ekTUiuqxMC&pg=PA161).  

---

