抽象書き換えシステム

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

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

意味

抽象縮約システム（ARS）は、オブジェクトとそれらを変換するために適用可能な規則の集合を規定する最も一般的な（一次元的な）概念である。近年では、抽象書き換えシステムという用語も用いられている。^{[ 2 ]}（ここで「書き換え」ではなく「縮約」という語が好まれているのは、ARSを特殊化したシステムの名称において「書き換え」という語が一様に用いられていることから逸脱している。「縮約」という語はより特化したシステムの名称には現れないため、古い文献では縮約システムはARSの同義語となっている。）^{[ 3 ]}

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

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

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

例1

オブジェクトの集合が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は、かつ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は結合可能であるとされます。この定義から、結合可能性関係を と定義できることは明らかです。ここで、は関係 の合成です。結合可能性は通常、やや紛らわしいことに とも表記されますが、この表記法では下矢印は二項関係、つまりxとy が結合可能である場合と書きます。 ${\displaystyle x{\stackrel {*}{\rightarrow }}z{\stackrel {*}{\leftarrow }}y}$ ${\displaystyle {\stackrel {*}{\rightarrow }}\circ {\stackrel {*}{\leftarrow }}}$ ${\displaystyle \circ}$ ${\displaystyle \downarrow}$ ${\displaystyle x\mathrel {\downarrow } y}$

チャーチ＝ロッサーの性質と合流の概念

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

チャーチ＝ロッサー則よりも単純な様々な性質が、これと同値である。これらの同値の性質の存在により、より少ない労力でシステムがチャーチ＝ロッサー則であることを証明することができる。さらに、合流の概念は特定の対象の性質として定義することができるが、これはチャーチ＝ロッサー則では不可能である。ARSは、次のように表現される。 ${\displaystyle (A,\rightarrow )}$

• 合流性とは、 A内のすべてのw、x、yに対してが成り立つ場合のみである。 大まかに言えば、合流性とは、共通の祖先（w）から2つの経路がどのように分岐したとしても、それらの経路は共通の後継者で合流することを意味する。この概念は、特定のオブジェクトwの特性として洗練され、そのすべての要素が合流している場合、そのシステムは合流性を持つと呼ばれる。${\displaystyle x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y}$ ${\displaystyle x\mathrel {\downarrow } y}$
• 半合流性とは、 A内のすべてのw、x、yに対して が成り立つときに限ります。 これは、 wからxへの1ステップの縮約によって合流性とは異なります。${\displaystyle x\leftarrow w{\stackrel {*}{\rightarrow }}y}$ ${\displaystyle x\mathrel {\downarrow } y}$
• 局所合流性とは、 Aの 任意のw、x、yに対して が成り立つことと同値である。この性質は、弱い合流性と呼ばれることもある。${\displaystyle x\leftarrow w\rightarrow y}$ ${\displaystyle x\mathrel {\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 }$

参照

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

注記

1. ブック＆オットー 1993、9ページ
2. テレーズ 2003、p. 7
3. ブック＆オットー 1993、p. 10
4. テレーズ 2003、7～8ページ
5. Baader & Nipkow 1998、pp. 8–9
6. チャーチ＆ロッサー 1936
7. バーダー＆ニプコウ 1998、9ページ
8. Baader & Nipkow 1998、p. 11
9. Baader & Nipkow 1998、p. 12
10. テレーズ 2003、11ページ
11. ダフィー 1991、p. 153、sect.7.2.1
12. ハリソン 2009、260ページ

参考文献

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