람다 대수 의미 구조

박준규·2023년 3월 21일
1

이 글은 책 The implementation of functional programming languages에서 2장 람다 대수 중 2.2.2.1 Simple examples of beta-reduction까지 읽고 정리한 것이다.

람다 대수 의미 구조

지금까지는 람다 대수의 문법 구조만 설명했다. 그런데 명색이 이름에 계산(calculus)이 들어가니까 이제 계산하는 법을 알아보자. 번역어로 람다 대수가 널리 쓰이고 있지만 원래 이름은 Lambda Calculus이다.

람다 표현식을 다른 표현식으로 바꾸는 변환 규칙(conversion rules) 세 가지를 소개할 건데 그 전에 용어 정리를 먼저 하자.

종속 변수와 자유 변수

아래와 같은 람다 표현식이 있다고 하자.

(λx.  +  x  y)  4(\lambda x.\;+\;x\;y)\;4

이 표현식을 완전히 평가하려면 yy'전역(global)' 값을 알아야 한다. xx는 함수의 형식 인자라서 xx의 '전역' 값을 알 필요는 없다. xxyy의 상태가 다르다고 할 수 있다. global의 의미가 뭔지 모르겠다. global, local scope의 그것인가?

λx\lambda x 때문에 xx종속 변수이다(occurs bound). xx는 람다 추상화를 인자에 적용할 때 44가 들어오는 '빈 자리(hole)'이다.

반면에 yy는 어느 λ\lambda에도 종속되지 않았기 때문에 자유 변수(occurs free)라고 부른다. 보통 표현식의 값은 자유 변수의 값에 달렸다고 한다.

어떤 람다 추상화가 다른 람다 표현식 안에 들어 있을 때도 그 람다 추상화에 해당하는 변수를 종속 변수라고 한다. 아래 예에서 xxyy는 종속 변수이고 zz는 자유 변수이다.

λx.  +  ((λy.  +  y  z)  7)  x\lambda x.\;+\;((\lambda y.\;+\;y\;z)\;7)\;x

'종속'이나 '자유'라는 용어는 표현식에서 변수가 어떻게 나타나는지(specific occurrences)를 표현하는 용어라는 점을 잘 봐야 한다. 왜냐하면 어떤 한 변수가 표현식에서 종속 변수이면서 동시에 자유 변수인 것처럼 보일 수 있기 때문이다. 아래 식에서 첫 번째 xx는 자유 변수인데 두 번째 xx는 종속 변수이다.

+  x  ((λx.  +  x  1)  4)+\;x\;((\lambda x.\;+\;x\;1)\;4)

하나의 변수는 종속 변수이거나 아니면 자유 변수이어야 한다. 둘 다일 수는 없다.

다음 절에서는 '자유'와 '종속'의 형식 정의(formal definition)에 대해서 다룬다.

베타 변환

람다 추상화는 함수를 나타낸다. 이 함수를 어떻게 값에 적용하는지 알아보자. 예를 들어 다음과 같은 표현식이 있다고 하자.

(λx.  +  x  1)  4(\lambda x.\;+\;x\;1)\;4

위 표현식은 아래 두 개를 같이 적은 것이다.

  • 람다 추상화 (λx.+x1)(\lambda x.\,+\,x\,1)
  • 인자 44

특정 람다 추상화를 인자 44에 적용한 함수를 나타낸다. 함수를 적용(application)하는 규칙은 다음과 같이 간단하다.

람다 추상화를 인자에 적용한 결과는 람다 추상화의 본문(body)인데 본문 중 형식 인자 자리의 변수를 인자의 값으로 바꿔 쓴 것이다.

그래서 람다 추상화 (λx.+x1)(\lambda x.\,+\,x\,1)를 인자 44에 적용한 결과는 다음과 같다.

+  4  1+\;4\;1

(+  4  1)(+\;4\;1)은 본문 (+  x  1)(+\;x\;1)에서 형식 인자 xx를 인자 값 44로 바꿔 쓴 것이다. 화살표 \rightarrow를 이용해서 표현식을 줄여쓰자.

(λx.  +  x  1)  4+  4  1(\lambda x.\;+\;x\;1)\;4\quad\rightarrow\quad+\;4\;1

이런 작업을 베타 축약(β\beta-reduction)이라고 부른다.

베타 축약 예제

형식 인자는 람다 추상화 본문에 여러 개가 있을 수 있다.

(λx.  +  x  x)  5+  5  510\begin{aligned} (\lambda x.\;+\;x\;x)\;5\quad&\rightarrow\quad+\;5\;5\\ &\rightarrow\quad10 \end{aligned}

반대로 본문에 형식 인자가 없을 수도 있다.

(λx.  3)  53(\lambda x.\;3)\;5\quad\rightarrow\quad3

이렇게 형식 인자 (xx)가 없어서 인자 (55)를 바꿔 쓸 수 없을 때는 인자를 쓰지 않고 버린다.

람다 추상화의 본문은 다른 람다 추상화에서 그대로 유지될 수도 있다.

(λx.  (λy.    y  x))  4  5(λy.  y  4)  5  5  41\begin{aligned} (\lambda x.\;(\lambda y.\;-\;y\;x))\;4\;5\quad&\rightarrow\quad(\lambda y.\;-y\;4)\;5\\ &\rightarrow\quad-\;5\;4\\ &\rightarrow\quad1 \end{aligned}

λx\lambda x 추상화 본문의 인스턴스를 만들 때 그 안에 들어 있는 λy\lambda y 추상화의 전체 본문을 통째로 복사한다. 물론 이때 xx의 값은 인자로 바꿔 쓴다. 이때 커링(currying)이 발생하는데 λx\lambda x 추상화의 적용이 그 결과로 함수(λy\lambda y 추상화)를 리턴한다. 그 결과는 (  5  4)(-\;5\;4)이다.

아래 적는 첫 번째 표현식을 두 번째 표현식처럼 줄여 쓸 수 있다.

(λx.  (λy.  E))(λx.  λy.  E)(\lambda x.\;(\lambda y.\;E))\\ (\lambda x.\;\lambda y.\;E)

함수를 인자로 넣을 수도 있다.

(λf.  f  3)  (λx.  +  x  1)(λx.  +  x  1)  3+  3  14\begin{aligned} (\lambda f.\;f\;3)\;(\lambda x.\;+\;x\;1)\quad&\rightarrow\quad(\lambda x.\;+\;x\;1)\;3\\ &\rightarrow\quad+\;3\;1\\ &\rightarrow\quad4 \end{aligned}

λf\lambda f 추상화 본문의 ffλx\lambda x 인스턴스로 바뀌었다.

참고

profile
코딩하는 물총새

0개의 댓글