抽象書き換えシステム

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

歴史的に、抽象的な設定での書き換えの形式化はいくつかあり、それぞれに特異性があります。これは、一部の概念が同等であるという事実によるところが大きいです。この記事の後半を参照してください。モノグラフや教科書で最もよく見られる形式化は、Gérard Huet (1980) によるもので、ここでも一般的に採用されています。^[1]

抽象リダクション システム( ARS ) は、オブジェクトと、それらを変換するために適用できるルールのセットを指定する最も一般的な (一次元的な) 概念です。最近では、著者は抽象書き換えシステムという用語も使用しています。^[2] (ここで「書き換え」ではなく「リダクション」という単語が好まれているのは、ARS を特殊化したシステムの名前で「書き換え」が一様に使用されていることから離れているからです。「リダクション」という単語は、より特化したシステムの名前には現れないため、古いテキストでは、リダクション システムはARS の同義語です。) ^[3]

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

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

数学的対象として、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 が存在し、である場合に既約であるといいます。そうでない場合は既約でない、または正規形であるといいます。オブジェクトyは、 であり、が既約である場合にxの正規形と呼ばれます。 x に一意の正規形がある場合、これは通常 で表されます。上記の例 1 では、c は正規形であり、 です。すべてのオブジェクトが少なくとも 1 つの正規形を持つ場合、ARS はを正規化 していると呼ばれます。 ${\displaystyle x\rightarrow y}$${\displaystyle x{\stackrel {*}{\rightarrow }}y}$${\displaystyle x\downarrow}$${\displaystyle c=a\downarrow =b\downarrow }$

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

ARS は、すべてのオブジェクトx、yに対してが成り立つ場合のみ、チャーチ＝ロッサー特性を持つと言われます。同様に、チャーチ＝ロッサー特性は、反射的推移対称閉包が結合可能性関係に含まれていることを意味します。アロンゾ・チャーチとJ. バークレー・ロッサーは、1936 年にラムダ計算がこの特性を持つことを証明しました。^[6]これがこの特性の名前の由来です。^[7]チャーチ＝ロッサー特性を持つ ARS では、単語問題は共通の後継者を探すことに簡約できます。チャーチ＝ロッサー システムでは、オブジェクトは最大で 1 つの正規形を持ちます。つまり、オブジェクトの正規形は存在する場合は一意ですが、存在しない可能性もあります。 ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$${\displaystyle x{\mathbin {\downarrow }}y}$

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

• 合流性とは、A内のすべてのw、x、yに対して が成り立つ場合のみである。大まかに言えば、合流性とは、2 つのパスが共通の祖先 ( w ) からどのように分岐しても、パスが共通する後継パスで合流することを意味します。 この概念は、特定のオブジェクトwのプロパティとして洗練され、すべての要素が合流している場合、システムは合流していると呼ばれることがあります。${\displaystyle x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y}$${\displaystyle x{\mathbin {\downarrow }}y}$
• 半合流性であるためには、 A 内のすべての w 、 x 、 y に対して が成り立つことが 必要です。これは、wからxへの1 ステップ簡約によって合流性と異なります。${\displaystyle x\leftarrow w{\stackrel {*}{\rightarrow }}y}$${\displaystyle x{\mathbin {\downarrow }}y}$
• 局所的に合流性であるために は、 A内のすべてのw、x、yに対して が成り立つことが必要です。この性質は、弱い合流性と呼ばれることもあります。${\displaystyle x\leftarrow w\rightarrow y}$${\displaystyle x{\mathbin {\downarrow }}y}$

定理。ARSの場合、次の3つの条件は同等である：(i)チャーチ・ロッサー特性を持つ、(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として定義することができます。Book と Otto にあるこの定義は、合流系ではここで示されている一般的な定義と同等ですが、非合流 ARS ではより包括的です。 ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$

一方、局所合流は、このセクションで説明した他の合流の概念と同等ではありませんが、合流よりも厳密に弱いものです。典型的な反例は で、これは局所合流ですが合流ではありません (図を参照)。 ${\displaystyle \{b\rightarrow c,c\rightarrow b,b\rightarrow a,c\rightarrow d\}}$

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

定理(ニューマンの補題): 終了 ARS が合流性を持つのは、それが局所的に合流性を持つ場合のみです。

1942年にニューマンが行ったこの結果の最初の証明はかなり複雑でした。1980年にヒュートが、終了するときに十分根拠のある帰納法を適用できるという事実を利用したはるかに単純な証明を発表しました。^[12]${\displaystyle \rightarrow}$

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

• バーダー、フランツ、ニプコウ、トビアス（1998）。用語の書き換えとそのすべて。ケンブリッジ大学出版局。ISBN 9780521779203。学部生に適した教科書。
• Nachum DershowitzとJean-Pierre Jouannaud書き換えシステム、Jan van Leeuwen (編)、『理論計算機科学ハンドブック B 巻: 形式モデルとセマンティクス』、Elsevier および MIT Press、1990 年、ISBN 0-444-88074-7、pp. 243–320 の第 6 章。この章のプレプリントは著者から無料で入手できますが、図が欠落しています。 
• 書籍、ロナルド V. ; オットー、フリードリヒ (1993)。「1、「抽象的縮約システム」「文字列書き換えシステム」 Springer ISBN 0-387-97965-4。
• マルク・ベゼム;ヤン・ウィレム・クロップ;ロエル・デ・ヴリエル。テレーゼ (2003)。 「1」。用語書き換えシステム。ケンブリッジ大学出版局。ISBN 0-521-39115-6。これは包括的なモノグラフです。ただし、他ではあまり見られないような表記法や定義がかなり使用されています。たとえば、Church-Rosser プロパティは合流と同じであると定義されています。
• ハリソン、ジョン（2009）。「4「平等」」「実践論理と自動推論ハンドブック」ケンブリッジ大学出版局。ISBN 978-0-521-89957-4。等式論理における問題を解決する実践的な観点からの抽象的な書き換え。
• Gérard Huet、「合流型縮約: 項書き換えシステムへの抽象的性質と応用」、Journal of the ACM ( JACM )、1980 年 10 月、第 27 巻、第 4 号、797 ～ 821 ページ。Huet の論文は、現代の概念、結果、表記法の多くを確立しました。
• Sinyor, J.; 「文字列書き換えシステムとしての 3x+1 問題」、International Journal of Mathematics and Mathematical Sciences、Volume 2010 (2010)、記事 ID 458563、6 ページ。
• Duffy, David A. (1991).自動定理証明の原理. Wiley.
• Church, Alonzo; Rosser, JB (1936). 「変換のいくつかの特性」.アメリカ数学会誌. 39 (3): 472–482. doi : 10.2307/1989762 . ISSN  0002-9947. JSTOR  1989762.