기술 요약: Distant Bang Calculus를 위한 근사 이론 (Approximation Theory)

1. 문제 정의

근사 이론(Approximation theory)은 유한 또는 무한의 수단을 통해 프로그램의 동작을 특징짓는 $\lambda$-계산 의미론의 핵심적인 접근 방식 역할을 한다. Böhm Tree와 테일러 전개(Taylor Expansion)를 통해 Call-by-Name(CbN)에 대해서는 잘 확립되어 있으나, Call-by-Value(CbV) 환경은 역사적으로 뒤처져 왔다. 최근 CbV Böhm tree(예: Kerinec [29, 28])의 발전은 표준 CbV 축약(Plotkin의 $\beta_v$)이 너무 약하여, 인자가 정규형(normal form)이지만 값(value)이 아닌 경우 축약이 막히는 현상을 드러냈다. 이는 $\sigma$-규칙(permutation rules)을 포함하는 $\lambda\sigma_v$-calculus 또는 거리 기반 계산법(dCbV)과 같은 대안적 프레임워크를 필요로 했다.

**Bang-calculus (Bang)**는 선형 논리(Linear Logic) 변환을 통해 CbN과 CbV를 모두 포괄하는 통합 프레임워크로 제안되었다. 그러나 표준 Bang-calculus는 부적절한 redex가 평가를 차단하는 CbV의 문제를 그대로 물려받는다. $\sigma$-규칙이 이론적으로 이를 해결할 수 있지만, Bang 환경에서는 순환성(confluence)을 보존하는 데 실패한다. distant Bang-calculus (dBang) [15]는 명시적 치환(explicit substitutions)과 "distant" 축약을 활용하여 $\sigma$-규칙 없이도 순환성을 보장함으로써 이 문제를 해결한다.

dBang의 순환성 및 의미론적 유효성(meaningfulness)에 관한 진전[30, 9, 15]에도 불구하고, dBang에 대한 포괄적인 **근사 이론(approximation theory)**은 여전히 미개발 상태로 남아 있었다. 구체적으로, dBang을 위한 Böhm 유사 근사 트리(Böhm-like approximation trees)와 테일러 전개를 정의하는 통일된 프레임워크가 없었으며, 이들을 연결하는 교환 정리(Commutation Theorem)에 대한 증명도 부재했다. 또한, 최근의 일반적인 접근 방식(Mazza & Dufour [19])이 존재하기는 하나, 직접적인 의미론적 유효성 개념이 결여되어 있으며 CbN과 CbV의 구체적인 해결 가능성(solvability)/검사 가능성(scrutability) 개념과 명확하게 연결되지 않는다.

2. 방법론

저자들은 두 가지 핵심 패러다임인 테일러 전개(자원 민감적 의미론)와 근사 트리(Böhm 전통)를 통합하여 dBang을 위한 통일된 근사 이론을 개발한다.

2.1 자원 계산법 ($\delta$Bang)

저자들은 테일러 전개의 대상으로 자원 계산법 $\delta$Bang을 정의한다. 이 계산법은 지수($!M$)를 유한 멀티셋(bags)의 자원 항들로 대체한다.

• 근사 관계 ($\triangleleft!$): 자원 항과 dBang 항 사이의 다중 선형(multilinear) 관계가 정의된다.
• 축약: 축약 관계 $\Rightarrow_\delta$는 bag의 순열로 인해 비결정적이지만, 선형성 덕분에 강한 정규화(strongly normalizing)를 가진다.
• 테일러 정규형 (Taylor Normal Form, TNF): 모든 자원 근사항(resource approximants)의 완전한 정규형들의 집합으로 정의된다.

2.2 근사 트리 (Approximation Trees)

저자들은 정의되지 않은 계산을 나타내는 기호 $\bot$을 추가하여 dBang의 근사 트리를 정의한다.

• 근사항 (Approximants): 정의되지 않은 하위 항을 포함할 수 있는 정규형을 나타내는 용어의 문법이 정의된다.
• 이상 완결 (Ideal Completion): 맥락적 전순서(contextual preorder) $\sqsubseteq$ 하에서 항 $M$의 근사항 집합 $A(M)$은 이상(ideal)을 형성한다. 근사 트리 $AT!(M)$은 이 이상의 상한(supremum)이며, 항의 동작의 극한을 나타낸다.
• 구분: 클래식한 CbN Böhm tree가 근사항을 head normal form으로 제한하는 것과 달리, 저자들은 dBang의 특수한 의미론과 임베딩을 수용하기 위해 더 넓은 정의(CbN의 Lévy-Longo tree 및 CbV의 CbV Böhm tree와 유사함)를 채택한다.

2.3 변환 (Translations)

