CurryHowardIsomorphism

propositions-as-types 으로도 알려진 커리-하워드 동형(Curry-Howard isomorphism)은 형식 논리 체계와 컴퓨터 프로그램 간의 대응 관계를 말한다. 이 개념은 함의 \(A \to B\) 가 \(A\) 에서 \(B\) 로 가는 함수형(function type)에 대응된다는 간단한 아이디어에서 출발했다. \(A \to B\) 와 \(A\) 로부터 \(B\) 를 추론해내는 것은 \(A \to B\) 에 \(A\) 를 입력하여 \(B\) 를 출력하는 함수와도 같다. 실제로 \(A \to B\) 를 증명하는 것은 영역 \(A\) 의 임의의 원소를 \(B\) 의 원소로 출력하는 함수를 구성하는 것과 같다.

그런데 이 아이디어는 사실 오래된 아이디어였다. \(A\) 에서 \(B\) 로 가는 함의에 대한 구성적 증명은 \(A\) 의 증명을 \(B\) 의 증명으로 변환하는 절차와 같다. 커리-하워드 동형은 이 아이디어를 엄밀하게 형식하했다.

1930년대 해스켈 커리(Haskell Brooks Curry)는 사실상 증명에 관련된 모든 개념이 계산의 관점으로 변환될 수 있고, 사실상 다양한 람다 계산의 구문론적 특징과 그와 비슷한 체계들이 증명 이론의 언어로 형식화될 수 있다는 것을 발견했다. 가령, 술어 논리의 양화는 종속곱(dependent product), 2차 논리는 다형성(polymorphism), 귀류법에 의한 증명은 컨트롤 연산자(control operator)에 대응된다. 더 나아가 다양한 논리적 형식화들, 가령, 힐베르트 스타일, 자연 연역, 시퀸트 계산 등이 계산 모델, 가령, 조합적 논리, 람다 계산 등을 흉내낼 수 있다는 것이 밝혀졌다.

1969년에 윌리엄 하워드(William Howard)는 propositions-as-types 대응이 단순히 흥미로운 결과 중 하나가 아니라 근본적인 원리라는 것을 이해했다. 증명 정규화와 절단 제거는 \(\beta\)-축소(\(\beta\)-reduction) 와 동등한 계산의 또 다른 모델이라는 것이 밝혀졌다. 증명 이론과 계산 이론은 본질적으로 같은 학문의 다른 양면을 보여주고 있다는 것이 드러났다.

이에 따라 발전된 타입 이론(type theory)은 컴퓨터 프로그램의 개발 도구로 사용되고 있고, 컴퓨터 과학의 근본적인 과제로써 효과적인 형식적 방법(efficient formal method)에 대한 필요성이 늘어나고 있다.

한편, 폴 로렌젠(Paul Lorenzen)는 증명가능성이 대화형 게임(dialogue game)으로 표현가능하다는 아이디어를 제시했다. 커리-하워드 동형을 통하여 항(term)은 게임을 플레이하는 전략으로 볼 수 있다. 증명과 프로그램이 같은 대상을 나타낸다는 주장은 이미 정립되었지만, 대화형 게임이나 그러한 게임의 전략 또한 같은 대상이라고 주장하기에는 아직 조심스럽다. 그럼에도 불구하고 커리-하워드 동형에 의하여 증명과 프로그램이 같은 세계를 서로 다른 방식으로 표현한다는 것이 드러난 것처럼, 게임도 같은 세계를 게임으로 방식으로 표현하는 것일 수도 있다. 그렇다면 이 증명, 프로그램, 게임이 본질적으로 같은 대상인 것이다.

또 한편, 지라드(J.Y. Girard)의 선형 논리(linear logic)는 커리-하워드 동형의 또 다른 측면을 보여주어서 증명과 계산 사이를 연결하는 완전히 새로운 세상을 열었다.

커리-하워드 동형을 공부하기 위한 첫번째 목표는 논리와 타입 람다 계산(typed lambda-calculi)의 관계를 이해하는 것이다. 반면, 프로그래머의 입장에서 기술적인 관점으로 커리 하워드 동형을 공부하기 위한 첫번째 목표는 논리와 프로그래밍 언어 사이의 관계를 이해하는 것이다.

