15
$\begingroup$

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:picture of a zigzag

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

$\endgroup$
  • $\begingroup$ Johan van Benthem used the term zig-zag relations in his dissertation for a different notion similar to bisimulation. $\endgroup$ – Vijay D Jul 3 '12 at 16:49
  • $\begingroup$ 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. $\endgroup$ – Blaisorblade Jun 12 '17 at 23:46
8
$\begingroup$

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

$\endgroup$
6
$\begingroup$

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. 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). For the unweighted version, this property is also sufficient for tractability (Bulatov, Dalmau).

It is also known 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 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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – András Salamon Nov 14 '14 at 15:40
  • $\begingroup$ @AndrásSalamon My answer is about ternary relations, not binary ones. How do you define a Mal'tsev polymorphism for relations other than ternary? $\endgroup$ – Tyson Williams Nov 14 '14 at 16:16
  • $\begingroup$ A polymorphism is applied componentwise. The arity of the tuples does not matter. $\endgroup$ – András Salamon Nov 14 '14 at 16:23
  • $\begingroup$ @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$? $\endgroup$ – Tyson Williams Nov 14 '14 at 19:16
  • $\begingroup$ I'm not sure what you are objecting to, but I said that "having a Mal'tsev polymorphism" can be applied to any arity. $\endgroup$ – András Salamon Nov 17 '14 at 13:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.