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

余帰納法に基づく定理証明の自動化
四宮 誠一

海野 広志

本研究では、余帰納的に定義された述語に関する定理のための自動証明法を提案する。そのような述語を用いると、ストリーム・無限木といった無限データ構造や循環データ構造に関する性質を記述したり、プログラムの無限実行トレースの集合を表現したりすることが可能であるため、プログラムの検証にも応用できる。本研究では、余帰納的定理証明の自動化のため、証明システムを定式化し、SMT ソルバを用いた証明探索法を提案する。また、提案手法を実装し、関連手法との比較実験を行った。

無限リスト全体の集合である。

1 はじめに

図 1 は余帰納法を用いて証明できる定理の例で本研究は余帰納法と呼ばれる定理証明法を自動化すあり、本研究で実装した自動証明ツールへの入力例るための手法を提案する。余帰納法とは、数学的帰納でもある。この述語定義の記法は L. Simon らの提法に代表される帰納法と対照的な証明法である。帰納唱する co-LP(co-Logic Programming) [1] の記法と法は自然数全体の集合や有限長のリスト全体の集合なほぼ同じであり、違いは大文字が関数を表し小文字

どの、帰納的に定義された集合に関する定理証明に用が変数を表すという点だけである。co-LP の述語定いられる。一方で、余帰納法は無限長のリスト全体の義の記法はプログラミング言語 Prolog と全く同じ集合や無限長のツリー全体の集合などの、余帰納的にだが、述語を余帰納的に解釈する点が異なる。す定義された集合に関する定理証明に用いられる。余帰なわち、述語の定義文から一意に定まる関数 F を納的に定義された集合は、次のように定式化される。

用いて、F に対応する集合 νF として述語を定義する。例えば図 1 の述語 lexOrder に対応する F は

定義 1.1 (余帰納的に定義された集合 νF ) 台集
合を L として、単調関数 F : 2L → 2L に関して

S ⊆ F (S) を満たす集合 S のうち最大のものを
余帰納的に定義された集合と呼び、νF と書く。
例えば単調増加数列全体を集めた集合は F (S) ={Cons(x1, Cons(x2, xs)) | x1 < x2 ∧ Cons(x2, xs) ∈S} に対応する集合 νF である。このとき台集合 L は次のようになる。F (S)(x1, x2) = ∃a, as, b, bs.(x1 =Cons(a, as) ∧ x2 = Cons(b, bs) ∧ a < b) ∨ (x1 =Cons(a, as) ∧ x2 = Cons(b, bs) ∧ a = b ∧ S(as, bs))
また、assert 文では上で定義した述語を用いて定理を記述する。|= の左側を前提部と呼び、右側を帰結部と呼ぶ。前提部の中のコンマは論理積を意味する。帰結部は述語変数適用（p(x, y) など）ただ 1 つでなければならない。assert 文の中の変数はすべて全称量化∗ Automating Coinductive Theorem Prooving.

This is an unrefereed paper. Copyrights belong tothe Authors.
Seiichi Shinomiya, Hiroshi Unno, 筑波大学大学院 シス
テム情報工学研究科, Graduate School of Systems andInformation Engineering, University of Tsukuba.

される。本研究の手法で証明に成功すると、証拠として証明手順を表す証明木が得られる。
本論文は 4 つの節で構成される。第 2 節では自動証明手法を解説する。第 3 節では実装したツールの実験結果を述べる。第 4 節では関連研究との比較をl e x O r d e r ( Cons ( a , a s ) , Cons ( b , bs ) ) :− a < b .
l e x O r d e r ( Cons ( a , a s ) , Cons ( b , bs ) ) :− a = b , l e x O r d e r ( as , bs ) .
a s s e r t ( l e x O r d e r ( x , y ) , l e x O r d e r ( y , z ) |= l e x O r d e r ( x , z ) ) .
図1

無限リスト上の辞書式順序の推移律

定理 n ∈ {1, 2, 3, ...} ∧ S ⊆ F n (S) ⇒ S ⊆ νF を行う。

ジャッジメントに適用する規則である。F n は関数 F2 自動証明手法

を n 回合成した関数を表す。余帰納法の原理とは次

本研究の提案手法では与えられた述語定義文との定理のことである。

