Congruence Closure

[DavePearce]

The concept of congruence is a pretty thorny issue. At the moment, there are numerous issues related to this (e.g. #67), and I really want to design a proper interface (e.g. #63).

Normal Forms (The Good)

Roughly speaking, the problem revolves around representation of formula. At the moment, I attempt to ensure that formula are always stored in normal form (and most of the issues arise when this is not the case). Consider this super-contrived example:

1. x == y
2. x < y

Here, apply congruence closure to (2) gives y < y and, hence, a contradiction. In summary, there are several reasons why we want to represent expressions in a normal form:

• Idealised manipulation of equations. If we have x == 1 + y but, elsewhere, we additionally know that x == y, then we can arrive at a contradiction.
• Reduced Search Space. If we knew x == y but didn't exploit this, then we could end up generating separate facts, such as x == 1 + z as distinct from y == 1 + z.
• Easier manipulation of terms. For example, having arithmetic expressions in the form of a Polynomial does make life more convenient. That said, have two possible representations for the same thing (e.g. x and its polynomial form 0+x) also makes life tricky.

Normal Forms (The Bad)

On the negative side, there is the problem of "lost representation". Consider this example:

define contains(int[] items, int item) is:
    exists(int k).(items[k] == item)

assert:
   forall(int[] xs, int x):
       if:
          |xs| > 0
          !contains(xs,x)
       then:
          xs[0] > x      

In a proof-by-contradiction, we'll end up with the equivalence xs[0] == x. In order to prove the contradiction, we need to instantiate against xs[0]. But, if we had decided xs[0] was the representative of the equivalence class containing both xs[0] and x, then we can end up missing xs[0] and not triggering instantiation. This happens because automatically substitution moves terms to their normal form.

Other situations where normal form representation can cause problems:

• Array length axiom. This triggers specifically on array length terms of the form |A|. For example, it would trigger on |A| < 0. But, we might have (|A| := x) && (x < 0).
• Array index axioms. These are similar for array length. This axiom looks for terms of the form A[i] and then triggers on various situations, including those involving |A|.
• Fresh term construction. Whenever a new term is created from existing terms (e.g. |A| is created from A) we have to make sure to convert that term into the appropriate normal form. Otherwise, we end up with some terms in the wrong form, and this causes things to be missed.

The other difficult thing caused by normal form representation is that the printed proofs don't resemble their original form. The normal form tends to be a bit ugly in places as well (especially with have inequalities always represented by >= because you end with gross things like |A| >= (i+1) which is much better denoted as i < |A|.

Strong vs Weak Normal Forms

There are two basic approaches to using normal forms. Either maintain all formula in normal form, or convert expressions to normal form as necessary:

• Strong Normal Form. All formula are maintained in normal form. This means that, whenever a new fact is inferred, it is then automatically converted into normal form. Pros: This is potentially the most efficient, since there is no repeated conversions. Cons: This perhaps results in formulae that are harder to understand from the users perspective (i.e. because they are further from the original program source).
• Weak Normal Form. In this case, formula are converted into normal form on demand. This would happen when new equations are inferred and we need to try and simplify them as much as possible (ideally to false). Pros: this results in proofs which are potentially easier to understand since the generated formulae are presumably closer to the original program source. Cons: potentially there will be lots of needless repetition converting formulae into normal form.

The latter approach may actually reduce the size of the overall proofs generated though. This is because they won't include steps for normalising formula, as currently occurs.

[DavePearce]

Congruence versus Normal Forms

An interesting question: is congruence closure a kind of normal form?

This is is interesting as it goes the question of whether we should be distinguishing congruence from normal forms. We can roughly distinguish them:

• Normal Form. The movement of a given expression into a normal form representation. This applies, for example, simplification rules, etc. That an expression is in normal form is a "global property" which is independent of e.g. any particular prover state.
• Congruence Closure. The additional application of known congruences (e.g. x==y) in normalising a given formula (e.g. x-y != 0 --> y-y != 0 --> false). What is a "congruence" here though? That an expression is "closed" over congruence is a "local property" which is specific to a given prover state (i.e. where certain congruences are known to hold).

The key here is whether it's actually possible to order congruence versus normalisation. If not, then separating them makes sense and we just iterate them to a fixed point. A rough algorithm is:

1. Traverse expression tree. For each TERM encountered:
2. Simplify TERM
3. Lookup TERM in congruence map
4. Consider parent

For example, consider applying this to x+x > y in the context of a congruence x==y+1. First, we simplify x (which does nothing) and then substitute x for y+1, to give: (y+1) + (y+1) > y. At this point, we simplify the parent to give (2*y) + 2 > y and, finally, simplify the whole equation to give y+2 > 0.

In simplifying a parent, the question is: how far does does the recursion go? If NormalForm and Congruence are completely separate, then calling NormalForm.simplify() on a parent would naturally recurse all children first. Is this what we want?

[DavePearce]

Congruence / Simplification as Proof Rules?

The other option which I think can be pulled off is to actually implement congruence closure and simplification as rewrite rules. This could be done with special support from a Prover.