논리와 저수준(Low-level) 자료 표현(Data representation) 연작

• 1 편
• 2 편 $\text{---}$ 이 글

다시 보는 논리적이 되는 방법 - 논건 대수(論件 代數, Sequent Calculus)

1 편에서 다루었던 "논리적"이 되는 두번째 방법, 즉 논건 대수를 다시 한 번 짚고 넘어가자. 우선 논건 대수에서 다루는 대상은

명제의 진리 대한 가정적 판단 $\Gamma \vdash P\ \texttt{true}$

였다. 여기서 명제란

1. 단위 명제(Atomic Proposition) $A$
2. 참 명제(True Proposition) $\top$
3. 거짓 명제(False Proposition) $\bot$
4. 명제 $P$와 $Q$가 있을 때, $P \land Q$($P$ 그리고 $Q$)
5. 명제 $P$와 $Q$가 있을 때, $P \lor Q$($P$ 또는 $Q$)
6. 명제 $P$와 $Q$가 있을 때, $P \to Q$($P$라면 $Q$)

같은 방법을 통해 만들어질 수 있는 대상이었다.

논건 대수에서는 이 명제의 진리에 대한 가정적 판단이 논리적인지 아닌지를 다음과 같은 추론 규칙에 기반하여 증명했다.

각 추론규칙은 줄 위의 판단(전제)을 증명했을 때 줄 아래의 판단(결론)을 증명하는 규칙이다.

1 편에서 논건 대수는 위의 규칙 중 $\text{cut}$을 제거함으로서 일관적임, 즉 거짓을 증명할 수 없는 체계임을 쉽게 보일 수 있게 만든 것이라 설명했다. 또한 이 체계가 가지는 단점(증명에 대응되는 컴퓨터 공학적으로 직관적인 항을 주기 어려움) 역시 다루었다.

그렇다면 논건 대수는 컴퓨터 공학적으로 쓸모가 없을까? 물론 아니다! 아주 약간의 변형을 통해 컴퓨터 공학적으로 유용한 해석이 가능한 항을 줄 수 있다. 이 해석을 주기에 앞서 어떤 변형이 필요한지에 대해 먼저 알아보자.

논건 대수 변형하기 - 반(半)공리적 논건 대수(Semi-Axiomatic Sequent Calculus)

우선 접근 방식의 근간을 변경하도록 하자. 이전에는 논건 대수의 일관성을 보이기 위해 $\text{cut}$ 규칙을 없애는 데에 초점을 맞추고 있었다. 반면에 이제는 컴퓨터 공학적으로 유용한 해석을 주는데에 집중해서, $\text{cut}$ 규칙을 없애는 대신에 최대한 활용하려고 해보자. 이런 관점에서는 논건 대수의 몇몇 규칙은 쓸데없는 복잡도를 가지고 있다. 다른 말로는 이런 규칙들은 $\text{cut}$이 이미 담당한 일과 일부 겹치는 일을 하고 있다. 예를 들어

규칙을 사용하기 위해서는 $P\ \texttt{true}$와 $Q\ \texttt{true}$를 전제로 먼저 증명해야만 한다. 다음의 변형된 규칙에서처럼 가정에 $P\ \texttt{true}$와 $Q\ \texttt{true}$가 이미 주어졌다고 하는 것으로 규칙을 서술한다면 이 "먼저 증명해야함"이라는 규칙의 복잡도를 피할 수 있다.

이 변형된 규칙 $\text{AR}\land$는 따로 놓고 보았을 때는 원래의 $\text{R}\land$보다 증명할 수 있는 판단이 적지만, $\text{cut}$ 규칙을 최대한 활용한다면 같은 능력을 지닌다. 원래의 규칙을 다음과 같은 꼴로 대체할 수 있기 때문이다^[1].

다시 말해서 $\text{R}\land$는 $\text{AR}\land$라는 "순수한 $\land$를 위한 규칙"과 $\text{cut}$으로 분해할 수 있다. 여기서 $\text{AR}\land$와 같이 어떤 전제도 가지지 않은 추론 규칙을 "공리"("Axiom")라고 한다. 이 규칙이 $\text{A}$로 시작하는 이름을 가지는 이유도 바로 이 규칙이 공리(Axiom)이기 때문이다. 같은 방법을 다음의 $\text{R}\lor_1$ 규칙

