lambda-calculus - ラムダ計算のベータ簡約

Question

これはおそらく本当に単純なことだと思いますが、これを減らす方法を理解するのに問題があります。以下は私の方程式です。

(λx λy . y x) z

私は完全に道に迷っているので、どこから始めればよいかというアイデアが必要です。

Answer 1

そのラムダ式は構文的に正しくありません。次のように書くつもりだったと思います。

(λx.λy.y x) z 

または

(λxy.y x) z

有効なラムダ式は λx.M の形式であり、λx M ではないため、これは重要です。または、シンタックス シュガーを使用すると、λxy.M を記述できますが、λxλy.M を記述できず、この (λx.λy.yx) は混乱を招くように見えます。アプリケーションのように。

(λx.λy.y x) z私は両方を減らします(λx.λy.yx) z

1) (λx.λy.y x) z
2) (λx.λy.y x)x をλx.λy.yに適用することで還元するため、(λx.λy.y x) zに還元されます。 λy.y z 3) λy.y zz を に適用することで還元するλy.y zと、結果は z になります。

そして、あなたが(λx.λy.yx)zを意味するなら

1) (λx.λy.yx) z 2) λx.(λy.yx) z 3) 最初の抽象化に z を適用します: λy.yz 4) 結果を減らすために他に何もありません:λy.yz

ラムダ計算の定義を見て、アプリケーション、抽象化、変数の違いを理解することをお勧めします。

また、初期段階では () を使用し、常にラムダ式を拡張して記述すると、ミスが少なくなります。