A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-cri...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/667/pdf |
| _version_ | 1797268684011470848 |
|---|---|
| author | Takahito Aoto Yoshihito Toyama |
| author_facet | Takahito Aoto Yoshihito Toyama |
| author_sort | Takahito Aoto |
| collection | DOAJ |
| description | We give a method to prove confluence of term rewriting systems that contain
non-terminating rewrite rules such as commutativity and associativity. Usually,
confluence of term rewriting systems containing such rules is proved by
treating them as equational term rewriting systems and considering E-critical
pairs and/or termination modulo E. In contrast, our method is based solely on
usual critical pairs and it also (partially) works even if the system is not
terminating modulo E. We first present confluence criteria for term rewriting
systems whose rewrite rules can be partitioned into a terminating part and a
possibly non-terminating part. We then give a reduction-preserving completion
procedure so that the applicability of the criteria is enhanced. In contrast to
the well-known Knuth-Bendix completion procedure which preserves the
equivalence relation of the system, our completion procedure preserves the
reduction relation of the system, by which confluence of the original system is
inferred from that of the completed system. |
| first_indexed | 2024-04-25T01:36:23Z |
| format | Article |
| id | doaj.art-3420baaff54142d9b5e13ce33e6e249c |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:23Z |
| publishDate | 2012-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-3420baaff54142d9b5e13ce33e6e249c2024-03-08T09:27:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-03-01Volume 8, Issue 110.2168/LMCS-8(1:31)2012667A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting SystemsTakahito AotoYoshihito ToyamaWe give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also (partially) works even if the system is not terminating modulo E. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.https://lmcs.episciences.org/667/pdfcomputer science - logic in computer scienced.3.1, f.3.1, f.4.2, i.2.2 |
| spellingShingle | Takahito Aoto Yoshihito Toyama A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems Logical Methods in Computer Science computer science - logic in computer science d.3.1, f.3.1, f.4.2, i.2.2 |
| title | A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems |
| title_full | A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems |
| title_fullStr | A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems |
| title_full_unstemmed | A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems |
| title_short | A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems |
| title_sort | reduction preserving completion for proving confluence of non terminating term rewriting systems |
| topic | computer science - logic in computer science d.3.1, f.3.1, f.4.2, i.2.2 |
| url | https://lmcs.episciences.org/667/pdf |
| work_keys_str_mv | AT takahitoaoto areductionpreservingcompletionforprovingconfluenceofnonterminatingtermrewritingsystems AT yoshihitotoyama areductionpreservingcompletionforprovingconfluenceofnonterminatingtermrewritingsystems AT takahitoaoto reductionpreservingcompletionforprovingconfluenceofnonterminatingtermrewritingsystems AT yoshihitotoyama reductionpreservingcompletionforprovingconfluenceofnonterminatingtermrewritingsystems |