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

Study of Program Inversion for Functional Programs Defining Injective Functions

Research Project

Project/Area Number 21700011
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionNagoya University

Principal Investigator

NISHIDA Naoki  名古屋大学, 情報科学研究科, 助教 (00397449)

Project Period (FY) 2009 – 2012
Project Status Completed (Fiscal Year 2012)
Budget Amount *help
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2011: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2010: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Keywordsプログラム逆化 / プログラム変換 / 項書換え系 / 関数型言語 / 情報基礎 / 逆関数 / 単射性 / ログラム変換
Research Abstract

In this research, we aimed at applying program inversion methods that automatically generate inverse computation programs, into practical functional programs, and we developed a program inversion method that inverts a given program to a function-definition set which is deterministic with respect to function application, namely a program. To apply the method into several functional languages, as target programs, we dealt with term rewriting systems of which the class is known as a computation model of functional programs. First, we proposed a new inversion transformation that specializes in tail recursive functions, and then incorporated it into the program inversion method developed at our previous work. Next, we proposed a method for determinizing rewrite rules that are indeterministic with respect to application of rules. More precisely, with preserving desired computation, the method instantiates each of the rules by analyzing the right-hand side by means of narrowing computation. By using the method as a postprocess of the inversion method, we succeeded in improving the existing inversion method. Finally, we implemented the inversion method and provided a service of inversion via web browsers.

Report

(5 results)
  • 2012 Annual Research Report   Final Research Report ( PDF )
  • 2011 Annual Research Report
  • 2010 Annual Research Report
  • 2009 Annual Research Report
  • Research Products

    (26 results)

All 2012 2011 2010 2009 Other

