一句话：本文用预立方集合为互斥锁并发程序建模，引入非正曲率概念，证明有向同伦与无向同伦在特定有向路径上一致。
并发程序的语义可用预立方集合（precubical sets）给出，以刻画动作间的高阶交换及可能执行空间的“几何”结构。本文研究仅使用互斥锁（mutex）这一最广泛同步原语的程序，证明此类程序生成的预立方集合具有非正曲率；作者为预立方集合引入并研究该概念，视其为度量空间非正曲率性质的代数类比。借助这一性质及范畴重写技术，论文证明在这些预立方集合中，有向路径的有向同伦与无向同伦一致。最后研究预立方集合在度量空间中的几何实现，说明所加条件与度量空间相应条件一致；由于度量空间范畴不余完备，需转向广义度量空间并研究其性质。
A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding the "geometry" of the space of possible executions of the program. Here, we study the particular case of programs using only mutexes, which are the most widely used synchronization primitive. We show that in this case, the resulting programs have non-positive curvature, a notion that we introduce and study here for precubical sets, and can be thought of as an algebraic analogue of the well-known one for metric spaces. Using this it, as well as categorical rewriting techniques, we are then able to show that directed and non-directed homotopy coincide for directed paths in these precubical sets. Finally, we study the geometric realization of precubical sets in metric spaces, to show that our conditions on precubical sets actually coincide with those for metric spaces. Since the category of metric spaces is not cocomplete, we are lead to work with generalized metric spaces and study some of their properties.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1908-06684,
title = {Directed Homotopy in Non-Positively Curved Spaces},
author = {Eric Goubault and Samuel Mimram},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:4)2020}
}