현재 소프트웨어 개발은 성능 테스트로 검증된다. 프로그램에 입력되는 다양한 값의 파라미터를 검증하여 버그가 발생하지 않는지 테스트하는 것이다. 그러나 수학에서의 접근은 조금 다르다. 모든 자연수에 대한 성질 \(P(n)\) 을 증명할 때 수학자들이 \(P(0)\) 가 성립한다는 것을 확인하고, \(P(1)\) 가 성립한다는 것을 확인하고, \(P(2)\) 가 성립한다는 것을 확인하고, 매우 큰 수에 대해서도 성립한다는 것까지 확인하고, 이 성질이 그의 경험적 기준에 만족될만큼 검증되었을 때 "거의 다" 검증되었다는 결론을 내리지 않는다.

프로그래밍에서 아무리 자명해보이는 코드에서 수없이 다양한 파라미터로 프로그램이 잘 작동한다는 것을 테스트했다고 하더라도, 예상하지 못한 파라미터에서 프로그램이 오작동할 수도 있다. 왜냐하면 인간의 경험적 기준과 실질적인 타당성 간에 엄청난 갭이 있기 때문이다. 우리가 우리의 경험적인 기준으로 충분히 많이 검증했다고 판단해도 충분하지 않을 수도 있다. 실제로 컴퓨터 프로그램을 아주 헤비하게 테스트하고 상용화해도 에러와 버그가 발견된다. 병렬 컴퓨팅이 상용화되기 시작할 때부터 버그가 프로세스의 특정 스케줄링에 따라 트리거될 수도 있게 되었다. 따라서 어떤 것에 대한 확신을 원한다면 검증하지 말고 증명해야 한다. 1970년대에 이미 다익스트라(Dijkstra)는 테스트로 버그의 존재를 보일 수는 있지만 버그가 존재하지 않는다는 것을 보일 수는 없다고 말했다. 프로그램을 형식적으로 검증한다는 아이디어는 이때로부터 20년을 더 거슬러 올라가 1949년 튜링의 논문 《On checking a large routine》 에서 소개된다. 프로그램을 진정으로 믿고 싶다면 검증 방법을 테스트에서 증명으로 옮겨야 한다. 커리-하워드 동형 관계를 통하여 프로그램의 타당성의 증명을 수행하는 방법을 이해할 수 있다.

그러면 어떻게 증명의 기술을 프로그램에 적용하여 프로그램의 타당성을 검증할 수 있는가? proof-as-program 대응 관계(커리-하워드 동형) 덕분에 새로운 아이디어를 만들어야할 필요가 없다. 엄밀하게 말하면, 타입 함수형 프로그래밍 언어에서 프로그램의 타입은 식(fomula), 프로그램 그 자체는 식을 증명하는데 요구되는 정보와 같다. 증명이 공리에 추론규칙을 적용하여 새로운 참인 사실을 확인하는 과정인 것과 같이 프로그램은 기본 데이터(공리)에 연산(추론규칙)을 적용하여 새로운 데이터를 만드는 과정이다. 결국 다음과 같은 사실을 인지하고 있다면, 수학에서의 기술을 프로그램을 연구하는데에 사용할 수 있다는 것을 알 수 있을 것이다.

그러면, 또 다른 한편으로는, 수학의 증명으로부터 계산적인 내용을 이끌어낼 수도 있다는 것을 알 수 있다.

증명이론은 논리적 문제 뿐만 아니라 컴퓨터 과학을 벗어난 다양한 분야에도 적용된다. AI 라는 말을 처음 사용한 존 매카시는 지식을 표현하고 조작하기 위하여 수리논리(mathematical logic)를 사용해야 한다고 강하게 주장했다. 그의 이 신념이 신경망을 인공신경망으로 만들었고, 미래가 인공신경망을 통하여 어떻게 만들어질지 아무도 모르게 되었다.