All Journal Article (8 results) (of which Peer Reviewed: 7 results) Presentation (14 results) Remarks (4 results)

  • [Journal Article] Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity2012

    • Author(s)
      Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
    • Journal Title

      Logical Methods in Computer Science

      Volume: Vol. 8, No. 3 Pages: 1-49

    • NAID

      120005530823

    • Related Report
      2012 Final Research Report
    • Peer Reviewed
  • [Journal Article] Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity2012

    • Author(s)
      Naoki Nishida,, Masahiko Sakai, and Toshiki Sakabe
    • Journal Title

      Logical Methods in Computer Science

      Volume: 8 Pages: 1-49

    • DOI

      10.2168/lmcs-8(3:4)2012

    • NAID

      120005530823

    • Related Report
      2012 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Termination of Narrowing via Termination of Rewriting, Applicable Algebra in Engineering2010

    • Author(s)
      Naoki Nishida and German Vidal
    • Journal Title

      Communication and Computing

      Volume: Vo l . 21, No. 3 Pages: 177-225

    • Related Report
      2012 Final Research Report
    • Peer Reviewed
  • [Journal Article] Termination of Narrowing via Termination of Rewriting2010

    • Author(s)
      Naoki Nishida, German Vidal
    • Journal Title

      Applicable Algebra in Engineering, Communication and Computing

      Volume: 21 Pages: 177-225

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Completion after Program Inversion of Injective Functions2009

    • Author(s)
      Naoki Nishida and Masahiko Sakai
    • Journal Title

      Electronic Notes in Theoretical Computer Science

      Volume: Vol. 237 Pages: 39-56

    • Related Report
      2012 Final Research Report
    • Peer Reviewed
  • [Journal Article] Completion after Program Inversion of Injective Functions2009

    • Author(s)
      Naoki Nishida, Masahiko Sakai
    • Journal Title

      Electronic Notes in Theoretical Computer Science 237

      Pages: 39-56

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Improving the Termination Analysis of Narrowing in Left-Linear Constructor Systems2009

    • Author(s)
      Jose Iborra, Naoki Nishida, German Vidal
    • Journal Title

      Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation

      Pages: 48-56

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 条件付き等式の変換に基づくプログラム生成2009

    • Author(s)
      長島正憲, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗
    • Journal Title

      信学技報 109

      Pages: 37-42

    • NAID

      120005527807

    • Related Report
      2009 Annual Research Report
  • [Presentation] Computing More Specific Versions of Conditional Rewriting Systems2012

    • Author(s)
      Naoki Nishida and German Vidal
    • Organizer
      the 22nd International Symposium on Logic-Based Program Synthesis and Transformation
    • Place of Presentation
      ルーベン(ベルギー)
    • Year and Date
      2012-09-20
    • Related Report
      2012 Final Research Report
  • [Presentation] Extending Matching Operation in Grammar Program for Program Inversion2012

    • Author(s)
      Minami Niwa, Naoki Nishida, and Masahiko Sakai
    • Organizer
      the 22nd International Symposium on Logic-Based Program Synthesis and Transformation
    • Place of Presentation
      ルーベン(ベルギー)
    • Year and Date
      2012-09-20
    • Related Report
      2012 Final Research Report
  • [Presentation] More Specific Term Rewriting Systems2012

    • Author(s)
      Naoki Nishida and German Vidal
    • Organizer
      the 21st International Workshop on Functional and (Constraint) Logic Programming
    • Place of Presentation
      名古屋
    • Year and Date
      2012-05-29
    • Related Report
      2012 Final Research Report
  • [Presentation] On Soundness of CTRS Transformations2011

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

    • Author(s)
      Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
    • Organizer
      the 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applicationthe 22nd International Conference on Rewriting Techniques and Applications
    • Place of Presentation
      ノビサド(セルビア)
    • Year and Date
      2011-06-01
    • Related Report
      2012 Final Research Report
  • [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
    • Related Report
      2011 Annual Research Report
  • [Presentation] Program Inversion for Tail Recursive Functions2011

    • Author(s)
      Naoki Nishida and German Vidal
    • Organizer
      the 22nd International Conference on Rewriting Techniques and Applications
    • Place of Presentation
      ノビサド(セルビア)
    • Year and Date
      2011-05-31
    • Related Report
      2012 Final Research Report
  • [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
    • Related Report
      2011 Annual Research Report
  • [Presentation] Proving Injectivity of Functions via Program Inversion in Term Rewriting2010

    • Author(s)
      Naoki Nishida and Masahiko Sakai
    • Organizer
      the 10th International Symposium on Functional and Logic Programming
    • Place of Presentation
      仙台
    • Year and Date
      2010-04-21
    • Related Report
      2012 Final Research Report
  • [Presentation] Proving Injectivity of Functions via Program Inversion in Term Rewriting2010

    • Author(s)
      Naoki Nishida, Masahiko Sakai
    • Organizer
      the 10th International Symposium on Functional and Logic Programming
    • Place of Presentation
      東北大学(宮城県)
    • Year and Date
      2010-04-20
    • Related Report
      2010 Annual Research Report
  • [Presentation] 制約付き等式の定理自動証明器の試作2009

    • Author(s)
      西田直樹, 中林直生, 酒井正彦, 草刈圭一朗, 坂部俊樹
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      松江
    • Year and Date
      2009-09-17
    • Related Report
      2009 Annual Research Report
  • [Presentation] Extending Matching Operation in Grammar Program for Program Inversion

    • Author(s)
      Minami Niwa, Naoki Nishida, and Masahiko Sakai
    • Organizer
      the 22nd International Symposium on Logic-Based Program Synthesis and Transformation
    • Place of Presentation
      Leuven, Belgium
    • Related Report
      2012 Annual Research Report
  • [Presentation] Computing More Specific Versions of Conditional Rewriting Systems

    • Author(s)
      Naoki Nishida and German Vidal
    • Organizer
      the 22nd International Symposium on Logic-Based Program Synthesis and Transformation
    • Place of Presentation
      Leuven, Belgium
    • Related Report
      2012 Annual Research Report
  • [Presentation] More Specific Term Rewriting Systems

    • Author(s)
      Naoki Nishida and German Vidal
    • Organizer
      the 21st International Workshop on Functional and (Constraint) Logic Programming
    • Place of Presentation
      Nagoya, Japan
    • Related Report
      2012 Annual Research Report
  • [Remarks]

    • URL

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

    • Related Report
      2012 Final Research Report
  • [Remarks] プログラム逆化ツールREPIUSのwebページ

    • URL

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

    • Related Report
      2012 Annual Research Report
  • [Remarks]

    • URL

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

    • Related Report
      2011 Annual Research Report
  • [Remarks]

    • URL

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

    • Related Report
      2010 Annual Research Report

URL: 

Published: 2009-04-01   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi