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

2008 年度 実績報告書

関数型言語の解析・検証・効率的実行のための書換え系理論の研究

研究課題

研究課題/領域番号 18500011
研究機関名古屋大学

研究代表者

酒井 正彦  名古屋大学, 大学院・情報科学研究科, 教授 (50215597)

研究分担者 坂部 俊樹  名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
草刈 圭一朗  名古屋大学, 大学院・情報科学研究科, 准教授 (90323112)
西田 直樹  名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
粕谷 英人  愛知県立大学, 情報科学部, 助教 (10295579)
キーワード項書換え系 / 関数型言語 / 停止性 / 合流性 / 単純型書換え系 / 定理自動証明
研究概要

本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャップとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
今年度は以下の成果が得られた。
1. これまでに提案している高階書換え系に対する依存対法による停止性証明法において、(1)証明可能なクラスを拡張し、「関数安全渡し」と名付けた。(2)1階のシステムにおける「利用可能規則」の手法を高階のシステム用に拡張した。
2. 高階書換え系に対して、書換え可能な項(リデックス)の集合を認識する木オートマトンの構成法を示した。これにより、書換え関係の反射的推移的閉包を含む関係を認識する木オートマトンが構成できるようになり、到達可能性を保証するツールの作成が可能になった。
3. 1階の項書換え系における正規化戦略を高階書換え系に拡張した。実際に、(1)与えられた項の書換えるべき箇所を発見する手続き、(2)この戦略が適用可能な書換え系かを判定する手続きを明らかにした。
4. プレスブルーガ文などの具体的に意味が与えられた条件を付加した項書換え系の停止性を示す簡約化順序を与えた。これにより、C風の手続き型言語のプログラムの正しさの証明ツールを強化できる。
5. 線形な左シャロー項書換え系のクラスでは、最内到達可能性と文脈依存到達可能性がいずれも決定可能であることを示した。
6. 依存対の右辺が線形かつシャローである項書換え系に対して、停止性、最内停止性、文脈依存停止性がいずれも決定可能な性質であることを示した。これは、昨年度得られた結果の拡張になっている。

  • 研究成果

    (10件)

すべて 2009 2008

すべて 雑誌論文 (3件) (うち査読あり 3件) 学会発表 (7件)

  • [雑誌論文] Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques2009

    • 著者名/発表者名
      Keiichirou Kusakari, Masahiko Sakai
    • 雑誌名

      IEICE Transactions on Information and Systems E92-D

      ページ: 235-247

    • 査読あり
  • [雑誌論文] Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes2009

    • 著者名/発表者名
      Hideto Kasuya Masahiko Sakai, Kiyoshi Agusa
    • 雑誌名

      IPSJ Transactions of Programming 2

      ページ: 144-165

    • 査読あり
  • [雑誌論文] Recognizability of Redexes for Higher-Order Rewrite Systems2009

    • 著者名/発表者名
      Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa
    • 雑誌名

      IPSJ Transactions of Programming 2

      ページ: 166-175

    • 査読あり
  • [学会発表] Decidability of termination for TRSs with right-shallow DPs2009

    • 著者名/発表者名
      Masahiko Sakai
    • 学会等名
      The 31st Workshop on Term Rewriting Systems
    • 発表場所
      加賀市
    • 年月日
      2009-02-24
  • [学会発表] Decidability of Termination Properties for Term Rewriting Systems consisting of Shallow Dependency Pairs2008

    • 著者名/発表者名
      Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe, Keiichirou kusakari, Naoki Nishida
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      高知市
    • 年月日
      2008-12-19
  • [学会発表] On confluent property of shallow term rewriting systems2008

    • 著者名/発表者名
      Masahiko Sakai
    • 学会等名
      The 30th Workshop on Term Rewriting Systems
    • 発表場所
      札幌市
    • 年月日
      2008-08-26
  • [学会発表] On Decidability of Innermost Termination for Shallow Term Rewriting Systems2008

    • 著者名/発表者名
      Masahiko Sakai
    • 学会等名
      Mini-Workshop on Rewriting Techniques
    • 発表場所
      能美市
    • 年月日
      2008-08-01
  • [学会発表] 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序2008

    • 著者名/発表者名
      西田直樹, 坂田翼, 酒井正彦, 草刈圭一朗, 坂部俊樹
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      函館市
    • 年月日
      2008-07-31
  • [学会発表] Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems2008

    • 著者名/発表者名
      Yoshiharu Koiima, Masahiko Sakai
    • 学会等名
      19th International Conference on Rewriting Techiniques and Applictions (査読有)
    • 発表場所
      ハーゲンベルグ
    • 年月日
      2008-07-15
  • [学会発表] プレスブルガー文付き項書換え系における書換え帰納法について2008

    • 著者名/発表者名
      坂田翼, 西田直樹, 酒井正彦、草刈圭一朗, 坂部俊樹
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      宮崎市
    • 年月日
      2008-05-29

URL: 

公開日: 2010-06-11   更新日: 2016-04-21  

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

Powered by NII kakenhi