Constructing (Co)inductive Types via Large Sizes

"Constructing (Co)inductive Types via Large Sizes" (대형 크기를 통한 (공)유도형 구성)이라는 제목의 논문에 대한 상세한 기술적 요약입니다. 저자는 Bastiaan Laarakker, Daniël Otten, Benno van den Berg 입니다.

1. 문제 제기

증명 보조 도구 (Agda, Lean, Rocq 등) 는 일관성과 결정 가능성을 보장하기 위해 종속 타입 이론에 의존합니다. 여기서 핵심 요구사항은 모든 재귀 함수가 **전체적 (total, 종료됨)**이어야 하고, 모든 코재귀 함수가 **생산적 (productive)**이어야 한다는 것입니다.

• 현재의 한계: 대부분의 시스템은 구문적 검사 (예: 구조적 재귀 또는 크기 변경 종료) 를 통해 전체성을 강제합니다. 이러한 검사는 종종 제한적이며, 모듈성이 없고, 코드 리팩토링에 민감합니다.
• 크기 타입 (Sized Types): 타입 기반 대안은 타입에 "크기" (순서수) 를 주석으로 달아, 크기에 대한 정렬된 귀납을 통해 종료를 증명할 수 있게 합니다.
• Agda 의 불일치: Agda 는 크기 타입을 구현하지만, 전체 유도/공유도 타입을 $\infty$에서의 근사치로 정의하기 위해 최대 크기 ($\infty$) 를 도입합니다. 이는 논리적 불일치로 이어집니다: 시스템이 $\infty < \infty$를 증명하여 엄격한 정렬의 반사성 위반을 초래합니다.
• 이전 이론적 작업: 매개변수 양화자 (유도형에 대한 존재 양화자 $\exists$, 공유도형에 대한 전칭 양화자 $\forall$) 를 사용하여 이를 수정하려는 시도는 제한적이었습니다. 구체적으로, 크기 타입이 자연수 집합 ($\mathbb{N}$) 으로 해석되었기 때문에 무한 분기 구조에 필요한 극한 순서수가 부재하여 유한 분기 유도형만 구성할 수 있었습니다.

목표: 불일치하는 최대 크기에 의존하지 않고, 크기 타입과 매개변수 양화자를 사용하여 모든 (공)유도형 (무한 분기형 포함) 을 지원하는 일관된 타입 이론을 구성하는 것입니다.

2. 방법론

저자들은 이를 달성하기 위해 마틴 - 뢰프 타입 이론 (MLTT) 을 특정 기능으로 확장하고, 실현 가능성 모델을 통해 그 일관성을 증명합니다.

A. 확장된 타입 이론

이 이론은 표준 MLTT 기능 (우주, $\Sigma$, $\Pi$, 동일성 타입) 에 다음을 추가합니다:

1. 크기 타입 (Size):
   • 영 ($0$) 과 후자 ($\uparrow i$) 를 갖습니다.
   • 단순 명제로 인코딩된 사전순서 ($\leq$) 로 정렬됩니다.
   • 중요하게: Size 는 우주 $U$에 속하지 않는 대형 타입이지만, 이에 대한 양화는 소형 타입을 생성할 수 있습니다.
2. 매개변수 양화자:
   • $\exists i. A(i)$ (존재): 근사치들의 합집합을 나타냅니다. 항은 쌍 $\langle s, a \rangle$이지만, 크기 $s$는 추상화되어 패턴 매칭이 불가능합니다. 소거는 소형 타입으로 제한됩니다.
   • $\forall i. A(i)$ (전칭): 근사치들의 교집합을 나타냅니다. 함수는 모든 크기에 대해 균일하게 작용합니다.
   • 매개변수성 공리: 이 이론은 양화자가 타입 생성자와 교환된다는 공리를 포함합니다 (예: $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$). 이는 크기가 균일하게 취급된다는 아이디어를 내부화한 것입니다.
3. 정렬된 귀납 (fix):
   • 크기에 대한 귀납으로 정의를 허용하는 고정점 연산자: $f : \forall i. ((\forall j < i. A(j)) \to A(i))$가 주어졌을 때, $fix\ f : \forall i. A(i)$를 정의합니다.
   • 타입 검사의 결정 가능성을 유지하기 위해 $\beta$ 규칙은 정의적이 아닌 명제적입니다.

B. (공)유도형의 구성

저자들은 (공)유도형을 다항식 엔도펑터 ($F$) 에 대한 초기 대수와 최종 코대수로 인코딩합니다.

1. 순서수 근사치: 크기 인덱스 펑터 $F[\exists -]$와 $F[\forall -]$를 정의합니다. fix 연산자를 사용하여 이러한 크기 인덱스 펑터에 대한 초기 대수 ($\mu_3 F$) 와 최종 코대수 ($\nu_2 F$) 를 구성합니다. 이는 특정 크기에서 절단된 타입을 나타냅니다.
2. 양화를 통한 전체 타입:
   • 유도형: $\mu F := \exists i. (\mu_3 F) i$로 정의됩니다. 존재 양화자는 어떤 크기에 의해 경계된 모든 항을 수집합니다.
   • 공유도형: $\nu F := \forall i. (\nu_2 F) i$로 정의됩니다. 전칭 양화자는 항이 어떤 깊이에서도 관찰 가능하도록 보장합니다.
3. 무한 분기형 처리: 핵심 혁신은 다항식 펑터가 존재 양화자와 약하게 교환됨을 보이는 것입니다. 이는 크기들이 단순히 $\mathbb{N}$일 경우 불가능한 순서수 열의 상한 (극한 순서수) 의 존재를 필요로 합니다.

C. 일관성 증명: 실현 가능성 모델

이론이 일관됨을 증명하기 위해, 저자들은 Hyland 의 유효 토포스를 기반으로 한 실현 가능성 모델을 구성합니다.

• 타입의 해석:
  • 소형 타입: 자연수 (계산 가능한 데이터) 위의 **부분 동치 관계 (PERs)**로 해석됩니다.
  • 대형 타입: 계산 가능성 관계를 가진 집합인 **어셈블리 (Assemblies)**로 해석됩니다.
• Size 의 해석:
  • 타입 Size 는 $\nabla \omega_1$로 해석되며, 여기서 $\omega_1$은 첫 번째 비가산 순서수 (모든 가산 순서수의 집합) 입니다.
  • "완전한" 실현 가능성 관계가 부여되어, 사상 (morphisms) 은 모든 크기를 균일하게 취급해야 함을 의미합니다 (매개변수성).
• 검증:
  • $\omega_1$이 극한 순서수를 포함하기 때문에, 이 모델은 무한 분기 유도형에 필요한 매개변수성 공리를 검증합니다.
  • 이 모델은 비예측성 (대형 타입에 대한 양화가 소형 타입을 생성함) 과 **동일성 증명 유일성 (UIP)**을 검증합니다. 이는 구문에서 이를 가정하지 않음에도 불구하고, 구문이 더 강력한 이론 (예: 호모토피 타입 이론) 과 호환되지만 그것들에 의해 제한받지 않음을 보여줍니다.

3. 주요 기여

1. (공)유도형의 일반적 구성: 유한 분기형으로 제한된 이전의 매개변수 접근법과 달리, 이 작업은 무한 분기형 (예: 브라우어 순서수, 구성적 집합 이론 모델) 을 포함한 모든 (공)유도형을 구성합니다.
2. Agda 의 불일치 해결: 불일치하는 "최대 크기" ($\infty$) 를 대형 크기 타입에 대한 매개변수 양화자로 대체함으로써, 저자들은 Agda 의 현재 구현에 대한 일관된 대안을 제공합니다.
3. 메커니즘으로서의 매개변수 양화자: 크기에 대한 $\exists$와 $\forall$를 통해 매개변수성을 내부화하는 것이 비종단적 행동과 논리적 불일치를 방지하기 위해 필요한 추상화를 효과적으로 강제함을 보여줍니다.
4. 견고한 실현 가능성 모델: Size 를 $\omega_1$로 해석하는 모델의 구성은 이론에 대한 엄밀한 의미론적 근거를 제공하며, 매개변수성 공리가 일관됨을 증명합니다.

4. 결과

• 이론적 건전성: 이 논문은 임의의 다항식 엔도펑터에 대한 초기 대수와 최종 코대수가 확장된 이론 내에서 존재함을 증명합니다.
• 일관성: 실현 가능성 모델은 이론이 일관됨을 확인합니다. 크기가 비가산 순서수로 해석될 때 매개변수 양화자에 대한 공리가 성립함을 보여줍니다.
• 호환성: 구성은 구문에서 UIP 나 비예측성에 의존하지 않으므로, 모델이 이러한 속성을 만족함에도 불구하고 결과는 호모토피 타입 이론 (HoTT) 과 호환됩니다.

5. 의의 및 향후 작업

• 증명 보조 도구에 미치는 영향: 이 작업은 $\infty$ 크기로 인해 발생하는 현재 불일치 없이 증명 보조 도구 (Agda 등) 에 크기 타입을 구현할 수 있는 길을 제시합니다. 더 모듈화되고 구성적인 종료 검사를 가능하게 합니다.
• 계산적 행동: 저자들은 이론이 일관되지만, 현재 구문은 매개변수성 공리에 대한 계산적 행동이 부족함을 인정합니다 (이들은 축소 규칙이 아닌 공리입니다). 향후 작업은 결정 가능성과 실제에서의 정통성을 보장하기 위해 이를 내부 매개변수성 (예: 브리지 타입 또는 큐비컬 타입 이론을 통해) 과 연결해야 합니다.
• 부등식의 결정 가능성: 이 모델은 크기 간의 부등식이 일반적으로 결정 불가능함을 (상한으로 인해) 시사합니다. 저자들은 실제 구현을 위해 정의적 대 명제적 부등식의 하이브리드 접근법을 제안합니다.
• 일반화: 이 모델은 다른 부분 결합 대수 (partial combinatory algebras) 로 일반화되거나, 효과와 동치성 (univalence) 과 통합될 수 있습니다.

요약하자면, 이 논문은 이론적 필요성인 매개변수 크기 타입과 일관성에 대한 실용적 요구 사이의 간극을 성공적으로 연결하여, 건전한 타입 이론적 프레임워크 내에서 복잡한 (공)유도형을 구성할 수 있게 합니다.