에 적용하면 다음의 공리를 얻을 수 있다.

또한 $\text{R}\lor_2$에도 마찬가지 변환을 적용해 공리 $\text{AR}\lor_2$를 얻어낼 수 있다.

지금까지 $\text{R}\land$와 $\text{R}\lor_1$, $\text{R}\lor_2$를 공리로 바꾸어 $\text{cut}$이 하는 일과 중복되는 "쓸데없는" 복잡도를 줄여보았다. 그렇다면 공리로 바꿔 쓸 "쓸데없는" 복잡도는 항상 $\text{R}$ 규칙이 가지고 있을까? 안타깝게도 그리 단순하지만은 않다. $P \to Q$를 위한 규칙의 경우 $\text{R}\to$ 규칙이 아닌 다음의 $\text{L}\to$ 규칙

에서만 $\text{cut}$이 하는 일과 겹치는 부분을 관찰할 수 있고, 이를 다음과 같이 제거할 수 있다.

명제를 만드는 방법들이 가지는 이 차이, 즉 $\text{cut}$과 겹치는 일을 하는 규칙이 $\text{R}$ 규칙인 방법($\land$와 $\lor$)과 $\text{L}$ 규칙인 방법($\to$)의 차이가 인위적인 차이로 보일지 모르나, 이 차이는 사실 논리적으로 매우 자연스럽고 중요한 여러 결과들을 주며 컴퓨터 공학적으로도 직관적인 구분을 준다. 이로 인해 이 두 방법에

• 양(Positive)의 방법: $\text{R}$ 규칙이 공리로 바뀌어야 하는 명제를 만드는 방법 ($\land$와 $\lor$)
• 음(Negative)의 방법: $\text{L}$ 규칙이 공리로 바뀌어야 하는 명제를 만드는 방법 ($\to$)

같이 이름을 붙이기도 한다. 이후의 절에서 컴퓨터 공학적으로 이 둘이 어떻게 구분되는지에 대해 설명하며 이 이름을 사용할 것이다.

지금까지 $\text{cut}$ 규칙을 최대한 활용할 수 있도록 다른 규칙들에서 $\text{cut}$ 규칙이 담당한 일과 중복되는 부분을 최대한 제거해보았다. 요약하자면 다음과 같은 규칙들을 얻었다.

여기서 (컴퓨터 공학적으로는 그다지 중요하지 않은 $\top$과 $\bot$을 무시하면) 각 방법의 정확히 절반이 공리로 바뀌었다는 점에 유의하자. 이런 구성으로 인해 이 변형된 논건 대수를 "반(半)공리적 논건 대수"("Semi-Axiomatic Sequent Calculus", 줄여서 "SAX"^[2])라고 부른다^[3].

반공리적 논건 대수와 저수준(low-level) 자료 표현(data representation)

이 글에서 논건 대수의 변형인 반공리적 논건 대수를 소개한 당초의 이유는 논건 대수의 컴퓨터 공학적 해석, 즉 커리-하워드 대응을 찾기 위해서였다. 이제 커리-하워드 대응을 주기에 적합한 논건 대수의 변형을 끝마쳤으니 본격적으로 이 커리-하워드 대응을 설명할 것이다. 우선 각 판단들을 프로그램에서 쓸 수 있도록 표식을 붙이자. 1 편에서 다룬 자연 연역과 함수형 언어의 관계에서는 모든 가정에 변수 이름이라는 표식을 붙여 가정을 프로그램 내에서 쓸 수 있도록 했다. 논건 대수에서 사용할 표식은 단순한 이름과는 살짝 다른, "메모리 주소"("memory address")이다. 이 메모리 주소를 모든 가정과 귀결에 붙이도록 하자. 예를 들어 $\text{L}\land$ 규칙에 메모리 주소를 붙이면 다음의 규칙을 얻는다.

여기서 전제의 가정 $P\ \texttt{true}$와 $Q\ \texttt{true}$에 붙은 $a.0$와 $a.1$이라는 메모리 주소에 주목하자. 이 주소는 결론에 등장하는 $a$라는 주소에 $.0$과 $.1$이라는 "접근자"("accessor")를 추가한 것이다. 이 대응에서 $\text{L}\land$ 규칙을 해석하는 방식을 통해 접근자의 의미를 이해해보자. $\text{L}\land$ 규칙의 해석은 다음과 같다.

