논리적인 말?

언제 어떤 문장이 "논리적이다"고 할 수 있을까? 일상적으로는 우리는 이를 남용해 의미가 있어 보이는 것을 "논리적이다"라고 수식하고는 한다. 그러나 필자는 이 남용이 "논리적"이라는 표현을 너무 가볍게 보고 있는 것이라 말하겠다. 어떤 것이 진정 논리적이기 위해서는 의미가 있는 것은 물론이거니와 최소한 다음의 두 조건을 더 만족해야한다.

1. 몇몇 가정으로부터 그것을 증명해야 한다.
2. 증명에 쓰인 체계가 모순을 보일 수 없어야 한다.

이 글에서는 이 중 1 번을 중점으로 설명하여 "좋은 가정 아래" 어떤 것이 논리적임을 증명하는 두 방법에 대해 다루어 볼 것이다. 두 방법 중 하나는 함수형 언어로 쓰인 프로그램과 유사한 구조를 가지며 나머지 하나는 일반적인 함수형 언어와는 상이한 구조를 가진다. 이 중 두번째 방법에 대해서는 (약간의 부정행위를 하면…\ldots) 2 번을 간단하게 보일 수 있기 때문에 이 또한 다룰 것이다.

논리적 증명의 대상

어떻게 어떤 것이 논리적이라는 걸 증명할 수 있는 지에 설명하기에 앞서 짚고 넘어가야 할 매우 중요한 요소가 하나 있다. 바로

는 것이다. 이 글에서는 철학적인 복잡도를 덜기 위해 이 대상을 다음과 같이 단순히 설명할 것이다.

논리적일 수 있는 대상은 명제(proposition)에 대한 판단(judgment)이다.

여기서 명제는 다음과 같이 정의되는 대상이다.

1. 단위 명제(Atomic Proposition) AA는 명제이다.
2. 참 명제(True Proposition) ⊤\top은 명제이다.
3. 거짓 명제(False Proposition) ⊥\bot은 명제이다.
4. 명제 PP와 QQ가 있을 때, P∧QP \land Q(PP 그리고 QQ)는 명제이다.
5. 명제 PP와 QQ가 있을 때, P∨QP \lor Q(PP 또는 QQ)는 명제이다.
6. 명제 PP와 QQ가 있을 때, P→QP \to Q(PP라면 QQ)는 명제이다.

여기서 단위 명제란 우리가 선택한, 더이상 세밀하게 분석하지 않을 논리적인 최소 단위이다. 예를 들어 1+1=21 + 1 = 2와 0+2=30 + 2 = 3을 단위 명제로 두었을 때^[1] 다음과 같은 것들이 명제이다.

• ⊤\top
• 1+1=21 + 1 = 2
• (1+1=2)∧(0+2=3)(1 + 1 = 2) \land (0 + 2 = 3)
• (0+2=3)→⊥(0 + 2 = 3) \to \bot
• ⊤→⊥\top \to \bot

그렇다면 판단이란 무엇인가? 우리가 명제에 가지는 논리적 태도이다. 이 글에서는 다음과 같은 판단만을 이야기 할 것이다.

P trueP\ \texttt{true}, 즉 명제 PP가 참이다.

이를 "진리 판단"("truth judgment")이라고 한다. 좀 더 엄밀히는 다음과 같이 가정을 포함한 판단에 대해 다룰 것이다.

• Γ⊢P true\Gamma \vdash P\ \texttt{true}

이 판단은 어떤 진리 판단의 나열 Γ\Gamma을 가정했을 때 명제 PP가 참이라고 말하는 판단이다. 이를 "가정적 판단"("hypothetical judgement")이라고 한다. 또한 여기서 Γ\Gamma를 "가정"("hypothesis") 혹은 "전건"("前件", "antecedent")이라고 하고, P trueP\ \texttt{true}를 "귀결("consequent") 혹은 "후건"("後件", "succedent")이라고 한다. 요약하자면 이 절의 핵심 질문

에 대한 답은 다음과 같다.

진짜 논리적이 되는 방법 1 - 자연 연역(Natural Deduction)

이제 어떤 가정적 판단이 논리적인지 증명하는 한 방법에 대해서 알아보자. 우선 PP가 참이라는 판단이 가정 중 하나라면 당연히 그 가정 아래에서는 PP가 참이라고 판단할 수 있을 것이다. 이를 간략하게 표현한 규칙(rule)이

이다. 이 규칙 표현은 줄 위의 것들을 전제(premise)로 줄 밑의 결론(conclusion)을 추론(infer)해 낼 수 있음을 말한다. 전제에 쓰여있는 P true∈ΓP\ \texttt{true} \in \Gamma는 P trueP\ \texttt{true}가 가정의 나열 Γ\Gamma에 포함되어 있음을 말한다. 또한 줄 옆에 써져있는 "hyp"는 이 추론 규칙(inference rule)의 이름으로서 가정(hypothesis)을 사용한다는 것을 나타낸다.

이런 추론 규칙을 명제를 만드는 각각의 방법에 대해 정의할 수 있다. 참 명제 ⊤\top에 대해서는

