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

論理制約付き項書き換えシステムにおける新しい制約付き項の書き換えの提案
高畑 幹汰

青戸 等人

等式論理に基づく基本的な項書き換えシステムでは扱いが難しい, 整数型といった帰納的な構造を持たないデータ型を扱う仕組みを持つ項書き換えの体系として, 論理制約付き項書き換えシステム (LCTRS) が提案されている(Nishida & Kop, 2013). LCTRS では通常の項の書き換えの他に, 制約付き項の書き換えが考えられている. しかし, 通常の項の書き換えと異なり, 等価変換が定義に組み込まれているため, 制約付き項の書き換えの計算は容易でな
い. また, 同一の規則を用いて同一の位置で書き換えたとしても書き換えの結果が一意に定まらない, 書き換えの前に等価変形を行わないと書き換えられない場合もある等, 取り扱いが困難である. そこで, 本稿では制約付き項の定義やその書き換えの定義を見直し,LCTRS における新しい制約付き項とその書き換えを提案する. また, 等価関係の定義から自然に導かれる擬順序を用いて従来の制約付き項の書き換えと新しい制約付き項の書き換えの間の関係を示す.

における書き換えの結果が一意に定まらないような

1 はじめに例を以下に示す.

項書き換えシステムは等式論理に基づく計算モデ

例 1.1. 以下のような規則を考える．

ルである. 項書き換えシステムは純粋に形式的なモデ

f (x) → g(y)[x ≥ 0]ルであるため，整数や浮動小数点といった帰納的な構

この規則を用いて，f (x)[x ≥ 0] という制約付き項の造を持たないデータ型の扱いが困難である. そのため，書き換えを考える．すぐに書き換える場合は以下のよ

それらの取り扱いを容易にするために，論理制約付き

うな項を考えることができる．

f (x)[x ≥ 0] →rule g(x)[x ≥ 0]

項書き換えシステム (LCTRS) が提案されている [2].
また，合流性や完備化，書き換え帰納法などの研究がまた，具体的な数値を直接入れてしまっても，問題進められている [1] [3] [4] [5].

ない．

LCTRS では通常の項の書き換えの他に，制約付き

f (x)[x ≥ 0] →rule g(3)[x ≥ 0]

項の書き換えが考えられている. 制約付き項は項と論書き換える前に制約付き項における等価関係を用い

理制約の対で与えられる. 制約付き項の書き換えには，て等価変換を行ったあと，書き換えることもできる.

通常の後の書き換えと異なり，等価変換が定義に組み

例えば，変数と制約を増やした後に書き換えることも込まれているため，書き換えの計算が容易でない. ま

できる.

∼

f (x)[x ≥ 0 ∧ y < 0]ても書き換えの結果が一意に定まらないことや書き→ruleg(y)[x ≥ 0 ∧ y < 0]

換えの前に等価変換を行わないと書き換えができな

また，関係のない変数を加えることもできる.

い場合もある等，取り扱いが困難である. 制約付き項

f (x)[x ≥ 0]

た，同一の規則を用いて同一の位置で書き換えたとし∗ A New Format of Rewriting for Constrained Terms

in Logically Constrained Term Rewriting Systems.
Kanta Takahata, Takahito Aoto, 新潟大学大学院自然科学研究科, Graduate School of Science and Technology, Niigata University.

f (x)[x ≥ 0]∼

f (x)[x ≥ 0 ∧ y = −3 ∧ z > π]→ruleg(y)[x ≥ 0 ∧ y = −3 ∧ z > π]等価変換を行ってから書き換えることで，書き換え結果に無限のバリエーションを生み出すことができる.
同様に書き換えた後の結果に対して，等価変換を行う

ことでも無限のバリエーションを得ることができる．

また，制約付き規則 l → r[φ] の論理変数は LVar(l →このように，制約付き項の書き換えは計算結果が一r[φ]) = Var(φ) \ (Var(r) \ Var(l)) と定義される. 同

意に定まらず，また一つの項から同じ規則で書き換え

様に EVar(l → r[φ]) = Var(r) \ (Var(l) ∪ Var(φ))

られた項同士が等価関係を満たすとも限らない．

と 定 義 す る.

本稿では新しい制約付き項の枠組みとして，存在制

代 入 γ が 規 則 を respect す る とは ，以 下 の 3 つ の 条 件 を 満 た す と き で あ る.

1.

約付き項とその書き換えを提案する. 存在制約付き項

dom(γ) = Var(l) ∪ Var(r) ∪ Var(φ), 2. 任意の変のアイデアは，制約付き項の論理制約に存在量化子を

数 x ∈ LVar(l → r[φ]) について，γ(x) ∈ Val, 3.

つけることで，論理制約のみに出現する変数を束縛すM ⊨ φγ. このとき，γ ⊨ l → r[φ] と表記する．

ることにある. この意図するところは書き換えを制限して，より性質のいい書き換え関係を構成することに関数記号の集合 F, モデル M, 制約付き規則の集合

R の 3 つ組 hF, M, Ri を LCTRS と呼ぶ．

ある．また，書き換えを行うことで変数が新しく出現
したり，あるいはなくなってしまうような場合でも破2. 2 制約付き項

綻しないように書き換えを再定義する. そして，存在制約付き項は項と論理制約の対で与えられ，項 s と制約付き項の書き換えと通常の制約付き項の書き換

論理制約 φ を用いて，s[φ] で表される．代入 γ が論

えを，等価関係から自然に導かれる擬順序を用いて，

理制約 φ を respect するとは，以下の 2 つの条件を

従来の制約付き項の書き換えと存在制約付き項の書満たすときをいう．1. 任意の変数 x ∈ Var(φ) につ

き換えの間の関係を示す.

本稿の構成は以下の通り

