beta reduction 띠용 ㅠㅜ

(lambda x.(lambda x.x)) z -> [x |-> z](lambda x.x) -> lambda x.x ????

(lambda x.(lambda y.x)) y ->
[ x |-> y ] (lambda y.x) -> [x |->y] (lambda z.x) ?????
-> (lambda z.y)

(lambda x.(lambda y.x y)) (lambda x.x) z ->
( [x |-> lambda x.x] (lambda y.x y)) z -> 
[ y |-> z ] (lambda x.x y) -> (lambda x.x z) -> z

힘이 듭니다…


교수님께 질문해서 얻어낸 보충 설명:

  1. 첫번째 예시의 첫번째 x 와 두번째 세번째 x 는 서로 다른 것.
    (lambda x.(lambda y.y)) z -> [x |-> z](lambda x.x) -> lambda y.y

로 바꿔도 상관없음
2. 두번째 예시에서 두 y 는 아무 상관 없음. 얘도 다른 변수로 바꿔도 됨.

변수 이름 충돌과 scope 때문에 혼란하네요. 나중에 여유 있을 때 설명해드리겠습니다

1 Like

감사합니다!! 교수님이 일부러 변수 이름 충돌 시켜서 예제 내신 것 같습니다 ㅋㅋ 좀 익숙해졌네요

1번 문제

각 lambda 는 각자의 environment를 만듭니다. 그러므로 같은 문자라도 다른 binding 을 가지죠. alpha reduction 으로 변수 충돌을 제거하면

-> (lambda x1 . (lambda x2 . x2) ) z -> [x1 := z] (lambda x2 . x2) -> (lambda x2 . x2)

2번 문제
(lambda y. x) 에서 x는 이 lambda 의 argument가 아니니 free variable 이고 y는 bound variable 이죠

-> (lambda x.(lambda y1.x)) y -> [x := y] (lambda y1.x) -> (lambda y1 . y)

bound variable 끼리 이름만 똑같으면 같은 의미니 교수님처럼 (lambda z . y) 로 바꿔도 됩니다.

3번 문제
(lambda x . x) 는 identity 라는 함수입니다. 무슨 값을 넘겨줘도 그 값을 그대로 반환하죠. 헷갈리지 않게 id 라 대신 쓰겠습니다.

-> (lambda x.(lambda y.x y)) id z

여기서도 alpha reduction 합시다.

-> (lambda x.(lambda y1.x y1)) id z
-> [x := id] (lambda y1.x y1) z
-> (lambda y1. id y1) z
-> [y1 := z] (id y1)
-> (id z)
-> z

1 Like

와우 하나도 모르겠어여. 이거 읽으려면 뭘 배워야하지용?

프로그래밍 언어 수업에서 배운 람다 칼큘러스입니다

전 피피티오만 배웠지만 람다 칼큘러스 책에서 배울거 같아요!