「タイプとプログラミング言語」のセクション6.1.2では、ラムダ式の自由変数に番号を付けるために使用されるネーミングコンテキストについて説明しています。彼らが提供したスキームの例を使用すると、両方ともλx.xb、明らかに異なる用語である場合のように、 λx.xxdeBruijn表現を持ちます。λ.00これはどのように作動しますか？
2198 次
1 に答える
17
あなたが言ったように、本はn自由変数をからの数にマップする命名コンテキストを使用0しn-1ます。ただし、本の例をよく見ると、変数を表すためにこれらの数値を直接使用していないことがわかります。たとえば、のマッピングが4ではなく3であっても、として表さλw. y wれます。λ. 4 0y
ここで起こっていることは、彼が変数の入れ子の深さを数値に追加することです。つまり、自由変数vがラムダでネストされている場合、それはだけでなくdインデックスを取得します。Γ(v)+dΓ(v)
したがって、この例では、コンテキストを使用すると、ではなく、Γ {b -> 0} λx.xbとして表されます。したがって、あいまいさはありません。λ. 0 1λ. 0 0
于 2012-02-26T05:04:12.570 に答える