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

決定手続きを用いた項書き換えシステムの帰納的定理
自動証明
山口 諒

青戸 等人

等式論理において，自然数やリストなどのデータ構造上で成立する等式を帰納的定理という．帰納的定理の自動証明法として，項書き換えシステムを用いた書き換え帰納法が知られている (Reddy, 1990)．また，自然数の乗加算やリスト構造のいくつかの演算を用いた等式については帰納的定理の決定手続きが知られている (Aoto&Stratulat,2014)．本報告では，書き換え帰納法と帰納的定理の決定手続きを融合した帰納的定理自動証明法を提案する．提案
手法では，必要な等式公理を満たす関数記号を書き換え帰納法を用いて検出することで，予めどのような関数記号が用いられているかといった情報がない場合や，異なる公理が用いられている場合にも，可能な決定手続きを適用する．また，乗加算やリスト演算以外の関数記号や等式公理を持つような項書き換えシステムについても，書き換え帰納法の途中で決定手続きが利用できる補題を検出した場合には決定手続きを適用する．提案手法を実装するとともに，いくつかの具体例に対して実験を行い，提案手法の有効性を確認した．

決定手続きを組み合わせた，強力な帰納的定理の自動

1 はじめに証明システムの実現を提案する．

プログラムの性質のうちには，自然数やリストと

文献 [1] で提案されている帰納的定理の決定手続き

いったデータ構造に関する帰納法で証明されるようなは，関数記号が与えられている特定の項書き換えシス性質がある．例えば，リストを連結する append 関数

テムに対して機能する．このため，書き換え帰納法なは結合性をもつが，この性質はリストの構造に関するどの一般的な証明法において，この決定手続きを利用帰納法を用いることで証明することが出来る．等式論するには，その特定の理論に用いる関数記号を前もっ理の枠組みでは，このような性質は帰納的定理というて知る必要がある．

概念でとらえられており，書き換え帰納法や潜在帰納

そこで提案手法では，書き換え帰納法を用いること法といった，帰納的定理の自動証明法が知られている

で，どのような関数記号が必要となる公理を満たすか[2] [3]．

を検証する．次に，関数記号を推定できたら，決定手

一方で，Aoto と Stratulat(2014) により，いくつ続きが適用可能な場合には決定手続きを，そうではなかの特定の項書き換えシステムについて，帰納的定理

い場合には書き換え帰納法を適用することで，書き換が決定可能であることが示されている [1]．文献 [1] のえ帰納法と文献 [1] の手法の組み合わせを実現する．

手法は書き換え帰納法が失敗する場合にも成功するが，適用範囲は限定的である．一方，書き換え帰納法

2 準備は失敗することもあるが，適用範囲は広い．

2. 1 項書き換えシステム

そこで，本報告では，書き換え帰納法と文献 [1] のProving inductive theorems of term rewriting systems
automatically using decision procedures.
Ryo Yamaguchi, Takahito Aoto, 新潟大学大学院自然科学研究科, Graduate School of Science and Technology, Niigata University.

本報告で用いる定義及び記法を紹介する．
ソートの集合を S ，多ソート関数記号集合を F と表す．関数記号 f のソートを α1 , α2 , . . . , αn → β と表す．以下では簡単のため，単一ソートを持つ場合について説明する．変数集合を V と表わし，項の集合を T (F, V) と記す．項 t の変数集合を V(t) と表し，
項 t の根記号を root(t) と記す．

表1

入力

関数 σ : V → T (F, V) で集合 {x | σ(x) ̸= x} が有擬簡約な項書き換えシステム R，等式集合 E ，限であるものを代入とよぶ．また，集合 {x | σ(x) ̸= x}を代入 σ の定義域とよび，dom(σ) と記す．項 s と t

書き換え帰納法の入出力

R ⊆ > なる簡約順序 >出力“証明成功” または “証明失敗”の最汎単一化子を mgu(s, t) と記す．
文脈とは，ホールとよばれる特別の定数 □ を持つ

2. 2 帰納的定理項のことをいう．また，文脈 C[ ] のホールを項 t に等式 s ≈ t が, 項書き換えシステム R の帰納的定理置き換えて得られる項を C[t] と記す．s = C[t] となであるとは，s ≈ t の任意の基底具体化 sθg ≈ tθg にるとき，t を s の部分項とよぶ．