いて，γ(x) ∈ Val, 2. M ⊨ φγ. このとき，γ ⊨ φ とである. 第 2 節は準備である. 第 3 節では，存在制約表記する．制約付き項 s[φ], t[ψ] が等価関係にある付き項の定義とその等価関係，書き換え関係を示す.

とは，γ ⊨ φ を満たす任意の代入 γ について，δ ⊨ ψ

第 4 節では従来の制約付き項の書き換えと新しく定を満たす代入が存在し，sγ = tδ を満たし，またそ義した存在制約付き項の書き換えの関係性を示す. 第の逆も成り立つときである．このとき，s[φ] ∼ t[ψ]5 節は，本稿のまとめである.

と表記する．制約付き項上の書き換え s[φ] →rule t[ψ]と s[φ] →calc t[ψ] について定義する．制約付き項

2 準備

s[φ], t[ψ] について，s[φ] →rule t[ψ] とは，以下をみ

2. 1 論理制約付き項書き換えシステム

たす l → r[π] ∈ R, γ が存在するときをいう.

多ソート関数記号の集合 F は F = Fterms ] Ftheory• φ が充足可能で φ = ψ,で与えられる. また，全てのソート ι について，それぞ• s = C [lσ], t = C [rσ],れのソートは値の集合 Valι を持ち，Valι ⊆ Ftheory∪
である．また，値の全体集合は Val = ι Valι で定義• dom(γ) = Var(l) ∪ Var(r) ∪ Var(π),• 任意の x ∈ LVar(l → r[π]) について，γ(x) ∈される．変数の集合は V で表され，V ∩ F = ∅ であVal ∪ Var(φ),

る．項の全体集合を T (F, V) と記す．M = hI, J i を• M ⊨ φ ⇒ (πγ)．

Ftheory 上のモデルとする．ここで，I(ι) はソート ι

制約付き項 s[φ], t[ψ] について，s[φ] →calc t[ψ] とはの台集合を，J (f ) は f ∈ Ftheory の解釈を与える．こ以下を満たすときをいう．

こで，I(ι) ∼= Valι と仮定する. また，T (Ftheory , V)

• 関数記号 f ∈ Ftheory \ Fterms と，s1 , . . . , sn ∈は論理項と呼ぶ．また論理項のうち，ソートが bool

Val ∪ Var(φ) を用いて，s = C [f (s1 , . . . , sn )],なものを論理制約と呼ぶ．論理制約 φ が妥当である• 新しい変数 x を用いて，t = C [x],とは，M 上の任意の付値 ρ について，JφKρ = True

• ψ = (φ ∧ x = f (s1 , . . . , sn )).

となるときであり，M ⊨ φ と記す．制約付き規則は，

ここで，制約付き項上の書き換えについて →R =l, r ∈ T (F, V) と論理制約 φ を用いて，l → r[φ] の→rule ∪ →calc , −→R = ∼ ◦ →R ◦ ∼ のように定義する．

三つ組で定義される．ただし，l(ϵ) ∈ Fterms \ Ftheory ．

∼

存在制約付き項の例

3 存在制約付き項の等価関係と書き換え関係

f (x)[∃y.x = 3 ∧ y = y]f (x)[x = 3]

第 3 節では存在制約付き項とその書き換え，等価g(x, y)[∃z.x = 2z ∨ y = 3z]h[∃x.x ≥ 0]

関係を定義する. また Rule 書き換え，Calc 書き換え

補題 3.4. 任意の存在制約付き項 s[∃⃗x.φ] について，それぞれについて，制約付き項における書き換えと存BV(∃⃗x.φ) = Var(φ) \ Var(s).

在制約付き項における書き換えの間の関係を等価関係の定義から自然に導かれる擬順序を用いて示す.

(証明). (⊆)

定義より，BV(∃⃗x.φ) ∩ Var(s) = ∅. ま

た BV(∃⃗
x.φ) ⊆ Var(φ) より，BV(∃⃗x.φ) ⊆ Var(φ) \Var(s).
3. 1 存在制約付き項(⊇)

定義 3.1 (存在量化子付き論理制約). 存在量化子付
き論理制約とは ∃x1 , . . . , xn .φ の形の述語論理式をいう (n ≥ 0). ここで，φ は論理制約であり，x1 , . . . , xn
は {x1 , . . . , xn } ⊆ Var(φ) を満たす. 以降では，略記のために変数列 x1 , . . . , xn を ⃗x のように表現する.

y ∈ Var(φ) \ Var(s) に つ い て 考 え る. 定

義 よ り，Var(s) ⊇ FV(∃⃗x.φ) が 言 え る の で ，y ∈/FV(∃⃗x.φ).

つ ま り，y ∈ Var(φ) \ FV(∃⃗x.φ) =

BV(∃⃗x.φ). 以上より，Var(φ) \ Var(s) ⊆ BV(∃⃗x.φ)が 言 え る.

し た がって ，BV(∃⃗x.φ) = Var(φ) \Var(s).

また存在量化子付き論理制約について，自由変数

FV(∃⃗x.φ) と束縛変数 BV(∃⃗x.φ) をそれぞれ以下のよ

補題 3.5. 任意の存在制約付き項 s[∃⃗x.φ] について，

うに定義する.

FV(∃⃗x.φ) = Var(φ) ∩ Var(s).

• FV(∃⃗x.φ) = Var(φ) \ {⃗x}.

(証明). (⊆)

• BV(∃⃗x.φ) = {⃗x}.

つまり，FV(∃⃗x.φ) ⊆ Var(φ). また，FV(∃⃗x.φ) ⊆定義 3.2 (存在制約付き項). 存在制約付き項 (Exis-

tential Constrained Term) とは s[∃⃗x.φ] のように表

定義より，FV(∃⃗x.φ) = Var(φ) \ {⃗x}.

