lambda - ラムダ計算でβ還元を使用して式を評価するにはどうすればよいですか？

Question

次の式を評価したい：

(λx.y)((λz.zz)(λw.w))

βリダクションを使用します。

答えは次のとおりです。

(λx.y)((λz.zz)(λw.w)) ->
(λx.y)((λw.w)(λw.w)) ->
(λx.y)(λw.w) -> y

しかし、私は第2段階を理解していません：

ここから：(λx.y)((λz.zz)(λw.w))ここへ(λx.y)((λw.w)(λw.w))

私たちはそこで何をしていますか？私の理解では、α等価ルールを使用する必要があります。

score 3 · Accepted Answer

あなたが提案する削減は、値による削減です。

 (λx.y) z -> y[x/z] IF z is a value.

名前によるリダクションを使用して、直接 y にリダクションできます

 (λx.y) z -> y[x/z].

あなたの質問に答えるには：

(λx.y)((λz.zz)(λw.w)) -> (λx.y)((λw.w)(λw.w))

なぜなら

 ( (λz.zz)(λw.w) ) is not a value (as (λx.y)z is never a value.)

そして、なぜなら

  (zz)[z/(λw.w)] i.e.substitute every occurence of z with (λw.w) leads to 

  (λw.w)(λw.w)

score 3 · Accepted Answer

ベータ簡約により、項 (λx.t)s を t[x := s] に簡約できます。問題のステップでは、x は z、t は zz、s は λw.w です。したがって、ここで t[x := s] は zz[z := λw.w] であり、これは (λw.w)(λw.w) です。

2 に答える 2