Graphical foundations for dialogue games
Graphical foundations for dialogue games
复制标题
DOI：
--
复制
发表时间：
2013-10
期刊：
影响因子：
--
通讯作者：
Cai Wingfield
中科院分区：
文献类型：
--
作者：
Cai Wingfield
在1980年代和1990年代，Joyal和Street开发了一种用于monoidal范畴的各种风格的图形符号，使用平面上绘制的图形，通常称为弦图。特别是，他们的工作包括一个严格的拓扑基础的符号。在2007年，Harmer、Hyland和Mellies给出了游戏语义的正式数学基础，他们使用了一个被称为“时间表”、"时间表“和”堆“的概念。时间表描述了在游戏中使用双头和双头形成的游戏的交错，堆提供了用于回溯的指针。他们的定义本质上是组合的，但研究人员在实践中经常绘制某些图像。在这篇论文中，我们扩展了Joyal和Street的框架，对游戏语义研究人员已经非正式使用的图形方法进行了正式的描述。我们给出了一个几何公式的n-时间表和n-时间表，并证明了他们所描述的游戏是同构的那些描述在Harmer等人。的条款，以及那些由一个更一般的图形表示交错跨游戏的多个组件。我们进一步说明了几何方法的价值，通过证明几个关键属性的证明（例如，组合的时间表是关联的）可以直接进行，反映了平面的几何形状，并超越了Harmer等人的证明中的一些繁琐的组合细节。的条款。我们进一步扩展了形式平面图的框架，以考虑O和P的回溯函子中使用的堆和指针结构。
In the 1980s and 1990s, Joyal and Street developed a graphical notation for various flavours of monoidal category using graphs drawn in the plane, commonly known as string diagrams. In particular, their work comprised a rigorous topological foundation of the notation. In 2007, Harmer, Hyland and Mellies gave a formal mathematical foundation for game semantics using a notions they called ⊸-schedules, ⊗-schedules and heaps. Schedules described interleavings of plays in games formed using ⊸ and ⊗, and heaps provided pointers used for backtracking. Their definitions were combinatorial in nature, but researchers often draw certain pictures when working in practice. In this thesis, we extend the framework of Joyal and Street to give a formal account of the graphical methods already informally employed by researchers in game semantics. We give a geometric formulation of ⊸-schedules and ⊗-schedules, and prove that the games they describe are isomorphic to those described in Harmer et al.’s terms, and also those given by a more general graphical representation of interleaving across games of multiple components. We further illustrate the value of the geometric methods by demonstrating that several proofs of key properties (such as that the composition of ⊸-schedules is associative) can be made straightforward, reflecting the geometry of the plane, and overstepping some of the cumbersome combinatorial detail of proofs in Harmer et al.’s terms. We further extend the framework of formal plane diagrams to account for the heaps and pointer structures used in the backtracking functors for O and P.