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

2011 Fiscal Year Annual Research Report

単射性を持つ関数型プログラムの逆関数プログラム生成に関する研究

Research Project

Project/Area Number 21700011
Research InstitutionNagoya University

Principal Investigator

西田 直樹  名古屋大学, 大学院・情報科学研究科, 助教 (00397449)

Keywords情報基礎 / 項書換え系 / 関数型言語 / プログラム変換 / 逆関数 / 単射性
Research Abstract

単射性を持つ関数型プログラムの逆化コンパイラの開発およびウェブを介したサービス提供に向けて,本年度は以下の成果を得た.
●末尾再帰型関数の逆化手法を提案し,末尾再帰型であるすべてのベンチマークに対して停止性および決定性を持つ逆計算プログラムの生成できることを確認した.
●生成したプログラムの関数定義に重なりがある場合に,ナローイング計算を用いた手法で等価で重なりのない関数定義に変更する手法を提案し,すべてのベンチマークで重なりのない関数定義を生成できることを確認した.本手法については次年度に国際会議で発表する予定である
●上記の手法を実装し,本手法のウェブサイトにて変換を実行できるようサービスを開始した.また,ダウンロード用ツールの配布も開始した.
●他グループで提案された逆化手法の一部であるLR解析を利用した決定化手法を改良し,その手法が生成に失敗していた例題に対し,改良後の手法が逆化に成功することを確認した.本結果については次年度に国際会議で発表する予定である.
●関数定義を末尾再帰型に変換する手法である継続渡しスタイルへの変換について,一階プログラム上での既存手法を調査し,匿名関数を含んだ中間結果を経由しない直接的な変換を項書換え系上で定式化し,その正当性を証明した.本結果は,前述の末尾再帰型関数の逆化手法とまとめて,次年度に論文誌に投稿する予定である.
本年度の取り組みにより,ベンチマークにあるプログラムに対して停止性と決定性を持つ逆関数定義を生成できる逆化手法の枠組みを構築し,その変換サービスの提供を開始した.

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本年度の取り組みにより,性質のよい逆関数プログラムを生成する枠組みの構築およびその実装を公開するに至った.その一方で,現在の実装は計算モデルである項書換え系を対象としており,本年度に予定していた実際の関数型プログラムへの適用する変換を実装できなかった.しかし,この部分のみが本研究課題の目標を達成するために残された課題であり,次年度に十分達成できるので,おおむね順調に進展している.

Strategy for Future Research Activity

次年度は本研究課題の最終年度であるので,本年度の成果を国際会議や論文誌に投稿し発表し,成果をまとめる.本研究課題の目標を達成するために残された課題は実装したツールが実際の関数型プログラムに対応するように,前処理・後処理の変換を実装することである.また,逆化手法を評価するためのベンチマークの共通化が本研究分野で早急に取り組むべき課題である.他グループと協議し,共通化したベンチマークを整備することで,逆化手法の分野の研究が活性化するように次年度の研究を進める予定である.

  • Research Products

    (4 results)

All 2011 Other

All Presentation (3 results) Remarks (1 results)

  • [Presentation] On Soundness of CTRS Transformations2011

    • Author(s)
      Naoki Nishida
    • Organizer
      the 35th TRS meeting
    • Place of Presentation
      名古屋大学(名古屋)
    • Year and Date
      2011-09-13
  • [Presentation] Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity2011

    • Author(s)
      Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
    • Organizer
      the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)
    • Place of Presentation
      ノビサド大学(セルビア)
    • Year and Date
      2011-06-01
  • [Presentation] Program Inversion for Tail Recursive Functions2011

    • Author(s)
      Naoki Nishida, German Vidal
    • Organizer
      the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)
    • Place of Presentation
      ノビサド大学(セルビア)
    • Year and Date
      2011-05-31
  • [Remarks]

    • URL

      http://www.trs.cm.is.nagoya-u.ac.jp/repius

URL: 

Published: 2013-06-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi