Presheaf Models for Concurrency
Presheaf Models for Concurrency
复制标题
Presheaf 并发模型
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
G. Winskel
中科院分区：
文献类型：
--
作者：
Gian Luca Cattani;G. Winskel
本文研究了并行计算中的预层模型。一个目的是利用一般机械周围的预压为目的的过程演算。传统的模型，如同步树和事件结构已被证明是完全和忠实地嵌入在特定的预层模型，以这样一种方式，互模拟，通过存在的一个跨度的开放地图表示，是保守的。正如Joyal和Moerdijk的工作所示，预层中有丰富的结构，它们通过非常一般的性质的参数来保持开映射和互模拟。本文贡献了类似的结果，但偏向于进程演算的互模拟问题。它关注的是建模过程的建设上presheaves，显示这些保持开放的地图，并将这些结果转移到传统的模型的过程。这里的一个新结果是，广泛的左Kan扩展，类别之间的presheaves，保持开放的地图。作为一个推论，这也意味着在预层范畴之间的任何保余限函子都保持开映射。一个特定的左Kan扩展与事件结构上的细化操作相吻合。提出了一个广泛的类的预层模型的一般过程演算。一般的参数给出了为什么一个预层模型的操作保持开放的地图，为什么特定的预层模型的操作与传统的模型相吻合。
This paper studies presheaf models for concurrent computation. An aim is to harness the general machinery around presheaves for the purposes of process calculi. Traditional models like synchronisation trees and event structures have been shown to embed fully and faithfully in particular presheaf models in such a way that bisimulation, expressed through the presence of a span of open maps, is conserved. As is shown in the work of Joyal and Moerdijk, presheaves are rich in constructions which preserve open maps, and so bisimulation, by arguments of a very general nature. This paper contributes similar results but biased towards questions of bisimulation in process calculi. It is concerned with modelling process constructions on presheaves, showing these preserve open maps, and with transferring such results to traditional models for processes. One new result here is that a wide range of left Kan extensions, between categories of presheaves, preserve open maps. As a corollary, this also implies that any colimit-preserving functor between presheaf categories preserves open maps. A particular left Kan extension is shown to coincide with a refinement operation on event structures. A broad class of presheaf models is proposed for a general process calculus. General arguments are given for why the operations of a presheaf model preserve open maps and why for specific presheaf models the operations coincide with those of traditional models.