1997 Fiscal Year Annual Research Report
| Project/Area Number |
09780235
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
ミデルドープ アート 筑波大学, 電子・情報工学系, 助教授 (30251044)
|
|---|
| Keywords | 項書換え / 記号計算 / 簡約戦略 / 決定可能性 / 木のオートマトン / 永続性 / 論理性 |
|---|
| Research Abstract |
項書換え系の効率の良い簡約を実現するため、決定可能な必須呼び計算の研究を行なった。本研究の成果は、次の通りである。
1.決定可能なルート必須簡約
木のオートマトン理論を必須簡約の決定可能性に応用すつ新たな手法に着目し、研究を進めた。決定手続きの複雑さについては、これまで議論がなされていないため、決定アルゴリズムの複雑さの上限を与えることができなかった。そこで、本研究では、定規形やルート安定形を求めるための必須呼び戦略について、木のオートマトン理論だけに基づく新たな決定手続きを開発し、複雑さの上限を与えることに成功した。また、すでに複雑さの知られている強逐次性やNV逐次性との比較を行なった。現在、これら複雑さに関する研究成果の論文を執筆中である。
2.項書換えにおける型付け
項書換え系の性質の照明を容易にするための型付け手法がすでに知られているが、本研究ではこの研究を拡張し、さらに難しい場合である等式系付き書換え系へ適用できるようにした。この結果の応用として、AC停止性の決定不能性を導くことができる。Yaroslavlで開催されたLFCS'97では、この成果についての研究発表を行なっている。
3.条件付き項書換え系の論理性
条件付き項書換え系が論理性を持つとは、対応する等式系と論理的強さが等価なことをいう。本研究では、すでに知られている論理性に関する性質をまとめ、書換え系の重要なクラスである定向条件付き書換え系の論理性を保証するような新たな十分条件を提示した。Lilleにおいて開催されたCAAP'97において、この研究成果の発表を行なった。
|
-
[Publications] T.Yamada dt al.: "Logicality of Conditional Rewrite Systems" Proceedings of the 22nd Colloquium on Trees in Algebra and Programming(CAAP'97). LNCS1214. 141-152 (1997)
-
[Publications] A.Geser, A.Middeldorp et.al.: "Relative Undecidability in the Termination Hierarchy of Single Rewrite Rules" Proceedings of the 22nd Colloquium on Trees in Alegebra and Programming(CAAP'97). LNCS1214. 237-248 (1997)
-
[Publications] H.Ohsaki and A.Middeldorp: "Type Introduction for Equational Rewriting" Proceedings of the 4th Symposium on Logical Foundations of Computer Science. LNCS1234. 283-293 (1997)
-
[Publications] I.Durand and A.Middeldorp: "Decidable Call by Need Computations in Term Rewriting" Proceedings of the 14th International Conference on Automated Deduction. LNAI1249. 4-18 (1997)
-
[Publications] A Geser and A.Middeldorp et al.: "Relative Undecidability in Term Rewriting" Proceedings of the 10th Annual Conference of the European Asociation for Computer Science Logic. LNCS1258. 150-166 (1997)
