Automating Boundary Filling in Cubical Type Theories

기술 요약: 입방형 유형론(Cubical Type Theories)에서의 경계 채우기 자동화

문제 정의
입방형 유형론(CTT)에서 고차원 구조(고차 유도 유형 및 일관성(Univalence)을 통한 위상 공간 등)를 추론하기 위해서는 지정된 경계를 가진 "큐브(cubes)"를 구성해야 한다. 경계를 채우는 이 과정은 컨토션(contortion, 변형)(셀을 경계에 맞게 재매개변수화하는 것)과 칸 채우기(Kan filling)(여러 큐브를 붙여서 열린 상자(open box)를 채우는 것)라는 두 가지 주요 메커니즘을 포함한다. 컨토션이 이러한 등가 추론의 한 형태라면, 칸 채우기는 이러한 추론의 고차원적 일반화이다.

핵심적인 과제는 이러한 큐브를 수동으로 구성하는 것이 매우 번거롭고 오류를 범하기 쉽다는 점이며, 특히 차원이 높아질수록 더욱 그러하다. 또한, 일반적인 칸 채우기(Kan filler)를 찾는 문제는 결정 불가능(undecidable)하며, 데데킨트(Dedekind) 및 드 드 모르간(De Morgan)과 같이 표현력이 풍부한 이론에 대해 최적의 컨토션을 찾는 제한된 문제조차 조합 폭발(예: 데데킨트 수의 급격한 증가) 문제를 겪는다. 본 논문은 CTT의 일상적인 증명 목표를 위해 이러한 경계 채우기 작업을 자동화하는 알고리즘적 접근 방식을 고안하는 것을 목표로 한다.

방법론
저자들은 "컨토션 이론"(허용된 재매개변수화의 클래스)에 의해 매개변수화된 단순화되고 일반적인 입방형 언어를 개발한다. 이들은 두 가지 별개의 자동화 문제인 **컨토션 해결(Contortion Solving)**과 **칸 해결(Kan Solving)**을 분리하여 다룬다.

1. 컨토션 해결:

   • 이론적 기초: 저자들은 데데킨트 및 드 드 모르간 컨토션을 포셋 맵(poset maps)(구체적으로 유한한 거듭제곱 포셋 $I = \{0 < 1\}$ 사이의 단조 함수)으로 매핑한다. 이는 유한 분산 격자와 유한 포셋 사이의 비르크호프 쌍대성(Birkhoff's duality)을 활용한다.
   • 표현: 탐색 공간의 지수적 증가를 관리하기 위해, 저자들은 **잠재 포셋 맵(Potential Poset Maps, PPMs)**을 도입한다. PPM은 도메인 포셋에서 공역 포셋의 멱집합으로의 맵으로, 여러 유효한 컨토션들을 동시에 나타내는 집합을 의미한다. 이를 통해 원시 열거 방식의 초지수적 증가가 아닌, 차원에 따라 지수적으로 증가하는 효율적인 표현이 가능해진다.
   • 알고리즘: 저자들은 대상 경계 면(boundary faces)에 의해 부과된 제약 조건에 따라 PPM을 반복적으로 제한하는 알고리즘(Algorithm 1)을 제안한다. 제약 조건을 차원 순서대로 정렬하고 제약을 전파함으로써, 최종적인 브루트 포스(brute-force) 검사를 수행하기 전에 탐색 공간을 크게 줄인다.

2. 칸 해결:

   • 제약 충족 문제(Constraint Satisfaction): 칸 채우기(특히 고차원 채우기) 탐색은 **제약 충족 문제(CSP)**로 정식화된다. 이 CSP의 변수는 열린 상자의 미지의 면들을 나타내며, 도메인은 (효율성을 위해 PPM으로 표현된) 유효한 컨토션들로 구성된다.
     ธ์ 휴리스틱 탐색: 탐색 공간이 무한할 수 있으므로(중첩된 채우기가 가능하기 때문), 저자들은 **너비 우선 탐색(breadth-first search)**과 반복 심화(iterative deepening) 전략(Algorithm 2 및 3)을 사용한다. 솔버는 "자연스러운 채우기"(경계 면이 이미 채우기인 경우)와 단순한 컨토션을 우선시한다. 이러한 방법이 실패할 때만 더 높은 차원의 열린 상자를 구성하고, 누락된 면들을 위해 재귀적으로 해결한다.
   • 이론 매개변수화: 솔버는 컨토션 이론에 구애받지 않도록 설계되어, 문제의 복잡도에 따라 카테시안(Cartesian), 분산(Disjunctive), 데데킨트 또는 드 드 모르간 이론 사이를 전환할 수 있다.

주요 기여

• 일반 프레임워크: 다양한 기존 시스템(카테시안, CCHM 등)을 통합하여 컨토션 이론에 의해 매개변수화된 일반적인 입방형 언어를 정식화하였다.
• 복잡도 분석:
  • 칸 채우기가 유한 제시 군(finitely presented groups)의 단어 문제(word problem)를 칸 해결 문제로 환원함으로써 결정 불가능함을 증명하였다.
  • 데데킨트 및 드 드 모르간 컨토션 해결이 NP-완전(및 함의(entailment)에 대해 coNP-하드)임을 입증하여, 브루트 포스 접근 방식의 비효현성을 강조하였다.
• 효율적인 알고리즘:
  • 데데킨트 및 드 드 모르간 컨토션 문제를 해결하기 위한 PPM 기반 알고리즘을 개발하여, 단순 열거법에 비해 탐색 공간을 획기적으로 줄였다.
  • 컨토션 해결을 하위 루틴으로 통합한 CSP 기반의 칸 채우기 솔버를 개발하였다.
• 구현: 이러한 알고리즘을 구현한 실용적인 Haskell 구현체를 제공하여, agda/cubical 및 1lab 라이브러리의 경계 문제를 해결할 수 있음을 보여주었다.

결과
저자들은 다음과 같은 벤치마크 세트를 통해 솔버를 평가하였다:

• 경로 연결의 결합 법칙(Associativity of Path Concatenation): 경로 역전을 포함하는 드 드 모르간 컨토션을 사용하여 해결하였다.
• 엑스만-힐튼 논법(Eckmann-Hilton Argument): 솔버는 2-루프 연결이 가환(commutative)임을 증명하기 위해 필요한 3-큐브 및 4-큐브 채우기를 성공적으로 구성하였다. 이는 큐브 구성에 약 150ms, 관련 합성 보조정(composition lemma)에 15ms가 소요되었다.
• 성능: 표준 노트북에서 일상적인 증명 의무(예: 큐브 측면 재배열)는 50ms 미만에 해결되었다. 솔버는 수동으로 구성하기 까다로운 복잡한 다단계 증명들도 성공적으로 처리하였다.

의의 및 주장
본 논문은 입방형 유형론을 위한 체계적인 자동 추론 연구 중 하나를 제시한다고 주장한다. 그 의의는 다음과 같다:

1. 간극 해소: 현재 표준 라이브러리에서 예측하거나 열거하기 어려운, 합성 호모토피 이론(synthetic homotopy theory)에서 일상적인 보조 정리로 등장하는 "입방형 퍼즐(cubical puzzles)" 문제를 해결한다.
2. 복잡도 처리: 포셋 맵과 CSP를 활용함으로써, 저자들은 데데킨트/드 드 모르간 컨토션 해결과 같이 이론적으로 어려운 문제라도 휴리스틱 탐색과 효율적인 표현을 통해 실질적인 사례들에 대해 다룰 수 있음을 입증하였다.
3. 실용적 유용성: 이 구현체는 자동화가 Cubical Agda의 증명 부담을 크게 줄일 수 있음을 보여주는 개념 증명(proof-of-concept) 역할을 하며, 향-후 루틴한 목표를 해결하는 택틱(tactic)으로 기능할 수 있다.

저자들은 현재의 한계에 대해 겸손한 태도를 유지하며, 솔버가 아직 모든 복잡한 목표(예: 7차원 스퀘어-투-큐브 아날로그 또는 실렙시스(syllepsis))를 합리적인 시간 내에 해결할 수는 없으며, 고차원 경로의 탐색 공간이 여전히 방대하다는 점을 언급하였다. 이들은 본 연구를 향후 연구 및 정리 증명기(theorem prover)로의 통합을 위한 토대로 규정한다.