라는 규칙을 줄 수 있다. 이 규칙 I⊤\text{I}\top은 어떤 Γ\Gamma를 가정하든 참 명제는 참이라고 판단할 수 있다는 규칙이다. 여기서 이름의 I\text{I}는 참 명제를 결론에 소개(Introduce)하는 규칙이라는 뜻이다. 대칭적으로 거짓 명제에 대해서는

라는 규칙을 줄 수 있다. 이 규칙 E⊥\text{E}\bot은 어떤 가정들 Γ\Gamma로 부터 거짓 명제가 참이라고 판단했다면 그 가정들 아래에서는 아무 명제나 참이라고 판단할 수 있다는 규칙이다^[2]. 여기서 이름의 E\text{E}는 우리가 거짓 명제가 참임을 결론으로 가지는 전제에 도달했을 때 그 결론을 제거(Eliminate)하여 다른 결론에 도달할 수 있도록 하는 규칙이라는 뜻이다.

⊤\top과 ⊥\bot을 제외한 명제를 만드는 방법들은 이 두 종류의 규칙(I\text{I} 규칙과 E\text{E} 규칙)을 모두 가진다. P∧QP \land Q의 경우는 다음과 같다.

I∧\text{I}\land는 Γ\Gamma를 가정하여 PP와 QQ 각각이 참이라 판단했다면 같은 가정에서 P∧QP \land Q도 참이라고 판단할 수 있다는 규칙이다. 반대로 E∧\text{E}\land는 Γ\Gamma를 가정하여 P∧QP \land Q이 참이라 판단했고 Γ\Gamma에 더해 P trueP\ \text{true}와 Q trueQ\ \text{true}를 가정했을 때 RR이라는 명제가 참이라고 판단할 수 있다면 Γ\Gamma만 가정하고도 RR이 참이라고 판단할 수 있다는 뜻이다. P∨QP \lor Q와 P→QP \to Q를 위한 규칙도 나열하면 다음과 같다.

여기서 I∨1\text{I}\lor_1과 I∨2\text{I}\lor_2는 PP나 QQ 중 하나가 참이라고 판단했다면 P∨QP \lor Q가 참이라고 판단할 수 있다는 규칙이며 E∨\text{E}\lor는 P∨QP \lor Q가 참이라고 판단할 수 있고 PP가 참이라고 가정하든 QQ가 참이라고 가정하든 RR이 참이라고 판단할 수 있다면 그 가정 없이 RR이 참이라고 판단할 수 있다는 규칙이다. I→\text{I}\to는 PP가 참임을 가정해서 QQ가 참이라고 판단할 수 있다면 P→QP \to Q 또한 참이라고 판단할 수 있다는 규칙이며 E→\text{E}\to는 P→QP \to Q가 참이라고 판단할 수 있고 PP가 참이라고 판단할 수 있다면 QQ가 참이라고 판단할 수 있다는 규칙이다. 이렇게 소개 규칙과 제거 규칙의 쌍으로 논리적 증명을 하는 방식을 "자연 연역"("Natural Deduction")이라고 한다.

자연 연역으로 단순한 논리적 증명을 하는 방법의 예시를 들어보겠다. 어떤 단위 명제 AA, BB, CC에 대해서 A→BA \to B와 B→CB \to C가 참이라고 판단했다면 A→CA \to C 또한 참이라 판단할 수 있다. 이 증명은 다음과 같다. 우선 A→BA \to B 그리고 B→CB \to C와 AA가 참이라고 판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.

이를 써서 다음과 같이 증명을 끝낼 수 있다.

따라서 논리적으로 A→BA \to B 그리고 B→CB \to C가 참임을 가정했을 때 A→CA \to C가 참이라고 판단할 수 있다.

자연 연역과 함수형 언어

혹자는 위 규칙들에서 미묘한 친숙함을 발견했을지도 모른다. 이를 좀 더 구체적으로 살펴보기 위해 →\to의 규칙들을 다시 살펴보자.

여기에 약간의 조작을 가해보자. 우선 Γ\Gamma를 단순한 판단의 나열로 취급하는 대신 이름 붙은 판단들로 취급하자. 예를 들어 위의 P trueP\ \texttt{true} 라는 판단에 xx라는 이름을 붙이면 다음과 같은 규칙을 얻는다.

더욱이 각각의 규칙들에 지금까지의 증명을 나타내는 항들을 더해보도록 하겠다. 예를 들어 I→\text{I}\to 규칙에서 Γ,x:P true⊢Q true\Gamma, x {:} P\ \texttt{true} \vdash Q\ \texttt{true}가 어떤 항 MM으로 나타내지는 증명이라면 Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}의 증명은 fun (x:P)⇒M\mathtt{fun}\ (x \mathbin{:} P) \Rightarrow M이라는 항으로 나타내도록 하자. 마찬가지로 E→\text{E}\to 규칙에서 Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}가 MM, Γ⊢P true\Gamma \vdash P\ \texttt{true}가 NN이라는 항으로 나타내진다면 Γ⊢Q true\Gamma \vdash Q\ \texttt{true}의 증명은 M NM\ N으로 나타내도록 하자. 이 항들을 판단에 끼워넣으면 다음과 같이 규칙을 바꿔 쓸 수 있다.

이는 (단순한) 함수형 언어의 형 검사 규칙과 동일하다! 함수 fun (x : P) => M이 형 P -> Q를 가지는지 검사하고 싶을 때는 x : P를 가정한 뒤 M이 형 Q를 가지는지 검사하면 된다. 또한 함수 M을 인자 N에 적용하는 것이 형 Q를 가지는지 알고 싶다면 함수 M이 형 P -> Q를 가질 때 인자 N이 형 P를 가지는지 검사하면 된다. 마찬가지 변화를 다음과 같이 모든 추론 규칙들에 적용할 수 있다.

⊤\top은 단위(unit) 자료형에 대응되며 ⊥\bot은 빈 자료형에 대응되고 P∧QP \land Q는 P 형과 Q 형의 쌍(pair) 자료형에 대응된다. 같은 방식으로 P∨QP \lor Q는 P 형과 Q 형의 합(sum) 자료형^[3]에 대응된다. 항에서부터 각각의 추론 규칙이 (I\texttt{I} 규칙의 경우) 각 자료형의 생성자(constructor)나 (E\texttt{E} 규칙의 경우) 패턴 맞추기(pattern matching)의 형 검사 규칙에 대응된다는 것을 볼 수 있을 것이다. 이를 처음 구체화시킨 두 사람의 이름을 따 이 대응을 "커리-하워드 대응"("Curry-Howard correspondence")이라고 부른다. 이 대응이 발견됨으로써 논리적인 사고와 프로그래밍 언어의 이해 간에 중요한 연결고리가 생겼고 이는 현재에도 프로그래밍 언어의 발전과 논리학의 발전 양측에 모두 지대한 영향을 끼치고 있다.

이 대응을 따랐을 때 어떤 판단을 증명한다는 것은 그 판단의 형을 가지는 프로그램(program)을 짜는 것과 동일하다. 이를 보다 구체적으로 이해하기 위해 앞서의 예시 증명을 다시 반복해보자. 증명의 너비를 줄이기 위해 Γ\Gamma를 x:A→B true,y:B→C true,z:A truex{:}A \to B\ \texttt{true},\allowbreak y{:}B \to C\ \texttt{true}\allowbreak, z{:}A\ \texttt{true} 대신 사용하겠다.

즉 함수 x : A -> B와 인자 z : A가 있을 때 함수 적용 x z이 B trueB\ \texttt{true}의 증명이다. 이어서,

따라서 fun (z : A) => y (x z)가 x : A -> B와 y : B -> C가 주어졌을 때 A→C trueA \to C\ \texttt{true}의 증명이다.

지금까지 자연 연역에 대해서 알아보았다. 자연 연역은 함수형 언어를 쓰는 사람들에게는 어찌보면 매우 친숙할 수 있는 증명 방식이다. 그러나 자연 연역을 사용했을 때 거짓을 증명할 수 없다는 것을 보이는 것은 쉽지 않다. 자연 연역을 처음 도입한 게르하르트 겐첸(Gerhard Gentzen)은 같은 논문에서 거짓을 증명할 수 없다는 것을 보다 쉽게 보일 수 있는 다른 방식 또한 소개하였는데, 그것이 바로 논건 대수(論件 代數, Sequent Calculus)^[4]이다.

진짜 논리적이 되는 방법 2 - 논건 대수(論件 代數, Sequent Calculus)

논건 대수 또한 명제의 진리에 대한 가정적 판단을 추론 규칙을 통해 이끌어낸다는 점은 자연 연역과 동일하다. 자연 연역과 논건 대수의 가장 큰 차이점은 명제를 만드는 각 방법에게 어떤 식으로 추론 규칙을 부여하는지에 있다. 자연 연역에서는 소개 규칙(I\text{I} 규칙)과 제거 규칙(E\text{E} 규칙)이라는 분류를 통해 ∧\land, ∨\lor, …\ldots에 추론 규칙을 부여했다. 논건 대수의 접근법은 이와는 살짝 다르다. 예를 들어 논건 대수에서의 P∧QP \land Q의 규칙에 대해 살펴보자.

차이점을 눈치챘는가? 크게 두 차이점이 있다.

1. 규칙의 이름이 다르다. 😅
2. E∧\text{E}\land을 대체하는 L∧\text{L}\land의 꼴이 다르다.

먼저 이름의 차이를 설명하고 넘어가자. 자연 연역의 경우 I∧\text{I}\land 규칙은 ∧\land를 소개(introduce)하는 규칙, E∧\text{E}\land 규칙은 ∧\land를 제거(eliminate)하는 규칙이었다. 반면에 논건 대수의 R∧\text{R}\land 규칙은 ∧\land를 오른쪽(Right side)에 소개하는 규칙이고 L∧\text{L}\land 규칙은 ∧\land를 왼쪽(Left side)에 소개하는 규칙이다. E∧\text{E}\land와 L∧\text{L}\land의 꼴의 차이는 이 접근법의 차이에서부터 자연스럽게 따라나온 것이다.

명제를 만드는 다른 방법들에 있어서도 논건 대수의 방식을 따라서 추론 규칙을 마련해 줄 수 있다.

그리고 논건 대수가 자연 연역과 동등함을 (비교적) 쉽게 보이기 위해서는 명제를 만드는 각 방식의 R\text{R}과 L\text{L} 규칙에 더해 다음의 두 규칙을 추가해야한다.

여기서 init\text{init} 규칙은 자연 연역에서의 hyp\text{hyp} 규칙과 같은 꼴이다. 반면에 cut\text{cut} 규칙은 직접적으로 비교할만한 자연 연역에서의 규칙이 존재하지 않는데, 이는 논건 대수가 자연 연역과 전혀 다른 방식으로 증명을 전개하기 때문이다. 자연 연역에서는 예를 들어 I∧\text{I}\land 규칙으로 만들어진 P∧QP \land Q가 참이라는 판단을 바로 E∧\text{E}\land에 사용할 수 있었다. 함수형 언어로 말하자면

case (M, N) of
  (x, y) => L

같은 꼴의 사용이 가능했다. 그러나 논건 대수에서는 R∧\text{R}\land 규칙은 가정적 판단의 (오른쪽) 후건에, L∧\text{L}\land 규칙은 가정적 판단의 (왼쪽) 전건에 ∧\land를 새로 만들어낼 뿐이고 두 규칙이 상호작용할 수 있는 방법이 없다. 이 공백을 해결해주는 규칙, 즉 자연 연역의 I\texttt{I}/E\texttt{E} 규칙 쌍의 상호작용에 의한 증명을 논건 대수에서도 표현할 수 있게 해주는 규칙이 바로 cut\text{cut} 규칙이다.

그런데 이 상호작용은 과연 필요한 것인가? 위의 함수형 언어를 통한 예시에서 보다 분명히 볼 수 있는 것은 예시의 I∧\text{I}\land와 E∧\text{E}\land 규칙의 연달은 사용이 사실은 불필요하다는 점이다. 이는 자연 연역에서는 저런 식의 증명 대신 L에서 x가 등장하는 자리에 M을 치환해넣고, y가 등장하는 자리에 N을 치환해넣은 증명 또한 가능하기 때문이다. 이런 상호작용의 불필요성에 대한 대한 자연 연역에서의 직관을 이에 대응되는 논건 대수의 cut\text{cut} 규칙에 대해서 구체화한 것이 바로 다음의 cut\text{cut} 제거 정리이다.

cut\text{cut} 제거 정리의 의의는 단순히 필요없는 규칙을 제거하는 정도에 멈추지 않는다. cut\text{cut}을 제거하고 나면 논건 대수에서 가정 없이는 거짓을 증명하지 못한다는 것이 자명해지기 때문이다.

증명은 다음의 네 문장이면 충분하다.

1. 귀결이 ⊥ true\bot\ \texttt{true}인 R\text{R} 규칙이 존재하지 않기 때문에 어떤 R\text{R} 규칙도 쓸 수 없다.
2. 가정이 없기 때문에 어떤 L\text{L} 규칙도 쓸 수 없다.
3. 마찬가지로 가정이 없기 때문에 init\text{init} 규칙을 쓸 수 없다.
4. 따라서 어떤 규칙도 판단 ⊢⊥ true\vdash \bot\ \texttt{true}을 결론으로 주지 않는다.

앞서 이 글의 서두에서 논건 대수의 일관성을 보이기 위해 "약간의 부정행위"를 저지를 것이라고 말했다. 오해가 없도록 명시하자면 위의 증명은 cut\text{cut}을 제거한 논건 대수에 있어서는 문제가 없다. 부정행위라고 부를 만한 부분은 바로 cut\text{cut} 제거 정리의 증명이 더 어렵다는 점이다. 이 증명은 단순화하기 쉽지 않기 때문에 글에서 직접적으로 다루지는 않을 것이고, 이것이 바로 서두에서 언급한 "부정행위"이다. 다만 이 어려운 증명도 수학적 귀납법(Induction) 이상의 지식은 필요로 하지 않기 때문에, 시도해보고자 하는 독자가 있다면 직접 시도해 볼 수 있을 것이다^[5].

논건 대수의 소개를 앞서의 예시 증명을 논건 대수에서 반복하는 것으로 마치도록 하자. 우선 A→BA \to B와 AA가 참이라고 판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.

이를 써서 다음과 같이 증명을 끝낼 수 있다.

앞서의 자연 연역 증명의 구조가 크게 다름에 주의해서 논건 대수 증명의 구조를 이해해보도록 하자. 앞서의 자연 연역 증명은

의 구조를 가지고 있다. 즉 결론에 I\texttt{I} 규칙을 적용하고 어떤 가정에 E\texttt{E} 규칙을 적용해서 이 둘이 만나는 지점을 찾는 것이 증명의 구조이다. 이와는 다르게 논건 대수의 증명은

와 같이 (여러 개의) init\texttt{init} 규칙에서 시작해서 L\texttt{L} 규칙으로 가정, R\texttt{R} 규칙으로 귀결을 변경해 결론에 도달할 때까지 차례로 내려오는 구조를 가진다. 이런 구조의 차이가 바로 (자연 연역의) hyp\texttt{hyp} 규칙과 (논건 대수의) init\texttt{init} 규칙이 (같은 꼴임에도 불구하고) 다른 이름을 가지게 된 이유이자 논건 대수의 init\texttt{init} 규칙이 시작점(initial point)에 해당하는 이름을 가지게 된 이유이다.

논건 대수의 항

논건 대수를 좀 더 컴퓨터 공학적으로 이해할 수 있을까? 이를 위해 자연 연역의 경우와 마찬가지로 논건 대수에도 증명에 커리-하워드 대응을 통해 항을 주려고 시도할 수 있다. 그러나 앞서 언급한 것처럼 논건 대수 증명은 자연 연역의 증명, 그러니까 함수형 언어와 구조가 크게 다르다. 따라서 원본 그대로의 논건 대수에 주는 항은 상대적으로 복잡하고 다양한 개념들(생산자, 소비자, 소비자를 생산자로 바꾸기, 생산자와 소비자가 거래하게 하기, …\ldots)을 요구하고, 결과적으로 이는 컴퓨터 공학적인 직관성이 떨어지는 복잡한 항을 만들어 내게 된다. 이어질 2 편에서는 논건 대수에 약간의 변형을 가하면 직관적이고 쉽게 이해가 가능한 항을 줄 수 있으며, 항이 뜻하는 바가 저수준(low-level) 자료 표현(data representation)과 자연스럽게 연결될 수 있음을 설명할 것이다.

마치며

2 편의 "논리와 저수준 자료표현" 연작 중 1 편인 이 글에서는 논리적 증명을 하는 두 방법과 커리-하워드 대응에 대해서 설명했다. 1 편의 내용은 말하자면 2 편의 바탕 및 서두 역할을 하고 있다. 이 내용들이 2 편에서 다룰 본격적인 논리와 자료 표현의 관계에 대해 흥미를 불러일으켰기를 바라며 이만 마치도록 하겠다.

---

1. 이 중 두번째 단위 명제는 일반적인 자연수 체계에서 거짓이나, 명제의 정의 자체는 명제가 참인지 거짓인지에 대해 논하지 않는다는 것을 강조하기 위해 단위 명제에 포함하였다. ↩︎

2. 거짓도 참이라면 대체 무엇이 참이 아니겠는가? ↩︎

3. 이는 Rust나 OCaml의 Result 형 혹은 Haskell의 Either형과 같은 형이다. ↩︎

4. 전건(前件, antecedent)과 후건(後件, succedent)을 개별적으로 다룰 수 있다는 의미에서 "Sequent Calculus"를 논건 대수(論件 代數)라고 번역하였다. 보다 일반적으로 "시퀀트 대수"라는 표현이 쓰이나, 이는 "시퀀트"가 의미하는 바가 "논리에서 다루는 물건/사건/…\ldots"이라는 표현보다 직관성이 떨어진다고 보아 재번역을 하였다. ↩︎

5. 증명에 대한 구체적인 질문이 있다면 답글을 남겨주기를 바란다. ↩︎

함수형 언어(Functional Language)의 핵심

함수형 언어가 점점 많은 매체에 노출되고, 더 많은 언어들이 함수형 언어의 특징을 하나 둘 받아들이고 있다. 함수형 언어, 적어도 그 특징이 점점 대세가 되고 있다는 이야기이다. 하지만, 함수형 언어가 대체 무엇이란 말인가? 무엇인지도 모르는 것이 대세가 된다고 할 수는 없지 않은가?

함수형 언어란 아주 단순히 말해서 함수가 표현식^[1]인 언어를 말한다. 다른 말로는 함수가 값이기 때문에 다른 함수를 호출해서 함수를 얻어내거나 함수의 인자로 함수를 넘길 수 있는 언어를 말한다. 그렇다면 이 단순화된 핵심만을 포함하는 언어로 함수형 언어의 핵심을 이해할 수 있지 않을까? 이게 바로 람다 대수(Lambda Calculus)의 역할이다.^[2]

람다 대수는 딱 세 종류의 표현식만을 가지고 있다.

1. 변수 (xx, yy, …\ldots)
2. 매개변수 xx에 인자를 받아 한 표현식 MM(함수의 몸체)을 계산하는 함수 (λx→M\lambda x\to M)
3. 어떤 표현식 LL의 결과 함수를 인자 NN으로 호출 (L NL\ N)

이후의 설명에서는 MM 과 NN, 그리고 LL이라는 이름을 임의의 표현식을 나타내기 위해 사용할 것이다. 람다 대수가 어떤 것들을 표현할 수 있는가? 앞에서 말했듯이 람다 대수는 함수의 인자와 함수 호출의 결과가 모두 함수인 표현식을 포함한다. 예를 들어 λx→(λy→y)\lambda x \to (\lambda y \to y) 는 매개변수 xx에 인자를 받아 함수 λy→y\lambda y \to y를 되돌려주는 함수이고, λx→(x (λy→y))\lambda x \to (x\ (\lambda y \to y))는 매개변수 xx에 함수인 인자를 받아 그 함수를 (λy→y\lambda y \to y를 인자로 사용하여) 호출하는 함수이다.

