明示的な置換

コンピュータサイエンスでは、ラムダ計算は置換プロセスの形式化に特別な注意を払っている場合、明示的な置換を持つと言われています。これは、計算内では表現されていない暗黙的な方法でベータ削減によって置換が実行される標準的なラムダ計算とは対照的です。このような暗黙的な計算の「新鮮さ」条件は、エラーの原因として悪名高いものです。 ^{[1]この概念は、}抽象マシン、述語論理、記号計算など、まったく異なる分野の多数の論文に登場しています。

明示的な置換を含むラムダ計算の簡単な例は「λx」です。これは、ラムダ計算に新しい形式の項、つまり「M で x が N に置換される」という形式 M⟨x:=N⟩ を追加します。(新しい用語の意味は、多くのプログラミング言語の一般的な慣用句let x:=N in Mと同じです。) λx は、次の書き換え規則 で記述できます。

1. (λx.M) N → M⟨x:=N⟩
2. x⟨x:=N⟩ → N
3. x⟨y:=N⟩ → x (x≠y)
4. (M ₁ M ₂ ) ⟨x:=N⟩ → (M ₁ ⟨x:=N⟩) (M ₂ ⟨x:=N⟩)
5. (λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y かつ x は N 内で自由ではない)

この定式化は、置換を明示的にしながらも、ラムダ計算の「変数規約」の複雑さを依然として保持しており、ルールを適用する前に最後のルールの「(x≠y かつ x は N 内で自由ではない)」条件が常に満たされるように、縮約中に変数を任意に名前変更する必要があります。したがって、明示的な置換の計算の多くは、いわゆる「名前のない」De Bruijn インデックス表記を使用して、変数名を完全に回避します。

^{明示的な置換は、Curryの組合せ論理に関する本[2]}の序文で概説され 、たとえばAUTOMATHで使用された「実装トリック」から発展し、ラムダ計算と書き換え理論における尊敬される統語論となった。これは実際にはde Bruijn ^[3]によって考案されたが、置換が非公式なメタ理論ではなくオブジェクト言語の一部である特定の計算のアイデアは、伝統的にAbadi、Cardelli、Curien、およびLévyによるものとされている。彼らのλσ計算に関する独創的な論文^[4]では、ラムダ計算の実装では置換を扱う際に非常に注意する必要があると説明されている。構造を共有するための洗練されたメカニズムがなければ、置換はサイズ爆発を引き起こす可能性があるため、実際には置換は遅延され、明示的に記録される。これにより、理論と実装の対応が非常に困難になり、実装の正確性を確立することが困難になる可能性があります。 1 つの解決策は、置換を計算の一部にすること、つまり、明示的な置換の計算を行うことです。

しかし、置換が明示的に行われると、置換の基本的な性質は意味論的性質から構文的性質に変わります。最も重要な例の1つは「置換補題」で、λxの表記では次のようになります。

• (M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (ただし x≠y かつ x は P において自由ではない)

^{メリエス[5]}による驚くべき反例は、この規則が明示的置換の元の計算でコード化された方法は強く正規化されていないことを示しています。これに続いて、明示的置換計算の構文特性間の最良の妥協点を提供しようと、多数の計算が記述されました。^{[6] [7] [8]}

• 組み合わせ論理
• 置換インスタンス