반변 우주 서브타이핑(Contravariant Universe Subtyping)의 형식화 및 기계 구현

누적된 우주 계층 구조를 가진 타입 이론에서, extit{서브타이핑(subtyping)}은 종종 낮은 우주 레벨을 더 높은 우주로 끌어올리는 방식으로 통합됩니다. 실제로는 증명 보조기(proof assistants)의 커널들이 일반적으로 우주 서브타이핑을 보수적으로 구현합니다: 즉, 서브타이핑은 $\Pi$ 타입의 출력 타입으로 공변적(covariantly)으로만 전파되며, 입력 타입은 동등해야 합니다. 완전한 서브타이핑 관계는 또한 입력 타입을 반변적(contravariantly)으로 비교합니다. 그러나 반변 서브타이핑은 기존 집합론적 모델로는 정당화되지 않으며, 완전한 서브타이핑 알고리즘 개발에 어려움을 야기합니다. 우리는 핵심 Martin-Löf 타입 이론(MLTT)을 위한 반변 우주 서브타이핑의 완전한 기계적 연구인 extmclttsub를 제시하며, 이는 Rocq의 검증된 McTT 커널 확장을 통해 구축되었습니다. 우리는 정규화-평가(normalization-by-evaluation, NbE) 알고리즘의 구문 메타 이론과 건전성 및 완전성 속성을 재확립합니다. 타입 체커를 위한 검증된 파이프라인을 완성하기 위해, 두 가지 완전하고 건전한 서브타이핑 알고리즘을 제공합니다. 첫 번째 알고리즘은 모든 $\Pi$ 반복에서 출력 타입을 extit{재정규화(renormalizes)}합니다. 간단한 완전성 증명에도 불구하고, 이 알고리즘은 추가적인 계산 비용을 발생시킵니다. 따라서 두 번째 알고리즘은 모든 재정규화를 피함으로써 이러한 비용을 우회합니다. 이는 단순히 이미 정규화된 두 타입을 구조적으로 재귀 비교할 뿐입니다. 그럼에도 불구하고, 의미론적 접근 방식에서 이 알고리즘의 완전성 증명은 하위 컨텍스트(sub-contexts)에서의 정규화에 대해 추론해야 하며, 이는 현재의 의미론적 가젯(semantic gadget)이 제공하는 범위를 넘어섭니다. 대신, 우리는 비시뮬레이션 관계(bisimulation relations)를 통해 프로그램 동등성 증명을 수행합니다. 이 기술을 사용하여, NbE 알고리즘이 우주 레벨까지 하위 컨텍스트에서 동일한 정규형(normal forms)을 반환함을 증명하고, 서브타이핑 알고리즘의 완전성을 성공적으로 결론지었습니다.