条件付き項書き換えシステムの十分完全性の自動証明

情報処理学会

書誌事項

タイトル別名
  • Automatically Proving Sufficient Completeness of Conditional Term Rewriting Systems

この論文をさがす

抄録

項書き換えシステム（TRS）は，関数型プログラミング言語の形式的な計算モデルであり，書き換え規則の集合として与えられる．TRSでは，プログラムに関する様々な性質や操作を言語の制約にとらわれず柔軟に取り扱うことが可能である．TRSの拡張として，条件部が加わった書き換え規則を扱う条件付き項書き換えシステム（CTRS）がある．TRS上で，関数がすべての入力に対して解を持つかという性質は十分完全性と呼ばれる．十分完全性の十分条件の1つは停止性と擬簡約性を持つことである．一方，CTRSに対する十分完全性については，代数仕様記述システムMaude上の十分完全性証明システムは報告されているが，理論的な解明に適した枠組みで十分完全性を判定するような証明システムは従来あまり知られていない．本発表では，様々な研究で用いられている基本的なCTRSの体系である指向式3型の左線形な決定的CTRSに対する，十分完全性の自動検証システムの実装について報告する．本システムでは，入力のCTRSをアンラベリング変換を用いて，TRSへ変換する．その後，補パターンアルゴリズムを用いて得られたTRSの擬簡約性を判定する．また，外部ツールを用いて停止性を検証する．これにより与えられたCTRSの十分完全性を証明する．アンラベリング変換は，直観的には，条件の評価を再帰的に行うことで項を書き換えていく操作を，TRSの書き換え規則でエンコードしたものとなっている．補パターンアルゴリズムは，左線形なTRSに対する擬簡約性の判定法である．また，実装システムを使ってデータセットに対して実験を行った結果を報告する．

A term rewriting system (TRS) is a formal computational model of functional programming languages, and is given as a set of rewriting rules. The framework of TRSs allows flexible handling of various properties and operations related to programs without being restricted by language constraints. An extension of TRSs is a framework of conditional term rewriting systems (CTRSs), which handles rewriting rules extended by the conditional part. Sufficient completeness is a property of TRSs that expresses that each function has a solution for all inputs. One of the sufficient conditions of sufficient completeness of a TRS R is that R is terminating and quasi-reducible. For CTRSs, sufficient completeness checker of CTRSs based on an algebraic specification system Maude has been known. However, sufficient completeness checkers for basic frameworks of CTRSs suitable for theoretical investigation have not been known. In this presentation, we report an implementation of an automated verification system of sufficient completeness for left-linear deterministic CTRS of type 3, which is a basic framework of CTRSs adapted in many theoretical research. In this system, the input CTRS is first converted to TRS using the unraveling transformation. Then, the quasi-reducibility of the obtained TRS is checked using the complement pattern algorithm, and the termination of the obtained TRS is verified using external tools. In this way, the sufficient completeness of the given CTRS is proved. Intuitively, unraveling transformation expresses an encoding of conditional rewriting involving recursive evaluation of the condition by the rewriting rules of TRS. The complement pattern algorithm is an method for checking quasi-reducibility of left-linear TRSs. Furthermore, we report experiments on a data set using the implemented sufficient completeness checker.

収録刊行物

キーワード

詳細情報 詳細情報について

  • CRID
    1050001338895234304
  • NII論文ID
    170000180842
  • NII書誌ID
    AA11464814
  • ISSN
    18827802
  • Web Site
    http://id.nii.ac.jp/1001/00200625/
  • 本文言語コード
    ja
  • 資料種別
    article
  • データソース種別
    • IRDB
    • CiNii Articles

問題の指摘

ページトップへ