20세기 초반 러셀의 모순이 발견되었고, 이것은 힐베르트가 모든 수학을 공리화하고 그 공리화가 무모순이라는 것을 보이게 한 동기가 되었다. 괴델의 불완전성 정리가 이것에 명확한 해답이 없다는 것을 밝혔지만, 그래도 수학의 거의 대부분이라도 형식화하려는 다양한 형식 체계가 제시되었다. 대표적으로 ZFC 로 알려진 집합론이고, 또 하나는 러셀의 타입 이론이다. 사람들은 보통 ZFC 를 수학의 기초로 생각하지만, 실제로는 타입 이론을 수학의 기초로 채택해도 상관없다. 왜냐하면 타입으로도 집합을 표현할 수 있기 때문이다. 타입 이론은 기초적인 철학적 질문에 대답할 수 있는 틀을 제공해주었다. 추론이 무엇인지, 증명이 무엇인지, 인간이 어떤 것이 존재하는지 알고 있다면 이것을 실제로 알고 있는 것인지, 어떤 두 대상이 같다는 것은 무엇인지 등등. 이런 것을 철학적으로 대답할 수 있지만 이런 대상들을 형식화하고 추론 규칙에 의하여 질문에 대답하면 훨씬 더 만족스러운 결론을 얻을 수 있다. 우리 삶의 중요한 부분을 수학적 세계로 바라봄으로써 계산이 자기 자신을 3가지 형태로 나타낸다는 계산적 삼위일체라는 사상을 생각할 수 있다.

커리-하워드 동치가 논리와 프로그래밍 간의 관계를 설명한다. 또 다른 사상은 오직 실제로 구성될 수 있는 것만 받아들이는 구성주의(constructivism)이다. 구성주의는 핵심적인 역할을 하는데, 프로그램이 정확하게 대상의 구성을 서술하는 방법들로 구성되기 때문이다.

생각을 산술화 할 수 있고 더 나아가서 기계화 할 수 있다면 그 생각은 코드가 되고 프로그램이 된다. 이것은 하나의 수학 명제에 대한 추론과 증명이다. 그런데 버그가 발생하고 예상치 못한 에러가 생기고 이를 통해 해킹이 가능한 이유는 원작자의 생각과 그 생각의 기계화 사이에 갭이 있다는 것이다. 만약 모두가 버그라고 생각하고 해킹가능한 구멍이라고 여겨지는 동작이 어떤 프로그램에서 실행되고 있어도 그것이 원작자의 생각이 제대로 기계화된 것이라면 그것은 버그가 아니다. 그러므로 버그는 생각과 그것의 기계화물 사이에 존재하는 차이이다.

이것이 원론적인 이야기이지만, 조금 더 현실적으로 생각하면 ssh 나 원격 프로그램 등 극소수의 프로그램을 제외하고는 대부분의 프로그램이 rc 를 허용하지 않는다. 즉, 대부분의 프로그램 원작자들이 자신의 프로그램으로 타인이 명령어를 실행하겠다는 생각을 하지 않는다. 이러한 공통적인 생각 규범의 집합을 형성하면 프로그램의 원작자로부터 어떤 생각을 갖고 있는지 구체적으로 듣지 않아도 프로그램의 타당성을 검증할 목표가 생긴다.

그러면 그러한 극소수의 예외적인 프로그램들을 생각하지 않고, 대다수의 프로그램이 갖고 있는 보안 규범을 지키는 것을 목표로 하여 기계들이 진행하는 게임을 만들 수 있다. 이는 상대 기계의 목표를 깨뜨리는 버그나 해킹가능 지점으로 도달할 수 있는 경로에 대한 존재 증명을 이루는 방식의 게임이다. 둘 이상의 기계는 상대 컴퓨팅 기기의 목표로의 도달가능성(reachability)을 증명해야 하고, 이 도달가능성의 증명이 곧 poc 가 된다. 그리하여 최종적으로는 자기 자신의 목표를 훼방할 수 없도록 상대 컴퓨팅 기기가 자신으로 도달할 수 있는 경로의 존재성을 부정을 증명하는 것이 게임의 끝이 된다. 이 자기 자신으로의 도달가능성의 부정의 증명 또한 poc 가 된다.

이 기계가 실행되면 이 기계는 효과적인 컴퓨팅 기기로부터의 자기 자신으로의 도달가능성의 부정의 증명을 계속해서 이루어나갈 것이다. 효과적이 컴퓨팅 기기란 다양한 기준으로 선정될 수 있는데, 가령, 가장 가까운 컴퓨팅 기기, 또는 가장 견제되는 컴퓨팅 기기 등등이 될 수 있다. 이 기계들을 서로 경쟁시킴으로써 가장 성능이 좋은 극소수의 기계들, 또는 그 기계들이 선택한 정책들을 사장시키지 않고 보존하며 살아남은 기계들에게 전수할 수 있다. 왜냐하면 인공지능의 파라미터는 전수가능하기 때문이다.