프레임워크를 검증하기 위해, 저자들은 distant Call-by-Name (dCbN) 및 **distant Call-by-Value (dCbV)**를 dBang으로 변환하는 기존의 변환들을 활용한다. 이들은 이러한 변환들이 축약 단계를 보존하고 의미론적 유효성을 보존함을 증명하여, dBang에서 도출된 결과가 dCbN 및 dCbV로 투영될 수 있도록 한다.

3. 주요 기여 및 결과

3.1 시뮬레이션 및 교환 (Simulation and Commutation)

본 논문은 dBang의 연산적 축약과 그 근사 사이의 엄밀한 연결 고리를 구축한다.

• 시뮬레이션 정리 (정리 21): dBang 항의 테일러 전개는 그 축약을 시뮬레이션한다. 즉, $M \to! N$이면, $T(M)$은 병렬 자원 축약(parallel resource reduction)을 통해 $T(N)$으로 축약된다.
• 교환 정리 (정리 46): 이것이 핵심 결과이다. 이는 항의 근사 트리의 테일러 전개가 해당 항 자체의 테일러 정규형과 같음을 나타낸다:
  $$T(AT!(M)) = TNF(M)$$
  이는 무한한 의미론(트리)과 자원 민감적 의미론(테일러 전개)이 dBang 프레임워크 내에서 일관됨을 확인해 준다.

3.2 CbN 및 CbV 사례의 회복

dCbN과 dCbV를 dBang으로 변환함으로써, 저자들은 이 특정 계산법들에 대한 근사 이론을 회복한다.

• 정리 59: dBang으로 변환된 항의 근사 트리는 소스 계산법에서의 근사 트리의 변환과 정확히 일치한다.
• 정리 60: 교환 정리는 dBang의 결과로부터 직접적인 결과로서 dCbN 및 dCbV 모두에 대해 성립한다.

3.3 의미론적 유효성(Meaningfulness) 및 테일러 전개

논문은 의미론적 유효성(테스트 맥락 하에서 항이 값으로 축약되는 능력)과 테일러 정규형의 비공집합(non-emptiness) 사이의 관계를 조사한다.

• 정리 61: 만약 dBang 항이 의미론적으로 유효하다면, 그 테일러 정규형은 공집합이 아니다 ($TNF(M) \neq \emptyset$).
• 역관계: 일반적인 dBang 계산법에 대해서는 역관계가 성립하지 않는다. "clash"($xx$와 같은 항)를 포함하는 의미론적 유효성이 없는 항들이 존재하기 때문이다.
• 파편 (Fragments): 그러나 dCbN($dBang_N$) 및 dCbV($dBang_V$)에 해당하는 특정 파편들에 대해서는 동등성이 복구된다:
  • 따름정리 68 (dCbN): $M$은 의미론적으로 유효할 필요충분조건은 $TNF(M) \neq \emptyset$이다.
  • 따름정리 73 (dCbV): $M$은 의미론적으로 유효할 필요충분조건은 $TNF(M) \neq \emptyset$이다.

4. 의의 및 주장

본 논문은 dCbN과 dCbV를 위한 무한한 의미론과 자원 민감적 의미론을 단일 시스템(dBang) 내에서 포착하는 근사 이론의 통합적 프레임워크를 제공한다고 주장한다.

• 통합: CbN과 CbV를 위한 별개의 발전 과정이 dBang 계산법 아래로 귀속될 수 있음을 입증하여, 별도의 의미론적 이론이 필요했던 역사적 요구를 해결한다.
• 강건성 (Robustness): distant 변형(dBang)을 사용함으로써, 저자들은 표준 Bang 계산법에서 $\sigma$-규칙과 관련된 순환성 문제를 피하고, 근사 이론을 위한 더 깨끗한 환경을 제공한다.
• 의미론의 가교: 교환 정리는 "형태 기반(shape-based)" 무한 의미론(근사 트리)과 "자원 기반(resource-based)" 미분 의미론(테일러 전개) 사이의 깊은 가교를 dBang이라는 통일된 설정 내에서 구축한다.
• 의미론적 유효성의 특징 규명: 본 연구는 dCbN 및 dCbV에 대해 비어 있지 않은 테일러 정규형을 통해 의미론적 유효성을 구문론적으로 특징짓는 방법을 제공하며, 이는 기존의 표준 CbN/CbV에 대한 결과를 확장한 것이다.

저자들은 변환된 파편들에 대해서는 의미론적 유효성과 비어 있지 않은 테일러 정규형 사이의 동등성이 성립하지만, (변환을 넘어선) 더 큰 일반적 dBang 파편이 이와 유사하게 특징지어질 수 있는지 여부는 여전히 미해결 과제로 남아 있다고 겸허히 언급한다. 또한, Mazza와 Dufour의 연구를 바탕으로 이러한 개념을 증명 구조(proof structures)로 확장하는 향후 연구 방향을 제시한다.