람다 대수(Lambda Calculus)의 평가(Evaluation)

이제 문제는

그래서 람다 대수의 표현식이 하는 일이 뭔데?

이다. 위의 표현식에 대한 소개는 산수로 말하자면 x+yx + y와 같이 연산자(++)와 연산항(xx와 yy)로부터 얻어지는 문법만을 설명하고 있고, 3+53 + 5와 같은 구체적인 표현식을 계산해서 88이라는 결과 값을 내놓는 방식을 설명하고 있지 않다. 이런 표현식으로부터 값을 얻어내는 것을 언어의 "평가 절차"("Evaluation Procedure")라고 한다. 람다 대수의 평가 절차를 설명하는 것은 어렵지 않다. 적어도 표면적으로는 말이다.

• 함수는 이미 값이다.
• 함수 λx→M\lambda x \to M을 NN으로 호출하면 MM에 등장하는 모든 xx을 NN으로 치환(Substitute)하고 결과 표현식의 평가를 계속한다.

이는 겉으로 보기에는 말이 되는 설명처럼 보인다. 하지만 이 설명을 실제로 해석기(Interpreter)로 구현하려고 시도한다면 이 설명이 사실 여러 세부사항을 무시하고 있다는 점을 깨닫게 될 것이다.

1. 함수 호출 L NL\ N에서 LL이 (아직) λx→M\lambda x \to M 꼴이 아닐 때는 어떻게 해야하지?
2. 함수 호출 (λx→M) N(\lambda x \to M)\ N에서 NN을 먼저 평가하는 게 낫지 않나? xx가 MM에 여러번 등장한다면 NN을 여러번 평가해야 할텐데?

첫번째 문제는 비교적 간단히 해결할 수 있다. LL을 먼저 평가해서 λx→M\lambda x \to M 꼴의 결과 값을 얻어낸 뒤에 호출을 실행하면 되기 때문이다. 반면에 두번째 질문은 좀 더 미묘한 문제를 가지고 있다. 함수 호출의 평가에서 발생하는 이 문제에 구체적인 답을 하기 위해서는 값에 의한 호출(Call-By-Value, CBV)와 이름에 의한 호출(Call-By-Name, CBN)이 무엇인지 이해해야 한다.

값에 의한 호출(Call-By-Value)? 이름에 의한 호출(Call-By-Name)?

앞에서 말한 함수 호출에서부터 발생하는 문제는 사실 함수형 언어에서만 발생하는 문제는 아니다. C와 같은 명령형 언어에서도 함수를 호출할 때 인자를 먼저 평가해야하는지를 결정해야하기 때문이다. 즉 이 문제는 함수를 가지고 있고 함수를 호출해야하는 모든 언어들이 가지고 있는 문제이다.

그렇다면 이 일반적인 문제를 어떻게 해결하는가? 대부분의 언어가 취하는 가장 대표적인 방식은 "값에 의한 호출"("Call-By-Value", "CBV")이라고 한다. 이 함수 호출 평가 절차에서는 함수의 몸체에 인자를 치환하기 전에^[3] 인자를 먼저 평가한다. 이 방식을 사용하면 인자를 여러번 평가해야하는 상황을 피할 수 있다.

또 다른 방식은 "이름에 의한 호출"("Call-By-Name", "CBN")이라고 한다. 이 방식에서는 함수의 몸체에 인자를 우선 치환한 후 몸체를 평가한다. 몇몇 언어의 매크로(Macro)와 같은 기능이 이 방식을 사용한다. 얼핏 보기에는 CBN은 장점이 없어보인다. 그러나 함수가 인자를 사용하지 않을 경우는 CBN이 장점을 가진다는 것을 볼 수 있다. 극단적으로 평가가 종료되지 않는 표현식(Non-terminating expression)이 있다면^[4] CBV는 종료하지 않고 CBN만이 종료하는 경우가 있음을 다음 예시를 통해 살펴보자. 표현식 (λx→(λy→y)) N(\lambda x \to (\lambda y \to y))\ N이 있다고 할 때, NN이 평가가 종료되지 않는 표현식이라고 하자. 이 경우 CBV를 따른다면 종료하지 않는 NN 평가를 먼저 수행하느라 이 표현식의 값을 얻어낼 수 없지만, CBN을 따른다면 λy→y\lambda y \to y라는 값을 손쉽게 얻어낼 수 있다. 바로 이런 상황 때문에

CBN은 CBV보다 일반적으로 더 많은 표현식들을 평가할 수 있다

고 말한다.

모호한 선택을 피하는 방법

두 방식의 장점을 모두 가질 수는 없을까? 다시 말해서, 어떤 상황에서는 이름에 의한 호출을 사용하고, 어떤 상황에서는 값에 의한 호출을 사용할 수 없을까? 이 질문에 답한 수많은 선구자들 가운데 폴 블레인 레비(Paul Blain Levy)가 내놓은 답인 "값 밀기에 의한 호출"("Call-By-Push-Value", "CBPV")은 함수형 언어의 평가를 기계 수준(Machine level)에서 이해하는데에 있어 강력한 도구를 제공한다. CBPV는 우선 "계산"("Computation")과 "값"("Value")을 구분한다.

