Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

당신이 궁극의 "증명 보조기(Proof Assistant)"를 만들려고 노력하고 있다고 상상해 보세요. 이 기계는 인간의 수학과 논리 숙제를 검토하여 그것이 100% 정확한지 확인하도록 돕는 아주 똑똑한 로봇입니다. 수십 년 동안, 대부분의 이러한 로봇들은 **의존 유형 이론(Dependent Type Theory, DTT)**이라는 특정 설계도를 사용하여 구축되었습니다. 이것은 매우 복잡하고 첨단 기술이 집약된 레고 세트로 로봇을 만드는 것과 같습니다. 모든 레고 블록에는 특정 라벨이 붙어 있으며, 로봇은 블록들을 결합하기 전에 라벨이 완벽하게 일치하는지 확인합니다.

하지만 이 논문에서 저자 데일 밀러(Dale Miller)는 이 로봇을 만드는 또 다른, 어쩌면 더 나은 방법이 있을 것이라고 제안합니다. 그는 우리가 구조적 증명론(Structural Proof Theory), 구체적으로는 **시퀀트 계산법(Sequent Calculus)**이라 불리는 프레임워크를 살펴보아야 한다고 주장합니다. 이것은 딱딱한 레고 세트가 아니라, 논리가 유지되는 한 조각들이 움직이고 형태를 바꿀 수 있는 역동적이고 움직이는 퍼즐이라고 생각하십시오.

밀러가 왜 이 "퍼즐" 접근 방식이 "레고" 접근 방식보다 우월할 수 있다고 생각하는지에 대한 이유를 여섯 가지 핵심 아이디어를 사용하여 다음과 같이 설명합니다.

1. "무엇"과 "어떻게"의 분리

레고의 세계(DTT)에서 로봇은 두 가지를 동시에 결정합니다. 즉, 당신이 어떤 논리를 사용하는지(무엇)와 그 증명이 어떻게 구축되는지(어떻게)입니다. 이는 마치 "우리는 오직 빨간색 블록만을 사용하여 탑을 쌓아야 하며, 쌓는 방식은 오직 수직으로만 가능하다"라고 말하는 것과 같습니다.
밀러는 이 둘을 분리해야 한다고 제안합니다. 우리는 논리(게임의 규칙)를 결정한 다음, 그 문제를 해결하기 위해 어떠한 증명 구조라도 선택할 수 있습니다. 이는 당신이 축구를 하고 싶다고 결정한 다음, 규칙이 허용한다면 발로 차거나, 헤더를 하거나, 혹은 네트 캐논을 사용하는 등 다양한 방식으로 골을 넣을 수 있다는 것을 깨닫는 것과 같습니다. 시퀀트 계산법을 사용하면 (자연 연역, 타블로, 또는 해상법과 같은) 많은 다양한 "움직임"을 강요받지 않고도 사용할 수 있습니다.

2. "코드로서의 증명" 문제

레고 방식은 증명을 컴퓨터 프로그램(λ-항)처럼 취급합니다. 컴퓨터는 프로그램을 실행하는 데 뛰어나지만, 때로는 매우 까다로울 수 있습니다. 때때로 프로그램은 답에 도달하기 위해 이상한 경로를 거치거나, 특정 유형의 입력을 기다리느라 멈춰버릴 수도 있습니다.
밀러는 레고 방식이 "유니버스 레벨(universe levels)"(유형들이 서로 충돌하지 않도록 조직하는 복잡한 방법)이나 "증명 무관성(proof irrelevance)"(실제로 중요하지 않은 부분의 증명을 확인하느라 시간을 낭비하는 것)과 같은 지저분한 문제들을 다뤄야 한다는 점을 지적합니다. 시퀀트 계산법 접근 방식은 더 단순합니다. 그것은 증명을 복잡한 코드 스크립트보다는 플로우차트처럼 직접적으로 다루기 때문에, 이러한 무거운 타이핑 규칙들을 걱정할 필요가 없습니다.

3. "고전적" 논리 처리 (이것 아니면 저것의 문제)

어떤 논리는 "직관주의적"(무언가를 존재함을 증명하려면 그것을 직접 만들어내야 함)이고, 어떤 논리는 "고전적"(그것이 존재하지 않는다는 것이 불가능함을 보여줌으로써 존재를 증명할 수 있음)입니다.
레고 방식은 "고전적" 스타일을 매끄럽게 처리하는 데 어려움을 겪습니다. 이를 작동시키기 위해 종종 추가적이고 투박한 규칙들을 덧붙여야 합니다. 밀러는 시퀀트 계산법이 처음부터 두 스타일을 모두 잘 다룰 수 있도록 설계되었으며, 마치 별도의 육중한 컨버터 없이도 어떤 플러그든 맞출 수 있는 범용 어댑터와 같다고 주장합니다.

4. "아마도"를 수용하기 (비결정론)

이것은 매우 중요한 지점입니다. 레고 로봇들은 "결정론적(deterministic)"으로 구축되어, 즉 증명을 확인하기 위해 단 하나의 직선 경로만을 따라가야 합니다. 만약 막다른 길에 부딪히면, 그들은 멈춥니다.
밀러는 약간의 "비결정론(non-determinism)"(추측과 백트래킹)을 허용하는 것이 오히려 초능력이 될 수 있다고 제안합니다. 미로를 상상해 보세요. 결정론적인 로봇은 한 경로를 따라 걷다가 벽에 부딪히면 멈춥니다. 반면 비결정론적인 로봇은 한 경로를 시도하다가 벽에 부딪히면, "앗" 하고 말한 뒤 즉시 다른 경로를 시도할 수 있습니다.
밀러는 증명 검사기가 "추측"하고 백트래킹할 수 있게 함으로써, "증명 인증서(proof certificates)"(당신이 제출하는 숙제)를 훨씬 더 작게 만들 수 있다고 주장합니다. 로봇이 탐색이라는 무거운 작업을 수행하므로, 당신은 모든 단계를 일일이 적어낼 필요가 없습니다. 이것은 트레이드오프입니다. 로봇이 조금 더 열심히 생각하게 하는 대신, 당신의 숙제지는 더 작아지는 것입니다.

5. "움직이는 바인더(Moving Binders)"의 마법

이것은 이 논문의 가장 흥ile한 기술입니다. 논리에서 우리는 종로 종종 "바운드(bound)"된 변수들을 다룹니다 (예: "모든 x에 대하여..."에서의 x). 레고의 세계에서 이러한 변수들은 고정되어 있는 경우가 많으며, 이를 다루는 것은 기술적인 골칫거리(유명한 POPLMark 챌린지와 같은)의 악몽이 됩니다.
밀러는 변수가 **이동 가능(mobile)**하다는 관점을 제 제안합니다. 그는 이를 **λ-트리 구문(λ-tree syntax)**이라고 부릅니다.
변수를 이름표라고 상상해 보세요. 레고의 세계에서는 사람을 움직이면 이름표가 떨어지거나 혼란을 줄 수 있습니다. 하지만 밀러의 세계에서 이름표는 사람에게 붙어 있습니다. 당신이 방 안에서 사람을 어떻게 움직이더라도(혹은 증명 내에서 어떻게 움직이더라도), 이름표는 그와 함께 유지됩니다.
그는 **∇-양화사(nabla quantifier)**라는 특별한 도구를 도입합니다. 이것을 "로컬 스코프(local scope)" 버튼이라고 생각하십시오. 이 버튼을 누르면, "이 변수는 오직 이 특정 부분에만 속하며, 절대 탈출할 수 없다"라고 선언하는 것과 같습니다. 이는 프로그래밍 언어나 컴퓨터 간의 통신을 모델링하는 방식인 π-계산법(pi-calculus)처럼 복잡한 규칙을 가진 언어들을 이해하기 매우 쉽게 만듭니다.

6. 아벨라(Abella) 로봇

밀러는 단순히 말로만 설명하는 것이 아니라, 이것이 작동함을 증명하기 위해 로봇을 직접 만들었습니다. 그것의 이름은 **아벨라(Abella)**입니다.
아벨라는 전적으로 이러한 시퀀트 계산법 원리에 기반하여 구축된 정리 증명기(theorem prover)입니다. 아벨라는 복잡한 논리와 바인딩을 쉽게 다루기 위해 "움직이는 바인더"와 "∇-양화사"를 사용합니다. 레고 기반의 로봇들(Coq나 Lean과 같은)은 매우 인기 있고 방대한 사전 구축된 증명 라이브러리를 가지고 있지만, 아벨라는 변수가 이름 붙여지고 이동하는 방식과 관련된 까다로운 문제들—특히 변수의 이름과 이동을 다루는 문제들—에 있어서 이 새로운 접근 방식이 더 자연스럽고 우아하다는 것을 시사합니다.

요약

밀러는 레고 로봇(의존 유형 이론)이 나쁘다거나 그것들을 버려야 한다고 말하는 것이 아닙니다. 그는 그것들이 성숙하고, 널리 사용되며, 많은 일에 유용하다는 점을 인정합니다.
하지만 그는 증명 보조기의 기초를 설계함에 있어서, 시퀀트 계산법이 더 유연하고, 단순하며, 강력한 도구 상자를 제공한다고 제안합니다. 그것은 논리와 구조를 분리하고, 스마트한 추측을 수용하며, "움ло이는 변수"를 다루는 까다로운 문제를 현재의 표준이 겪는 어려움보다 훨씬 우아하게 처리합니다. 이것은 논리의 다른 분야에서 성공적이었던 프레임워크를 사용하여, 대화형 증명 보조기의 세계에서 아직 주목받지 못한 다른 각도에서 문제를 바라보자는 초대입니다.