1　はじめに
合流性は書換え系に関する重要な性質の一つであるが，一般に，とくに入計算などの高階書換え系の合流性を証明することは難しい．例えば，型のない入計算のβ簡約では，強正規化性やダイヤモンド性が成立しないため，合流性の証明には並行簡約や，complete developmentなどのアイデアが必要となる．Z定理[1]は書換え系の合流性を証明する手法の一つであり, Z性と呼ばれる性質を満たす写像が存在するならば書換え系が合流性を持つことを保証する．例えば，入計算のβ簡約については，入項中に存在するβ簡約基を一度に簡約する写像であるcomplete developmentがZ性を満たすので，Z定理によって合満性が証明できる．しかし，書換え系に対しZ性を持つ写像を構成することは，一般には容易ではない．合流性を直接示すことが難しい場合，合流性に関して健全な書換え系の変換を用いる手法がある．この手法の例として，条件付き項書換え系（CTRS）におけるunraveling [3]が挙げられる．これはCTRSを近似的に通常の項書換え系（TRS）に変換する写像である.変換後のTRSの合流性が変換前のCTRSの合流性を含意するときunravelingは合流性に関して健全であるという．つまり，合流性に関して健全なunravelingによって， CTRSの合流性を変換後のTRSの合流性に綿着することができる.本研究では，書換え系の変換を用いて，既にZ性を満たすことが分かっている写像から，新たにZ性を満たす写像を構成する手法を提案する。より具体的には，一定の条件を満たす変換F : A → Bと，B上のZ性を満たす写像から，Ａ上のZ性を満たす写像を構築する．さらに，この手法を用いて明示的代入を含む入計算においてZ性を満たす写像を構築できることを示す.
2　合流性とＺ定理
本章では，合流性とZ定理について説明する．定義2.1 (合流性). (A, →)を抽象書換え系であるとする．つまり， Aを集合， →をA上の二項関係とする．また， →を→の反射推移閉包であるとする．任意のx, y1, y2 ∈ Aについて, y1 ←− x → y2ならはy1 —» z «— y2を満たすz ∈ Aが存在するとき, (A, →)は合流性を持つと言う. Z定理は合流性を証明する手法の一つである.定義2.2 (Z性[1]). Aを集合， →をA上の二項関係とする．また，→を→の反射推移関包であるとする.写像ƒ : A → Aが，任意のα,b ∈ Aについてα → bならばb → f (α) → f (δ)を満たすとき， fは→について乙性を満たすと言う.また，書換え系(A, →)に対して，Z性をみたす写像が存在するとき， ( A , →)はZ性を満たすと言う.条件が図１のように書けるため，この性質をZ性と呼ぶ。定理2.3 (Z定理[1]).抽象書換え系が乙性を満たすならば，その抽象書換え系は合流性を持つ. Z性は合流性よりも真に強い性質であることがわかっている．つまり，合流性を持つ抽象書換え系に対して，Z性を満たす写像が存在するとは限らない．これは図2の反例によって示される．図2の書換え系は合流性を持つが，Z性を満たす写像は存在しない.乙性を満たす写像の一つの例は入計算のβ簡約についてのcomplete developmentである.定義2.4 (入計算).入項は次のように定義される. M := x | λ x . M | M M .入項に対するβ簡約は次のβ規則のcompatible closureとして定義される. ( λ x . M ) N → M [ x := N ] (β),ただし， M [ x := N ]はα変換によって新たな束縛を生じない代入とする.ある項中の，一つの規則の左辺とマッチする部分項を簡約基と呼ぶ。complete developmentは全ての見えている簡約基を一度に簡約する写像である.定義2.5 (β簡約のcomplete development). β簡約に対するcomplete development M*は次のように定義される. 1. x* = x 2. (λ x . M )* = λ x . M * 3.  ((λx.M1)M2)* = Mi [x := M2] 4. (M 1 M 2 )* = M 1 M 2 (その他のとき)定理2.6 ([1]).写像M*はZ性を満たす.
3　書換え系の変換によるZ性証明
まず準備としてトライアングル性について説明する.定義3.1 (トライアングル性). Aを集合， →をA上の二項関係とする。写像ƒ : AとA上の二項関係⇒が以下の性質を満たすとき，ƒと⇒はトライアングル性を満たすという.任意のa,b ∈ Aについてa ⇒ bならばb ⇒ f(a).また，今後のために⇒ rという表記を以下のように定義する.定義3.2 (⇒ f)  (A, →)をARS,  fを→についてZ性を満たす写像とする．このとき，⇒ fを以下で定義する. α ⇒ f b iff α −∞ b −∞ f (α) Z性とトライアングル性について以下の事実が成    以上の証明を図に表すと図3のようになる. り立つ.補題3.3. (A, →)上でƒ : A → AがZ性を満たすとき, ƒと⇒ ƒはトライアングル性を満たす. Proof.任意のα ⇒ γ bについて，⇒ γの定義より, a — b —» f(a). a —» bとfのZ性より, f(a) —» f(b).したがって，b ⇒ f f(a)が成り立ち，fと⇒ fはトライアングル性を満たす. ●補題3.4. (A, →)に対してƒ : A → Aと⇒がトライアングル性を満たすとき，以下が成り立つ．任意のα,ｂ∈ Aについてα ⇒ bならばb ⇒ f(α) ⇒ f(b) (1ステップのZ性) Proof. fと⇒はトライアングル性を満たすので, α ⇒ bならばb ⇒ f (a).さらにトライアングル性より, b ⇒ f(a)ならばf(a) ⇒ f(b).以上より, a ⇒ bならばb ⇒ f(a) ⇒ f(b)が成り立つ. ●以上の事実から以下の定理が証明できる.定理 3.5.  (A, → λ), (B, → B)をARS, g : B → Bを→ BについてZ性を満たす写像とする．F : A → B,G : B → Aが次を満たすとする. 1.任意のa,a' ∈ Aについてa → λ α'ならばF(α) ⇒ g F(α') 2. 任意のb,b' ∈ Bについてb ⇒ b'ならばG(b) -» A G(b') 3.任意のα ∈ Aについてα → λ G ◦ F(α)このとき，G o g o Fは(A, → λ )についてZ性を満たす. Proof.任意のa → a ′について,条件1.より, F(a) ⇒ g F(a').補題3.3より, gと⇒ gはトライアングル性を満たす.補適3.4より,  F(α) ⇒ 9 F(α') ⇒ 9 g ◦ F(α) ⇒ g g ◦ F(α′). 条件2.より，G ◦ F(α) ⇒ л GoF(a') → Λ GogoF(a) → Λ GogoF(a').条件3.より, α′ → λ G ◦ F (α′).以上より,任意のα → λ α′について，α′ → λ G ◦ g ◦ F (α) → λ G ◦ g ◦ F (α′).したがって，ＧｏｇｏＦは(A, → λ )についてZ性を満たす.
4　明示的代入計算入のZ性証明
定理3.5を用いて，明示的代入を含む入計算であるλ。についてZ性を満たす写像を構成する.定義4.1 (λ x). λ xの項は次のように定義される. M := x | λ x . M | M | M | x := M ⟩ .入。の簡約は次の規則のcompatible closureとして定義される.
y〈y := N〉 → N ( π h i t ) x〈y := N〉→ x (πgc) (λx.P){y := N} → λx.P{y := N} (Tabs) (PQ){y := N} → P{y := N}Q{y := N}   (πapp)定理3.5を用いることで，入のZ性を入計算のβ簡約のZ性に帰着することができる．定理3.5で用いる写像として，Fを明示的代入を通常の代入に変換する写像，Gを恒等写像と定義する．定義 4.2.明示的代入を通常の代入に変換する写像Fは以下のように定義される. 1. F(x) = x 2.  F(λx.M) = λx.F(M) 3.  F(M 1 M 2 ) = F(M 1 ) F(M 2 ) 4.  F(M1 {y := M2 }) = F(M1)[x := F(M2 )]定理4.3. → xをλ xの簡約，→ pを定義2.4の入計算のβ簡約とする．gを定義2.5で与えたβ簡約に対するcomplete developmentとする．このとき， g o Fは→ xについてZ性を満たす. Proof.定理3.5を適用する. Aは定義4.1のλ x , Bは定義2.4の入計算とする．条件1.について， M → x Nが規則(βx)を行うとき, F(M) → β F(N). M → x Nがその他の規則を行うとき, F(M) = F(N).したがって，条件1.は成り立つ.条件2., 3.は簡単に証明できる. ●入。に対してZ性を満たす写像は合成的Z定理を用いて既に与えられているが[2]，定理4.3のg ◦ Fは
●
この写像と同一のものである.
5　まとめと今後の課題
本研究では，定理3.5によって既にZ性を満たすことが分かっている写像から，新たにZ性を満たす写像を構成する手法を与えた．また，定理3.5を用いて明示的代入を含む入計算のZ性を証明した．今後の課題としては，refinementやCTRSに対する定理3.5の応用が挙げられる. ARS (A, → A), (B, → B)について, B ⊂ Aかつ→ BC→λを満たすとき, (A,→ λ )は(B,→ B)のrefinementであると言う．例えば，定義4.1の入，は定義2.4の入計算のrefinementになっている. 入xと入計算のcomplete developmentは，定理3.5の条件を満たしているが，一般にはrefinement BとA上のZ性を満たす写像が定理3.5の条件を満たすとは限らない．例えば，図4の書換え系AはBのrefinementであり，ＢはＺ性を満たすがＡはＺ性を満たさないため，定理3.5の条件を満たさない．今後，どのようなrefinementが定理3.5の条件を満たすかを考えていきたい.