A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

기술 요약: 부적격적 순수 유형 체계(Impredicative Pure Type Systems)의 일관성에 대한 기계 검증된 증명

문제 및 배경
본 논문은 유형 이론(type theory)을 기계화하는 과정에서의 어려움, 특히 순수 유형 체계(Pure Type Systems, PTS)의 메타 이론적 속성에 초점을 맞춘 문제를 다룹니다. 치환(substitution)과 $\beta$-축약($\beta$-reduction)을 정형화할 때 발생하는 핵심적인 어려움은 이름 캡처를 방지하기 위한 변수 이름 변경(variable renaming)을 처리하는 것입니다. 전통적인 정의(예: Curry-Feys)는 비원시 재귀적(non-primitive recursive)인 이름 변경 단계로 인해 항의 길이에 대한 잘 정립된 귀납법(well-founded induction)을 요구하며, 이는 기계화를 어렵게 만듭니다. de Bruijn indices (dBI), 로컬리 네임리스(locally nameless) 구문, 또는 고차 추상 구문(Higher-Order Abstract Syntax, HOAS)과 같은 대안적 접근 방식들은 해결책을 제시하지만, 각각 고유한 단점들을 수반합니다. dBI는 인간이 읽기에 번거롭고, 로컬리 네임리스 구문은 메타 이론적 결과에 "오염"을 일으키는 적절성 술어(well-formedness predicates)를 필요로 하며, HOAS는 실행 가능한 코드의 생성이나 결정 가능성 문제의 정식화를 방해하는 경우가 많습니다.

저자들은 고전적 구문(이름이 있는 변수 사용)을 유지하면서 **Stoughton의 동시 치환(simultaneous substitutions)**을 활용하는 접근 방식의 타당성을 평가하고자 합니다. 이 방법은 변수 이름 변경을 단일 구조적 재귀를 통해 치환과 동시에 수행함으로써, 대부분의 증명에서 항의 길이에 대한 잘 정립된 귀납법을 사용할 필요 없이 이를 수행합니다.

방법론
본 개발은 Agda(v2.6.2.2)와 표준 라이브러리를 사용하여 완전히 기계 검증되었습니다. 방법론은 다음의 핵심 구성 요소에 의존합니다:

1. Stoughton의 동시 치환: 치환은 변수에서 $\lambda$-항으로의 함수($Sub = V \to \Lambda$)로 정의됩니다. 연산 $M \bullet \sigma$는 구조적 재귀에 의해 정의됩니다. $\lambda$-추상화와 $\Pi$-타입의 경우, 결합된 변수는 함수 $X$에 의해 선택된 새로운 이름 $y$로 이름이 변경되며, 치환은 기존의 결합된 변수를 이 새로운 이름으로 매핑하도록 업데이트됩니다. 이는 각 추상화당 단 한 번의 재귀 호출만을 보장하여 원시 재귀성을 유지합니다.
2. $\alpha$-교환 관계($\alpha$-Commutative Relations): 저자들은 $\alpha$-변환과 교환되는 관계 이론을 개발합니다. 관계 $S$가 $\alpha$-교환적이라는 것은 $M \sim_\alpha N$이고 $N S P$이면 $M S Q$이고 $Q \sim_\alpha P$를 만족하는 $Q$가 존재함을 의미합니다. 이 프레임워크를 통해 저자들은 $\alpha$-변환까지의 합류성(confluence)을 깔끔하게 처리할 수 있으며, 다른 정식화에서 흔히 보이는 관계의 중복을 피할 수 있습니다.
3. Takahashi의 합류 증명 수정: 저자들은 원래의 Tait 및 Martin-Löf 증명 대신, 병렬 축약(parallel reduction, $\Rightarrow$)을 사용하는 Takahashi의 수정된 방식을 채택합니다. 저자들은 축약 단계에서 명시적인 $\alpha$-변환 규칙 없이 병렬 축약을 정의하고, 대신 펜타곤 성질(pentagon property, $\alpha$-변환까지의 다이아몬드 성질의 일반화)을 이용하여 합류성을 증명합니다.
4. 정규화 가정(Normalization Assumption): 일관성 증명은 고려 중인 특정 PTS가 정규화 가능(모든 잘 정형화된 항이 약한 정규화 가능함)하다는 것을 가정합니다. 저자들은 부적격적 시스템에 대한 정규화 증명을 Agda 내에서 수행하는 것은 Agda의 메타 언어가 부적격성을 갖지 못한다는 점 때문에 불가능할 것이라고 언급합니다.

