Proofs of confluence in rewriting systems: from constructive to computable

Mizuhito Ogawa

(JAIST Kanazawa)

Termination and confluence are two major target properties of rewriting systems. When a rewrite system is terminating, confluence is equivalent to whether each critical pair joins, shown by Knuth and Bendix, 1970.

For nonterminating term rewriting systems, a seminal result is by Rosen in 60's followed by Huet 1980. A left-linear (i.e., no duplicated occurrences of the same variable in the lhs of each rule) term rewriting system (TRS, for short) is confluent if there are no critical pairs. Huet extended it to allow trivial critical pairs (and further allowing critical pairs that can be closed one parallel step with the specified direction). There are several extensions in 90's. Among all proofs, confluence is reduced to termination of peak elimination procedure, and they give an explicit bound/measure on peak elimination procedure.

For non-linear TRSs, confluence becomes much harder problems, and sometimes it does hold even in a natural setting. There are two directions:

(1) Instead of confluence, a weaker property, focus on unique normal form. Its origin can be traced back to Klop's thesis 1977 and Chew's thesis 1980.

(2) Confluence on a restricted class, e.g., with the right-linear condition we expect to recover confluence (which is open from 1990).

The main difficulties of both again come from finding an explicit bound/measure on peak elimination. Recently, we have several attempts to tackle confluence of non-linear term rewriting systems, which are computable in the sense that termination of peak elimination procedure is proved classically, i.e., without giving explicit bounds/measures.

We also briefly mention these difficulties shared with extensions of lambda calculus and pure (sub)type systems.

Monday 2nd April 2012, 14:00
Board Room
Department of Computer Science