Setoids in Intensional Type Theory

기술 요약: 내포적 유형론에서의 세토이드(Setoids)

문제 제기
본 논문은 내포적 유형론(Intensional Type Theory, ITT) 내에서 외연적 유형론(Extensional Type Theory with Universes, ETU)의 모델을 구축하는 데 따르는 과제를 다룬다. ITT(특히 --safe 및 --without-K 옵션이 적용된 Agda에서 구현된 버전인 IRU로 지칭됨)는 구문론과 메타 이론을 형식화하는 데 널리 사용되지만, ETU에 내재된 함수 외연성(function extensionality)이나 항등 증의 유일성(uniqueness of identity proofs)과 같은 외연성 원칙이 결여되어 있다. 저자는 기존 문헌에 외연성을 위한 세토이드 모델들이 존재하지만, 순수한 IRU 시스템 내에서 ETU의 의미론을 완전히 기계적으로 검증된 방식으로 구축한 사례는 없음을 지적한다. Palmgren (2022)과 같은 기존의 접근 방식들은 의미론적 함수와 건전성 증명을 암시적으로 남겨두거나, 더 복잡한 일관성 조건(coherence conditions) 또는 집합론적 해석에 의존한다. 또한, ITT에서 잘 정의된 식(well-formed expressions)의 의미론을 정의하는 것은(단순히 잘 정의됨의 유도 과정을 넘어) 명제적 동등성(propositional equality)에 대한 정의적 동등성(definitional equality)의 부재로 인해 "놀라운 기술적 어려움"을 야기하며, 이는 부분 함수(partial functions)와 증명 무관성(proof irrelevance)을 신중하게 다루는 것을 요구한다.

방법론
본 논문은 IRU 내에서 의존 유형(dependent types)을 모델링하기 위해 "표시된 세토이드(displayed setoid)" 접근 방식을 채택한다. 방법론은 다음과 같이 진행된다:

1. 프레임워크 (IRU): 구축은 의존 함수 유형, 의존 레코드 유형, 그리고 (inductive-recursive 정의로 닫힌 유니버스 계층을 포함하는) 귀납적 데이터 유형(--without-K 포함)을 포함하는 Safe Agda (IRU)에서 수행된다.
2. 표시된 세토이드 (Displayed Setoids): 핵심적인 혁신은 "표시된 세토이드"(정의 3.2)라는 특정 개념의 사용이다. 복잡한 일관성 조건이나 증명 무관한 명제(SProp)를 요구하는 이전의 접근 방식들과 달리, 이 정의는 동치 관계가 Set 값을 갖는 "와일드(wild)" 세토이드를 사용한다. 증명 무관한 명제에 의존하지 않고 유형의 항(term)에 대한 의존성을 처리하기 위해, 저자들은 동치 관계의 의존적 곱(dependent product)을 데카르트 곱(cartesian product)으로 대체한다. 이는 이질적(heterogeneous) 동등성의 명시적 처리와 의존 유형론의 변환 규칙(conversion rule)을 관리하기 위한 강제(coercion, coe) 및 일관성(coherence, coh) 항의 포함을 필연적으로 수반한다.
3. 세토이드 유니버스: 저자들은 귀납적-재귀적(inductive-recursive) 정의를 사용하여 가산적인 세토이드 유니버스 계층($U_l$)과 그에 연관된 표시된 세토이드($E\ell_l$)를 구축한다. 이 유니버스들은 다음의 코드들을 포함한다:
   • 자연수와 공집합 유형(empty type).
   • 외연적 동등성 유형(extensional equality types).
   • $\eta$-변환을 포함하는 의존 곱 유형($\Pi$-types).
   • 유니버스 자체의 계층.
   • 결정적으로, 타이핑 컨텍스트(typing contexts)의 코드를 위한 별도의 세토이드 유니버스($C$). 이는 컨텍스트의 정의적 동등성을 모델링할 수 있게 한다.
4. 구문 표현: ETU의 구문은 "잘 범위 지정된 로컬리 네임리스(well-scoped locally nameless)" 표현을 사용하여 외연적으로 정식화된다. 컨텍스트, 유형, 항의 잘 정의됨(well-formedness)에 대한 판단(judgements)은 Agda에서 귀납적 데이터 타입으로 정의된다.
5. 의미론 구축: Streicher (1991)의 전략을 따라, 저자들은 가공되지 않은 구문(raw syntax)에 대해 부분적 의미론 함수를 정의한다. 그 후, 이 관계들이 모든 잘 정의된 식에 대해 전역적(total)이고 단일 값(single-valued, 세토이드 관점에서)임을 증명한다. 이는 컨텍스트, 유형, 항에 대한 의미론적 관계를 정의하고, 정의적 동등성에 대해 이들의 건전성(soundness)을 증명하는 과정을 포함한다.

주요 기여

• 표시된 세토이드 정의: 본 논문은 Palmgren (2022)에서 발견되는 복잡한 일관성 조건을 피하고 증명 무관한 명제의 유니버스를 필요로 하지 않는, 단순화된 표시된 세토이드 정의(정의 3.2)를 도입한다. 이는 이질성을 관리하기 위해 데카르트 곱과 명시적인 일관성 항에 의존한다.
• 컨텍스트 유니버스: 이 구축은 타이핑 컨텍스트의 코드($C$)를 위한 세-토이드 유니버스를 포함하며, 저자는 이것이 이 맥락에서 새로운 기능이라고 언급한다. 이를 통해 컨텍스트 동등성에 대한 직접적인 의미론적 처리가 가능하다.
• IRU에서의 완전한 의미론: 본 논문은 IRU 내에서 ETU의 의미론에 대한 완전한 기계 검증된 정식화를 제공한다. 여기에는 모든 유형 형성자(특히 $\Pi$-타입 및 외연적 동등성 포함)에 대한 의미론적 함수를 정의하고, 그 성질(전역성, 단일 값성, 건전성)을 증명하는 과정이 포함된다.
• 일관성 증명: 의미론의 직접적인 결과로서, 본 논문은 IRU 내에서 ETU의 일관성을 도출하는 기계 검증된 증명을 제공한다.

결과

• 정리 6.8 (일관성): 본 논문은 $\neg (\Sigma_{a \in \text{Tm}} (\diamond \vdash a :_0 \text{Emp}))$ 타입의 IRU 항이 존재함을 증명한다. 이는 ETU가 IRU에 대해 일관적임을 확립한다. 이 증명은 공집합 유형의 의미론적 해석이 진정으로 비어 있음(unit 타입에서 empty 타입으로 가는 함수)을 이용하며, 공집합의 원소가 존재한다는 유도가 모델 내에서 모순을 초래할 것임을 근거로 한다.
• 건전성: 의미론적 관계는 ETU의 정의적 동등성 규칙에 대해 건전함이 증명된다(정리 6.7 및 섹션 6.5). 구체적으로, 두 항이 ETU에서 정의적으로 동등하다면, 그들의 의미론적 해석은 대응하는 세토이드 내에서 동등하다.

의의
본 논문은 주로 기초론적 측면에서 그 의의를 주장한다. 이는 외연성에 의존하는 언어들의 의미론적 구축이 얼마나 내포적 유형론 내에서 수행될 수 있는지를 명확히 한다.

• 기초론적 관심: 이는 "Streicher의 영감을 받은" 외연적 유형론의 의미론이 외연성 공리나 복잡한 쿼션 귀납적 유형(quotient inductive types)을 가정하지 않고도 매우 최소한의 내포적 설정(IRU)에서 달성될 수 있음을 보여준다.
• 실용적 정식화: 본 연구는 이러한 개념들을 Safe Agda에서 기계적으로 검증 가능한 방식으로 정식화한 사례이며, 더 강력한 논리적 가정을 사용하지 않고도 내포적 의미론(예: 부분 함수 및 증명 무관성)의 기술적 어려움을 처리하는 구체적인 방법을 제시한다.
• 메타 이론: 이 작업은 다양한 언어의 구문을 표현하고 그 메타 이론을 조사하기 위해 내포적 유형론을 사용하는 것을 뒷받침하며, 외연적 속성들이 세토이드를 통해 내부적으로 모델링될 수 있음을 보여준다. 저자는 이 모델이 직접적인 계산적 응용을 가질 수는 없으나, 내포적 시스템에서 외연성의 상대적 일관성을 이해하고, 의존 유형론에서의 정규화-바이-평가(normalization-by-evaluation)와 같은 구성의 내포적 버전에 관한 향후 연구를 위한 필수적인 단계라고 언급한다.