Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics

기술적 요약: 게임, 모바일 프로세스 및 함수

문제 제기
본 논문은 고차 언어를 위한 두 가지 주요 의미론적 프레임워크인 연산적 게임 의미론 (OGS) 과 $\pi$-계 (특히 내부 $\pi$-계, $I\pi$) 간의 긴밀하고 형식적인 대응 관계 부재를 다룹니다. 두 모델 모두 $\lambda$-계 항의 행동을 특징짓는 데 사용되지만, 구성 방식에서 현저한 차이를 보입니다. OGS 는 프로그램의 의미 (denotations) 가 환경과의 상호작용을 나타내는 구성 (configurations) 에서 구성적으로 유도되는 내적 (intensional) 모델을 제공하며, 종종 교대성 (alternation) 과 잘 괄호화 (well-bracketing) 와 같은 속성을 강조합니다. 반면, $\pi$-계는 밀너 (Milner) 의 인코딩을 통해 함수를 프로세스로 모델링하며, 대수적 구조와 비동시성 (bisimilarity) 과 같은 프로세스 동치성을 활용합니다. 저자들은 비정형 호출-값 (call-by-value) $\lambda$-계 ($\Lambda_V$) 와 호출-이름 (call-by-name) 에 대해 이러한 모델들 간의 정밀한 연산적 대응 관계를 수립하여, 이들이 동일한 행동 동치성을 유도하고 한쪽의 기법이 다른 쪽으로 전이될 수 있음을 입증하고자 합니다.

방법론
저자들은 $\Lambda_V$의 연산적 의미론을 세 가지 다른 OGS 변형과 두 가지 $I\pi$ 변형에 대해 비교 분석합니다:

1. OGS 변형:
   • 교대 OGS (A-OGS): 프로그램 (플레이어) 과 환경 (상대) 간의 엄격한 교대를 강제합니다.
   • 동시 OGS (C-OGS): 구성 내에서 여러 항이 병렬로 실행되도록 허용합니다.
   • 잘 괄호화된 OGS (WB-OGS): 연속 (continuations) 에 스택 규칙을 강제하여 상대가 후입선출 (LIFO) 순서로만 응답하도록 제한합니다.
2. $I\pi$ 변형:
   • 표준 $I\pi$ LTS: 내부 $\pi$-계를 위한 표준 레이블 전이 시스템입니다.
   • 출력 우선 $I\pi$ LTS (opLTS): 입력 동작이 대기 중인 출력 또는 내부 동작이 없을 때만 가시적이도록 제한된 LTS 로, 순차성 제약을 강제합니다.

핵심 방법론은 OGS 구성 (환경 및 실행 중인 항 포함) 에서 $I\pi$ 프로세스로의 매핑 ($\mathcal{V}$) 을 정의하는 것을 포함하며, 이는 $\lambda$-항에 대한 밀너의 인코딩을 확장합니다. 저자들은 이후 특정 조건 하에서 OGS 의 전이가 $I\pi$의 전이에 대응되고 (그 역도 성립) 함을 보여주는 연산적 대응 정리를 증명합니다. 특히, OGS 에서의 비동시성 증명을 단순화하기 위해 $I\pi$로부터 가져온 "up-to" 기법 (특히 context up-to 및 composition up-to) 을 활용합니다. 또한 프로세스 계산의 병렬 구성과 유사하게 트레인의 인터리빙을 모델링하기 위해 OGS 구성을 위한 텐서 곱을 도입합니다.

주요 기여

1. 연산적 대응: 본 논문은 다음 간의 긴밀한 연산적 대응 관계를 수립합니다:

   • 출력 우선 LTS (opLTS) 하의 A-OGS 와 $I\pi$.
   • 표준 LTS 하의 C-OGS 와 $I\pi$.
     이러한 대응 관계는 내부 감소를 고려하기 위해 확장 관계 ($\lesssim$) 를 활용하여 강 (strong) 및 약 (weak) 전이 모두에 대해 성립합니다.

