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

名目書き換えにおける強可換性を用いた合流性証明 ∗菊池 健太郎

本稿では，名目書き換え (nominal rewriting) に関する基本事項と強可換性を用いた合流性の証明手法について説明する．名目書き換えは，Gabbay-Pitts による名目技法に基づいて変数束縛を扱えるように第一階項書き換えを拡張した体系であり，アルファ同値性を構文の中で明示的に扱うなどの特徴を持つ．最近導入されたアトム変数を用いる
書き換え規則によって定義される名目書き換えシステムは，書き換えの対象が基底名目項に制限されるものの，これまでのシステムよりも単純であり，理解が比較的容易である．本稿では，それらの名目書き換えシステムにおける基本的な性質および合流性が成立するための条件について議論する．

近 [8] で導入されたアトム変数を持つ体系の部分体系

1 はじめにである．この体系では，書き換え対象と書き換え規則

名目書き換え (nominal rewriting) [4] は，Gabbay-で異なる言語を用いる．書き換え対象は変数を含まPitts による名目技法 [5] [10] に基づいて変数束縛を扱ない基底名目項であり，書き換え規則は変数を含む項えるように第一階項書き換えを拡張した体系である．

(項式とよぶ) から構成される．

名目書き換えでは，束縛される可能性のある変数はアトムとよばれ，アトムに関するアルファ同値性が構文2. 1 準備の中で明示的に扱われるという特徴を持つ．

議論の対象を定めるために，関数記号の集合 Σ を名目書き換えにおける合流性の成立条件について考える．関数記号は f, g 等で表される．また，変数のは， [2] [4] [7] [11] [12] で議論されてきている．本稿で可算無限集合 X ，アトムの可算無限集合 A，アトムは，最近 [8] で導入されたアトム変数を用いる書き換

変数の可算無限集合 XA を用意する．変数は X, Y, Z

え規則によって定義される名目書き換えシステムを取等で，アトムは a, b, c 等で，アトム変数は A, B, C 等り扱う．著者らは，この体系における直交システムので表す．Σ, X , A, XA は互いに共通の要素を持たない合流性を [6] で示しているが，本稿では，強可換性をものとする．また，X , A, XA の要素を表すメタ変数用いた合流性の証明手法について説明する．

(X, Y, a, b, A, B 等) として異なる記号を用いたときは，異なる要素を表すものとする．

2 名目書き換え
本節では，名目書き換えの基本事項を説明する．ここで扱うのは，元々の名目書き換え [4] ではなく，最∗ Proving confluence by strong commutation in nomi-nal rewriting. — This is an unrefereed paper. Copyrights belong to the Author.
Kentaro Kikuchi, 東 北 大 学 電 気 通 信 研 究 所, Research Institute of Electrical Communication, Tohoku University.

2 項関係 ▷◁ の反射閉包は ▷◁= で，反射推移閉包は▷◁∗ で表す．▷◁ が → を用いて書かれるとき，その逆▷◁−1 は ← を用いて書かれる．
2. 2 基底名目項
基底名目項の集合 NLa は，文法t ∈ NLa ::= a | [a]t | f t | ⟨t1 , . . . , tn ⟩で生成される．以下では，基底名目項を単に項という．

::= の右側の項はそれぞれ，アトム，抽象，関数適用，⊢NLa a#t⊢NLa a#f t⊢NLa a#bタプルとよばれる．関数適用は抽象よりも結合が強い⊢NLa a#t1 · · · ⊢NLa a#tn
⊢NLa a#⟨t1 , . . . , tn ⟩ものとする．f ⟨ ⟩ を単に f と略し，定数とよぶ．抽象 [a]t は，t の中で a が束縛されることを意図してい⊢NLa a#t⊢NLa a#[b]tる．項 t に現れる自由アトムの集合 FA(t) は，以下で⊢NLa a#[a]t定義される．FA(a) = {a}; FA([a]t) = FA(t) \ {a};∪i FA(ti ).

FA(f t) = FA(t); FA(⟨t1 , . . . , tn ⟩) =図1