Var(s). したがって，FV(∃⃗x.φ) ⊆ Var(φ) ∩ Var(s).
(⊇)

y ∈ Var(φ) ∩ Var(s) に つ い て 考 え る. 定される，項と存在量化子付き論理制約の対で，以下の義 よ り，BV(∃⃗x.φ) ∩ Var(s) = ∅ が 言 え る の で ，条件を満たすものをいう:

y ∈/ BV(∃⃗x.φ). つまり，y ∈ Var(φ) \ BV(∃⃗x.φ) =• s は項，∃⃗x.φ は存在量化子付き論理制約.

FV(∃⃗x.φ). 以上より，Var(φ) ∩ Var(s) ⊆ FV(∃⃗x.φ)• Var(s) ⊇ FV(∃⃗x.φ).

が言える.

• BV(∃⃗x.φ) ∩ Var(s) = ∅.

したがって，FV(∃⃗x.φ) = Var(φ) ∩ Var(s).

例 3.3 に存在制約付き項でない例と存在制約付き項である例を示す. 例にある通り，通常の制約付き項でも存在制約付き項の条件を満たすこともある.
例 3.3. 存在制約付き項でない例

f (x)[x = 3 ∧ y = y]g(x, y)[x = 2z ∨ y = 3z]

f (x)[∃⃗x.x = 3 ∧ y = 2]h[∃⃗y .x ≥ 0]

左上，左下， 右下の項は，存在制約付き項の自由変数と項の変数集合の関係の定義に反している. さらに，
右下の項は存在量化子付き論理制約の定義に反している. 右上の項は束縛変数と項の変数集合の重なる部分がないという条件に反している.

次に，制約付き項と存在制約付き項の変換を定義
する.
定義 3.6 (通常の制約付き項から存在制約付き項への変換). 制約付き項から，存在制約付き項への変換 ext を ext(s[φ]) = s[∃⃗x.φ] により定義する. ここで，{⃗x} = Var(φ) \ Var(s). この変換を Existential

Extension Transformation(EE 変換) と呼ぶ.
逆に，存在制約付き項から，制約付き項への変換

rmv を rmv (s[∃⃗x.φ]) = s[φ] と定義し，Existential
Removal Transformation(ER 変換) と呼ぶ.
例 3.7. f (x, y)[z = x + y ∧ w ≥ 0] という制約付き項の，存在制約付き項への変換を考えると，以下のよ例 3.10.

うになるf (x)[∃y.x = 3 ∧ y = y]ext(f (x, y)[z = x + y]) = f (x, y)[∃z.z = x + y]
逆に, 存在制約付き項 f (x, y)[∃z, w.z = x+y ∧w ≥ 0]∼

f (z)[∃x, y.x = 3 ∧ y = y ∧ z = x]

補題 3.11. 制約付き項 s[φ] とその存在制約付き項へを制約付き項へ変換すると，以下のようになる.

rmv (f (x, y)[∃z.z = x + y]) = f (x, y)[z = x + y]の変換 ext(s[φ]) について，以下の関係が成立する.

s[φ] ∼ ext(s[φ])補題 3.8. 制約付き項 s[φ] について，

rmv (ext(s[φ])) = s[φ]同様に，存在制約付き項 s[∃⃗x.φ] とその制約付き項へが成立する. 同様に，存在制約付き項 s[∃⃗x.φ] につの変換 rmv (s[∃⃗x.φ]) について以下の関係が成立する.

s[∃⃗x.φ] ∼ rmv (s[∃⃗x.φ])

いて，ext(rmv (s[∃⃗x.φ])) = s[∃⃗x.φ](証明). s[φ] ∼ ext(s[φ]) について考える. ここで，が成立する.

ext(s[φ]) = s[∃⃗x.φ] とする. 任意の γ ⊨ φ を満たす
代入 γ は γ ⊨ ∃⃗x.φ も満たす. 当然，sγ = sγ.

(証明). rmv (ext(s[φ])) = s[φ] は自明.
ext(rmv (s[∃⃗x.φ])) = s[∃⃗x.φ] について考える. 定

逆に，任意の δ ⊨ ∃⃗x.φ を満たす代入 δ を考える. こ

義 よ り，rmv (s[∃⃗x.φ]) = s[φ]. ま た ，ext(s[φ]) =のとき解釈の定義より，ある a1 , . . . , an ∈ |M| が存

s[∃⃗y .φ]. こ こ で ，{⃗x} = {⃗y } と な れ ば 良 い.

補在して，δ ⊨ρ φ. ただし，ρ = {xi 7→ ai | 1 ≤ i ≤ n}.

題 3.4 より，BV(∃⃗x.φ) = Var(φ) \ Var(s). また，

ここで，|M|= Val に注意すると，δ ′ ⊨ φ を満た{⃗x} = BV(∃⃗x.φ) より，{⃗x} = Var(φ) \ Var(s). 変

すような代入 δ ′ を δ ′ = δ ◦ {x1 7→ a1 , . . . , xn 7→換の定義より，{⃗y } = Var(φ) \ Var(s). したがって，

an } のように取れる. ここで，{x1 , . . . , xn } = {⃗x}.

ext(rmv (s[∃⃗x.φ])) = s[∃⃗x.φ].

BV(∃⃗x.φ) ∩ Var(s) = ∅, BV(∃⃗x.φ) = {⃗x} よ り，sδ = sδ ′ . したがって，s[φ] ∼ ext(s[φ]) が示せた.

3. 2 存在制約付き項の等価関係
代入 γ が存在量化付き論理制約 ∃⃗x.φ を respect す
るとは，以下の 2 つの条件を満たすときである.

