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

完備化に基づくプログラム自動変換の研究

Research Project

Project/Area Number 16016202
Research Category

Grant-in-Aid for Scientific Research on Priority Areas

Allocation TypeSingle-year Grants
Review Section Science and Engineering
Research InstitutionTohoku University

Principal Investigator

外山 芳人  東北大学, 電気通信研究所, 教授 (00251968)

Co-Investigator(Kenkyū-buntansha) 青戸 等人  東北大学, 電気通信研究所, 助教授 (00293390)
菊池 健太郎  東北大学, 電気通信研究所, 助手 (40396528)
Project Period (FY) 2005
Project Status Completed (Fiscal Year 2005)
Budget Amount *help
¥4,500,000 (Direct Cost: ¥4,500,000)
Fiscal Year 2005: ¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 2004: ¥2,100,000 (Direct Cost: ¥2,100,000)
Keywords情報基礎 / ソフトウェア検証 / プログラム変換 / 定理自動証明 / 項書き換えシステム
Research Abstract

プログラム変換の手法である融合変換と、定理自動証明の手法である完備化を組み合わせた新しいプログラム変換手法を提案することを目的として、プログラム変換の実験と解析を行った。とくに、帰納的定理の強力な自動証明手法である書き換え帰納法と組み合わせることによって、プログラム変換に必要な性質を自動証明しながら、その結果を利用してプログラム変換を進めていくので、従来よりも強力な変換が可能となる。また、変換に必要な性質を自動的に発見することを可能とする補題発見機構を組み入れることにより、高度なプログラム自動変換を実現することができることを実証することができた。
さらに、パターンをもちいたプログラム変換システムRAPTを開発した。これまでの研究から、プログラムの効率化にはいくつかの定石があることが明らかになっている。そこで、これらの定石を高階の変換パターンで表現し、パターンマッチングによるプログラム変換で効率を改良する方法を提案した。変換の正当性を検証するためには、プログラムのさまざまな帰納的性質を証明する必要がある。そこで、プログラムを書き換えシステムでモデル化し、定理自動証明の手法である潜在帰納法を適用することにより、プログラム変換とその正当性の検証を完全に自動化することに成功した。RAPTは入力プログラムを自動変換して出力プログラムを得るまでの手続きを6段階に分けて実現している。実装は関数型言語SMLをもちいて行い、ソースコードのサイズは約5000行である。
また、プログラムの変換や検証に不可欠な基礎技術である高階プログラムの帰納的性質や停止条件に関する理論的な解析を進めるとともに、プログラムの実行メカニズムの設計に不可欠なリダクションの戦略に関する基礎理論の確立を行った。

Report

(2 results)
  • 2005 Annual Research Report
  • 2004 Annual Research Report
  • Research Products

    (12 results)

All 2006 2005 2004

All Journal Article (12 results)

  • [Journal Article] RAPT : A Program Transformation System based on Term Rewriting2006

    • Author(s)
      Yuki Chiba
    • Journal Title

      Proceedings of 8th JSSST Workshop on Programming and Programming Languages

      Pages: 60-74

    • Related Report
      2005 Annual Research Report
  • [Journal Article] 書き換え帰納法における向き付け不能な等式の証明2006

    • Author(s)
      青戸等人
    • Journal Title

      第8回プログラミングおよびプログラミング言語ワークショップ論文集

      Pages: 75-89

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Introducing Sequence Variables in Program Transformation based on Templates2005

    • Author(s)
      Yuki Chiba
    • Journal Title

      Information Technology Letters 4

      Pages: 5-8

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Program Transformation by Templates based on Term Rewriting2005

    • Author(s)
      Yuki Chiba
    • Journal Title

      Proceedings of the 7th ACA-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2005).

      Pages: 59-69

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Confluent Term Rewriting Systems2005

    • Author(s)
      Yoshihito Toyama
    • Journal Title

      Lecture Notes in Computer Science 3467

      Pages: 1-1

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Dependency Pairs for Simply Typed Term Rewriting2005

    • Author(s)
      Takahito Aoto
    • Journal Title

      Lecture Notes in Computer Science 3467

      Pages: 120-134

    • Related Report
      2005 Annual Research Report
  • [Journal Article] 修正AC単調意味論経路順序によるAC停止性2005

    • Author(s)
      落合 秀幸
    • Journal Title

      信学技報 COPMP2004-76

      Pages: 23-32

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Termination of S-Expression Rewriting Systems2005

    • Author(s)
      Y.Toyama
    • Journal Title

      第6回PPL論文集

      Pages: 17-17

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Termination of S-Expression Rewriting Systems2004

    • Author(s)
      Y.TOYAMA
    • Journal Title

      Lecture Notes in Comput.Sci. Vol.3091

      Pages: 40-54

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Inductive Theorems for Higher-Order Rewriting2004

    • Author(s)
      T.Aoto
    • Journal Title

      Lecture Notes in Comput.Sci. Vol.3091

      Pages: 269-284

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Termination of simply-typed applicative term rewriting systems2004

    • Author(s)
      T.Aoto
    • Journal Title

      Proceedings of the 2nd international Workshop on HOR

      Pages: 61-65

    • Related Report
      2004 Annual Research Report
  • [Journal Article] 書き換え帰納法に基づくプログラム融合変換2004

    • Author(s)
      坂本邦彦
    • Journal Title

      日本ソフトウェア科学会第21回大会予稿集

    • Related Report
      2004 Annual Research Report

URL: 

Published: 2004-04-01   Modified: 2018-03-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi