Lambda Calculus - Formal 정리 (Reduction)

Ji·2021년 5월 27일
0

본 글은 https://jurogrammer.tistory.com/136?category=959000을 보고 정리한 글로, 영어 자료를 보면서 공부했던 나에게 한 줄기 빛을 내려주신 글쓴이 분께 다시 한 번 감사하다고 전해드리고 싶다.

Reduction

  • 말 그대로 '줄인다' 라는 의미.
  • α-conversion, β-reduction, η-reduction이 존재.

1. α-conversion

  • bound variable의 이름을 바꾸도록 하는 연산.
  • λx.x 에서 bound variable인 x를 y로 치환-> λy.y 라고 표현 가능함.

유의 사항

  • bounded variable에 정확한 룰 적용을 할 필요가 있음.
    ex) λx.y (λx.z x) : 두 번째 람다에 의해 맨 오른쪽 x가 bounded 된 상황. λx.z x의 x가 λx.z x λx에 의해 binding됨. 따라서 λx.λx.x => λy.λx.x 은 옳으나, λx.λx.x => λy.λx.y 은 틀린 표현

2. β-reduction

  • 함수의 적용. (ex) f(x) = x^2 -> f(2) = 2^2

정의

the β-reduction of (λV.M) N is M[V := N]

  • V에 N을 집어넣는다면, M에 있는 V는 N으로 치환

3. η-reduction

  • 람다 연산의 축소.
    λx.f x 와 f 를 비교해 보자.
    λx.f x 의 f 에 free variable x가 나타나지 않는다면, f 엔 x가 없음. 따라서 f라고만 표현 가능.
    -> 따라서 λx.f x 는 η-reduction에 의해 f 로 변환 가능
profile
공부방

0개의 댓글