assert 文を元に初期ジャッジメントを作り、ジャッジメントに対して図 2 の推論規則を適用していくことで証明を行う。ジャッジメントとは推論規則中のD; A; ϕ ⊢ C のことを指す。D は述語の定義の集合、A は前提部の論理式に含まれる述語変数適用を集めた集合、ϕ は前提部の論理式から述語変数適用を除いた論理式、C は帰結部の論理式である。
ジャッジメント D; A; ϕ ⊢ C は各述語変数を余帰納∧的に解釈したもとで A ∧ ϕ ⇒ C が妥当であることを意味する。余帰納的な解釈とは、co-LP と同様の方法 [1] で D の述語定義文から関数 F を抽出し、F に対応する集合 νF として各述語変数の意味を与えることを指す。

定理 2.1 (余帰納法の原理) 台集合を L として、任意の単調関数 F : 2L → 2L と任意の集合 S に対して S ⊆ F (S) ⇒ S ⊆ νF が成り立つ
例 え ば 図 1 の assert 文 の 内 容 は S(as, cs) =∃bs.lexOrder(as, bs) ∧ lexOrder(bs, cs) とし、νF =lexOrder とすれば S ⊆ νF と同値である。そのため
余帰納法の原理を適用して、S ⊆ F (S) を意味するジャッジメントに帰着できる。

COINDUCT 規則で使われている記号の意味は次の通り。fvs は与えられた論理式中に出現する変数の集合を返す関数である。xe は変数の列である。{ex} は変数の列を変数の集合として扱うことを表す。\ は集D::={d1 , ..., dm }d::=P (et) :- ϕ1 , ..., ϕm , P1 (et1 ), ..., Pk (etk ).

t::=x | n | true | false | f (et) | t1 + t2 | t1 ∗ t2

ϕ::=t 1 < t 2 | t 1 = t 2 | ϕ1 ∧ ϕ2 | ⊤A::={P1 (et1 ), ..., Pm (etm )}C::=t 1 < t 2 | t 1 = t 2 | C1 ∧ C2 | C1 ∨ C2| P (et) | ∃x.C

ここで t は項を表すメタ変数であり、P は述語変数を表すメタ変数である。x は項の変数を表し、n は整数の定数を表す。また、f は Cons などの構成子を表すメタ変数である。ただし t1 + t2 と t1 ∗ t2 と t1 < t2は整数型の項にのみ定義される。
図 1 の assert 文 の 場 合 、初 期 ジャッジ メ ン トは A = {lexOrder(x, y), lexOrder(y, z)}, ϕ = ⊤,C = lexOrder(x, z) となる。
COINDUCT 規則は余帰納法の原理を一般化した合の差の演算子である。X はジャッジメントの前提部にのみ現れる変数の集合である。∃X は変数の集合の各要素を存在量化変数として扱うことを表す。F は帰結部の述語 νF を定義するために用いられた関数を表す。

UNFOLD 規則はジャッジメントの前提部の述語変数適用を述語の定義にしたがって展開する推論規則である。lexOrder のように 2 つ以上の節で定義される述語を展開する場合は証明木が枝分かれする。

VALID 規則は、証明木の枝を閉じるための推論規則である。この規則が適用できるのは妥当性判定に成功したときに限られる。妥当性判定とはジャッジメン
トの前提部の論理式が真のとき帰結部の論理式も真であることの判定である。本研究では、ジャッジメント∧D; A; ϕ ⊢ C を論理式 A ∧ ϕ ⇒ C に変換して、代表的な SMT ソルバの 1 つである Z3 [2] に解かせる

X = fvs(∧A ∧ ϕ) \ {ex}n ∈ {1, 2, 3, ...}

S = λex.∃X.

∧A∧ϕD; A; ϕ ⊢ F (S)(ex)n(COINDUCT)

D; A; ϕ ⊢ νF (ex)P (et) ∈ A

σ = {ex 7→ et}(for each (P (ex) :-∧D; A ∪ σA′ ; ϕ ∧ σϕ′ ⊢ C′|=′A ∧ ϕ ) ∈ D)

D; A; ϕ ⊢ C
図2(UNFOLD)∧A∧ϕ⇒C

D; A; ϕ ⊢ C(VALID)

提案手法の推論規則

ことで妥当性判定を行う。Z3 は代数的データ型と未UNFOLD 規則を適用する述語変数適用は幅優先探

