TY - GEN
T1 - Temporal structures
AU - Casley, Ross
AU - Crew, Roger F.
AU - Meseguer, José
AU - Pratt, Vaughan
N1 - Funding Information:
'f Dept. of Computer Science, Stanford University, Stanford, CA 94305 :~ SRI International, Menlo Park, CA 94025 and Center for the Study of Language and Information, Stanford University, Stanford, CA 94305 :~ Supported by the Office of Naval Research under contracts N00014-86-C-0450 and N00014-88-C-0618, and by the National Science Foundation under grant CCR-8707155.
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1989.
PY - 1989
Y1 - 1989
N2 - 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,.., (formula presented), 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 (formula presented)! = premetric spaces.
AB - 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,.., (formula presented), 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 (formula presented)! = premetric spaces.
UR - http://www.scopus.com/inward/record.url?scp=85029841289&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85029841289&partnerID=8YFLogxK
U2 - 10.1007/BFb0018343
DO - 10.1007/BFb0018343
M3 - Conference contribution
AN - SCOPUS:85029841289
SN - 9783540516620
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 21
EP - 51
BT - Category Theory and Computer Science - Proceedings
A2 - Rydeheard, David E.
A2 - Poigne, Axel
A2 - Pitts, Andrew M.
A2 - Pitt, David H.
A2 - Dybjer, Peter
PB - Springer
T2 - 3rd International Conference on Category Theory and Computer Science, CTCS 1989
Y2 - 5 September 1989 through 8 September 1989
ER -