NLa 上の非出現制約の定義

例 1. ラ ム ダ 計 算 の 項 を 表 現 す る た め に ，関 数
記号の集合として Σλ = {lam, app} を考える．項

app⟨lam⟨[a]lam⟨[b]app⟨b, a⟩⟩⟩, b⟩ は，通常の記法での⊢NLa a ≈α a

⊢NLa t1 ≈α s1 · · · ⊢NLa tn ≈α sn⊢NLa ⟨t1 , . . . , tn ⟩ ≈α ⟨s1 , . . . , sn ⟩ラ ム ダ 項 (λa.λb.ba)b を 表 す．こ の 項 t に 対 し て ，FA(t) = {b} となる．
2 つのアトム a と b を交換する操作を互換といい，(a b) で表す．置換 π は，定義域 dom(π) = {a ∈⊢NLa t ≈α s
⊢NLa [a]t ≈α [a]sA | π(a) ̸= a} が有限集合となるような A 上の全図2単射である．置換は，互換の有限列によって表すことができる．その場合，列の右から順に互換をアトムに適用するものとする．例えば，置換 (b c)(a b)に対して，((b c)(a b))(a) = c，((b c)(a b))(b) = a，((b c)(a b))(c) = b となる．アトムに対する関数である置換は，以下の定義により項に対する操作へ拡張される．π·a = π(a); π·([a]t) = [π·a](π·t);

π·(f t) = f π·t; π·⟨t1 , . . . , tn ⟩ = ⟨π·t1 , . . . , π·tn ⟩.
例 2. 例 1 の項 t に対して，(a b)·t =app⟨lam⟨[b]lam⟨[a]app⟨a, b⟩⟩⟩, a⟩ となる．
項の位置は正整数の有限列で表される．空列を εで表す．項 t の位置集合 Pos(t) は，以下のように定義される．Pos(a) = {ε}; Pos([a]t) = Pos(f t) =∪{1p | p ∈ Pos(t)} ∪ {ε}; Pos(⟨t1 , . . . , tn ⟩) = i {ip |p ∈ Pos(ti )} ∪ {ε}. 位置 p ∈ Pos(t) の部分項は，t|pで表される．
文脈は特別な定数 □ を含む項である．文脈 C の位置 pi (i ∈ {1, . . . , n}) に現れる □ を項 ti でそれぞれ置き換えて得られる項を C[t1 , . . . , tn ]p1 ,...,pn あるい
は単に C[t1 , . . . , tn ] で表す．
アトム a と項 t の組 a#t を非出現制約とよぶ．関係 ⊢NLa a#t を，図 1 の推論規則により帰納的に定義する．この関係は a ∈/ FA(t) と同値である．

NLa 上の関係 ⊢NLa t ≈α s を，図 2 の推論規則に⊢NLa t ≈α s
⊢NLa f t ≈α f s⊢NLa (a b)·t ≈α s ⊢NLa b#t⊢NLa [a]t ≈α [b]sNLa 上のアルファ同値性の定義

より帰納的に定義する．この関係は合同関係であり[4]，通常の意味でのアルファ同値性 (束縛アトムの名前換えにより到達できる関係) と一致する [5]．
非出現制約，アルファ同値性，置換に関して，以下の性質が成り立つ [4] [13]．
命題 3.

1. ⊢NLa a#t であるとき，かつそのときに限り⊢NLa π·a#π·t.
2. ⊢NLa t ≈α s であるとき，かつそのときに限り⊢NLa π·t ≈α π·s.
3. ⊢NLa a#t かつ ⊢NLa t ≈α s ならば ⊢NLa a#s.

2. 3 名目項式
名目項式の集合 NLAX は，文法e ∈ NLAX ::= A | X | [A]e | f e | ⟨e1 , . . . , en ⟩で生成される．以下では，名目項式を単に項式という．項式 e に現れる変数の集合を VarX (e)，アトム変数の集合を VarXA(e)，それらの和を VarX,XA(e) で表す．項式 e が線形であるとは，各変数 X ∈ VarX (e)が e に一度だけ現れることとする．
項式 e の位置集合 Pos(e) は，Pos(A) = Pos(X) =⊢sub⟨[A]app⟨X, Y ⟩, Z⟩→app⟨sub⟨[A]X, Z⟩, sub⟨[A]Y, Z⟩⟩(subapp )⊢sub⟨[A]A, X⟩→

