私は\x->\y->x
の中で2番目のxが最初のものに拘束されていることを知っています(私が間違っていることを修正してください)。\x->\x->x
最後のxは中間のものに拘束されています。しかし、これはアルファ等価性に関しては違いがありますか? x - > x-> x alphaは x - > y-> xと等価ですか?
アルファは\x->\y->x
に相当しますか?
私は\x->\y->x
の中で2番目のxが最初のものに拘束されていることを知っています(私が間違っていることを修正してください)。\x->\x->x
最後のxは中間のものに拘束されています。しかし、これはアルファ等価性に関しては違いがありますか? x - > x-> x alphaは x - > y-> xと等価ですか?
アルファは\x->\y->x
に相当しますか?
二つの用語t1
とt2
アルファ同等である場合、任意のコンテキストのE[.]
、E[t1]
とE[t2]
は同じ用語を減少させます。
したがって、2つの用語があり、それらを2つの異なる用語に縮小するコンテキストがある場合、それらはアルファに相当しないことがわかります。
ここでは、t1 = \x.\x.x
とt2 = \x.\y.x
があり、2つの異なる用語を適用するコンテキストをとります。 v1
とv2
、あなたが持っている:
t1 v1 v2 = (\x.\x.x) v1 v2 --> (\x.x) v2 --> v2
と
t2 v1 v2 = (\x.\y.x) v1 v2 --> (\y.v1) v2 --> v1
このようにあなたは、彼らがアルファ等価ではありません推測することができます。
あなたは本当にアルファ等価で作業したい場合は、自由変数と有界変数の理解に時間を費やし、変数バインディングの点でアルファに相当するものが何であるかを尋ねる必要があります。
私は心配する必要がないように非常に努力します。 *名前を再利用しない* – Caleth