抽象書き換えシステム

数理論理学および理論計算機科学において、抽象書き換えシステム（または（抽象）還元システム、抽象書き換えシステム、略称ARS）は、書き換えシステムの本質的な概念と特性を捉える形式体系である。最も単純な形式では、ARSは単に（「オブジェクト」の）集合と、伝統的にで表される二項関係からなる。${\displaystyle \rightarrow }$; この定義は、二項関係のサブセットにインデックス（ラベル）を付けることでさらに洗練できます。その単純さにもかかわらず、ARSは正規形、停止性、さまざまな合流概念など、書き換えシステムの重要な特性を記述するのに十分です。

歴史的に、抽象的な設定での書き換えにはいくつかの形式化があり、それぞれに独自の特徴があります。これは、いくつかの概念が同等であるという事実にも一部起因しています（この記事の後半を参照）。モノグラフや教科書で最もよく見られる形式化であり、ここでも一般的に採用されているのは、ジェラール・ユエ（1980）によるものです。^{[ 1 ]}

抽象還元システム( ARS ) は、オブジェクトのセットと、それらを変換するために適用できるルールを指定することに関する最も一般的な (一次元) 概念です。最近では、著者は抽象書き換えシステムという用語も使用しています。^{[ 2 ]} (ここで「書き換え」ではなく「還元」という言葉が好まれるのは、ARS の特殊化であるシステムの名称で「書き換え」が統一的に使用されていることからの逸脱です。より特殊化されたシステムの名称には「還元」という言葉が見られないため、古い文献では還元システムはARS の同義語となっています。) ^{[ 3 ]}

ARS は、通常オブジェクトと呼ばれる要素を持つ集合Aと、伝統的に → で表され、還元関係、書き換え関係^{[ 2 ]}、または単に還元^{[ 3 ]}と呼ばれるA上の二項関係とから成ります。この (定着した) 「還元」という用語の使用は、関係が必ずしもオブジェクトの何らかの尺度を還元するとは限らないため、少し誤解を招く可能性があります。

場合によっては、規則のサブセット、つまり還元関係→のサブセットを区別することが有益な場合があります。たとえば、還元関係全体が結合規則と交換規則から構成される場合があります。したがって、一部の著者は還元関係→をいくつかの関係のインデックス付き和集合として定義します。たとえば、${\displaystyle {\rightarrow _{1}\cup \rightarrow _{2}}={\rightarrow }}$使用される表記は (A, → ₁ , → ₂ ) です。

数学的対象として、ARS はラベルなし状態遷移システムとまったく同じであり、関係がインデックス付き和集合とみなされる場合、ARS はインデックスがラベルであるラベル付き状態遷移システムと同じである。ただし、研究の焦点と用語は異なる。 状態遷移システムでは、ラベルをアクションとして解釈することに関心があるのに対し、ARS では、オブジェクトが他のオブジェクトにどのように変換（書き換え）されるかに焦点が当てられる。^{[ 4 ]}

オブジェクトの集合をT = { a , b , c } とし、二項関係をa → b、b → a、a → c、b → cという規則で定義します。これらの規則はaとbの両方に適用してcを得ることができることに注意してください。さらに、 cにはそれ以上変換する規則を適用することはできません。このような性質は明らかに重要なものです。

まず、いくつかの基本的な概念と表記法を定義します。^{[ 5 ]}

• ${\displaystyle {\stackrel {+}{\rightarrow }}}$は推移閉包である${\displaystyle \rightarrow }$。
• ${\displaystyle {\stackrel {*}{\rightarrow }}}$反射的推移閉包は${\displaystyle \rightarrow }$すなわち推移閉包${\displaystyle (\rightarrow )\cup (=)}$ここで、 = は恒等関係である。同様に、${\displaystyle {\stackrel {*}{\rightarrow }}}$最小の予約注文には${\displaystyle \rightarrow }$。
• 同様に、${\displaystyle {\stackrel {+}{\leftarrow }}}$、 そして${\displaystyle {\stackrel {*}{\leftarrow }}}$閉鎖は${\displaystyle {\leftarrow }}$の逆の関係${\displaystyle {\rightarrow }}$。
• ${\displaystyle \leftrightarrow }$は対称閉包である${\displaystyle \rightarrow }$つまり、${\displaystyle \rightarrow }$と${\displaystyle {\leftarrow }}$。
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$反射的推移的対称閉包は${\displaystyle \rightarrow }$すなわち推移閉包${\displaystyle (\leftrightarrow )\cup (=)}$同等に、${\displaystyle {\stackrel {*}{\leftrightarrow }}}$は、​${\displaystyle \rightarrow }$。

