Pi-calculus를 외연적 의미론 (Denotational Semantics)에 연결하기

우리는 AWpi라고 불리는 비동기 Pi-calculus (Asynchronous pi-calculus)의 방언을 소개합니다. 이 방언에서는 (1) 입력 이름 (input name)은 어느 시점에서든 최대 하나의 프로세스에 의해서만 소유될 수 있으며, (2) 각 이름은 입력 능력 (input capability) 또는 출력 능력 (output capability) 중 하나만을 가집니다. 그 결과, 와이어 (wires, 또는 전달자 (forwarders), 즉 한 이름으로 값을 수신하여 재전송하는 프로세스)라고 불리는 특수한 프로세스들은 다른 AWpi 프로세스와 합성될 때 대입 (substitutions)처럼 동작합니다. 따라서 AWpi는 자연스럽게 하나의 범주 (category)를 생성하며, 이 범주의 사상 (morphisms)은 AWpi 프로세스들(참조적 행동 동치 (reference behavioural equivalence), 즉 barbed congruence를 기준으로 함)이고, 대상 (objects)은 타입 (types)이며, 와이어는 항등 사상 (identity morphisms)으로 작용합니다. 우리는 게임 의미론 (game semantics)에서 얻은 통찰을 활용하여, 프로세스의 범주가 문헌에 등장하는 일반적인 고차 언어 (higher-order language) 기능의 해석에 필요한 구조를 가진 (부분) 범주들로 더 조직화될 수 있음을 보여줍니다. 특히, 우리는 병행 게임 의미론 (concurrent game semantics)이 가진 범주론적 구조인 상대적 Seely 범주 (relative Seely category)를 구축합니다. 동시에, AWpi는 개발 및 증명 과정에서의 상당한 기술적 차이에도 불구하고, 표현력 (expressiveness)이 보존되고 운영 및 대수 이론 (operational and algebraic theory)이 유사한 방식으로 발전한다는 점에서 일반적인 Pi-calculi의 전통을 따릅니다. 요약하자면, AWpi의 목표는 Pi-calculi의 운영 및 대수적 전통에 충실하면서도 프로그래밍 언어를 위한 외연적 모델 (denotational models)의 전통과 연결하는 것입니다.