Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations

We propose an extension of rewriting techniques to derive inclusion relations a ⊆ b between terms built from monotonic operators. Instead of using only a rewriting relation ⊆ −→ and rewriting a to b, we use another rewriting relation ⊇ −→ as well and seek a common expression c such that a ⊆ −→ ∗ c and b ⊇ −→ ∗ c. Each component of the bi-rewriting system ⊆ −→, ⊇ −→ is allowed to be a subset of the corresponding inclusion ⊆ or ⊇. In order to assure the decidability and completeness of the proof procedure we study the commutativity of ⊆ −→ and ⊇ −→. We also extend the existing techniques of rewriting modulo equalities to bi-rewriting modulo a set of inclusions. We present the canonical bi-rewriting system corresponding to the theory of non-distributive lattices.

• Type: Conference
• Year: 1993
• Where: RTA
• Authors: Jordi Levy, Jaume Agustí-Cullell
• Keywords: Common Expression, Inclusion Relations, Monotonic Operators, RTA 1993, Theoretical Computer Science