1. 任意の変数 x ∈ FV(∃⃗x.φ) について，γ(x) ∈ Val
2. M ⊨ (∃⃗x.φ)γ
なお，⃗
x = ϵ のとき，代入 γ が論理制約 φ を respect
することの従来の定義と同値になることに注意する.
このとき，γ ⊨ ∃⃗x.φ と記す．
定義 3.9 (存在制約付き項における等価関係). 存
在制約付き項 s[∃⃗x.φ], t[∃⃗y .ψ] が等価関係にあるとは，任意の γ ⊨ ∃⃗x.φ を満たす代入 γ について，ある δ ⊨ ∃⃗y .ψ を満たす代入 δ が存在し sγ = tδ を満たし，またその逆も同様に言えるときをいう. このとき

s[∃⃗x.φ] ∼ t[∃⃗y .ψ] と記す.
また，制約付き項と存在制約付き項の間の等価関係も同様に定義する.
例 3.10 は存在制約付き項における等価関係の例である.

s[∃⃗x.φ] ∼ rmv (s[∃⃗x.φ]) に つ い て も 同 様 に 示 せる.
ここで等価関係 ∼ を分解し，一方向のみの条件を考える.
定義 3.12 (制約を弱める関係). 制約付き項 s[φ], t[ψ]について，γ ⊨ φ を満たす任意の代入 γ について，δ ⊨ ψ を満たす代入 δ が存在し sγ = tδ となるとき，
s[φ] ⊂ t[ψ] と表記する. 存在制約付き項についても∼同様に定義し，制約付き項と存在制約付き項の間でも同様に定義する.
直観的には ⊂ は制約を弱める関係になっている.
∼
例 3.13. 存在制約付き項 g(x)[x > 0], g(y)[∃x.x >0 ∧ y = y] は以下のような関係にある.
g(x)[x > 0] ⊂ g(y)[∃x.x > 0 ∧ y = y]∼
補題 3.14. ⊂ は擬順序関係である.
∼(証明). 定義より自明.
補題 3.15. 以下の関係が成立する．

⊃∩⊂=∼
∼ ∼

(証明). 制約付き項 s[φ], t[ψ] について，s[φ] ⊂ t[ψ]∼かつ t[ψ] ⊂ s[φ] が成立することを仮定する. 定義よ∼り，γ ⊨ φ を満たすような代入 γ に対して，δ ⊨ ψ をられる．

満たすような代入 δ が存在し sγ = tδ を満たす，か

以下のように書き換えることもできる．

つ，δ ⊨ ψ を満たすような代入 δ に対して，γ ⊨ φ を

f (x)[x ≥ 0] →rule g(x)[x ≥ 0]
また，t := x + 1 でも式 (1) は成立する．したがって，

f (x)[x ≥ 0]満たすような代入 γ が存在し tδ = sγ を満たす. これは制約付き項における等価関係の定義と同じなので，

s[φ] ∼ t[ψ].

∼f (x)[x ≥ 0 ∧ y = x + 1]

→ruleg(y)[x ≥ 0 ∧ y = x + 1]

同様に，y = x + k (k ≥ 0) など，無限に取り得る．
一方で，存在制約付き項 f (x)[x ≥ 0] を書き換えたいとすると，以下のように機械的に書き換えることが3. 3 存在制約付き項の書き換えできる．

定義 3.16 (存在制約付き項における Rule 書き換え).

f (x)[x ≥ 0] →rule g(y ′ )[∃x.x ≥ 0 ∧ x ≤ y ′ ]存在制約付き項 s[∃⃗x.φ] がある規則 ρ : l → r[π] ∈ R

補題 3.19. 存在制約付き項 s[∃⃗x.φ] について，あるを 用 い て t[∃⃗y .ψ] へ 書 き 換 え ら れ る と は ，あ る 文

規則 ρ : l → r[π] を用いて，s[∃⃗x.φ] →rule t[∃⃗y .ψ] と

脈 C と 代 入 γ が 存 在 し ，s = C [lγ], t = C [rγ]書き換えられるならば，t[∃⃗y .ψ] は存在制約付き項でを 満 た し か つ 以 下 を 満 た す と き で あ る. た だ し 一ある.

般 性 を 失 う こ と な く，π = π1 ∧ π2 , π1 = π ⇂Var(l), Var(ρ) ∩ (Var(s) ∪ Var(φ)) = ∅ を仮定す
る. つまり，π1 は制約 π を CNF で表したとき，変数として l に出現する変数しか含まない節の論理積を(証明). 存在制約付き項 s[∃⃗x.φ] と項 t，存在量化子付き論理制約 ∃⃗y .ψ からなる項 t[∃⃗y .ψ] について，文脈 C と代入 γ を用いて，s = C [lγ], t = C [rγ] と書け, 以下の条件を満たすとする.

表す．

• dom(γ) = Var(l),• x ∈ dom(γ) について，γ(x) ∈ Val ∪ FV(∃⃗x.φ),∧• ψ = φ ∧ y∈EVar(ρ) y = y ∧ π2 γ,

π=

π1 ∧ π2Var(π1 )⊆Var(l)

dom(γ)=

ψ=

Var(l)∧
φ∧y = y ∧ π2 γ

{⃗
y}

=

Var(ψ) \ Var(t)M ⊨ (∃⃗x.φ)

⇒

π1 γ

• {⃗
y } = Var(ψ) \ Var(t),• ∃⃗x.φ が充足可能かつ，M ⊨ (∃⃗x.φ) ⇒ π1 γ.
このとき，s[∃⃗x.φ] →rule t[∃⃗y .ψ] と表記する.

y∈EVar(ρ)

このとき，t[∃⃗y .ψ] が存在制約付き項の条件を満たす

例 3.17.

ことを示す.

f (x′ ) → g(y ′ , z ′ )[x′ ≥ 0 ∧ z ′ > 3]という規則において，f (x)[x > 0] という存在制約付BV(∃⃗y .ψ) = Var(ψ) \ Var(t) より，BV(∃⃗y .ψ) ∩

