Definitional Inversion, Without Normalisation

기술 요약: 정규화 없는 정의적 역전 (Definitional Inversion, Without Normalisation)

문제점
의존 타입 시스템은 중요한 증명 보조기(Agda, Lean, Rocq)와 프로그래밍 언어(Idris, dependent Haskell)의 근간을 이룹니다. 이러한 시스템의 메타 이론적 성질, 특히 정의적 역전 원리(정의적 생성자의 단사성 및 혼동 없음)를 확립하는 것은 건전성(soundness), 타입의 유일성, 그리고 커널 검증을 입증하는 데 필수적입니다. 그러나 기존의 메타 이론적 도구들은 심각한 한계에 직면해 있습니다:

1. 합류성 기반 접근법 (Confluence-based approaches): 현대적인 $\eta$-법칙(laws)과 같은 기능들을 다루는 데 어려움을 겪습니다. 합류성은 $\beta$-축약(reduction)에는 작동하지만, 타입 변환(typed conversion) 및 $\eta$-법칙(예: 함수나 쌍에 대한 법칙)을 혼합하면 비합류적 시스템이 되거나 복잡하고 비표준적인 제시 방식이 필요하게 됩니다.
2. 정규화 기반 접근법 (Normalisation-based approaches, 논리적 관계): 전통적인 논리적 관계(logical relations)는 정규형(normal forms)의 존재에 의존합니다. 이는 비정규화 타입 이론(non-normalising type theories, 예: Type:Type이나 고정점 결합자(fixed-point combinators)를 사용하는 경우)에서는 실패합니다. 또한, 정규화를 증명하기 위해서는 대상 논리(object logic)보다 더 강력한 주변 논리(ambient logic, 예: 귀납-재귀(induction-recursion)나 다수성(impredicativity)을 포함하는)가 필요하며, 이는 증명 보조기 자체 내에서 자신의 메타 이론을 연구하는 것(예: Lean4Lean, MetaRocq)을 불가능하게 만듭니다.

본 논문은 MLTT$\eta$의 구체적인 사례를 다룹니다. 이는 의존 곱($\Pi$), $\beta$ 및 $\eta$ 방정식, 그리고 Type:Type 우주(universe)를 갖는 마틴-뢰프(Martin-Löf) 타입 이론의 변형입니다. 이 시스템은 $\eta$로 인해 합류성이 깨지고, Type:Type으로 인해 정규화가 불가능하여, 그 정의적 역전 성질이 아직 증명되지 않은 상태입니다.

방법론
저자들은 도메인 이론(domain theory), 특히 **유한 투영 모델(finitary projection models)**을 활용한 새로운 증명 기법을 제안합니다. 핵심 통찰은 타입을 정규형(존재하지 않을 수도 있는)이 아니라, 스코트 도메인(Scott domain) 내의 컴팩트 요소(compact elements)를 통한 "관측 가능한 행동"으로 해석하는 것입니다.

1. 도메인 구축: 저자들은 타입 생성자($\Pi$, $\mathcal{U}$ 등)를 나타내는 재귀적 도메인 방정식의 해로서 도메인 $D$를 구축합니다. 이 도메인은 증가하는 유한 근사 순서($C_n$)의 극한으로 구축되며, 여기서 요소들은 컴팩트(finite observations를 나타냄)합니다.
   • 결정적으로, 이 모델은 함수에 대한 $\eta$-법칙을 만족시키기 위해 $\bot$을 $\lambda x.\bot$과 동일시하는 한편, $\Pi$-생성자를 $\mathcal{U}$와 구별하여 상호 배타성을 보장합니다.
2. 의미론적 타이핑 (Semantic Typing): 도메인의 컴팩트 요소들 위에 의미론적 타이핑 관계를 정의합니다. 이 관계는 유한 투영기(finitary projectors)(연속 사상 $p: D \to D$로서 $p(\alpha) \le \alpha$이고 $p(p(\alpha)) = p(\alpha)$를 만족하는 사상)를 사용하여 공식화됩니다. 타입은 유한 투영기로 해석되며, 항(term)은 해당 투영자의 고정점(fixed point)을 가질 때 타입과 연관됩니다.
3. 논리적 관계 (Logical Relation): 구문적 항과 의미론적 증거(컴팩트 요소) 사이의 논리적 관계를 정의합니다. 전통적인 논리적 관계가 타입의 정규형을 재귀적으로 탐색하는 것과 달리, 이 관계는 컴팩트 요소의 단계(stage) $n$과 의미론적 증거의 구조를 따라 재귀적으로 정의됩니다.
   • 이 관계는 중립적 항(neutral terms)을 $\bot$으로 해석함으로써 열린 항(open terms)을 처리하며, 이를 통해 키르케(Kripke) 스타일의 양화(quantification) 없이도 열린 문맥에서의 역전을 지원하면서도 복잡성을 피합니다.
   • 관계는 **헤드 축약(head reduction)**까지 고려하여 $\beta$ 및 $\eta$ 규칙을 논리적 관계의 구조 안에 직접 포함합니다.
