A Graded Modal Dependent Type Theory with Erasure, Formalized

1. 문제 제기 (Problem)

강력한 타입 시스템을 가진 프로그래밍 언어에서는 변수의 사용 방식 (사용 빈도, 소멸 가능성, 선형성 등) 을 정적으로 분석하여 프로그램의 안전성, 최적화, 또는 보안 속성을 보장하려는 시도가 많습니다.

• 기존 연구의 한계: 기존 연구들은 주로 단순 타입 시스템에 국한되거나, 의존형 타입 (Dependent Types) 을 다룰 때 메타 이론적 성질 (정규화, 결정 가능성 등) 을 증명하는 데 어려움을 겪었습니다. 특히, **에러 (Erasure)**와 **선형성 (Linearity)**을 동시에 지원하면서도 **대규모 제거 (Large Elimination, 타입 내에서 값 계산)**를 허용하는 의존형 타입 이론의 완전한 형식화와 검증은 미해결 과제였습니다.
• 핵심 문제: 소거 가능한 (erasable) 부분을 컴파일 시 제거했을 때 프로그램의 실행 결과가 변하지 않는지 (Soundness) 를 어떻게 엄밀하게 증명할 것인가? 특히 열린 프로그램 (Open programs, 자유 변수가 있는 경우) 과 일관성 있는 문맥 (Consistent contexts) 하에서 이 성질을 보장하는 것은 복잡합니다.

2. 방법론 (Methodology)

저자들은 **등급 (Grades)**을 가진 모달 타입 이론을 설계하고 이를 Agda 로 형식화했습니다.

• 모달 구조 (Modality Structure): 등급은 **부분 순서 반군 (Partially Ordered Semiring)**으로 정의됩니다. 이 구조는 변수의 사용 횟수나 보안 수준 등을 추적하는 데 사용됩니다.
  • 연산자: 덧셈 (+), 곱셈 (·), 만남 (meet, ∧) 및 자연수 재귀를 위한 nr 함수를 포함합니다.
  • 예시: 에러 (Erasure, {0, $\omega$}), 아핀 타입 (Affine), 선형 타입 (Linear) 등을 이 구조의 인스턴스로 구현할 수 있습니다.
• 문법 및 타입 시스템:
  • $\Pi$-타입, 약한/강한 $\Sigma$-타입, 자연수 ($\mathbb{N}$), 공집합 타입 ($\bot$), 유니버스 ($U$) 를 지원합니다.
  • 대규모 제거 (Large Elimination): 자연수 재귀 (natrec) 를 통해 타입을 계산할 수 있도록 하여 완전한 의존형 타입 시스템을 구현했습니다.
  • 사용 추론 (Usage Inference): 주어진 항 (Term) 에 대해 자동으로 등급 문맥을 추론하는 알고리즘을 정의했습니다.
• 형식화 및 증명 전략:
  • 논리적 관계 (Logical Relation): 타입 이론과 비타입화된 $\lambda$-계산 (Target Language) 간의 관계를 정의하여 에러의 안전성을 증명했습니다.
  • 두 단계 접근법: 먼저 등급을 무시한 표준 의존형 타입의 의미론을 정의한 후, 이를 등급 인식 (Resource-aware) 의미론으로 세밀화 (Refinement) 했습니다.
  • Agda 형식화: 약 11 만 줄의 Agda 코드로 전체 메타 이론 (주제 축소, 정규화, 정의적 동등성의 결정 가능성 등) 을 기계적으로 검증했습니다.

3. 주요 기여 (Key Contributions)

1. 자연수 재귀를 위한 등급 함수 (nr) 의 확장: 기존 연구에서 사용된 natrec-star 연산자를 더 유연한 nr 함수로 대체하여, 선형성 등 다양한 모달리티를 정확하게 모델링할 수 있도록 개선했습니다.
2. 대규모 제거를 지원하는 완전한 메타 이론 형식화: 유니버스와 대규모 제거를 포함하는 등급 의존형 타입 이론의 메타 이론 (치환 정리, 주제 축소, 정규화, 정의적 동등성 결정 가능성) 을 최초로 완전히 형식화했습니다.
3. 등급 할당 및 사용 추론: 자유 변수의 사용량을 분류하는 결정 가능한 등급 판단 (Grading Judgement) 을 도입하고, 치환 정리 및 축소 하에서의 등급 보존을 증명했습니다.
4. 에러의 논리적 관계 기반 안전성 증명:
   • 소거 가능한 부분을 제거한 후에도 프로그램의 값 (Natural number type) 이 보존됨을 증명했습니다.
   • **열린 프로그램 (Open Programs)**에 대한 증명을 확장했습니다. 모든 자유 변수가 소거 가능하고 문맥이 일관적 (Consistent) 이라면, 열린 프로그램도 안전하게 소거될 수 있음을 보였습니다.
   • 약한 $\Sigma$-타입의 소거된 매칭 (Erased Matches): 소거된 쌍 (Pair) 에 대한 패턴 매칭을 허용할지 여부를 제어하는 메커니즘을 제안하고, 이를 허용할 경우 발생할 수 있는 문제 (Canonicity 손실) 를 분석했습니다.
5. 강한/약한 단위 타입 (Unit Types) 및 등급 $\Sigma$-타입 확장: 선형 논리의 단위 타입 개념을 확장하여 형식화에 포함시켰으며, Atkey 의 의존 텐서 곱과 유사한 등급 $\Sigma$-타입을 추가했습니다.

4. 결과 (Results)

• 메타 이론적 성질 증명: 제안된 이론은 주제 축소 (Subject Reduction), 일관성 (Consistency), 정규화 (Normalization), **정의적 동등성의 결정 가능성 (Decidability of Definitional Equality)**을 만족함이 Agda 를 통해 증명되었습니다.
• 에러 추출의 안전성 (Soundness of Extraction):
  • 소거된 등급 (0) 으로 표시된 함수 인자와 타입을 제거하여 비타입화된 $\lambda$-계산으로 변환하는 추출 함수를 정의했습니다.
  • 비엄격 (Call-by-name) 및 엄격 (Call-by-value) 두 가지 실행 모델 모두에서 추출된 프로그램이 원본 프로그램과 동일한 값을 가짐을 논리적 관계를 통해 증명했습니다.
  • 특히, 일관된 문맥 (Consistent Context) 하에서 열린 프로그램에 대해서도 이 성질이 성립함을 보였습니다.
• 에러 매칭의 한계: 약한 $\Sigma$-타입에 대해 소거된 매칭 (Erased matches) 을 허용할 경우, 자연수에 대한 **정규성 (Canonicity)**이 깨질 수 있음을 반례를 통해 보였습니다. 이는 소거된 매칭을 제한하거나 문맥의 일관성을 요구해야 함을 시사합니다.

5. 의의 (Significance)

• 이론적 엄밀성: 의존형 타입 이론에서 에러와 같은 정적 분석 속성을 수학적으로 엄밀하게 다룬 최초의 완전한 형식화 중 하나입니다. 특히 대규모 제거를 지원하는 것은 실제 프로그래밍 언어 (Agda, Idris 등) 에 적용 가능한 수준임을 보여줍니다.
• 실용적 적용 가능성:
  • 컴파일러 최적화: 에러 가능한 코드를 컴파일 시 제거하여 런타임 오버헤드를 줄일 수 있음을 이론적으로 보장합니다.
  • 보안 및 정보 흐름: 에러 격자 (Erasure Lattice) 를 보안 격자 (Security Lattice) 로 해석하여 정보 흐름 분석 (Information Flow Analysis) 에 적용 가능한 프레임워크를 제공합니다.
  • 검증된 도구 개발: Agda 형식화는 향후 검증된 타입 체커나 컴파일러 구현의 신뢰할 수 있는 기초 (Base) 가 될 수 있습니다.
• 미래 연구 방향: 소거된 매칭을 허용하는 경우의 안전성 증명, 등급 추론 (Grade Inference) 알고리즘 개발, 그리고 실제 언어 (Agda, Idris) 의 메타 변수와의 상호작용 연구 등을 위한 토대를 마련했습니다.

요약하자면, 이 논문은 등급 모달 의존형 타입 이론을 체계적으로 정립하고, 에러를 포함한 다양한 속성을 형식적으로 검증함으로써, 안전하고 효율적인 프로그래밍 언어 설계를 위한 강력한 이론적 기반을 제공했습니다.