き項の書き換えを考える. このとき，f (x)[x > 0] はVar(t) = ∅. したがって，FV(∃⃗y .ψ) ⊆ Var(t) を示

以下のように書き換えられる.

せば良い. FV(∃⃗y .ψ) = Var(ψ) \ BV(∃⃗y .ψ) より，

→rule

f (x)[x > 0]FV(∃⃗y .ψ) = Var(ψ) \ (Var(ψ) \ Var(t)). ここで，g(y ′ , z ′ )[∃x.x > 0 ∧ y ′ = y ′ ∧ z ′ > 3]

Var(ψ) \ (Var(ψ) \ Var(t)) = Var(ψ) ∩ Var(t) より，

例 3.18.

よ り，FV(∃⃗y .ψ) = FV(∃⃗y .ψ) ∩ Var(t). し た がっ

f (x′ ) → g(y ′ )[x′ ≤ y ′ ]という規則を用いて，制約付き項 f (x)[x ≥ 0] を書き換えたいとする．このとき，書き換えるためには，M⊨ x≥0⇒x≤tFV(∃⃗y .ψ) = Var(ψ)∩Var(t).BV(∃⃗y .ψ)∩Var(t) = ∅(1)

なる項 t を見つける必要がある．例えば，t := x を取れば，式 (1) は成立するので，以下のように書き換えて，FV(∃⃗y .ψ) ⊆ Var(t). したがって，FV(∃⃗y .ψ) ⊆

Var(t) が示された.
以上より，t[∃⃗y .ψ] は存在制約付き項である.
補 題 3.20. 存 在 制 約 付 き 項 s[∃⃗x.φ], t1 [∃y⃗1 .ψ1 ],t2 [∃y⃗2 .ψ2 ] に つ い て ，s[∃⃗x.φ] →ruleる.

M ⊨ φ ⇒ (π1 ∧ π2 )γ よ り，M ⊨ φ ⇒s[∃⃗x.φ] →rule t2 [∃y⃗2 .ψ2 ] が同じ規則と同じ位置に

π1 γ.

Var(π1 ) ⊆ Var(l) よ り，π1 γ = π1 γ ′ . よっ

置いて書き換えられているならば，変数の名前変えのて ，M ⊨ φ ⇒ π1 γ ′ も 成 立.

もとで t1 [∃y⃗1 .ψ1 ] と t2 [∃y⃗2 .ψ2 ] は同一．

より，Var(lγ ′ ) ⊆ Var(s). したがって，Var(π1 ) ⊆t1 [∃y⃗1 .ψ1 ],(証明). 用いた書き換えを l → r[π1 ∧ π2 ] とする．このとき，書き換え規則は定義 3.16 に従う．このとき，

s = C [lγ], dom(γ) = Var(l) より，γ は一意に定まる．よって，t = C [rγ] より，t も一意に定まる．同Var(l) より，Var(π1 γ ′ ) ⊆ Var(lγ ′ ) ⊆ Var(s). 一
方，(Var(φ) \ Var(s)) ∩ Var(s) = ∅ より，(Var(φ) \Var(s)) ∩ Var(π1 γ ′ ) = ∅. つまり，{⃗x} ∩ Var(π1 γ) =∅. したがって，以下が成立する.
M ⊨ φ ⇒ π1 γ ′様に ψ1 と ψ2 も一意に定まり，y⃗1 と y⃗2 も同一である．

EE 変換を用いた，従来の制約付き項の Rule 書き

lγ ′ は s の 部 分 項⇒

M ⊨ ∀⃗x.(φ ⇒ π1 γ ′ )⇒M ⊨ ∃⃗x.φ ⇒ π1 γ ′以上より，s[∃⃗x.φ] →rule t[∃⃗y .ψ] のように書き換える

換えと存在制約付き項の Rule 書き換えの関係を以下ことができた.

に示す．
補題 3.21. 制約付き項 s[φ], t[φ] について，s[φ] →rule

次に，書き換えられた項 u[∃⃗y .ψ] について，t[φ] ⊂∼u[∃⃗y .ψ] が成立するかを考える. つまり，δ ⊨ φ を

t[φ] のように書き換えができるとき，ある存在制約付満たす任意の δ について，ある代入 δ ′ が存在して，き項 u[∃⃗y .ψ] が存在し，以下の 2 つが成立する.

δ ′ ⊨ ∃⃗y .ψ かつ，tδ = uδ ′ が成立するかを考える.

1. 同じ規則と同じ位置において，ext(s[φ]) →ruleδ ⊨ φ とする．このとき，以下の 2 つが成立する.

u[∃⃗y .ψ] のように書き換えられる.

∀x ∈ Var(φ).δ(x) ∈ Val

2. t[φ] ⊂ u[∃⃗y .ψ].
∼M ⊨ φδ

(証明). s[φ] →rule t[φ] を仮定する. このとき，規則
ρ : l → r[π1 ∧ π2 ] を用いて，s = C [lγ], t = C [rγ]とできると仮定する. ただし，π1 ⇂ Var(l), dom(γ) =こ こ で ，δ′= δ ◦ γ を と る と ，t = uγ よ り，tδ = (uγ)δ = u(δ ◦ γ) = uδ ′ . こ こ で ，ψ =∧φ ∧ y∈EVar(ρ) y = y ∧ π2 γ ′ に 注 意 し て ，ψ のVal ∪ Var(φ), M ⊨ φ ⇒ (π1 ∧ π2 )γ を満たす. また，それぞれの構成要素について考える. まず，δ ′ ⊨∧y .π2 γ ′ に∃⃗y . y∈EVar(ρ) y = y は自明. 次に δ ′ ⊨ ∃⃗一般性を失うことなく，Var(ρ) ∩ Var(s) ∪ (Var(φ)) =ついて考える．x ∈ Var(π2 ) とする．このとき，x ∈∅.