$P$와 $Q$의 쌍(Pair) $P \land Q$를 저장하고 있는 메모리 주소 $a$에서 $P$를 저장하고 있는 메모리 주소 $a.0$과 $Q$를 저장하고 있는 메모리 주소 $a.1$을 얻어내 이를 사용하는 규칙

이를 좀 더 구체화시켜 다음과 같은 메모리 도식을 그릴 수 있다. 아래 도식에서 연속된 사각칸은 연속된 메모리 영역을 뜻한다.

이 도식이 말하는 것은 $a$라는 주소에 $.0$이라는 접근자를 추가하면 메모리 주소 $a$에 저장되어 있는 값을 주소로 쓰고, $.1$이라는 접근자를 추가하면 그 다음 주소를 사용한다는 것이다. 이는 쌍이 (가장) 직관적인 구조로 메모리에 저장되어있을 때 쌍의 각 구성원을 접근하는 방법에 대한 설명을 준다.

비슷한 방식으로 $\text{L}\lor$에도 메모리 주소를 추가할 수 있다.

여기서는 전제의 가정에 등장하는 $P\ \texttt{true}$와 $Q\ \texttt{true}$ 모두 $a.1$이라는 주소를 사용하고 있다. 이는 $a.0$의 자리에 $P \lor Q$($P$ 혹은 $Q$)가 $P$로부터 만들어졌는지 $Q$로부터 만들어졌는지 구분하는 태그(tag)가 있기 때문이다. 예를 들어 $P$로부터 $P \lor Q$를 만들었을 경우, $a : P \lor Q\ \texttt{true}$에 대한 메모리를 도식화하면 다음과 같다.

$a$가 가리키고 있는 메모리 주소에는 $0$($P$로부터 만들어졌음을 뜻하는 태그)만이 들어있음에 유의하자. $Q$로부터 $P \lor Q$를 만들었다고 한다면 $0$대신 $1$을 태그로 넣어 이를 표시할 수 있다. ($P$나 $Q$에 대응되는) 실제 값은 메모리 주소 $a.1$에 저장되어 있다. 이 또한 태그된 합 자료형(Tagged sum type)을 나타내는 가장 직관적인 방법에 대한 설명이다.

그렇다면 귀결의 위치에는 왜 메모리 주소를 붙였을까? 위의 규칙에서 메모리 주소 $b$에 대해서는 특별한 설명을 하지 않아 이 메모리 주소가 쓸모가 없어 보일 수 있다. 이 메모리 주소의 유용성을 설명하기 위 $\land$와 $\lor$의 나머지 규칙, 즉 $\text{AR}$ 규칙에 대해, 특히 $\text{AR}\land$ 규칙에 대해 살펴보자.

메모리의 관점에서 설명하자면 이 규칙은

$P$값을 가진 주소 $a$와 $Q$값을 가진 주소 $b$가 있다면 $P \land Q$ 값을 가진 주소 $c$에 값을 채워넣을 수 있다

는 규칙이라고 볼 수 있다. 이 규칙의 결과를 메모리 도식으로 그려보면 다음과 같다.

즉, 주소 $a$와 $b$를 $c.0$과 $c.1$에 복사하는 것이라고 볼 수 있다. 마찬가지로 $\text{AR}\lor_1$과 $\text{AR}\lor_2$ 또한 가정의 주소와 적절한 태그를 귀결의 메모리 주소가 가리키는 메모리에 복사해 넣는 것이라고 볼 수 있다.

지금까지는 가정과 귀결에 주소를 붙이고 이 주소가 어떻게 쓰이는지 이해하는데 초점을 맞췄다. 이제 이 이해를 바탕으로 증명에 해당하는 항을 써 보자. 자연 연역의 항과 귀결은 $:$을 구분자로 사용하였지만, 반공리적 논건 대수의 경우 귀결의 자리에 "주소 : 진리 판단" 꼴이 이미 쓰이고 있다. 따라서 항과 귀결을 구분하기 위해 $:$를 사용하는 대신 $\dblcolon$을 사용할 것이다. 항을 포함한 완전한 $\text{AR}\land$ 규칙은 다음과 같다.

