람다 대수 변환

이 글은 책 The implementation of functional programing languages에서 아래 섹션을 읽고 정리한 것이다.

• 2.2.2.4 Conversion, reduction and abstraction
• 2.2.3 Alpha-conversion
• 2.2.4 Eta-conversion

베타 변환

축약된 람다 표현식에 베타 규칙($\beta$-rule)을 반대로 적용하면 람다 추상화를 얻을 수 있다.

이 작업을 베타 추상화($\beta$-abstraction)라 하고 왼쪽 화살표 '$\leftarrow$'와 함께 적는다. 베타 변환($\beta$-conversion)은 베타 축약($\beta$-reduction)이나 베타 추상화를 뜻하고 양쪽 화살표 '$\xleftrightarrow[\text{$\beta$}]{}$'로 적는다.

베타 변환을 앞으로 나올 다른 변환과 구분하기 위해서 화살표 밑에 $\beta$를 같이 적는다. 아무 글자도 적지 않은 축약 화살표 '$\rightarrow$'는 아래 중 하나를 의미한다.

• 하나 또는 둘 이상의 베타 축약
• 내장 함수의 축약

아무 글자도 적지 않은 변환 화살표 '$\leftrightarrow$'는 0개나 그 이상의 아무 종류의 변환을 의미한다. 무슨 말이야...

베타 축약과 베타 추상화를 작업(operations)으로 보기보다는 베타 변환을 두 표현식이 동치(equivalence)임을 나타내는 표현으로 볼 수 있다. 동치란 다르게 보이지만 사실은 같은 의미인 것을 말한다. 동치인지 확인하려면 두 개 이상의 규칙이 필요한데 어떤 규칙인지 알아보자.

알파 변환

다음 두 람다 추상화를 살펴보자.

두 람다 추상화는 같아야 할 것 같다. 알파 변환($\alpha$-conversion)은 람다 추상화에서 형식 인자의 이름을 바꿀 수 있게 해준다. 그래서 아래와 같은 변환이 가능하다.

알파 변환임을 나타내기 위해서 화살표에 $\alpha$를 적었다. 새로 변환한 이름은 원래 람다 추상화의 본문에서 자유 변수이면 안 된다. 알파 변환은 앞절에서 예를 들었던 이름 충돌을 제거하는데 사용한다. 알파 변환이 꼭 필요한 상황이 있다.

에타 변환

동치인지 확인하려면 변환 규칙이 하나 더 필요하다. 아래 두 표현식을 보자.

이 두 표현식에 인자를 적용했을 때 두 표현식은 완전히 같은 방식으로 동작한다. 두 표현식 모두 인자에 1을 더한다. 에타 변환($\eta$-conversion)은 두 표현식이 동치임을 보여주는 규칙이다.

에타 변환 규칙을 더 일반적으로 표현하면 아래와 같다.

$x$는 $F$에서 자유 변수가 아니어야 하고 $F$는 함수여야 한다.

$F$에서 $x$가 자유 변수가 아니어야 한다는 조건은 잘못된 변환을 방지해준다. 예를 들어 $(+\;x)$에서 $x$가 자유 변수이기 때문에 아래 두 식은 서로 에타 변환할 수 없다.

$F$가 함수여야 한다는 조건도 내장 상수를 잘못 변환하는 것을 방지해준다. 예를 들어 아래 두 식은 서로 에타 변환할 수 없다.

에타 변환을 왼쪽부터 오른쪽으로 적용하는 것을 에타 축약($\eta$-reduction)이라고 한다. 하스켈에서는 포인트 프리(Pointfree)라고 한다.

참고

• https://archive.org/details/implementationof00peyt
• https://wiki.haskell.org/Pointfree