Child pages
  • CSU 290 (Spring 2008)

Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

Decision Procedure for Equivalences

Coming soonThis decision procedure is used to establish whether an implication where the hypotheses are equalities and the conclusion is also an equality is true, in the special case where this information can be decided without relying on the definition of the functions in the expression. (For instance, this may be interesting when we have no definition for the functions in the expression; that's what defstub does, by the way, it "defines" a function without actually giving an actual definition.)

Let's be more concrete. Suppose that we have no information about functions f and g, but we are asked to prove that:

No Format

(implies (and (= a c)
              (= (f a) b)
              (= (g c) c)
         (= (f (g a)) b))

Here's an argument that us humans can come up with easily, written in infix notation to simplify the presentation:

No Format

(f (g c)) = (f (g a))  # because a = c
          = (f c)      # because (g c) = c
          = (f a)      # because a = c
          = b          # because (f a) = b

No problem. How does ACL2s prove it, though? It uses a procedure called congruence closure. It has the advantage of working for an arbitrary equivalence relation, not just equality.

You can find precise definitions of the congruence closure algorithm in many places. See these slides on congruence closure if you are curious. I will describe it at a very high level here.

First off, take the formula you have, and extract all the subterms in it. The subterms are all the function applications that occur in the expression, and all the constants. List them all, the order is not important. Here are the subterms in the example above, listed in roughly in order of increasing complexity:

No Format

a  
b  
c  
(f a)  
(g c)  
(g a)  
(f (g a))

Note that (g a) is a subterm because it appears in (f (g a)).

Good. Now, the procedure is to repeatedly look at the equations in the hypotheses (there are three in our example), and "lump" together the terms in our list that the equation force to be equal. Lumping terms together may lead to further lumping, because new things may be made equal that we didn't know before were equal.

Let's start. Let's look at the first equation a = c. It tells you to lump together a and c. Let's do that:

No Format

a  c  
b  
(f a)  
(g c)  
(g a)  
(f (g a))

I am representing lumps by putting terms on the same line. Terms lumped together are simply terms that can be proved to be equal using the equations we have been looking at. Knowing that a and c are equal tells you also that (g a) and (g c) are equal, so we can lump those two together too:

No Format

a  c  
b  
(f a)  
(g c)  (g a)  
(f (g a))

That's it, we cannot lump things together any further based on what we know.

Let's look at the second equation, (f a) = b. It tells you to lump together (f a) and b. Easy enough:

No Format

a  c  
b  (f a)  
(g c)  (g a)  
(f (g a))

That's it, we cannot lump things together any further.

Let's look at the last equation, (g c) = c. It tells you to lump together (g c) and c. Now, because c is already lumped with something, and (g c) is also already lumped with something, let's merge the respective lumps. (After all, lumping just means that things can be proved equal.)

No Format

a  c  (g c)  (g a)  
b  (f a)  
(f (g a))

Oh, now we've learned a lot, in particular, that (g a) = a. This means that (f (g a)) = (f a), so that we can lump (f a) and (f (g a)) together:

No Format

a  c  (g c)  (g a)  
b  (f a)  (f (g a))

And that's it, we cannot lump things any further. And we've exhausted all of our equations in the hypotheses. So the lumps above represent all the different things that can be proved equal to each other. Our conjecture asks whether the three equations imply that (f (g a)) = b; in other words, do the three equations ensure that (f (g a)) and b are lumped together by the above procedure? It is easy to see that yes, they are. Therefore, the algorithm (and ACL2s) will report that the conjecture is true.