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

文脈移動法によるプログラム変換の正当性について
菊池 健太郎

青戸 等人

外山 芳人

プログラムの自動検証を容易にすることを目的としたプログラム変換法として，Giesl(2000) により文脈移動法および文脈分割法が提案されている．それらの手法は，先行評価の関数型言語における末尾再帰プログラムを自動検証に適した非末尾再帰プログラムへと変換する．本稿では，佐藤ら (2015) によって定式化された項書き換えシステムに対する文脈移動法の正当性を，先行評価に基づく意味論と始代数に基づく意味論に対して証明し，二種類の意味論における正当性の違いについて説明する．て説明する．

1 はじめに
末尾再帰プログラムは，最後の再帰呼び出しの結果を返り値に用い，呼び出し時の実行状態を保持する必要のない効率的なプログラムである．末尾再帰プログ

2 準備
本節では，項書き換えシステムに関する用語や概念を文献 [1] に従って定義する．

ラムは，一般に計算の途中結果を保存するためアキュ

関数記号と変数の集合をそれぞれ F , V とする．

ムレータとよばれる引数をもつ．しかし，その値は再F, V で構成できる項全体の集合を T (F , V) と記す．

帰呼び出しで変化するため，末尾再帰プログラムに対項 t に含まれる変数全体の集合を V(t)，関数記号全体して帰納法に基づく自動証明を適用することは困難の集合を F (t) で表す．項の列 t1 , t2 , . . . , tn を t̄ で表∪n∪す．このとき V(t̄) = ni=1 F (ti )i=1 V(ti )，F(t̄) =であることが知られている．

Giesl [2] は，先行評価の関数型プログラムを対象に，と定める．V(t) = ∅ であるとき項 t を基底項とよび，検証のための変換法として文脈移動法・文脈分割法を

基底項の集合を T (F ) で表す．項 t の根記号 root(t)提案した．それらの手法は，適当な条件のもとで，末は，t ∈ V のとき t，t = f (t1 , . . . , tn ) のとき f であ尾再帰プログラムを等価な非末尾再帰プログラムへとる．特別な定数記号 □ をちょうど 1 つ含む項を文脈変換する．変換で得られた非末尾再帰プログラムは，とよび，文脈 C の □ を t で置き換えた項を C[t] で表帰納法による自動証明に適した構造となっている．

す．文脈 C は C[ ] とも表す．写像 θ : V → T (F , V)

本稿では，佐藤ら [4] によって定式化された項書きを代入とよび，θ : T (F , V) → T (F , V) へ自然に拡張

換えシステムに対する文脈移動法の正当性を，先行評する．代入 θg : V → T (F ) を基底代入とよぶ．以下

価に基づく意味論と始代数に基づく意味論に対してでは θ(t) を tθ と表記する．

証明し，二種類の意味論における正当性の違いについ項の対 (l, r) が l ∈/ V かつ V(l) ⊇ V(r) をみたすと
き (l, r) を書き換え規則といい，l → r と表す．項書き

On the Correctness of Context-Moving Transformations.
Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama,
東北大学電気通信研究所, Research Institute of Electrical Communication, Tohoku University.

換えシステム R は書き換え規則の有限集合である (なお，項書き換えシステム中の変数は必要に応じて名前替えを行う)．項書き換えシステム R の定義関数記号の集合を D = {root(l) | l → r ∈ R}，R の構成子記

号の集合を C = F \ D と定める．項 v ∈ T (C, V) を構成子項という．項書き換えシステム R のすべての書き換え規則 f (l1 , . . . , ln ) → r について li (1 ≤ i ≤ n)が構成子項であるとき，R を構成子システムとよぶ．

R=項 v ∈ T (C) を基底構成子項という．θgc : V → T (C)を基底構成子代入とよぶ．


Mult(S(x), y, z) → Mult(x, y, Add (y, z)) Mult(0, y, z) → z
Add (S(x), y) → S(Add (x, y)) Add (0, y) → y

関数記号 Mult を変換対象，z をアキュムレータとして文脈移動法を適用する．R の規則は以下のように3 項書き換えシステムに対する文脈移動法
本節では，文献 [4] で定式化された項書き換えシス
テムに対する文脈移動法の正当性が，先行評価に基づく意味論と始代数に基づく意味論において成り立つことを示す．また，それらの意味論における正当性の違いについて議論する．

