37

Wikiでラムダ計算を読んでいるときに、キャプチャ回避置換という用語に出くわしました。どこからともなく定義が見つからなかったので、誰かがそれが何を意味するのか説明してもらえますか？

ありがとう

PS

私が知りたいのは、その操作をキャプチャ回避置換に伝える理由です。誰かがそれをすることができればそれは大きな助けになるでしょう

4

3 に答える 3

62

通常、ラムダ計算で選択した特定の変数名は無意味です。の関数は、またはxの関数と同じです。言い換えると：abc

（λx。（λy.yx））は（λa。（λb.ba））と同等です-toとtoの名前xを変更しても何も変更されません。ayb

このことから、任意の置換が許可されていると結論付けることができます。つまり、任意のラムダ項の任意の変数を他の変数に置き換えることができます。これはそうではありません。上記の最初の式の内側のラムダについて考えてみます。

（λy.yx）

この式では、xは「無料」です。ラムダ抽象化によって「バインド」されていません。に置き換えるyとx、式は次のようになります。

（λx.xx）

これはまったく異なる意味を持っています。両方ともx、ラムダ抽象化の引数を参照するようになりました。その最後のx（元々は「無料」でした）が「キャプチャ」されました。ラムダ抽象化によって「バインド」されます。

自由変数を誤ってキャプチャすることを回避する置換は、想像を絶するほど「キャプチャ回避置換」と呼ばれます。

さて、ラムダ計算で気にしたのが、ある変数を別の変数に置き換えることだけだったとしたら、人生はかなり退屈でしょう。より現実的には、変数をラムダ項に置き換えることです。したがって、変数をラムダ抽象化（λx.t）またはアプリケーション（xt）に置き換えることができます。どちらの場合も、同じ考慮事項が適用されます。置換を行うときは、元々フリーだった変数を誤って「キャプチャ」して、元の式の意味を変更しないようにする必要があります。

于 2012-07-04T16:24:00.890 に答える
8

変数をバインドするラムダ（または存在する場合は他のバインディングコンストラクト）の下に配置されている場合、変数はキャプチャされます。これは、置換内の自由変数が元の式内でキャプチャされることをプロセスが誤って許可することを回避するため、キャプチャ回避置換と呼ばれます。

于 2012-06-28T20:28:22.230 に答える
5

EのxをE'に置き換える（[E' / x] Eと表記）

  • 手順1.EとE'のバインドされた変数の名前を変更して、一意になるようにします
  • ステップ2.EのxをE'にテキストで置換することを、キャプチャ回避置換
    と呼びます。

例： [y（λx.x）/x]λy。（λx.x）yx

名前を変更した後：[y（λv.v）/x]λz。（λu.u）zx
置換後：λz。（λu.u）z（y（λv.v））

于 2012-06-28T06:45:39.177 に答える