Weekly Reading: Term Rewriting, Formal Logic System

    My current reading goal is to review and finish the book "Term Rewriting And All That" by Franz Baader and Tobias Nipkow as soon as possible. This week, I covered the part of termination, confluence and completion. The first two combined together is used to judge if a term rewriting system (TRS) is convergent, which is regarded as a well-defined TRS, while a completion procedure is to compute a convergent TRS from a given set of identities by applying a number of inference rules if there exists one.
    In general, the decision problem on terminating and confluence given an arbitrary order is undecidable. So in the chapter of termination, the book introduced a concept called Reduction Order, which satisfies the properties of well-founded, compatible with Σ-operations, and closed under substitutions, and proposed some widely-used orders as the interpretation methods which are consistent with the reduction order. Note that the property of well-founded can be replaced by that of Simplification Order, which is much easier to show the termination of the given order. There are three classical orders introduced here: polynomial order, lexicographic path order, and the famous Knuth-Bendix order. Polynomial order requires that all function symbols in Σ under interpretation must be monotone in order to satisfy the third property of reduction order. It's easy to define, but can only show the termination of those TRS's that cannot be bound by primitive recursion (like Ackerman function). Both LPO and KBO can address this problem, and the decision procedure using either of them is decidable, while it's an NP-complete problem. LPO and KBO are both recursively defined, but KBO applies an extra weight function and the occurrence of variables in terms for the comparison.
    For the issue of confluence, it's closely related to critical pairs under the set of rules R. If TRS is terminating, then by Newman's Lemma, it's confluent iff it's locally confluent. Thus, in this case, if we can show that all critical pairs given E and R are joinable, then TRS is confluent. More generally, for a not necessarily terminating TRS, we have to show that it's left-linear (i.e. no variable occurs twice in l of any rule l -> r in R) and parallel closed over all critical pairs, which is Corollary 6.4.9 from the Parallel Closure Theorem (Theorem 6.4.8).
    In the chapter of completion procedures, a basic completion procedure is introduced, which is correct as a semidecision procedure and quite inefficient. Then an improved completion procedure was defined by applying a set of inference rules, like DEDUCE, ORIENT, DELETE, SIMPLIFY-INDENTIFY, R-SIMPLIFY-RULE, L-SIMPLIFY-RULE, many of which are quite similar to those in the decision procedure of equational unification problems. The main idea is to add those identities in E and critical pairs computed from E and R into R, then simplifying them under R and forming all resulted rules in R satisfying the reduction order >. This procedure is iterative until E becomes empty, which means that all critical pairs are joinable and the procedure terminates SUCESSFULLY. Otherwise, if E is never empty, which means that there exists some un-joinable critical pair, or some (s, t) is not comparable, which means that neither s -> t nor t -> s satisfies the reduction order >, then the procedure terminates with FAILURE. A tool named proof order is used to prove the correctness of the improved completion procedure, which is also a fair completion procedure. After that, a famous Huet's completion procedure was introduced, which works in a similar way, is correct but not fair.