Directed proof-relevant logical relations in simplicial HoTT

기술 요약: 심플리셜 HoTT에서의 유향 증명-관련 논리 관계 (Directed Proof-Relevant Logical Relations in Simplicial HoTT)

문제 정의
전통적인 증명-관련 논리 관계(종종 범주적 글루잉(categorical gluing)을 통해 정식화됨)는 타입을 계산 가능한 항들의 패밀리로 해석하며, 여기서 계산 가능성 술어는 단순한 명제가 아닌 타입의 패밀리이다. 등식적 제시(equational presentations)를 갖는 타입 이론에서, 판단적 등식(judgmental equality)은 메타 수준의 등식으로 표현된다. 논리 관계는 "확장의 폐쇄성(closure under expansion)" 레마에 의존한다: 만약 항 $M$이 $M'$으로 축약되고($M \to M'$), $M'$이 계산 가능하다면, $M$ 또한 계산 가능하다. 그러나 이 접근 방식은 계산을 (등식을 통한) 대칭적 관계로 취급하거나, 수동적인 역방향 폐쇄성 증명에 의존한다. 이는 축약의 유향적(directed) 성질—즉, 항이 다른 항으로 단계적으로 이동하지만($M \to M'$), 그 역은 반드시 성립하지 않는 성질—을 내부적으로 다루지 못한다. 본 논문은 외부의 축약 관계나 증명-무관한 확장 레마에 의존하지 않고, 축약의 유향적 성질을 내부적으로 설명할 수 있는 증명-관련 논리 관계를 구축하는 과제를 다룬다.

방법론
저자들은 유향 간격(directed interval)과 부등식 타입($x \leq_A y$)을 포함하는 HoTT의 유향 확장인 심플리셜 호모토피 타입 이론(simplicial HoTT) 내에서 프레임워크를 개발한다.

1. 유향 구문 (Directed Syntax via Directed QIITs):
   대상 언어(object-language) 구문은 **유향 몫 유도-유도 타입(directed quotient inductive-inductive type, directed QIIT)**으로 제시된다. 일반적인 QIIT가 몫을 판단적 등식(경로 생성자)으로 취하는 것과 달리, 이 구문은 부등식 타입을 생성하는 **유향 생성자(directed constructors)**를 포함한다. 예를 들어, 곱(product)에 대한 $\beta$-축약은 다음과 같이 부등식으로 내부화된다:
   $$\times\beta_1 : \text{fst}(\text{pair } a \, b) \leq a$$
   구문은 "얇은 세갈 타입(thin Segal type)"으로 구성되어, 축약이 합성되고 동일한 끝점 사이의 부등식은 유일함(증명-무관함)을 보장하며, 이는 일반적인 범주가 아닌 전순서(preorder)를 모델링한다.

2. 공변성으로서의 증명-관련 확장 (Contravariance as Proof-Relevant Expansion):
   심플리셜 타입 이론에서 **공변 패밀리(contravariant families)**가 증명-관련 확성을 위한 정확한 구조를 제공한다는 것이 핵심적인 이론적 통찰이다. 이 설정에서, 타입 $A$에 대한 계산 가능성 술어 $A^\bullet$는 단순히 타입의 패밀리가 아니라, 반드시 공변 패밀리여야 한다.

   • 정의: 패밀리 $C: X \to \mathcal{U}$가 공변적이라는 것은, 모든 부등식 $f: x \leq_X y$와 증거 $v: C(y)$에 대하여, 리프트(lift)의 타입 $\sum_{u:C(x)} u \leq_{C(f)} v$가 수축 가능(contractible)함을 의미한다.
   • 함의: 이 수축 가능성은 유일하고 함수적인 "역방향 수송(backward transport)" 연산 $f^*: C(y) \to C(x)$를 보장한다. 이 연산은 확장 레마를 내부화한다: 계산 가능성 증거는 항이 축약되는 경로를 따라 자동으로 항등성과 합성을 준수하며 역방향으로 수송될 수 있다.

3. 의존 타입 및 유니버스 처리 (Handling Dependent Types and Universes):
   이를 의존 타입으로 확장하면 충돌이 발생한다: 타입 변환(type conversion)은 대칭적 등식을 요구하지만, 구문은 유향 부등식만을 제공하기 때문이다.

   • 이산화 (Discretization): 저자들은 타입 유니버스($Ty$)를 타입 부등식을 등식으로 바꾸는 생성자를 추가하여 이산화한다($A \leq Ty B \implies A = Ty B$). 이를 통해 유향 축약을 유지하면서도 표준적인 타입 변환을 허용한다.
   • 플랫 모달리티 (Flat Modality): 유니버스 술어의 증명-관련성을 유지하면서도 이산성을 잃지 않기 위해, 저자들은 크리스프(crisp) 타입 이론의 **플랫 모달리티($\flat$)**를 사용한다. 유니버스에 대한 계산 가능성 술어는 플랫 코드(flat codes)로 저장된다. $\flat X$는 이산적이므로, 술어 사이의 부등식은 등식으로 붕괴되며, 이는 유니버스의 계산 가능성 증거에 필요한 유일성을 보장한다.

주요 기여

1. 유향 몫 구문: 판단적 축약을 유향 부등식으로 내부화하는 타입 이론 구문의 형식화.
2. 공변성으로서의 확장: 심플리셜 타입 이론에서 공변 패밀리를 확장 레마의 증명-관련 일반화로 식별하여, 역방향 수송을 위한 내재적 함수성과 보편 성질을 제공함.
3. 단항 논리 관계 모델: 유향 불리언 정형성(directed Boolean canonicity)을 입증하는 단항 논리 관계 모델 구축: 모든 닫힌 불리언 항 $M$은 $M \leq \text{true}$ 또는 $M \leq \text{false}$를 만족한다.
4. 기계화 (Mechanization): 단순 타입 파편(곱, 함수, 불리언)에 대한 Cubical Agda에서의 개념 증명 기계화 구현.
5. 의존 타입 및 유니버스로의 확장: 타입 이산화와 플랫 모달리티를 사용하여 의존 타입 문제를 해결함.
6. 이항 파라메트릭성 (Binary Parametricity): 수직적 축약(공변성)과 수평적 파라메트릭성을 분리하는 이항 논리 관계의 적응, 큐(queue)의 표현 독립성 논증을 통해 입증.

결과

• 유향 정형성 (Directed Canonicity): 유향 설정에 대한 논리 관계의 기본 정리가 확립되었다. 임의의 닫힌 불리언 항 $M$에 대해, 모델은 $M$이 정형적인 불리언으로 축약된다는 증거를 제공한다.
• 표현 독립성 (Representation Independence): 이항 논리 관계는 수직적 차원(축약/공변성)과 수형적 차원(파라메트릭성)을 성공적으로 분리하여, 관계가 지그재그(zig-zag)가 아닌 스팬(span)이 되는 증명-관련 표현 독립성을 가능하게 한다.
• 기계화: 유향 구문과 논리 관계 모델의 구축을 포함한 단순 타입 파편이 Cubical Agda에서 형식화되었다.

의의 및 주장
본 논문은 구문이 등식이 아닌 축약에 의해 제시될 때도 논리 관계가 정형성과 파라메트릭성을 검증할 수 있음을 보여주는 타입 이론적 내부화를 제공한다고 주장한다.

• 이론적 통합: 심플리셜 타입 이론의 내재된 유향 구조를 활용하여, 계산의 운용적 관점(유향 축약)과 논리 관계의 의미론적 관점(증명-관련 글루잉)을 통합한다.
• 공변성의 새로운 역할: 공변 패밀리를 단순한 도구를 넘어, 임의적인 확장 레마를 보편 성질로 대체하는 근본적인 메커니즘으로 격상시킨다.
• 겸손한 태도: 저자들은 결과가 "놀랍지 않다"(논리 관계가 축약에 대해서도 작동해야 함)고 언급하면서도, 그 내부화가 갖는 중요성을 강조한다. 또한 의존 타입 확장이 복잡한 수송 문제를 안고 있음을 인정하며, 현재의 기계화가 단순 타입에 국한되어 있음을 밝힌다. 이들은 항등 타입(identity types)에 관한 유향 설정의 문제를 완전히 해결했다고 주장하지 않으며, 향면의 연구 과제로 위상 구분(phase distinction)이나 모나딕 모달리티를 제시한다.

이 연구는 심플리셜 타입 이론이 합성 $\infty$-범주론의 도구일 뿐만 아니라, 프로그래밍 언어와 타입 이론의 축약 의미론을 추론하기 위한 유효한 메타이론임을 입증한다.