Justification Logic of the Lambda Calculus

당신이 하는 모든 생각이 하나의 코드 조각이 되고, 모든 코드 조각이 당신의 생각이 타당하다는 증명이 되는 세상을 상상해 보십시오. 이것은 컴퓨터 과학과 논리학이 만나는 기묘하고도 아름다운 교차점인 "커리-하워드 대응(Curry-Howard correspondence)"입니다. 이를 '증명(proof)'이라는 단어와 '프로그램(program)'이라는 단어가 사실상 동의어인 마법의 사전라고 생각해보세요. 만약 당신이 실행 중에 충돌(crash) 없이 돌아가는 컴퓨터 프로그램을 작성할 수 있다면, 당신은 어떤 명제가 참임을 수학적으로 증명한 것입니다. 수십 년 동안 과학자들은 컴퓨터가 자신의 작업을 스스로 검증하여, 소프트웨어 업데이트 뒤에 숨겨진 논리가 수학적 정리만큼이나 견고하도록 만드는 시스템을 구축하기 위해 이 아이디어를 사용해 왔습니다. 하지만 한 가지 문제가 있습니다. 보통 이러한 시스템들은 '증명'(논리)과 '프로그램'(계산)을 서로 비슷해 보일 뿐인 두 개의 서로 다른 언어로 취급합니다. 그들은 마치 같은 언어의 서로 다른 방언을 사용하는 두 사람과 같습니다. 서로 이해는 하지만, 완전히 같은 사람은 아닙니다.

여기서 이야기는 흥미로워집니다. 만약 우리가 단순히 두 언어 사이를 번역하는 것이 아니라, 이들을 하나의 강력한 슈퍼 언어로 합친다면 어떻게 될까요? 만약 '증명'이 프로그램에 붙여진 단순한 라벨이 아니라, 프로그램 그 자체라면 어떨까요? 이것이 실비아 길레잔(Silvia Ghilezan)과 파라스 파디아르(Paaras Padhiar)가 그들의 새로운 논문에서 다루는 핵심 질문입니다. 그들은 다음과 같이 묻고 있습니다. "우리는 계산하는 행위 자체가 곧 증명하는 행위가 되는 논리 체계를 구축할 수 있는가?" 그들은 단순히 이것이 멋진 아이디어라고 제안하는 데 그치지 않고, 실제 청사진을 만들고, 규칙을 작성하며, 이 시스템이 무너지지 않고 작동한다는 것을 증명했습니다. 그들은 이 새로운 시스템을 "Jλ"(J-람다라고 발음)라고 부르며, 이는 컴퓨터가 실시간으로 자신의 계산에 대해 추론할 수 있게 하여, '생각하는 것'과 '행하는 것' 사이의 경계를 하나가 될 때까지 허무는 데 설계되었습니다.

"행함"의 새로운 논리

저자들은 **람다 계산의 정당화 논리(Justification Logic of the Lambda Calculus, Jλ)**라는 새로운 종류의 논리를 소개합니다. 무엇이 이 시스템을 특별하게 만드는지 이해하기 위해, 당신이 미스터리를 풀려는 탐정이라고 상상해 보십시오. 표준 논리에서 당신은 "범죄의 증거"라고 적힌 서류 폴더를 가질 수 있습니다. 그 안에는 "X, Y, Z 때문에 이것을 증명했다"라는 메모가 들어 있습니다. 폴더는 증명이지만, 그 안의 메모는 단지 기술(description)일 뿐입니다. 기존의 시스템(LP, 즉 논리의 논리 등)에서 '증명'은 인증서와 같은 정적인 객체입니다.

길레잔과 파사디아르의 Jλ는 게임의 판도를 바꿉니다. 이 시스템에서 '증명'은 인증서가 아니라, 행위(action) 그 자체입니다. 대신에 폴더를 갖는 대신, 탐정이 범죄를 해결하는 실시간 영상 피드를 가지고 있다고 상상해 보십시오. 그 영상이 바로 증명입니다. 만약 탐정이 움직이면, 증명도 즉시 업데이트됩니다. Jλ에서 '증명 항(proof terms)'은 실제로 작업을 수행하는 컴퓨터 프로그램($\lambda$-terms)과 정확히 일치합니다. 시스템이 "A가 참임을 안다"라고 말할 때, 그것은 단순히 그렇다는 표지판을 들고 있는 것이 아니라, A를 계산하는 실제 코드를 들고 있는 것입니다. 이는 논리가 자신의 계산에 대해 동시에 추론할 수 있음을 의미합니다. 마치 자신이 생각하는 방식에 대해 생각하면서 동시에 생각을 수행하는 로봇과 같습니다.

기계를 구축하기: 게임의 규칙

이 논문은 단순히 이 아이디어를 제안하는 데 그치지 않고, 엔진 전체를 밑바닥부터 구축합니다. 저자들은 먼저 게임의 근본적인 규칙인 **공리(axioms)**를 작성하는 것으로 시작합니다. 그들은 표준 직관주의 논리(컴퓨터 과학에서 사용되는 유형의 논리로, 무언가가 참이라고 말하기 위해서는 실제로 증명을 구성해야 함을 요구함)의 규칙을 가져와 특수한 '박스(box)' 연산자를 추가합니다. 일반적인 논리에서 박스는 "A는 필연적이다"라고 말할 수 있습니다. Jλ에서 그 박스는 $[t]A$라고 쓰인 특정 코드 조각으로 대체되며, 이는 "코드 $t$는 A가 참이라는 증명이다"라는 의미를 갖습니다.

