ラムダ微積分：捕捉回避の再帰的定義

Question

私は型なしラムダ計算の実装をプログラミングするのに数週間を費やしました。

私は、ウィキペディアで与えられた置換の定義にうまく収まる、置換を避けるキャプチャのための再帰的な定義を定式化していると思います。

誰かが私のために正しいのかどうかを確かめることができたら、私は本当に感謝しています。なぜなら、この定義がめったに使われない理由を説明しているからです。

ウィキペディアの定義：

x[x := N] ≡ N 
y[x := N] ≡ y, if x ≠ y 
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N]) 
(λx.M)[x := N] ≡ λx.M 
(λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y, provided y ∉ FV(N) 

私の追加の定義は、キャプチャ回避を強制します

y' ∉ (FV(N) ∪ FV(M)) 
M' ≡ M[y:=y'] 

Answer 1

あなたのルールが正しい

(λy.M)[x := N] ≡ λy'.(M'[x := N]), if x ≠ y and y ∈ FV(N) 

。

フリー変数を追跡する必要があるため、頻繁には使用されません。この実装では、名前が重要な役割を果たしているのに対し、名前は決して重要ではないという意味で、直感的に直感的ではありません。

まだ操作上のセマンティクスは表示されていません。そうする場合、がNでキャプチャされているかどうかをアプリルールで確認する必要があります（(λx.M) N）。その場合は、アルファの名前を変更する必要があります。

ここで問題となるのは、本質的な1つの表現には、あまりにも多くの（無限の）表現があります。これを解決する典型的な方法の1つは、Bruijinインデックスを使用する方法、またはローカル名なしと呼ばれるハイブリッド方法です。

https://en.wikipedia.org/wiki/De_Bruijn_index

https://www.chargueraud.org/research/2009/ln/main.pdf

主な考え方は同じである：両方が一つの発現は、正確に一つの標準形を有するように、結合した式の商を取ります。