無限項書き換えシステムにおける強頭部正規化可能性の反証手続き
A Procedure for Disproving Strong Head Normalizationof Inﬁnitary Term Rewriting Systems
岩見 宗弘 1 , 青戸 等人 2
1 島根大学 総合理工学部 数理・情報システム学科

munehiro@cis.shimane-u.ac.jp
2 東北大学 電気通信研究所

aoto@nue.riec.tohoku.ac.jp
概要
ストリームといった仮想的に無限長と見做されるデータを扱う関数型プログラ
ムの計算モデルとして，無限項書き換えシステムが知られている．通常の項書き換えシ
ステムに対しては，様々な停止性の証明法や反証法が知られている．しかしながら，通常の項書き換えシステムとは対照的に，無限項書き換えシステムでは停止性を考える意
味があまりない．このため，無限項書き換えシステムにおいては，停止性に替わる自然な性質として項のどの位置も有限回しか書き換えられないことを保証する性質である強頭部正規化可能性が考えられている．近年，Zantema(2008) や Endrullis ら (2009) が，
強頭部正規化可能性の自動証明法を与えている．しかしながら，強頭部正規化可能性の自動反証法についてはあまり知られていない．本論文では，強頭部正規化可能性を反証するための手続きを提案し，その正当性を示す．

はじめに

1

遅延評価に基づくデータ構造やストリームといったデータ構造を用いたプログラムでは，データを仮想的に無限長と見做すことによって見通しのよい議論が可能になる場合が少なくない．このような無限長のデータを扱う計算モデルとして，無限項書き換えシステム(inﬁnitary term rewriting
systems) が知られている [7, 13, 14, 15, 18, 20, 21]．無限項書き換えシステムは，関数型プログラ
ムの計算モデルとして知られている項書き換えシステム(term rewriting systems) [2, 18] の拡張である．通常の項書き換えシステムと大きく異なる特徴は，通常の項書き換えシステムが有限の大きさの項しか対象にしないのとは対照的に，無限項書き換えシステムでは無限の大きさの項 (無限項(inﬁnitary terms)) も対象とする点である．
項書き換えシステムに基づく様々な検証法において停止性(termination) は非常に有用な性質として知られている [2, 18]．このため，通常の項書き換えシステムの枠組みにおいては，様々な停止性の証明法や反証法が提案されている [2, 9, 10, 18, 19]．また，停止性検証ツールの開発やツールのコンペティッションも行われている∗ ．一方，通常の項書き換えシステムとは対照的に，無限項書き
換えシステムでは停止性を考える意味があまりない．無限項をも対象として考える場合には，容易に無限の書き換え列が構成でき，停止性を持たないことが多いためである．例えば，非常に簡単な(f を g に替えるだけの) 書き換え規則 R = {f(x) → g(x)} を考えた場合でも f が無限に重なるような無限項 f(f(f(· · · ))) をとると，f(f(f(· · · ))) →R g(f(f(· · · ))) →R g(g(f(f(· · · )))) →R · · · のように無限書き換え列が構成できてしまう．
∗

http://www.termination-portal.org

このため無限項書き換えシステムにおいては，停止性に替わる自然な性質として，強頭部正規化可能性† (strong head normalization) とよばれる性質が考えられている [7, 15, 20]．強頭部正規化可能性は，項のどの固定位置も有限回しか書き換えられないという性質であり，これによって，強頭部正規化可能性をもつ無限項書き換えシステムにおいて，ストリームのプレフィックスのように観測可能な有限部分のデータについては，正規形 (書き換えによって変わらない項) が求まることが保証される．例えば，エラトステネスの篩を用いて素数を計算する項書き換えシステム R は以下のように記述できる [18]．
ﬁlter(x : y, 0, m)→ 0 : ﬁlter(y, m, m)








 ﬁlter(x : y, s(n), m) → x : ﬁlter(y, n, m)





 sieve(0 : y)
→ sieve(y)R=sieve(s(n) : y)→ s(n) : sieve(ﬁlter(y, n, n)) 










nats(n)→n:nats(s(n))






primes→ sieve(nats(s(s(0))))
このとき，R は停止性を持たないが，重要な性質の 1 つとして，リスト primes の先頭要素をいくつとっても次の要素が求まるかという性質が考えられる．このような性質の定義方法や検証手法について，無限項書き換えシステムの枠組みを用いた研究が近年進められている [1, 8, 21]．
左線形規則 (左辺に同じ変数が 2 度以上出現しない規則) のみを考える場合には，強頭部正規化可能性は ω-強頭部正規化可能性(ω-strong head normalization) と同等であることが知られている[14, 18]．ω-強頭部正規化可能性は，長さ ω の書き換え列に限定して強頭部正規化可能性を保証する性質である．近年，Zantema [20] は ω-強頭部正規化可能性に対して意味論に基づく特徴付けを示し，行列解釈を用いた ω-強頭部正規化可能性の自動証明法を与えている．そして，組合せ子(combinator)[3, 6, 17] の書き換え規則のいくつかについて，ω-強頭部正規化可能性の自動証明に成功することを報告している．また，Endrullis ら [7] は，木オートマトンを使って，初期項集合を限定した局所 ω-強頭部正規化可能性の証明手法を与えている．
一方，非 ω-強頭部正規化可能性については，縮退規則 (collapsing rule) を持つ無限項書き換えシ
ステムが ω-強頭部正規化可能性を持たないことが知られているが，それ以外の十分条件や証明法は従来あまり知られていない．その一方で，よく知られた組合せ子の書き換え規則の多くは，非縮退であるにもかかわらず，ω-強頭部正規化可能性を持たないことが最近報告されている [22]．このため，縮退規則を持たない無限項書き換えシステムに対しても適用可能であるような ω-強頭部正規化可能性の自動反証法は，より強力な無限項書き換えシステムの ω-強頭部正規化可能性判定法を実現するためには不可欠と考えられる．本論文では，縮退規則を持たない無限項書き換えシステムに対しても適用可能であるような ω-強頭部正規化可能性の反証手続きを提案し，その正当性を示す．
本論文の構成は以下の通りである．第 2 節では，無限項書き換えシステムに関する定義や記法を与え，続いて，ω-強頭部正規化可能性について説明する (第 3 節)．第 4 節において，ω-強頭部正規化可能性の反証手続きを与えるとともにその正当性を証明し，文献 [22] で報告された ω-強頭部正規化可能性を持たない組合せ子の書き換え規則に対して，提案手法を適用した結果について報告する．
第 5 節に結論を示す．

