• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2011 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 20500008
Research InstitutionNagoya University

Principal Investigator

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

Co-Investigator(Kenkyū-buntansha) 坂部 俊樹  名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
酒井 正彦  名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
西田 直樹  名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
Keywords関数プログラム / 再帰定義 / 停止性
Research Abstract

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

  • Research Products

    (4 results)

All 2012 2011

All Presentation (4 results)

  • [Presentation] 高階書換え系における引数切り落とし関数の下での実効規則について2012

    • Author(s)
      大井一展, 草刈圭一朗, 酒井正彦, 坂部俊樹,西田直樹
    • Organizer
      電気情報通信学会
    • Place of Presentation
      高知
    • Year and Date
      20120100
  • [Presentation] 単純型付き項書換え系における書換え帰納法について2012

    • Author(s)
      尾関朗, 草刈圭一朗, 坂田翼, 西田直樹, 酒井正彦, 坂部俊樹
    • Organizer
      電気情報通信学会
    • Place of Presentation
      高知
    • Year and Date
      20120100
  • [Presentation] 制約付き項書換え系における木準同型写像を用いた関数等価性検証2011

    • Author(s)
      高桑一也, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗
    • Organizer
      日本ソフトウェア科学会
    • Place of Presentation
      那覇
    • Year and Date
      20110900
  • [Presentation] 多重文脈書換え帰納法における反証と補題追加2011

    • Author(s)
      坂田翼, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹
    • Organizer
      日本ソフトウェア科学会
    • Place of Presentation
      那覇
    • Year and Date
      20110900

URL: 

Published: 2013-06-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi