JAIST Repository
https://dspace.jaist.ac.jp/Title

非決定計算のための項書き換え理論

Author(s)廣川, 直Citation

科学研究費助成事業研究成果報告書: 1‑4

Issue Date

2013‑05‑31

TypeResearch Paper

Text version

publisher

URL

http://hdl.handle.net/10119/11371

RightsDescription

研究種目：若手研究（Ｂ）, 研究期間：2010〜2012,
課題番号：22700009, 研究者番号：50467122, 研究分
野：項書換え, 科研費の分科・細目：情報学・情報学
基礎Japan Advanced Institute of Science and Technology

様式Ｃ－１９
科学研究費助成事業（科学研究費補助金）研究成果報告書
平成２５年５月３１日現在
機関番号：13302
研究種目：若手研究（Ｂ）
研究期間：2010～2012
課題番号：22700009
研究課題名（和文） 非決定計算のための項書き換え理論
研究課題名（英文） Rewriting Techniques for Non-Deterministic Computation
研究代表者
廣川 直（HIROKAWA NAO）
北陸先端科学技術大学院大学・情報科学研究科・准教授
研究者番号：50467122
研究成果の概要（和文）：
本研究では関数型プログラムや定理証明システムの計算モデルである項書換えシステムに対し、その基礎理論を相対停止性という性質をもとに再考した。その研究成果として、合流性に関する主要二定理（Rosen の直交性と完備性）を左線形の場合に対し統一した。また極大完備化という定理証明ための新たな基盤技術を開発した。これらの新技法を採用した強力な合流性解析ツール Saigawa と自動完備化ツール Maxcomp を開発した。
研究成果の概要（英文）：Term rewriting is a computational model which underlies functional programming andtheorem proving. In this research project we revisited its fundamental theory in the lightof relative termination. As an outcome, we established a new confluence criterion thatunifies two major confluence criteria (Rosen’s orthogonality and Knuth and Bendix’completeness) for left-linear systems. Moreover, we introduced a new technique for
automated deduction, dubbed maximal completion. Based on those new technologies, wedeveloped the powerful confluence analyzer Saigawa and the fully automatic completion
tool Maxcomp.
交付決定額（金額単位：円）2010 年度
2011 年度
2012 年度
年度
年度
総 計

直接経費
1,100,000
1,000,000
800,000

間接経費
330,000
300,000
240,000

2,900,000

870,000

合計
1,430,000
1,300,000
1,040,000

3,770,000

研究分野：項書換え
科研費の分科・細目：情報学・情報学基礎
キーワード：項書換え・合流性・完備化・戦略

１． 研究開始当初の背景
項書換えシステムは、宣言型プログラミング言語や定理証明システムの基礎を成す等式論理のための計算モデルである。計算の非決定性は、計算規則が重なりを持つことによって「直交性」といわれる性質が破壊される時に生じる。直交性が破壊されると、合流性と呼ばれる計算結果の一意性を保証する性質や、関数型言語の遅延評価のように停止しない計算を回避して計算結果に辿り着く保証（正規化戦略）が失われてしまう。
非決定計算はプログラムの最適化や定理証明の本質であるが、既存の理論の大部は計算体系に「停止性」か「直交性」のいずれかを前提にし、非決定計算を扱う理論が欠如している。事実、多くの関数型言語は合流性と正規化戦略の保証のために、関数定義とパターンマッチングの直交性をユーザーに強制している。これは直交性が崩れた場合に、どう合流性を保証し、どう計算すれば計算結果である正規形に辿り着くか、それらを解析する系統的な理論体系がないためである。

２．研究の目的
本研究の目標は、計算の基礎をなす「合流性」に新たな知見を与え、非決定な計算のための項書き換え理論を確立することである。
本研究に先立つ別の研究プロジェクトにおいて、これまであまり注目されていなかった「相対停止性」(Geser 1995)の有用性・柔軟性に気づいた。その知見をもとに、これまで停止性・直交性をベースに作られていた項書換え理論の技法を、相対停止性をベースにして再構成する着想を得た。
本プロジェクトでの目標は以下の通り。
(1) 基礎理論（合流性・戦略）の研究。
（非左線形の場合に対し）既存の停止性・直交性をベースとする合流性の主要２定理（Rosen 1973, Knuth-Bendix 1970）を相対停止性により統一する。またそれに対応する正規化戦略を研究する。
(2) 応用（完備化・E 単一化）の開発。定理
自動証明システムの基盤アルゴリズムである完備化手続き、および直交性がベースであった方程式を解く手法（ナローイング）の枠組みを刷新する。
(3) 前節(1)(2)に基づく自動解析ツール・演繹ツールを実装し評価、一般公開する。
(4) コミュニティの形成。項書換えにおいて停止性と合流性は二大テーマである。停止性研究に関しては、国際ワークショップや停止性自動証明ツールの国際競技会が開催され、研究の国際競争と協調促進の場として極めて有効的に機能している。
合流性研究の発展のため、これと同様の組織を立ち上げる。

３．研究の方法

前節の目標達成のため、停止性・完備化の研究を行っている Middeldorp インスブルック大学教授のグループと連携し、以下の事項に取り組んだ。
(1) 基礎理論（合流性・戦略）の研究。危険対ステップという概念を導入し、その相対停止性が合流性の十分条件であることを 示 し 、 さ ら に こ の 条 件 下 で fullsubstitution, 並列最外戦略, 根必須戦
略が正規化戦略になることを証明する。
直交性と Knuth-Bendix の定理を統合した後は development closedness というもう一つの主要な定理も統合する計画であった。しかしこれは他研究者に先を越されたため、方針を転換。より難易度の高い、非左線形システムのための新たな合流性定理の創出に取り組んだ。
(2) 応用（完備化・E 単一化）の開発
定理自動証明および E 単一化は、停止性と合流性の理論を組み合わせた技術によって成り立っている。当初、この停止性の部分を相対停止性に緩和し、より一般的な枠組みを得る計画を立てていた。
しかし研究を進めるにつれ、そのような体系を実現するには、そもそも柔軟で実装の容易な枠組みが欠如しているとの結論に至った。停止性の自動解析が SAT やSMT ソルバにより容易かつ高速になったことにヒント得、SAT/SMT ソルバを用いたアプローチを試みた。
(3) 上述の合流性・完備化に関する理論成果を実装し、評価を行う。完備化の問題集はインスブルック大学のグループが編纂したものがあり、それを使用した。一方、合流性の問題集は各研究グループが独自に編纂しており、まずそれらを統合する必要がある。そのため、各国のグループが共通で利用できる問題集データベース(COnfluence ProblemS Database, Cops)を開発・一般利用できるように公開した。
(4) 学会発足。共同研究を行っているインスブルック大学および東北大学のグループと連携し、合流性に関するワークショッ
プ、合流性ツールの国際競技会の発足のため、IEEE IFIP Working Group 1.6(Rewriting)、RTA Steering Committeeとの交渉を行った。また合流性問題のデータベースのプロトタイプシステムを構築後、インスブルック大学のグループとともに実システム構築を行った。

４．研究成果

研究(B) No. 25730004）へと引き継ぐ。

(1) 基礎理論（合流性・戦略）に関する成果(3) 自動解析・演繹ツール① 主要２定理の統合。前述のとおり、左線形システムに対し Rosen の直交性条件(1973)と Knuth-Bendix の合流性条件(1970)を統合する定理を得た。さらにそれを弱直交性を包含する定理へと拡張した。これら定理は危険対ステップの相対停止性という条件に基づいており、さらなる拡張が強く期待される。
② 非左線形・非停止システムのための合流性の十分条件。前項の定理は左線形性に限定されたものであるが、その制限を受けない Knuth-Bendixの合流性条件を拡張する定理を得た。
E 危険対の合流性、相対停止性、そし て strong non-overlappingnessに基づいている。
③ 前項①で得た合流性の十分条件を満た す と き full substitution
strategy が正規化戦略になることを示した。並列最外戦略・ルート必須戦略もまた正規化戦略になると予想し、長らく取り組んだが、証明することはついにできなかった。
(2) 応用（自動演繹）に関する成果① MaxSAT に基づく高効率な完備化手続き「極大完備化」を開発した。完備化は Knuth-Bendix (1970)が発案した一階の定理自動証明の基盤アルゴリズムであるが、適切な簡約順序を人が指定する必要があった。その克服のため Kurihara & Kondo (1999)
は多重完備化という手法を開発していた。本手法はそれとは完全に独立した手法で同等以上の効率を実現した。MaxSAT ソルバを用いるその実装は極めて簡潔かつ容易である。
② 極大完備化を実際の（一階・帰納的）定理証明に適用させる「制約等式」という枠組みを開発した。

