• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

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

研究課題

研究課題/領域番号 09780235
研究種目

奨励研究(A)

配分区分補助金
研究分野 計算機科学
研究機関筑波大学

研究代表者

ミデルドープ アート  筑波大学, 電子・情報工学系, 助教授 (30251044)

研究期間 (年度) 1997 – 1998
研究課題ステータス 完了 (1998年度)
配分額 *注記
2,200千円 (直接経費: 2,200千円)
1998年度: 1,000千円 (直接経費: 1,000千円)
1997年度: 1,200千円 (直接経費: 1,200千円)
キーワード項書換え / 記号計算 / 簡約戦略 / 木オートマトン / 計算量 / ナローイング / 停止性 / 決定不能性 / 決定可能性 / 木のオートマトン / 永続性 / 論理性
研究概要

本研究プロジェクトの第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で公表した.また,合流性や停止性に関連した書換え系の性質の決定不能性についての研究論文を現在投稿中である.この論文は,現在知られる決定不能性の結果をさらに発展させるものである.

報告書

(2件)
  • 1998 実績報告書
  • 1997 実績報告書
  • 研究成果

    (11件)

すべて その他

すべて 文献書誌 (11件)

  • [文献書誌] A.Middeldorp: "Call by Need Computations to Root-Stable Form" Proc.24th ACM SIGPLAN-SIGACT. 94-105 (1997)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] I.Durand: "Decidable Call by Need Computations in Term Rewriting" Proc.14th International Conference on Automated Deduction. LNAI 1249. 4-18 (1997)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] A.Middeldorp: "Simple Termination of Rewrite Systems" Theoretical Computer Science. 175(1). 127-158 (1997)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] A.Middeldorp: "A Deterministic Lazy Narrowing Calculus" Journal of Symbolic Computation. 25(6). 733-757 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Hanus: "Strongly Seguential and Inductively Seguential Term Rewriting Systems" Information Processing Letters. 67(1). 1-8 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] T.Yamada: "Logicality of Conditional Rewrite Systems" Theoretical Computer Science. (to appear). (1999)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] 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)

    • 関連する報告書
      1997 実績報告書
  • [文献書誌] 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)

    • 関連する報告書
      1997 実績報告書
  • [文献書誌] 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)

    • 関連する報告書
      1997 実績報告書
  • [文献書誌] 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)

    • 関連する報告書
      1997 実績報告書
  • [文献書誌] 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)

    • 関連する報告書
      1997 実績報告書

URL: 

公開日: 1997-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi