ラムダcaculus

Question

の減少を停止するときに私は、ラムダ低減がterminates.Forたとえば、数2は

我々はベータ代入ルールを適用し、それを作り続けるべきではないのはなぜ

\xy.xxy 

として書かれているかについて混乱していますlike

\xy.(x)xy 
＝＞\ab.axy 
＝＞\b.yx 
＝＞y 

これは明らかに間違っています。しかし、私は理由を知りません。

Answer 1

トラブル置換を行うことがある場合、私はあなたが完全に拡張されたフォーム

\xy.xxy 

を使用することを推奨しますが、それは

することができ

λx. λy. (x x) y 

あるない

\xy.(x)xy 

ですη-reducedに

であり、さらに

ベータ置換は、この特定の問題では必要ではなかった低減することができない

λx. λy. (x x) y λx. (x x) λx. x x