分割される．

RA = {Mult(S(x), y, z) → Mult(x, y, Add (y, z))
RB = {Mult(0, y, z) → z Add (S(x), y) → S(Add (x, y))RC = Add (0, y) → y
ここで，移動文脈は C1 = Add (y, □), C2 = □ であ

3. 1 文脈移動法による項書き換えシステムの変換
関数型プログラムの文脈移動法 [2] は，末尾再帰呼る．このとき′RA= {Mult(S(x), y, z) → Add (y, Mult(x, y, z))

び出しにおけるアキュムレータ位置の文脈を，再帰呼となる．よって，以下の項書き換えシステム R′ が得び出しの外側に移動する．項書き換えシステムに対すられる．
 Mult(S(x), y, z) → Add (y, Mult(x, y, z)) Mult(0, y, z) → z′
R =
Add (S(x), y) → S(Add (x, y)) Add (0, y) → y

る文脈移動法 [4] も同様な考え方に基づいて定式化される．
定義 3.1 (項書き換えシステムに対する文脈移動法).
項書き換えシステムに対する文脈移動法は，以下の項書き換えシステム R から R′ への変換である．

R = RA ∪ RB ∪ RC
RA = {f (¯li , z) → f (r̄i , Ci [z]) | 1 ≤ i ≤ m}

本節の残りでは，二種類の意味論における文脈移動法の正当性について議論する．

RB = {f (¯lj , z) → Cj [z] | m + 1 ≤ j ≤ n}
RC = {lk → rk | n + 1 ≤ k ≤ p}
R′3. 2 先行評価意味論における文脈移動法の正当性′= RA∪ RB ∪ RC

まず，文献 [2] と同様な先行評価に基づく意味論に′RA= {f (¯li , z) → Ci [f (r̄i , z)] | 1 ≤ i ≤ m}
′RA , RAは m 個の f の再帰規則，RB は n−m 個の fの非再帰規則，RC は p−n 個の補助関数の書き換え規おける文脈移動法の正当性について議論する．本小節
では，文脈移動法による変換の対象となる項書き換えシステムとして，構成子システム R を考える．

則を表す．関数記号 f を変換対象，文脈 C1 [ ], . . . , Cn [ ]項 s が項 t に先行戦略によって書き換えられるとを移動文脈，変数 z をアキュムレータとよぶ．変換対象

は，書き換え規則 l → r ∈ R，文脈 C[ ]，基底構成f とアキュムレータ z は上記の変換規則で明示された子代入 θgc が存在して，s = C[lθgc ] かつ t = C[rθgc ]場所以外には出現しないものとする．すなわち，以下∪¯の (i), (ii) を仮定する．(i) f ∈/( mi=1 F(li , r̄i , Ci )) ∪∪n∪p¯( j=m+1 F (lj , Cj )) ∪ ( k=n+1 F (lk , rk )). (ii) z ∈/∪m∪n¯¯(V(li , r̄i , Ci )) ∪ (V(lj , Cj )).となることである．以下では，決定性をもつ書き換え

i=1j=m+1ev

を考え，s が t に書き換えられるとき s →R t と記す．
ev

→R の反射推移閉包を →∗R で表す．s ≡R t とは，任ev

ev

意の基底構成子項 v に対して，s →∗R v が成り立つと
ev

例 3.2 (文脈移動法による変換例). 乗算を行う次のき，かつそのときに限り t →∗R v が成り立つことで項書き換えシステム R を考える．

ある．

ev

先行評価意味論における文脈移動法の正当性を保が存在して，s = C[lθ] かつ t = C[rθ] をみたすこと証するため，文献 [2] を参考に，移動文脈の交換律をであり，このとき s →R t と記す．→R の反射推移閉

以下で定義する．

包を →R で表す．s →R t となる t が存在しないとき

定義 3.3 (文脈交換律). C1 [ ], . . . , Cn [ ] を移動文脈

s を正規形という．t →R s かつ s が正規形であるととする．このとき，以下の条件を文脈交換律とよぶ．

き s は t の正規形であるという．t の正規形 s が存在∗

∀i(1 ≤ i ≤ m).∀j(1 ≤ j ≤ n).∀θgc .
ev∗

して一意に定まるとき，s を t↓R と記す．任意の基底∗∗(CCOM )

項 t, t1 , t2 について t →R t1 かつ t →R t2 ならばある

ただし，Ci [ ], Cj [ ] は共通変数をもたないように，変基底項 s が存在して t1 →R s かつ t2 →R s となると数の名前替えを行う．

き R は基底合流性をもつという．任意の基底項 s に例 3.4 (文脈交換律の例). 例 3.2 の文脈移動法に対してある基底構成子項 v が存在して s →R v が成よる変換を考える．移動文脈は，C1 = Add (y, □)立するとき，R は十分完全性 [3] をもつという．R が(m = 1), C2 = □ (n = 2) であるから，文脈交換律

基底合流性と十分完全性をもつとき，任意の基底項 sCi [Cj [z]]θgc ≡R Cj [Ci [z]]θgcev

ev∗∗∗の条件 (CCOM ) は，∀θgc .Add (x, Add (y, z))θgc ≡Rに対して s↓R が定義され，基底構成子項となる．本Add (y, Add (x, z))θgc となる．

小節では，変換対象として，基底合流性と十分完全性

ev
定義 3.5 (R ⇒fcm R′ ).

をもつ項書き換えシステム R を考える．

ev

R を構成子システムとする．

関数記号 f を変換対象とする文脈移動法によって R′ev

本小節で考える意味論における文脈移動法の正当から R が得られ，文脈交換律の条件 (CCOM ) がみ性を保証するため，移動文脈の交換律を以下で定義

ev
たされているとき，R ⇒fcm R′ と書く．

する．

以下の補題が成り立つ (証明は文献 [5] を参照)．
補題 3.6.

ev
R ⇒fcm R′ とし，1 ≤ i ≤ m とする．任意定義 3.8 (文脈交換律). C1 [ ], . . . , Cn [ ] を移動文脈とする．このとき，以下の条件を文脈交換律とよぶ．の基底構成子代入 θgc と基底項 t̄, u，基底構成子項 v∀i(1 ≤ i ≤ m).∀j(1 ≤ j ≤ n).∀θg .

に対して，以下が成立する．

Ci [Cj [z]]θg ↓R = Cj [Ci [z]]θg ↓Revev
1. Ci θgc [f (t̄, u)] →∗R v ならば f (t̄, Ci θgc [u]) →∗R v ．
ev
ev
2. f (t̄, Ci θgc [u]) →∗R′ v ならば Ci θgc [f (t̄, u)] →∗R′ v ．

上の補題を用いて，先行評価意味論における文脈移(CCOM)

ただし，Ci [ ], Cj [ ] は共通変数をもたないように，変数の名前替えを行う．
定義 3.3 における条件 (CCOMev ) とは異なり，上動法の正当性が示される．の条件 (CCOM) は，R の始代数上で成り立つ等式，ev定理 3.7. R ⇒fcm R′ とする．任意の基底項 s と基底ev構成子項 v に対して，s →∗R v が成り立つとき，かつevそのときに限り s →∗R′ v が成り立つ．

すなわち R の帰納的定理に対応する．したがって，帰納的定理証明器による検証が可能である．
定義 3.9 (R ⇒fcm R′ ). R を基底合流性と十分完全性をもつ項書き換えシステムとする．関数記号 f を

3. 3 始代数意味論における文脈移動法の正当性

変換対象とする文脈移動法によって R から R′ が得ら

前小節で示された文脈移動法の正当性は，文脈交換れ，文脈交換律の条件 (CCOM) がみたされているとev

律の条件 (CCOM ) に基づいているが，それは先行き，R ⇒fcm R′ と書く．

評価の概念に依存しており，始代数上の等式に対応す

以下の補題が成り立つ (証明は文献 [5] を参照)．

るとは限らない．本小節では，始代数上の等式に正確

補 題 3.10. R ⇒fcm R′ の と き ，任 意 の 基 底 代 入に対応する文脈交換律の条件に基づいて，前小節とは

θg \f : V → T (F \ {f }) と基底構成子項 v に対して，異なる文脈移動法の正当性を示す．

f (x̄, z)θg \f →R v ならば f (x̄, z)θg \f →R′ v が成立

はじめに，項書き換えシステムにおける標準的な∗∗する．

定義をいくつか導入する．項 s が項 t に書き換えられ補題 3.11. R ⇒fcm R′ のとき，任意の基底項 s と基るとは，書き換え規則 l → r ∈ R，文脈 C[ ]，代入 θ

底構成子項 v に対して，s →R v ならば s →R′ v が∗∗成立する．

′が成立する．したがって，R ⇒Sumcm R が成り立ち，

補題 3.12. R ⇒fcm R′ のとき，R′ は十分完全性を′∪ {(b)–(h)} が得られる．
R ′ = RA

もつ．

以上の変換において，ソート Nat の項に対しては，補題 3.13. R ⇒fcm R′ のとき，任意の基底項 s と基∗∗本小節で行った文脈移動法の正当性に関する議論が

底構成子項 v に対して，s →R′ v ならば s →R v が成立する (ソート NatStream の項に対しては，定理成立する．

3.15 の形での変換の正当性は要求しない)．

補題 3.14.

R ⇒fcm R′ のとき，R′ は基底合流性をもつ．

この変換に対しては，定理 3.7 による文脈移動法の正当性も成立する．しかし，関数記号 Inc を含む基以上より，前小節とは異なる文脈移動法の正当性を表す次の定理が示される．
定理 3.15.

底項については，規則 (e) により先行戦略による書き換えが停止しない．したがって，それらの項に対して

R ⇒fcm R′ であるとき，任意の基底項 sについて s↓R = s↓R′ が成立する．

定理 3.7 で示されることは，書き換えの非停止性が変換によって保存されるということのみである．

例 3.16. 本例では，ソート Nat と NatStream をもつ多ソート項書き換えシステム R を考える．ここで，4 おわりにソート Nat × NatStream → NatStream をもつ “:”

本稿では，項書き換えシステムに対する文脈移動法

は，ソート NatStream の唯一の構成子記号である．
(a) Sum(S(x), α, z) →
Sum(x, Tl (α), Add (Hd (α), z))




(b)
Sum(0,α, z) → z (c) Hd (x : α) → xの正当性が，先行評価意味論と始代数意味論という二R=ある．

(d)

Tl (x : α) → α(e) Inc → 0 : Succ(Inc)





(f ) Succ(x : α) → S(x) : Succ(α)





(g) Add (S(x), y) → S(Add (x, y))(h) Add (0, y) → y

関数記号 Sum を変換対象，z をアキュムレータとして文脈移動法を適用する．ここで，ソート Nat の項に対しては十分完全性が成り立つ．すなわち，ソート Nat の任意の基底項は，ある基底構成子項に書き換えられる．R の規則は RA = {(a)}, RB = {(b)},RC = {(c)–(h)} のように分割される．移動文脈は
C1 = Add (Hd (α), □), C2 = □ である．このとき
 (a)′ Sum(S(x), α, z) →′RA =
Add (Hd (α), Sum(x, Tl (α), z))となる．また∀θg .Add (Hd (α), Add (Hd (β), z))θg ↓R =Add (Hd (β), Add (Hd (α), z))θg ↓R(CCOM)

種類の意味論において成立することを示した．また，それらの意味論における正当性の違いを明らかにする例を与えた．それぞれの正当性を保証するための条件を判定する手続きの実装については今後の課題で参 考 文 献[ 1 ] F. Baader and T. Nipkow. Term Rewriting andAll That. Cambridge University Press, 1998.
[ 2 ] J. Giesl. Context-moving transformations forfunction verification. In Proc. of 9th LOPSTR, volume 1817 of LNCS, pages 293–312. Springer-Verlag,
2000.
[ 3 ] D. Kapur, P. Narendran, and H. Zhang.
On suﬃcient-completeness and related propertiesof term rewriting systems.
Acta Informatica,
24(4):395–415, 1987.
[ 4 ] 佐藤洸一, 菊池健太郎, 青戸等人, 外山 芳人. 項書き換えシステムの変換を利用した帰納的定理自動証明. コンピュータソフトウェア, 32(1):179–193, 2015.
[ 5 ] K. Sato, K. Kikuchi, T. Aoto, and Y. Toyama.
Correctness of context-moving transformations forterm rewriting systems. In Pre-proc. of 25th LOPSTR, 2015. Available at http://www.nue.riec.
tohoku.ac.jp/user/kentaro/cntxt/.