Var(l) なら Var(π2 γ) ⊆ Var(s), dom(γ)∩Var(s) = ∅Var(l)∪Var(r)∪Var(π1 ∧π2 ), ∀x ∈ LVar(ρ).γ(x) ∈最初に，ext(s[φ]) = s[∃⃗x.φ] が同じ規則を用いて 書 き 換 え ら れ る か ど う か を 考 え る.

ここで，

γ ′ = {x 7→ γ(x) | x ∈ Var(l)} とする. このとき，
lγ = lγ ′ より，s = C [lγ] = C [lγ ′ ]. ここで，s[∃⃗x.φ]より，γ(γ ′ (x)) = γ ′ (x) = γ(x). また，x ∈/ Var(l) ならば，xγ ′ = x より，γ(γ ′ (x)) = γ(x). したがって，

π2 γ ′ δ ′ は以下のように変形できる.
π2 γ ′ δ ′が以下のように書き換えられることを示す.

s[∃⃗x.φ]=(π2 γ)δ

=C [lγ ][∃⃗x.φ]

ここで，⊨ φ ⇒ (π1 ∧ π2 )γ かつ δ ⊨ φ より，δ ⊨ π2 γ.

→rule

′

C [rγ ][∃⃗y .ψ]

したがって，⊨ (π2 γ)δ. したがって，⊨ (π2 γ ′ )δ ′ . よっ

=

t[∃⃗
y .ψ]

て，δ ′ ⊨ ⃗y .π2 γ ′ .

y∈EVar(ρ)=((π2 γ ′ )γ)δ′ただし，ψ, ⃗y は以下のように定義する.
∧
ψ = φ∧
y = y ∧ π2 γ

{⃗
y}

=

Var(ψ) \ Var(t)まず，M ⊨ ∃⃗x.φ ⇒ π1 γ ′ が成立するかを考え最後に，Var(ρ) ∩ Var(φ) = ∅, dom(γ) = Var(ρ)
より，φγ = φ. よって，φδ ′ は以下のように変形できる.

在しない．したがって，どのような t を考えても，

φδ

′

=

(φγ)δ

M ⊭ x ≥ 0 ⇒ t × t = x．したがって，制約付き項=φδ

f (x)[x ≥ 0] は正規形である．
補題 3.24. 存在制約付き項 s[∃⃗x.φ], t[∃⃗y .ψ] について，′′

M ⊨ φδ よ り，M ⊨ φδ . 以 上 よ り，δ ⊨ φ ∧
∧
′
′
y .ψ.
y∈EVar(ρ) y = y ∧ π2 γ . したがって，δ ⊨ ∃⃗′′以上より，tδ = uδ かつ δ ⊨ ∃⃗y .ψ が言えたので，

t[φ] ⊂ u[∃⃗y .ψ] が言えた.
∼s[∃⃗x.φ] →rule t[∃⃗y .ψ] のように書き換えができるとき，同じ規則と同じ位置において，rmv (s[∃⃗x.φ]) →ruleu[φ] のように書き換えられるならば，u[φ] ⊂ t[∃⃗y .ψ].
∼(証明). s[∃⃗x.φ] →rule t[∃⃗y .ψ] を仮定する. 補題 3.21
より，ある t1 [∃y⃗1 .φ1 ] を用いて以下が言える．

ext(rmv (s[∃⃗x.φ])) →rule t1 [∃y⃗1 .φ1 ]例 3.22.

f (x′ ) → g(y ′ , z ′ )[x′ ≥ 0 ∧ z ′ > 3]という規則を用いて，f (x)[x > 0] という制約付き項

u[φ] ⊂ t1 [∃y⃗1 .φ1 ]∼補題 3.8 より，s[∃⃗x.φ] = ext(rmv (s[∃⃗x.φ])). また，の書き換えは以下のようにできる. ただし，これは書

補題 3.20 より，t1 [∃y⃗1 .ψ1 ] = t[∃⃗y .ψ].

き換えられるうちの一例である.

f (x)[x > 0] →rule g(x, 4)[x > 0]
このとき，ext(f (x)[x > 0]) = f (x)[x > 0] の書き換えも考えると，以下のように書き換えられる.

f (x)[x > 0]
→ruleg(y ′ , z ′ )[∃x.x > 0 ∧ y ′ = y ′ ∧ z ′ > 3]

定義 3.25 (存在制約付き項における Calc 書き換え). 存在制約付き項 s[∃⃗x.φ] の Calc 書き換えを考える. 関数記号 f ∈ Ftheory \ Val と，s1 , . . . , sn ∈Val ∪ FV(∃⃗x.φ) について，s|p = f (s1 , . . . , sn ) と書けるとき，s[∃⃗x.φ] は以下のように書き換えできる.

s[∃⃗x.φ]

このとき，書き換えられた項は以下のような関係に=ある.

g(x, 4)[x > 0] ⊂ g(y ′ , z ′ )[∃x.x > 0∧y ′ = y ′ ∧z ′ > 3]∼
ER 変換を用いて，存在制約付き項の Rule 書き換
えと従来の制約付き項の Rule 書き換えの関係性を補
題 3.21 と同じような形の補題で示したい．しかし，存在制約付き項は書き換えられる一方で，従来の制約→calc
f (s1 , . . . , sn ).

例 3.26. このとき，f (4 + z, x)[∃y.x > y ∧ z = 3] という存在制約付き項を考える. このとき, 以下のように Calc 書き換えできる.

f (4 + z, x)[∃y.x > y ∧ z = 3]→calc

例 3.23.

f (x′ ) → g(y ′ )[y ′ × y ′ = x′ ]という規則を用いて，存在制約付き項 f (x)[x ≥ 0]s[x]p [∃⃗y .ψ]ただし，{⃗y } = Var(ψ) \ (Var(s[x]p )), ψ = φ ∧ x =付き項は書き換えられない例が存在する．以下にその例を示す．