X(subvar )A#B⊢sub⟨[A]B, X⟩→

B(subvarϵ )A#B, B#Y⊢

sub⟨[A]lam⟨[B]X⟩, Y ⟩→lam⟨[B]sub⟨[A]X, Y ⟩⟩(sublam )図3

NRSAX Rsub⊢(XY )⟨A := Z⟩→(X⟨A := Z⟩)(Y ⟨A := Z⟩)(subapp )⊢A⟨A := X⟩→X(subvar )A#B⊢

B⟨A := X⟩→B(subvarϵ )A#B, B#Y⊢(λB.X)⟨A := Y ⟩→λB.(X⟨A := Y ⟩)(sublam )図4

NRSAX Rsub (通常の記法){ε} である他は，項の場合と同様に定義される．位が線形であるときをいう．

置 p ∈ Pos(e) の部分項式は e|p で表される．位置

定義 5. 名目書き換えシステムとは，書き換え規則のp ∈ Pos(e) が変数位置であるとは，e|p が変数である有限集合である．以下では，名目書き換えシステムをときをいい，そうでない場合は，非変数位置であると略して NRSAX で表す．NRSAX R が左線形であるという．

は，すべての書き換え規則 R ∈ R が左線形であると代入 σ は，変数に項を，アトム変数にアトムを割り当きをいう．

てる写像で，定義域 dom(σ) が有限集合となるもので

例 6. 例 1 の集合 Σλ を関数記号 sub によって拡張ある．項式 e と代入 σ に対して VarX,XA(e) ⊆ dom(σ)

する．項 sub⟨[a]t, s⟩ は明示的代入 t⟨a := s⟩ を表す．となるとき，e に σ を適用して得られる項を eσ でこのとき，ベータ簡約を実現する NRSAX は以下の書表し，e の基底具体化という．このとき，自由アトム

き換え規則 (Beta)の捕獲を考慮することなく，e に現れる変数 X を項⊢app⟨lam⟨[A]X⟩, Y ⟩→sub⟨[A]X, Y ⟩σ(X) で，アトム変数 A をアトム σ(A) でそれぞれ置と，代入を実行する NRSAX Rsub (図 3) によって定き換えることに注意する．

義される．Rsub は，通常の記法で表すと図 4 のよう

アトム変数 A と項式 e の組 A#e を非出現制約式とよび，非出現制約式の有限集合を非出現文脈とよぶ．になる．
次に，NRSAX による書き換えを定義する．
定義 7. R = ∇ ⊢ l → r を書き換え規則とする．項

2. 4 名目書き換えシステム

s から項 t への書き換えを表す関係 s →⟨R,p,σ⟩ t が成次に，名目書き換え規則と名目書き換えシステムを立するのは，以下の条件を満たすときとする．

定義する．

1. すべての非出現制約式 A#e ∈ ∇ に対して，

定義 4. 名目書き換え規則とは，非出現文脈 ∇ と項

⊢NLa Aσ#eσ.

式 l, r の 3 つ組で，以下の条件を満たすもののことで

2. ⊢NLa s|p ≈α lσ.

ある．

3. t|p = rσ.
p

1. VarX,XA(∇) ∪ VarX,XA(r) ⊆ VarX,XA(l).

s →⟨R,p,σ⟩ t となる σ が存在するとき，s →R t と書

2. l は変数またはアトム変数でない．

く．また，s →⟨R,p,σ⟩ t となる p と σ が存在すると以下では，名目書き換え規則を ∇ ⊢ l → r で表す．まき，s →R t と書く．NRSAX R に対し，s →R t となた，名目書き換え規則のことを単に書き換え規則といる R ∈ R が存在するとき，s →R t と書く．

