Termination and confluence checking

[taktoa]

Ideally, we could warn the user if the rewriting system they give is known not to be terminating and confluent. There is a sizable amount of research in this direction:

• TTT2 uses a wide range of techniques for proving and disproving the termination of term-rewriting systems: approximated dependency graph, argument filtering, bounds, dependency pair method, Knuth-Bendix order, lexicographic path order, loop detection, matrix interpretation, polynomial interpretation, predictive labeling, recursive SCC, root labeling, semantic labeling, simple projection and subterm criterion, uncurrying, usable rules. It is written in OCaml.
• ConCon is a confluence checker for conditional term rewriting systems. It is written in Scala. ConCon works by first trying to simplify rules, removing infeasible rules from the input system, and then employing the following three confluence criteria:
  1. A quasi-decreasing strongly deterministic 3-CTRS is confluent if all its critical pairs are joinable.
  2. An almost orthogonal extended properly oriented right-stable 3-CTRS is confluent.
  3. A deterministic 3-CTRS R is confluent if its unraveling U(R) is left-linear and confluent.
• CSI is a confluence checker for first-order term rewriting systems. CSI^ho is an extension of CSI for higher-order pattern rewriting systems. Both are written in OCaml.
• CaT analyzes a term-rewriting system to figure out its computational complexity. It is written in OCaml.