Multi-clocked Guarded Recursion Beyond {\omega}

기술 요약: $\omega$를 넘어선 다중 클록 가드된 재귀 (Multi-clocked Guarded Recursion)

문제 정의
다중 클록 가드된 재귀를 갖는 타입 이론(Clocked Type Theory, CloTT 등)은 공층적(coinductive) 타입들을 프로그래밍하고 비결정론(non-determinism) 및 확률적 선택(probabilistic choice)과 같은 고급 구문들을 특징으로 하는 프로그래밍 언어의 데노테이션 모델을 구축하는 데 유연한 프레임워크를 제공한다. 이러한 이론들은 트리(trees)의 토포스(index $\omega$) 상의 프리셰프(presheaves)를 통해 성공적으로 모델링되어 왔으며, 최근에는 큐비컬 셋(cubical sets)의 프리셰프로도 확장되었다. 그러나 이러한 결과들을 표준 집합론의 "실제 세계"와 연결하는 데에는 여전히 간극이 존재한다.

구체적으로, 표준 집합론적 해석은 클록 양화(clock quantification)와 특정 펑터(예: 유한 멱집합 펑터 $P_f$ 및 유한 분포 펑터 $D_f$) 사이의 교환성(commutativity)을 보존하는 데 실패하는 경우가 많다. 트리의 토포스에서 존재 양화($\exists$)는 항상 집합에서의 존재로 외재화(externalize)되지 않으며, $P_f$ 및 $D_f$와 같은 펑터들은 표준 모델에서 클록 양화와 교환되지 않는다. 결과적으로, Clocked Cubical Type Theory에서 증명된 결과들(예: 모나드 간의 분배 법칙 또는 Probabilistic FPC에서의 문맥적 동등성)은 현재 hsets 상의 모나드에 대한 진술로 해석되고 있으며, 이들의 유효성이 표준 범주인 $\mathbf{Set}$에서 검증되지 않은 상태로 남아 있다.

방법론
본 논문은 필요한 교환성을 복원하기 위해 다중 클록 가드된 재귀의 외연적 프리셰프 모델을 더 높은 오디널(higher ordinals, $\rho > \omega$)로 확장하는 방법을 조사한다. 방법론은 다음과 같다:

1. 모델 확장: CloTT의 프리셰프 모델(원래 Mannaa 등이 $\rho = \omega$에 대해 정의함)을 임의의 정규 극한 오디널(regular limit ordinal) $\rho$에 의해 인덱싱되도록 일반화한다. 모델은 시간 객체(time objects) $T_\rho$ 위의 프리셰프 범주에서 구축되며, 여기서 객체는 유한 클록 집합과 $\rho$로의 사상(map)의 쌍이다.
2. 교환성의 의미론적 분석: 유니버설 클록 양화($\forall \kappa$)가 다음 항목들과 교환되는 조건을 분석한다:
   • 대수적 이론(algebraic theories)에 의해 생성된 펑터(특히 $P_f$ 및 $D_f$와 같은 모나드).
   • 존재 양화($\exists$).
3. 구문적 및 의미론적 조건:
   • 펑터의 경우: 펑터 $F$가 $\kappa$-접근 가능(accessible)하고, $\kappa$-작은 교집합을 보존하며, 모노모피즘의 풀백(pullback)을 보존한다면, $\rho$가 $\kappa$의 카디널리티를 가진 오디널을 포함할 때 $F$는 $\rho^{op}$-인덱스 리미트(limits)와 교환된다.
   • 대수적 이론의 경우: 하나의 구문적 조건이 식별되었다: 대수적 이론은 "드롭 방정식(drop equations)"(두 항의 자유 변수 집합이 서로 다른 방정식)을 포함해서는 안 된다. 이는 생성된 모나드가 위의 의미론적 조건을 만족하도록 보장한다.
   • 존재 양화의 경우: 타입 $X$에 대해 $\forall \kappa$가 $\exists$와 교환되는 것은 $X$의 파이버(fibers)의 카디널리티가 인덱싱 오디널 $\rho$보다 엄격히 작을 때임을 증명한다. 또한, 위젯(witness)이 유한한 지연 단계(delay steps) 내에서 유일하게 결정되는 "본질적으로 유일한(essentially unique)" 존재 양화에 대해서도 다룬다.

핵심 기여 및 결과

• Set에 대한 보존성(Conservativity over Set): 본 논문은 Clocked Type Theory 모델이 표준 집합론적 타입 이론 모델에 대해 보존적임을 명시적으로 기술하고 증명한다. 이는 $\mathbf{Set}$의 내부 언어로 표현 가능하며 $\mathbf{Set}$에서 참인 모든 진술이 CloTT에서도 참임을 의미한다.
• 모나드의 교환성: 대수적 이론에 의해 생성된 모나드가 클록 양화와 교환되기 위한 의미론적 조건과 구문적 기준(드롭 방정식의 부재)을 제공한다. 이는 $\rho$가 충분히 클 경우(예: 가산 연산에 대해 $\omega_1$), $P_f$ 및 $D_f$를 사용하는 것을 정당화한다.
• 존재 양화의 교환성: 충분히 큰 정규 오디널(예: $\omega_1$ 또는 그 이상)을 선택함으로써, 유니버설 클록 양화가 $\rho$ 미만의 카디널리티를 가진 집합에 대한 존재 양화와 교환됨을 입증한다. 이는 트리의 토포스에서 $\mathbf{Set}$으로 존재 증명을 외재화하는 문제를 해결한다.
• 기존 연구의 해석: 이전에 Clocked Cubical Type Theory를 통해 정형화된 응용 사례들, 즉:
  • 비결정론적 및 확률적 시스템의 코알제브라적 모델링.
  • 약한 쌍사성(weak bisimilarity) 및 모나드 간의 분배 법칙에 관한 추론.
  • Probabilistic FPC에 대한 문맥적 동등성 증명
    —이들이 충분히 큰 오디널에 의해 인덱싱된 집합론적 모델에서 해석될 수 있음을 보여준다. 이는 해당 결과들의 표준 집합론적 해석에 대한 정당성을 입증한다.

의의
본 논문은 모델의 인덱싱 오디널을 변화시킴으로써, 가드된 재귀의 내부 논리(생산성과 공층성을 우아하게 처리함)와 표준 집합론의 외부 세계 사이의 간극을 메울 수 있다고 주장한다.

주된 의의는 Clocked Cubical Type Theory의 메커니즘을 사용하여 증명된 결과들을, 큐비컬 셋의 특성에 의존하지 않고도 충분히 큰 인덱싱 오디널을 사용하는 모델을 통해 표준 집합론 내에서 검증할 수 있다는 점이다. 이는 비결정론, 확률, 공층적 술어(coinductive predicates)를 포함하는 응용 분야를 정형화하기 위한 의미론적 기초를 구축할 수 있음을 시사한다. 본 논문은 비록 증명에 사용된 메타이론이 고전적 집합론이지만, 이 결과들이 쿼티 타입(quotient inductive types) 및 존재 양화를 포함하는 공층적 타입들의 인코딩에 대한 엄밀한 집합론적 정당성을 제공한다고 밝히고 있다.