λ 계산법에서 β 감소를 사용하여 표현식을 평가하는 방법은 무엇입니까?

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))

우리가 거기 뭐하는거야? 내 이해에서 α 등가 규칙을 사용해야합니다.

Answer 1

베타 감소는 용어 (λx.t)가 t [x : = s]로 감소되도록 허용합니다. 문제 단계에서 x는 z, t는 zz, s는 λw.w입니다. 여기서 t [x : = s]는 zz [z : = λw.w]이며, 이는 (λw.w) (λw.w)입니다.

Answer 2

당신이 제안하는 감소는 감소 가치입니다.

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

당신은 당신의 질문에 대답하기 위해 이름

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

을 감소를 사용하여 y로 직접 줄일 수 :

(λ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)