4. 적절성 (Adequacy): 저자들은 **적절성 정리(adequacy theorem)**를 증명합니다. 즉, 두 항이 구문적으로 동등하다면 논리적 관계 내에서 서로 연관됩니다. 이를 통해 도메인 요소의 상호 배타성으로부터 구문적 성질(예: 단사성)을 도출할 수 있습니다.

주요 기여

• 새로운 증명 기법: 정규화나 합류성에 의존하지 않고 정의적 역전(단사성 및 혼동 없음)을 증명하는 도메인 이론적 방법을 제시합니다.
• $\eta$ 및 비정규화 처리: 이 기법은 $\eta$-법칙과 Type:Type(또는 고정점 결합자)이 공존하는 시스템에 대해서도 단사성을 성공적으로 증명합니다. 이는 기존 방식으로는 다루기 힘들었던 조합입니다.
• 약한 주변 논리: 이 증명은 자연수에 대한 기초적인 귀납법만을 사용하며, 정규화 증명에 필요한 강력한 논리적 원리(예: 귀납-재귀)를 피합니다. 이는 자기 검증 프로젝트(예: Lean 내부에서 Lean의 성질을 증명하는 것)에 적합합니다.
• 확장성: 본 기법은 MLTT$\eta$에 대해 시연되었으며, 다음과 같은 더 풍부한 이론들로 확장 가능함을 보여주었습니다:
  • $\eta$-법칙을 갖는 의존 합($\Sigma$) 및 단위 타입($1$).
  • 고정점 결합자($Y$)를 통한 일반 재귀.
  • 패턴 매칭을 갖는 자연수($\mathbb{N}$).
  • 전송(transport)을 갖는 증명 관련 항등 타입($Id$).
  • 정의적 증명 무관성(definitional proof irrelevance)을 갖는 엄격한 명제($Prop$) 우주.
• 기계화 (Mechanisation): 위에서 언급된 다양한 확장들을 포함하여 Agda, Lean, Rocq에서 기계화되었습니다.

결과

• $\Pi$의 단사성: 본 논문은 $\Pi x:A.B \equiv \Pi x:A'.B'$이면 $A \equiv A'$ 이고 $B \equiv B'$임을 증명합니다.
• 상호 배타성 (Disjointness): 타입 생성자들은 서로 배타적입니다 (예: $\Pi x:A.B \not\equiv \mathcal{U}$).
• 주제 감소 (Subject Reduction) 및 진행 (Progress): 역전 원리의 결과로서, 저자들은 진행 및 보존 정리를 도출하여 프로그래밍 언어로서의 언리의 건전성을 확립합니다.
• UIP의 실패: 이 모델은 항등 증명의 유일성(UIP/K-rule)이 이 시스템에서 도출될 수 없음을 보여줍니다. 이는 도메인 모델이 항등의 서로 다른 증거들을 구분하기 때문입니다.

의의
본 논문은 의존 타입 시스템의 메타 이론에서 존재하는 "사각지대"를 채운다고 주장합니다. 정의적 역전을 정규화로부터 분리함으로써, 이 기법은 현대적인 증명 보조기와 프로그래밍 언어에서 흔히 볼 수 있는 풍부한 방정식 이론(예: $\eta$) 및 비정규화 시스템을 엄밀하게 연구할 수 있는 길을 열어줍니다.

저자들은 이 작업을 Lean4Lean 및 MetaRocq와 같은 프로젝트를 위한 기초적인 단계로 위치시킵니다. 이 프로젝트들은 괴델의 제2 불완전성 정리로 인해 대상 논리의 정규화를 가정할 수 없으므로, 이러한 도메인 이론적 접근 방식은 더 강력한 주변 논리를 요구하지 않고도 커널을 검증하고 타입 체크 알고리즘의 정확성을 보장할 수 있는 실행 가능한 경로를 제공합니다. 또한 저자들은 비종료(non-terminating) 특징이나 점진적 타이핑(gradual typing)을 사용하는 의존 타입 프로그래밍 언어에 대한 잠재적 응용 가능성도 제시합니다.