How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)

기술 요약: "아코디언 연주법: $\lambda$-계산의 선형 근사의 균일성 및 (비)보존성"

문제 정의
본 논문은 Ehrhard와 Regnier의 미분 $\lambda$-계산 및 리소스 계산(resource calculus) 프레임워크 내에서, $\lambda$-계산의 선형 근사가 갖는 **보존성(conservativity)**을 조사한다. 테일러 전개 $T(M)$이 $\beta$-축약(즉, $M \to_\beta N$이면 $T(M) \twoheadrightarrow_r T(N)$)을 시뮬레이션할 수 있다는 점은 잘 알려져 있으나, 그 역의 문제, 즉 리소스 계산에서의 모든 축약이 실제 소스 $\lambda$-계산에서의 축약에 의해 유도되는가 하는 질문이 남아 있다.

형식적으로, 리소스 계산에서의 축약 $T(M) \twoheadrightarrow_r T(N)$(무한한 리소스 항들의 선형 결합에 작용하는)이 주어졌을 때, $\beta$-축약 시퀀스 $M \to_\beta N$이 존재하는가? 저자들은 두 가지 설정을 구분한다:

1. 유한 $\lambda$-계산: 항(terms)은 유한하며, 축약은 유한한 시퀀스이다.
2. 무한 $\lambda$-계산 ($\lambda^{001}$): 항은 무한할 수 있으며(공인적/coinductive), 축약은 무한한 시퀀스($\to^{001}_\beta$)일 수 있다(단, redex들이 증가하는 깊이에서 발사된다는 조건 하에).

핵심 문제는 이러한 설정들에서 선형 근사가 소스 계산의 **보존적 확장(conservative extension)**인지 여부이다.

방법론
저자들은 재작성 이론(rewriting theory), 공인적 정의(coinductive definitions), 그리고 "매시업(mashup)" 기법(소스 항과 그 리소스 근사치를 연결하는 기법)을 결组合하여 사용한다.

1. 유한 사례 분석: 유한한 항에 대해, 저자들은 Kerinec와 Vaux Auclair가 사용한 "매시업" 증명 기법을 변형하여 적용한다. 이들은 $\lambda$-항과 그 리소스 근사치를 연결하는 관계 $\vdash$를 정의한다. $T(M) \twoheadrightarrow_r T(N)$이면 $M \vdash T(N)$이고, 나아가 $M \vdash T(N)$이 $M \to^*_\beta N$을 함의함을 증명함으로써, 유한한 경우의 보존성을 확립한다.
2. 무한 사례 반례 (아코디언): 무한한 경우를 다루기 위해, 저자들은 특정 반례인 **아코디언(Accordion, $A$)**을 구성한다. 이 항은 구조를 "늘리고 압축하는" 무한한 축약 시퀀스를 시뮬레이션하도록 설계되었다.
   • 항 $A$는 무한한 항 $\bar{A} = (\langle T \rangle)(\langle F \rangle)\omega$를 근사하는 항들의 시퀀스로 축약된다.
   • 결정적으로, $T(A) \twoheadrightarrow_r T(\bar{A})$는 성립하지만, 저자들은 유효한 무한 $\beta$-축약 $A \to^{001}_\beta \bar{A}$가 존재하지 않음을 증명한다. $A$의 축약 경로들은 무한 $\beta$-축약에 요구되는 층화 조건(stratification condition, Lemma 2.5)을 위반하는, 제한된 깊이에서의 "전역적(global)" 단계를 필요로 하기 때문이다.
3. 균일성 및 일관성: 무한한 설정에서 보존성을 회복하기 위해, 저자들은 Ehrhard와 Regnier의 연구에서 핵심적이었던 **균일성(uniformity)**을 도입한다. 이들은 리소스 항들에 대한 일관성 관계($\bowtie$)를 정의하고, 축약 관계를 균일 합(uniform sums)(모든 요소가 서로 쌍을 이루어 일관적인 합)으로 제한한다.
   • 이들은 균일 리소스 축약($\to^{\curvearrowright}_r$)과 그 무한 폐쇄(infinitary closure, $\to^{\curvearrowright \infty}_r$)를 정의한다.
   • 이러한 제한은 리소스 계산에서의 축약이 실제 $\lambda$-계산의 축약과 엄격하게 대응하도록 보장하며, 실제 $\beta$-축약으로 매핑되지 않는 "비균일한(non-uniform)" 경로들을 제거한다.
4. $\beta_\perp$로의 확장: 저자들은 이 결과들을 $\beta_\perp$-축약($\bot$이 해결 불가능한 항들을 붕괴시키는 축약)으로 확장하여, 균일성이 $\bot$-축약이 포함된 경우에도 보존성을 유지함을 보여준다.

주요 기여

1. 유한 항에 대한 보존성: 선형 근사가 유한 $\lambda$-계산에 대해 보존적임을 입증하는 엄밀한 증명을 제공한다 (Theorem 3.1).
2. 무한 항에 대한 비보존성: 표준적인 점별 리소스 축약($\twoppedrightarrow_r$)은 무한 $\lambda$-계산에 대해 보존적이지 않음을 보여준다. 저자들은 아코디언($A$) 반례를 구성하여 $T(A) \twoheadrightarrow_r T(\bar{A})$가 $A \to^{001}_\beta \bar{A}$를 함의하지 않음을 증명한다 (Theorem 4.4).
3. 균일성을 통한 복구: 저자들은 균일성이 무한 $\lambda$-계산의 보존성을 회복하는 데 필요한 누락된 요소임을 식별한다. 리소스 계산을 균일 축약($\to^{\curvearrowright \infty}_r$)으로 제한함으로써, 선형 근사가 무한 $\lambda$-계산의 보존적 확장이 됨을 증명한다 (Theorem 5.10).
4. $\beta_\perp$로의 확장: 표준 축약의 비보존성은 $\beta_\perp$-축약으로도 확장되며, 균일한 접근 방식은 $\beta_\perp$에 대해서도 보존적임을 보여준다 (Theorems 5.18 및 5.19).

결과

• 유한 설정: 리소스 축약에 의한 유한 $\beta$-축약의 시뮬레이션은 보존적이다.
• 무한 설정 (표준): 표준적인 점별 리소스 축약에 의한 무한 $\beta$-축약의 시뮬레이션은 비보존적이다. 아코디언 항 $A$는 리소스 계산에서는 $\bar{A}$로 축약되지만, $\lambda$-계산에서는 그렇지 않다.
• 무한 설정 (균일): 균일 리소스 축약에 의한 무한 $\beta$-축약의 시뮬레이션은 보존적이다.
• $\beta_\perp$ 설정: 표준 축약의 비보존성은 $\beta_\perp$-축약으로 확장되지만, 균일한 축약은 $\beta_\perp$에 대해서도 보존적이다.

의의
본 논문은 선형 근사가 $\lambda$-계산의 역학을 충실하게 모델링하기 위한 정확한 조건을 명확히 한다. 이는 양적 선형 근사가 무한 설정에서 보존적이지 않다는 제1 저자의 박사 학위 논문의 추측을 해결한다.

주된 의의는 균일성이 단순히 테일러 전개의 의미론적 속성일 뿐만 아니라, 보존성을 보장하기 위해 리소스 계산 자체에 적용되어야 하는 필수적인 구문론적 제약임을 식별했다는 점에 있다. 이 제한이 없다면, 리소스 계산은 특히 무한한 항이 존재할 때 소스 $\lambda$-계산에 대응하는 것이 없는 "유령(ghost)" 축약을 허용하게 된다. 본 연구는 "교환 정리(commutation theorem, 정규화가 근사와 교환됨)"를 시뮬레이션과 보존성을 구분함으로써 정교화하며, 시뮬레이션은 일반적으로 성립하지만 보존성을 위해서는 더 엄격한 균일 프레임워크가 필요함을 보여준다.

저자들은 본 연구가 반례에 대한 완전한 증명을 제공하고, $\beta_\perp$-축약으로 분석을 확장함으로써 이전 컨퍼런스 버전을 개선했음을 명시한다. 이는 항들을 그들의 뵘 트리(Böhm trees)와 연결하는 데 매우 중요하다.