日本ソフトウェア科学会第 35 回大会 (2018 年度) 講演論文集

無限のデータを含む等式に対する帰納的定理証明
菊池 健太郎篠埜 功

本稿では、停止性を持たない関数を含む等式に対する帰納的定理の証明法について議論する。項書き換えシステムにおける潜在帰納法は、停止性が成り立たない場合にも適用できることが知られているが、全ての基底項が値に到達するまで書き換え可能であること (十分完全性) が条件となっている。本研究では、帰納的定理の証明のためには、十分完全性が、全ての基底項に対してではなく、証明すべき等式の両辺に基底代入を適用した項に対してのみ成立すればよいことを利用する。提案手法による証明の具体例として、遅延評価の関数型言語におけるプログラムの性質を、合流性自動判定システムを用いて示す。

1 はじめに
等式論理における帰納的定理の証明は、代数的仕様の検証において以前より使用されているが、近年では証明支援システムを用いた検証においても頻繁に用いられている。それらの証明では、等式理論に含まれる関数が停止性を満たすことを条件としている場合が多く、停止性を持たない関数を含む等式理論の上での帰納的定理の証明ついて議論されることはあまり多くない。
項書き換えシステム (TRS) における帰納的定理の証明法である潜在帰納法は、TRS が停止性を持たな

data Nat = Z | Suc Nat deriving Show
replicate1 Z = []replicate1 (Suc n) = Suc Z : replicate1 n
mytake (Z, xs) = []mytake (Suc n, []) = []mytake (Suc n, x:xs) = x : mytake (n, xs)
repeat1 = Suc Z : repeat1{- 示したい等式
repliate1 m = mytake (m, repeat1)-}
図1

Haskell プログラム例

い場合にも適用できることが知られている [3] [4]。しかしながら、対象となる TRS で扱われる全ての基底明例は提供されてこなかった。

項 (変数を含まない項) が正規形あるいは値に到達す

本稿では、上述の条件を緩めることにより、基底るまで書き換え可能であることを条件としているた項が必ずしも値まで書き換え可能とは限らない TRS

め、停止性を持たない実際的なプログラムの性質の証においても潜在帰納法が適用できることを説明する。例として、図 1 の Haskell プログラムに対応するInductive theorem proving for equations with infinite
data
Kentaro Kikuchi, 東 北 大 学 電 気 通 信 研 究 所, Research Institute of Electrical Communication, Tohoku University.
Isao Sasano, 芝浦工業大学工学部情報工学科, Departmentof Information Science and Engineering, Shibaura
Institute of Technology.

TRS(図 2) について潜在帰納法の適用を考える。(この TRS では、無限リストを生成する基底項 repeat1が値まで書き換え可能ではない。) また、潜在帰納法の適用条件の一つである合流性の判定に対しては、合流性自動判定システムの利用を提案する。

 replicate1 (Z) → Nil
replicate1 (Suc(n))
→ Cons(Suc(Z), replicate1 (n))
 mytake(Z, xs) → NilR
mytake(Suc(n), Nil ) → Nil





mytake(Suc(n), Cons(x, xs))





