람다 계산법 용어를 일반 형식으로 환원

Question

이것은 숙제하기 전에 숙제하기위한 것이며, 나는 단지 지침을 찾고 있습니다. 내가 올바르게 생각하고 있는지 확인하고 싶습니다

(λx.λy.x y)(λx.x y) 
=(λx.λz.x z)(λx.x y)   α-renaming 
=(λz.(λx.x y) z) 
=(λx.x y) 

:

다음은 첫 번째 질문의 용어입니다. 오른쪽에있는 값은 매개 변수 x에 입력 한 값입니다. 맞습니까? 그러면 x의 모든 인스턴스가 오른쪽의 용어로 대체됩니다. y라는 이름을 변경하여 자유로운 y와 경계가있는 y와 어떤 혼동도 없었습니다. 이제 이해가 안되는 것은 =로 시작하는 두 번째 줄입니다. 가장 오른쪽 z가 변수 z에 대한 매개 변수로 전달됩니까? 또는 x에 전달됩니까? 어느 쪽이든 나는 대답이 같다고 생각하지만 올바른 방법을 알고 싶습니다. (λx.x) 변수 x에 대한 용어 치환됩니까 여기

는 제 2 항을 질문 때문에 괄호

((λx.λy.x y)(λx.x)) y 
=((λx.λz.x z)(λx.x)) y 
=(λz.(λx.x)z) y 
=(λx.x)y 
=(λx.x) 

있습니까? 또는 y가 x로 대체 되나요?

나는 이것이 의미가 있기를 바랍니다. 모든 도움을 미리 감사드립니다.

Answer 1

람다 계산법은 문맥 자유 문법에있다

E ::= v  Variable 
    | λ v. E Abstraction 
    | E E  Application 

여기서 함께

(λ x. B) E => B where every occurrence of x in B in substituted by E 
    λ x. E x => E if x doesn't occur free in E 

a가 자유λ b. b a을에있는 베타 - 및 ETA 환원 규칙 변수 위에 v 범위 , λ a. λ b. b a에는 없습니다. 두 축소 규칙이 적용되지 않는 표현식은 정규 서식에 있습니다.

보통 주문은 가장 왼쪽의 redexes의 감소를 우선시합니다. 적용 순서은 대체하기 전에 인수를 정규화합니다.

올바른 일반 차 베타와 두 식의 ETA-정상화 :

(λ x. (λ y. x y)) (λ a. a b) 
= (λ x. x) (λ a. a b)   Eta-reduction 
= λ a. a b      Beta-reduction 

    ((λ x. (λ y. x y)) (λ a. a)) f 
= ((λ x. x) (λ a. a)) f 
= (λ a. a) f 
= f