A Fibrational Perspective on Differential Linear Logic

문제 제기
미분 선형 논리 (DiLL) 는 선형 논리 (LL) 에 미분을 위한 규칙 (공축약, 공약화, 공제한) 을 추가하여, 선형 논리와 비선형 논리 공식 간의 대칭성을 통해 고차 미분을 포착합니다. DiLL 은 이미 범주론적 모델 (미분 Seely 범주) 과 데카르트 미분 범주 (CDC) 와의 연결고리를 확립했으나, 여전히 단순 타입 이론에 머무르고 있습니다. 이는 개념적 간극을 야기합니다: 미분기하학에서 매끄러운 함수 $f: M \to N$의 미분은 $x$에 의존하는 접공간 $TM_x$를 가진 의존 함수 $D_x(f): TM_x \multimap TN_{f(x)}$입니다. 본 논문은 DiLL 의 의존 버전이 존재하는지, 그리고 선형 타입 (벡터 공간) 과 비선형 타입 (다양체) 간의 이러한 의존성을 수용하기 위해 그 모델이 어떻게 표현될 수 있는지를 묻습니다.

방법론
저자는 그로텐디크 피브레이션의 프레임워크를 활용하여 의존성을 모델링하며, 의존 타입 이론의 범주론적 의미론에서 유래한 방법론을 선형 - 비선형 (LNL) 수반 관계의 맥락에 적용합니다.

1. 선형 단순 피브레이션: 비선형인 데카르트 범주 $\mathcal{C}$와 선형인 대칭 모노이달 범주 $\mathcal{L}$ 사이의 LNL 수반 관계에서 시작하여, "선형 단순 범주" $LS(\mathcal{C})$를 구성합니다. 이 범주는 단순 타입 이론의 단순 범주에 대응하는 선형 논리 버전으로 기능합니다. 대상은 $X \in \mathcal{C}$와 $A \in \mathcal{L}$인 쌍 $(X, A)$이며, 이는 선형 타입 $A$가 비선형 문맥 $X$에 의존하는 문맥을 나타냅니다.
2. 피브드 수반 관계: 본 논문은 원래의 LNL 수반 관계가 $\mathcal{C}$의 단순 피브레이션과 선형 단순 피브레이션 $LS(\mathcal{C})$ 사이의 피브드 수반 관계로 승화된다는 것을 보여줍니다.
3. 선형 접함수: 미분을 도입하기 위해, 본 논문은 "선형 접함수" $T: \mathcal{C} \to LS(\mathcal{C})$를 정의합니다. 이 함수는 피브레이션의 곱-보존 단면이어야 하며, 비선형 대상의 접다발과 부분적 선형성을 가진 사상들에 관한 특정 공리들을 만족해야 합니다.
4. 일반화된 미분 Seely 범주 (GDSC): LNL 수반 관계에 이 선형 접함수를 부여함으로써, 본 논문은 GDSC 를 정의합니다.

주요 기여

• 선형 단순 피브레이션: 임의의 LNL 수반 관계로부터 $LS(\mathcal{C})$를 구성하여, 의존 타입 이론의 구조를 반영하는 선형 논리를 위한 피브드 의미론을 제공합니다.
• 피브드 LNL 수반 관계: 임의의 LNL 수반 관계가 베이스의 단순 범주와 선형 단순 범주 사이의 피브드 수반 관계를 유도하며, 섬유별로 논리적 구조를 보존함을 증명합니다.
• 일반화된 미분 Seely 범주 (GDSC): 세 가지 공리를 만족하는 선형 접함수를 갖춘 가산적 LNL 수반 관계로 GDSC 를 정의합니다:
  • $T$는 곱을 보존하는 단면입니다.
  • $T(U(A)) = (U(A), A)$ (벡터 공간 대상의 접다발은 그 대상 자체입니다).
  • 접함수가 약화와 부분적 선형 사상과 올바르게 상호작용하도록 보장하는 "부분 선형성 규칙".
• 모델의 동치성: 임의의 GDSC 에서 선형 단순 피브레이션의 모든 섬유가 미분 Seely 범주 (DSC) 임을 증명합니다. 반대로, 임의의 DSC 는 GDSC 를 유도합니다. 이는 피브드 접근법이 기존 모델들을 일반화함을 확립합니다.
• 일반화된 CDC 와의 연결: 본 논문은 GDSC 와 일반화된 데카르트 미분 범주 (GCDC) 간의 관계를 조사합니다. DSC 의 클라이스리 범주가 CDC 임을 보이며, GDSC 에서 접함수에 의해 유도된 엔도함수가 GCDC 의 대부분의 공리를 만족함을 보여줍니다. 다만, 모든 사상에 대한 교환 규칙 (GCDC.7) 은 여전히 열린 질문으로 남아 있습니다.

결과

• 본 논문은 선형 접함수가 존재한다면, DiLL 의 의미론을 Seely 범주에서 쌍곱을 갖춘 임의의 가산적 LNL 수반 관계로 확장할 수 있음을 확립합니다.
• GDSC 내의 선형 단순 피브레이션의 섬유 자체가 DSC 임이 증명되었으며, 이는 피브드 구조가 표준 DiLL 모델을 국소적으로 복원하면서도 전역적인 의존 구조를 제공함을 의미합니다.
• 이 구성은 각 섬유 내에서 표준 유도 변환 $\partial$를 복원하여, DiLL 의 상수, 라이프니츠, 선형, 연쇄, 교환 규칙을 모두 만족합니다.
• 이 연구는 피브드 관점을 미분 범주의 더 넓은 지형과 연결하여, GDSC 를 DSC 와 신흥 피브드 접범주 이론 사이에 위치하는 일반화로 자리매김합니다.

의의와 주장
본 논문은 이 연구가 미분 선형 논리와 의존 타입을 통합하기 위한 "첫걸음"이라고 주장합니다. 접함수를 갖춘 그로텐디크 피브레이션 쌍으로 DiLL 모델을 표현함으로써, 저자는 미분기하학에 내재되어 있으나 표준 DiLL 에는 부재하는 비선형 문맥에 대한 선형 타입의 의존성을 처리할 수 있는 범주론적 프레임워크를 제공합니다.

그 의의는 다음과 같습니다:

1. 통합: 의존 DiLL 을 모델링할 수 있는 경로를 제시하여, $\Pi_{x:M} (TM_x \multimap TN_{f(x)})$와 같은 타입의 표현을 가능하게 할 잠재력을 가집니다.
2. 일반화: Seely 범주를 넘어 임의의 가산적 LNL 수반 관계로 DiLL 의 의미론적 범위를 확장하여, 접범주에서 비롯된 새로운 모델 탐색의 문을 엽니다.
3. 기초적 연결: 미분의 범주론적 의미론 (DSC, CDC) 과 의존성의 의미론 (피브레이션, 이해 범주) 을 연결하여, 접범주가 GCDC 와 의존 DiLL 모델을 위한 자연스러운 의존 일반화가 될 수 있음을 시사합니다.

저자는 겸손하게, 이 피브드 구성이 LNL 수반 관계 위의 단순 피브레이션이라는 특정 사례에 대해 작동하지만, 궁극적인 목표는 Vákár 와 Lundfall 이 설명한 것과 같은 의존 LL 의 일반 모델에서 이러한 조건을 만족하는 구조를 찾는 것이라고 언급합니다. 본 논문은 의존 DiLL 타입 이론을 완전히 구성했다고 주장하는 것이 아니라, 그러한 발전을 지원하기 위한 필수적인 범주론적 인프라 (GDSC) 를 제공했다고 주장합니다.