→ Cons(x, mytake(n, xs))
repeat1 → Cons(Suc(Z), repeat1 ){Hreplicate1 (m) → mytake(m, repeat1 )あり、R ∪ {s → t} は合流性を持つので、v と v ′ は同∗∗じ値である。よって、sθg →R v = v ′ ←R tθg となり∗sθg ↔R tθg が成立する。
s θg −−−−−→ t θg{s→t}∗yR∗yRvv′
by CR of R ∪ {s → t}

例 3. 定理 2 の適用例として、図 2 の TRS R と等式.
replicate1 (m) = mytake(m, repeat1 ) を考える。この等式の両辺の項は R のもとで十分完全であることが示せる。{replicate1 (m) → mytake(m, repeat1 )} を

図2

図 1 の Haskell プログラムに対応する TRSH とすると、R ∪ H の合流性は、合流性自動判定シス
テム ACP [1] を用いて示すことができる (図 3)。した.
がって、replicate1 (m) = mytake(m, repeat1 ) は R

2 潜在帰納法による帰納的定理証明の帰納的定理であることがいえる。このことは、図 1

TRS の基本事項については省略する (文献 [2] を参照)。項は多ソート 1 階述語論理の場合と同様に定義の Haskell プログラムにおいて、示したい等式の両辺の評価結果が常に等しいことを意味する。

され、関数記号は構成子と定義関数記号に分かれているものとする。関数記号として構成子のみを含む項を構成子項とよび、そのうち基底項であるものを基底構成子項あるいは値とよぶ。代入のうち値域が基底項からなるものを基底代入とよぶ。

3 おわりに
本稿では、十分完全性の条件を緩めることにより、基底項が必ずしも値まで書き換え可能でない TRS においても潜在帰納法が適用できることを示した。また、

定義 1 (項に対する十分完全性). TRS R と項 t に対して以下が成り立つとき、t は R のもとで十分完全であるという: 任意の基底代入 θg に対してある値 v∗が存在して tθg →R v となる。
.
等式 s = t が TRS R の帰納的定理であるとは、任∗意の基底代入 θg に対して sθg ↔R tθg が成り立つことをいう。次の定理は、証明すべき等式の両辺の項に対してのみ十分完全性を要求するという点で、従来の潜在帰納法 [3] [4] の拡張となっている。
.
定理 2. 等式 s = t と TRS R に対して以下が成り立つとする。

その具体例として、無限リストを生成する Haskell プログラムに対応する TRS に対して帰納的定理を証明した。
潜在帰納法の適用条件の一つである合流性の判定に対しては、近年開発が進んでいる合流性自動判定システムを利用することが有効である。一方、もう一つの適用条件である項に対する十分完全性を判定する手続きを提案することは、今後の課題である。また、多相型と高階関数を持つ関数型プログラムの帰納的性質を証明するための枠組みを構築することも今後の課題である。

1. s と t は R のもとで十分完全である。
2. TRS R ∪ {s → t} は合流性を持つ。

謝辞 本研究の一部は日本学術振興会研究拠点形成

3. 任意の値は R ∪ {s → t} における正規形である。
.
このとき、s = t は R の帰納的定理である。

国際研究拠点形成」および日本学術振興会科学研究

証明．s と t は R のもとで十分完全であるから、任意の費助成事業 基盤研究 (C) 16K00091、基盤研究 (C)′∗

基底代入 θg に対してある値 v, v が存在して sθg →R v∗

かつ tθg →R v ′ となる。また、sθg →R∪{s→t} tθg で事業 (A. 先端拠点形成型) 「数理論理学とその応用の16K00106、基盤研究 (C) 17K00005 の補助を得て行われた。

YES
Rewrite Rules:[ replicate1(Z) -> Nil,replicate1(Suc(?n)) -> Cons(Suc(Z),replicate1(?n)),mytake(Z,?xs) -> Nil,mytake(Suc(?n),Nil) -> Nil,mytake(Suc(?n),Cons(?x,?xs)) -> Cons(?x,mytake(?n,?xs)),
repeat1 -> Cons(Suc(Z),repeat1),
replicate1(?m) -> mytake(?m,repeat1) ]Apply Direct Methods...
Inner CPs:
[ ]Outer CPs:
[ Nil = mytake(Z,repeat1),
Cons(Suc(Z),replicate1(?n)) = mytake(Suc(?n),repeat1) ]Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Linearunknown Development Closed
unknown Strongly Closedunknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ mytake(Z,repeat1) = Nil,mytake(Suc(?n),repeat1) = Cons(Suc(Z),replicate1(?n)),Nil = mytake(Z,repeat1),
Cons(Suc(Z),replicate1(?n_1)) = mytake(Suc(?n_1),repeat1) ]unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <mytake(Z,repeat1), Nil> by Rules <6, 0> preceded by []joinable by a reduction of rules <[([],2)], []>Critical Pair <mytake(Suc(?n),repeat1), Cons(Suc(Z),replicate1(?n))> by Rules <6, 1> preceded by []joinable by a reduction of rules <[([(mytake,2)],5),([],4)], [([(Cons,2)],6)]>
Satisfiable by 3,2,7,6>1,5,4; Suc(0)Cons(0,0)mytake(0,0)replicate1(0); 5>6,2>7>3>4,1
Diagram Decreasing
Direct Methods: CR
Final result: CR
replicate1.trs: Success(CR)(3 msec.)
図3

図 2 の TRS R ∪ H に対する合流性自動判定システム ACP の出力

参 考 文 献[ 1 ] ACP (Automated Confluence Prover). http://www.nue.ie.niigata-u.ac.jp/toyama/tools/acp/[ 2 ] F. Baader and T. Nipkow. Term Rewriting andAll That. Cambridge University Press, 1998.

[ 3 ] 小池広高, 外山 芳人. 潜在帰納法と書換え帰納法の比較. コンピュータソフトウェア, 17(6):1–12, 2000.
[ 4 ] Y. Toyama. How to prove equivalence of term
rewriting systems without induction. TheoreticalComputer Science, 90(2):369–390, 1991.