2. 동치성 일치: 저자들은 모든 이러한 모델이 $\lambda$-항에 유도하는 행동 동치성이 일치함을 증명합니다. 구체적으로:

   • A-OGS, C-OGS, 그리고 $I\pi$(표준 및 opLTS 모두) 의 트레인 동치성과 비동시성은 $\Lambda_V$ 항에 대해 동일한 관계를 정의합니다.
   • 이 유도된 동치성은 Lassen 의 eager normal-form 비동시성(종종 Lassen 의 트리로 시각화됨) 으로 식별됩니다.
   • 완전한 트레인 (종료하는 상호작용을 설명하는 트레인) 의 경우, 교대, 동시, 그리고 잘 괄호화된 OGS 의 의미론도 일치합니다.

3. 기법의 전이:

   • Composition up-to: 저자들은 $I\pi$로부터 "context up-to" 및 "expansion" 기법을 OGS 로 가져옵니다. 그들은 OGS 를 위한 새로운 기법인 **"composition up-to"**를 정의하는데, 이를 통해 복잡한 구성을 기본 요소 (싱글톤 구성) 로 분할하여 독립적으로 추론할 수 있게 됩니다.
   • 합동성과 구성성: $I\pi$와의 대응 관계를 활용함으로써, 논문은 OGS 에 대한 합동성 속성 (예: $M \sim N$이면 $C[M] \sim C[N]$) 을 유도하고 트레인의 인터리빙을 계산하는 구성을 위한 텐서 곱을 정의합니다.

4. 저장에 대한 완전 추상화: 잘 괄호화된 OGS 에서의 완전한 트레인 연구는 가변 저장소 (mutable store) 가 있는 $\lambda$-계에 대한 문맥적 동치성과 연결됩니다. 논문은 $\lambda$-항을 $I\pi$로 인코딩하는 것이 저장소가 확장된 $\lambda$-계로 작성된 문맥에 대해 완전 추상화 결과를 산출함을 보여줍니다.

5. 호출-이름 확장: 논문은 비정형 호출-이름 $\lambda$-계에 대한 유사한 대응 관계를 개략적으로 제시하며, 유도된 동치성이 Lévy-Longo 트리와 일치함을 보여줍니다.

결과

• 정리 6.7 및 7.3: 해당 LTS 하에서 OGS 구성과 $I\pi$ 프로세스 간의 연산적 대응 관계를 수립합니다.
• 계 6.12 및 7.7: $\lambda$-항에 대해 A-OGS, C-OGS, 그리고 $I\pi$의 트레인 동치성과 비동시성이 동일함을 보여줍니다.
• 정리 8.1: "composition up-to" 기법을 사용하여 C-OGS 비동시성이 Lassen 의 eager normal-form 비동시성과 일치함을 직접 증명합니다.
• 정리 12.2: 완전 트레인 동치성이 WB-OGS, A-OGS, 그리고 C-OGS 간에 동일함을 증명합니다.
• 보조정리 7.16 및 정리 7.17: $I\pi$로부터 가져온 C-OGS 에 대한 "reduction 및 composition up-to 비동시성"의 건전성을 증명합니다.

의의
본 논문은 OGS 와 $\pi$-계 간의 "긴밀하고 정밀한 대응 관계"를 수립하는 데에 주된 의의가 있다고 주장합니다. 이 연결은 두 모델 간에 결과와 기법의 전이를 가능하게 합니다. 구체적으로:

• OGS 가 게임 이론적 프레임워크 내에서 직접 개발하기 어려운 풍부한 대수적 구조와 강력한 증명 기법 (up-to 기법 등) 을 $\pi$-계로부터 활용할 수 있게 합니다.
• $\pi$-계가 OGS 의 원어 (source language) 에 대한 근접성과 제어 연산자나 저장소와 같은 특정 계산 효과를 모델링하는 유연성으로부터 혜택을 받을 수 있게 합니다.
• $\lambda$-계 의미론에 대한 통합된 관점을 제공하여, OGS 의 "의미론적 입방체 (Semantic Cube)" 조건 (교대, 잘 괄호화) 과 $I\pi$의 순차성 제약 (opLTS 를 통해) 이 동전의 양면임을 보여주며, 둘 다 동일한 근본적인 행동 동치성 (호출-값의 경우 Lassen 의 트리) 을 특징짓습니다.

저자들은 게임 의미론과 프로세스 계산 간의 유사성이 이전에 탐구된 바 있으나 (예: 전략을 프로세스로 번역), 본 작업은 함수의 *해석 (interpretation)*에 대한 직접적인 비교와 OGS 에 대한 새로운 결과를 유도하기 위한 증명 기법의 체계적인 전이에서 차별화된다고 지적합니다.