The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
复制标题
因果几何：交互的多标记几何及其因果展开
DOI：
--
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
P. Clairambault
中科院分区：
文献类型：
--
作者：
Simon Castellan;P. Clairambault
介绍了一种用于理想化并行ALGOL(IPA)的多令牌机，IPA是一种具有共享状态和信号量的高阶并发程序设计语言。我们的机器采用术语的合成解释的形式作为Petri网结构，特定的有色Petri网。对于IPA的纯功能片段，我们的机器在概念上接近交互令牌机的几何形状，源于线性逻辑，并将高阶计算表示为令牌通过表示该术语的图(证明网)的低级别过程。在此，我们将这些思想与一阶命令式并发程序表示为有色Petri网的民俗思想结合起来。为了证明我们的机器在参考操作语义方面具有足够的计算能力，我们遵循游戏语义，将类型表示为指定计算事件之间的依赖和冲突的特定游戏。Petri网策略是指从类型中提取出的遵守游戏规则的Petri网结构。我们展示了在事件结构上的并发博弈意义下，Petri网策略如何展开为并发策略。这种与并发策略的联系不仅允许我们证明机器的充分性，还允许我们在操作上生成高阶类型程序行为的因果描述，这与并发游戏中的解释在外延上是一致的。
We introduce a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. Our machine takes the shape of a compositional interpretation of terms as Petri structures, certain coloured Petri nets. For the purely functional fragment of IPA, our machine is conceptually close to Geometry of Interaction token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. We combine here these ideas with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets. To prove our machine computationally adequate with respect to the reference operational semantics, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. Petri strategies are those Petri structures obeying the rules of the game extracted from the type. We show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This link with concurrent strategies not only allows us to prove adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types, which is shown to coincide with that given denotationally by the interpretation in concurrent games.