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

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

Research Project

Project/Area Number 14019003
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) 草刈 圭一朗  東北大学, 電気通信研究所, 助手 (90323112)
Project Period (FY) 2002
Project Status Completed (Fiscal Year 2002)
Budget Amount *help
¥2,600,000 (Direct Cost: ¥2,600,000)
Fiscal Year 2002: ¥2,600,000 (Direct Cost: ¥2,600,000)
Keywordsプログラム変換 / 完備化 / 融合変換 / 自動証明
Research Abstract

完備化に基づくプログラム融合変換が失敗した場合には,どのような条件を追加すれば変換が成功するかを調べた.さらに,より広いクラスのプログラムに対して変換が成功するように,完備化手続きの改良を行った.
具体的には、項書き換えシステムに基づいた融合変換手続きの形式化を行い、融合変換手続きの停止条件に焦点を絞った解析を行った.その結果,変換途中で生成される項のパターンが高々有限となるための条件と,融合変換手続きの停止条件は密接に関係していることが明らかになった.この成果に基づき,項の反復パターンを発見すると新しい関数として自動的に定義するメカニズムを,完備化手続きに組み込んだ.この拡張された完備化手続き上でプログラム融合変換の実験を計算機上で行ない,従来は完備化が発散して失敗して例に対しても,融合変換が可能となることを示した.
さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,帰納的定理の判定問題が決定可能となるための十分条件を解析し,融合変換に帰納的定理を自動適用する可能性を検討した.帰納的定理の判定問題を一般化し,抽象的なリダクションシステムの等価性判定問題としてとらえることにより,書き換え帰納法に基づく簡明で見通しの良い判定条件を与えることに成功した.この条件は,従来知られていた結果の拡張になっている.ここで与えられた決定可能条件は,Kapurら(2000,2001)の条件の一般化となっており,より広いクラスの決定問題に対して適用可能である.

Report

(1 results)
  • 2002 Annual Research Report
  • Research Products

    (6 results)

All Other

All Publications (6 results)

  • [Publications] Yoshihito Toyama: "Decidability for left-linear growing term rewriting systems"Information and Computation. 178. 499-514 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Keiichirou Kusakari: "On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique"The First International Workshop on Higher-Order Rewriting. HOR'02. 25 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Yoshihito Toyama: "Decision procedure for inductive theorems by rewriting induction,"Technical Report of IEICE COMP. 2002-45. 41-45 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 外山 芳人: "書き換え帰納法による帰納的定理の決定手続き"日本ソフトウェア科学会第19回大会論文集. 2002-9. 3A-2 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 鶴川敏孝: "変換パターンに基づく高階プログラム変換"信学技報COMP. 2002-83. 61-68 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 伊藤芳浩: "完備化手続きによるプログラム融合変換の停止条件"信学技報COMP. 2002-84. 69-76 (2002)

    • Related Report
      2002 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi