Directed Homotopy in Non-Positively Curved Spaces

摘要: A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding "geometry" space possible executions program. Here, we particular case only mutexes, which are most widely used synchronization primitive. We show that this case, resulting have non-positive curvature, a notion introduce and here for thought as an algebraic analogue well-known one metric spaces. Using it, well categorical rewriting techniques, then able directed non-directed homotopy coincide paths these sets. Finally, geometric realization sets spaces, our conditions on actually with those Since category spaces is not cocomplete, lead work generalized some their properties.