Dependent Multiplicities in Dependent Linear Type Theory

문제 진술
기존의 정량적 타입 이론들, 예를 들어 정량적 타입 이론 (QTT) 과 등급 모달 타입 이론은 변수가 사용 횟수를 지정하는 다중성 (multiplicities) 을 갖는 리소스 주석을 허용합니다. 그러나 이러한 시스템들은 일반적으로 자연수나 반환 (semirings) 과 같은 고정된 리소스 대수에서 유래된 정적 다중성에 의존합니다. 이러한 정적 성격은 리소스를 직접 표현하지 않고 분기 (조건부) 및 재귀와 같이 리소스를 조직화하는 프로그램 논리를 다룰 때 상당한 한계를 초래합니다.

현재 시스템들에서 두 가지 분기 사이를 선택하는 데 사용되는 불리언 조건은 두 분기가 모두 동일한 리소스를 소비하도록 요구합니다. 이는 서로 다른 분기가 일반적으로 서로 다른 작업을 수행하기 때문에 종종 비현실적입니다. 마찬가지로, 고차 함수나 귀납적 타입 (예: 이진 트리) 에서는 함수가 적용되거나 리소스가 소비되는 횟수가 런타임에만 알려진 값 (예: 트리의 리프 노드 수) 에 의존하는 경우가 많습니다. 종속 타입 이론 (DTT) 과 선형 논리를 결합하려는 이전의 시도들은 항에 의존하는 타입이 해당 항의 "사용"을 구성하는지 여부에 대한 질문에서 어려움을 겪었습니다. McBride 와 Atkey 는 타입이 계산을 위한 것이 아니라 숙고를 위한 것이므로 (선형 변수에 대한 의존을 허용함) 라고 주장했지만, 그들의 결과인 QTT 는 여전히 다중성을 정적 요소로 제한하여 재귀 프로그램과 데이터 의존적 분기에 내재된 동적 리소스 사용을 포착하지 못했습니다.

방법론
본 논문은 선형 논리를 표준 직관주의 종속 타입 이론 (주체 이론, "host theory") 에 직접 내포하는 새로운 종속 선형 타입 이론을 제안합니다. 핵심 혁신은 다중성을 정적 대수적 요소가 아닌 주체 이론 자체 내의 항으로 취급하는 것입니다.

1. 두 가지 추론 관계: 이 시스템은 두 가지 판단을 구분합니다:
   • $\vdash$: 타입, 항, 그리고 의존성을 정의하는 데 사용되는 표준 직관주의 DTT(주체 이론).
   • $\Vdash$: 항이 "공급 (supplies)"(선형 문맥) 에서 유도되는 리소스 인식 계산.
2. 직관주의 타입으로서의 공급: 전통적인 선형 문맥과 달리, 이 시스템에서 공급은 주체 이론의 항입니다. 이는 주체 이론이 리소스 주석과 함께 계산할 수 있게 합니다. 구체적으로, 시스템은 주체 이론의 자연수를 사용하여 공급의 "곱셈"($\Delta \hat{m}$) 을 정의합니다. 여기서 $m$은 $\mathbb{N}$ 타입의 항입니다. 이 연산은 공급을 $m$ 번 복제할 수 있게 하며, 여기서 $m$은 문맥 내의 다른 변수들에 의존할 수 있습니다.
3. 동적 다중성: 주체 이론의 열린 항 (open term) 으로 다중성 $m$을 허용함으로써 시스템은 동적 리소스 주석을 지원합니다. 예를 들어, 트리를 매핑하는 함수는 함수 $f$가 정확히 leafs(t) 번 사용됨을 지정할 수 있으며, 여기서 leafs(t)는 입력 트리 $t$의 구조에서 계산됩니다.
4. 타입 생성자: 논문은 이러한 동적 다중성이 주석된 표준 DTT 타입 생성자 (함수, 쌍, 불리언, W-타입) 의 선형 버전을 정의합니다. 특히, 불리언과 W-타입의 소거 규칙은 런타임 값에 따라 분기나 생성자 간에 리소스를 다르게 분배할 수 있게 합니다.
5. 의미론: 의미론은 대칭 모노이달 범주로 인덱싱된 범주족 (Categories with Families, CwF) 인 "선형 범주족 (Linear Categories with Families, lCwF)"으로 특징지어집니다. 이 구조는 QTT 에 사용되는 정량적 CwF 를 일반화합니다.

