ボトムアップ最内項書き換えシステムの最内到達可能性

摘要

Durand and Senizergues(2007) showed that reachability of bottom-up linear term rewriting systems is decidable. In this paper we propose the class of bottom-up innermost systems by replacing "bottom-up rewriting" with "bottom-up innermost rewriting", and show that innermost reachability is decidable for bottom-up innermost left-linear term rewriting systems. Furthermore, we give a class of bottom-up innermost systems-the class of strongly k-bottom-up innermost systems-and show that it is decidable whether a left-linear term rewriting system belongs to the class.%DurandとSénizergues(2007)によってボトムアップ線形項書き換えシステムの到達可能性が決定可能であることが示されている.本論文では，ボトムアップ書き換えをボトムアップ最内書き換えに変更したボトムアップ最内システムのクラスを提案し，ボトムアップ最内左線形項書き換えシステムの最内到達可能性が決定可能であることを示す.また，ボトムアップ最内システムを制限した強たボトムアップ最内システムを提案し，左線形項書き換えシステムが強kボトムアツプ最内システムか否かが決定可能であることを証明する.