그다음 그들은 이 시스템이 어떻게 자신의 추론을 **내재화(internalize)**할 수 있는지 보여줍니다. 이것은 시스템이 자신의 단계를 살펴보고 "헤이, 방금 이 단계를 수행했고, 내가 올바르게 수행했음을 증명하는 코드는 이것이다"라고 말할 수 있다는 것을 의미하는 세련된 표현입니다. 그들은 만약 시스템이 정리를 유도할 수 있다면, 그 정리를 정당화하는 구체적인 코드(증명 항)를 자동으로 생성할 수 있음을 증명합니다. 이는 자율 주행 자동차가 상점에 갈 뿐만 아니라, 규칙을 준수하며 운전했음을 증명하기 위해 자신이 거친 모든 회전 경로에 대한 상세한 로그를 작성하는 것과 같습니다.

3단계 투어: 규칙에서 현실로

그들의 새로운 논리가 단지 환상이 아님을 확실히 하기 위해, 저자들은 독자를 세 가지 다른 관점으로 안내하며 이들이 모두 동일한 결과로 이어진다는 것을 증명합니다.

1. 규칙집 (공리계, Axiomatic System): 먼저, 그들은 헌법처럼 규칙을 작성합니다. 그들은 이 규칙들을 따르면 정리를 유도할 수 있음을 보여줍니다. 그들은 이 시스템이 "자기 내재적(self-internalizing)"임을 증명하는데, 이는 시스템이 주장하는 모든 것에 대해 항상 증명 코드를 생성할 수 있음을 의미합니다.
2. 작업실 (자연 연역, Natural Deduction): 다음으로, 그들은 "자연 연역" 시스템을 구축합니다. 이것을 가구를 조립하는 것처럼 단계별로 증명을 만들어가는 작업실이라고 생각하십시오. 그들은 모든 나무 조각(모든 항)이 특정 라벨(타입)을 가진 유형화된 버전($\lambda J\lambda$)을 도입합니다. 그들은 여기서 당신이 만드는 '증명'이 규칙집의 '증명 항'과 완벽하게 일치함을 보여줍니다. 이는 설명서의 지침이 상자 안의 실제 부품들과 일치함을 보여주는 것과 같습니다.
3. 공장 (순차 계산, Sequent Calculus): 마지막으로, 그들은 증명을 위한 고속 조립 라인과 같은 "순차 계산"을 만듭니다. 그들은 **컷 제거(cut-elimination)**라고 불리는 중요한 속성을 증명합니다. 간단히 말해, '컷(cut)'은 증명에서 중간 단계를 건너뛰는 것, 즉 어떻게 그 결과에 도달했는지 보여주지 않고 다른 곳에서 결과를 가져다 쓰는 것을 의미합니다. '컷 제거'는 이러한 지름길을 항상 제거하고 모든 단계를 처음부터 다시 보여주도록 증명을 재작성할 수 있음을 의미합니다. 저자들은 그들의 시스템이 항상 이 작업을 수행할 수 있음을 증명하며, 이는 시스템이 "정규화 가능(normalizable)"함을 보장합니다. 즉, 증명은 무한 루프에 빠지지 않고 결국 깨끗하고 표준적인 형태로 정착하게 됩니다.

왜 중요한가 (그리고 무엇이 아닌가)

저자들은 자신의 연구를 이전의 시도들과 구분하기 위해 매우 주의를 기울입니다. 과거에 연구자들은 논리와 계산을 연결하려고 시도했지만, 종종 벽에 부딪혔습니다. 논리가 컴퓨터 프로그램이 할 수 있는 복잡한 기술들을 처리하기에는 너무 단순했기 때문입니다. 저자들은 자신들의 시스템이 $\lambda$-계산(함수형 프로그래밍의 기초)으로부터 직접 구축되었기 때문에 독특하다고 지적합니다. 그들은 억지로 맞지 않는 조각을 끼워 맞출 필요가 없습니다. 논리와 코드는 동일한 재료로 만들어졌기 때문입니다.

그들은 또한 자신들의 시스템이 하지 못하는 일에 대해서도 명확히 밝힙니다. 그들은 모든 수학을 대체하거나 컴퓨터 과학의 모든 문제를 해결하려는 것이 아닙니다. 대신, 그들은 논리의 "부정 파편(negative fragment)"( '그리고'와 '함의'를 다룸)에 구체적으로 집중하고 있습니다. 그들은 이 특정 범위 내에서 자신들의 시스템이 완벽하게 작동함을 증명합니다. 그들은 자신들의 시스템에서 증명을 가져와 표준 컴퓨터 프로그램으로, 그리고 그 반대로 정보의 손실 없이 번역할 수 있음을 보여줍니다.

결론

길레잔과 파디아르는 '사실을 증명하는 것'과 '프로그램을 실행하는 것' 사이의 경계가 사라지는 새로운 논리적 프레임워크를 성공적으로 구축했습니다. 그들은 공리, 자연 연역 규칙, 그리고 순차 계산을 제공했으며, 이러한 서로 다른 관점들이 서로 일관됨을 엄격하게 증명했습니다. 그들은 이 시스템이 자신의 계산에 대해 추론할 수 있으며, 생성된 증명 항이 프로그램 그 자체와 구별할 수 없음을 보여주었습니다. 그들이 모든 논리적 미스터리를 해결했다고 주장하는 것은 아니지만, 컴퓨터가 자신의 코드를 수학적 증명으로서 진정으로 이해할 수 있는 견고하고 작동 가능한 모델을 제공함으로써, 미래의 더 강력하고 자기 검증적인 소프트웨어 시스템을 위한 문을 열어주었습니다.