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

2010 年度 実績報告書

高階関数プログラムの停止性判定に関する研究

研究課題

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

研究代表者

草刈 圭一朗  名古屋大学, 大学院・情報科学研究科, 准教授 (90323112)

研究分担者 坂部 俊樹  名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
酒井 正彦  名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
西田 直樹  名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
キーワード関数プログラム / 停止性 / 静的依存対法
研究概要

本研究の目的は、関数プログラムの停止性証明法の理論整備と、得られた理論成果に基づく停止性自動照明システムの構築である。特に、関数プログラムで広く利用されている高階関数への対応を重点的に研究する。
今年度は以下の成果が得られた。
1. 我々が提案した静的依存対法は関数プログラムの性的再帰構造を解析することにより停止性を証明する非常に強力でかつ効率的な手法である。静的依存対法を効果的かつ効率的に使用するためには引数切り落とし法と実効規則の概念が重要となってくる。本年度は、匿名関数を記述するために用いられる関数抽象を含む豊かな高階の系における、引数切り落とし法と実効規則の厳密な定義と正当性の証明を与えた。この成果により匿名関数を利用した高階関数プログラムの停止性証明が劇的に強力になった。
2. 開発中の高階定理自動証明系HOPSYS (Higher-Order Proving SYStem)の停止性ライブラリに前年度までのほぼ全ての成果を実装した。現在は、公開に向けてWebユーザインターフェース等の開発中である。

  • 研究成果

    (5件)

すべて 2011 2010

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

  • [雑誌論文] Argument Filterings and Usable Rules in Higher-Order Rewrite Systems2011

    • 著者名/発表者名
      SUZUKI Sho, KUSAKARI Keiichirou, Frederic Blanqui
    • 雑誌名

      IPSJ Transactions on Programming

      巻: Vol.4, No.2 ページ: 1-12

    • 査読あり
  • [学会発表] 制約付き木オートマトンとその閉包性2011

    • 著者名/発表者名
      倉橋克尚, 酒井正彦, 西田直樹, 野村太志, 坂部俊樹, 草刈圭一朗
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      那覇市
    • 年月日
      2011-03-07
  • [学会発表] 順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について2010

    • 著者名/発表者名
      服部達哉, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      渋川市
    • 年月日
      2010-12-14
  • [学会発表] 等式理論を法とするDPLL遷移系について2010

    • 著者名/発表者名
      馬場達也, 坂部俊樹, 西田直樹, 草刈圭一朗, 酒井正彦
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      岩手県
    • 年月日
      2010-10-15
  • [学会発表] Argument Filterings and Usable Rules in Higher-Order Rewrite Systems2010

    • 著者名/発表者名
      SUZUKI Sho, KUSAKARI Keiichirou, Frederic Blanqui
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      旭川市
    • 年月日
      2010-08-05

URL: 

公開日: 2012-07-19  

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

Powered by NII kakenhi