う．書き換え規則 ∇ ⊢ l → r が左線形であるとは，l例 8. 例 6 の書き換え規則 (Beta) を用いることで，

以下のように (λa.λb.ba)b を表す項は (λb.ba)⟨a := b⟩を表す項に書き換えられる．

app⟨lam⟨[a]lam⟨[b]app⟨b, a⟩⟩⟩, b⟩→⟨Beta,ε,σ⟩ sub⟨[a]lam⟨[b]app⟨b, a⟩⟩, b⟩
ここで，σ は代入 [A := a, X := lam⟨[b]app⟨b, a⟩⟩,Y := b] である．さらに Rsub の規則を用いて書き換えを進めることにより，正規形 lam⟨[c]app⟨c, b⟩⟩ に至る．ここでは，自由アトムの捕獲がどのように回避されるかを見るために，規則 (sublam ) による最初の書き換えについて詳しく説明する．

s = sub⟨[a]lam⟨[b]app⟨b, a⟩⟩, b⟩ と お く．(sublam )s1 −→q R t1 · · · sn −→q R tn(C)G[s1 , . . . , sn ] −→q R G[t1 , . . . , tn ]ここで，n (≥ 0) は文法的文脈 G の形に依存する自然数である．
並列簡約に関して，以下の性質が成り立つ．
補題 11.

1. s −→
q R s.

2. s −→
q R t ならば C[s] −→q R C[t].
3. s →R t ならば s −→q R t.
4. s −→
q R t ならば s →∗R t.
証明.

1. s の構造に関する帰納法による．

2. 文脈 C に関する帰納法による．

