項書換え系における決定可能な必須呼び計算

术语重写系统中可确定的基本调用计算

• 批准号: 09780235
• 负责人: ミデルドープ アート
• 金额: $ 1.41万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1997
• 资助国家: 日本
• 起止时间: 1997 至 1998
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-09780235/
• 关键词: 項書換え; 記号計算; 簡約戦略; 木オートマトン; 計算量; ナローイング; 停止性; 決定不能性; 決定可能性; 木のオートマトン; 永続性; 論理性

本研究プロジェクトの第1段階では,必須呼び計算理論のための新しい枠組を提案した.これは,木オートマトンと基底木変換子を利用し,項書換え系における正規形や根安定形を求めるものである.これまでに知られていた逐次性といく複雑な概念を利用することなく,より大きな書換え系のクラスが決定可能であることを簡潔に証明することに成功した.得られた研究成果は国際会議CAD'97で発表した.プロジェクトの第2段階では,基底木変換子を使うことなく,木オートマトンだけを利用して決定可能性を直接証明できることを示した.これにより,計算量の新たな上限を与えることが可能になった.より詳しく言えば,大山口のNV近似に関して,あるいは,Jacquemardの増大近似に関して,最適正規化簡約戦略が倍指数時間で決定可能であることを証明した.増大近似に関する計算量は,先行研究と比較して著しく改善されている.本研究ではさらに,遅延ナローイング計算系(Lazy Narrowin Calculus, LNCと略す)の推論規則適用時に問題となる非決定性を排除するため,どのような制限を加えればよいかを明らかにした.これにより,LNCの研究は完了したといえる.非決定性を取り除いて得られた計算系LNCdは正交な書換え系において最適性(同じ解を繰り返し計算しなという性質)を持ち,LNCよりも効率的である.LNCやLNCdに関する研究成果は,昨年,学術誌Journal of Symbolic Computationに公表した.また,LNCの条件付き書換え系への拡張であるLCNC計算系に関して,新たな完全性定理を証明し,その結果を国際会議DMTCS/CATS'99において発表した.その他,最近の研究としては,帰納的逐次書換え系と強逐次書換え系とのクラスの等価性を証明し,研究成果をInformation Processing Lettersで公表した.また,合流性や停止性に関連した書換え系の性質の決定不能性についての研究論文を現在投稿中である.この論文は,現在知られる決定不能性の結果をさらに発展させるものである.

In the first stage of this study, it is necessary to propose a new set of computational theories. The root of the tree is the root of the tree. This is a simple proof of how to use the concept of continuity. International Conference CAD'97 was held. The second step of the first step is to prove the possibility of using the base tree to determine the probability of the first step. The calculation of the amount of new The most appropriate normalized reduction strategy is the exponential time decision. Increase the approximate calculation amount, study first, compare and improve. In this study, the Lazy Narrowin Calculus (LNC) and inference rules are applied to the problem of non-determinism. The research of LNC is finished. Non-deterministic computation system LNCd and orthogonal computation system LNCd and orthogonal computation system LNC and LNCd have been studied in the Journal of Symbolic Computation. The LNC calculation system is related to the LNC condition, and the new completeness theorem is proved. The results are presented in the international conference DMTCS/CATS'99. The most recent research on this subject is to prove the equivalence of successive letters. The results of this research are listed in the Information Processing Letters. The nature of a book's system is determined by the nature of a research paper. This paper, now known as the decision can not be the result of the development of the future.

项目成果

A.Middeldorp: "A Deterministic Lazy Narrowing Calculus" Journal of Symbolic Computation. 25(6). 733-757 (1998)

A.Middeldorp：“确定性惰性窄化微积分”符号计算杂志。

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)

A.Geser、A.Middeldorp 等人：“单重写规则终止层次结构中的相对不可判定性”第 22 届代数和编程树学术讨论会论文集 (CAAP97)。

I.Durand: "Decidable Call by Need Computations in Term Rewriting" Proc.14th International Conference on Automated Deduction. LNAI 1249. 4-18 (1997)

I.Durand：“术语重写中需要计算的可判定调用”Proc.14th 国际自动演绎会议。

A.Middeldorp: "Simple Termination of Rewrite Systems" Theoretical Computer Science. 175(1). 127-158 (1997)

A.Middeldorp：“重写系统的简单终止”理论计算机科学。

M.Hanus: "Strongly Seguential and Inductively Seguential Term Rewriting Systems" Information Processing Letters. 67(1). 1-8 (1998)

M.Hanus：“强连续和归纳连续术语重写系统”信息处理快报。