Presheaf Models for the pi-Calculus
Presheaf Models for the pi-Calculus
复制标题
pi 微积分的 Presheaf 模型
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
G. Winskel
中科院分区：
文献类型：
--
作者：
Gian Luca Cattani;I. Stark;G. Winskel
近期的研究表明，预层范畴提供了一种并发的通用模型，其具有基于开映射的双模拟的内在概念。在此展示了这种方法如何也能处理这样的系统：随着进程的演化，动作的语言可能会动态变化。例子是π - 演算，一种用于“移动进程”的演算，其通信拓扑随着通道的创建和丢弃而变化。在一个索引的函子范畴内，为π - 演算描述了一种指称语义；该模型对于双相似性是完全抽象的，也就是说，从开映射得到的模型中的双模拟与从π - 演算的操作语义得到的通常的双模拟是一致的。虽然注意力集中在π - 演算的“迟”语义上，但也说明了如何能涵盖“早”语义及其他变体。
Recent work has shown that presheaf categories provide a general model of concurrency, with an inbuilt notion of bisimulation based on open maps. Here it is shown how this approach can also handle systems where the language of actions may change dynamically as a process evolves. The example is the π-calculus, a calculus for ‘mobile processes’ whose communication topology varies as channels are created and discarded. A denotational semantics is described for the π-calculus within an indexed category of profunctors; the model is fully abstract for bisimilarity, in the sense that bisimulation in the model, obtained from open maps, coincides with the usual bisimulation obtained from the operational semantics of the π-calculus. While attention is concentrated on the ‘late’ semantics of the π-calculus, it is indicated how the ‘early’ and other variants can also be captured.