주요 기여

• 종속 다중성을 갖는 구문: 논문은 변수 다중성이 주체 이론의 항이 되는 구문을 제시하여, 이전 선형 시스템에서는 타입 지정이 불가능했던 분기와 재귀를 포함하는 프로그램의 정밀한 타입 지정을 가능하게 합니다.
• 선형 W-타입: 선형 설정에서 귀납적 타입 (구체적으로 유한 위치를 갖는 W-타입) 에 대한 원칙적인 처리를 제공합니다. 시스템은 재귀적 구조의 동적 리소스 사용을 정확히 고려하는 도입 및 소거 규칙을 제공합니다.
• 의미론적 특징화: 저자들은 표준 DTT 모델과 선형 논리 모델이 어떻게 결합되는지 보여주기 위해 이론의 의미론적 모델로 lCwF 를 정의합니다. 그들은 이 모델이 선형 W-타입에 대한 정교한 규칙을 정당화하며 기존 QTT 모델을 일반화함을 보여줍니다.
• 실현 가능성과 소거: BCI-대수 기반의 실현 가능성 모델이 구성되어, 직관주의 단편 ($\vdash$) 이 계산을 위해 소거될 수 있고 실행을 위해 선형 단편 ($\Vdash$) 만 남는다는 것을 보여줍니다. 이는 QTT 의 0 및 1 단편과 유사합니다.
• 구현: 이 이론은 Agda 에 구현되었습니다. 이 구현은 선형 판단을 공급 증명을 갖춘 직관주의 항으로 매핑하는 의미론적 해석을 사용하여 엄격하지만 아직 실용적이지는 않은 타입 체커를 생성합니다.

결과

• 표현력: 시스템은 매핑 함수의 사용이 리프 노드 수에 비례하는 이진 트리에 대한 map 함수와 같은 동적 리소스 카운팅이 필요한 프로그램들을 성공적으로 타입 지정합니다.
• 완전성: 논문은 특정 소거기를 통해 값을 폐기하거나 복제하지 않는 직관주의 항인 "명확한 선형 항"에 대한 완전성 결과를 증명하여, 이러한 항들이 선형 시스템에서 정밀하게 타입 지정될 수 있음을 보여줍니다.
• 직관주의 논리의 회복: 선형 지수 콤모나드 ("!") 를 도입함으로써, 시스템은 선형 단편 내에서 완전한 직관주의 논리를 회복하여 필요한 곳에서 리소스의 제한 없는 사용을 가능하게 합니다.
• 결정성 트레이드오프: 저자들은 자연수의 열린 항을 비교해야 하므로 (예: $\Delta \hat{m}$이 $\Delta \hat{n}$과 같은지 확인), 일반적인 경우 타입 체킹이 결정 불가능함을 인정합니다. 그러나 그들은 주체 이론의 명제적 등식을 사용하여 타입 체커를 리소스 동등성에 대해 설득할 수 있음을 지적합니다.

의의
본 논문은 고정된 리소스 대수에서 주체 이론에서 유래된 동적이고 계산 가능한 다중성으로 이동함으로써 정량적 타입 이론의 더 표현력 있는 버전을 제공한다고 주장합니다. 선형 논리를 별도의 논리로 취급하는 대신 DTT 에 내포시킴으로써, 시스템은 이전 작업에서 발견된 직관주의 변수와 선형 변수 간의 제한적인 이분법을 피합니다. 이는 대규모 귀납적 타입과 고차 함수에 대한 "원칙적인 리소스 인식 처리"를 가능하게 합니다. 이 작업은 기존 종속 타입 언어를 이 시스템으로 확장할 수 있음을 보여주며, 종속 타입의 표현력을 희생하지 않고 함수형 프로그래밍에서 더 정밀한 리소스 관리로 가는 길을 제시합니다. 저자들은 이 작업을 정적 다중성이 런타임 의존적 리소스 사용을 처리하는 데 갖는 한계를 해결하는 QTT 의 일반화로 위치시킵니다.