lambda - ラムダ計算の削減

Question

私は最近ラムダ計算について勉強していますが、還元と代入について多くの疑問があります。アルファ還元とベータ還元とは？そして、いつ、なぜそれらが使用されるのですか?.

誰かがラムダ計算の縮約と代入に関する良いリソースを教えてくれたら素晴らしいでしょう.

score 5 · Accepted Answer

ベータ還元は、ラムダ計算内で計算に使用される主要なアプリケーションルールにすぎません。次のように、置換によって適用されます。

ラムダ項: (\xx) とその右側に値がある場合: y

次に、バインドされたすべての変数をラムダ項の (.) の右側に置き換えます。バインドされた変数は、(.) の左側の変数に一致する変数なので、この場合は x.

The reduction would be of the form:
(\x.x)y    //y gets bound to all occurences of x to the right of the period
y

y は、ラムダ式で出現するすべての x にバインドされます。これがアイデンティティ関数です。

アルファ「リダクション」は通常、アルファ等価性またはアルファ書き換え規則と呼ばれます。彼らは、式の意味を変更することなく、ラムダ項とそれにバインドされた変数の名前を変更できると述べています。

たとえば、上記の恒等関数を使用すると、ラムダ項を (\jj) のように簡単に書くことができます。次のように、アプリケーションの結果は変わりません。

(\j.j)y    //y gets bound to all occurrences of j to the right of the period
y

学習リソースについて: ウィキペディアのページはかなり詳細ですが、表記が重く、おそらく何度か読み直す必要があります。

ラムダ計算がどのように機能するかについてのより良い直感を探しているだけなら、ほとんどのコンピューターサイエンス部門にはスライドが用意されています。

1 に答える 1