準備2

本節では，本論文で使用する定義や記法を与える．詳細は文献 [7, 18] 等を参考して頂きたい．
関数記号の集合を F ，変数の可算無限集合を V と記す (F ∩V = ∅)．0 引数の関数記号を定数とよび，∗
n 引数の関数記号集合を Fn と記す．N+ を正整数集合とし，正整数の有限列を N+ と記す．部分関数†

無限停止性 (inﬁnitary normalization) あるいは強収束性 (strong convergence) とよばれることもある．

∗t : N+ → F ∪ V のうち，以下の条件を満たすものを F, V 上の項とよぶ：(1) t(²) ∈ F ∪ V; (2) 任意∗の p ∈ N+ について，t(pi) ∈ F ∪V ⇐⇒ t(p) ∈ Fn かつ 1 ≤ i ≤ n．ここで，² は空列を表わす．F, V∗
上の項の集合を Tinf (F, V) と表す．項 t ∈ Tinf (F, V) の定義域 Pos(t) = {p ∈ N+ | t(p) ∈ F ∪ V}の要素を t における位置とよぶ．特に，位置 ² を根位置とよぶ．t(p) を項 t の位置 p に出現する記号とよぶ．項 t に出現する変数集合を V(t) と表す．位置集合 Pos(t) が有限集合であるとき，項 t
を有限であるという．有限項の集合を Tﬁn (F, V) と記す．位置 p ∈ Pos(t) における項 t の部分項t|pを t|p (q) = t(pq) により定義する．関数記号 f ∈ Fn および項 t1 , . . . , tn ∈ Tinf (F, V) に対して, (1)∗t(²) = f ; (2) t(ip) = ti (p) (1 ≤ i ≤ n, p ∈ N+ ) により定義される項 t を f (t1 , . . . , tn ) と記す．位置∗
集合上のプレフィックス順序を p ≤ q ⇔ ∃r ∈ N+ . q = p.r により定義する．ある位置 q および正整数 i < j が存在して，q.i ≤ p1 ，q.j ≤ p2 となるとき，p1 は p2 の左に位置するという．
関数 σ : V → Tinf (F, V) を代入とよぶ．代入 σ を項 t ∈ Tinf (F, V) に適用した結果 σ(t) を，以下∗のように定義する：σ(t)(p) = σ(t(p0 ))(p1 ) (p = p0 p1 かつ t(p0 ) ∈ V を満たす p0 , p1 ∈ N+ が存在する場合); σ(t)(p) = t(p) (それ以外の場合)．直観的には，σ(t) は t に出現する変数 x ∈ V を σ(x)により置き換えた結果得られる項を表わす．代入 σ の定義域 {x ∈ V | σ(x) 6= x} を dom(σ) と記す．
dom(σ) = {x1 , . . . , xn }，σ(xi ) = ui なる代入を {x1 := u1 , . . . , xn := un } とも記す．dom(σ) が有限かつ任意の x ∈ dom(σ) について σ(x) ∈ Tﬁn (F, V) なるとき，σ を有限代入とよぶ．σ(t) を tσ とも記す．項 s, t について，sσ = t となる代入 σ が存在するとき，項 s は t と照合可能であるという．
そのような代入 σ のうち，dom(σ) = V(s) なる σ を match(s, t) と記す．
¤ 6∈ F ∪ V なる定数 (ホールとよぶ) を考える．Tinf (F ∪ {¤}, V) の要素のうち，{p | C(p) = ¤}が有限集合となるものを文脈とよぶ．C ∈ Tinf (F ∪ {¤}, V) が {p1 , . . . , pn } = {p | C(p) = ¤} かつ
任意の i < j について pi が pj より左に位置するとき，C を C[ ]p1 ,...,pn と記す．文脈 C[ ]p1 ,...,pn と項
t1 , . . . , tn ∈ Tinf (F, V) に対して，項 t = C[t1 , . . . , tn ]p1 ,...,pn を以下のように定義する：t(p) = ti (q)(∃i, q. p = pi .q の場合); t(p) = t(p) (それ以外の場合)．直観的には，C[t1 , . . . , tn ]p1 ,...,pn は C に出現するホールを左から順に t1 , . . . , tn に置き換えて得られる項を表わす．
有限項 l, r ∈ Tﬁn (F, V) の組 hl, ri で，l(²) 6∈ V かつ V(r) ⊆ V(l) を満たすものを書き換え規則とよぶ‡ ．書き換え規則の集合 R を無限項書換えシステム(inﬁnitary TRS) とよぶ．以下では書き換え
規則 hl, ri を l → r と表す．項 s, t ∈ Tinf (F, V) に対して，l → r ∈ R, 代入 σ ，文脈 C[ ]p が存在しpて，s = C[lσ]p かつ t = C[rσ]p となるとき，s →R t と記す．これを位置 p における項 s から項 t への簡約または書き換えとよぶ．根位置 ² における簡約を根書き換えとよぶ．文脈から明らかな場合∗
もしくは必要がない場合は p, R は省略する．→R の反射推移閉包を →R と記す．項における任意の変数の出現が高々1 回のとき, 線形であるといい，任意の l → r ∈ R に対して l が線形であるとき, R を左線形であるという．また，ある書き換え規則 l → r ∈ R に対して, r ∈ V となるとき，Rを縮退性を持つという．
項 t が正則(regular または rational) であるとは，t の部分項集合が有限集合であるときをいう [5]．
正則項の集合を Treg (F, V) と記す．有限項は明らかに正則であることに注意する．dom(θ) が有限集合，かつ，任意の x ∈ dom(θ) について，θ(x) が正則である代入 θ を正則代入とよぶ．正則項は正則代入の適用に関して閉じており，代入の正則性は関数合成 ◦ によって保存される．また，正則項
s, t について，θ = match(s, t) が存在するとき，θ は正則代入となる．
有限代入 θ = {x1 := u1 , . . . , xn := un } が u1 , . . . , un ∈ Tﬁn (F, V) \ V であるとき，これを再帰式
表現(a system of regular equations) とよぶ．再帰式表現を用いて，正則項を表現することが出来る．
今，θ = {x0 := t0 , . . . , xn := tn } とおき，任意の 0 ≤ i ≤ n について，ti = Ci [xi1 , . . . , xiki ]pi,1 ,...,pi,kiとする．ただし，ここで，xi1 , . . . , xiki は変数 x0 , . . . , xn のうち ti 中に出現するもの全てであると‡書き換え規則の左辺を有限項に制限するのは一般的である [7, 18]．本論文では文献 [7] と同様に右辺も有限項に制限する．