여기서 $x \colonequals v$는 값 $v$를 주소 $x$가 가리키는 메모리에 써넣는다는 뜻이다. 즉 이 규칙은 주소 $a$와 $b$를 쌍으로 묶어서 이를 주소 $x$가 가리키는 메모리에 써넣는 규칙이 된다. 이와 비슷하게 $\text{AR}\lor_1$과 $\text{AR}\lor_2$에는 다음의 항을 줄 수 있다.

$\text{L}$ 규칙도 앞서의 메모리에 대한 이해를 바탕으로 "메모리의 값을 읽어 작업을 한다"는 항을 줄 수 있다. 예를 들어 $\text{L}\land$의 완전한 규칙은 다음과 같다.

즉, $M$이 $a.0$와 $a.1$을 사용해서 $b$에 $R$ 형의 값을 써넣는다면, $\text{read}\ a\ \text{as}\ ({,}) \Rightarrow M$는 $a$를 사용해서 $b$에 같은 값을 써넣는 프로그램이 된다. $\text{L}\lor$의 완전한 규칙 역시 같은 구조를 설명한다.

$M_0$가 $a.1{:}P\ \texttt{true}$를 사용해서 $b$의 값을 채우고, 마찬가지로 $M_1$이 $a.1{:}Q\ \texttt{true}$를 사용해서 $b$의 값을 채운다면 $\text{read}\ a\ \text{as}\ (0{,}) \Rightarrow M_0\ |\ (1{,}) \Rightarrow M_1$ 가 $a$를 사용해서 $b$의 값을 채울 수 있는 프로그램이 된다.

이제 양의 방법($\land$와 $\lor$)을 어떻게 이해해야하는지 모두 살펴봤으니, 음의 방법($\to$)은 어떻게 이해해야하는지 살펴보도록 하자. 우선 $\text{R}\to$를 보자.

이 규칙은 주어진 메모리 주소 $a$에서 값을 읽어 주어진 메모리 주소 $b$에 결과를 쓰는 $M$라는 프로그램이 주어졌을 때, 임의의 두 메모리 주소 $a$, $b$에 대한 프로그램 $M$이 우리 $P \to Q$를 위한 메모리 주소 $c$에 쓸 값이라는 규칙이다. 컴퓨터의 관점에서 이는 인자의 주소($a$)와 반환 값의 주소($b$)가 주어졌을 때 인자를 사용해 반환값을 채워넣는 프로그램이 바로 함수라는 이야기이다. 나머지 규칙인 $\text{AL}\to$는 이렇게 저장된 함수를 "읽는" 규칙이다.

이는 인자의 주소 $a$와 반환값을 저장할 주소 $c$가 주어졌으니, 이들을 사용해 $b$가 가지고 있는 "인자를 사용해 반환값을 채워넣는 프로그램"을 실행하라는 규칙이다.

지금까지 $\text{AR}$ 혹은 $\text{R}$ 규칙이 어떤 메모리 주소에 값을 써넣는 규칙이고 $\text{AL}$ 혹은 $\text{L}$ 규칙이 어떤 메모리 주소에서 값을 읽어내는 규칙임을 살펴보았다. 그렇다면 $\text{init}$와 $\text{cut}$ 규칙은 무슨 역할을 할까? 우선 $\text{init}$ 규칙에 주소를 추가해보도록 하자.

$P$의 값을 가진 메모리 주소 $a$가 있고, $P$의 값을 써넣어야 하는 메모리 주소 $b$가 있다. 무엇을 할 수 있을까? 메모리 $a$의 값을 복사해 넣을 수 있다! 따라서 다음과 같은 이름을 항에 붙일 수 있다.

$\text{cut}$ 역시 중요한 역할을 맡는다. 이는 지금까지의 논의에서 빠져 있었던 "메모리 주소를 얻는 방법"을 주기 때문이다. 완전한 $\text{cut}$ 규칙은 다음과 같다.

즉, $\text{cut}$은 $P$의 값을 위한 메모리 $a$를 할당(allocate)하고, $M$을 통해 $a$를 초기화한 뒤 $N$을 실행하는 규칙이라고 볼 수 있다.

지금까지 다룬 규칙을 포함해 반공리적 논건 대수의 모든 규칙을 항과 함께 쓰면 다음과 같다.

양의 방법과 음의 방법의 차이

