Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs

1. 연구 배경 및 문제 정의 (Problem)

기존 연구의 한계:

• 무한 객체(Infinite Objects)와 리라이팅(Rewriting): 컴퓨터 과학에서 비종료 계산(non-terminating computation)이나 무한 스트림 등을 다루기 위해 '무한 리라이팅' 연구가 진행되어 왔습니다. 기존 방식은 주로 위상수학적 완비성(metric completion)과 서수(ordinal) 인덱스를 가진 리라이팅 시퀀스에 의존했습니다.
• 압축 성질(Compression Property)의 중요성: 무한 리라이팅 시스템에서 임의의 서수 길이($\gamma$)를 가진 리라이팅 시퀀스를 길이 $\omega$인 시퀀스로 '압축'할 수 있는 성질을 의미합니다. 이는 무한한 계산 과정을 유한한 단계로 근사(approximation)할 수 있음을 보장하는 핵심적인 성질입니다.
• 비정형 증명 이론(Non-wellfounded Proof Theory)과의 괴리: 커리-하워드 대응(Curry-Howard correspondence)에 따라 증명 이론에서도 무한 증명 트리(infinite proof trees)를 다루지만, 기존의 무한 리라이팅 이론은 '무한 용어(infinitary terms)'에 특화되어 있어 '무한 증명(non-wellfounded proofs)'의 동역학을 통합적으로 설명하기에는 부족했습니다.

핵심 문제:
본 논문은 무한 용어(λ-calculus 등)와 무한 증명(non-wellfounded proofs)을 모두 아우를 수 있는 일반적이고 공변성(coinductive)적인 무한 리라이팅 프레임워크를 구축하고, 이 프레임워크 내에서 압축 성질(Compression)을 일반화하여 증명하는 것을 목표로 합니다.

2. 연구 방법론 (Methodology)

본 논문은 기존의 위상수학적 접근 대신 **공변성(Coinduction)**을 중심에 둔 방법론을 채택합니다.

1. 일반적 프레임워크 구축 (Generic Framework):
   • 유도적(inductive) 생성자와 공변적(coinductive) 생성자가 혼합된 '유도적/공변적 혼합 타입(mixed induction and coinduction)'을 정의합니다.
   • 이를 통해 1차 용어(first-order terms), 무한 $\lambda$-계산(infinitary $\lambda$-calculi), 그리고 비정형 증명 트리(non-wellfounded derivation trees)를 하나의 통일된 수학적 구조로 표현합니다.
2. 공변적 무한 리라이팅 정의:
   • 서수 인덱스를 사용하는 기존 방식 대신, 공변적 규칙(double rules)을 사용하여 무한 리라이팅 관계를 정의합니다. 이는 위상수학적 수렴(strong Cauchy convergence)과 동등함을 증명합니다.
3. 압축 성질의 공변적 정식화:
   • 길이가 $\omega$인 리라이팅 시퀀스를 공변적으로 정의하고, 압축 성질을 $\to^\infty = \to^\omega$라는 관계로 정식화합니다.
4. 압축 성질의 일반적 특성 규명 (Characterization):
   • 압축 성질이 성립하기 위한 필요충분조건인 성질 $Q$를 도출합니다. 이는 특정 유도 가설($P_\delta$) 하에서 서수 길이 $\delta+1$의 리라이팅을 길이 $\omega$로 변환할 수 있는지를 다룹니다.

3. 주요 기여 및 결과 (Key Contributions & Results)

1. 통합적 프레임워크 제시:
   • 1차 리라이팅, $\lambda$-계산, 비정형 증명 이론을 하나의 공변적 프레임워크로 통합했습니다. 이는 서로 다른 분야의 무한 리라이팅 이론을 단일한 이론적 토대 위에서 다룰 수 있게 합니다.
2. 압축 성질의 일반적 정리 (Theorem 14):
   • 임의의 리라이팅 시스템에서 압축 성질이 성립하기 위한 수학적 조건을 일반화하여 제시했습니다. 이 증명은 기존의 복잡한 초한 귀납법(transfinite induction)을 피하고, **완전한 공변적 방식(fully coinductive proof)**으로 수행되었습니다.
3. 기존 시스템에 대한 적용 및 검증:
   • 1차 리라이팅(First-order rewriting): 좌측 선형(left-linear) 시스템이 압축 성질을 가짐을 증명했습니다.
   • $\lambda$-계산(Infinitary $\lambda$-calculi): $\lambda$-계산의 $\beta$-리덕션이 압축 성질을 가짐을 확인했습니다.
4. 비정형 증명 시스템 $\mu\text{MALL}_\infty$에 적용:
   • 고정점(fixed points)을 포함하는 곱셈-덧셈 선형 논리($\mu\text{MALL}_\infty$)의 컷 제거(cut-elimination) 과정이 압축 성질을 만족함을 증명했습니다. 이는 비정형 증명 이론의 핵심적인 기술적 난제를 해결한 것입니다.

4. 연구의 의의 (Significance)

• 이론적 통합: 산술적/위상수학적 접근과 공변적 접근 사이의 간극을 메우고, 용어 리라이팅과 증명 리라이팅을 하나의 이론으로 통합했습니다.
• 증명 기법의 혁신: 압축 성질에 대한 증명을 공변적 방식으로 재구성함으로써, 더 직관적이고 일반적인 증명 절차를 제공했습니다.
• 실용적 가치: $\mu\text{MALL}_\infty$에서의 컷 제거 압축 증명은 고정점을 가진 다양한 논리 시스템(직관 논리, 고전 논리, 시간 논리 등)의 컷 제거를 증명하는 데 있어 핵심적인 도구(key lemma)로 활용될 수 있습니다.
• 향후 연구 방향 제시: 공변적 프레임워크를 통해 비정형 증명 이론의 메타 이론을 Rocq(Coq)와 같은 증명 보조기(proof assistant)에서 형식화(formalization)할 수 있는 길을 열었습니다.