ラムダ計算、通常の順序、ノーマル形式、

Question

ラムダ計算では、用語が正規形である場合、通常の順序削減戦略は常にそれを生成します。

私はちょうど上記の命題を厳密に証明する方法を疑問に思っていますか？

Answer 1

あなたが言及した結果は、標準化定理の帰結であり、任意の縮小シーケンスM-> Nに対して、同じ用語MとNの間に別の「標準」があり、最も外側の最も外側で再デコードを実行する注文。証明はあまり自明ではなく、文献にはいくつかの異なるアプローチがあります。私は以下の短い参考文献を追加します。

最近のKashima 5の証明書（1も参照）は、残差の概念を使用せず、純粋に誘導性の技術に基づいているという利点があります。それは公式化2のためにも良いですが、あなたがまだその主題に自信がない限り、それは特に有益ではありません。

標準化の背景にある一般的な考え方は次のとおりです。 は2 redexesのRとSがRに関して左端の最も外側の位置にあるSを、持っているし、次の削減を検討すると仮定します。あなたの代わりに、Sを発射開始することができ、その後

   R  S 
      M -> P -> N 

を、しかし、この方法では、あなたSを発射した後のRの本質的に残っているこれらの再デコードは、残差と呼ばれ、通常はR/S（read：Sの後のRの残差）として示されます。 そこで、基本補題は、標準化のためにそれを使用するために

   R S = S (R/S) 

は、我々は最左最外位置WRTでない可約式を用いて、標準であると仮定してもよいことは、任意の配列ρ（rを一般化する必要があることですS）。

  (*) ρS = S (ρ/S) 

しかし、（ρ/ S）の標準化はそれほど明白ではないが、それでもなお真である。この目的のために、 は、発火S = C [\ xM N]の前にρが実行されたことを観察すると、 は3つの断絶領域：文脈C、M、およびNにおいて本質的に項を分割することを観察する。 これは、

  ρ1 inside M 
      ρ2 inside N 
      ρ3 inside C 

（ただし、最も外側の最も外側の位置にはredexが存在しないことに注意してください）。 複製可能（または消去済み）の部分はρ2であり、残りの部分は ρ2-0...ρ2-kであり、Sの発火によって作成されたNのk個のコピーの の異なる位置に従って簡単に並べ替えられます。したがって

S ρ1 ρ2-0 ... ρ2-k ρ_3 

は、（*）の標準バージョンです。

基本的な参考文献。

1 A.Asperti、JJ。徴収。 The cost of usage in the lambda-calculus。 LICS 2013.

3 H. P. Barendregt。ラムダ微積分、北ホラント（1984年）。

4 G.Gonthier、JJ。レヴィ、PA。 Mellies。 An abstract standardisation theorem。 LICS '92。

2 F.Guidi。 Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover。公式推論雑誌 5（1）：1-25、2012.

5 R.Kashima。 A proof of the standardization theorem in lambda-calculus。 テクニカルレポートC-145、東京工業大学2000.

[6] JW。 Klop。コンビナトリアルリダクションシステム。博士論文、CWI、 アムステルダム、1980年。

[7] G.Mitschke。ラムダ計算の標準化定理。 Z. Math.Logik。 Grundlag。 Math、25：29-31、1979

[8] M.Takahashi。ラムダ計算の並列減少。 Information and Computation 118、pp.120-127、1995.

[9] H. Xi、Upper bounds for standardizations and an application。 Journal of Symboloc Logic 64、pp.291-303、1999.