2023-01-27T19:55:31Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000775912020-10-27T05:02:43Z00934:00935:06375:06536
Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting SystemsDecidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systemseng通常論文http://id.nii.ac.jp/1001/00077591/Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=77591&item_no=1&attribute_id=1&file_no=1Copyright (c) 2011 by the Information Processing Society of JapanGraduate School of Information Science, Nagoya University／Research Fellow of the Japan Society for the Promotion of ScienceGraduate School of Information Science, Nagoya UniversityGraduate School of Information Science, Nagoya UniversityGraduate School of Information Science, Nagoya UniversityGraduate School of Information Science, Nagoya UniversityYoshiharu, KojimaMasahiko, SakaiNaoki, NishidaKeiichirou, KusakariToshiki, SakabeThe reachability problem for an initial term, a goal term, and a rewrite system is to decide whether the initial term is reachable to goal one by the rewrite system or not. The innermost reachability problem is to decide whether the initial term is reachable to goal one by innermost reductions of the rewrite system or not. A context-sensitive term rewriting system (CS-TRS) is a pair of a term rewriting system and a mapping that specifies arguments of function symbols and determines rewritable positions of terms. In this paper, we show that both reachability for right-linear right-shallow CS-TRSs and innermost reachability for shallow CS-TRSs are decidable. We prove these claims by presenting algorithms to construct a tree automaton accepting the set of terms reachable from a given term by (innermost) reductions of a given CS-TRS.The reachability problem for an initial term, a goal term, and a rewrite system is to decide whether the initial term is reachable to goal one by the rewrite system or not. The innermost reachability problem is to decide whether the initial term is reachable to goal one by innermost reductions of the rewrite system or not. A context-sensitive term rewriting system (CS-TRS) is a pair of a term rewriting system and a mapping that specifies arguments of function symbols and determines rewritable positions of terms. In this paper, we show that both reachability for right-linear right-shallow CS-TRSs and innermost reachability for shallow CS-TRSs are decidable. We prove these claims by presenting algorithms to construct a tree automaton accepting the set of terms reachable from a given term by (innermost) reductions of a given CS-TRS.AA11464814情報処理学会論文誌プログラミング（PRO）4412352011-09-221882-78022011-09-16