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

2000 年度 研究成果報告書概要

簡約戦略に関する研究

研究課題

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

基盤研究(C)

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

研究代表者

MIDDELDORP Aart  筑波大学, 電子・情報工学系, 助教授 (30251044)

研究分担者 山田 俊行  筑波大学, 電子・情報工学系, 助手 (60312831)
井田 哲雄  筑波大学, 電子・情報工学系, 教授 (70100047)
研究期間 (年度) 1999 – 2000
キーワード項書き換え / ナローイング / 記号計算 / 必要呼び計算 / モジュラー性 / 停止性 / 完全性
研究概要

本研究では,意味ラベリングと呼ばれる,項書換え系の停止性を証明する手法について考察を行なった.Zantemaは,意味ラベリングを等式付き書換えへ拡張しているが,この拡張は制限が強い.このため,(1)意味解釈を与える代数上の順序(半順序または擬順序)(2)代数と書換え系の関係(モデルまたは準モデル)(3)等式に現われる関数記号のラベル付け可能性(禁止または許可)の3つをパラメタ化することにより,強力な意味ラベリングの手法を導入した.Ohsaki,Gieslらとの共著論文では,この新しい停止性証明手法が健全性と完全性をもつことを証明し,応用の可能性を示した(論文一覧を参照).
また,遅延ナローイング計算系の完全性に関する考察も行なった.我々は,以前に発表した研究論文で,遅延ナローイング計算系LCNCが,条件部に外変数をもつ条件付き書換え系において,正規解に関して完全性をもつことを証明した.しかし,この論文中では,有用な選択関数を与えることができなかったため,計算系を実装する際,全ての解を列挙するために,ゴール中の等式を選択する場所へのバックトラックが必要となった.本研究では,この問題を解消するため,最左の等式を選択することにより,完全性が得られることを証明した.得られた研究成果は,Suzukiとの共著論文により公表する予定である(論文一覧を参照).
Durandとの共著論文(論文一覧を参照)では,必要呼び計算の研究に有用な理論を導入した.この理論をでは,木オートマトンと基底木変換系を用い,簡潔な決定可能性の証明を与えることができる.本研究では,停止性の成立する書換え系に関する所属問題のモジュラー性について考察を行なった.まず,関数記号を追加した場合の性質の保存について考察を行なった後,書換え系に対する制約を強めることにより,一般のモジュラー性や,構成子記号の共有を許す場合に,同様の結果が成立するかどうかも調べた.

  • 研究成果

    (8件)

すべて その他

すべて 文献書誌 (8件)

  • [文献書誌] H.Ohsaki,A.Middeldorp,J.Giesl: "Equational Termination by Semantic Labelling"Proc.14th Annual Conference of the European Association for Computer Science Logic, LNCS. 1862. 457-471 (2000)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] T.Suzuki,A.Middeldorp: "A Complete Selection Function for Lazy Conditional Narrowing"Proc.5th International Symposium on Functional and Logic Programming, LNCS. (印刷中). (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] I.Durand,A.Middeldorp: "On the Modularity of Deciding Call-by-Need"Proc.International Conference on the Foundations of Software Science and Computation Structures, Genova, LNCS. (印刷中). (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] A.Geser,A.Middeldorp,E.Ohlebusch,H.Zantema: "Relative Undecidability in Term Rewriting. Part 1: The Termination Hierarchy"Information and Computation. (印刷中). (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] H.Ohsaki, A.Middeldorp, J.Giesl: "Equational Termination by Semantic Labelling"Proc.14th Annual Conference of the European Association for Computer Science Logic, Lecture Notes in Computer Science 1862. 457-471 (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] T.Suzuki and A.Middeldorp: "A Complete Selection Function for Lazy Conditional Narrowing"Functional and Logic Programming, Lecture Notes in Computer Science. Accepted for publication. (2001)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] I.Durand and A.Middeldorp: "On the Modularity of Deciding Call-by-Need"Foundations of Software Science and Computation Structures, Genova, Lecture Notes in Computer Science. Accepted for publication. (2001)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] A.Geser, A.Middeldorp, E.Ohlebusch, and H.Zantema: "Relative Undecidability in Term Rewriting. Part 1 : The Termination Hierarchy"Information and Computaion. Accepted for publication.. (2001)

    • 説明
      「研究成果報告書概要(欧文)」より

URL: 

公開日: 2002-03-26   更新日: 2021-04-07  

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

Powered by NII kakenhi