有界な余帰納的定義による非同期マルチパーティセッション型の無限トレース意味論

本発表は進行中のマルチパーティセッション型の拡張に関する研究について述べる．マルチパーティセッション型（MPST）は並行分散プログラミングのための型である．MPSTを用いた開発フローは，グローバル型と呼ばれる，システム全体の通信シナリオを表す単一の型をデザインすることから始まる．このため，グローバル型の意味論の理解はMPSTにおける鍵である．しかしながら，グローバル型の従来の操作的意味論では，一部の参加者のみが局所的なループを構成している場合に，他の後続の参加者がそれを「追い越す」ような非同期的なアクションを扱えない問題がある．これは，既存の構造操作的意味論における規則の無限展開として現れる．本発表は，この問題に対してDagninoらの有界余帰納定義（bounded coinductive definition）を導入する．有界余帰納定義は，グラフのような循環構造やプログラムの無限のトレースを余帰納法により宣言的に扱える一方で，余帰納的解釈により無制限に現れてしまうトレースを，余規則（corule）によって整形できるようにした体系である．本発表は，有界余帰納定義を用いた，グローバル型のトレース意味論の自然な定義と，これと等価なラベル付き遷移系（LTS）を提案する．本提案に基づき，多様な通信パターンを扱える一般化されたマルチパーティセッション型の理論の構築するとともに，余帰納的定義の見通しの良さを用いた，マルチパーティセッション型のCoqにおける形式化を目指す．

This talk presents our ongoing research on extensions to Multiparty Session Types. Multiparty Session Types (MPST) are types for concurrent and distributed programming. The development flow with MPSTs starts with the design of a global type, which represents the communication scenario for the entire system. Thus, it is mandatory to give a concise understanding on the semantics of global types. However, there is an issue on the conventional operational semantics of global types, as it cannot handle certain kinds of asynchronous communication pattern where some participants make a local loop and actions from other participants “skip” it. This talk introduces the bounded coinductive definition of Dagnino et al. It permits to handle circular structures such as graphs and infinite traces in a declarative manner via coinduction, while tailoring unlimited traces via corules. Based on bounded coinduction, we propose a natural trace semantics for global types and an equivalent labelled transition system (LTS). Based on this, we also talk our perspective for a generalised theory for Multiparty Session Types that can handle a variety of communication patterns, and a plan for formalising Multiparty Session Types in Coq based on the simplifed theory based on bounded coinduction.