A内のオブジェクトxは、 A内に他のyが存在し、${\displaystyle x\rightarrow y}$そうでなければ、既約または正規形と呼ばれる。オブジェクトyがxの正規形であるとは、次の条件を満たす場合をいう。${\displaystyle x{\stackrel {*}{\rightarrow }}y}$そしてyは既約である。xが一意の正規形を持つ場合、これは通常、で表される。${\displaystyle x\downarrow }$上記の例1では、cは正規形であり、${\displaystyle c=a\downarrow =b\downarrow }$すべてのオブジェクトが少なくとも 1 つの正規形を持つ場合、ARS は正規化と呼ばれます。

正規形の存在よりも関連はあるものの弱い概念として、2つのオブジェクトが結合可能であるという概念がある。xとyは、ある性質を持つzが存在する場合に結合可能であると言われる。${\displaystyle x{\stackrel {*}{\rightarrow }}z{\stackrel {*}{\leftarrow }}y}$この定義から、結合可能性関係を次のように定義できることは明らかです。${\displaystyle {\stackrel {*}{\rightarrow }}\circ {\stackrel {*}{\leftarrow }}}$、 どこ${\displaystyle \circ }$は関係の合成です。結合可能性は、やや紛らわしいことに、通常、で表されます。${\displaystyle \downarrow }$しかし、この表記では下向き矢印は二項関係を表し、つまり次のように書きます。${\displaystyle x\mathrel {\downarrow } y}$xとyが結合可能な場合。

