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

2014 Fiscal Year Research-status Report

項書換えの合流性解析とその応用

Research Project

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

Principal Investigator

廣川 直  北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)

Project Period (FY) 2013-04-01 – 2016-03-31
Keywords項書換え / 合流性 / 国際研究者交流 / オーストリア
Outline of Annual Research Achievements

インスブルック大学、名古屋大学のグループと共同研究を行い次の三つの成果を得た。
現在の合流性解析における困難な問題のひとつは、足し算や掛け算、文字列の連接に代表されるような結合規則や交換規則を含むシステムの解析である。単一化理論と可換性(合流性を一般化した性質)の研究を行い、それらの規則を含む左線形システムに対して、極めて有効な合流性解析の手法を確立した(国際会議 CADE-25 に論文採択済)。
可換性の研究を応用することで、関数型言語の遅延評価の基礎になっている正規化定理に対し簡潔な証明を与えた。この成果と、平成25年度に発表した計算量解析のための手法(RTA-TLCA 2014)を組み合わせることで、基本正規化定理という遅延評価実装に有効な枠組みを構築した(国際ワークショップ IFIP WG 1.6 の招待講演として発表、国際会議 RTA 2015 に論文採択済)。
また合流性を効果的に特徴づける critical-pair-closing system の概念を共同研究により得た(国際ワークショップ IWC 2014 で口頭発表)。
最後に学会活動について。7月にウィーンにおいて3回目となる合流性の自動解析ツールの国際コンペティション(CoCo 2014)をインスブルック大学・東北大学と共催した。また合流性問題の公開データベース Cops の開発・運営を行っているが、そのバックエンドシステムの刷新を行った。

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

    (8 results)

All 2015 2014 Other

All Journal Article (1 results) (of which Peer Reviewed: 1 results,  Open Access: 1 results,  Acknowledgement Compliant: 1 results) Presentation (3 results) (of which Invited: 1 results) Remarks (4 results)

  • [Journal Article] AC-KBO Revisited2015

    • Author(s)
      Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
    • Journal Title

      Theory and Practice of Logic Programming

      Volume: 未定 Pages: 印刷中

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Presentation] CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems2015

    • Author(s)
      Kiraku Shintani and Nao Hirokawa
    • Organizer
      25th International Conference on Automated Deduction
    • Place of Presentation
      ベルリン、ドイツ
    • Year and Date
      2015-08-04 – 2015-08-07
  • [Presentation] Leftmost Outermost Revisited2015

    • Author(s)
      Nao Hirokawa, Aart Middeldorp and Georg Moser
    • Organizer
      26th International Conference on Rewriting Techniques and Applications
    • Place of Presentation
      ワルシャワ、ポーランド
    • Year and Date
      2015-06-29 – 2015-07-01
  • [Presentation] Basic Normalization2014

    • Author(s)
      Nao Hirokawa
    • Organizer
      International Federation for Information Processing (IFIP) Working Group 1.6: Term Rewriting
    • Place of Presentation
      ウィーン、オーストリア
    • Year and Date
      2014-07-13
    • Invited
  • [Remarks] 研究代表のホームページ

    • URL

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

  • [Remarks] 合流性ツール Saigawa

    • URL

      http://www.jaist.ac.jp/project/saigawa/

  • [Remarks] 合流性コンペティション CoCo

    • URL

      http://coco.nue.riec.tohoku.ac.jp/

  • [Remarks] 合流性問題のデータベース

    • URL

      http://cops.uibk.ac.at/

URL: 

Published: 2016-06-01  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi