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

2009 Fiscal Year Annual Research Report

項書き換えに基づく計算量解析の自動化

Research Project

Project/Area Number 20800022
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

廣川 直  Japan Advanced Institute of Science and Technology, 情報科学研究科, 助教 (50467122)

Keywords情報基礎 / 計算量 / 項書き換え
Research Abstract

プログラムの時間効率がどれくらいなのかを解析することは、プログラムを解析する上での中心的なテーマである。仮に探索アルゴリズムやソートアルゴリズムを開発したとする。そのとき時間的計算量、すなわち「入力の大きさに対しどれくらいの速度(ステップ数)で動作するか」という自然な疑問が生じる。本研究の目的はこの計算量を自動解析する手法を確立することであり、本年度は重差原理の研究とUncurrying変換の研究が課題であった。
まず重差原理の研究から、1970年に導入されたKnuth-Bendix順序が要求する探索空間が実は有限であることが判明した。この順序は定理証明システムに広く採用されている停止性証明の手法であり、この順序を用いるには関数記号から自然数への適切な写像を見つける必要がある。本研究により入力の項書き換え系のサイズをnとした場合、{0,…,2^(2^n)}への写像で全ての場合が網羅されることが証明された。この成果は国際論文誌JARに掲載された。
Uncurryingは関数型プログラムの項構造の変換手法であり、変換後の計算量解析は容易である。本研究では変換後のプログラムが最内停止性を持つなら元のプログラムの最内停止性が結論できること(健全性)、しかし驚くべきことにその逆(完全性)は成立しないことを証明した(full strategyでは完全だった)。またfull strategyでは多項式計算量が変換前後で保存されることを明らかにした。この成果は計算量自動解析ツールTCTやCaTに採用されている。これらの成果をまとめた論文は国際ワークショップHORに受理された。

  • Research Products

    (4 results)

All 2010 2009 Other

All Journal Article (1 results) (of which Peer Reviewed: 1 results) Presentation (1 results) Book (1 results) Remarks (1 results)

  • [Journal Article] KBO Orientability2009

    • Author(s)
      Harald Zankl, Nao Hirokawa, Aart Middeldorp
    • Journal Title

      Journal of Automated Reasoning 43(2)

      Pages: 173-201

    • Peer Reviewed
  • [Presentation] Uncurrying for Innermost Termination and Derivational Complexity2010

    • Author(s)
      Harald Zankl, Nao Hirokawa, Aart Middeldorp
    • Organizer
      5^<th> International Workshop on Higher-Order Rewriting
    • Place of Presentation
      エジンバラ大学(イギリス)(発表確定)
    • Year and Date
      2010-07-14
  • [Book] 電子情報通信学会 知識ベース 7群1編「ソフトウェア基礎」2章「定理証明と検証法」3節「SAT」執筆2010

    • Author(s)
      廣川直
    • Total Pages
      7
    • Publisher
      社団法人 電子情報通信学会
  • [Remarks]

    • URL

      http://www.jaist.ac.jp/~hirokawa/

URL: 

Published: 2011-06-16   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi