Nominal Type Theory by Nullary Internal Parametricity

기술적 요약: Nullary Internal Parametricity 에 의한 명목적 형식 이론

문제 제기
람다 계산과 같은 바인더를 포함하는 언어의 구문을 형식화하는 것은 $\alpha$-동치, 이름 추상화, 그리고 신선성 (freshness) 처리를 필요로 합니다. 명목적 프레임워크는 "이름 추상화" 유형 (기호 $\@N \multimap -$ 로 표기) 을 사용하여 이를 해결합니다. 그러나 기존 접근법들은 다음과 같은 트레이드오프에 직면해 있습니다:

1. 실존적 표현 (Existential Presentation): 추상화를 이름 - 항 쌍 $\langle x, a \rangle$으로 취급합니다. 이는 편리한 "명목적 패턴 매칭"(바인더 분해) 을 지원하지만, 복잡한 신선성 전파를 요구하는 번거로운 유형 규칙으로 고통받습니다.
2. 보편적 표현 (Universal Presentation): 추상화를 신선한 이름을 소비하는 함수 (아핀 함수) 로 취급합니다. 이는 깔끔한 추론 규칙을 제공하지만, 명목적 패턴 매칭 수행 능력이 결여된 것처럼 보입니다.

현재의 명목적 프레임워크들은 종종 이 간극을 메우기 위해 외부 의미론 (예: 명목적 집합) 이나 복잡한 내부 메커니즘에 의존합니다. 본 논문은 완전히 형식 이론적 설정 내에서 보편적 표현의 깔끔한 규칙과 실존적 표현의 패턴 매칭 능력을 통합하는 기초를 모색합니다.

방법론
저자들은 **Nullary Internally Parametric Type Theory (nullary PTT)**를 기반으로 구축된 종속 형식 이론인 **Parametric Nominal Type Theory (PNTT)**를 제안합니다. 이 접근법은 Cavallo 와 Harper(CH) 의 이진 내부 매개변수 형식 이론을 매개변수성의 차수를 2 에서 0 으로 줄임으로써 적응합니다.

핵심 방법론은 다음과 같습니다:

1. Nullary Bridges: 표준 이진 경로/브리지 유형을 nullary bridge 로 대체합니다. Nullary bridge $q : \text{Bridge } A \dots$는 bridge interval $\@N$으로부터의 아핀 함수로 취급됩니다. 이러한 브리지는 "신선한" 변수를 나타냅니다.
2. 구조 추상화 원리 (Structure Abstraction Principle, SAP): 이 이론은 SAP 를 통해 매개변수성을 내부화하며, 이는 유형 $K$와 그 "브리지 유형" $\@N \multimap K$ 사이의 동치를 확립합니다. 핵심적으로, SAP 는 브리지 유형 형성자가 모든 다른 유형 형성자와 가환함을 주장합니다.
3. 이름 유도 (Name Induction): 브리지 interval $\@N$은 1 급의 이름 유형 $\text{Nm}$으로 확장됩니다. 새로운 소거자 이름 유도($\text{ind}_{\text{Nm}}$) 가 도입됩니다. 이는 이름 $n$에 대한 경우 분석을 가능하게 합니다: $n$이 현재 범위 내에 있는 특정 아핀 변수 $x$이거나, $x$가 $n$에서 신선한 경우입니다.
4. 명목적 데이터 유형: 무정형 람다 계산의 구문과 같은 표준 명목적 데이터 유형은 이름을 인자로 취할 수 있는 생성자를 사용하여 정의됩니다.

주요 기여

1. 명목적 패턴 매칭의 회복: 본 논문은 일반적으로 실존적 추상화와 연관된 명목적 패턴 매칭이 보편적 설정에서 회복될 수 있음을 보여줍니다. 명목적 데이터 유형 $D$에 SAP 를 적용함으로써, 브리지 유형 $\@N \multimap D$는 "매개변수적 번역" $D_1$(예: $Ltm_1$) 과 동치임이 입증됩니다. $D_1$는 명시적인 "홀"(hole) 생성자를 포함합니다. 따라서 $D$의 바인더에 대한 패턴 매칭은 $D_1$에 대한 유도로 축소되며, 여기서 "홀" 경우는 바인딩된 변수에 해당합니다.
2. 통합된 원시 연산: 저자들은 PNTT 가 자연스럽게 다음을 지원함을 보여줍니다:
   • 보편적 이름 추상화: Nullary bridge 유형을 통해.
   • 유형적 신선성 (Typal Freshness): 특정 이름이 신선한 항들을 분류하는 $\text{Gel}$ 유형을 통해.
   • 실존적 추상화: SAP 와 신선성 유형을 통해 비원시적으로 유도됨.
   • 이름 교환 및 로컬 스코핑: 아핀 함수와 $\nu$-바인더($\text{ung}(\lambda x. t)$로 구현됨) 를 사용하여 구현됨.
3. 합성 Kripke 매개변수성: 본 논문은 nullary 매개변수성을 Kripke 이진 매개변수성과 연결합니다. nullary 매개변수성 (명목적 추론용) 과 표준 이진 매개변수성 공리를 결합함으로써, 저자들은 Kripke 모델을 모방합니다. 이는 무정형 람다 계산의 De Bruijn 구문과 그 고차원 추상 구문 (HOAS) 인코딩 사이의 동치를 증명함으로써 입증됩니다.
4. 이름에서의 구조 추상화 원리 (SAP): $\@N \multimap \text{Nm} \simeq 1 + \text{Nm}$임을 보이는 구체적인 증명이 제공됩니다. 이 동치는 이름 유도 원리와 패턴 매칭 회복의 핵심입니다.

결과

• 이론적 건전성: 저자들은 $\square_0$가 유한 순서수와 단사 함수의 범주 (Schanuel 토포스의 기초) 인 presheaf 범주 $\text{Psh}(\square_2 \times \square_0)$에서 PNTT 를 위한 의미론적 모델을 제공합니다. 이는 시스템의 일관성을 확인합니다.
• 구현 가능성: 본 논문은 이진 CH 이론이 Cubical Agda 에서 구현되었으므로, PNTT(실질적으로 nullary CH + 이름 유도) 의 구현이 가능하다고 주장합니다.
• 사례 연구:
  • $\pi$-calculus 치환: 저자들은 바인딩 패턴에 매칭함으로써 $\pi$-calculus 프로세스에 대한 치환 함수를 정의하며, SAP 기반 접근법의 유용성을 입증합니다.
  • HOAS 적절성: 외부 이진 매개변수성 공리에 의존하는 증명 개요가 제시되어, 람다 계산의 명목적 구문이 그 HOAS 인코딩과 동치임을 보여주며, 이는 Atkey 의 Kripke 매개변수성 결과를 반영합니다.

의의 및 주장
본 논문은 실존적 및 보편적 이름 추상화 간의 역사적 긴장을 해결하는 "정당한 명목적 프레임워크"를 제공한다고 주장합니다.

• 통합: 외부 메타 이론을 요구하지 않고 보편적 추상화의 깔끔한 추론 규칙과 실존적 추상화의 실용적 패턴 매칭 능력을 통합합니다.
• 내부화: 이전 접근법들에서 매개변수성이 메타 이론적 속성이었던 것과 달리, PNTT 는 SAP 를 통해 매개변수성을 내부화하여 매개변수성 결과를 이론 내에서 증명할 수 있게 합니다.
• 신규성: 저자들은 명목적 형식 이론의 기초로서 nullary 매개변수성을 명시적이고 적극적으로 사용한 최초의 사례라고 밝힙니다.
• 겸손함: 본 논문은 한계를 인정합니다. 복잡한 항에 대한 SAP 증명은 "불편하며" 현재는 항 구조의 수동 재현을 필요로 합니다. 저자들은 향후 작업으로 SAP 증명 구성의 자동화 또는 명시적 SAP 증명 필요성을 피하기 위해 Narya 증명 보조기와 같은 "관찰적" PNTT 버전으로의 전환을 제안합니다. 또한 완전한 FreshMLTT 이름 교환 규칙 (치환과 가환) 이 임시 제한 없이 완전히 수용되지는 않았음을 지적합니다.

요약하자면, 본 논문은 nullary internal parametricity 를 명목적 형식 이론을 위한 견고한 기초로 확립하여, 단일하고 일관된 형식 이론 시스템 내에서 바인더, 신선성, 그리고 패턴 매칭을 처리하는 원칙적인 방법을 제시합니다.