2024-03-28T19:12:56Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00028615
2023-01-16T04:21:35Z
312:313:314
Conditions for confluence of innermost terminating term rewriting systems
Ishizuki, Sayaka
Oyamaguchi, Michio
Sakai, Masahiko
open access
“This is a post-peer-review, pre-copyedit version of an article published in [Applicable Algebra in Engineering, Communication and Computing]. The final authenticated version is available online at: http://dx.doi.org/10.1007/s00200-018-0377-8”.
Confluence
Innermost termination
Term rewriting systems
Decidability
This paper presents a counterexample for the open conjecture whether innermost joinability of all critical pairs ensures confluence of innermost terminating term rewriting systems. We then show that innermost joinability of all normalized instances of the critical pairs is a necessary and sufficient condition. Using this condition, we give a decidable sufficient condition for confluence of innermost terminating systems. Finally, we enrich the condition by introducing the notion of left-stable rules. As a corollary, confluence of innermost terminating left-weakly-shallow TRSs is shown to be decidable.
ファイル公開:2020/08/01
Springer
2019-08
eng
journal article
AM
http://hdl.handle.net/2237/00030806
https://nagoya.repo.nii.ac.jp/records/28615
https://doi.org/10.1007/s00200-018-0377-8
0938-1279
1432-0622
Applicable Algebra in Engineering, Communication and Computing
30
4
349
360
https://nagoya.repo.nii.ac.jp/record/28615/files/aaecc2018.pdf
application/pdf
327.2 kB
2020-08-01