文献

J-GLOBAL ID：201702273352036227   整理番号：17A0517533

十分完全性を持たない階層的条件付き項書換え系の合流性証明

Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness

著者 (3件)： 黒田貴之 (名古屋大 大学院情報科学研究科) ,  西田直樹 (名古屋大 大学院情報科学研究科) ,  関浩之 (名古屋大 大学院情報科学研究科)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 116  号： 512(SS2016 60-83)  ページ： 103-108  発行年： 2017年03月02日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 条件付き項書換え系(CTRS)における合流性の検証手法として項書換え系への変換を経て証明する手法が知られているが,自然数リストの並び替えを行うCTRSの合流性は証明できていない。このCTRSは関数記号の振舞いが階層的に定義される階層的CTRSとなっており,十分完全性を持っていない。本稿では,十分完全性を持たない階層的CTRSの合流性を証明する手法を提案する。具体的には,条件付き等式に対する書換え帰納法を十分完全性を持たないTRSに拡張し,書換え帰納法を用いて条件付き危険対の条件から別の条件を導出することでその危険対が会同可能であることを示す。次に,書換え規則の条件部が成立することを考慮できる単純化順序を設計し,その単純化順序により階層的CTRSの停止性を証明する手法を提案する。(著者抄録)

シソーラス用語： *項書換え系 ,  *関数型言語 ,  アルゴリズム ,  *帰納的関数 ,  完全性 ,  停止 ,  計算モデル ,  証明 ,  定理 ,  条件 ,  整数 ,  *プログラム検証
準シソーラス用語： 条件付き項書換え系 ,  合流性 ,  書換え帰納法 ,  十分完全性 ,  停止性 ,  条件付き等式

分類 (2件)： 応用プログラミング言語  (JD03052Y) ,  計算理論  (JB02000A)

引用文献 (21件)：

• T. Aoto and S. Stratulat. Decision procedures for proving inductive theorems without induction. In Proc. PPDP 2014, pp. 237-248, ACM, 2014.
• F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998.
• A. Bouhoula. Automated theorem proving by test set induction. J. Symb. Comput., 23(1):47-77, 1997.
• A. Bouhoula and F. Jacquemard. Automated induction for complex data structures. CoRR, abs/0811.4720, 2008.
• N. Dershowitz, M. Okada, and G. Sivakumar. Canonical conditional rewrite systems. In Proc. CADE 1988, vol. 310 of LNCS, pp. 538-549, Springer, 1988.

タイトルに関連する用語 (4件)： 完全性 ,  項書換え系 ,  合流性 ,  証明