# Unification of expressions involving sets

Let's let $\def\OP#1#2{\left\langle#1,#2\right\rangle}\OP xy$ represent the set $\{\{x\},\{x,y\}\}$ as is usual, per Kuratowski. Then:

$$\begin{eqnarray} \OP{\OP ab}c & = & \{\{\{\{a\}, \{a,b\}\}\}, \{\{\{a\}, \{a, b\}\}, c\}\} \\ \OP x{\OP yz} & = & \{\{x\}, \{x, \{\{y\}, \{y,z\}\}\}\} \end{eqnarray}$$

I would like to unify these two equations to produce a set of relations on $a,b,c,x,y,z$ that give the most general conditions for which $\OP{\OP ab}c = \OP x{\OP yz}$.

The unification algorithm I know works on expressions. Applying it to $\OP{\OP ab}c = \OP x{\OP yz}$ directly gives $x=\OP ab, c=\OP yz$. This is correct, but may not be the most general possible set of conditions.

I can also abbreviate $\{x\}$ as $Sx$ and $\{y,z\}$ as $Dxy$, so that $\OP xy = \{\{x\}, \{x, y\}\} = DSxDxy$. Then the two set expressions I want to unify become $DSDSaDabDDSaDabc$ and $DSxDxDSyDyz$. I can unify these; the result is the same as in the previous paragraph.

But this may not be fully general, because it fails to capture the fact that for sets, $\{a, a\} = \{a\}$. Abbreviating $\{x\}$ as $Sx$ and $\{y,z\}$ as $Dxy$, and attempting to unify $\{x\}$ and $\{y, z\}$ with this method fails outright. But I want it to succeed and to yield the equations $x=y, x=z$.

How can I fix either the unification algorithm or my representation of the expressions to allow $\{x\}$ to unify with $\{y, z\}$?

I can make some progress on this particular problem by representing $\{x\}$ as $Dxx$. Then $\{x\}$ unifies with $\{y,z\}$ because $Dxx$ unifies with $Dyz$ giving $x=y, x=z$ as I wanted.

But this is not quite enough either, because it doesn't understand that $\{x, y\} = \{y, x\}$. I want the unification of $\{x, y\}$ with $\{a, b\}$ to give me not simply $x=a, y=b$ but $[x=a, y=b] \lor [x=b, y=a]$.

The problem grows worse if any of the sets have more than two elements. There are several possible ways in which $\{x, y\}$ could unify with $\{a,b,c\}$. For example, we might have $x=a=c, y=b$, or $x=c, y=a=b$.

Is there a modified version of the unification algorithm that can handle unification of sets in this way?

-

When the ordered pair $\langle x, y \rangle$ is defined as the set $\{\{x\}, \{x, y\}\}$, your original unification algorithm is correct and gives the most general conditions for equality; the fact that $\{ x ,x \}=\{x\}$ is already accounted for.
In particular, $\langle x, y \rangle$ always contains exactly one singleton element, $\{ x \}$, containing the first half of the ordered pair. If it contains a second element, that element is $\{x, y\}$ (with $x\neq y$), from which the second half of the pair can be read off (since we already know the first half). If it does not contain a second element, then the second half of the ordered pair is the same as the first. Since the first and second halves of each ordered pair can be deduced from its corresponding set, $\langle a, b \rangle = \langle c, d \rangle$ if and only if $a=b$ and $c=d$.
I understand. Thanks. ${}{}$ –  MJD Jul 8 '12 at 1:38