앞에서 양의 방법과 음의 방법이 직관적인 차이를 가진다고 설명했다. 이제 반공리적 논건대수의 컴퓨터 공학적 해석을 설명했으니 이 직관적인 차이를 보다 구체적으로 설명해보자. 양의 방법의 경우 $\text{L}$ 규칙이 메모리에 저장된 모든 자료를 읽어낼 수 있다. 다시 말해 $a.1$ 등의 주소를 통해 주소 $a$에 저장된 자료의 상세를 알아낼 수 있다. 반면에 음의 방법의 경우 $\text{AL}$ 규칙이 메모리에 저장된 모든 자료를 읽어낼 수 없다. $\to$의 $\text{AL}$ 규칙은 인자의 메모리와 반환값의 메모리가 주어졌을 때 주어진 인자에 해당하는 반환값만을 읽어낼 수 있고, 메모리 안에 저장된 자료의 상세는 알아낼 수 없다. 이를 다른 방식으로는 다음과 같이 표현하고는 한다.

• 양의 방법은 모든 상세를 읽어낼 수 있다.
• 음의 방법은 원하는 상세를 관찰할 수 있다.

마치며

1 편에 이어서 논리적 증명을 컴퓨터 공학적으로 해석하는 방법에 대해 알아보았다. 이 글에서는 특히 논건 대수와 메모리 수준의 자료 표현의 관계를 커리-하워드 대응의 관점에서 살펴보았다. 이 관계를 명확히 하기 위해 사용된 변형된 논건 대수인 반공리적 논건대수는 프랭크 페닝(Frank Pfenning) 교수님^[4]의 최근(2020년) 연구물이자 현재에도 활발하게 연구가 진행 중인 체계이다^[5]. 이 체계의 다른 응용 중 하나를 언급하는 것으로 이 체계의 유용성을 강조하며 글을 마치도록 하겠다. 이는 함수형 언어를 저수준으로 컴파일(Compile)하는 것으로, 자연 연역(함수형 언어에 대응되는 체계)을 반공리적 논건 대수(저수준 자료 표현 체계)로 변환하는 논리적 변환이 컴파일에 그대로 대응될 수 있다는 점을 이용한다. 이 컴파일 과정 역시 ML(Meta Language^[6])계열의 언어를 컴파일하는데 응용하기 위해 연구가 진행 중이다. 이 두 편의 글이 논리와 컴퓨터 공학의 관계를 개발자들이 이해하는데에 도움을 주었기를 바라며 이만 줄이도록 하겠다.

---

1. 엄밀히 말한다면 $\Gamma \vdash Q\ \texttt{true}$를 바로 사용할 수는 없고, "논리적 약화"라고 불리는 것을 증명해서 $\Gamma \vdash Q\ \texttt{true}$라면 $\Gamma, P\ \texttt{true} \vdash Q\ \texttt{true}$임을 보인 뒤에 $\Gamma, P\ \texttt{true} \vdash Q\ \texttt{true}$를 대신 사용해야만 한다. 여기에서는 글의 번잡함을 피하기 위해 가정이 서로 다른 두 가정적 판단 사이에서도 $\text{cut}$ 규칙을 사용 가능한 것으로 놓고 증명을 구성하였다. ↩︎

2. 원 저자는 이를 /sɒks/(양말의 "Socks"와 같은 발음)라고 발음한다. ↩︎

3. 여기의 "반"이 반대를 뜻하는 것이 아니라 절반을 뜻하는 것임을 다시 강조하고자 한다. 이 이름 자체가 절반의 규칙이 공리인 이 변형 논건 대수의 특징을 설명하고 있다. ↩︎

4. 람다 대수($\lambda$-Calculus)를 처음 만들어 낸 알론조 처치(Alonzo Church) 교수님의 제자의 제자("학문적 손자"라고도 한다)이시며 현대의 북미의 컴퓨터 공학과 논리에 지대한 영향을 끼치고 계신 교수님이시다. ↩︎

5. 예를 들어 기본적인 반공리적 논건 대수의 반복되는 참조를 개선한 체계인 SNAX(Semi-Axiomatic Sequent Calculus with Snip, 2023년) 등의 연구가 계속 이어지고 있다. ↩︎

6. Machine Learning 언어가 아니다! ↩︎