베타 감소 : 바운드 변수를 바꿀 올바른 방법은 무엇입니까?

Question

다음과 같은 람다 식의 예가 있습니다. \x은 람다를 나타냅니다.

다음과 같은 베타 감소는 무엇입니까?

(\x.\x.(x x)) \z.z 

나의 첫번째 본능

\x.(\z.z \z.z) 

수 있도록이에 대한했을 것이다 그러나 나는이와 통화를 누군가가 두 번째 \ X가도 \z.z

로 대체 될 것이라는 의견이었다 것 그것이 실제로라는 것을 의미합니다.

\(\z.z).(\z.z \z.z) 

누군가가 올바른 접근 방식이 될 것입니다. 나는 두 번째 접근법을 정말로 이해한다고 말할 수는 없다. 변수는 항상 가장 가까운 람다 추상화에 바인딩되어 있기 때문에

Answer 1

사실, (\x.\x.(x x)) \z.z는 (\x.\y.(y y)) \z.z에 알파 것과 같습니다.

이 (\x.\x.(x x)) \z.z 수단 \x.(x x)에 베타 동일하다.

교체, 람다 추상화에 \x. 부분을 수행되지 않습니다.