• 계산 MM, NN, LL, …\ldots = 함수 λx→M\lambda x \to M 또는 함수 호출 L VL\ V
• 값 VV, UU, WW, …\ldots = 변수 xx

잠깐, 앞서서 함수형 언어에서 함수는 값이라고 하지 않았던가? 이는 값 밀기에 의한 호출에서 함수와 함수 호출을 종전과 전혀 다르게 이해하기 때문이다. 함수 λx→M\lambda x \to M는 스택(Stack)에서 값을 빼내어(Pop) xx라는 이름을 붙인 후 MM을 평가하는 것이고, 함수 호출 L VL\ V는 스택에 값 VV를 밀어넣고(Push)^[5] LL을 평가하는 것이다. 따라서 함수 λx→M\lambda x \to M는 평가의 결과가 아닌 추가적인 평가가 가능한 표현식이 된다. 이 구분을 간결하게 설명하는 것이 다음의 CBPV 표어이다.

값은 "~인 것"이다. 계산은 "~하는 것"이다.

그렇지만 함수형 언어이기 위해서는 함수를 값으로 취급할 수 있어야 한다고 했지 않은가? 그렇다. 이를 위해 CBPV는

계산을 강제한다면(force\mathbf{force}) 계산 MM를 하는 지연된 계산인 값 thunk(M)\mathbf{thunk}(M)

을 추가로 제공한다. 이 둘 (force(V)\mathbf{force}(V)와 thunk(M)\mathbf{thunk}(M))을 다음과 같이 문법에 추가할 수 있다.

• 계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V)
• 값 = xx 또는 thunk(M)\mathbf{thunk}(M)

CBPV를 완성하기 위해 필요한 마지막 조각은 계산을 끝내는 법이다. 현재까지 설명한 λx→M\lambda x \to M와 L VL\ V 그리고 force(V)\mathbf{force}(V) 는 모두 다음 계산을 이어서 하는 표현식이고, 계산을 끝내는 방법을 제공하지는 않는다. 예를 들어 λx→M\lambda x \to M의 평가는 스택에서 값을 빼내고 계산 MM의 평가를 이어한다. 그렇다면 계산의 끝은 무엇인가? 결과 값을 제공하는 것이다. 이를 위해 return(V)\mathbf{return}(V)를 계산에 추가하고, 이 결과 값을 사용할 수 있도록 M to x→NM\ \mathbf{to}\ x \to N (계산 MM을 평가한 결과 값을 xx라고 할 때 계산 NN을 평가하는 계산) 또한 계산에 추가하면 다음의 완성된 CBPV를 얻는다.

• 계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V) 또는 return(V)\mathbf{return}(V) 또는 M to x→NM\ \mathtt{\mathbf{to}}\ x \to N
• 값 = xx 또는 thunk(M)\mathbf{thunk}(M)

이제 CBPV를 얻었으니 원래의 목표로 돌아가보자. 어떻게 CBV 호출과 CBN 호출을 CBPV로 설명할 수 있을까?

• CBV 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를 return(thunk(λx→M))\mathbf{return}{(\mathbf{thunk}(\lambda x \to M))}과 L to x→N to y→force(x) yL\ \mathbf{to}\ x \to N\ \mathbf{to}\ y \to \mathbf{force}(x)\ y로 표현할 수 있다. 즉, CBPV의 관점에서 CBV의 함수는 지연된 원래 계산 λx→M\lambda x \to M을 값으로 되돌려주는 계산으로 이해할 수 있고, 함수 호출 L NL\ N은 함수 부분 LL을 먼저 평가하고 NN을 평가한 뒤 NN의 계산 결과 yy를 스택에 밀어넣고 지연된 계산인 함수 부분 xx의 계산을 강제하는(force(x)\mathbf{force}(x)) 것으로 이해할 수 있다.
• CBN 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를 λx→M\lambda x \to M(단, 변수 xx의 모든 사용을 force(x)\mathbf{force}(x)로 치환함)과 L thunk(N)L\ \mathbf{thunk}(N)로 표현할 수 있다. 즉, CBPV의 관점에서 함수 호출은 L NL\ N은 지연된 NN을 스택에 밀어넣은 뒤 LL의 계산을 이어가는 것으로 볼 수 있다. 이 지연된 NN은 이후에 스택에서 빼내어져 어떤 이름 xx가 붙은 뒤, 이 변수가 사용될 때에야 비로소 계산된다.

다소 설명이 복잡할 수 있으나, 단순하게 말해서 CBPV는 CBV에 따른 상세한 평가 순서와 CBN 따른 상세한 평가 순서를 세부적으로 설명할 수 있는 충분한 기능을 모두 갖추고 있으며, 이를 통해 CBV 함수 호출과 CBN 함수 호출을 모두 설명할 수 있다는 이야기이다.

기계 수준(Machine level)에서의 Call-By-Push-Value의 장점

