What does it take to certify a conversion checker?

기술 요약: 변환 검사기(Conversion Checker)를 인증하는 데 필요한 것은 무엇인가?

문제 정의
증명 보조기 커널(증명을 검사하는 핵심 구성 요소)의 인증은 의존 타입 이론(Dependent Type Theory)에서 매우 중요한 과제입니다. "드 브뤼인 기준(de Bruijn criterion)"은 작은 커널에 신뢰를 둘 수 있게 해주지만, 커널 자체를 인증하는 것은 어렵습니다. 왜냐하면 의존 타입 이론은 복잡한 불변량(invariants)에 의 rely하기 때문입니다. 구체적으로, 변환 검사기(정의적 동등성 $\sim=$을 결정하는 것)의 정당성을 증명하는 것은 전통적으로 시스템의 정규화(reduction의 종료)를 증명할 것을 요구합니다. 그러나 괴델의 제2 불완전성 정리로 인해, 시스템은 자신의 일관성이나 정규화를 스스로 증명할 수 없습니다. 결과적으로, 시스템 내부에서 의존 타입 커널을 완전히 인증하는 것은 불가능합니다. 본 논문은 완전한 정규화 증명에 의존하지 않고, "우아한 실패(grace failure)"—즉, 더 약한, 증명 가능한 속성에 기반하여 검사기를 인증하는 것—를 목표로 하여, 변환 검사기를 인증하는 데 필요한 최소한의 메타 이론적 속성을 식별하고자 합니다.

방법론
저자들은 메타 이론(주입성 및 정규화와 같은 속성을 담은 "불투명한 도구 상자")과 알고리즘적 인증(검사기의 구현)을 분리하는 모듈식 접근 방식을 채택합니다.

1. 공식 체계: 본 연구는 의존 함수($\Pi$) 및 쌍($\Sigma$) 타입, 귀납적 타입(공집합, 자연수, 항등 타입), 그리고 대형 제거(large elimination)를 갖춘 마틴-뢰프 타입 이론(MLTT)의 버전을 위해 Rocq 증명 보조기(구 Coq)에서 공식화되었습니다.
2. 알고리즘: 두 가지 변환 검사 알고리즘이 구현 및 인증되었습니다:
   • 타입 기반 변환(Typed Conversion): Coq 및 Agda에 있는 것과 유사한 타입 지향적, 양방향 알고리즘으로, 검사 과정 전반에 걸쳐 타입 정보를 유지합니다.
   • 타입 미지정 변환(Untyped Conversion): Rocq 및 Lean과 유사한 용어 지향적 알고리즘으로, 용어의 축약(reduction) 중에 타입 정보를 유지하지 않지만, 정당성을 위해 타입이 지정된 명세(typed specification)에 의존합니다.
3. 인증 프레임워크: 알고식의 부분성(partiality)을 처리하기 위해 McBride의 자유 재귀 모나드(PartialFun 경유)를 사용하여 알고리즘을 구현했습니다. 저자들은 알고리즘의 전제 조건(불변량)과 사후 조건을 정의합니다. 정당성은 다음과 같이 분해됩니다:
   • 양의 건전성(Positive Soundness): 알고리즘이 "yes"를 반환하면, 두 용어는 변환 가능합니다.
   • 음의 건전성(Negative Soundness): 알고리즘이 "no"를 반환하면, 두 용어는 변환 가능하지 않습니다.
   • 종료성(Termination): 알고리즘은 항상 멈춥니다.

주요 기여
본 논문의 주요 기여는 타입 및 용어 생성자의 주입성(injectivity) 속성이 정규화와는 크게 독립적으로, 변환 검사기의 건전성을 인증하는 데 결정적이고 충분한 메타 이론적 속성임을 식별하고 입증한 것입니다.