ついて， sθg ↔R tθg が成立するときをいう．また，

2 つの項 l, r が，l ∈ V ，V(r) ⊆ V(l) を満たすと∗等式集合 E のすべての要素が R の帰納的定理である

き，l → r を書き換え規則とよぶ．書き換え規則の有とき，R |=ind E と表す．

限集合を項書き換えシステムとよぶ．書き換え規則

例 2.1 (帰納的定理)
 +(0, y)R= +(s(x), y)l → r ∈ R，代入 σ ，文脈 C[ ] が存在して，s = C[lσ]かつ t = C[rσ] となるとき，s →R t と記し，書き換えステップとよぶ．s →R t となるような t が存在しないとき，項 s を正規形とよぶ．→R の反射推移閉∗∗

包を −→R ，→R の等価閉包を ↔R と記す．
項 t が V(t) = ∅ を満たすとき，t を基底項とよぶ．

→y

→ s(+(x, y)) 

このとき，+(+(x, y), z) ≈ +(x, +(y, z)) は，R の帰納的定理となる．よって，R |=ind {+(+(x, y), z) ≈+(x, +(y, z))} が成立する．

シグニチャF 上の基底項の集合を T (F) と記す．また，任意の x ∈ dom(σg ) について σg (x) ∈ T (F) と2. 3 書き換え帰納法なっているような代入 σg を，項 t の基底代入とよぶ．

書き換え帰納法は Reddy [2] により提案された帰納V(t) ⊆ dom(σg ) となっているとき，項 tσg を基底具的定理の自動証明法である．書き換え帰納法では，等体化とよぶ．等式 sσg ≈ tσg が等式 s ≈ t の基底具体

式集合 E と項書き換え規則集合 H の対 ⟨E, H⟩ に関化であるとは，V(s) ∪ V(t) ⊆ dom(σg ) となっているする導出を行いながら，証明を行う．表 1 に書き換ときをいう．

え帰納法の入出力を，図 1 に書き換え帰納法の導出

関数記号を定義記号と構成子に分け，R の定義記号の集合 D を，D = {root(l) | l → r ∈ R}，構成子の集合 C は，C = F\D と定義する．
ある f ∈ D と t1 , . . . , tn ∈ T (C, V) が存在して規則を示す．ここで，Expand 規則に用いられる関数

Expd は以下のように定義される．
Expdu (s, t) ={C[r]σ ≈ tσ | s = C[u], σ =mgu(u, l), l → r ∈ R}

t = f (t1 , . . . , tn ) となるとき，項 t が基本項であると⊎ は直和を表す．等式の向きは区別しない (したがっいい，基本項の集合を B(D, C, V) と記す．また，基て，Simplify 規則は，等式の左辺も右辺も簡約化す

底基本項の集合を B(D, C) と記し，どの基底基本項る)．R および > は入力として与えられる項書き換えも正規形にならないとき，R を擬簡約であるという．

システムと簡約順序である．

項 t の部分項のうち基本項であるものを基本部分項と等式集合と項書き換え規則集合の対について， 図よぶ．また，B(s) は s の基本部分項の集合を表わす．

1 の推論規則を適用して，⟨E, H⟩ から ⟨E ′ , H ′ ⟩ が得

文脈と代入に関して閉じた関係を書き換え関係とられることを ⟨E, H⟩ ; ⟨E ′ , H ′ ⟩ と記す． ; の反射よび，整礎な書き換え関係を簡約関係とよぶ．簡約関推移閉包を ;∗ と記す． 必要に応じて， ; に添字係が半順序 (非反射的かつ推移的) のとき，簡約順序をつけ Simplify 規則 (Delete 規則， Expand 規則)とよぶ．

による導出を ;s (;d , ;e ) と表す．

Simplify⟨E ⊎ {s ≈ t}, H⟩⟨E ∪ {s′ ≈ t}, H⟩

s →R∪H s′Delete⟨E ⊎ {s ≈ s}, H⟩⟨E, H⟩Expand⟨E ⊎ {s ≈ t}, H⟩u ∈ B(s), s > t⟨E ∪ Expdu (s, t), H ∪ {s → t}⟩

