4

Haskellで不純な型なしラムダ計算インタープリターを実装しています。

私は現在、「alpha-congruence」（一部の教科書では「alpha-equivalent」または「alpha-equality」とも呼ばれます）の実装に固執しています。2つのラムダ式が互いに等しいかどうかを確認できるようにしたいと思います。たとえば、インタプリタに次の式を入力すると、True（\ラムダ記号を示すために使用されます）が生成されます。

>\x.x == \y.y
True

問題は、次のラムダ式がアルファ等価と見なされるかどうかを理解することです。

>\x.xy == \y.yx
???

>\x.yxy == \z.wzw
???

私の場合\x.xy == \y.yx、答えはTrueです。これは、\x.xy => \z.zyと\y.yx => \z.zyと両方の右側が等しいためです（記号=>はアルファリダクションを示すために使用されます）。

のcaeで\x.yxy == \z.wzw私は同様に答えがであると推測しますTrue。これは、\x.yxy => \a.yay（\z.wzw => \a.waw私が思うに）どちらが等しいからです。

問題は、私の教科書のすべての定義で、2つのラムダ式が等しいと見なされるには、バインドされた変数の名前のみを変更する必要があると述べられていることです。式の自由変数についても、一律に名前を変更する必要があることについては何も述べていません。したがって、yとwは両方ともラムダ式の正しい位置にありますが、プログラムは、最初が最初を表し、2番目が2番目を表すことをどのように「認識」yしますwか。実装では、これについて一貫している必要があります。yw

つまり、エラーのないバージョンの関数を実装するにはどうすればよいでしょうisAlphaCongruentか。これが機能するために私が従う必要がある正確なルールは何ですか？

deBruijnインデックスを使用せずにこれを実行したいと思います。

4

1 に答える 1

11

あなたは誤解しています：異なる自由変数はアルファ等価ではありません。だから、、、、y /= xそして。同様に、。\w.wy /= \w.wx\x.xy /= \y.yx\x.yxy /= \z.wzwy /= w

あなたの本は、自由変数の名前を一律に変更することは許可されていないため、自由変数の名前を一律に変更できることについては何も述べていません。

（このように考えてください：私がまだとの定義をあなたに話していないなら、notあなたはそして同等であるとid期待しますか？私は確かにそうしないことを望みます！）\x. not x\x. id x

于 2012-05-28T14:56:29.360 に答える