ARSは、以下の条件を満たす場合に限り、チャーチ・ロッサー財産を保有すると言われます。${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$暗示する${\displaystyle x\mathrel {\downarrow } y}$すべてのオブジェクトx、yについて。 同等に、チャーチ・ロッサーの性質は、反射的推移的対称閉包が結合関係に含まれることを意味します。アロンゾ・チャーチとJ. バークレー・ロッサーは1936 年にラムダ計算がこの性質を持つことを証明しました。^{[ 6 ]}そのため、この性質の名前が付けられました。^{[ 7 ]}チャーチ・ロッサーの性質を持つ ARS では、単語の問題は共通の後継者の探索に還元できます。 チャーチ・ロッサー システムでは、オブジェクトは最大で 1 つの正規形を持ちます。つまり、オブジェクトの正規形は存在する場合は一意ですが、存在しない場合もあります。

チャーチ・ロッサーよりも単純な様々な性質が、チャーチ・ロッサーと同等である。これらの同等の性質の存在により、より少ない労力でシステムがチャーチ・ロッサーであることを証明できる。さらに、合流の概念は特定のオブジェクトの性質として定義できるが、これはチャーチ・ロッサーでは不可能である。ARS${\displaystyle (A,\rightarrow )}$と言われているのは、

• 合流するのは、 Aのすべてのw、x、yに対して、 ${\displaystyle x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y}$暗示する${\displaystyle x\mathrel {\downarrow } y}$大まかに言えば、合流性とは、2つの経路が共通の祖先（ w ）からどのように分岐しても、それらの経路は共通の後継者で合流するということを意味する。この概念は、特定のオブジェクトwの特性としてより詳細化することができ、そのすべての要素が合流性を持つ場合、そのシステムは合流性を持つと呼ばれる。
• 半合流的であるのは、Aのすべてのw、x、yに対して、 ${\displaystyle x\leftarrow w{\stackrel {*}{\rightarrow }}y}$暗示する${\displaystyle x\mathrel {\downarrow } y}$これは、 wからxへの単一ステップの削減によって合流とは異なります。
• 局所的に合流するのは、Aのすべてのw、x、yに対して、 ${\displaystyle x\leftarrow w\rightarrow y}$暗示する${\displaystyle x\mathrel {\downarrow } y}$この性質は、弱い合流性と呼ばれることもあります。

定理。ARSの場合、次の 3 つの条件は同等である。(i) Church–Rosser 特性を持つ、(ii) 合流性である、(iii) 半合流性である。^{[ 8 ]}

系^{[ 9 ]}合流型ARSでは、${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$それから

• xとyが両方とも正規形である場合、 x = yとなる。
• yが正規形である場合、${\displaystyle x{\stackrel {*}{\rightarrow }}y}$。

これらの等価性のため、文献では定義にかなりのばらつきが見られます。例えば、Tereseでは、Church–Rosser特性と合流性は同義であり、ここで提示されている合流性の定義と同一であると定義されています。ここで定義されているChurch–Rosserは名前が付けられていませんが、同等の特性として与えられています。他のテキストとのこの違いは意図的なものです。^{[ 10 ]}上記の系により、xの正規形yを、次の性質を持つ既約yとして定義することができます。${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$BookとOttoに見られるこの定義は、合流型システムではここで示されている一般的な定義と同等ですが、非合流型ARSではより包括的なものとなっています。

一方、局所的合流は、この節で述べた他の合流の概念とは同値ではなく、合流よりも厳密に弱い概念である。典型的な反例は、${\displaystyle \{b\rightarrow c,c\rightarrow b,b\rightarrow a,c\rightarrow d\}}$これは局所的には合流しているが、合流しているわけではない（図を参照）。

抽象書き換えシステムは、無限連鎖が存在しない場合、終端的またはネーター的であると言われる。${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$（これは単に書き換え関係がネーター関係であると言っているだけです。） 終端ARSでは、すべてのオブジェクトが少なくとも1つの正規形を持つため、正規化します。逆は真ではありません。たとえば例1では、無限書き換えチェーン、すなわち、${\displaystyle a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots }$システムが正規化している場合でも、合流して終了する ARS は、正準^{[ 11 ]}または収束と呼ばれます。収束 ARS では、すべてのオブジェクトに一意の正規形があります。ただし、例 1 で示されているように、すべての要素に一意の正規形が存在するためには、システムが合流して正規化しているだけで十分です。

定理（ニューマンの補題）：終端ARSが合流的であるのは、それが局所的に合流的である場合に限る。

ニューマンによるこの結果の1942年の元の証明はかなり複雑だった。1980年になってようやく、ヒューエは、${\displaystyle \rightarrow }$終了時には、根拠のある帰納法を適用できます。^{[ 12 ]}

• 文章問題（数学） —特に抽象書き換えシステムに関するセクション

• バーダー、フランツ；ニプコウ、トビアス（1998）。用語書き換えとその他諸々。ケンブリッジ大学出版局。ISBN 9780521779203。学部生に適した教科書。
• ナフム・ダーショウィッツとジャン＝ピエール・ジュアナウ「書き換えシステム」 、ヤン・ファン・レーウェン編『理論計算機科学ハンドブック、第B巻：形式モデルと意味論』第6章、エルゼビアおよびMITプレス、1990年、ISBN 0-444-88074-7 、 243 ～ 320ページ。この章のプレプリントは著者から無料で入手できますが、図は含まれていません。
• Book, Ronald V. ; Otto, Friedrich (1993). "1, "抽象還元システム".文字列書き換えシステム. Springer. ISBN 0-387-97965-4。
• マルク・ベゼム;ヤン・ウィレム・クロップ;ロエル・デ・ヴリエル;テレーゼ (2003)。 「1」。用語書き換えシステム。ケンブリッジ大学出版局。ISBN 0-521-39115-6。本書は包括的なモノグラフである。しかしながら、他ではあまり見られない記号や定義が数多く用いられている。例えば、チャーチ＝ロッサー特性は合流と同一視されている。
• ハリソン、ジョン（2009）。「4 「平等」『実践論理と自動推論ハンドブック』ケンブリッジ大学出版局ISBN 978-0-521-89957-4。等式論理における問題解決の実践的な観点からの抽象概念の書き換え。
• ジェラール・ユエ、「合流還元：抽象特性と項書き換えシステムへの応用」、Journal of the ACM ( JACM )、1980年10月、第27巻、第4号、 797 ～ 821ページ。ユエの論文は、現代の概念、結果、表記法の多くを確立した。
• Sinyor, J.; 「文字列書き換えシステムとしての3x+1問題」、International Journal of Mathematics and Mathematical Sciences、第2010巻（2010年）、論文ID 458563、6ページ。
• ダフィー、デイビッド A. (1991).自動定理証明の原理. ワイリー。
• Church, Alonzo; Rosser, JB (1936). 「変換のいくつかの性質」 .アメリカ数学会紀要. 39 (3): 472–482 . doi : 10.2307/1989762 . ISSN 0002-9947 . JSTOR 1989762 .