図1

書き換え帰納法の推論規則

直観的には，E はこれから証明しようとする等式を，H は帰納法の仮定および証明済みの定理を表す．

表2

入力

DecP rocN {×,+} の入出力

等式集合 E ⊆ T ({f× , f+ , fs , f0 }, V)2

等式集合 E が R の帰納的定理であることを証明する

f× : N, N → Nには，⟨E, ∅⟩ から導出を始める．最終的に ⟨∅, H⟩ がf+ : N, N → N導出されるとき，証明成功となる．

fs : N → N

書き換え帰納法は半アルゴリズムである．すなわ
ち，等式集合が空にならないまま無限に導出を繰り返

f0 : N
出力

して手続きが停止しないことがあり得る．この場合をTrueif RN(f× ,f+ ,fs ,f0 ) |=ind E

False

if RN
(f× ,f+ ,fs ,f0 ) ̸|=ind E

手続きが発散するという．また，規則を適用する等式の選び方や適用する推論規則に任意性があるので上記の手続きは非決定的である．

表3

入力

DecP rocN {+} の入出力

等式集合 E ⊆ T ({f+ , fs , f0 }, V)2

例 2.2 (書き換え帰納法の実行例) 項書き換えシステ

f+ : N, N → N

ム R と証明する等式集合 E として，以下が与えられ

fs : N → Nたとする．
 +(0, y)R= +(s(x), y){
E=+(+(x, y), z)

f0 : N→y→s(+(x, y)) ≈+(x, +(y, z))出力True

if RN(f+ ,fs ,f0 ) |=ind E

False

if RN
(f+ ,fs ,f0 ) ̸|=ind E}> を優位順序 + > s > 0 に基づく辞書式経路順序としたときの書き換え帰納法の実行過程の例を図 2 に示す．

3 特定の関数記号に依存しない帰納的定理の決定手続き
Aoto&Stratulat によって，特定の項書き換えシス

次の定理により，書き換え帰納法の手続きが “証明テム R に対する帰納的定理の決定手続きが与えられ成功” を返した場合，入力等式集合 E が入力項書き換ている [1]．自然数の乗加算の項書き換えシステムに関えシステム R の帰納的定理であることが保証される．

する決定手続き DecP rocN {×,+} の入出力を表 2 に，

命題 2.3 (書き換え帰納法の正当性 [2]) R を擬簡約

自然数の加算の項書き換えシステムに関する決定手な項書き換えシステム， E を等式集合，> を R ⊆ >続き DecP rocN {+} の入出力を表 3 に示す．

なる簡約順序とする．ある項書き換え規則集合 H が存

ここで，RN(f× ,f+ ,fs ,f0 ) は以下の項書き換えシステ在して，⟨E, ∅⟩ ;∗ ⟨∅, H⟩ となるならば，R |=ind E

ムを表す．また，RN(f+ ,fs ,f0 ) は以下の項書き換えシである．

ステムの最初の 2 つの書き換え規則から成る．