解釈関数を扱う機能を持っている。ジャッジメントを索の順序で選ぶ。すなわち、未展開の述語変数適用論理式に変換する際に、述語は Bool 型の値を返す未はキューで管理し、先頭の述語変数適用を UNFOLD解釈関数としてエンコードし、Cons などの関数記号対象とする。UNFOLD 規則によって新たに追加されは代数的データ型のコンストラクタとしてエンコーた述語変数適用はキューの末尾に入る。

ドする。このエンコードに基づく妥当性判定は健全だが完全ではない。

2. 1 推論規則の適用戦略
本研究では次の戦略に従って推論規則を適用することで定理を証明する。

1. k = 1 とする
2. 与えられた入力から作ったジャッジメントにCOINDUCT 規則 (n = k) を適用する
3. もし妥当性判定の結果が成功なら VALID 規則を適用して証明木の枝を閉じる

4. もし妥当性判定の結果が失敗なら(a) もし UNFOLD 規則の適用回数が閾値を超えていたら k = k + 1 として手順 2 に戻って証明を再試行する

上記の手法で lexOrder の推移律 (図 1) を証明すると、次のような証明木が生成される。

COINDUCT| UNFOLD l e x O r d e r ( x , y )| | UNFOLD l e x O r d e r ( y , z )| | | VALID| | | VALID| | UNFOLD l e x O r d e r ( y , z )| | | VALID| | | VALID

3 実験結果
上記の自動証明手法を実装し、既存の余帰納的定理の証明ツールである Circ [3] のオンライン・デモ・(b) UNFOLD 規則を適用し、生成された各ページに掲載されているサンプルコードの定理群を自ジャッジメントに対して手順 3 から証明を動証明させる実験を行った。61 個の定理のうち、14行う個の定理の証明に成功し、47 個の定理の証明に失敗

本来、UNFOLD 規則は無限に適用し続けることがした。成功率が低い原因を分析したところ、Circ のできる。しかし UNFOLD 規則を何回か適用すると、サンプルコードで用いられている再帰関数には自分それ以上 UNFOLD しても意味がない述語変数適用、自身だけでなく他の再帰関数も呼び出すような複雑すなわち妥当性判定の結果に影響を及ぼさないようなものが多く含まれており、提案手法ではそのようなな述語変数適用が現れる。そこで、UNFOLD 規則の再帰関数にうまく対応できていないことが分かった。

適用回数が一定値を超えたら証明を一旦打ち切り、k

また、そのような再帰関数に関する定理を証明するにを 1 増やして COINDUCT 規則を適用し直して証明

は、COINDUCT 規則を適用する前に UNFOLD 規を再試行する。

則を何度か適用するとうまくいく可能性があることが分かった。提案手法を改良し、そのような再帰関数に対応できるようになると実験結果は大幅に改善で表1

実験結果きると考えられる。一方、サンプルコードを Circ に定理証明させたところ全ての定理の証明に成功した。これ

lexOrder の推移律

✓××

は Circ で証明できる定理だけをサンプルコードとしlexOrder の反射律✓✓×て掲載したためだと考えられる。そのため、この定理

lexOrder の反対称律

✓

✓

×

群は各ツールの性能を比較するためのベンチマークinc(s) ⇒ inc(even(s))✓××セットとしては不適切と言える。

zip1(s, t) = zip2(s, t)✓×✓

我々は余帰納法を用いる定理証明器のために広く提案手法 Dafny Circzip1(even(s), odd(s)) = s××✓

使われているベンチマークセットを探したが、そのよeven(zip1(s, t)) = s✓×✓

うなものは見つけることができなかったので、新たにeven(zip2(s, t)) = s✓✓✓

ベンチマークセットを作成して評価実験を行った（表concat(s) ⇒ alt(s)✓✓×1）。既存の証明ツールである Dafny [4] と Circ にも無限二分木の mirror の対称律✓✓×同じ定理を証明させて結果を比較した。表中の ✓ はf(morse) = morse

××✓

証明成功を、× は証明失敗を表す。また、定理中の seven(morse) = morse××✓と t は無限リスト型の全称量化変数を表す。

nots ◦ f = f ◦ nots

✓×✓

全部で 24 個の定理のうち証明に成功した定理の数

rev2(rev2(s)) = s✓×✓は提案手法が 21 個、Dafny が 12 個、Circ が 14 個とcountUp(s) ⇒ inc(s)✓✓×いう結果になった。Dafny でも Circ でも証明できな

adds の交換律✓✓✓

