Temporal Structures
Ross Casley, Roger F. Crew, José Meseguer, Vaughan Pratt · Lecture notes in computer science · 1991
We have been developing a process specification language PSL based on an algebra of labeled partial orders. The order encodes temporal precedence of events, and the event labels represent the actions performed. In this paper we extend this basis to encompass other temporal metrics by generalizing partial orders to generalized metric spaces, an interpretation of enriched categories due to Lawvere.Two needs then arise: a means of specifying kinds of spaces, and a well-defined semantics for PSL relative to a given kind. We define kinds to be semiconcrete symmetric monoidal (ssm) categories, forming the category SSM. We find in SSM not only kinds of spaces, with and without labels, but their underlying metrics and kinds of labeling alphabets, including certain basic bicomplete kinds 1,2,3,..., \(\bar R_ + \), etc. We equip SSM with functors ! and ⊳, where D ! denotes the category of spaces on a metric D and D ⊳ ɛ that of D-structured ɛ-labeled spaces. Finally we establish the continuity of these operators.We define the kind language KL whose terms are formed via the operators ! and ⊳ from constants for the basic kinds. A KL kind is the denotation of a KL term, by induction on which we obtain that all KL kinds are bicomplete. We give a uniform semantics for PSL relative to any KL kind, whether a metric, a metric space, an alphabet, or a labeled metric space. That this semantics is well-defined follows from its adherence to universal constructions and bicompleteness of KL kinds.KL kinds include 1! = sets, 1 ⊳ 1! = pointed sets, 2! = preordered sets, 2! ⊳ 1! = labeled preordered sets, 1!! = categories, 2!! = order-enriched categories, 1!!! = 2-categories, 3! = causal spaces, 3′! = prossets, and \(\bar R_ + \)! = premetric spaces.