s[f (s1 , . . . , sn )]p [∃⃗x.φ]

f (w, x)[∃y, z.x > y ∧ z = 3 ∧ w = 4 + z]

補 題 3.27. 存 在 制 約 付 き 項 s[∃⃗x.φ] に つ い て ，s[∃⃗x.φ] →calc t[∃⃗y .ψ] と 書 き 換 え ら れ る な ら ば ，t[∃⃗y .ψ] は存在制約付き項である.

という存在制約付き項の書き換えは以下のようにで(証明). あ る 位 置 p，関 数 記 号 f

きる．

∈ Ftheory \f (x)[x ≥ 0] →rule g(y ′ )[∃x.y ′ × y ′ = x ∧ x ≥ 0]

Val, s1 , . . . , sn ∈ Val ∪ FV(∃⃗x.φ) について，s|p =

一方，制約付き項 f (x)[x ≥ 0] を以下のように書き換

f (s1 , . . . , sn ) と仮定する. このとき，s[∃⃗x.φ] は以下

えたい．

のように書き換えができる.

s[∃⃗x.φ]f (x)[x ≥ 0] →rule g(t)[x ≥ 0]
こ の と き ，M ⊨ x ≥ 0 ⇒ t × t = x を満 た す．

=

しかし，x が平方数でない限り，そのような t は存

→calc

s[f (s1 , . . . , sn )]p [∃⃗x.φ]
s[x]p [∃⃗y .ψ]ただし，{⃗y } = Var(ψ) \ (Var(s[x]p )), ψ = (φ ∧ (x =Ftheory \ Val, s1 , . . . , sn ∈ Val ∪ Var(φ), 変数 xf (s1 , . . . , sn ))). t = s[x]p としたとき，t[∃⃗y .ψ] が存を用いて, 以下のように書ける.

在制約付き項となることを示す.

s|p=

f (s1 , . . . , sn )BV(∃⃗y .ψ) = {⃗y } で，{⃗y } = Var(ψ) \ (Var(s[x]p ))

t

=

s[x]p

よ り，BV(∃⃗y .ψ) = Var(ψ) \ Var(t). し た がって ，ψ=φ ∧ (x = f (s1 , . . . , sn ))BV(∃⃗y .ψ) ∩ Var(t) = ∅. 次に FV(∃⃗y .ψ) ⊆ Var(t)ここで，ext(t[ψ]) = t[∃w.ψ],⃗ext(s[φ]) = s[∃⃗x.φ]

を 示 す.FV(∃⃗y .ψ) = Var(ψ) \ BV(∃⃗y .ψ) よ り，とする. 補題 3.5 を用いて，FV(∃⃗x.φ) = Var(φ) ∩FV(∃⃗y .ψ) = Var(ψ) \ (Var(ψ) \ Var(t)). ここで，Var(s)．また，f (s1 , . . . , sn ) ⊴ s より，si ∈ Var(φ)

Var(ψ) \ (Var(ψ) \ Var(t)) = Var(ψ) ∩ Var(t) より，のとき，s ∈ FV(∃⃗x.φ)．よって，定義より以下のよFV(∃⃗y .ψ) = Var(ψ)∩Var(t).BV(∃⃗y .ψ)∩Var(t) = ∅うに書き換えることができる.

よ り，FV(∃⃗y .ψ) = FV(∃⃗y .ψ) ∩ Var(t). し た がっs[∃⃗x.φ]=→calcて，FV(∃⃗y .ψ) ⊆ Var(t). したがって，FV(∃⃗y .ψ) ⊆

Var(t) が示された.

=

したがって，t[∃⃗y .ψ] は存在制約付き項である.
補 題 3.28. 存 在 制 約 付 き 項 s[∃⃗x.φ], t1 [∃y⃗1 .ψ1 ],t2 [∃y⃗2 .ψ2 ] に つ い て ，s[∃⃗x.φ] →calc

t1 [∃y⃗1 .ψ1 ],s[∃⃗x.φ] →calc t2 [∃y⃗2 .ψ2 ] が同じ位置で書き換えられているならば，変数の名前変えのもとで，t1 [∃y⃗1 .ψ1 ]と t2 [∃y⃗2 .ψ2 ] は同一．

(証明). f ∈ Ftheory \ Val と s1 , . . . , sn ∈ Val ∪s[f (s1 , . . . , sn )]p [∃⃗x.φ]
s[x]p [∃⃗z.φ ∧ x = f (s1 , . . . , sn )]t[∃⃗z.ψ]た だ し ，{⃗z } = Var(ψ) \ Var(s[x]p ). ま た ，こ のとき {w}⃗ = BV(∃w.ψ)⃗= Var(ψ) \ Var(t) = {⃗z}.
したがって，ext(t[ψ]) = t[∃⃗z .ψ] が示されたので，

ext(s[φ]) →calc ext(t[ψ]) と書き換えられることが示せた.

(2) s[∃⃗x.φ] →calc t[∃⃗y .ψ] を 仮 定 す る と ，f ∈Ftheory \ Val, s1 , . . . , sn ∈ Val ∪ FV(∃⃗x.φ), 変数 xを用いて以下のように書ける.

Var(φ) を 用 い て，s = s[f (s1 , . . . , sn )]p と 書 け る

s|p=f (s1 , . . . , sn )ことを仮定する．このとき，t = s[x]p で x は存在制

t

=

s[x]p

約付き項に存在しない新しい変数．x として，どん

∃⃗
y .ψ

=

∃⃗
y .φ ∧ (x = f (s1 , . . . , sn ))な変数を取ったとしても，⃗
y は一意に定まる．また，た だ し ，{⃗y } = Var(ψ) \ Var(s[x]p ).

