非正曲率空间中的有向同伦
Directed Homotopy in Non-Positively Curved Spaces
AI总结：
本文研究仅用互斥锁的并发程序，通过预立方集引入非正曲率概念，证明有向与非有向同伦一致，并借助广义度量空间实现几何化，为并发程序语义提供新视角。
摘要：
并发程序的一种语义可以通过预立方集给出，以便研究动作之间的（高阶）交换，从而编码程序可能执行空间的“几何”结构。这里，我们研究仅使用互斥锁（最广泛使用的同步原语）的程序的特殊情况。我们证明在这种情况下，所得程序具有非正曲率，这一概念我们在此针对预立方集引入并研究，可以看作是众所周知的度量空间概念的一个代数类比。利用这一点以及范畴重写技术，我们能够证明在这些预立方集中，有向路径的有向同伦与非有向同伦是一致的。最后，我们研究预立方集在度量空间中的几何实现，以表明我们关于预立方集的条件实际上与度量空间的条件一致。由于度量空间范畴不是余完备的，我们转而使用广义度量空间并研究它们的一些性质。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