する．このとき，項 θ? (x0 ), . . . , θ ? (xn ) を以下のように定義する．
{
Ci (p)(p ∈ Pos(Ci ) ∧ Ci |p 6= ¤ の場合)?
θ (xi )(p) =?
θ (xij )(q) (∃j, q. p = pi,j q の場合).
項 θ? (x0 ), . . . , θ ? (xn ) を再帰式表現の解とよぶ．再帰式表現の定義より，t1 , . . . , tn ∈/ V であるから
pi,j > ² となっており，θ? (xi ) が良定義される (well-deﬁned) ことに注意する．以下が成立する．
命題 1 ([4, 5]) 再帰式表現の解は正則項である．また，任意の正則項はある再帰式表現の解となる．
つまり，再帰式表現を用いることによって，任意の正則項を記述することが出来る．例えば，無限項f(f(· · · )) は {x := f(x)}? (x) となり，θ = {x := f(y), y := g(x)} に対して，θ? (x) = f(g(f(g(· · · ))))，
θ? (y) = g(f(g(f(· · · )))) となる．一方，θ が再帰式表現のとき，θ? は dom(θ) = dom(θ? ) なる正則代
入となる．また，正則項が有限項かどうか，つまり再帰式表現 θ が与えられたときに θ? (x) が有限項かどうかは決定可能であることに注意する．
特定の形の正則項については，以下のより簡明な表記法を用いる．(1) f ω は {x := f (x)}? (x) を意味する．(2) µx.t は {x := t}? (x) を意味する．慣習に従って，µx. は関数適用より結合力が弱い
ものとして括弧を省略する．例えば，{x := g(y, y), y := f(y)}? (x) = g(f ω , f ω )，{x := g(y, x), y :=f(y)}? (x) = µx.g(f ω , x) である．
正則項 s, t について，sσ = tσ となる正則代入 σ が存在するとき，正則項 s は t と単一化可能であるという．そのような正則代入 σ を単一化子とよぶ．正則代入上の順序 - を θ - η ⇐⇒ある正則代入 ρ が存在して η = ρ ◦ θ により定めるとき，単一化子のうち順序 - に関して極小となる単一化子を最汎単一化子とよぶ．正則項 s と t の最汎単一化子を mgureg (s, t) と記す．正則項の単一化について以下の事実が知られている．
命題 2 ([4, 5, 12, 16]) 正則項の単一化問題は決定可能である．また，単一化可能であるときに最汎単一化子を求めるアルゴリズムが存在する．
つまり，再帰式表現 θ, θ 0 を与えたときに，θ? (x)η = θ0? (y)η なる正則代入 η が存在するかの判定ア
ルゴリズムが存在する．また，正則項の同値問題や照合問題は，右辺または両辺の項に含まれる変数を定数と見なすと単一化問題に帰着できるので，これらも決定可能である．なお，s, t が有限項であっても，正則項上の最汎単一化子 mgureg (s, t) は有限代入とならない場合があることに注意する．
例えば，mgureg (g(x, x), g(x, f(x))) = {x := f ω } となる (一方，有限項上では，g(x, x) と g(x, f(x))
は単一化可能ではない)．
無限項書き換えシステムに正則項を用いた研究としては，Kennaway ら [13] によるグラフ書き換
えと正則項上の無限簡約の対応や，Inverardi と Zilli [11] による正則項上の項書き換えの枠組みが知られている．

3

ω-強頭部正規化可能性

本節では，ω-強頭部正規化可能性について説明し，ω-強頭部正規化可能性の反証についての従来結果を説明する．
p

定義 3 (ω-強頭部正規化可能性) R を無限項書き換えシステムとする．任意の無限書き換え列 t0 →R0
t1 →pR1 t2 →pR2 · · · (i ∈ ω) について，あるインデックス n0 が存在して任意の n ≥ n0 について pn 6= ²となるとき，R は ω-強頭部正規化可能性を持つという．

Zantema [20] や Endrullis ら [7] によって，無限項書き換えシステムが ω-強頭部正規化可能性を持つことを示す手法が知られている．一方，無限項書き換えシステムが ω-強頭部正規化可能性を持たないための十分条件として以下の条件が知られている [20]．
命題 4 (縮退システムの ω-強頭部正規化可能性) 無限項書き換えシステム R が縮退性を持つとき，
ω-強頭部正規化可能性を持たない．

(証明) R の縮退性より，C[x, . . . , x] → x (ただし C 6= ¤) なる書き換え規則が R に存在する．このとき，正則項 t ∈ Treg (F, V) を
t = µx.C[x, . . . , x]
とおく．このとき，

t = C[t, . . . , t] →²R t = C[t, . . . , t] →²R · · ·となるので，R は ω-強頭部正規化可能性を持たない．

¤

縮退性を持たない無限項書き換えシステム R についても，根書き換えが無限回出現するような無限書き換え列を構成することによって，R が ω-強頭部正規化可能性を持たないことを示せる場合がある．岩見 [22] は組合せ子の書き換え規則に対して，ω-強頭部正規化可能性が成立しないことを，反例を構成することによって報告している．
以下，本論文の組合せ子の例では，適用演算子 · に中置記法を用いる．また，慣例にしたがい，·は左結合であるとして，不要な括弧は省略する．
例 5 (ω-強頭部正規化可能性を持たない無限項書き換えシステム (1)[22]) 無限項書き換えシステ
ムRをR = {L · x · y → x · (y · y)}
とおく．このとき，正則項 t = µx.L · x をとる．このとき，t = L · t であることに注意すると，

L · t · y →²R
=
→²R
=
→²R

t · (y · y)
L · t · (y · y)t · ((y · y) · (y · y))
L · t · ((y · y) · (y · y))···となるので，R は ω-強頭部正規化可能性を持たない．
例 6 (ω-強頭部正規化可能性を持たない無限項書き換えシステム (2)[22]) 無限項書き換えシステ
ムRをR = {J · x · y · z · w → x · y · (x · w · z)}
とおく．正則項 t = µx0 .J · x0 · x をとる．このとき，t = J · t · x であることに注意すると，J · t · y · z · w →²R
=
→²R
=
→²R

t · y · (t · w · z)
J · t · x · y · (t · w · z)
t · x · (t · (t · w · z) · y)
J · t · x · x · (t · (t · w · z) · y)···となるので，R は ω-強頭部正規化可能性を持たない．
これらの例では，適切な正則項 t を与えることによって，無限回の根書き換えを含むような無限書き換え列を構成している．もし，このような正則項 t を自動的に構成もしくは発見できれば，ω強頭部正規化可能性の自動反証が可能になるはずである．

4

ω-強頭部正規化可能性の反証手続き

本節では，ω-強頭部正規化可能性の反証手続きを与えるとともに，その健全性を示す．まず，無限項書き換えシステム R が ω-強頭部正規化可能性を持たないことを保証する十分条件を与える．
補題 7 (非 ω-強頭部正規化可能性の十分条件) R を無限項書き換えシステムとする．ある書き換え∗
規則 l → r ∈ R とある代入 σ, η が存在して，rσ →R lση となるとき，R は ω-強頭部正規化可能性を持たない．

(証明) 仮定より，無限書き換え列∗∗∗

lσ →²R rσ →R lση →²R rση →R (lση)η →²R (rση)η →R · · ·が構成できる．この無限書き換え列には，根書き換えが無限に出現するため，R は ω-強頭部正規化可能性を持たない．
¤∗

従って，ω-強頭部正規化可能性の反証を行なうためには，rσ →R lση となるような代入 σ, η を構成できればよい．このような代入 σ, η を構成するために，ナローイング [2] のアイデアを用いる．
ナローイングは書き換えに必要な代入を単一化によって求めながら，与えられた項の代入例からの簡約結果を求める方法で，関数・論理融合型プログラム言語の計算メカニズムとして知られている．
従来知られているナローイングは有限項上のナローイングだが，正則項の単一化の決定可能性 (命題 2) から，正則項を対象とするナローイングへ容易に拡張できる．
定義 8 (正則項のナローイング) R を無限項書き換えシステム，s を正則項とする．ある書き換え
規則 l → r ∈ R について s の非変数部分項 s|p と l が (正則項上で) 単一化可能であるとする．
θ = mgureg (s|p , l)，t = s[r]p θ とおくとき，s Ãpθ,R t と記す．ただし，文脈から明らかな場合もしくは必要がない場合は θ, R, p は省略する．ÃR を R のナローイング関係とよぶ．Ã の反射推移閉包∗∗を Ã と記す．s1 Ãθ1 s2 Ãθ2 · · · Ãθn−1 sn となるとき，σ = θn−1 ◦ · · · ◦ θ1 に対して s1 Ãσ sn と記
す．また，p = ² の場合を根ナローイングとよぶ．
無限項書き換えシステムが有限集合であること，および，正則項の単一化の決定可能性から，正則項 s が与えられたときに，s Ãθ,R t なる t が存在するならば，そのような t すべてを実効的に構成することが可能である．以下の性質は容易に導かれる．
∗

補題 9 (ナローイングの性質) s を正則項とする．(1) s Ãθ t となるとき，t は正則項．(2) s Ãσ t∗ならば，sσ →R t．

(証明) (1) は，最汎単一化子が正則代入であること，および，正則項が正則代入に閉じていることから明らか．(2) は，有限項のナローイングと同様に示せる．
¤
例 10 根ナローイングを用いることによって，根書き換えを更に行うために必要な正則代入を求めることができる．以下では，右側に記述してある正則代入を適用することで，次の簡約が可能となる．
L · x0 · y0 →²R x0 · (y0 · y0 ){x0 := L · x1 }= L · x1 · (y0 · y0 )→²R x1 · ((y0 · y0 ) · (y0 · y0 )){x1 := L · x2 }= L · x2 · ((y0 · y0 ) · (y0 · y0 ))→²R x2 · (((y0 · y0 ) · (y0 · y0 )) · ((y0 · y0 ) · (y0 · y0 ))) {x2 := L · x3 }= L · x3 · (((y0 · y0 ) · (y0 · y0 )) · ((y0 · y0 ) · (y0 · y0 )))→²R · · ·

しかしながら，根ナローイングでは，より長い (有限長の) 書き換え列が可能になる代入が求まる
だけで，無限書き換え列の構成に必要な代入が必ずしも求まるわけではない．例えば，上の例では，
例 5 で見たように，無限書き換え列を構成するには t = L · t なる正則項を代入する必要がある．
ここで，上記の例で，右側に現われている代入が {xi := L · xi+1 } の形をしていることと，t = L · t
なる正則項は，再帰式表現 {x := L · x} の解であることに着目すると，いくつかの変数を同一視することによって代入を変更すれば適当な再帰式表現が構成できると予想される．そこで，いくつかの変数を同一視する代入上の関係を以下に導入する．

∪
定義 11 (正則代入上の関係 I) θ = {x1 := u1 , . . . , xn := un } を正則代入，X = 1≤i≤n V(ui )，Y = X ∪ {x1 , . . . , xn } とおく．このとき，(1) dom(σ) ⊆ X ，(2) ∀x ∈ dom(σ). σ(x) ∈ Y を満たす
代入 σ が存在して，θ0 = σ ◦ θ となるとき，θ0 I θ とする．
θ が固定されたときに，θ0 I θ となる θ0 の個数は有限であることに注意する．
例 12 (正則代入上の関係 I) σ = {x1 := x0 } をとると，{x0 := L · x0 , x1 := x0 } I {x0 := L · x1 }が成立する．
次の定義を反証手続きに用いる．
定義 13 (正則代入の拡張) 正則代入 θ = {x0 := t0 , . . . , xn := tn } とおき，任意の 0 ≤ i ≤ n について，ti が非変数有限項ならば，ti = Ci [xi1 , . . . , xiki ]pi,1 ,...,pi,ki とする．ただし，ここで，xi1 , . . . , xiki
は変数 x0 , . . . , xn のうち ti 中に出現するもの全てであるとする．このとき，θ? (x), θ?? (x) を以下のように定める．
{θ(x)(θ(x) ∈ V または θ(x) ∈/ Tﬁn (F, V) の場合)
θ? (x) =??
θ (x) (θ(x) ∈ Tﬁn (F, V) \ V の場合){
Ci (p)(p ∈ Pos(Ci ) ∧ Ci |p 6= ¤ の場合)??
θ (xi )(p) =?
θ (xij )(q) (∃j, q. p = pi,j q の場合)．
直観的には，θ? は非変数有限項の場合のみ再帰式表現と同様に展開を行なって得られる代入を表
わす．また，θ?? は θ? を定義するための補助定義であり，以下で用いることはない．θ が再帰式表
現の場合は，再帰式表現に対する θ? の定義 (2 節) と上記の定義による θ? は等価になることに注意する．
手続き 14 (ω-強頭部正規化可能性の反証手続き) l → r ∈ R のそれぞれについて，以下の手続き
disprove-omega-shn を非決定的に適用する．

1: procedure disprove-omega-shn (l, r, R)
2: begin3:
t := r; σ := ∅;4:
while () {5:
if (∃θ, θ0 , η. θ = mgureg (REN(lσ), t), θ0 I θ, η = match(lσθ 0? , tθ0? ))6:then return lσθ0? ;7:else if ∃σ 0 , t0 . t Ãσ0 ,R t0
8:then t := t0 ; σ := σ 0 ◦ σ;
9:else Fail;10:}
11: endただし，7 行目のナローイングの導出も非決定的に実行されるものとする．REN(t) は項 t に出現する変数を新しい変数に名前換えした項を表す．return 命令によって 1 つでも正則項 lσθ 0? が返された場合，手続きは成功して終了し，全ての disprove-omega-shn の適用が失敗で終わった場合，手続きは失敗して終了する．いずれでもないときは手続きが終了しない (発散する) 場合である．
以下では，上記の手続きにもとづき，ω-強頭部正規化可能性の反証に成功する例を示す．まず，
例 5 の反例が上記の手続きにもとづいて導出できることを示す．
例 15 (ω-強頭部正規化可能性の反証例 (1)) R = {L · x · y → x · (y · y)} とおく．まず，手続き 3
行目で，t := x · (y · y), σ := ∅ とおかれる．このとき，θ = mgureg (L · x0 · y 0 , x · (y · y)) = {x :=L · x0 , y 0 := y · y}．次に，θ0 = {x := L · x, y 0 := y · y, x0 := x} I {x := L · x0 , y 0 := y · y} をとると，
θ0? = {x := t, y 0 := y · y, x0 := x}．ただし，ここで t = µx.L · x とする．よって，t = L · t に注意す
ると，η = match(L · t · y, t · (y · y)) = match(t · y, t · (y · y)) = {y := y · y} より，手続き 6 行目でlσθ 0? = t · y が返され，手続きが成功する．
例 6 の反例についても，上記の手続きにもとづいて次のように導出できることが容易に確認できる．
例 16 (ω-強頭部正規化可能性の反証例 (2)) R = {J·x·y·z·w → x·y·(x·w·z)} とおく．まず，手続
き 3 行目で，t := x·y·(x·w·z), σ := ∅ とおかれる．このとき，θ = mgureg (J·x0 ·y 0 ·z 0 ·w0 , x·y·(x·w·z)) ={x := J·x0 ·y 0 , y := z 0 , w0 := x·w·z}．次に，θ0 = {x := J·x·y, w0 := x·w·z, x0 := x, y 0 := y, z 0 := y} Iθ をとると，θ0? = {x := t, w0 := x·w·z, x0 := x, y 0 := y, z 0 := y} となる．ただし，ここで t = µx.J·x·yとする．よって，t = J · t · y に注意すると，η = match(J · (J · t · y) · y · z · w, J · t · y · y · (J · t · y · w · z)) =match(J · t · y · z · w, J · t · y · y · (J · t · y · w · z)) = {z := y, w := J · t · y · w · z} より，手続き 6 行目でlσθ 0? = J · t · y · z · w が返され，手続きが成功する．
次に 0 ステップのナローイングで成功する他の例を 2 例示す．
例 17 (ω-強頭部正規化可能性の反証例 (3)) R = {f(f(x)) → f(x)} とおく．まず，手続き 3 行目
で，t := f(x), σ := ∅ とおかれる．このとき，θ = mgureg (f(f(x0 )), f(x)) = {x := f(x0 )}, θ0 = {x :=f(x), x0 := x} I θ をとると，θ0? = {x := f ω , x0 := x} となる．よって，η = match(f(f(f ω )), f(f ω )) =match(f ω , f ω ) = ∅ より，手続き 6 行目で lσθ0? = f ω が返され，手続きが成功する．実際，f ω =f(f(f ω )) →²R f(f ω ) = f(f(f ω )) →²R · · · であるから，得られた項は R の ω-強頭部正規化可能性の反例になっている．
例 18 (ω-強頭部正規化可能性の反証例 (4)) R = {f(x) → f(f(x))} とおく．まず，手続き 3 行
目で，t := f(f(x)), σ := ∅ とおかれる．このとき，θ = mgureg (f(x0 ), f(f(x))) = {x0 := f(x)}となる．ここで，θ0 = {x0 := f(x)} I θ をとると，θ0? = {x0 := f(x)} となる．よって，η =match(f(x), f(f(x))) = {x := f(x)} より，手続き 6 行目で lσθ 0? = f(x) が返され，手続きが成功する．実際，f(x) →²R f(f(x)) →²R f(f(f(x))) →²R · · · であるから，得られた項は R の ω-強頭部正規化
可能性の反例になっている．
反証例 (3) では，反例として無限項が生成されている一方，反証例 (4) で生成される反例は有限項であることに注意する．
次にナローイングステップの導出についてのバリエーションがある例を 2 例示す．最初の例では，複数のナローイングステップが必要になる場合を示す．

例 19 (ω-強頭部正規化可能性の反証例 (5)) R = {f0 (x) → f1 (x), f1 (x) → f2 (x), f2 (x) → f0 (x)}とおく．まず，手続き 3 行目で，t := f1 (x), σ := ∅ とおかれる．手続き 5 行目で，f0 (x0 ) と f1 (x)との単一化に失敗するため，手続き 7 行目に飛ぶ．ここで唯一可能なナローイングステップは，
f1 (x) Ã²{x:=x1 } f2 (x1 ) である．t := f2 (x1 ), σ := {x := x1 } (8 行目) とおいて，5 行目に戻る．次もまた，f0 (x01 ) と f2 (x1 ) との単一化に失敗するため，手続き 7 行目に飛ぶ．ここで唯一可能なナロー
イングステップは，f2 (x1 ) Ã²{x1 :=x2 } f0 (x2 ) である．t := f0 (x2 ), σ := {x := x2 , x1 := x2 } (8 行目)
とおいて，5 行目に戻る．今度は，θ = mgureg (f0 (x02 ), f0 (x2 )) = {x02 := x2 }, θ0 = θ I θ をとると，
θ0? = θ．よって，η = match(f0 (x2 ), f0 (x2 )) = ∅ より，手続き 6 行目で lσθ 0? = f0 (x2 ) が返され，手続きが成功する．実際，f0 (x) →²R f1 (x) →²R f2 (x) →²R f0 (x) →²R · · · であるから，得られた項は Rの ω-強頭部正規化可能性の反例になっている．
同様に，無限項書き換えシステム R = {f0 (x) → f1 (x), f1 (x) → f2 (x), . . . , fk (x) → f0 (x)} に対しては，k − 1 ステップのナローイングが必要になることが容易にわかる．
次の例では，根でないナローイングステップが必要になる場合を示す．
例 20 (ω-強頭部正規化可能性の反証例 (6)) R = {f(x) → g(a), a → b, g(b) → f(a)} とおく．まず，手続き 3 行目で，t := g(a), σ := ∅ とおかれる．手続き 5 行目で，f(x0 ) と g(a) との単一化に失敗するため，手続き 7 行目に飛ぶ．ここで唯一可能なナローイングステップは，g(a) Ã1∅ g(b) である．このナローイングステップは，根ナローイングでないことに注意する．t := g(b), σ := ∅ (8 行目) とおいて，5 行目に戻る．次もまた，f(x0 ) と g(b) との単一化に失敗するため，手続き 7 行目に飛ぶ．こ
こで唯一可能なナローイングステップは，g(b) Ã²∅ f(a) である．t := f(a), σ := ∅ (8 行目) とおいて，
5 行目に戻る．今度は，θ = mgureg (f(x0 ), f(a)) = {x0 := a} となる．ここで，θ0 = θ I θ をとると，
θ0? = θ．よって，η = match(f(x), f(a)) = {x := a} より，手続き 6 行目で lσθ 0? = f(x) が返され，手続きが成功する．実際，f(x) →²R g(a) →1R g(b) →²R f(a) →²R g(a) →1R g(b) →²R f(a) →²R · · · であるから，得られた項は R の ω-強頭部正規化可能性の反例になっている．
次にナローイングによって得られた代入 σ によって，無限正則項が構成される例を示す．
例 21 (ω-強頭部正規化可能性の反証例 (7)) R = {f(x) → g(x), g(h(x)) → f(x)} とおく．まず，手続き 3 行目で，t := g(x), σ := ∅ とおかれる．手続き 5 行目で，f(x0 ) と g(x) との単一化に失敗するため，手続き 7 行目に飛ぶ．ここで唯一可能なナローイングステップは，g(x) Ã²{x:=h(x1 )}f(x1 ) である．t := f(x1 ), σ := {x := h(x1 )} (8 行目) とおいて，5 行目に戻る．すると，θ =mgureg (f(h(x01 )), f(x1 )) = {x1 := h(x01 )} となる．ここで，θ0 = {x1 := h(x1 ), x01 := x1 } I θ をとると，
θ0? = {x1 := hω , x01 := x1 } となる．よって，η = match(f(h(hω )), f(hω )) = match(f(hω ), f(hω )) = ∅より，手続き 6 行目で lσθ 0? = f(hω ) が返され，手続きが成功する．実際，f(hω ) →²R g(hω ) =g(h(hω )) →²R f(hω ) →²R · · · であるから，得られた項は R の ω-強頭部正規化可能性の反例になっている．
例 22 (ω-強頭部正規化可能性の反証例 (8)) R = {f(x) → h(g(x), g(x)), h(x, g(x)) → f(x)} とおく．まず，手続きの 3 行目で t := h(g(x), g(x)), σ := ∅ とおかれる．5 行目の単一化に失敗するため，手続き 7 行目に飛ぶ． ナローイングステップは h(g(x), g(x)) Ã²{x1 :=gω } f(gω ) である．
t := f(gω ), σ := {x1 := gω }(8 行目) とおいて，5 行目に戻る．θ = mgureg (f(x0 ), f(gω )) = {x0 := gω }，θ0 = {x0 := gω } I θ をとると，θ0? = {x0 := gω } となる． よって，η = match(f(gω ), f(gω )) = ∅ より，手続き 6 行目で lσθ 0? = f(gω ) が返され，手続きが成功する．実際，f(gω ) →²R h(g(gω ), g(gω )) =h(gω , g(gω )) →²R f(gω ) →²R · · · であるから，得られた項は R の ω-強頭部正規化可能性の反例になっている．

最後にナローイングの戦略によって，発散または成功する例を示す．
例 23 (ω-強頭部正規化可能性の反証例 (9)) R = {f(g(x)) → g(f(x)), g(f(x)) → f(x)} とおく．まず，手続き 3 行目で，t := g(f(x)), σ := ∅ とおかれる．手続き 5 行目で，f(g(x0 )) と g(f(x)) との単一化に失敗するため，手続き 7 行目に飛ぶ．ここでナローイングステップとして，g(f(x)) Ã1{x:=g(x1 )}g(g(f(x1 ))) をとる．t := g(g(f(x1 )))，σ := {x := g(x1 )} (8 行目) とおいて，5 行目に戻る．次もまた，f(g(x0 )) と g(g(f(x1 ))) との単一化に失敗するため，手続き 7 行目に飛ぶ．ここでナローイング
ステップとして，g(g(f(x1 ))) Ã11{x1 :=g(x2 )} g(g(g(f(x2 )))) をとる．t := g(g(g(f(x2 ))))，σ := {x :=g(g(x2 )), x1 := g(x2 )} (8 行目) とおいて，5 行目に戻る．以下，同様のナローイングステップをとり続きけると，いつまでも手続きは終了しない (発散する)．
一方，最初のナローイングステップとして，g(f(x)) Ã²{x:=x1 } f(x1 ) をとる．このときは，t := f(x1 )，σ := {x := x1 } (8 行目) とおいて，5 行目に戻る．そして，θ = mgureg (f(g(x01 )), f(x1 )) = {x1 :=g(x01 )} となる．ここで，θ0 = {x1 := g(x1 ), x01 := x1 } I θ をとると，θ0? = {x1 := gω , x01 := x1 }．
よって，η = match(f(g(gω ), f(gω )) = match(f(gω ), f(gω )) = ∅ より，手続き 6 行目で lσθ 0? = f(gω )が返され，手続きが成功する．実際，f(gω ) = f(g(gω )) →²R g(f(gω )) →²R f(gω ) →²R · · · であるから，得られた項は R の ω-強頭部正規化可能性の反例になっている．
以下では，手続き 14 の反証手続きの健全性，つまり，手続きに成功する場合には必ず ω-強頭部
正規化可能性に対する反例の存在が保証されていることを示す．
∗+

補題 24 l → r ∈ R とし，r Ãσ t, η = match(lσθ, tθ) が成立するとする．このとき，lσθ →R lσθη ．
∗∗∗(証明) r Ãσ t と補題 9 (2) より rσ →R t．よって，rσθ →R tθ．一方，η = match(lσθ, tθ) より，∗
lσθη = tθ．以上より，lσθ →²R rσθ →R tθ = lσθη ．
¤
定理 25 (ω-強頭部正規化可能性の反証手続きの健全性) 無限項書き換えシステム R に対して，手続き 14 の ω-強頭部正規化可能性の反証手続きが成功するとき，R は ω-強頭部正規化可能性を持たない．

(証明) n + 1 回目の while ループで lσθ0? が結果として返ったとする．今，t0 = r, σ0 = ∅ とおき，k(1 ≤ k ≤ n) 回目の while ループ終了後の t, σ, σ 0 の値をそれぞれ tk , σk , σk0 とおく．このとき，
i = 1, . . . , n について ti−1 Ãσi0 ti , σi = σi0 ◦σi−1 が成立する．ここで，r = t0 Ãσ10 t1 Ãσ20 · · · Ãσn0 tn ,∗00σn = σn0 ◦ σn−1 = σn0 ◦ σn−1
◦ σn−2 = · · · = σn0 ◦ σn−1
◦ · · · ◦ σ10 ．よって，r Ãσn tn ．仮定から n + 1
回目の while ループで，5 行目の条件判定に成功しているはずなので，η = match(lσn θ0? , tn θ0? ) な
る代入 θ0 , η が存在する．よって，補題 24 より題意が成立する．
¤

例 26 (組合せ子の書き換え規則に対する反証) 岩見 [22] は組合せ子の書き換え規則に対して，ω強頭部正規化可能性が成立しないことを，反例を構成することによって報告している．文献 [22] で示された組合せ子の書き換え規則の例に対して，提案手法を適用した結果および反証に成功した場合に構成された反例を表 1 に示す．なお，表中では組合せ子の適用演算子 · は省略している．ω-強頭部正規化可能性が成立しない 25 例に対して，提案手法が有効に適用できた．表下段の組合せ子
Y, U, U2 , O の書き換え規則は ω-強頭部正規化可能性を持つため，反証には成功しない．“発散” は手続きが停止しなかったことを意味する．

組合せ子

S
K
I
L
J
H
M
W
W1
W∗
W∗∗
B
C
D
E
F
G
Q
Q1
Q3
R
T
V
C∗
C∗∗
Y
U
U2
O

書き換え規則結果構成された反例

Sxyz → xz(yz)Kxy → xIx → x
Lxy → x(yy)Jxyzw → xy(xwz)
Hxyz → xyzy
Mx → xx
Wxy → xyy
W1 xy → yxx
W∗ xyz → xyzz
W∗∗ xyzw → xyzww
Bxyz → x(yz)Cxyz → xzy
Dxyzw → xy(zw)Exyzwv → xy(zwv)
Fxyz → zyx
Gxyzw → xw(yz)Qxyz → y(xz)Q1 xyz → x(zy)Q3 xyz → z(xy)Rxyz → yzx
Txy → yx
Vxyz → zxyC∗ xyzw → xywz
C∗∗ xyzwv → xyzvw
Yx → x(Yx)
Uxy → y(xxy)
U2 xy → y(xxxy)
Oxy → y(xy)

成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功
成功

S(µx.Sx)yzµx.Kxyµx.Ix(µx.Lx)yµx.Jxy
HHHH
MMWWW
W1 W1 W1
W∗ W∗ W∗ W∗
W∗∗ W∗∗ W∗∗ W∗∗ W∗∗
B(µx.Bxy)(yz)C(µx.Cx)(yz)D(µx.Dxy)yzw
E(µx.Exyz)yzwv
F(µx.Fx)y(F(µx.Fx))
G(µx.Gxy)yzw
Qx(µy.Qxy)z
Q1 (µy.Q1 xy})yz
Q3 (µx.Q3 x)y(Q3 (µx.Q3 x)y)R(µx.Rx)(R(µx.Rx))(R(µx.Rx))
T(µx.Tx)(T(µx.Tx))
V(µx.Vx)(V(µx.Vx))(V(µx.Vx))
C∗ (µx.C∗ x)yzw
C∗∗ (µx.C∗∗ x)yzwv
—
—
—
—

発散
発散
発散
発散

表 1. 組合せ子の書き換え規則に対する手続きの適用結果

例 27 (反証の発散例) 組合せ子 O の場合，以下のように手続きが発散した (以下でも · は省略する)．
R = {Oxy → y(xy)} とおく．まず, 手続き 3 行目で, t := y(xy), σ := ∅ とおかれる．このとき, θ =mgureg (Ox0 y 0 , y(xy)) = {y := Ox0 , y 0 := x(Ox0 )} より, θ0 = {y := Ox, y 0 := x(Ox), x0 := x} I θ をとる．θ0? = {y := Ox, y 0 := x(Ox), x0 := x} であるが, η = match(Ox(Ox), Ox(x(Ox))) が失敗し, 7行目に移る．t = y(xy) Ã²{x:=x1 ,y:=Ox1 } x1 (Ox1 )(x1 (x1 (Ox1 ))) = t0 より, t := x1 (Ox1 )(x1 (x1 (Ox1 ))),
σ := {x := x1 , y := Ox1 }．次に，5 行目の単一化 mgureg (Ox01 (Ox01 ), x1 (Ox1 )(x1 (x1 (Ox1 )))) が失敗し，7 行目に移る．次に，t = x1 (Ox1 )(x1 (x1 (Ox1 ))) Ã²{x1 :=O} O(O(OO))(OO(O(O(OO)))) = t0
より，t := O(O(OO))(OO(O(O(OO)))), σ := {x := O, y := OO, x1 := O} となる．以降, 5 行目の単一化に失敗し, 7 行目に移ることを繰り返し, 手続きは発散する．

5

おわりに

本論文では，無限項書き換えシステムにおける ω-強頭部正規化可能性について，その反証手続きを与えるとともに，手続きの健全性を証明した．提案した反証手続きの特徴は，より長い書き換え列を可能とするための代入から，変数の同一視により正則項による反例を具体的に構築する点である．従来，このような正則項を利用した ω-強頭部正規化可能性の反証法は知られておらず，提案手法を従来の ω-強頭部正規化可能性の自動証明法と組み合わせることにより，より強力な ω-強頭部
正規化可能性の自動判定法が実現可能である．
また，文献 [22] において非 ω-強頭部正規化可能性が報告されている組合せ子の書き換えシステ
ム 25 例に対して提案手続きを適用した結果，全 25 例に対して提案手法が有効であることが確認できた．
本論文では無限項書き換え規則の右辺を有限項に限定したが，容易に確認できるように無限項書
き換え規則の右辺を正則項へ制限を緩めても本論文の反証手続きは適用可能である．また，ω-強頭部正規化可能性を持たない無限項書き換えシステムは非強頭部正規化可能であるから，提案手続き
は強頭部正規化可能性の反証手続きにもなっている．
提案した反証手続きが完全か否か，つまり，ω-強頭部正規化可能性を持たない無限項書き換えシ
ステムに対して反証手続きが必ず成功するか否かは，まだ未解決である．ストリームの生成性検証[1, 8] や良定義性検証 [21] などへの応用を考えるには，計算戦略を考慮に入れる場合への拡張が重要となるが，これも今後の課題である．

謝辞
本研究に対してアドバイスやコメントをいただきました外山芳人教授および査読者の方々に感謝致します．本研究は日本学術振興会科学研究費 20500002, 21700017 の補助を一部受けて行われた．

参考文献[1] A. Ishihara. Productivity of algorithmic systems. In Proc. of SCSS 2008, pages 81–95, 2008.
[2] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[3] H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. 2nd revised edition, North-Holland,
1984.
[4] A. Colmerauer. Equations and inequations on ﬁnite and inﬁnite trees. In Proc. of FGCS 1984, pages
85–99, 1984.
[5] B. Courcelle. Fundamental properties of inﬁnite trees. Theoretical Computer Science, 25:95–169, 1983.
[6] H. B. Curry and R. Feys. Combinatory Logic. vol. 1, North-Holland, 1958.

[7] J. Endrullis, C. Grabmayer, D. Hendriks, J. W. Klop, and R. de Vrijer. Proving inﬁnitary normalization.
In Proc. of TYPES 2008, volume 5497 of LNCS, pages 64–82. Springer-Verlag, 2009.
[8] J. Endrullis, C. Grabmayer, D. Hendriks, A. Ariya and J. W. Klop. Productivity of stream deﬁnitions,
Theoretical Computer Science, 411:765–782, 2010.
[9] J. Giesl, R. Thiemann, and P. Schneider-Kamp. Mechanizing and improving dependency pairs. Journalof Automated Reasoning, 37(3):155–203, 2006.
[10] N. Hirokawa and A. Middeldorp. Tyrolean termination tool: Techniques and features. Information
and Computation, 205(4):474–511, 2007.
[11] P. Inverardi and M. V. Zilli. Rational rewriting. In Proc. of MFCS 1994, volume 841 of LNCS, pages
433–442. Springer-Verlag, 1994.
[12] J. Jaﬀar. Eﬃcient uniﬁcation over inﬁnite trees. New Generation Computing, 2:207–219, 1984.
[13] J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. On the adequacy of graph rewriting
for simulating term rewriting. ACM Transactions on Programming Languages and Systems, 16(3):493– 523, 1994.
[14] R. Kennaway, J. W. Klop, M. R. Sleep and F. -J. de Vries. Transﬁnite reductions in orthogonal term
rewriting systems. Information and Computation, 119:18–38, 1995.
[15] J. W. Klop and R. C. de Vrijer. Inﬁnitary normalization. In: We Will Show Them! Essays in Honourof D. Gabbay, vol. 2, pages 169–192, College Publications, 2005.
[16] K. Mukai. A uniﬁcation algorithm for inﬁnite trees. In Proc. of IJCAI 1983, pages 547–549, 1983.
[17] R. Smullyan. To Mock a Mockingbird. Knopf, New York, 1985.
[18] Terese. Term Rewriting Systems. Cambridge University Press, 2003.
[19] R. Thiemann and C. Sternagel, Loops under strategies. In Proc. of RTA 2009, volume 5595 of LNCS,
pages 17–31. Springer-Verlag, 2009.
[20] H. Zantema. Normalization of inﬁnite terms. In Proc. of RTA 2008, volume 5117 of LNCS, pages
441–455. Springer-Verlag, 2008.
[21] H. Zantema. Well-deﬁnedness of streams by termination. In Proc. of RTA 2009, volume 5595 of
LNCS, pages 164–178. Springer-Verlag, 2009.
[22] 岩見宗弘. 組合せ子の強収束性. In FIT2009 第 1 分冊 A-011, pages 251–258, 2009.