t1 , t2 と ψ1 , ψ2 も変数の名前変えのもとで一意に定

rmv (s[∃⃗x.φ]) = s[φ] についても s1 , . . . , sn ∈ Val ∪まる．

Var(φ) より，同じように書き換えることができる. つ

存在制約付き項の Calc 書き換えについて，以下の補題が言える. これは制約付き項での Calc 書き換えと存在制約付き項での Calc 書き換えが相互に変換可

ここで，

まり

s[φ]

=
→calc

s[f (s1 , . . . , sn )][φ]C [x][φ ∧ x = f (s1 , . . . , sn )]能であることを示している.

こ の と き ，rmv (t[∃⃗y .ψ]) = t[ψ], t = C [x], ψ =補 題 3.29. (1) 制 約 付 き 項 s[φ], t[ψ] に つ い て ，φ ∧ x = f (s1 , . . . , sn ) より，s[φ] →calc t[ψ]. したがっs[φ] →calc t[ψ] と書き換えられるとき，ext(s[φ]) →calcて，rmv (s[∃⃗x.φ]) →calc rmv (t[∃⃗y .ψ]) を示せた.

ext(t[ψ]) のように書き換えができる.
(2) 存 在 制 約 付 き 項 s[∃⃗x.φ], t[∃⃗y .ψ] に つ い て ，

4 存在制約付き項における書き換えと性質s[∃⃗x.φ] →calc t[∃⃗y .ψ] と 書 き 換 え ら れ る と き ，

この節では，存在制約付き項における書き換えを定rmv (s[∃⃗x.φ]) →calc rmv (t[∃⃗y .ψ]) のように書き換え義し，その書き換えと制約付き項の書き換えの関係をができる.

示す．また，存在制約付き項の書き換えによって同じ(証明). (1) s[φ] →calc t[ψ] を 仮 定 す る と ，f ∈規則，同じ位置で書き換えられた項のバリエーションについても考える．

約を最も広く取り，もっとも一般的な制約のみで書き

定義 4.1 (存在制約付き項の書き換え). 存在制約

換えを行う．このため，制約を弱めることに伴う非決付き項上の書き換えについて →R = →rule ∪ →calc ,定性を排除することができるため，書き換えがより∼−→R = ∼ ◦ →R ◦ ∼ のように定義する．

よい性質を持つことが期待できる．また，擬順序関係

定理 4.2. 制約付き項 s[φ], t[φ] について，ある位置に基づいてもとの書き換えを構成することができる．

p で s[φ] →R t[ψ] のように書き換えができるとき，今後の課題としては，存在制約付き項における等価関

ある u, ψ, ⃗y について，以下の 2 つが成立する.

係と書き換え関係の可換性について明らかにするこ

1. 同じ規則を用いて，同じ位置を ext(s[φ]) →Rとである．存在制約付き項に対して，書き換えを行っu[∃⃗y .ψ] のように書き換えることができる．

てから等価変換を行ったものと，等価変換を行ってか

2. ext(t[φ]) ⊂ u[∃⃗x.ψ].
∼(証明). 補題 3.21，補題 3.29 より成立する．

ら書き換え関係をおこなったものが存在制約付き項上の等価関係のもとで同一になるかは定かではない．
また，存在制約付き項の等価関係と書き換え関係の可定理 4.3. 存在制約付き項 s[∃⃗x.φ], t[∃⃗y .ψ] につい換性を示すことで，従来の制約付き項ではどのようなて，ある位置 p で s[∃⃗x.φ] →R t[∃⃗y .ψ] のように書ことが言えるのかも不明である．この点を解明するこき換えができるとき，同じ規則を用いて同じ位置をとが今後の研究の方向である．

rmv (s[∃⃗x.φ]) →R u[φ] のように書き換えられるならば，u[φ] ⊂ rmv (t[∃⃗y .ψ]).
∼

謝辞 本研究は一部日本学術振興会科学研究費

24K14817 の補助を受けて行われた.

(証明). 補題 3.24，補題 3.29 より成立する．
参 考 文 献また，存在制約付き項の書き換えについて，以下の定理が成立する．
定理 4.4. 存在制約付き項 s[∃⃗x.φ] について，同じ位置，同じ規則で項を書き換えるとき，書き換えられる
結果は変数の名前変えのもとで一意に定まる．

(証明). 補題 3.20，補題 3.28 より成立する．

5 おわりに
本稿では存在制約付き項の枠組みを提案し，その書
き換えも提示した．特に，等価関係から自然に導かれる擬順序関係を用いて，存在制約付き項上の書き換えと従来の制約付き項上の書き換えの間の関係性を示した．我々のアプローチでは，書き換えを行う際に制[1] Fuhs, C., Kop, C., and Nishida, N.: Verifying Procedural Programs via Constrained Rewriting Induction, ACM Trans. Comput. Logic, Vol. 18,
No. 2(2017).
[2] Kop, C. and Nishida, N.: Term Rewriting with
Logical Constraints, In Proc. of 9th FroCoS, LNAI,
Vol. 8152, Springer, 2013, pp. 343–358.
[3] Schöpf, J. and Middeldorp, A.: Conﬂuence Criteria for Logically Constrained Rewrite Systems, In
Proc. of 29th CADE, LNCS, Vol. 14132, Springer,
2023, pp. 474–490.
[4] Schöpf, J., Mitterwallner, F., and Middeldorp, A.:Conﬂuence of Logically Constrained Rewrite Systems Revisited, In Proc. of 12th IJCAR, LNCS,
Vol. 14740, Springer, 2024, pp. 298–316.
[5] Winkler, S. and Middeldorp, A.: Completion for
Logically Constrained Rewriting, In Proc. of 3rd
FSCD, LIPIcs, Vol. 108, 2018, pp. 30:1–30:18.