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

1995 年度 実績報告書

高階書き換えシステムをもちいたプログラム検証法の研究

研究課題

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

一般研究(C)

研究機関北陸先端科学技術大学院大学

研究代表者

外山 芳人  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)

研究分担者 酒井 正彦  北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (50215597)
キーワード項書き換えシステム / 高階書き換えシステム / 合流性 / 停止性 / リダクション
研究概要

高階書き換えシステムの基礎技術であるユニフィケーション,パターンマッチング,停止性,合流性の理論的な解析と実験を行った。具体的には,等号論理のもとでのユニフィケーション・アルゴリズムの効率的な実現法の検討,停止性を保証するための新しい経路順序の提案と解析,複雑なシステムを単純なシステムに分解して解析するためのモジュラ条件の検討,効率的な計算メカニズムを実現するための計算戦略の実験を行った。この結果,合流条件と停止条件に関しては、従来知られていた結集よりも一般的な条件を明らかにすることができた。新たに得られた知見は以下のとおりである。
1.計算結果の一意性を保証するために合流条件を検証する場合,非線形な書き換え規則の取り扱いが困難であった。しかし、非線形オペレータの入れ子の数で式のランクを定めることにより,従来よりも拡張された合流条件を求めることができた。
2.高階書き換えシステムの計算結果の存在保証を行うために,従来知られていた再帰経路順序よりも強力な再帰分解順序による停止条件を明らかにできた。

  • 研究成果

    (5件)

すべて その他

すべて 文献書誌 (5件)

  • [文献書誌] 酒井正彦,外山芳人: "優先順位付き項書き換え系の意味論とその強逐次性" 信学技報. SS95-40. 31-38 (1996)

  • [文献書誌] 草刈圭一朗,酒井正彦,外山芳人: "非線形項書き換え系の合流性について" 信学技報. COMP95‐86. 123-129 (1996)

  • [文献書誌] 岩見宗弘,酒井正彦,外山芳人: "高階項書き換え系の停止性について" 信学技報. COMP95‐85. 113-121 (1996)

  • [文献書誌] T.Nagaya,M.Sakai,Y.Toyama: "NVNF‐sequentiality of Left‐linear Term Rewriting Systems" 数理解析研究所講究録. 918. 109-117 (1995)

  • [文献書誌] Y.Toyama,M.Oyamaguchi: "Church‐Rosser Property and Unique Normal Form Property of Non‐Duplicating Term Rewriting Systems" 数理解析研究所講究録. 918. 139-149 (1995)

URL: 

公開日: 1997-02-26   更新日: 2016-04-21  

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

Powered by NII kakenhi