い lexOrder の推移律や inc(s) ⇒ inc(even(s)) など

adds の単位元✓✓✓の定理も提案手法では証明できた。inc は単調増加数

adds の結合律✓✓✓

列の述語、even は無限リストの偶数番目の要素 ([0],nots ◦ even = even ◦ nots

✓×✓[2], [4], ...) を取り出す関数である。

negs ◦ even = even ◦ negs

✓×✓

証明に失敗した定理の例として zip1(even(s), odd(s)) = merge の単調増加保存性✓✓×s がある。この定理は余帰納法の原理 S ⊆ F (S) ⇒adds の単調増加保存性✓✓×S ⊆ νF を素朴に適用しても証明できず、前提部を適adds の upDown 保存性✓××

当な集合 S’ との和集合に弱めてから余帰納法の原理

nots(nots(s)) = s✓✓✓(S∪S ′ ) ⊆ F (S∪S ′ ) ⇒ (S∪S ′ ) ⊆ νF を適用すれば証明できることが分かっている。この定理の場合、集合 S’

成功しているが even(zip1(s, t)) = s の証明には失敗の内容 S ′ (z, s) = ∃x, o, x′ , s′ , e.odd(Cons(x, s), o) ∧している。even と zip1 の再帰パターンが噛み合わな′′′s = Cons(x , s ) ∧ even(s , e) ∧ zip1(o, e, z) は元の定かったことが原因だと考えられる。

理の証明を試みる過程で機械的に特定可能である。そCirc は項書き換えと cyclic proof に基づく自動証のように、S’ を特定して前提部を弱める機能を提案明システムである。実験の結果、Circ は順序関係な手法に追加する拡張は将来の課題である。

どの述語に関する定理の証明が苦手だとわかった。例
えば lexOrder の推移律、反射律、反対称律はどれも

4 関連研究Circ では証明に失敗した。一般に、項書き換えに基Dafny は余帰納法を帰納法に帰着して SMT ソルバ

づく定理証明系は不等式や述語の定理証明が苦手とに解かせるというアプローチを採用している自動証いう事実が指摘されている [6]。Circ も同様の理由で明器である [5]。実験の結果、Dafny は再帰パターンそれらの定理証明に失敗したと考えられる。の異なる関数や述語が混在する定理の証明が苦手だと分かった。例えば even(zip2(s, t)) = s の証明にはいないので原因を明らかにし、アルゴリズムの改善に5 結論と今後の課題つなげる。

余帰納的に定義された述語に関する定理のための自動証明法を提案し、それを自動証明ツールとして

参 考 文 献実装した。実験の結果、既存ツール Circ のサンプル[1] Luke Simon, Ajay Bansal, Ajay Mallya, andGopal Gupta. Co-logic programming: Extending
logic programming with coinduction. In ICALP’07,pp. 472–483. Springer, 2007.
[2] Leonardo De Moura and Nikolaj Bjørner. Z3: Aneﬃcient smt solver. In TACAS’08, pp. 337–340.
Springer, 2008.
[3] Dorel Lucanu, Eugen-Ioan Goriac, Georgiana
Caltais, and Grigore Roşu. Circ: A behavioral
verification tool based on circular coinduction. In
CALCO’09, pp. 433–442. Springer, 2009.
[4] K. Rustan M. Leino. Dafny: An automatic
program verifier for functional correctness.
InLPAR’10, pp. 348–370. Springer, 2010.
[5] K. Rustan M. Leino and Michal Moskal. Coinduction simply.
In ISFM’14, pp. 382–398.
Springer, 2014.
[6] Takahiro Nagao and Naoki Nishida. Proving
inductive validity of constrained inequalities. In
PPDP’16, pp. 50–61. ACM, 2016.

コードに掲載されている定理はあまり証明できなかったものの、順序関係などの述語に関する定理証明ではCirc や Dafny よりも優れた性能を発揮することが分かった。
実験結果の節で触れたように COINDUCT 規則を適用する前に UNFOLD 規則を何度か適用するように推論規則の適用戦略を改良するのは今後の課題である。また、S ⊆ F (S) の証明に失敗した場合に(S ∪ S ′ ) ⊆ F (S ∪ S ′ ) の証明を試みるようにアルゴリズムを改良できると考えられる。今後これを実装し、自動証明できる定理の範囲を広げる予定である。さらに、証明に失敗した定理の一部は原因がまだ分かって