第 5 章 まとめ
5.2 今後の課題
第
5章
緩和することがあがる。
また、別の概念から項書換え系の十分条件を更に緩和したものを提案し、到達可能性や 合流性の決定可能を示していくことである。また、一般到達可能性の課題と同様に基底合 流性の決定可能性へつないでいくことがあがる。
謝辞
本研究を行なうにあたり、また学生生活全般に渡り多大なる御指導を頂いた外山芳人教 授に謹んで感謝致します。そして、研究活動において、適切な助言と多大なる御指導を頂 いた鈴木太朗助手に深く感謝します。
また、本研究に関する議論の場を与えて下さった研究室の皆さんに感謝します。最後 に、さまざまな形で学生生活をを支えてくれた家族に心から感謝します。
参考文献
[1] M.Dauchet, T.Heuillard, P.Lesdcanne, S.Tison, \Decidability of the Conuence of
FiniteGroundTermRewriteSystemsandofOtherRelatedTermRewriteSystems",
Information and Computaition 88, pp.187-20, 1990.
[2] M.Oyamaguchi, \TheChurchi-RosserPropertyforGroundTerm-RewritingSystems
is Decidable", Theoretical Computer Science49, pp.43-79, 1987.
[3] D.Kapur,P.Narendran,F.Otto, \OnGround-Conuence ofTermRewritingSystems
", Informationand Computation 86, pp.14-31, 1990.
[4] Zhang.H,Remy.J.L,\ContextualRewriting", Lect.NotesinComput.Sci.202,
pp.46-62, 1985.
[5] G.Huet, \Conuentreductions: Abstractprop erties andapplicationstoterm
rewrit-ingsystems", JournaloftheAsso ciationforComputingMachinery27, 4 pp.797-821,
1980.
[6] M.Dauchet, S.Tison, \The Theory of Ground RewriteSystems is Decidable", Fifth
Annual IEEE Syemp osium onLogic in Computer Science, pp.242-248, 1990.
[7] E.Hopcroft, D.Ullman, \Intro duction To Automata Theory, Languages And
Com-putation", Addison-WesleyPublishing Co, 1979 (野崎昭弘, 高橋正子, 町田元, 山崎 秀記 共訳「オートマトン 言語理論 計算論I」サイエンス社, 1984）.
[8] 安藤欣司, 鈴木太朗, 外山芳人, \項書換え系における到達可能性の決定問題", 平成
10年度電気関係学会北陸支部連合大会 講演論文集, pp.259, 1998.
[9] J.Leeuwen, \Handbo ok of Theretical Computer Science, volume B: Formal Models
and Semantics", ElseveirScience Publishiers, pp.163-166, 1990（広瀬健, 野崎昭弘,
小林孝次郎 監訳「コンピュータ基礎理論ハンドブックII 形式的モデルと意味論」丸 善社,1994）.
[10] F.Baader, T.Nipkow, \Term Rewriting and All That" CambridgeUniversity Press,
1998.
[11] H.Comon,M.Dauchet, R.Gilleron,D.Lugiez, S.Tison,M.Tommasi, \Tree Automata
Techniquesand Applications", www.grappa.univ-lille3.fr/tata.
[12] Y.Toyama, \Memb ership Conditional Term Rewriting Systems", The Transaction
of the IEICE E.72, pp.1224-1229, 1989.
[13] J.Co quide, M.Dauchet, R.Gilleron, S.Vagvolgyi \Bottom-up pushidown automata:
classication and connection with rewrite systems", Theoretical Computer Science
127, pp.69-98, 1994.
[14] K.Salomaa, \Deterministic Tree Pushdown Automata and Monadic Tree Rewriting
Systems", Journalof Computer and System Sciences 37, pp.367-394, 1988.
[15] F.Jacquenmard, \Decidable Approximations of Term Rewriting Systems", Lecture
Notes in Computer Science1103, pp.362-376, 1996.
[16] R.Gilleron, \Decision Problems for Term Rewriting systems and Recognizable tree
languages", LectureNotes inComputer Science 480, pp.148-159, 1991.
[17] W.S.Brainerd, \Tree generatingregularsystems", InformationandComputation 14,
pp.217-231, 1969.
付録
付録
Aメンバーシップが用いる集合をMとすると、RMはMの各要素について、合流性と停 止性をもち、かつRMに関する正規形は有限個である。このとき、正規形を uとすると き、uへ到達可能なRMの要素を受理する木オートマトンAuは作成できる。
証明 有限個の正規形を与えられているとする。このとき、RMはMの各要素について、
合流性と停止性をもっているので、RMでの変数を持った規則に対して、その規則の代わ りにその変数にすべての正規形を代入した規則ができる。この書換え系ををRM0 とする。
このとき、R0Mは基底書換え系である。[17]より基底書換え系において、到達可能性が 決定可能であり、ある項へ到達可能な項を受理する木オートマトンを作成可能である。2
付録
B集合Mとして、すべてのli 2 L;について、Vcにt !3
q 2 Q
ufである項tを代入した引 数の項を受理する木オートマトンAli
[V
c
]を作成する。
作成方法 以下のように、liの構造による帰納的な作成を行なう。
l
i
=tが定数であるとき、tだけを受理する木オートマトンを作成する。
l
i
=x2VnV
cであるとき、まず、すべての項を受理する木オートマトンAT(F)を作 成する。このとき、Ali[Vc ]を以下のように作成する。
A
l
i [V
c ]
:=(A
T(F) nA
U )[A
U
l
i
=x2V
c
:x2Mであるとき、RMに関する正規形をuとすると、Ali [Vc ]
:=A
uと