앞에서는 CBPV가 CBV와 CBN를 모두 설명할 수 있음을 다뤘다. 그러나 CBPV는 프로그래머(Programmer)가 직접 사용하기에는 과도하게 자세한 세부사항들을 포함하고 있기에, 프로그래머가 직접 CBPV를 써서 CBV와 CBN의 구분을 조율하기에는 적합하지 않다. 그렇다면 어느 수준에서 CBV와 CBN을 혼합해 사용할 때 도움을 줄 수 있을까? 바로 람다 대수를 기계 수준으로 컴파일(Compile)할 때이다. 이때는 CBPV가 가진 자세한 세부사항의 표현력이 굉장히 유용해진다.

예를 들어 람다 대수를 기계 수준으로 변환할 때 흔히 필요한 것 중 하나인 항수 분석(Arity analysis)에 대해 이야기해보자. 항수 분석은 함수가 하나의 인자를 받은 뒤 실행되어야 하는지, 혹은 두 인자를 모두 받아 실행되어야 하는지 등을 확인하여 이후에 그에 걸맞는 최적화된 기계어(Machine language)를 생성할 수 있게 도와주는 분석 작업이다. 평범한 람다 대수에서는 항수 분석의 결과를 직접적으로 표현하기 어렵다. 예를 들어 람다 대수의 λx→(λy→y)\lambda x \to (\lambda y \to y)의 경우 이 함수가 xx와 yy를 모두 받아 yy를 되돌려주는 함수인지 (항수가 2인 함수인지), 혹은 xx를 받아 λy→y\lambda y \to y라는 함수를 되돌려주는 함수인지 (항수가 1인 함수인지) 구분할 수 없다. 그러나 이를 CBPV로 변환한 λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))나 λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는 각각이 무엇을 뜻하는지 분명히 이해할 수 있다.

• λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))는 두 변수 xx와 yy를 스택에서 빼낸 뒤 yy의 값을 되돌려주는 함수(항수가 2인 함수)이다.
• λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는 변수 xx를 스택에서 빼낸 뒤 지연된 계산 λy→return(y)\lambda y \to \mathtt{return}(y)를 돌려주는 함수(항수가 1인 함수)이다.

이런 장점을 바탕으로 CBPV를 더 발전시킨 "언박싱한 값에 의한 호출"("Call-By-Unboxed-Value")을 GHC 컴파일러의 중간 언어(Intermediate language)로 구현하는 것에 대한 논의가 현재 진행되고 있으며 앞으로 더 많은 함수형 컴파일러들이 관련된 중간 언어를 채용하기 시작할 것으로 보인다.

마치며

이 글에서는 함수형 언어의 핵인 람다 대수를 간단히 설명하고 람다 대수를 평가하는 방법에 대해서 다루어보았다. 특히 그 중 값 밀기에 의한 평가(Call-By-Push-Value, CBPV)가 무엇이며 CBPV가 다른 대표적인 두 방법(CBV, CBN)을 어떻게 표현할 수 있는지, 그리고 CBPV의 장점이 무엇인지에 대해서도 다루어 보았다. 이 글에서 미처 다루지 못한 중요한 주제는 CBPV를 기계에 가까운 언어로 번역해보는 것이다. 여기에서는 글이 너무 복잡해지는 것을 피하기 위해 제했으나, CBPV의 장점에서 살펴봤듯 이는 CBPV에 있어 핵심 주제 중 하나이기 때문에 이후에 다른 글을 통해서라도 이 주제를 소개할 기회를 가지고자 한다. 이 글이 CBPV에 대한 친절한 소개글이었기를 바라며 이만 줄이도록 하겠다.

---

1. 결과 값(Value)을 가지는 언어 표현을 말한다. 예를 들어 1+11 + 1은 22라는 값을 가지는 표현식이지만 (JavaScript의) let x = 3;나 (Python의) def f(): ...은 그 자체로는 값이 없기 때문에 표현식이 아니다. ↩︎

2. 다만 실제 역사에서는 람다 대수의 이해와 발견이 함수형 언어의 개발보다 먼저 이루어졌다. 이런 역사적 관점에서는 (이미 많은 수학자들이 이해하고 있던) 람다 대수에 여러 기능을 추가한 것이 바로 함수형 언어라고 볼 수 있다. ↩︎

3. 프로그래밍 언어(Programming Language)는 실제로는 치환을 사용하지 않고 환경(Environment)을 사용하는 경우가 더 많지만 설명의 편의를 위해 다른 언어들 또한 환경 대신 치환에 기반해 평가한다고 가정하겠다. ↩︎

4. 앞서 설명한 람다 대수에서는 이를 쉽게 얻을 수 있다. 오메가(Ω\Omega)라고 부르는 표현식인 (λx→x x) (λx→x x)(\lambda x \to x\ x)\ (\lambda x \to x\ x)의 평가는 값에 의한 호출을 따르든 이름에 의한 호출을 따르든 종료되지 않는다. ↩︎

5. 바로 이 함수 호출을 값 밀기에 기반해 해석하는 데에서 CBPV의 이름이 유래했다. ↩︎