• 핵심 요구사항으로서의 주입성: 저자들은 타입 생성자의 주입성(예: $\Pi x:A.B \sim= \Pi x:A'.B'$ 이면 $A \sim= A'$ 이고 $B \sim= B'$)과 혼란 부재(no-confusion)(예: $\Pi x:A.B$는 $N$과 변환 가능할 수 없음)가 양의 건전성을 증명하는 데 충분함을 보여줍니다.
• 용어 수준의 주입성: 음의 건전성을 증명하기 위해, 저자들은 용어 생성자(특히 자연수와 $\Pi$ 타입)의 주입성 속성과 중립 비교의 완결성(convertible한 neutral들이 구조적으로 비교될 수 있음을 보장함)이 필요함을 입증합니다.
• 타입 지정 vs 미지정의 동등성: 본 논문은 타입 미지정 변환 검사기를 타입이 지정된 명세에 대해 인증하는 새로운 사례를 제시합니다. 이는 "타입 미지정" 변환이 사실상 "용어 지향적 타입 지정 변환"임을 명확히 하며, 여기서 타입 정보는 축약 단계가 아닌 불변량 속에 암시적으로 존재합니다.
• 의존성 분석: Rocq의 타입 클래스를 사용하여, 저자들은 어떤 메타 이론적 속성(주입성, 정규화 등)이 각 알고리즘적 속성(건전성, 종료성)에 필요한지에 대한 세밀한 의존성 맵(논문의 그림 1)을 제공합니다.

결과
공식화(기존 Rocq 베이스에 약 1만 줄의 코드 추가)를 통해 다음과 같은 구체적인 결과가 도출되었습니다:

1. 양의 건전성: 타입 생성자의 주입성만을 사용하여 두 알고리즘 모두에 대해 증명되었습니다. 이 속성은 논리적 일관성을 함의하지 않으며, 대상 이론(object theory)보다 약한 메타 이론에서도 증명될 수 있습니다.
2. 음의 건전성: 타입 및 용어 생성자의 주입성과 중립 비교의 완결성을 사용하여 증명되었습니다.
   • 타입 기반 알고리즘의 경우, 중립 비교의 완결성은 **양의 타입(positive types)**에서만 요구됩니다(속성 9).
   • 타입 미지정 알고리즘의 경우, 부정적 타입(negative types)의 $\eta$-확장을 안내할 타입 정보가 없기 때문에 모든 타입에서 완결성이 요구됩니다(속성 7).
3. 종료성: 깊은 정규화(deep normalisation)(속성 11)를 가정하여 두 알고리즘 모두에 대해 증명되었습니다. 이 속성은 유일하게 논리적 일관성을 함의하며, 대상 이론보다 강한 메타 이론을 필요로 합니다.
4. 동등성: 저자들은 두 알고리즘이 동등함을 증명합니다(명제 22 및 24). 이 증명은 강화(strengthening)(컨텍스트에서 무관한 변수를 제거함)와 정규화에 의존합니다. 타입 미지정 알고리즘은 타입 지정 명세의 유효한 구현임이 입증되었습니다.

의의 및 주장
본 논문은 타입 검사기 인증의 "핵심(keystone)"이 전체 정규화 증명이 아니라, 타입 시스템의 주입성 속성이라고 주장합니다.

• 우아한 실패: 저자들은 괴델적 한계로 인해 정규화를 증명할 수 없더라도, 검사기의 건전성은 여전히 인증할 수 있다고 주장합니다. 이를 통해 주입성을 공리로 가정하거나 더 약한 메타 이론에서 증명함으로써, 복잡하고 최적화된 구현체(Rocq나 Lean과 같은)를 인증할 수 있습니다.
• 모듈성: 본 연구는 "메타 이론을 블랙박스로 취급하는" 접근 방식을 옹호합니다. 알고리즘의 인증은 전체 타입 이론의 거대한 증명이 아니라, 주입성이나 중립의 완결성과 같이 공리화된 작은 속성 집합에 의존해야 합니다.
• 타입 미지정 인증: 본 논문은 용어 지향적(untyped) 검사기를 인증하는 것이 가능하며, 타입 지정과 타입 미지정 변환의 차이는 타입의 부재라기보다는 알고리즘의 방향(용어 지향 vs 타입 지향)에 관한 것임을 보여줍니다.
• 한로: 저자들은 자신들의 작업이 단순화된 MLTT 버전을 다루고 있음을 겸허히 밝힙니다. 그들은 정의적 단위 타입(모든 거주자가 변환 가능한 경우)이나 엄격한 명제(증명 무관성)와 같은 기능들이 중립 비교의 완결성을 복잡하게 만들 수 있으며, 이를 위해 타입 재추론이나 유니버스 추적과 같은 특정 전략이 필요함을 인정합니다. 또한, 확장적(extensional) 또는 큐비컬(cubical) 타입 이론이 강화 및 중립 완결성과 관련하여 추가적인 과제를 제시한다는 점도 언급합니다.

요약하자면, 본 논문은 주입성을 건전성의 충분 조건으로 격리함으로써, 변환 검사기의 인증을 어려운 전체 정규화 증명으로부터 분리하는 로드맵을 제공합니다.