Algebraic Tools for Binary Relations in Coq

• Binary relations have a hierarchy of partial axiomatisations with different properties; the following file illustrates why it may be easier to work with binary relations at this algebraic level.
• Some of these algebraic fragments enjoy decidable equality (semi-lattices, idempotent non-commutative semirings, Kleene algebras), so that we can define tactics to automatically solve the corresponding goals.

Deciding Kleene Algebras

For example, this tactic automatically solves goals of the form a#*(b+a#*(1+c))# = (a+b+c)# or a*b*c*a*b*c*a# <= a#*(b*c+a)#, where a, b, and c are elements of an arbitrary Kleene algebra (binary relations, regular languages, min-max expressions...), # is the (postfix) star operation, * is the infix product or concatenation operation, + is the sum or union operation, and 1 is the neutral element.

Changes in the second release

1. We switched to positive binary numbers, which required the introduction of a new infrastructure.
2. The construction algorithm is no longer Thompson's one; it is no longer implemented using a matricial representation.
3. The epsilon removal step is no longer computed algebraically: we prove that our construction returns acyclic epsilon-transitions, so that we can use a linear transitive closure algorithm.
4. The determinisation algorithm remained the same, but was reimplemented in a more natural way, thanks to a partial fixpoint operator. (In particular, we no longer need the CoLoR library: termination of the determinisation step no longer requires multiset well-founded orderings.)
5. We no longer use minimisation to tests DFAs fo equivalence; instead, we implemented Hopcroft and Karp's algorithm, using an efficient disjoint-sets data-structure.
6. In case of failure, the tactic now provides a counter-example to the user; the decision procedure was moreover proved complete.

Performances

We performed intensive tests on randomly generated regular expressions. On typical use cases, the tactic runs instantaneously. It runs in less than one second for expressions with 150 internal nodes and 20 variables, and less than one minute for even larger expressions (1000 internal nodes, 40 variables), that are very unlikely to appear in ``human-written'' proofs. (These timings were obtained by testing each regular expression with itself: this is approximately a worst case, since we implemented an early failure optimisation in the equivalence check.)

We also compared our approach with the works of Struth, Hoefner, and Dang, who work with automatic theorem provers (ATP). Timings can be found here, the whole benchmark is there.

Matrices

Rewriting closed equations modulo A / AC

Downloads

• Second release (25th of January, 2010): tar.gz. Distributed under LGPL 3. Compiles with the Coq v8.2 `bugfix' (-r 12575 and hopefully the following ones).
• First release (9th of June, 2009): tar.gz. Distributed under LGPL 3. Compiles with the Coq v8.2 `bugfix' (-r 12142 and hopefully the following ones).
• Documented Coq file that illustrates how to use our library:
  • simple generic Examples, .v source file;
  • some Church-Rosser theorems, .v source file.
• Twelve pages description of this development (presented at the Coq Workshop): A Tactic for Deciding Kleene Algebras, .pdf.
• A more recent description of this work: An Efficient Coq Tactic for Deciding Kleene Algebras, .pdf.
  T. Braibant and D. Pous, to appear in Proc. ITP'10, July 2010.
• A .v file explaining how we achieve type-erasing reification within Ltac.

Authors

Documentation