2024-03-29T13:08:36Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00007556
2023-01-16T03:53:00Z
320:502:503
Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof
Nishida, Naoki
Sakai, Masahiko
Sakabe, Toshiki
open access
Term rewriting systems (TRSs) are extended by allowing to contain extra variables in their rewrite rules. We call the extended systems EV-TRSs. They are ill-natured since every one-step reduction by their rules with extra variables is infinitely branching and they are not terminating. To solve these problems, this paper extends narrowing on TRSs into that on EV-TRSs and show that it simulates the reduction sequences of EV-TRSs as the narrowing sequences starting from ground terms. We prove the soundness of ground narrowing-sequences for the reduction sequences. We prove the completeness for the case of right-linear systems, and also for the case that no redex in terms substituted for extra variables is reduced in the reduction sequences. Moreover, we give a method to prove the termination of the simulation, extending the termination proof of TRSs using dependency pairs, to that of narrowing on EV-TRSs starting from ground terms.
2003-06
eng
journal article
VoR
http://hdl.handle.net/2237/9247
https://nagoya.repo.nii.ac.jp/records/7556
12th International Workshop on Functional and (Constraint) Logic Programming
198
211
https://nagoya.repo.nii.ac.jp/record/7556/files/sakai_8.pdf
application/pdf
195.1 kB
2018-02-19