Loading article…
抽象書き換えでは、[1]オブジェクトがそれ以上書き換えられない、つまり既約でない場合には、そのオブジェクトは正規形になります。書き換えシステムによっては、オブジェクトが複数の正規形に書き換えられる場合もあれば、まったく書き換えられない場合もあります。書き換えシステムの多くの特性は正規形に関連しています。
定義
正式に述べると、( A ,→) が抽象的な書き換えシステムである場合、x → yとなるy ∈ Aが存在しない、つまりx が既約項である とき、 x ∈ Aは正規形になります。
オブジェクトaが弱正規化であるとは、 aから始まる書き換えの特定のシーケンスが少なくとも 1 つ存在し、最終的に正規形になることを指します。書き換えシステムは、すべてのオブジェクトが弱正規化である場合、弱正規化プロパティを持つか、(弱) 正規化(WN) です。オブジェクトaが強く正規化であるとは、 aから始まる書き換えのシーケンスがすべて最終的に正規形で終了する場合を指します。抽象書き換えシステムは、各オブジェクトが強く正規化である場合、強く正規化、終了、ネーター、または(強い) 正規化プロパティ(SN) を持ちます。[2]
書き換えシステムが正規形の性質(NF)を持つのは、すべてのオブジェクトaと正規形bに対して、a がbに簡約される場合に限り、一連の書き換えと逆書き換えによってa からbに到達できるときである。書き換えシステムが一意正規形の性質(UN) を持つのは、すべての正規形a、b ∈ Sに対して、a がbに等しい場合に限り、一連の書き換えと逆書き換えによって b から a に到達できるときである。書き換えシステムが簡約に関して一意正規形の性質(UN → ) を持つのは、正規形aとbに簡約されるすべての項に対して、a がbに等しいときである。[3]
結果
このセクションでは、よく知られている結果をいくつか紹介します。まず、SNはWNを意味します。[4]
合流（略称 CR）は、NF を意味し、UN を意味し、UN → を意味します。[3]逆の含意は一般には成り立ちません。{a→b、a→c、c→c、d→c、d→e} は UN →ですが、b=e および b、e が正規形であるため UN ではありません。{a→b、a→c、b→b} は UN ですが、b=c および c が正規形であり、b が c に簡約されないため NF ではありません。{a→b、a→c、b→b、c→c} は正規形がないため NF ですが、a が b および c に簡約され、b、c に共通の簡約がないため CR ではありません。
WNとUN →合流を意味する。したがってWNが成立する場合、CR、NF、UN、UN →は一致する。[5]
例
一例として、算術式を簡略化すると数値が生成されるが、算術ではすべての数値は正規形である。注目すべき事実は、すべての算術式は一意の値を持つため、書き換えシステムは強く正規化され合流的であるということ：[6]
- (3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24
- (3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24
非正規化システム（弱くも強くもない）の例には、無限へのカウント（1 ⇒ 2 ⇒ 3 ⇒ ...）や、コラッツ予想の変換関数（1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ...、コラッツ変換のループが他にもあるかどうかは未解決問題）などのループがある。[7]もう1つの例は、単一ルールシステム{ r（x、y）→ r（y、x）}である。これは正規化特性を持たない。なぜなら、任意の項、例えばr （4、2）から、 r（4、2）→ r（2、4）→ r（4、2）→ r （ 2、4）→ ...という単一の書き換えシーケンスが開始され、これは無限に長いからである。これは、「交換性法」の書き換えというアイデアにつながる。この場合、交換性以外のルールが適用されない場合、項は正規形になる。[8]
システム { b → a、b → c、c → b、c → d } (図) は、弱正規化ではあるが強く正規化ではないシステムの例です。aとd は正規形であり、bとc はaまたはdに簡約できますが、無限簡約b → c → b → c → ... は、bもcも強く正規化されないことを意味します。
型なしラムダ計算
純粋な型なしラムダ計算は、強い正規化特性を満たさず、弱い正規化特性さえも満たしません。項（適用は左結合）を考えてみましょう。次の書き換え規則があります。任意の項 に対して、
しかし、それを自分自身に 適用すると何が起こるか考えてみましょう。
したがって、この項は強く正規化されていません。また、これは唯一の削減シーケンスであるため、弱く正規化されていません。
型付きラムダ計算
単純型付きラムダ計算、ジャン＝イヴ・ジラールのシステム F、ティエリー・コカンの構成計算など 、型付きラムダ計算のさまざまなシステムは、強く正規化されます。
正規化特性を持つラムダ計算システムは、すべてのプログラムが終了するという特性を持つプログラミング言語と見なすことができます。これは非常に便利な特性ですが、欠点があります。正規化特性を持つプログラミング言語はチューリング完全ではありません。そうでなければ、プログラムの型がチェックされるかどうかを見ることで停止問題を解決できます。これは、単純型ラムダ計算では定義できない計算可能な関数があることを意味し、構成計算やシステムFでも同様です。典型的な例は、トータルプログラミング言語の自己インタープリタです。[10]
参照
注記
参考文献
- ^ フランツ・バーダー、トビアス・ニプコウ（1998年）。用語の書き換えとそのすべて。ケンブリッジ大学出版局。ISBN 9780521779203。
- ^ Ohlebusch, Enno (1998). 「同値関係を法とする抽象縮約に関するチャーチ・ロッサー定理」。書き換え技術とアプリケーション。 コンピュータサイエンスの講義ノート。 第 1379 巻。 p. 18。doi :10.1007/BFb0052358。ISBN 978-3-540-64301-2。
- ^ ab Klop, JW; de Vrijer, RC (1989年2月). 「射影ペアリングによるラムダ計算の一意正規形」.情報と計算. 80 (2): 97–113. doi : 10.1016/0890-5401(89)90014-X .
- ^ 「ロジック - 書き換えシステムのコンテキストにおける強い正規化と弱い正規化の違いは何ですか?」。Computer Science Stack Exchange 。 2021年9月12日閲覧。
- ^ Ohlebusch, Enno (2013年4月17日). 用語書き換えの高度なトピック. Springer Science & Business Media. pp. 13–14. ISBN 978-1-4757-3661-8。
- ^ Terese (2003).項書き換えシステム. ケンブリッジ、イギリス: ケンブリッジ大学出版局. p. 1. ISBN 0-521-39115-6。
- ^ Terese (2003).項書き換えシステム. ケンブリッジ、イギリス: ケンブリッジ大学出版局. p. 2. ISBN 0-521-39115-6。
- ^ Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). 「6. 書き換えシステム」Jan van Leeuwen (編)理論計算機科学ハンドブック. 第 B 巻 . Elsevier. pp. 9–10. CiteSeerX 10.1.1.64.3114 . ISBN 0-444-88074-7。
- ^ N. Dershowitz および J.-P. Jouannaud (1990)。「Rewrite Systems」。Jan van Leeuwen (編) 著。形式モデルとセマンティクス。理論計算機科学ハンドブック。第 B 巻。Elsevier。p. 268。ISBN 0-444-88074-7。
- ^ Riolo, Rick; Worzel, William P.; Kotanchek, Mark (2015年6月4日). 遺伝的プログラミングの理論と実践 XII. Springer. p. 59. ISBN 978-3-319-16030-6. 2021年9月8日閲覧。