研究で得られた手法に基づく合流性ツール
Saigawa と完備化ツール Maxcomp を実装・公開した。下表はそれらと競合ツールの実験結果。問題集は(4)-③、学会発表文献①を参照。
合流性ツールの評価 (125 の合流性問題)
ACP
CSI
Saigawa
証明
78 個
67 個
71 個
反証
18 個
21 個
18 個
完備化ツールの評価（115 の完備化問題）
mkbTT Slothrop Maxcomp
成功
81 個
71 個
86 個

(4) 学会組織① 合流性に関する国際ワークショップ
IWC の 発 足 し 、 第 １ 回 IWC 2012(chair: 廣川・Middeldorp インスブ
ルック大学教授)を共催した。第 2回 IWC 2013 (chair: 廣 川 ・ vanOostrom ユトレヒト大教授)はオランダ Eindhoven で開催予定。
② 合流性解析ツールの国際競技会
CoCo を青戸等人准教授（東北大学）、Harald Zankl 研究員（インスブルック大学）とともに設立。第１回競技会を IWC 2012 において行った。
③ 合流性ツールの評価・検証において必要になる、合流性問題のデータベース Cops を、インスブルック大学のグループと共同開発し、公開した。
５．主な発表論文等（研究代表者、研究分担者及び連携研究者には下線）〔雑誌論文〕（計２件）③ ベーシックナローイングと完備化ツールを組み合わせた E 単一化のための萌芽的な枠組みを得た。

① Nao Hirokawa, Aart Middeldorp, andHarald Zankl.
UncurryingforTerminationandComplexity.
Journal of Automated Reasoning 50(3),pp. 279-315, 2013. 査読有(2)-②③の成果はまだ萌芽的な段階である。これらの研究は(1)-③の問題解決とともに、次年度以降の研究課題（若手② Nao Hirokawa and Aart Middeldorp.
Decreasing Diagrams and RelativeTermination.

Journal of Automated Reasoning 47(4),pp. 481-501, 2011. 査読有〔学会発表〕（計４件）① Dominik Klein and Nao Hirokawa.
Confluence of Non-Left-Linear TRSs via
Relative Termination.
Proceedings of the 18th International
Conference on Logic for Programming,
Artificial Intelligence and Reasoning,Merida, Venezuela. Lecture Notes inComputer Science 7180, pp. 258-273,
2012 査読有2012 年 3 月 11 日発表② Dominik Klein and Nao Hirokawa.
Maximal Completion.
Proceedings of the 22nd International
Conference on Rewriting Techniques andApplications, Novi Sad, Serbia.
Leibnitz International Proceedings inInformatics 10, pp. 71-80, 2011. 査読有2011 年 5 月 31 日発表③ Harald Zankl, Nao Hirokawa, and AartMiddeldorp.
Uncurrying for Innermost Termination
and Derivational Complexity
Proceedings of the 5th International
Conference on Higher-Order Rewriting,Edinburgh, UK. Electronic Proceedingsin Theoretical Computer Science 49, pp.
46-57, 2011. 査読有
doi:10.4204/EPTCS.49.4
2011 年 7 月 14 日発表④ Nao Hirokawa and Aart Middeldorp.
Decreasing Diagrams and RelativeTermination.
Proceedings of the 5th International
Joint
Conferenceon
Automated
Reasoning, Edinburgh, UK. Lecture
Notes in Artificial Intelligence 6173,pp. 487-501, 2010. 査読有2010 年 7 月 19 日発表〔その他〕
ホームページ等① 研究代表者のホームページ：
http://www.jaist.ac.jp/~hirokawa/② 合流性ツール Saigawa のウェブサイト：

http://www.jaist.ac.jp/project/saiga
wa/③ 完備化ツール MaxComp のウェブサイト：
http://www.jaist.ac.jp/project/maxco
mp/④ 第１回合流性に関する国際ワークショッ
プ (IWC 2012)：
http://cl-informatik.uibk.ac.at/even
ts/iwc-2012/⑤ 第１回合流性ツールの国際競技会 (CoCo2012)：
http://coco.nue.riec.tohoku.ac.jp/
６．研究組織(1)研究代表者
廣川 直（HIROKAWA NAO）
北陸先端科学技術大学院大学・情報科学研
究科・准教授研究者番号：50467122(2)研究分担者 なし(3)連携研究者 なし(4)研究協力者① MIDDELDORP AART (ミデルドープ アート)
University of Innsbruck・Institute for
Computer Science・Professor② KLEIN DOMINIK (クライン ドミニク)
北陸先端科学技術大学院大学・情報科学研究科・博士後期課程学生（当時）