Method guarantees consistent outcomes from complex rewrite systems
A new method for proving confluence on abstract reduction systems --- Confluence of non-E-overlapping weakly-shallow TRSs ---
Logic in Computer Science
Summary
When computers simplify or change expressions step-by-step, different paths could lead to different results, which is a problem. This paper introduces a new way to prove that certain systems always reach the same outcome, no matter how they are simplified. The authors improve previous methods by allowing a broader class of rules to be handled and make it easier to check this property automatically.
What this means in practice
- •For compiler developers: Improve reliability in program transformation steps by guaranteeing consistent outcomes through automatic confluence checks of rewrite rules.
- •For automated theorem proving engineers: Design theorem provers that ensure rule-based simplifications do not lead to conflicts by applying decidable criteria from this method.
A theory result. No direct application yet.
Authors
Masahiko Sakai, Mizuhito Ogawa, Michio Oyamaguchi
Abstract
This paper proposes a new method for proving the confluence of an abstract reduction system (ARS) by clarifying the sufficient conditions, called compatibility and edge commutativity, for expanding a given finite sub-ARS into a confluent one by adding rewrite edges. This method can be regarded as an extension of our earlier work, which showed that a weakly non-overlapping, shallow, and non-collapsing term rewriting system (TRS) is confluent. Furthermore, we apply our method to demonstrate that a non-$E$-overlapping and weakly shallow TRS is confluent. Here, a term is weakly shallow if each defined function symbol occurs either at the root or in the ground subterms, and a TRS is weakly shallow if both sides of all its rewrite rules are weakly shallow. This drops the non-collapsing condition assumed in our previous work on weakly shallow TRSs. Moreover, since a weakly shallow TRS is non-$E$-overlapping whenever it is non-$ω$-overlapping, and the latter property is decidable, we also obtain a decidable sufficient condition for confluence: non-$ω$-overlapping and weakly shallow TRSs are confluent.