は非出現文脈 ∇ = {A#B, B#Y } を持つので，位置

3. 2 と推論規則 (B) による．

p = ε で s に (sublam ) を適用するためには，

4. s −→
q R t の導出に関する帰納法による．

(a) ⊢NLa Aσ#Bσ(b) ⊢NLa Bσ#Y σ

3 強可換性を用いた合流性証明(c) ⊢NLa s ≈α (sub⟨[A]lam⟨[B]X⟩, Y ⟩)σ

本節では，左線形な NRSAX に対する強可換性をを 満 た す 代 入 σ を 見 つ け る 必 要 が あ る ．こ こ で ，用いた合流性証明法を説明する．名目書き換えにおσ(B) = b となる σ をとることはできない．なぜなら，いて合流性を議論するためには，いくつかの定義と(c) とアルファ同値性の定義 (図 2) により Y σ = b でな

NRSAX に関する条件が必要になる．

ければならず，(b) と矛盾するからである．したがって，
例えば，σ = [A := a, B := c, X := app⟨c, a⟩, Y := b]

3. 1 強可換性による合流性証明法

をとり，書き換えの結果として (lam⟨[B]sub⟨[A]X,本小節では，強可換性による合流性証明法を概観す

Y ⟩⟩)σ = lam⟨[c]sub⟨[a]app⟨c, a⟩, b⟩⟩ を得る．
[8] で指摘されているように，書き換えについて以下の性質が成り立つ．

るため，第一階項 (抽象を含まない項) に対する書き換えシステム (TRSAX で表す) を考える．この手法の基本的な戦略は，TRSAX のどの 2 つの規則による補題 9. R を書き換え規則とする．項 s, t に対して書き換えも可換になることを示すことである．まず，s →R t が成り立つならば，任意の置換 π に対して可換性に関する定義と補題を述べる ( [3] の pp. 31–33

π·s →R π·t が成り立つ．

を参照)．
定義 12. R1 , R2 を書き換え規則とする．

2. 5 並列簡約
次節で左線形 NRSAX の合流性について議論するが，そこで重要となる (分離) 並列簡約の概念を定義する．
定義 10. 文法的文脈は，以下の文法で定義される文脈である．

G ::= a | [a]□ | f □ | ⟨□1 , . . . , □n ⟩書き換え規則 R に対し，並列簡約 −→q R を以下の推論規則によって帰納的に定義する．
εs →R t(B)s −→q Rt

1. →R1 と →R2 が可換であるとは，s →∗R1 s1 かつ s →∗R2 s2 ならば，ある t が存在して s1 →∗R2 tかつ s2 →∗R1 t が成り立つことをいう．

2. →R1 が −→q R2 と強可換であるとは，s →R1 s1
か つ s −→
q R2 s2 な ら ば ，あ る t が 存 在 し て

s1 −→q R2 t か つ s2 →∗R1 t が 成 り 立 つ こ と をいう．

q−s −−−−→ s2R2

R
∗yR1
y 1q−
s1 −−−−→ tR2

補題 13. →R1 が −→q R2 と強可換であるならば，→R1に書き換えられるかが問題となる．そこで，抽象書きと →R2 は可換である．

換えで用いられる [9] ような，同値関係 ≈α を法とし

定義 14. TRSAX R が合流性を持つとは，s →∗R s1た性質について議論を行う．

かつ s →∗R s2 ならば，ある t が存在して s1 →∗R t か

以下では，⊢NLa t ≈α s を単に t ≈α s と書く．まつ s2 →∗R t が成り立つことをいう．

た，◦ は 2 項関係の合成を表す．

補題 15. R を TRSAX とする．すべての Ri , Rj ∈ R

定義 19. R を NRSAX とする．

に対して →Ri と →Rj が可換であるならば，R は合1. 項 s と t が ≈α を法として交差する (s ↓≈α t と記す) とは，s (→∗R ◦ ≈α ◦ ←∗R ) t が成り立つこ流性を持つ．
補題 13 と補題 15 より，TRSAX R が合流性を持とをいう．

つことを示すためには，R の書き換え規則の任意の2. R が ≈α を法とした合流性を持つとは，任意の組み合わせ Ri , Rj ∈ R (Ri = Rj の場合を含む) に

項 s, t に対して，s (←∗R ◦ →∗R ) t ならば s ↓≈α tついて，→Ri が −→q Rj と強可換である，あるいは，が成り立つことをいう．

→Rj が −→q Ri と強可換であることを示せばよい．
以下では，→R1 が −→q R2 と強可換になるための十3. R が ≈α を 法 と し た チャー チ・ロッサ ー 性(CR ≈α 性 と記す) を持つとは，任意の項 s, t に分条件を与える．

対して，s (←R ∪ →R ∪ ≈α )∗ t ならば s ↓≈α t

定義 16. R1 と R2 (= ∇2 ⊢ l2 → r2 ) を左線形なが成り立つことをいう．

書き換え規則とする．このとき，条件 sc1 (R1 , R2 )，sc2 (R1 , R2 ) を以下のように定義する．

として可換であるとは，任意の項 s, t に対して，– sc1 (R1 , R2 ) ⇐⇒ s →R1 s′ かつ s −→q R2 t が規defε

則 (C) を最後に適用して導かれるならば，ある t′′

4. R′ を NRSAX とする．→R と →R′ が ≈α を法′が存在して s −→q R2 t かつ t →∗R1 t′ ．
pdef
ε
– sc2 (R1 , R2 ) ⇐⇒ s →R1 s′ かつ s →R2 t，ここ′s (←∗R ◦ →∗R′ ) t ならば s (→∗R′ ◦ ≈α ◦ ←∗R ) tが成り立つことをいう．
一般に，同値関係 ∼ を法としたチャーチ・ロッサー性は，∼ を法とした合流性よりも強い性質であること

で p が l2 の非変数位置であるならば，ある t がが知られている [9]．したがって，本稿では，NRSAX存在して s′ −→q R2 t′ かつ t →∗R1 t′ ．

R が CR ≈α 性 を持つための条件を考える．そのため補題 17. R1 と R2 を左線形な書き換え規則とする．に，NRSAX が左線形であることに加え，書き換え規

このとき，条件 sc1 (R1 , R2 ) と sc2 (R1 , R2 ) が成立す則についても制約を与える．以下の一様性 [4] というるならば，→R1 は −→q R2 と強可換である．

性質は，直観的には，書き換えによって新たな自由ア証明. s −→q R2 t の導出に関する帰納法により，s →R1s′ かつ s−→q R2 t ならば，ある t′ が存在して s′ −→q R2 t′かつ t →∗R1 t′ が成り立つことを示せばよい．
補題 13, 15, 17 より，以下の定理が導かれる．

トムが現れないことを意味する．
定義 20. 書き換え規則 ∇ ⊢ l → r が一様であるとは，以下の条件を満たすときをいう．VarX,XA(l) ⊆dom(σ) かつ，すべての非出現制約式 A#e ∈ ∇ に対して ⊢NLa Aσ#eσ であるとき，⊢NLa a#lσ ならば定理 18. R を左線形な TRSAX とする．すべての⊢NLa a#rσ が成り立つ．NRSAX R が一様であるとRi , Rj ∈ R に対して，sc1 (Ri , Rj ) かつ sc2 (Ri , Rj )，は，すべての書き換え規則 R ∈ R が一様であるとき

あるいは，sc1 (Rj , Ri ) かつ sc2 (Rj , Ri ) が成立するなをいう．

らば，R は合流性を持つ．

一様な書き換え規則に対しては，以下の性質が成り立つ．

3. 2 名目書き換えにおける合流性

補題 21. R を一様な書き換え規則とし，s →R t と名目書き換えにおいて合流性を議論する際には，書する．このとき，任意のアトム a に対し，⊢NLa a#sき換えによって分岐した 2 つの項がアルファ同値な項ならば ⊢NLa a#t が成り立つ．

定義 22. R を書き換え規則とする．→R が ≈α と強両え規則とする．このとき，条件 sc1 (R1 , R2 , ≈α ) と立であるとは，任意の項 s, t に対して，s (≈α ◦ →R ) t

sc2 (R1 , R2 , ≈α ) が成立するならば，→R1 は ≈α を法ならば s (→=R ◦ ≈α ) t が成り立つことをいう．

として −→q R2 と強可換である．

補題 23. R が一様な書き換え規則ならば，→R は≈α と強両立である．

補題 23, 25, 26, 28 より，以下の定理が導かれる．
定理 29. R を左線形かつ一様な NRSAX とする．
すべての Ri , Rj ∈ R に対して，sc1 (Ri , Rj , ≈α ) か

3. 3 名目書き換えにおける CR ≈α 性 の十分条件

つ sc2 (Ri , Rj , ≈α )，あるいは，sc1 (Rj , Ri , ≈α ) かつ

本小節では，3.1 節で述べた TRSAX が合流性を持sc2 (Rj , Ri , ≈α ) が成立するならば，R は CR ≈α 性 をつための十分条件を拡張して，NRSAX が CR ≈α 性持つ．

を持つための十分条件を提案する．
まず， [9] では扱われていない ≈α を法とした強可換性の概念を定義する．

4 おわりに本稿では，アトム変数を持つ名目書き換えにおいて定義 24. R1 , R2 を書き換え規則とする．→R1 が ≈α

CR ≈α 性 が成り立つ条件について議論してきた．≈αを法として −→q R2 と強可換であるとは，s →R1 s′ かを法とした強可換性の概念を新たに定義し，それが成

つ s −→
q R2 t ならば，ある t′1 , t′2 が存在して s′ −→q R2 t′2立するための十分条件を提案した．

かつ t →∗R1 t′1 かつ t′1 ≈α t′2 が成り立つことをいう．

q−s −−−−→R2
Ry 1

今後の課題としては，提案した条件の判定手続きを合流性検証器 [1] に実装し，様々な例に適用すること

t

∗yR1

でその有効性を調査することがあげられる．

q−s′ −−−−→ t′2 ≈α t′1

謝辞 本研究の一部は JSPS 科研費 JP17K00005,

補題 25. →R1 が ≈α を法として −→q R2 と強可換でJP19K11891, JP20H04164 の助成を受けて行われた．

R2あり，→R1 と →R2 がともに ≈α と強両立であるな
らば，→R1 と →R2 は ≈α を法として可換である．

参 考 文 献補題 26. R を NRSAX とする．すべての Ri , Rj ∈ R[ 1 ] Aoto, T., Kikuchi, K.: Nominal confluence
tool. In: Olivetti, N., Tiwari, A. (eds.) IJCAR
2016. LNCS, vol. 9706, pp. 173–182. Springer-Verlag(2016)[ 2 ] Ayala-Rincón, M., Fernández, M., Gabbay,M.J., Rocha-Oliveira, A.C.: Checking overlaps ofnominal rewriting rules. Electronic Notes in Theoretical Computer Science 323, 39–56 (2016)[ 3 ] Baader, F., Nipkow, T.: Term Rewriting and All
That. Cambridge University Press (1998)[ 4 ] Fernández, M., Gabbay, M.J.: Nominal rewriting. Inform. Comput. 205, 917–965 (2007)[ 5 ] Gabbay, M.J., Pitts, A.M.: A new approach toabstract syntax with variable binding. Formal Aspects Comput. 13, 341–363 (2002)[ 6 ] Kikuchi, K., Aoto, T.: Confluence and commutation for nominal rewriting systems with atomvariables. In: Pre-proceedings of the 30th LOPSTR(2020) Available at https://nms.kcl.ac.uk/maribel.fernandez/LOPSTR2020/[ 7 ] Kikuchi, K., Aoto, T., Toyama, Y.: Parallel closure theorem for left-linear nominal rewriting systems. In: Proceedings of the 11th FroCoS. LNCS,
vol. 10483, pp. 115–131. Springer-Verlag (2017)[ 8 ] Kutz, Y., Schmidt-Schauß, M.: Rewriting withに対して →Ri と →Rj が ≈α を法として可換である
ならば，R は CR ≈α 性 を持つ．
次に，→R1 が ≈α を法として −→q R2 と強可換になるための十分条件を与える．
定義 27. R1 と R2 (= ∇2 ⊢ l2 → r2 ) を左線形な書き換え規則とする．このとき，条件 sc1 (R1 , R2 , ≈α )，sc2 (R1 , R2 , ≈α ) を以下のように定義する．
– sc1 (R1 , R2 , ≈α ) ⇐⇒ s →R1 s′ かつ s −→q R2 tdef

εが規則 (C) を最後に適用して導かれるならば，ある t′1 , t′2 が存在して s′ −→q R2 t′2 かつ t →∗R1 t′1 かつ t′1 ≈α t′2 ．
p– sc2 (R1 , R2 , ≈α ) ⇐⇒ s →R1 s′ かつ s →R2 t，def

ε

ここで p が l2 の非変数位置であるならば，あるt′1 , t′2 が存在して s′ −→q R2 t′2 かつ t →∗R1 t′1 かつt′1 ≈α t′2 ．
補 題 28. R1 と R2 を 左 線 形 か つ 一 様 な 書 き 換generalized nominal unification. Math. Struct. Comput. Sci., pp. 1–26 (2020) https://doi.org/10.10
17/S0960129520000122[ 9 ] Ohlebusch, E.: Church-Rosser theorems for abstract reduction modulo an equivalence relation. In:
Proceedings of the 9th RTA. LNCS, vol. 1379, pp.
17–31. Springer-Verlag (1998)[10] Pitts, A.M.: Nominal logic, a first order theoryof names and binding. Inform. Comput. 186, 165–193 (2003)[11] Suzuki, T., Kikuchi, K., Aoto, T., Toyama, Y.:

Confluence of orthogonal nominal rewriting systems
revisited. In: Proceedings of the 26th RTA. LIPIcs,vol. 36, pp. 301–317 (2015)[12] Suzuki, T., Kikuchi, K., Aoto, T., Toyama, Y.:
Critical pair analysis in nominal rewriting. In: Proceedings of the 7th SCSS. EPiC, vol. 39, pp. 156–168. EasyChair (2016)[13] Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoret. Comput. Sci. 323, 473–497(2004)