Loading article…
抽象書き換えにおいて、[ 1 ]オブジェクトが正規形であるのは、それ以上書き換えることができない、つまり既約である場合である。書き換えシステムによっては、オブジェクトは複数の正規形に書き換えられる場合もあれば、全く書き換えられない場合もある。書き換えシステムの多くの特性は正規形に関連している。
正式に述べると、( A ,→) が抽象的な書き換えシステムである場合、x ∈ Aは、 x → yとなるようなy ∈ Aが存在しない、つまりxが既約項である場合に正規形である。
オブジェクトaは、aから始まる書き換えの特定のシーケンスが少なくとも 1 つ存在し、最終的に正規形が得られる場合、弱正規化である。書き換えシステムは、すべてのオブジェクトが弱正規化である場合、弱正規化特性を持つか、（弱）正規化（WN）である。オブジェクトaは、 aから始まるすべての書き換えのシーケンスが最終的に正規形で終了する場合、強正規化である。書き換えシステムは、その各オブジェクトが強正規化である場合、強正規化、終了性、ネーター性、または（強）正規化特性（SN）を持つ。[ 2 ]
書き換えシステムは、すべての対象aと正規形bについて、aから一連の書き換えと逆書き換えによってbに到達できるのはa がbに縮約される場合に限る場合、正規形特性 (NF) を持つ。書き換えシステムは、すべての正規形a、b ∈ Sについて、aから一連の書き換えと逆書き換えによって b に到達できるのは a が b と等しい場合に限る場合、一意正規形特性(UN) を持つ。書き換えシステムは、縮約に関して一意正規形特性(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 ]
非正規化システム（弱正規化でも強正規化でもない）の例としては、無限に数えること（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 ]
