3 minute read

Curry-Howard Coresspondence

타입 이론(type theory) 또는 타입 체계(type system)에 대한 공부를 하다보면, 굉장히 흥미로운 주장이 한 가지 나온다. 바로 커리-하워드 대응인데, 아주 쉽게 얘기해 논리의 증명 연산이 타입 체계와 대응된다는 주장이다.

개념 정리를 겸하기 위해 조금의 예시를 첨가하자면, 명제 ‘P이면 Q이다’를 기호로 표현한 \(P \rightarrow Q\) (또는 \(P \supset Q\))는 타입 체계에서 function type인 \(P \rightarrow Q\)와 대응, 명제 ‘P이고 Q이다’를 기호로 표현한 \(P \wedge Q\)는 타입 체계에서 pair의 type인 \(P \times Q\)와 대응된다고 할 수 있다는 것이다.

이는 단순히 꼴이 비슷하다 정도가 아니라, 이렇게 대응하였을 때 어떤 명제 P의 증명(proof)이 존재한다는 것을, 그에 대응하는 타입 P에 어떤 값(정확히는 term) t가 존재한다는 것으로 설명 가능하게 된다.

언뜻 보면 완전히 독립적일 것처럼 보이는 타입 체계와 논리 명제가, 결국 같은 구조를 가지며 같은 이야기를 하고 있을지도 모른다는 것이다!

대응, 동형, 동치

커리-하워드 대응은 커리-하워드 동형(isomorphism), 동치(equivalence) 등으로 표현되기도 한다. 독립적으로 보이는 두 체계가 서로 대응되며 각자의 언어로 기술되어 쌓여 온 것들이 통일되는 순간을 표현하기에 적절한 단어들이 아닌가 한다.

오래 전부터 이런 성격의 발견에 굉장한 흥미와 동경을 품고 있었다. 이를테면 제타 함수(엄밀히는 확장된 리만 제타 함수)와 수소의 분포 사이의 관계에 대한 가설인 리만 가설이라든가, 어떤 잘 정의된 계산 문제(well-defined computational problem)를 다른 형태의(일반적으로 더 넓은 형태의) 문제로 환원(reduce)하는 모든 과정 같은 것들 말이다.

아주 보잘것 없는 경험이지만, 어릴 적 꽤나 비슷한 형태의 발견을 스스로 해낸 기억이 있다. 너무 오래 전이라 명확하고 구체적인 것은 다 잊었지만, 대략 중고등 물리학을 배울 때 여러 요소들이 가지고 있는 자체적인 성질(이를 \(k_1, k_2\)라는 수치로 나타낼 수 있다 하자)과 각 요소들 사이의 관계(이를 \(m:n\)이라는 실수 비로 나타낼 수 있다 하자)를 값으로 표현하였을 때, 그 요소들이 섞이며 나타나게 되는 최종 성질이 \(k_1 \cdot n + k_2 \cdot m\)와 같은 형태로 표현 가능하다는 것을 배운 적이 있다. 이 식을 보고 바로 무게중심(질량중심)을 구하는 식이 떠올랐고, 이를 가르치던 선생님이 떠오르는 게 없냐 물으셨을 때 무게중심을 이야기하니 어떻게 알았냐며 놀라며 둘의 관계에 대해 설명하시던 소소한 추억이 있다. 그 때 당시에는 그저 참신한 비유나 말장난에 취미가 있던 터라 뜬금없는 맥락의 개념을 어떻게든 끌고 오는 것에 혈안이 되어 있기에 우연히 맞아 떨어진 게 아닌가 하고 넘어갔지만, 그것이 학술적으로 의미를 가질 수 있다는 것이 꽤나 충격이었다.

창의성과 과학적 발견

연구자의 길에 막 들어서려는, 이제 조금씩 발부터 담그고 있는 지금 생각해 보면 내가 경험했던 바로 그 경험이 결국 창의라는 것이고 연구의 키 아이디어가 되는 발견이 아닌가 한다. 새로운 패러다임을 여는 과학적 발견은, 대부분의 경우 그 사람이 생각할 수 없었던 말도 안 되게 새로운 개념이 어디선가 튀어나오는 게 아니라 이미 그 사람이 사유하고 있던 추상화된 구조들이 재결합하고 재발견되며 자리를 찾아간 결과이다.

요하네스 케플러는 물리천문학의 기본이 되는 여러 법칙을 찾아냈다. 지금이야 하늘에 천구라는 것은 없고, 넓디 넓은 우주가 펼쳐져 있다는 것이 상식처럼 받아들여지고 있지만, 케플러가 천체에 대한 탐구를 하던 때만 해도 천구가 당연시되었고, 케플러 역시 하늘과 하늘에 보이는 여러 별들(정확히는 행성들)이 존재하는 형태를 여러 정다면체들로 설명하려 했다. 이후 다양한 탐구적 고비를 겪고, 튀코 브라헤의 정밀하고 방대한 관측 자료를 수학적으로 철저히 분석한 끝에 조화의 법칙과 같은 지금까지도 받아들여지고 확장되는, 과장하면 진리에 가까운 법칙을 발견해냈다. 그가 처음 정다면체로 천구를 설명하려 했던 것은, 당시 그가 기하학에 빠져 있었기 때문에 어떤 현상을 설명하고자 할 때 본인의 머리 대부분을 차지하고 있는 기하학의 언어로써 설명하려는 시도 끝에 나타나게 된 결과이다. 그리고 결국 시대를 관통하는 법칙을 찾아낸 것 역시, 그에게 주어진 (튀코의) 관측 자료를 그 누구보다 깊고 정밀하게 다루어 그가 좋아하던 수학의 언어로 표현하고자 하는 노력을 통해 일궈냈다 할 수 있다. 그의 머릿속을 전부 들여다보지 못하는 우리는 꽤 많은 탐구 과정을 생략하고 ‘새로운’ 발견이라 생각하곤 한다. 그리고 그것이 곧 창의성의 발현이 아닐까.

창의성의 발현이 과학적 발견으로 이어지는 사례는 이외에도 너무나도 많다. 옥수수 과학자 바바라 매클린톡의 사례는 그의 전기책 [생명의 느낌]을 통해 꽤나 유명해졌는데, 그가 평생 옥수수를 관찰하고 연구하며 발견한 수많은 생물학적 업적들은 그의 표현대로 “자신이 그 생명체가 된다는 느낌”을 받을 때 이루어냈다고 한다. 말 그대로 몰아일체의 경지에 도달한 순간, 머릿속 어딘가에 있던 추상적인 개념들이 정답을 속삭이는 것이다.

위와 같은 사례들처럼 놀라운 과학적 발견을 해내는 과정에는 번뜩이는 관찰력과 뼈를 깎는 노력이 필요할 것이다. 나는 내가 사랑하는 연구 분야에서 얼마나 창의적일 수 있을까. 얼마나 새로운 대응을 이끌어낼 수 있을까.

You May Also Enjoy