Determining if lattice elements are equal

Question

I am working in a distributive lattice with top and bottom elements.

I would like to know if there is an algorithm to determine if $s=t$ for any two elements $s,t$ in the lattice. For example, if $t=s\cap s$, then clearly $s=t$.

Essentially, I am asking for an algorithm that, given an input of two strings in the language of a distributive lattice (say with n generators $e_i,\dots,e_n$) determine if those two strings are equal in the actual lattice.

For example, we can consider the strings $e_1\cap(e_2\cup e_2)$ and $e_1\cap e_2$. Those strings are not syntactically equal as strings. I would like an algorithm that will determine if they are yet equal when interpreted in a free distributive lattice, when $e_i$ is interpreted as the i-th generator, $\cap$ is interpreted as meet, and $\cup$ is interpreted as join.

I am fairly confident that this problem is decidable. Also, I am kindly requesting any references on the subject.

Answer 1

Let $E$ be the set of generators. Given a string $s$, using the distributivity (and the axioms of meet and join) we can derive the normal form, a join of meets $M_1 \cup M_2 \cup \ldots M_n$ (each $M_i$ is of the form $e_{i_1} \cap e_{i_2} \ldots \cap e_{i_m}$).
Since the join and meet operations are associative and commutative, we can think of this join of meets as a set of subsets of $E$, $N(s) = \{N_1, N_2 \ldots N_n\}$. Now, to make this representation unique, we should remove duplicates (because of idempotence) and sets $N_i$, which are contained in some $N_k$, since they are redundant (removing them does not change the final element of the lattice).

This gives us a way to check if two strings represent the same element of the free distributive lattice. All we need to do is to obtain the sets $N(s_1)$ and $N(s_2)$ using this procedure and check if they are equal.

A simpler answer could go like this: we can define the free distributive lattice on a set of all finite irredundant sets of finite subsets of $E$, and to check if two strings are equal when interpreted as elements of this free distributive lattice one must simply check if they represent the same irredundant set of subsets of $E$, as described here.

Answer 2

Distributive lattice $(L, \leq)$ with top and bottom element has enough in common with boolean algebra to use some algorithms developed for logic. In particular conversion to CNF when initial formula is built only with $\cup$ and $\cap$ can be done without stepping out of the lattice in the process, just by using distributive property absorption and idempotence. Once you convert strings to CNF, and make sure you can't simplify them anymore, you can easily compare all clauses to check if they form the same sets.

---

Edit: I just realized that CNF may not be unique for given formula; but you can use canonical version to ensure uniqueness.

Answer 3

You could use a "proof search" type of approach. Let us say $p_1, p_2, \ldots, p_n \models q$ for formulas $p_1, \ldots, p_n, q$ in the language of lattices if for each distributive lattice and each assignment of elements of that lattice to the atoms of the expressions, we have $p_1 \wedge \cdots \wedge p_n \le q$. Then the usual formal proof rules of ${\wedge}E$, ${\wedge}I$, ${\vee}E$, ${\vee}I$, ${\bot}E$, ${\top}I$, cut, and assumption are all sound for the theory of distributive lattices (where distributivity is used in showing ${\vee}E$ is sound); so if you can find proofs in this system of $p \vdash q$ and $q \vdash p$, then by the soundness that implies $p \models q$ and $q \models p$, so by antisymmetry $p$ and $q$ must have equal interpretations in any lattice for any assignment of values to atomic variables.

Completeness would be a bit trickier to show. One possible argument would be: if $p \models q$, then in particular that would imply $p \le q$ in the free Heyting algebra over the atoms of $p$ and $q$. Therefore, there must be a formal proof $p \vdash q$ in intuitionistic propositional logic. By the cut elimination theorem, there then must be a cut-free sequent calculus proof of $p \vdash q$. But with $p$ and $q$ not containing any implications, that implies that this cut-free sequent calculus proof can use only the rules listed above (and in fact also cannot use the cut rule, obviously).

For example, to show that $e_1 \wedge (e_2 \vee e_2) \vdash e_1 \wedge e_2$: first, by ${\wedge}E$ this reduces to showing $e_1, e_2 \vee e_2 \vdash e_1 \wedge e_2$. Then, by ${\vee} E$ this reduces to showing that both $e_1, e_2 \vdash e_1 \wedge e_2$ and $e_1, e_2 \vdash e_1 \wedge e_2$. In these two (identical) subproofs, the result follows by ${\wedge}I$ to reduce to showing that both $e_1, e_2 \vdash e_1$ and $e_1, e_2 \vdash e_2$, and in both cases, you can now use the assumption rule.

For the reverse $e_1 \wedge e_2 \vdash e_1 \wedge (e_2 \vee e_2)$: first, use ${\wedge}E$ to reduce to showing $e_1, e_2 \vdash e_1 \wedge (e_2 \vee e_2)$. By ${\wedge}I$, it suffices to show $e_1, e_2 \vdash e_1$ and $e_1 \wedge e_2 \vee e_2$. The first is true by the assumption rule. For the second, by ${\vee}I$ (on either side), it suffices to show $e_1, e_2 \vdash e_2$, which again is true by the assumption rule.

In particular, since the cut rule is dispensable (and probably, in practice it's much more dispensable for this subset of propositional logic than more generally), it should be straightforward to write a proof search algorithm which should usually be pretty efficient.