⟨ {+(+(x, y), z)e;⟨  +(y , z)≈+(x, +(y, z))} {, +(s(+(x1 , y1 )), z)≈ {, +(+(x, y), z)+(s(x1 ), +(y1 , z)) ;⟨s ;s ;s +(y , z)0 s(+(x1 , +(y1 , z))≈+(y0 , z)≈0;d ;d≈⟨ {+(0, +(y0 , z)) {, +(+(x, y), z)s(+(x1 , +(y1 , z)) →y→fs (f+ (x, y))→f0→

f+ (y, f× (x, y))}⟩+(x, +(y, z))








Step 1. 関数記号を定義記号 D と構成子 C に分類．





{f1 , f2 , f3 , f4 } と な る よ う な 乗 加 算 記 号 候 補

数記号におきかえられる．
しかしこの手続きは，関数記号をパラメータとして必要とする．そのため，書き換え帰納法と同じ枠組みで用いることができない．そこで，この節では与えられた等式が自然数の公理を満たしているかを確かめることで，関数記号を推定して決定手続きを用いる手法 (ProcNatInd) を提案する．
まず，関数記号の情報を用いて関数記号の候補を絞り込む．
定義 3.1 (f1 , f2 , f3 , f4 ) が乗加算記号候補であるとは，あるソート α ∈ S が存在し，f1 : α, α → α,f2 : α, α → α, f3 : α → α, f4 : α, f1 , f2 ∈ D,f3 , f4 ∈ C となるときをいう．同様にして，加算記号候補 (f2 , f3 , f4 ) であるとは，乗加算記号候補から f1に該当する関数記号を取り除いたものをいう．
適切な問題が発見されたとき，決定手続きを利用した帰納的定理証明手続き (ProcNatInd) を行う．その定義 3.2 (ProcNatInd)→+(x, +(y, z))

書き換え帰納法の実行例

ただし，(f× , f+ , fs , f0 ) は入力に応じて具体的な関入出力を表 4 に示す．

→⟩}} {} ⟩, +(+(x, y), z) → +(x, +(y, z))

図2 f+ (f0 , y)
 f (f (x), y)+ sf
× (f0 , z)
 f (f (x), y)× s} ⟩Step 2. D, C の情報とソート情報で，F(E) ⊆(f1 , f2 , f3 , f4 ) を見つける．候補がなければ Step5 へ．
Step 3. R |=ind RN(f1 ,f2 ,f3 ,f4 ) を入力された簡約
順序 > を用いて書き換え帰納法で証明．
証明成功なら Step 4 へ，失敗なら Step 2 へ戻って異なる候補を選択．
N {×,+}
Step 4. RN(f1 ,f2 ,f3 ,f4 ) |=ind E を DecP roc

が True ならば True を，それ以外は証明失敗を返す．

Step 5. D, C の情報とソート情報で，F(E) ⊆{f1 , f2 , f3 } と な る よ う な 加 算 記 号 候 補(f1 , f2 , f3 ) を見つける．候補がなければ失敗を返す．

Step 6. R |=ind RN(f1 ,f2 ,f3 ) を入力された簡約順
序 > を用いて書き換え帰納法で証明．
証明成功なら Step 7 へ，失敗ならそのまま失敗を返す．
N {+}Step 7. RNが(f1 ,f2 ,f3 ) |=ind E を DecP roc

True ならば True を，それ以外は証明失敗を返す．
定理 3.3 (ProcNatInd の正当性) ProcNatInd を用いて True が返ってきた場合は R |=ind E である．

ProcNatInd の入出力

号 D = {+}，構成子 C = {s, 0} に分割する (Step 1)．

擬簡約な項書き換えシステム R，次に，R に出現する関数記号が 3 つであることから，等式集合 E ，乗加算記号候補が見つからず，Step 5 へ移る (StepR ⊆ > なる簡約順序 >2)．D, C の情報とソート情報を用いて，加算記号候補

True または “証明失敗”(+, s, 0) が選ばれたとする (Step 5)．R |=ind RN(+,s,0)

表4

入力

出力を書き換え帰納法を用いて検証し，“証明成功” が返っ(証明) 以下では RN(f1 ,f2 ,f3 ) の場合は同様であるため，てきて Step 7 へ移る (Step 6)．RN(+,s,0) |=ind E を決N
N
RN(f1 ,f2 ,f, f4 ) の場合のみ考える．R(f1 ,f2 ,f, f4 ) を R

定手続きで判定し，帰納的定理であると決定されると省略する．

(Step 7)．

R |=ind R
で あ る ．RN∗

より，∀l → r ∈ R . lθg ↔R rθg

R において加算が第 2 引数に関する場合分けで定|=ind E と 仮 定 す る と ，∀u ≈ v ∈義されていることに注意する．このように，公理の形

NN∗∗

E. uθg ↔RN vθg であるから，∀u ≈ v ∈ E. uθg ↔Rが異なる場合にも，手続きをうまく適用することがでvθg ．よって，R |=ind E が成立．

きる．

2

例 3.4 入力として次の項書き換えシステム R，等式集合 E が与えられたとする．
plus(zero, x) plus(succ(x), z)R= times(zero, z) times(succ(x), y)

E=→→→→

xsucc(plus(x, z))
zero


plus(y, times(x,y)) 4 決定手続きを利用した書き換え帰納法
書き換え帰納法を用いて証明をする際，等式をそれ以上 Expand できずに停止してしまう場合 (証明失敗) や，等式集合が空にならないまま無限に導出を繰

り返して手続きが停止しないことがあり得る (発散)．

 ≈ plus(times(x, y), times(x, z)) しかし，決定手続きは，等式集合が自然数やリストの times(x, plus(y, z))

関 数 記 号 を 定 義 記 号 D = {times, plus}，構 成

公理を満たす場合に限定されるものの，発散すること子 C = {succ, zero} に 分 割 す る (Step 1)．こ のなく証明が終了する．そこで，書き換え帰納法と決定

情 報 と ソ ー ト 情 報 を 用 い て ，乗 加 算 記 号 候 補

手続きの手法を組み合わせることで，より強力な証明(plus, times, succ, zero) が選ばれたとする (Step 2)．

システムを実現する．

R |=ind RN(plus,times,succ,zero) を書き換え帰納法を用

例 4.1 入力として以下の項書き換えシステム R といて検証し，この場合は証明が失敗してしまうた

等式集合 E を与える．(pow は自然数を 2 乗する関数

め，Step 2 に戻る (Step 3)．前とは別の乗加算記号である．){候補 (times, plus, succ, zero) を選択する (Step 2)．

E=R |=ind RN(times,plus,succ,zero) を書き換え帰納法を用いて検証し，“証明成功” が返ってきて Step 4 へ移る (Step 3)．RN(times,plus,succ,zero) |=ind E を決定手続きで判定し，帰納的定理であると決定される (Step4)．

R=


T (Z, y)
T (S(x), y) P (Z, y)
P (S(x), y) pow(Z)pow(S(x))

pow(x)→→→→→→≈}T (x, x)

Z




P (y, T (x, y))yS(P (x, y))



Z


P (pow(x), S(T (x, S(S(Z)))))

例 3.5 (公理の表現が異なる例) 入力 R，E を以下のとおり与える．
 +(y, 0)R= +(y, s(x)){E=+(+(x, y), z)

この場合，導出過程は図 4 のとおりになり，証明に失
→y→s(+(x, y)) ≈+(y, +(z, x))

敗する．しかしながら，最後の等式集合に着目してみると，RN(T,P,S,Z) の帰納的定理である．よって，前節}

ここで ProcNatInd を用いると，関数記号を定義記の特定の関数記号に依存しない決定手続きを用いることで，証明に成功する．
そこで，次のように書き換え帰納法を拡張する．

⟨{pow(x)≈times(x, x)}, ∅⟩Z ≈ T (Z, Z) ⟩⟨P(pow(x),S(T(x,S(S(Z)))))
11;e≈ T (S(x1 ), S(x1 )){}pow(x) → T (x, x)
Z≈Z ⟩⟨P (T (x1 , x1 ), S(T (x1 , S(S(Z)))))
s

;


≈ P (S(x1 ), T (x1 , S(x1 ))){}pow(x) → T (x, x)


 ⟩
⟨
P (T (x , x ), S(T (x , S(S(Z)))))
1表5

入力

1

≈ P (S(x1 ), T (x1 , S(x1 ))) }{pow(x) → T (x, x);e これ以上 Expand できず失敗

図3pow 関数を用いた等式の書き換え帰納法での導出例

功する．

融合証明法の入出力

擬簡約な項書き換えシステム R，等式集合 E ，5 実装と実験
文献 [1] の決定手続き (DP)，書き換え帰納法 (RI)，

R ⊆> なる簡約順序 >出力1;d“証明成功” または “証明失敗”

本報告で提案した融合証明法 (FP) の 3 つの証明法を実装した．実装には関数型言語である SML/NJ を用

定義 4.2 (書き換え帰納法の拡張)

書き換え帰納いた．プログラムコードは約 2,000 行である．

20 個の例で実験を行った結果を表 5 に示す．この例

法に以下の規則を追加する．

では，基本的に奇数番目が特定の関数記号 (×, +, s, 0)

E-Delete⟨E ⊎ {s ≈ s′′ }, H⟩⟨E, H⟩に依存した等式集合，偶数番目がそれらに依存しない等式集合である．決定手続きや書き換え帰納法を用い
ProcNatInd(R, {s ≈ s′′ }, >) = true

た場合よりも，強力な証明を実現できた．

この拡張した書き換え帰納法を融合証明法と呼び，そ6 おわりにの入出力を表 4 に示す．

文献 [1] の自然数の乗加算の記号を用いた決定手続と表す．この規則は，き (DecP rocN ) の手法と書き換え帰納法を融合する

導出過程の等式集合 E に含まれる等式 s ≈ s′′ についことで，帰納的定理証明の能力を高める手法を提案て，決定手続き (ProcNatInd) を用いて帰納的定理がした．今後の課題としては，書き換え帰納法と文献

E-Delete による導出を ;Ed′′証明成功する場合，該当する等式 s ≈ s を等式集合[1] のリスト構造の演算を用いた等式の決定手続きをE から取り除く．

融合することで，より強力な証明システムを構築す先の pow 関数を用いた例 4.1 が E-Delete 規則を適ることが挙げられる．リストの関数記号においても，用した拡張書き換え帰納法を用いることで証明に成

多ソート情報や，定義記号と構成子の分類を有効に用表6

提案手法を用いた帰納的定理証明の実験結果 (○:定理，×:失敗，∞:発散，–:適用不可)

等式集合 E

DPRI

FP

1s(+(x, +(y, 0))) ≈ +(y, +(s(0), x))○×○2succ(plus(x, plus(y, z))) ≈ plus(y, plus(succ(z), x))–×○

3s(+(+(x, x), +(y, x))) ≈ +(+(x, x), s(+(y, x)))○×○

4succ(plus(plus(x, x), plus(y, x))) ≈ plus(plus(x, x), succ(plus(y, x)))–×○

5+(+(y, +(0, x)), 0) ≈ +(y, x)○○○

6P (P (y, P (Z, x)), Z) ≈ P (y, x)

–

○

○

7+(+(s(0), x), 0) ≈ s(+(0, +(x, 0)))

○

○

○

8p(p(succ(zero), x), z) ≈ succ(p(z, p(x, zero)))–×○

9∗(x, +(0, 0)) ≈ ∗(+(x, x), 0)

○

×

○

10T (x, P (z, z)) ≈ T (P (x, x), z)

–

×

○

11s(s(+(+(s(x), ∗(x, x)), x))) ≈ +(s(x), s(s(+(x, ∗(x, x)))))

○

∞

○

12succ(succ(plus(plus(succ(x), times(x, x)), x)))–∞○≈ plus(succ(x), succ(succ(plus(x, times(x, x)))))
13s(0) ≈ +(s(0), ∗(∗(x, 0), s(x)))○×○

14s(z) ≈ plus(s(z), times(times(x, z), s(x)))–×○

15∗(∗(∗(∗(s(x), 0), x), 0), x)

○∞

○–∞

○≈ ∗(∗(0, +(s(∗(x, y)), x)), ∗(0, ∗(s(∗(y, y)), ∗(∗(y, x), x))))16

T (T (T (T (S(x), Z), x), Z), x)≈ T (T (Z, P (S(T (x, y)), x)), T (Z, T (S(T (y, y)), T (T (y, x), x))))17

pow(x) ≈ ∗(x, x)

–×

○

18

pow(x) ≈ T (x, x)–×○

19rev(rev(@(xs, ys))) ≈ @(xs, ys)–∞∞

20R(R(app(xs, ys))) ≈ app(xs, ys)

–∞

∞

9/20

3/20

18/20

成功数
いることで，関数記号を推定することが可能であると考える．また，決定手続きは反証も可能であるため，融合証明法を反証に応用することも課題である．

参 考 文 献[1] Aoto, T. and Stratulat, S.: Decision procedures for proving inductive theorems without induc-tion, Proc. of the 16th PPDP, ACM Press, 2014,
pp. 237–248.
[2] Reddy, U. S.: Term rewriting induction, Proc. ofthe 10th CADE, Vol. 449 of LNAI, Springer-Verlag,
1990, pp. 162–177.
[3] 小池広高, 外山芳人: 潜在帰納法と書換え帰納法の比
較, Vol. 17(2000), pp. 1–12.