Unification for Finitely Presented Algebras

The example below (using Boolean Algebra) is the kind of description of an “Algebra” that I wish I had when I learned this stuff in school- we did a lot of stuff with modular arithmetic, that I think was a lot harder.

The problem: Unification for Finitely Presented Algebras.  This is problem AN17 in the appendix.

The description: Given a description of an algebra as a set G of generator symbols, a set O of operator symbols (of possibly varying dimensions), and a Γ of “defining relations” over G and O.  We’re also given two expressions x and y over G and O, and a set of variables V.   Can we find “interpretations” for x and y, called I(x) and I(y) such that I(x) and I(y) are formed by replacements of variables such that I(x) and I(y) represent the same element of the algebra?

Example: The paper by Kozen that has the reduction gives a pretty good example of an algebra: Suppose G was {0,1}, O was {∧, ∨, ¬}, and Γ was {0∧0 ≡ 0, 0 ∧ 1 ≡ 0, 1 ∧ 0 ≡ 0, 1 ∧ 1 ≡ 1, 0 ∨ 0 ≡ 0, 0 ∨ 1 ≡, 1 ∨ 0 ≡ 1, 1 v 1 ≡ 1, ¬0 ≡ 1, ¬1 ≡}.  This is the normal Boolean Algebra we see everywhere.

Now we can ask questions like: If x = a ∨ b ∨ c and y = 0 ∨ 1 ∨ d, can we find a unification of the variables that makes the equations the same?  The answer is yes, with the replacements {a/0, b/1, d/c}.

I think the  “represent the same element” part of the problem statement means that we can also take advantage of unification rules, so we can ask questions like does ~x ∨ y ∨ ~z unify to 1?

Reduction: Kozen’s paper makes the point that if we use the Boolean Algebra that we used in the example, then the Satisfiability problem can be represented in Boolean Algebra using the rules above, and the question “Is this formula satisfiable” can be recast as “Does this formula unify to true?”

He doesn’t provide the proof, though, so I hope I’m representing him correctly.

Difficulty: 4.  Once you see how the Boolean Algebra relates, it’s pretty easy.

Leave a Reply

Your email address will not be published. Required fields are marked *