주요 기여
본 논문은 세 가지 주요 메타 이론적 속성에 대한 정식 증명을 제시합니다:

1. $\beta$-축약의 합류성(Confluence): 저자들은 PTS의 기저 구문에 대한 Church-Rosser 정리를 증명합니다. $\alpha$-교환 관계 이론과 Takahashi의 병렬 축약을 활용하여, 병렬 축약의 스타 폐쇄(star closure)가 다단계 $\beta$-축약과 일치하며 펜타곤 성질을 만족함을 입증합니다.
2. 주제 축약(Subject Reduction, SR): 본 논문은 축약에 따른 유형 보존을 정식화합니다. McKinna와 Pollack의 아이디어를 따라, 저자들은 컨텍스트(context)로 축약을 확장하고 컨텍스트의 유효성과 주체의 유형 보존에 관한 동시 정리를 증명합니다. 여기에는 역전을 위한 핵심 렌마인 곱 타입 인젝티비티(product injectivity) 증명이 포함됩니다.
3. 부적격적 PTS에 대한 일관성: 저자들은 특정 부적격적 PTS(특정 공리 및 규칙을 만족하는 클래스, 예: $(\ast, \square) \in \mathcal{A}$ 및 $(\square, \ast, \ast) \in \mathcal{R}$)에 대해, 빈 컨텍스트에서 타입 $\Pi[x : s]x$(커리-하워드 대응 하의 거짓을 나타냄)가 거주 불가능함을 증명합니다. 이 증명은 Coquand의 펜과 종이 증명을 확장한 것입니다. 이는 귀납적으로 정의된 정규 형태(normal form) 및 중립 형태(neutral form)의 건전성과 완전성, 역전 렌마, 그리고 가정된 정규화 성질에 의존합니다.

결과 및 평가

• 정식화 크기: 전체 개발은 약 **4,300행의 코드(LoC)**로 구성되며, 그 중 3,000행은 이전 작업의 Stoughton 치환 및 PTS 구문 기반 프레임워크에 기인합니다.
• 비교: 저자들은 de Bruijn indices를 사용한 정식화(Barras 및 Werner, ~2,900 LoC) 및 로컬리 네임리스 구문을 사용한 정식화(Aydemir 등, ~4,800 LoC)와 본 연구를 비교합니다. 저자들은 자신들의 접근 방식이 크기는 비슷하면서도, 용어의 개방(opening terms)을 관리하거나 신선한 파라미터를 수동으로 관리할 필요가 없으므로 사용된 구문에 대해 더 높은 투명성을 제공한다고 주장합니다.
• 타당성: 결과는 고전적 구문과 동시 치환을 사용하는 접근 방식이 의존 유형 이론(dependent type theories)에 대해 실현 가능하다는 것을 시사합니다. 저자들은 단 몇 개의 렌마만이 잘 정립된 귀납법을 필요로 했으며, 코드 크기가 폭발적으로 증가하지 않았음을 언급했습니다.

의의 및 주장
본 논문은 Stoughton의 치환을 사용하는 접근 방식이 특히 $\alpha$-변환 처리에 있어 유사한 개발들에 비해 메타 이론적 문제에 대해 "더 명확한 제시와 처리"를 제공한다고 주장합니다. 저자들은 자신들의 솔루션이 용어의 개방을 다루거나 신선한 파라미터를 수동으로 관리하는 번거로움 없이, 인간 독자에게 더 투명하며 고전적인 표기법(예: 약화 렌마가 고전적 표기와 거의 동일함)과 밀접하게 닮아 있다고 주장합니다.

본 연구의 의의는 정규화가 가정된다면 고전적 구문을 포기하지 않고도 부적격적 시스템에 대한 기계 검증된 일관성 증명이 가능하다는 것을 보여준 데 있습니다. 저자들은 부적격적 이론에 대한 완전한 정규화 기계화는 Gödel의 불완전성 정리의 영향으로 인해 Agda의 증명론적 강도 제한으로 인해 불가능할 수 있음을 겸허히 인정하지만, 일관성 증명 자체는 이러한 시스템을 위한 '정답 기반(correct-by-construction)' 타입 체킹 알고리즘을 향한 실질적인 단계임을 강조합니다. 이 연구는 향후 의존 유형 이론의 정식화를 위한 프레임워크의 유용성을 검증하는 역할을 합니다.