Language/OS - Multiplatform Resource Library/LANGUAGE OS.iso/ast_comp/concurre.tar/concurrency/man.tex

LaTeX Document | 1993-07-05 | 127.1 KB | 2,329 lines

% -*- Latex -*-
\documentstyle[11pt]{article}
%\pagestyle{empty}
\headheight 0pt
\headsep 0pt
\textheight 652.4pt
\topmargin 0pt
\long\def\comment#1{}
\newenvironment{definition}{\par\medskip\addtocounter{theorem}{1}%
  \noindent{\bf Definition \arabic{theorem}}\quad
  }{\hfill\qed\quad\medskip}
\def\A{{\bf\mbox{$\cal A$}}}
\def\B{{\bf\mbox{$\cal B$}}}
\def\C{{\bf\mbox{$\cal C$}}}
\def\D{{\bf\mbox{$\cal D$}}}
\def\E{{\bf\mbox{$\cal E$}}}
\def\I{{\bf\mbox{$\cal I$}}}
\def\T{{\bf\mbox{$\cal T$}}}
\def\X{{\bf\mbox{$\cal X$}}}
\def\Y{{\bf\mbox{$\cal Y$}}}
\def\one{{\bf 1}}
\def\two{{\bf 2}}
\def\three{{\bf 3}}
%\def\R{{\mbox{${\bf\bar R}_+$}}}
\def\R{{\bf R}}
\def\Rdp{{\bf R}^{\tt d}}
\def\N{{\mbox{\bf N}}}
\def\Set{{\bf Set}}
\def\SET{{\bf SET}}
\def\SSM{{\bf COSMON}}
\def\Seti{{\bf Seti}}
\def\Pos{{\bf Pos}}
\def\Pom{{\bf Pom}}
\def\Pros{{\bf Pros}}
\def\Prom{{\bf Prom}}
\def\Pomi{{\bf Pomi}}
\def\Cat{{\bf Cat}}
\def\CAT{{\bf CAT}}
\def\Grph{{\bf Grph}}
\def\Hom{{\rm Hom}}
\def\op{^{\rm op}}
\def\ob{{\rm ob}}
\def\min{{\rm min}}
\def\max{{\rm max}}
\def\SR{{\mathord{\bf SR}}}
%\def\DC{\D{\mbox -}\Cat}
%\def\DpC{\D'{\mbox -}\Cat}
\def\Z2{{\mbox{\bf Z$_2$}}}
\def\DYN{{\mbox{\bf DYN}}}
\def\TMP{{\mbox{\bf TMP}}}
\def\d{\delta}
\def\comma{\mathop{\rhd}}
\def\lc{\underline{;}}
\def\ll{\underline{\lambda}}
\def\darrow{\mathop{\downarrow}} % let's flush this, ok?
\def\vertex{\mathop{\rm vert}}
\def\
#1{\stackrel{#1}{\longrightarrow}}
\let\
=\darrow
\def\<#1>{\langle #1 \rangle}
\def\eqalign#1{\vbox{\halign{\hfil$##$&$\quad##$\hfil\cr #1}}}
\def\congh{\raise0.5ex\hbox{$\smash\cong$}}
\def\UV{U\
\def\Tau{T}
\def\qed{\vrule height6pt width4pt depth0pt} % end-of-proof etc.
\mathcode`\:="603A
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newenvironment{proof}{\medskip\noindent{\it Proof}:\quad}{\quad\qed\medskip}
\newenvironment{proofo}{\medskip\noindent{\it Outline of Proof}:\quad}{\quad\qed\medskip}
%%======================================================================%
%%    TeX  macros for drawing rectangular category-theory diagrams    %
%%                                    %
%%            Paul   Taylor                    %
%%                                    %
%%    Department of Computing, Imperial College, London SW7 2BZ    %
%%    [phone] x 5057              [e-mail]    %
%%                                    %
%%        For user documentation, see "diagram.doc.tex"        %
%%                                    %
%%    COPYRIGHT NOTICE:                        %
%%    This package may be copied and used freely for any academic    %
%%    (not commercial or military) purpose, on condition that it    %
%%    is not altered in any way, and that an acknowledgement is     %
%%    included in any published paper using it.            %
%%                                    %
%%======================================================================%
\message{<Paul Taylor's commutative diagrams, 20 December 1989>} \let\then
\relax\font\tenln=line10 \newdimen\zpt\zpt=0pt \def\tozpt{to \zpt}
\mathchardef\lt="313C \mathchardef\gt="313E
\newif\ifincommdiag\incommdiagfalse
\def\diagram{\bgroup\incommdiagtrue\null\baselineskip3.8ex \lineskip\zpt
\lineskiplimit\zpt\mathsurround\zpt\tabskip\zpt\let\\\cr\,\vcenter\bgroup
\halign\bgroup\hfil$##$\hfil&&\hfil$##$\hfil\cr\mathstrut\cr}
\def\enddiagram{\crcr\mathstrut\crcr\egroup\horizreformatmatrix\egroup\,%
\egroup}
\def\commdiag#1{{\diagram#1\enddiagram}}
\def\across#1{\span\omit\mscount=#1 \loop\ifnum\mscount>2 \spAn\repeat
\ignorespaces} \def\spAn{\relax\span\omit\advance\mscount by -1}
\def\horizreformatmatrix{\bombparameters\skip7=\zpt\setbox8=\vbox{}\loop
\setbox9=\lastbox\ifhbox9 \horizreformatrow\setbox8=\vbox{\box9\vskip\skip7%
\unvbox8}\skip7=\lastskip\unskip\repeat\vskip\skip7 \unvbox8 }
\def\horizreformatrow{\setbox9=\hbox{\unhbox9\setbox5=\box9\spanspace\zpt
\prevspace\zpt\skip9=\lastskip\unskip\setbox6=\hbox{}\loop\setbox7=\lastbox
\ifhbox7\setbox0=\hbox{\unhcopy7}\hsize=.5\wd0 \ourspace=.5\wd7 \advance
\ourspace-.5\wd0 \horizreformatcell\skip8=\lastskip\unskip\repeat\hskip\skip8%
\ifhbox5\box5\fi\unhbox6}}
\def\bombparameters{\parfillskip\zpt minus10\hsize\linepenalty9000\parskip
\zpt\parindent\zpt\everypar{}\pretolerance10000 \tolerance10000 \hyphenpenalty
10000 \exhyphenpenalty10000 \adjdemerits0 \doublehyphendemerits0
\finalhyphendemerits0 \leftskip\zpt\rightskip\zpt\looseness0 \hfuzz10\hsize}
\def\addtobomblist{\global\setbox6=\hbox{\box7\hskip\skip8\ifhbox5\ifdim
\ourspace=\zpt\then\box5\else\hbox to\wd5{\kern-\ourspace\unhbox5}\fi\fi
\unhbox6}}
\newdimen\prevspace\newdimen\ourspace\newdimen\spanspace
\def\horizreformatcell{\setbox0=\vtop{\noindent\unhcopy0\endgraf\ifcase
\prevgraf\global\advance\spanspace\ourspace\global\ourspace\zpt\addtobomblist
\or\global\prevspace=\ourspace\addtobomblist\or\setbox2=\lastbox\unskip
\unpenalty\setbox1=\lastbox\global\setbox7=\hbox to.5\wd7{\kern\spanspace
\unhbox2 \unskip\unskip\unpenalty\global\advance\prevspace2\spanspace\kern-%
\prevspace\hskip\parfillskip}\global\ourspace\zpt\prevspace=\wd7
\addtobomblist\global\setbox5=\hbox to\prevspace{\unhbox1 \unskip\unpenalty
\kern-\spanspace\global\spanspace\zpt\hskip\parfillskip}\global\prevspace\zpt
\fi}}
\newif\ifmoremapargs\newif\ifmapargisupper
\def\gettwoargs{\let\upperlabel\empty\let\lowerlabel\empty\moremapargstrue
\mapargisuppertrue\def\cmd{\mapargisupperfalse\ifmoremapargs\then\let\next
\whatis\let\cmd\thecmd\else\let\next\thecmd\fi\next}\whatis}
\def\whatis{\futurelet\thenexttoken\showcat}
\def\getlabeldocmd#1{\ifmapargisupper\def\upperlabel{#1}\else\def\lowerlabel{%
#1}\fi\cmd}
\def\eattokengetlabeldocmd#1{\getlabeldocmd}
\def\eatspacerepeat{\afterassignment\whatis\let\junk= }
\def\catcase#1:#2\esac#3\esacs{{\ifcat\noexpand\thenexttoken#1\gdef\next{#2}%
\else\gdef\next{#3\esacs}\fi}\next}\def\tokcase#1:#2\esac#3\esacs{{\ifx
\thenexttoken#1\gdef\next{#2}\else\gdef\next{#3\esacs}\fi}\next}\def\default:%
#1\esac#2\esacs{#1}\let\esacs\relax
\def\showcat{\catcase\egroup:\moremapargsfalse\cmd\esac\catcase{&}:%
\moremapargsfalse\cmd\esac\catcase$:\moremapargsfalse\cmd\esac\catcase^:%
\mapargisuppertrue\eattokengetlabeldocmd\esac\catcase_:\mapargisupperfalse
\eattokengetlabeldocmd\esac\catcase{ }:\eatspacerepeat\esac\tokcase{\cr}:%
\moremapargsfalse\cmd\esac\tokcase{\crcr}:\moremapargsfalse\cmd\esac\tokcase
\end:\moremapargsfalse\cmd\esac\tokcase\enddiagram:\moremapargsfalse\cmd\esac
\tokcase\across:\moremapargsfalse\cmd\esac\tokcase\relax:\moremapargsfalse
\cmd\esac\tokcase\kern:\moremapargsfalse\cmd\esac\tokcase\mkern:%
\moremapargsfalse\cmd\esac\default:\ifincommdiag\then\let\next\getlabeldocmd
\else\moremapargsfalse\let\next\cmd\fi\next\esac\esacs}
\newdimen\HorizontalLineHeight\HorizontalLineHeight0.628ex \newdimen
\HorizontalLineDepth\HorizontalLineDepth-0.534ex \def\horizhtdp{height%
\HorizontalLineHeight depth\HorizontalLineDepth} \newdimen
\HorizontalMapLength\HorizontalMapLength5em \def\makeharrowpart#1{\hbox{%
\mathsurround\zpt$\mkern-1.5mu{#1}\mkern-1.5mu$}} \def\justhorizline{-}
\def\HorizontalMap#1#2#3#4#5{\setbox1=\makeharrowpart{#1}\def\arrowfillera{#2%
}\def\arrowfillerb{#4}\setbox5=\makeharrowpart{#5}\ifx\arrowfillera
\justhorizline\then\def\arra{\hrule\horizhtdp}\def\kea{\kern-0.01em}\let
\arrstruthtdp\horizhtdp\else\def\kea{\kern-0.15em}\setbox2=\hbox{\kea${%
\arrowfillera}$\kea}\def\arra{\copy2}\def\arrstruthtdp{height\ht2 depth\dp2 }%
\fi\ifx\arrowfillerb\justhorizline\then\def\arrb{\hrule\horizhtdp}\def\keb{%
kern-0.01em}\ifx\arrowfillera\empty\then\let\arrstruthtdp\horizhtdp\fi\else
\def\keb{\kern-0.15em}\setbox4=\hbox{\keb${\arrowfillerb}$\keb}\def\arrb{%
\copy4}\ifx\arrowfilera\empty\then\def\arrstruthtdp{height\ht4 depth\dp4 }\fi
\fi\setbox3=\makeharrowpart{{#3}\vrule width\zpt\arrstruthtdp} \dimen3=\wd3
\let\thecmd\execHorizontalMap\gettwoargs}
\def\labelstyle{\ifincommdiag\textstyle\else\scriptstyle\fi}
\def\execHorizontalMap{\setbox6=\hbox{$\quad\labelstyle\upperlabel\quad$}%
\setbox7=\hbox{$\quad\labelstyle\lowerlabel\quad$}\dimen0=\wd6 \ifdim\dimen0<%
\wd7\then\dimen0=\wd7\fi\ifdim\dimen0<\HorizontalMapLength\then\dimen0=%
\HorizontalMapLength\fi\skip2=.5\dimen0 \ifincommdiag plus 1fill\fi minus\zpt
\advance\skip2-.5\wd3 \skip4=\skip2 \advance\skip2-\wd1 \advance\skip4-\wd5
\kern0.4em \box1 \xleaders\arra\hskip\skip2 \vbox\ifincommdiag\tozpt\fi{%
\offinterlineskip\ifincommdiag\vss\fi\hbox to\dimen3{\hss\unhbox6\hss}\kern0.%
7ex \vtop\ifincommdiag\tozpt\fi{\box3 \kern0.7ex \hbox to\dimen3{\hss\unhbox7%
\hss}\ifincommdiag\vss\fi}}\ifincommdiag\kern-.5\dimen3\penalty-9999\null
\kern.5\dimen3\fi\xleaders\arrb\hskip\skip4 \box5 \kern0.4em }
\newdimen\VerticalMapHeight\VerticalMapHeight5ex \newdimen\VerticalMapDepth
\VerticalMapDepth4ex \newdimen\VerticalMapExtraHeight\VerticalMapExtraHeight
\zpt\newdimen\VerticalMapExtraDepth\VerticalMapExtraDepth\zpt\newdimen
\VerticalLineWidth\VerticalLineWidth0.04em \def\justverticalline{|}\def
\makevarrowpart#1{\hbox\tozpt{\hss$\kern\VerticalLineWidth{#1}$\hss}}
\def\VerticalMap#1#2#3#4#5{\setbox1=\makevarrowpart{#1}\def\arrowfillera{#2}%
\setbox3=\makevarrowpart{#3}\def\arrowfillerb{#4}\setbox5=\makevarrowpart{#5}%
\skip2=\VerticalMapHeight plus 1 fill \advance\skip2-\ht3 \advance\skip2%
\VerticalMapExtraHeight\advance\skip2-\ht1 \advance\skip2-\dp1 \skip4=%
\VerticalMapDepth plus 1 fill \advance\skip4-\dp3 \advance\skip4%
\VerticalMapExtraDepth\advance\skip4-\ht5 \advance\skip4-\dp5 \ifx
\arrowfillera\justverticalline\then\def\arra{\vrule width\VerticalLineWidth}%
\def\kea{\kern-0.05ex}\else\def\kea{\kern-0.35ex}\setbox2=\vbox{\kea
\makevarrowpart\arrowfillera\kea}\def\arra{\copy2}\fi\ifx\arrowfillerb
\justverticalline\then\def\arrb{\vrule width\VerticalLineWidth}\def\keb{\kern
-0.05ex}\else\def\keb{\kern-0.35ex}\setbox4=\vbox{\keb\makevarrowpart
\arrowfillerb\keb}\def\arrb{\copy4}\fi\let\thecmd\execVerticalMap\gettwoargs}
\def\execVerticalMap{\llap{$\labelstyle\upperlabel\>$}\vbox{\offinterlineskip
\kern-\VerticalMapExtraHeight\kern0.9ex \box1 \kea\xleaders\arra\vskip\skip2%
\kea\vtop{\box3 \keb\xleaders\arrb\vskip\skip4\keb\box5 \kern0.9ex \kern-%
\VerticalMapExtraDepth}}\rlap{$\labelstyle\>\lowerlabel$}}
\newif\ifPositiveGradient\PositiveGradienttrue\newif\ifClimbing\Climbingtrue
\newcount\DiagonalChoice\DiagonalChoice1 \newcount\lineno\newcount\rowno
\newcount\charno\newcount\DiagonalLineSegments\DiagonalLineSegments2
\def\laf{\afterassignment\xlaf\charno='} \def\xlaf{\hbox{\tenln\char\charno}}
\def\lah{\afterassignment\xlah\charno='} \def\xlah{\hbox{\rlap{\unhcopy2}%
\tenln\char\charno}} \def\makedarrowpart#1{\hbox{\mathsurround\zpt${#1}$}}
\def\DiagonalMap#1#2#3#4#5{\setbox2=\makedarrowpart{#2}\setbox1=%
\makedarrowpart{#1}\setbox5=\makedarrowpart{#5}\ifPositiveGradient\then\let
\mv\raise\else\let\mv\lower\fi\setbox0=\hbox{$\vcenter{\kern.9ex \hbox{\kern.%
4em \lineno=0 \mv-\ht1\box1 \loop\ifnum\lineno<\DiagonalLineSegments\mv
\lineno\ht2\copy2 \advance\lineno1 \repeat\mv\lineno\ht2\box5 \kern.4em }%
\kern.9ex }$} \dimen0=.5\wd0 \let\thecmd\execDiagonalLine\gettwoargs}
\def\execDiagonalLine{\kern\dimen0 \mv.5\wd2\hbox\tozpt{\hss$\labelstyle
\upperlabel$\kern.5\ht2}\kern-\dimen0 \box0 \kern-\dimen0 \mv-.5\wd2\hbox
\tozpt{\kern.5\ht2$\labelstyle\lowerlabel$\hss}\kern\dimen0 }
\def\rhvee{\mkern-10mu\gt} \def\lhvee{\lt\mkern-10mu} \def\dhvee{\vbox\tozpt{%
\vss\hbox{$\vee$}}} \def\uhvee{\vbox\tozpt{\hbox{$\wedge$}\vss}} \def\rhcvee{%
\mkern-10mu\succ} \def\lhcvee{\prec\mkern-10mu} \def\dhcvee{\vbox\tozpt{\vss
\hbox{$\curlyvee$}}} \def\uhcvee{\vbox\tozpt{\hbox{$\curlywedge$}\vss}} \def
\rhvvee{\mkern-10mu\gg} \def\lhvvee{\ll\mkern-10mu} \def\dhvvee{\vbox\tozpt{%
\vss\hbox{$\vee$}\kern-.6ex\hbox{$\vee$}}} \def\uhvvee{\vbox\tozpt{\hbox{$%
\wedge$}\kern-.6ex\hbox{$\wedge$}\vss}} \def\twoheaddownarrow{\rlap{$%
\downarrow$}\raise-.5ex\hbox{$\downarrow$}} \def\twoheaduparrow{\rlap{$%
\uparrow$}\raise.5ex\hbox{$\uparrow$}} \def\triangleup{{\scriptscriptstyle
\bigtriangleup}} \def\littletriangledown{{\scriptscriptstyle\triangledown}}
\def\htdot{\mkern3.15mu\cdot\mkern3.15mu} \def\vtdot{\vbox to 1.46ex{\vss
\hbox{$\cdot$}}} \def\utbar{\vrule height 0.093ex depth\zpt width 0.4em} \let
\dtbar\utbar\def\rtbar{\mkern1.5mu\vrule height 1.1ex depth.06ex width .04em%
\mkern1.5mu} \let\ltbar\rtbar\def\rthooka{\raise.603ex\hbox{$%
\scriptscriptstyle\subset$}} \def\lthooka{\raise.603ex\hbox{$%
\scriptscriptstyle\supset$}} \def\rthookb{\raise-.022ex\hbox{$%
\scriptscriptstyle\subset$}} \def\lthookb{\raise-.022ex\hbox{$%
\scriptscriptstyle\supset$}} \def\dthookb{\hbox{$\scriptscriptstyle\cap$}%
\mkern5.5mu} \def\uthookb{\hbox{$\scriptscriptstyle\cup$}\mkern4.5mu} \def
\dthooka{\mkern6mu\hbox{$\scriptscriptstyle\cap$}} \def\uthooka{\mkern6mu%
\hbox{$\scriptscriptstyle\cup$}} \def\hfdot{\mkern3.15mu\cdot\mkern3.15mu}
\def\vfdot{\vbox to 1.46ex{\vss\hbox{$\cdot$}}} \def\vfdashstrut{\vrule width%
\zpt height1.3ex depth0.7ex} \def\vfthedash{\vrule width\VerticalLineWidth
height0.6ex depth \zpt} \def\hfthedash{\vrule\horizhtdp width 0.26em} \def
\hfdash{\mkern5.5mu\hfthedash\mkern5.5mu} \def\vfdash{\vfdashstrut\vfthedash}
\def\dmcornervert{\vrule width\VerticalLineWidth height\HorizontalLineHeight}
\def\rdmcorner{\kern.4em\dmcornervert\vrule width .4em \horizhtdp} \def
\ldmcorner{\vrule width .4em \horizhtdp\dmcornervert\kern.4em} \def\rumcorner
{\kern.4em\vrule width .4em \horizhtdp} \def\lumcorner{\vrule width .4em
\horizhtdp\kern.4em} \def\urmcorner{\mkern-4.2mu} \let\drmcorner\urmcorner
\let\dlmcorner\urmcorner\let\ulmcorner\urmcorner
\def\NorthWest{\PositiveGradientfalse\Climbingtrue\DiagonalChoice0 } \def
\NorthEast{\PositiveGradienttrue\Climbingtrue\DiagonalChoice1 } \def
\SouthWest{\PositiveGradienttrue\Climbingfalse\DiagonalChoice3 } \def
\SouthEast{\PositiveGradientfalse\Climbingfalse\DiagonalChoice2 } \def\nwhTO{%
\nwarrow\mkern-1mu} \def\nehTO{\mkern-.1mu\nearrow} \def\sehTO{\searrow\mkern
-.02mu} \def\swhTO{\mkern-.8mu\swarrow} \def\NW{\NorthWest\DiagonalMap{\lah
111}{\laf100}{\laf100}{\laf100}{\laf100}} \def\NE{\NorthEast\DiagonalMap{\laf
0}{\laf0}{\laf0}{\laf0}{\lah22}} \def\SW{\SouthWest\DiagonalMap{\lah11}{\laf0%
}{\laf0}{\laf0}{\laf0}} \def\SE{\SouthEast\DiagonalMap{\laf100}{\laf100}{\laf
100}{\laf100}{\lah122}}
\def\rTo{\HorizontalMap\empty-\empty-\rhvee} \def\lTo{\HorizontalMap\lhvee-%
\empty-\empty} \def\dTo{\VerticalMap\empty|\empty|\dhvee} \def\uTo{%
\VerticalMap\uhvee|\empty|\empty} \let\uFrom\uTo\let\lFrom\lTo
\def\rDotsto{\HorizontalMap\empty\hfdot\hfdot\hfdot\rhvee} \def\lDotsto{%
\HorizontalMap\lhvee\hfdot\hfdot\hfdot\empty} \def\dDotsto{\VerticalMap\empty
\vfdot\vfdot\vfdot\dhvee} \def\uDotsto{\VerticalMap\uhvee\vfdot\vfdot\vfdot
\empty} \let\uDotsfrom\uDotsto\let\lDotsfrom\lDotsto
\def\rDashto{\HorizontalMap\empty\hfdash\hfdash\hfdash\rhvee} \def\lDashto{%
\HorizontalMap\lhvee\hfdash\hfdash\hfdash\empty} \def\dDashto{\VerticalMap
\empty\vfdash\vfdash\vfdash\dhvee} \def\uDashto{\VerticalMap\uhvee\vfdash
\vfdash\vfdash\empty} \let\uDashfrom\uDashto\let\lDashfrom\lDashto
\def\rImplies{\HorizontalMap==\empty=\Rightarrow} \def\lImplies{%
\HorizontalMap\Leftarrow=\empty==} \def\dImplies{\VerticalMap\|\|\empty\|%
\Downarrow} \def\uImplies{\VerticalMap\Uparrow\|\empty\|\|} \let\uImpliedby
\uImplies\let\lImpliedby\lImplies
\def\rMapsto{\HorizontalMap\rtbar-\empty-\rhvee} \def\lMapsto{\HorizontalMap
\lhvee-\empty-\ltbar} \def\dMapsto{\VerticalMap\dtbar|\empty|\dhvee} \def
\uMapsto{\VerticalMap\uhvee|\empty|\utbar} \let\uMapsfrom\uMapsto\let
\lMapsfrom\lMapsto
\def\rIntoA{\HorizontalMap\rthooka-\empty-\rhvee} \def\rIntoB{\HorizontalMap
\rthookb-\empty-\rhvee} \def\lIntoA{\HorizontalMap\lhvee-\empty-\lthooka} \def
\lIntoB{\HorizontalMap\lhvee-\empty-\lthookb} \def\dIntoA{\VerticalMap
\dthooka|\empty|\dhvee} \def\dIntoB{\VerticalMap\dthookb|\empty|\dhvee} \def
\uIntoA{\VerticalMap\uhvee|\empty|\uthooka} \def\uIntoB{\VerticalMap\uhvee|%
\empty|\uthookb} \let\uInfromA\uIntoA\let\uInfromB\uIntoB\let\lInfromA\lIntoA
\let\lInfromB\lIntoB\let\rInto\rIntoA\let\lInto\lIntoA\let\dInto\dIntoB\let
\uInto\uIntoA
\def\rEmbed{\HorizontalMap\gt-\empty-\rhvee} \def\lEmbed{\HorizontalMap\lhvee
-\empty-\lt} \def\dEmbed{\VerticalMap\vee|\empty|\dhvee} \def\uEmbed{%
\VerticalMap\uhvee|\empty|\wedge}
\def\rProject{\HorizontalMap\empty-\empty-\triangleright} \def\lProject{%
\HorizontalMap\triangleleft-\empty-\empty} \def\uProject{\VerticalMap
\triangleup|\empty|\empty} \def\dProject{\VerticalMap\empty|\empty|%
\littletriangledown}
\def\rOnto{\HorizontalMap\empty-\empty-\twoheadrightarrow} \def\lOnto{%
\HorizontalMap\twoheadleftarrow-\empty-\empty} \def\dOnto{\VerticalMap\empty|%
\empty|\twoheaddownarrow} \def\uOnto{\VerticalMap\twoheaduparrow|\empty|%
\empty} \let\lOnfrom\lOnto\let\uOnfrom\uOnto
\def\hEq{\HorizontalMap==\empty==} \def\vEq{\VerticalMap\|\|\empty\|\|} \let
\rEq\hEq\let\lEq\hEq\let\uEq\vEq\let\dEq\vEq
\def\hLine{\HorizontalMap\empty-\empty-\empty} \def\vLine{\VerticalMap\empty|%
\empty|\empty} \let\rLine\hLine\let\lLine\hLine\let\uLine\vLine\let\dLine
\vLine
\def\rPto{\HorizontalMap\empty-\empty-\rightharpoonup} \def\lPto{%
\HorizontalMap\leftharpoonup-\empty-\empty} \def\uPto{\VerticalMap
\upharpoonright|\empty|\empty} \def\dPto{\VerticalMap\empty|\empty|%
\downharpoonright} \let\lPfrom\lPto\let\uPfrom\uPto
\def\drBent{\VerticalMap\empty\empty\rdmcorner|\empty} \def\dlBent{%
\VerticalMap\empty\empty\ldmcorner|\empty} \def\urBent{\VerticalMap\empty|%
\rumcorner\empty\empty} \def\ulBent{\VerticalMap\empty|\lumcorner\empty\empty
} \def\rdBent{\HorizontalMap\empty\empty\drmcorner-\empty} \def\ldBent{%
\HorizontalMap\empty-\dlmcorner\empty\empty} \def\ruBent{\HorizontalMap\empty
\empty\urmcorner-\empty} \def\luBent{\HorizontalMap\empty-\ulmcorner\empty
\empty}
\def\drBentto{\VerticalMap\empty\empty\rdmcorner|\dhvee} \def\dlBentto{%
\VerticalMap\empty\empty\ldmcorner|\dhvee} \def\urBentto{\VerticalMap\uhvee|%
\rumcorner\empty\empty} \def\ulBentto{\VerticalMap\uhvee|\lumcorner\empty
\empty} \def\rdBentto{\HorizontalMap\drmcorner-\empty-\rhvee} \def\ldBentto{%
\HorizontalMap\lhvee-\empty-\dlmcorner\empty\empty} \def\ruBentto{%
\HorizontalMap\urmcorner-\empty-\rhvee} \def\luBentto{\HorizontalMap\lhvee-%
\empty-\ulmcorner}
\def\pile#1{{\incommdiagtrue\null\baselineskip\zpt\lineskip\zpt\lineskiplimit
\zpt\mathsurround\zpt\tabskip\zpt\let\\\cr\vcenter{\halign{ \hfil$##$\hfil\cr
#1 \crcr}}}}
\def\SEpbk{\rlap{\smash{\kern0.1em \vrule depth 2.67ex height -2.55ex width 0%
.9em \vrule height -0.46ex depth 2.67ex width .05em }}} \def\SWpbk{\llap{%
\smash{\vrule height -0.46ex depth 2.67ex width .05em \vrule depth 2.67ex
height -2.55ex width .9em \kern0.1em }}} \def\NEpbk{\rlap{\smash{\kern0.1em
\vrule depth -3.48ex height 3.67ex width 0.95em \vrule height 3.67ex depth -1%
.39ex width .05em }}} \def\NWpbk{\llap{\smash{\vrule height 3.6ex depth -1.39%
ex width .05em \vrule depth -3.48ex height 3.67ex width .95em \kern0.1em }}}
\def\hboxsm#1{\setbox0=\hbox{#1}\ht0\zpt\dp0\zpt\box0}
\textwidth=6.5in
\oddsidemargin=0in
\evensidemargin=0in
\setlength{\baselineskip}{16pt}
\parskip=14pt
\parindent=0pt
\hyphenation{hom-ob-ject hom-ob-jects}
% Springer-Verlag:
%\magnification=\magstep1
%\vsize=23.5true cm
%\hsize=16true cm
%\nopagenumbers
%\topskip=1truecm
%\headline={\tenrm\hfil\folio\hfil}
%\raggedbottom
%\abovedisplayskip=3mm
%\belowdisplayskip=3mm
%\abovedisplayshortskip=3mm
%\belowdisplayshortskip=3mm
%\normalbaselineskip=12pt
%\normalbaselines
\begin{document}
\title{Temporal Structures}
\author{Ross Casley$\dagger$       \and Roger F. Crew$\dagger$    \and
    Jos\'e Meseguer$\ddagger$  \and Vaughan Pratt$\dagger$}
%\date{}
\maketitle
{\parindent=0pt
$\dagger$ Dept. of Computer Science, Stanford University, Stanford, CA 94305 \\
$\dagger$ Supported by the National Science Foundation under grant
CCR-8814921 \\
$\ddagger$ SRI International, Menlo Park, CA 94025 and \\
Center for the Study of Language and Information, Stanford University, Stanford, CA 94305 \\
$\ddagger$ 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.
This paper is a revision of a CTCS-89 paper \cite{CCMP}.
\begin{abstract}
We combine the principles of the Floyd-Warshall-Kleene algorithm,
enriched categories, and Birkhoff arithmetic, to yield a useful class
of algebras of transitive vertex-labeled spaces.  The motivating
application is a uniform theory of abstract or parametrized time in
which to any given notion of time there corresponds an algebra of
concurrent behaviors and their operations, always the same operations
but interpreted automatically and appropriately for that notion of
time.  An interesting side application is a language for succinctly
naming a wide range of datatypes.
\end{abstract}
\section{Introduction}
Posets, metric spaces, ``closed'' automata, and categories have in
common the notion of a {\it space} of points with distances between
points.  These distances are respectively truth values, reals,
languages, and sets.
Distances have two facets, logical and metrical.  The logical facet is
expressed respectively via implications $p\to q$ between truth values,
comparisons $x\ge y$ between reals, inclusions $L\subseteq M$ between
languages, and functions $f:X\to Y$ between sets.  The metrical facet
is expressed via a suitable monotone associative operation,
respectively conjunction $p\land q$, addition $x+y$, concatenation
$LM$, and cartesian product $X\times Y$.  These two facets confer on
any such set of distances the attributes of an ordered monoid
$(D,\le,\otimes,I)$, having simultaneously the attributes of a poset
$(D,\le)$ and a monoid $(D,\otimes,I)$, with $\otimes$ monotone in each
argument with respect to $\le$.  For such cases as our last example,
sets as distances, the poset structure is generalized to category
structure, so that rather than an ordered monoid we have a monoidal
category, for which ``monotone operation'' must be correspondingly
generalized to ``functor.''
The transitivity law $u\le v\land v\le w\to u\le w$ for a poset, the
triangle inequality $d(u,v)+d(v,w)\ge d(u,w)$ for a metric space, the
requirement $L_{uv}L_{vw}\subseteq L_{uw}$ for an automaton to be
considered closed, and the family of composition operations
$m_{uvw}:\Hom(v,w)\times\Hom(u,v)\to\Hom(u,w)$ for a category,
respectively combine these two facets via essentially the same basic
triangle inequality.
Each of these classes of generalized metric spaces has a natural notion
of map, respectively monotone functions, contractions, morphisms of
automata, and functors, in each case making that class a category with
those maps as its morphisms.
In computer science some of the common elements of these notions have
been unified by organizing distances as an {\it idempotent semiring},
an ordered monoid whose underlying partial order contains all sups and
whose monoidal operation preserves (i.e. distributes over) those sups.
The basis for this unification is the O$(n^3)$ time procedure of Roy
\cite{Roy59} and independently that of S. Warshall \cite{War62} for
computing the transitive closure of a binary relation on $n$ elements
presented as an $n\times n$ Boolean (0- and 1-valued) matrix.  The
unification was hinted at by R.W. Floyd \cite{Flo62} who observed that
Warshall's procedure would compute shortest paths instead of transitive
closure if Booleans were replaced by nonnegative reals, disjunction by
{\bf min}, and conjunction by addition.  The uniform expression of this
common algorithm in terms of semirings was first described by Robert
and Ferland \cite{RF}.  Synonyms for this notion of semiring include
regular algebra \cite{Con}, Kleene algebra \cite{Koz80b,Koz81a}, and
quantale \cite{Vic89}.
Other instantiations of this abstract algorithm were subsequently
found.  Replacing Booleans in Warshall's algorithm by languages,
conjunction by concatenation, and disjunction by union, yields Kleene's
algorithm for ``closing'' an automaton $M$ having $n$ states, viewed as
an $n\times n$ matrix of (finitely presented) regular languages, from
which one may then easily read off a regular expression denoting the
language $L(M)$ accepted by $M$ \cite{AHU}.  Even Gaussian elimination
was found to be so describable in the (nonidempotent) ring of reals
made a field via $1/(1-x)=1+x+x^2+\ldots$.
Independently and working in a categorical setting, Eilenberg and Kelly
\cite{EK66a} developed a more categorically sophisticated version of
the same generalization of metric space under the name enriched
category or $V$-category.  In place of a semiring they used a monoidal
category $V$.  Distances became homobjects, a generalization of
homset.  The logical facet was expressed by the category structure of
$V$: the morphisms of $V$ permitted ``comparisons'' of homobjects.  The
metrical facet was expressed by the monoidal structure of $V$:
``consecutive'' homobjects were combined by the binary operation of the
monoid.
Although Eilenberg and Kelly described enriched categories in their
full generality, their motivating applications were confined to $V$'s
forming classes rather than sets, an emphasis continued in Kelly's
subsequent book on enriched categories \cite[p22]{Kel}.  Yet in 1974
F.W. Lawvere \cite{Law} in an excellent advertisement for the utility
of enriched categories emphasized $V$'s that were semirings, hence sets
rather than classes, and with category structure merely that of a
poset.  This brought enriched categories into close proximity to the
parallel computer science development.  Nevertheless this connection
between enriched categories and shortest-path algorithms remained
undetected for another 15 years \cite{Pr89a}.
The present paper starts from the notion of a partial order as a
behavior of a ``truly concurrent'' process, and uniformly extends it to
other classes of spaces via the above correspondences.  This extension
was first proposed by Pratt \cite{Pr84} with just the semiring view in
mind; here we extend that proposal to take advantage of the enriched
category perspective as well as additional basic operations whose
utility were not at all apparent at the time, and develop the resulting
framework in detail.
This approach achieves a considerable unification of ideas relevant to
concurrency, as well as making connections with other areas to which
the semiring and enrichment insights apply.  In the concurrency
application we characterize time abstractly as an ordered monoid, and
more generally albeit speculatively as a monoidal category, whose
objects are temporal quantities.  From this model of time we construct
via enrichment a category of behaviors.  A behavior, or computation, is
a space whose points represent events and whose distances are to be
interpreted as delays between events.
Various natural operations on such spaces correspond to useful
constructs for concurrent programming languages.  These operations are
functors, most of which prove to be definable via familiar categorical
constructions.  We treat only concurrency and not nondeterminism
(choice), in that we work only with single behaviors rather than sets
of them representing alternative behaviors.
An appealing feature of this approach is its abstractness.  A single
framework is developed independently of choice of ordered monoid or
monoidal category.  Instantiating the whole framework for a particular
monoidal structure yields the corresponding model of concurrency
incorporating that structure as its notion of time, with all the
operations of the framework likewise instantiated.  The development
lends itself to the application of categorical methods.
A practical application of this perspective is to improving the
organization of current theories of real time in concurrency modeling.
A case in point is the recent work of H. Lewis \cite{Lew90}.  Lewis
works with state diagrams each of whose transitions is labeled with a
set of $O(n^2)$ intervals, with larger sets at later transitions, per
his Figure 6.  In our framework the essence of this information would
be captured with one real labeling each edge of the {\it transitive
closure} of the diagram, with the delay from $u$ to $v$ being a lower
bound whose matching upper bound (to form an interval) is the negation
of the delay from $v$ to $u$.
The ordered monoids that have previously been found useful in this
setting are all useful here for one view or another of time.  In
addition we identify a class of finite generalizations of the ordered
monoid $\two$ of truth values which we call the {\it idempotent closed
ordinals} or ico's.  There are $2^{n-2}$ such closed or residuated
ordered monoids with $n$ elements, exactly one of which is cartesian
closed, proved via a pretty representation theorem.  We describe
natural applications for the two three-element ico's $\three$ and
$\three'$, and show where each has in effect been used in the
concurrency literature.
The operations on spaces ordinarily considered in the context of
shortest-path algorithms and their cousins can be collectively
understood as Kleene's {\it regular} operations $L+M$, $LM$, and $L^*$,
defined by Kleene only for languages but all equally meaningful for the
other domains, even the one for Gaussian elimination (with
$x^*={1/(1-x)}$).  In terms of matrices these are the operations of
pointwise sum of two $m\times n$ matrices $M,N$ to yield an $m\times n$
matrix $M+N$, product of an $m\times k$ matrix $M$ by a $k\times n$
matrix $N$ to yield an $m\times n$ matrix $MN$, and reflexive and/or
transitive closure of an $n\times n$ matrix $M$ to yield an $n\times n$
matrix $M^*$.  A reasonably close connection between such matrices and
spaces can be made by regarding rectangular $m\times n$ matrices as
complete bipartite graphs from $m$ vertices to $n$ vertices, and in the
other direction ordinary (nonbipartite) directed graphs as square
matrices, with distances entering as edge labels.
This paper adds to these regular operations a number of other
operations such as disjoint union or juxtaposition, tensor product,
concatenation, exponentiation, and useful variations on these obtained
by generalizing products to pullbacks and coproducts to pushouts.
These operations are generally better matched to the concurrency
modeling application than the regular operations, both extrinsically
and intrinsically.  Extrinsically juxtaposition captures concurrence,
tensor product captures orthocurrence, etc.  And intrinsically these
operations impose few if any constraints on relationships between
vertex sets of their arguments, unlike the regular operations.
An early and striking example of these ``nonregular'' operations is
provided by Birkhoff's arithmetic \cite{Birk37,Birk42} of posets up to
isomorphism under addition, multiplication, and exponentiation each of
two kinds, cardinal and ordinal.  Birkhoff's application was to the
arithmetic of cardinals and ordinals, which he proposed to unify by
regarding both as posets, with cardinals as discrete posets and
ordinals as linear.  In place of two sorts of data he then had two
sorts of operations.
In relating Birkhoff arithmetic to concurrent programming we make the
connections cardinal-concurrent and ordinal-sequential.  Discrete
posets model the purely concurrent behaviors (no sequentiality) while
linearly ordered posets model the purely sequential.  The cardinal
operations map discrete sets to discrete, i.e. they preserve
concurrency, while the ordinal operations map linear sets to linear,
i.e. they preserve sequentiality.
Our framework can then be viewed as a generalization of Birkhoff
arithmetic, in several directions: several additional operations, many
other metrics besides $\two$, provision of labels on points, and
setting Birkhoff arithmetic in a suitable categorical framework.  We
have not however succeeded in finding the right categorical expression
of either ordinal multiplication (i.e.  lexicographic product) or
ordinal exponentiation, which we therefore raise as an interesting
problem.
There is a recursive aspect to the enrichment process that permits a
further generalization of this framework.  We introduce an operation we
call $\D!$, the enriched category term for which is
$V$-Cat,\footnote{We prefer $\D$ to $V$ as connoting distance or
delay.} which takes a symmetric monoidal category $\D$ and returns the
symmetric monoidal category $\D!$ of all small $\D$-categories.  For
example if $\D$ is the monoidal category $\{0,1\}$ of truth values then
$\D!$ is the monoidal category of preordered sets.  This construction
can therefore be iterated to yield $\D!!$, $\D!!!$, etc.
Behaviors as sets of events require not only delay information between
events but information describing each event.  That is, we wish to
label vertices independently of the labeling of edges.  From a set
theoretic perspective there is nothing to this.  However from a
category theoretic perspective, with some operations defined as limits
or colimits the presence of labels is a nontrivial complication;
consider for example coproducts in the category of vertex-labeled
posets.  We define the category of $\E$-labeled $\D$-spaces, each of
whose objects is an object $d$ of $\D$ (we call such a $d$ a
$\D$-space) paired with an object $e$ of $\E$, along with a function
$f:U_d\to V_e$ from the underlying set of $d$ (the points of the
space $d$) to the underlying set of $e$ (typically the set $e$ itself,
construed as an alphabet of labels) serving as a vertex labeling
function.  The appropriate category of such $\E$-labeled $\D$-spaces is
the comma category $(U,V)$.
To make the comma-category construct iterable analogously to the
iterability of enrichment we need to extend its arguments so as to
carry both the structure we need for enrichment (i.e. a symmetric
monoidal category) and that for the comma construction (hence we need a
forgetful functor).  We denote this extension of the comma construction
to these extended arguments by $\D\comma\E$.
With these two operations, along with certain constants, we now have a
language with such expressions as $\one!$, $\three!!\comma\one!$,
$\R!$, etc.  The succinctness of each expression belies its content.
For example the expression $\one!!!$ does not merely hint at the
category of all 2-categories but specifies it in full detail, complete
with all internal features such as the interchange law, 2-functors
between 2-categories, etc.  Moreover it supplies some external
features: it is a closed category, and is equipped with a forgetful
functor to $\Set$ taking each 2-category to the set of its objects.
However it is not a 3-category as it should be, or even a 2-category,
and has no other useful forgetful functors such as to $\Cat$.  These
restrictions reflect our particular recursive construction of
categories, which yields only semiconcrete symmetric monoidal
categories.
\section{Operations}
The motivating application of our framework is to define an algebra of
concurrent behaviors (runs, computations), independently of any
particular choice of notion of time.  In this section we describe the
desired operations of such an algebra, and illustrate them for {\it
dual} metric spaces, spaces in which distance $d$ from $u$ to $v$
indicates that $v$ must follow $u$ by {\it at least} $d$ units (metric
spaces would replace ``at least'' by ``at most'').
In formal language theory, concatenation is defined on individual
strings as well as on languages (sets of strings) whereas union and
Kleene star are defined only on languages.  In the framework of the
present paper strings are generalized to {\it behaviors}, defined as
labeled spaces, with languages correspondingly generalized to {\it
processes} as sets of behaviors.  We shall define only operations on
individual behaviors, hence including concatenation but excluding union
and Kleene star.  The operations we treat include all behavior
operations of the process language of \cite{Pr86}, namely concurrence,
orthocurrence, concatenation, and local concatenation, as well as new
operations synchronized concurrence, exponentiation, product, and local
product.  The process operations of that paper are linearization,
union, intersection, complement, star, augment closure, and prefix
closure, whose definition we defer for now pending the appropriate
integration of our framework with the current understanding of
nondeterminism.
We now illustrate and define three forms of sum:  concurrence $p|q$,
concatenation $p;^dq$, and local concatenation $p\lc^dq$.  In these
examples all edges are labeled with reals or $\infty$, with absence of
an edge interpreted as distance $-\infty$.  These examples may be taken
as pomset examples by ignoring the edge labels (equivalent to taking
$-\infty$ as 0 and everything else as 1), and as automata examples by
treating distance $d$ as the set of all strings of length at most $d$
(making $-\infty$ the empty language).
In all of these forms of sum, the set of points of the sum is the
disjoint union of those of $p$ and $q$.  That is, the basic step in
forming the sum is to juxtapose $p$ and $q$.
{\it Concurrence} $p|q$ is the least constrained form of sum.  Labels
on points, and distances within $p$ and $q$, remain unchanged, while
the distance from an event of $p$ to one of $q$ is $-\infty$, and
likewise from $q$ to $p$.  {\it Disjoint} concurrence differs from
concurrence in that the labels from $p$ and $q$ are ``marked'' to
distinguish them:  the label $a$ becomes $a_0$ or $a_1$ according to
whether the point it labels is from $p$ or $q$.
\setlength{\unitlength}{0.0088in}
\begin{center}
\begin{picture}(671,130)(40,660)
\put( 25,670){Concurrence $(a;^3b)|(c|d)$}
\put( 45,715){$b$} \put( 45,755){$3$} \put( 52,790){$a$}
\put( 55,785){\vector( 0,-1){ 55}}
\put( 82,752){$|$} \put(103,790){$c$} \put(104,715){$d$}
\put(105,730){$\bullet$}
\put(105,780){$\bullet$}
\put(134,753){$=$} \put(160,755){$3$} \put(166,715){$b$} \put(167,790){$a$}
\put(170,780){\vector( 0,-1){ 50}}
\put(192,790){$c$} \put(193,780){$\bullet$} \put(194,715){$d$}
\put(195,730){$\bullet$}
\put(230,670){Concatenation $(a;^3b);^2(c|d)$}
\put(270,750){$3$} \put(282,790){$a$} \put(284,715){$b$}
\put(285,787){\vector( 0,-1){ 55}}
\put(312,754){$;^2$} \put(333,790){$c$} \put(334,715){$d$}
\put(335,730){$\bullet$} \put(335,780){$\bullet$}
\put(360,755){$=$} \put(390,750){$3$} \put(396,715){$b$} \put(397,790){$a$}
\put(400,730){\vector( 1, 0){ 50}} \put(400,730){\vector( 1, 1){ 50}}
\put(400,782){\vector( 0,-1){ 50}} \put(400,785){\vector( 1, 0){ 50}}
\put(400,785){\vector( 1,-1){ 50}}
\put(415,713){$2$} \put(416,736){$2$} \put(415,790){$5$}
\put(438,748){$5$} \put(448,715){$d$} \put(448,790){$c$}
\put(480,670){Local Concatenation $(a;^3B)\underline ;^2(c|D)$}
\put(513,750){$3$} \put(520,715){$B$} \put(522,790){$a$}
\put(525,787){\vector( 0,-1){ 55}}
\put(552,754){$\underline ;^2$} \put(573,790){$c$} \put(575,715){$D$}
\put(575,730){$\bullet$} \put(575,780){$\bullet$}
\put(600,755){$=$} \put(630,750){$3$} \put(635,715){$B$} \put(637,790){$a$}
\put(640,730){\vector( 1, 0){ 45}} \put(640,782){\vector( 0,-1){ 50}}
\put(640,785){\vector( 1, 0){ 45}}
\put(655,715){$2$} \put(655,790){$2$} \put(682,790){$c$} \put(684,715){$D$}
\end{picture}
\centerline{Figure 1.  Additive Operations.}
\end{center}
{\it Concatenation} $p;^dq$ is like $p|q$, differing only with respect
to the distances from $p$ to $q$, which are the least possible
distances no less than $d$.  Disjoint concatenation is to concatenation
as disjoint concurrence is to concurrence.
{\it Local concatenation} $p\lc^dq$ is intermediate in strength
between concurrence and concatenation: it only imposes the additional
distance constraints of concatenation between colocated elements of $p$
and $q$.  For the above example we have identified location with case
of label: lower case at one location, upper at the other.
We now illustrate and define three forms of product, namely
orthocurrence $p\otimes q$, product $p\times q$, and local product
$p\underline\times q$.
\setlength{\unitlength}{0.0088in}
\begin{center}
\setlength{\unitlength}{0.0088in}
\begin{picture}(671,130)(40,520)
\put( 20,530){Orthocurrence $(a;^3b)\otimes(c;^2d)$}
\put( 40,615){$3$} \put( 45,575){$b$} \put( 45,650){$a$}
\put( 50,645){\vector( 0,-1){ 55}}
\put( 65,615){$\otimes$} \put( 85,575){$d$} \put(85,650){$c$} \put(90,615){$2$}
\put( 90,645){\vector( 0,-1){ 55}}
\put(115,615){$=$} \put(130,575){$bc$} \put(130,650){$ac$} \put(148,615){$3$}
\put(145,645){\vector( 0,-1){ 50}} \put(145,645){\vector( 1, 0){ 55}}
\put(150,590){\vector( 1, 0){ 50}} \put(150,645){\vector( 1,-1){ 45}}
\put(170,575){$2$} \put(170,650){$2$} \put(175,620){$5$} \put(205,575){$bd$}
\put(205,645){\vector( 0,-1){ 50}} \put(205,650){$ad$} \put(210,615){$3$}
\put(270,530){Product $(a;^3b)\times(c;^2d)$}
\put(275,615){$3$} \put(280,575){$b$} \put(280,650){$a$}
\put(285,645){\vector( 0,-1){ 55}}
\put(300,615){$\times$} \put(320,575){$d$} \put(320,650){$c$} \put(325,615){$2$}
\put(325,645){\vector( 0,-1){ 55}}
\put(350,615){$=$} \put(365,575){$bc$} \put(365,650){$ac$}
\put(380,645){\vector( 0,-1){ 50}} \put(380,645){\vector( 1, 0){ 55}}
\put(385,590){\vector( 1, 0){ 50}} \put(385,645){\vector( 1,-1){ 45}}
\put(385,615){$3$} \put(405,575){$2$} \put(405,650){$2$} \put(410,620){$2$}
\put(440,575){$bd$} \put(440,650){$ad$} \put(445,615){$3$}
\put(440,645){\vector( 0,-1){ 50}}
\put(500,530){Local Product $(a;^3b)\underline\times c(;^2D,;^1c)$}
\put(505,615){$3$} \put(510,575){$B$} \put(510,650){$a$}
\put(515,645){\vector( 0,-1){ 55}}
\put(530,615){$\underline\times$}
\put(550,575){$D$} \put(555,615){$2$} \put(570,650){$c$}
\put(575,645){\vector( 1,-3){ 18.500}} \put(575,645){\vector(-1,-3){ 18.500}}
\put(590,575){$e$} \put(590,615){$1$} \put(615,615){$=$} \put(635,640){$ac$}
\put(652,640){\vector( 1, 0){ 45}}
\put(665,588){$BD$} \put(670,645){$1$} \put(675,600){$\bullet$}
\put(700,640){$ae$}
\end{picture}
\centerline{Figure 2.  Multiplicative Operations.}
\end{center}
The underlying set of each of these products is the cartesian product
of the underlying sets of their arguments (or a subset thereof in the
case of local product), while their labels are corresponding tuples:
thus if $\mu$ assigns labels to points then the label $\mu(\<u,v>)$ in
a product is $\<\mu_p(u),\mu_q(v)>$.
{\it Orthocurrence} $p|q$ is distinguished from other products by the
distance from $\<u,v>$ to $\<u',v'>$ being $d(u,u')+d(v,v')$.  {\it
Product} $p\times q$ takes this distance to be min$(d(u,u'),d(v,v'))$.
{\it Local product} $p\underline\times q$ is obtained from product by
deleting all points with mixed locations (again indicated by case in
the example), and reducing the distance between tuples at distinct
locations to $-\infty$.
For pomsets orthocurrence and product coincide, both combining the
distances $d(u,u')$ and $d(v,v')$ via conjunction.  For automata they
differ: orthocurrence uses concatenation, product intersection.
{\em Basic Constants}.  The empty schedule, denoted $0$, has no
events.  It is the identity for all sums: concurrence, concatenation,
and local concatenation.  The unit schedule, denoted $I$, has one event
with self-distance 0, and has the singleton alphabet $\{\bullet\}$,
whence that one event is labeled $\bullet$.  Up to isomorphism $I$ is
the identity for orthocurrence.  The top schedule, denoted 1, differs
from $I$ in having self-distance $\infty$.  Up to isomorphism it is the
identity for product.  (The isomorphism is not only between events but
between labels, via the evident isomorphism between $\Sigma$ and
$\Sigma\times\{\bullet\}$.)
We have illustrated these operations and constants for (dual) metric
spaces, and indicated how to derive the corresponding pomset and
automata examples.  However these operations and constants also admit
of obvious interpretations for the metrics themselves.  Concurrence is
respectively max, disjunction, and union for each of the ordered
monoids consisting of truth values, reals, and languages, and is the
same operation as concatenation and local concatenation.  Orthocurrence
is respectively arithmetic sum, conjunction, and concatenation.
Product is respectively min, conjunction, and intersection, and is the
same operation as local product.
%{\em Exponentiation}.  Denoted $B^A$.  The events of this schedule are the
%delay-preserving functions from $A$ to $B$.  For the pomset model we
%consider $f$ to precede $g$ if $fa$ precedes $ga$ for all events $a$ in
%$A$.  For the minimum delay model the delay from $f$ to $g$ is the infimum
%of the delays from $fa$ to $ga$ taken over the events of $A$.  $B^A$ can
%be interpreted as being derived from $B$ by redefining an event to be a
%{\em pattern\/} of events defined by $A$.  For example if $A$ is simply an
%ordered pair of events, then the events of $B^A$ are ordered pairs of
%events in $B$.
\section{Monoidal Categories and their Functors}
Monoidal categories and enrichment are less well established in the
computing literature than such other aspects of category theory as
adjunctions.  We therefore recall here enough details of these notions
to make this paper self-contained at least on a first reading by those
familiar with at least adjunctions.  In addition our treatment will
serve to define the perspective on these topics that we will assume of
the reader, and to coordinate this perspective with the rest of the
paper.  Considerably more information on these topics can be found in
the books of Mac~Lane \cite{Mac} and Kelly \cite{Kel}.
\subsection{Monoidal Categories}
Informally, a monoidal category amounts to a structure that is both a
monoid and a category.  Formally a {\it strict monoidal category}
$\D=(D,\otimes,I)$ is a category $D$ together with a functor
\hbox{$\otimes:D^2\to D$} called the {\it tensor product}
\footnote{Mac~Lane writes $\otimes$ as $\Box$.} and an object $I$ of
$D$ called the {\it unit}, such that the object part and the morphism
part of $D$ each form a monoid under $\otimes$ with respective
identities $I$ and $1_{I}$.  We refer to $(\otimes,I)$ as a {\it
monoidal structure} for the category $\D$.
The structure $(\Set,\times,\{\bullet\})$ with $\times$ cartesian product is
not strict monoidal because in general $X\times(Y\times Z)$ is not
equal to $(X\times Y)\times Z$, they are merely isomorphic.  Moreover
there is a particular isomorphism we would like to be able to {\it
assume} is the one meant when we say that they are isomorphic, namely
$\alpha_{XYZ}:(X\times Y)\times Z\to X\times(Y\times Z)$ defined as
$\alpha(\<\<x,y>,z>)=\<x,\<y,z>>$.  Similarly particular isomorphisms
take the place of the two identity laws for the unit $I=\{\bullet\}$.
We therefore define a more general notion.  A {\it monoidal category}
$\D=(D,\otimes,I,\alpha,\lambda,\rho)$ is as for strict monoidal
categories but specifying natural isomorphisms $\alpha:(c\otimes
d)\otimes e\cong c\otimes(d\otimes e)$, $\lambda:I\otimes d\cong d$ and
$\rho:d\otimes I\cong d$ in place of the usual three-axiom basis for
the theory of monoids.  A {\it symmetric} monoidal category specifies
an additional natural isomorphism $\gamma:d\otimes e\cong e\otimes d$.
We shall confine ourselves to symmetric monoidal categories throughout,
and understand ``monoidal'' to mean symmetric monoidal at all times.
The intent of these isomorphisms is that they be canonical: if an
element of one set corresponds to an element of another set at all,
this is a universal or global correspondence.  In particular there may
be at most one such isomorphism between two sets, and in the case of a
set in isomorphism with itself that isomorphism must be the identity.
This intuition is formalized via certain {\it coherence conditions},
whose effect is that if there are multiple ways to infer by
transitivity two isomorphisms between two sets, those isomorphisms must
be the same.  A strict monoidal category amounts to a monoidal category
whose such isomorphisms are all identities.
A monoidal category $C$ is {\it left closed} ({\it right closed}) when
${-}\otimes b$ ($a\otimes{-}$) has a right adjoint.  When both exist it
is called biclosed.  When $C$ is symmetric, either left closed or right
closed implies biclosed, and in this case we simply call it closed.
The right adjoint to ${-}\otimes b$ is notated ${-}^b:C\to C$ and
defined by an isomorphism $\Hom(a\otimes b,c)$ and $\Hom(a,c^b)$
natural in $a$ and $c$.  Setting $a$ to $I$ yields
via $\lambda$ the natural isomorphism $b\to c\cong I\to c^b$, that is,
$\Hom$ is naturally isomorphic to $\Hom':C\op\times
C\stackrel{{-}^{-}}{\to}C\stackrel{\Hom(I,-)}{\longrightarrow}\Set$.
In this sense ${-}^{-}$ {\it represents} $\Hom(b,c)$, making it the
{\it internal hom}(functor).  As $\R\op_\ge$ in example (3) below
shows, $I$ need not determine $\otimes$ and hence the internal hom even
up to isomorphism, showing that it is possible for the internal hom to
contain information not present in the external hom even together with
Since left adjoints preserve colimits, we have in any closed category
$(A+B)\otimes C\cong A\otimes C+B\otimes C$ and $C\otimes(A+B)\cong
C\otimes A+C\otimes B$ when the coproduct $A+B$ exists and $A\otimes
0\cong 0\cong 0\otimes A$ when the initial object 0 exists.
A category $D$ with all finite products determines the {\it cartesian}
symmetric monoidal category $(D,\times,1)$.  When the latter is closed
(common but not universal, e.g. {\bf Top}), $D$ is said to be {\it
cartesian closed}.
\subsection{Examples of Monoidal Categories}
We illustrate the above definitions with the monoidal categories we
will be using in KL.  Most of these will be closed and bicomplete, the
kind we are most interested in.
(1) Each successor ordinal $\bf n{+}1$, as an $n{+}1$-object category
with $n{+}2 \choose 2$ morphisms $i\to j$ where $0\le i\le j\le n$,
forms the cartesian closed category algebraic topologists call $[n]$.
That is, the symmetric monoidal structure is $(n{+}1,\land,n)$, and the
right adjoint of $\land$, the internal hom ${-}^{-}$, must be the
largest $a$ such that $a\land b\le c$, namely $n$ when $b\le c$ and $c$
otherwise.  The product of two such cartesian closed ordinals or cco's
is the cco $[m]\times[n]=[m+n]$.
But the category $\bf n{+}1$ = $[n]$ admits other monoidal structures,
all strict since $\bf n{+}1$ has no nonidentity isomorphisms, and all
bicomplete.  Of these, $2^n$ are idempotent ($x\otimes x=x$), since
each is representable as a permutation of $\{0,1,\ldots,n\}$ whose
domain partitions into two blocks on one of which the permutation is
monotone and on the other antimonotone.
Such a permutation can be written down by writing $0,1,2,\ldots,I$ (the
monotone block) from left to right and then reversing direction so as
to write $I+1,I+2,\ldots,n$ (the antimonotone block) from right to left
interleaved arbitrarily with the monotone block, leaving $I$ at the far
right.  For $n=3$ this can be done in eight ways, namely $0123$,
$01_32$, $0_312$, $0_{32}1$, $_3012$, $_30_21$, $_{32}01$, $_{321}0$,
here distinguishing the two blocks by writing the second as
subscripts.  Then $x\otimes y$ is taken to be the earlier of $x$ and
$y$ in the permutation.  Since $I$ is always at the right end of the
permutation it will always be the identity of $x\otimes y$.  For
$\otimes$ to be a functor it suffices that it be monotone, which the
reader may verify.
For $n>0$ exactly half of these are closed.  For to be closed we
require that for any $b$ and $c$ there be a largest $a$ for which
$a\otimes b\le c$.  Setting $c=0$ shows that $0\otimes b$ must be 0 for
all $b$, whence a necessary condition is that the permutation start
with 0.  But this is also sufficient since there then exists a solution
in $a$ to $a\otimes b\le c$, namely $a=0$; finiteness then ensures a
largest solution.  These then are the {\it idempotent closed ordinals}
or ico's.
There is therefore a unique ico {\bf 2}, namely $[1]$.  Here $\otimes$
is $\land$ and $I=1$.  (The nonclosed one has $\otimes=\lor$ and
$I=0$.) This category provides the metric for preordered sets.  This
two-valued cartesian closed logic is that of ordinary precedence, where
for any pair $u,v$ of events there are two cases: either $u$ is
constrained to precede $v$, or not.
There are two closed categories on 3, each appearing implicitly in one
of H. Gaifman's two papers on concurrency.  In each, the elements of 3
represent strengths of temporal precedence constraint between two
events, with 0 representing no constraint.  In the noncartesian case,
call it $\three'$, 1 represents nonstrict temporal precedence and 2
strict, with $1\otimes 2=2$ ($u\le v<w\to u<w$).  This structure is
hidden in the two-relation ``prosset'' model \cite{GP} used in the
proof of Kahn's principle relative to a pomset-based semantics of nets
\cite{Pr86}.
For the cartesian closed $\three$, 1 denotes ``temporal'' or accidental
order and 2 causal \cite{Ga89}.  Here $1\otimes 2=1$, that is, if $u$
accidentally precedes $v$ whereas $v$ causes (necessarily precedes)
$w$, then we may only infer that $u$ accidentally precedes $w$.  Thus
one may identify the logic of causal and accidental precedence with the
cartesian closed category $\three$.
Of the four idempotent closed categories on 4, described by the first
four permutations on the list five paragraphs above, the second and
third have the same $I$, namely 2, but their internal homfunctors
differ at $1^1$.  Composing $\Hom(I,-)$ with either yields the external
homfunctor for 4, whence the category and $I$ together are not
sufficient to determine either $\otimes$ or the internal homfunctor.
However neither of these are cartesian closed, and in fact for all $n$
the cartesian closed structure is the unique one with $I=n$.  We do not
as yet have a natural application for any of the structures on 4.
(2) We have already discussed $\Set$ with $\otimes$ taken to be
cartesian product, as a basic example of a nonstrict category.  This
monoidal structure for $\Set$ is cartesian closed, and will always be
the one we have in mind when referring to $\Set$ as a monoidal
category.  In the case of $\Set$ the internal homfunctor is {\it
identified with} its external one.
(3) Let $\R_\land$ denote the real numbers together with $\infty$ and
$-\infty$ with the usual ordering and considered as a category in the
usual way.  Now $\R_\land$ is bicomplete, and furthermore is cartesian
closed with $a\otimes b=a\land b$, $I=\infty$, and internal homfunctor
$c^b=\infty$ for $b\le c$ and $c$ otherwise (cf. the cartesian closed
ordinals above).  $\R_\land$ is isomorphic to its opposite
$\R\op_\lor$, the reals with their order reversed and with $\otimes$
now $\lor$.  $\R\op_\lor$ is the metric used for so-called ultrametric
spaces.
However a more useful closed structure for our purposes will be that
obtained by taking tensor product to be not min but +, making the unit
0, and with $\infty+({-}\infty)=-\infty$, necessary in order to be
closed.  We denote it by $\R$, or $\R_+$ when there might be
confusion.  To be closed requires $c^b$ satisfying $a+b\le c\cong a\le
c^b$, for which $c^b=c-b$ is the patently obvious solution.  Hence $\R$
is bicomplete and closed, but of course not cartesian closed since, as
we saw with the ordinals, a category admits at most one cartesian
closed structure.
We use $\R$ to represent lower bounds on delay.  A distance of 5 units
from event $u$ to event $v$ means that $v$ must wait at least 5 units
after $u$.  Thus a delay of 0 from $u$ to $v$ simply asserts that $v$
follows $u$, not necessarily strictly.
Now a delay of -5 units from $u$ to $v$ indicates that $v$ may precede
$u$ by at most 5 units.  Hence we can express upper bounds as negative
lower bounds in the opposite direction.  So to indicate that $v$ must
follow $u$ by 2 to 5 units we bound from below the delay from $u$ to
$v$ by 2 and that from $v$ to $u$ by -5.
Combining these two directions, we may read the two oppositely oriented
edges between $u$ and $v$ as together defining an interval.
Here as with $\R_\land$, $\R$ is isomorphic to its opposite $\R\op$,
the reals with their order reversed, however this time with the only
change to the monoidal structure being $\infty+(-\infty)=\infty$, this
being the one bit of asymmetry in $\R$.  As we have seen, $\R\op$ is
the monoidal structure associated with ordinary metric spaces.
A sometimes useful closed subcategory of $\R\op$, namely $\R\op_\ge$,
is obtained by omitting the negative reals and $-\infty$ \cite{Law}.
The internal homfunctor then becomes {\it truncated} subtraction, in
which negative differences are rounded up to 0.  This is the category
of generalized metric spaces; if the further restrictions are made that
distances be symmetric and distinct points are a nonzero distance apart
then we have the usual category of metric spaces and their
contractions, modulo a detail about constant factors in the
contractions.  $\R\op_\lor$ may be similarly truncated and its $I$ set
to 0 to yield Lawvere's basic example \cite{Law} of a cartesian and a
noncartesian closed structure on the same category with the same I.
(4) Take $\SR$ to be the category with objects arbitrary sets of reals
and with morphisms $X\to Y$ just when $X\subseteq Y$.  This poset is
cartesian closed when we take $\otimes=\cap$ and $I=\R$.  As with $\R$
however we shall prefer a different, hence noncartesian, closed
structure, namely $X\otimes Y = \{x+y\mid x\in X,y\in Y\}$ with
$I=\{0\}$, and with internal homfunctor $Z^Y=\{x \in \R \mid \{x\}+Y
\subseteq Z\}$.
The meaning of a set as a delay is that it consists of the disallowed
actual delays.  Thus $\emptyset$, like $-\infty$ in $\R$, is no
constraint while $\R$, like $\infty$, disallows all delays.
We may now find $\R$ and $\R\op$, as well as $\R\op$ truncated at 0, as
subcategories of $\SR$.  We note in particular that
$\R+\emptyset=\emptyset$, corresponding to $\infty+-\infty=-\infty$ in
$\R$.
(5) Any monoid $(M,\cdot,\epsilon)$ automatically forms a strict
monoidal category by taking the set $M$ as a discrete category.
Alternatively $M$ may be taken as indiscrete (the maximal preorder on
$M$).  We refer to these as discrete and indiscrete monoids
respectively.
For a discrete monoid to be closed means simply that for all $b,c$,
$a+b=c$ has a solution in $a$, whence closed discrete monoids coincide
with groups.  No nontrivial discrete monoid has finite products or
coproducts.
An indiscrete monoid on the other hand is trivially closed with all
limits and colimits.  Only the fact that it is strictly monoidal saves
it from total anarchy.  A nonstrict monoidal codiscrete category is no
more than an arbitrary binary operation on a pointed but otherwise
indiscrete set; nevertheless all such are bicomplete and closed.
(6) The category $\Pos$ of partially ordered sets forms a subcategory
of the cartesian closed category $\Pros$ of preordered sets.  The
tensor product is direct or cardinal \cite{Birk42} product of
preorders.  The cartesian closed structure of $\Pros$ is inherited from
that of its underlying metric, namely the cartesian closed $\two$.  The
following section on enrichment treats the passage from the metric to
the spaces in this example and the next two.
By the same token Gaifman's computations with distinct accidental and
causal orders \cite{Ga89} form a subcategory of a cartesian closed
category of such computations with cycles allowed.  As with $\Pros$ the
cartesian closed structure is inherited from that of its underlying
metric, here $\three$.
The Gaifman-Pratt ``prossets'' or preordered specification sets
\cite{GP}, each consisting of a set with an irreflexive partial order
$<$ and a preorder $\le$, with $u<v\le w\to u<w$, form a subcategory of
a noncartesian closed category of ``preprossets'' in which $<$ is
itself just a preorder, but still meeting the condition $u<v\le w\to
u<w$.
\subsection{Monoidal Functors}
Monoidal functors, as the appropriate morphisms of monoidal categories,
should preserve both the monoidal and category structure.  Just as
strict monoidal categories motivate monoidal categories, so do strict
monoidal functors motivate monoidal functors.  A {\it strict monoidal
functor\/} $F:\D\to\D'$ between monoidal categories $\D,\D$ is a
functor $F:D\to D'$ between their underlying categories satisfying
$Fx\otimes'Fy=F(x\otimes y)$ and $I'=FI$ for objects and similarly for
morphisms.  (The unit morphism is often written 1 instead of $I$ or
$1_I$.)
{\bf Definition}  A {\it lax monoidal functor}
$(F,\tau,t):(D,\otimes,I,\alpha,\lambda,\rho,\gamma)$ $\to$
$(D',\otimes',I',\alpha',\lambda',\rho',\gamma')$ consists of a functor
$F:D\to D'$, a natural transformation $\tau_{xy}:Fx\otimes'Fy\to
F(x\otimes y)$, and a morphism $t:I'\to FI$ of $D'$, with certain
coherence conditions requiring that natural transformations constructed
from $\tau$ and $t$ commute with $\alpha,\lambda,\rho,\gamma$ and all
the other natural transformations corresponding to the equations of the
theory of commutative monoids \cite{EK66a}.
When $\tau$ and $t$ are both isomorphisms or both identities we call
$F$ respectively {\it strong} or {\it strict}.  For the remainder of
this paper the default will be strong, that is, we take ``monoidal
functor'' to mean ``strong monoidal functor.''  In particular we take
the morphisms of the category {\bf SMON} of large (symmetric) monoidal
categories to be the strong monoidal functors.
We wish to be able to refer to the ``points'' of spaces.  This is
accomplished by the next definition.
{\bf Definition.}  The category $\SSM$ is the slice (comma) category
${\bf SMON}/\Set$.  Its objects are pairs $(\D,U)$ called {\it
semiconcrete monoidal categories}, where $\D$ is a (large) monoidal
category and $U_\D:\D\to\Set$ is a monoidal ``forgetful functor'' for
$\D$.  The morphisms $F:(\D,U)\to(\D',U')$ of $\SSM$ are monoidal
functors satisfying $U=U'F$, $\tau_U=\tau_{U'}\tau_F$, $t_U=t_{U'}t_F$.
Our interest in $\SSM$ is that its members carry enough structure to
support the definitions of the operations $\D!$ and $\D\rhd\E$
constructing categories of spaces and labeled spaces.  While this adds
some complexity to the development of enrichment, it does demonstrate
the feasibility of adding such structure when needed.  It would be
particularly useful to have a characterization of what structures can
be so added.
All the examples of monoidal categories in our list above belong to
$\SSM$; of these, only the discrete monoids are not bicomplete.
$\Set$, $\Pos$, etc. are large objects in $\SSM$.  The ordinal $\one$
is the null object of $\SSM$.
Our insistence on the identity $U=U'F$, as opposed to just a natural
transformation from $U$ to $U'F$, makes for a clean division of labor
between $\SSM$, where the kind language KL operates, and the objects of
$\SSM$, where PSL operates.  The significance of this identity is that,
via functors of $\SSM$, KL may act on kinds without disturbing the
underlying sets of objects of those kinds.
For example when we replace a numeric metric by a Boolean one we {\it
identically} preserve the vertex sets of the affected behaviors; only
the distances between their elements change, from numbers to truth
values.  In PSL on the other hand we work in a fixed object $\D$ of
$\SSM$, where we may do violence to vertex sets and alphabets via
morphisms of $\D$, but where we cannot change to another $\D$ and so
have no control over the metric or the kind of alphabet.
As a pleasant fringe benefit the bidirectionality of the identity in
$U=U'F$ permits the domain of $\comma$ to consist of all pairs $F,G$ of
functors of $\SSM$, not just those for which there exists a natural
transformation from $U'F$ to $U$.  However this benefit would accrue
even from a natural isomorphism $h:U\to U'F$ (assuming $h$ commutes
with both $\tau$ and $t$), whereas identity results
in total separation of the domains of KL and PSL.
\subsection{Examples of Monoidal Functors}
(1) Consider functors $F,G:\R\to \two$, defined by $F(x)=(x\ge 0)$ and
$G(x)= (x>-\infty)$.  Each functor equips its target with an
interpretation.  $F$ interprets $u\le v$ as saying that $u$ must
precede $v$, while $G$ makes it say that $v$ can only precede $u$ by a
bounded amount.  Only $G$ however is strong monoidal, since
$F(1+-1)=F(0)=1$ while $F(-1)\land F(1)=0$.  It is straightforward to
show that $G$ and the constantly true functors are the {\it only}
strong monoidal functors from $\R$ to $\two$.  In fact with the obvious
order on the functors from $\R$ to $\two$ to make $\two^\R$ a category,
we have $\two^\R\cong\two$ in $\SSM$, with the constant functor in
$\two^\R$ corresponding to 1 in $\two$.
Now consider any functor $F$ from $\two$ to $\R$.  $F$ must send 1 to
0, so $F(0)$ cannot be positive.  Moreover $F(0) =
F(0\land0)=F(0)+F(0)$ whence $F(0)$ must be either $-\infty$ or 0.
Hence $\R^\two\cong\two$ (again with $\R^\two$ made a category via the
obvious order on its two functors), with the constant functor in
$\R^\two$ corresponding to 1 in $\two$.
(2) The endofunctor $x/2$ from $\R$ to $\R$ that simply halves its
argument is clearly monoidal.  This is a ``speedup'' functor that
allows one to pass to a world where everything happens twice as fast.
In fact from $F(a+b)=F(a)+F(b)$ and $F(0)=0$ we infer that the linear
speedups and slowdowns and their negations (time reversals) are the
only functors, and thus we have $\R^\R\cong\R$.  The $\infty$ and
$-\infty$ speedups are included, and their range in each case is
isomorphic to the noncartesian closed ordinal $\three'$ with the
convention that $0\otimes\infty=0=0\otimes-\infty$.
(3) We leave it to the reader to verify that $\two^\two\cong\two$
with the constant functor corresponding to 1 as always.
\def\hfdot{\mkern6mu\cdot\mkern6mu}
%\def\item#1#2\enditem{\hfil\break\kern\parindent\llap{#1}{\advance\hsize by-\parindent\vtop{#2}}}
\section{Enriched Categories and the ! Operator}
We now introduce the basic notions of enriched categories.  Our hope is
that these will be made more accessible via definitions that are not
only close at hand but presented from the same perspective as the
applications.  Enriched categories or $V$-categories are treated
briefly by Arbib and Manes \cite{AM} and exhaustively and precisely by
Kelly \cite{Kel}.  Section I-8 of Mac~Lane also touches on them,
without calling them such.  As far as we are aware ours is the first
proposed engineering application of Lawvere's vision \cite{Law} of
enriched categories as a combined generalized metric and logic.
\subsection{\D-categories}
The essence of an enriched category may be found in an ordinary
category $C$.  Write $\d(u,v)$ for the set of morphisms from $u$ to
$v$.  Associated with each triple $u,v,w$ of objects of $C$ is a
function $m_{uvw}:\d(u,v)\times\d(v,w)\to\d(u,w)$ defining
composition.  And to each object $u$ there is a function
$j_u:\{\cdot\}\to\d(u,u)$ picking out the identity element
$1_u\in\d(u,u)$.
We pass from this account of an ordinary category $C$ to the notion of
a category $C$ {\it enriched in} $\D$, or $\D$-category, by requiring
each $\d(u,v)$ to be an object of $\D$ instead of a set, and each
$m_{uvw}$ and $j_u$ be a morphism of $\D$ instead of a function.  The
class of objects of $C$ do not participate in this passage: the objects
of $C$ remain a class.  A functor $F:A\to B$ participates partially
in this passage:  when we view it as the $\D$-functor $F:A\to B$, its
object part remains unchanged but its action on morphisms, viewed for
each pair $uv$ of objects of $A$ as a function
$F_{uv}:\d^A(u,v)\to\d^B(F(u),F(v))$, becomes a morphism of $\D$
between homobjects $\d^A(u,v)$ and $\d^B(F(u),F(v))$ of $A,B$
respectively.
From this viewpoint, ordinary categories and functors between them are
$\Set$-categories and $\Set$-functors, that is, categories and functors
enriched in $\Set$.
{\bf Definition.} A \D-{\it category} $A=(V,\d,m,j)$, or
{\it category enriched in} \D, consists of a set $V$,
a function $\d:V^2\to\ob(\D)$, and
families of morphisms of \D, namely compositions
$m_{uvw}:\d(u,v)\otimes\d(v,w)\to\d(u,w)$ and
identities $j_u:I\to\d(u,u)$,
such that for all objects $u,v,w$ in $V$ the following diagrams commute.
These diagrams express associativity of composition, and the left
and right identity laws, explained below.
$$\commdiag
{(\d(u,v)\otimes \d(v,w))\otimes \d(w,x) &\rTo{\alpha_{\d(u,v)\d(v,w)\d(w,x)}}{}\across 3 & \d(u,v)\otimes
(\d(v,w)\otimes \d(w,x))\cr \dTo{}{m_{uvw}\otimes1} & & & &\dTo{1\otimes m_{vwx}}{}\cr
\d(u,w)\otimes \d(w,x)  &\rTo{m_{uwx}}{} & \d(u,x) & \lFrom{m_{uvx}}{} &\d(u,v)\otimes \d(v,x)\cr
$$\commdiag
{I\otimes \d(u,v)&\rTo{\lambda_{\d(u,v)}}{}       &\d(u,v)&\lFrom{\rho_{\d(u,v)}
}{}   &\d(u,v)\otimes I\cr
\dTo{}{j_u\otimes 1}&               &\vEq{}{}&               &\dTo{1\otimes j_v}{}\cr
\d(u,u)\otimes \d(u,v)&\rTo{m_{uuv}}{}&\d(u,v)&\lFrom{m_{uvv}}{}&\d(u,v)\otimes
\d(v,v)\cr
For $\D=\two$ the diagrams expressing the associativity and identity
laws hold vacuously since $\D$ is an ordered set.  Thus composition and
identity become
$$\eqalign
{m_{uvw}:&u\le v~\land~ v\le w~~\to~~u\le w\cr
j_u:&u\le u \cr}
expressing respectively transitivity and reflexivity.  Thus
\two-categories (categories enriched in \two, as opposed to
2-categories which here are \Cat-categories) are just preorders.
For $\D=\R\op$, also an ordered set, we again may ignore the associativity and
identity laws.  Here we get
$$\eqalign
{m_{uvw}:&d(u,v)+d(v,w)\ge d(u,w)\cr
j_u:&0\ge d(u,u)\cr
%In this case $m$ expresses the triangle inequality while $j$ forces
%$\d(u,u)=0$, as there are no negative distances.  Thus $\R\op$-categories are
%what we shall call premetric spaces (Lawvere calls them generalized
%metric spaces), lacking the other two Fr\'echet conditions
%$\d(u,v)=\d(v,u)$ and $\d(u,v)=0$ implies $u=v$.  This example supports
%a more informative notion of concurrent behavior than preorders, since
%now the {\em delay} between two events can be indicated in addition to their
%precedence relation.
For $\D=\Cat$ we obtain ordinary 2-categories, along the same lines as
for $\D=\Set$ but with the addition of 2-cells between morphisms of
the same homset.
\subsection{\D-functors}
{\bf Definition}.  A \D-{\it functor} $F:A\to B$ where $A$ and $B$
are {\D}-categories consists of a function $F:V_A\to V_B$ between object
sets together with a family $F_{uv}:\d_A(u,v)\to \d_B(Fu,Fv)$
of morphisms between homobjects satisfying the following conditions
stating that compositions and identities are preserved.
$$\vbox{$\commdiag
{\d_A(u,v)\otimes \d_A(v,w)&\rTo{m_{uvw}}{}&\d_A(u,w)\cr
\dTo{F_{uv}\otimes F_{vw}}{}&        &\dTo{F_{uw}}{}\cr
\d_B(Fu,Fv)\otimes \d_B(Fv,Fw)&\rTo{m_{Fu,Fv,Fw}}{}&\d_B(Fu,Fw)\cr
\hfill\commdiag
{I&\rTo{j_u}{}&\d_A(u,u)\cr
\vEq{}{}&&\dTo{F_{uu}}{}\cr
I&\rTo{j_{Fu}}{}&\d_B(Fu,Fu)\cr
}$}$$
The elements of a $\D$-functor are depicted on the left of the following
figure, and compose in the obvious way as shown on the right.
$$\commdiag
{       u & \rImplies{\d_A(u,v)}{}  & v\cr
\dMapsto{F}{} & \dTo{F_{uv}}{} &\dMapsto{F}{}\cr
\noalign{\vskip5pt}
        Fu & \rImplies{\d_B(Fu,Fv)}{} &Fv\cr
 ~~~~~~~~
\commdiag
{       u & \rImplies{\d_A(u,v)}{}  & v\cr
\dMapsto{F}{} & \dTo{F_{uv}}{} &\dMapsto{F}{}\cr
\noalign{\vskip5pt}
        Fu & \rImplies{\d_B(Fu,Fv)}{} &Fv\cr
\dMapsto{G}{} & \dTo{G_{Fu,Fv}}{}   &\dMapsto{G}{}\cr
\noalign{\vskip5pt}
       GFu & \rImplies{\d_C(GFu,GFv)}{} & GFv\cr
It can be seen that \two-functors are monotone functions, \R-functors
and $\R\op$-functors are expanding and contracting maps respectively,
and \Set-functors are ordinary functors.  In our computational
application a \D-functor is an event map which maintains all temporal
constraints, though the result may have more constraints than the
source.
\subsection{Enrichment as a Function}
We now define the object part of the functor $-!:\SSM\to\SSM$.  Given a
semiconcrete monoidal $\D$ define $\D!$ to be the category {\D-\Cat} of
small categories enriched in $\D$.
$\D!$ is symmetric monoidal as follows \cite{EK66a}.  The tensor product
of two $\D$-categories $A$ and $B$ is defined to have as objects the
cartesian product $V_{A} \times V_{B}$, and homobjects
$$\d((u,v),(u',v')) = \d_{A}(u,u') \otimes_\D \d_{B}(v,v').$$ The
symmetry of $\D$ ensures that appropriate composition morphisms can be
defined and that $\D!$ is symmetric to boot.  The corresponding unit
$I$ is the one-object category with homobject
$\d_{I}(\cdot,\cdot)=I_\D$.
To make $\D!$ semiconcrete we define the forgetful functor
$U_{\D!}:\D!\to\Set$ mapping each $\D$-category $A$ to its underlying
set $V_A$ of objects and each $\D$-functor to its object map.
$U_{\D!}$ is monoidal by the above definition of $\otimes$ for $\D!$.
In our application $U$ yields the event set $U(b)$ of a behavior $b$.
We summarize the above as follows.
\begin{lemma}
If $\D$ is an object of $\SSM$ then so is $\D!$.
\end{lemma}
\subsection{Enrichment as a Functor}
We now define the action of ! on morphisms of $\SSM$.
\def\Fcat{{F_{\hbox{cat}}}}
{\bf Definition}
Given a monoidal functor $(F,\tau,t):\D\to \E$, define the functor
$(F,\tau,t)!=(F!,\tau!,t!):\D!\to\E!$ as follows:
$F!$ takes a $\D$-category $A$ to the $\E$-category $F!A=(V,\d,m,j)$
defined by
$$\eqalign{V        &= V_A  {\rm ~~~~(that~is,~~} U_{\D!}=U_{\D'!}F!) \cr
\d(u,v)  &= F(\d_A(u,v))\cr
m_{uvw}  &= F(m^{A}_{uvw})\tau_{\d_A(u,v)\d_A(v,w)}\cr
j_u      &= F(j^A_u)t\cr
$F!$ takes a \D-functor $G:A\to B$, to that $\E$-functor $F!G$ which
has the same object function and takes $(F!G)_{uv}$ to $F(G_{uv})$.
Thus $F!$ acts only on the distances within a behavior, and on the
``distance comparison'' part of a morphism of behaviors.
For $\D$-categories $A$ and $B$ and objects $u$ and $u'$ or $A$, and
$v$ and $v'$ of $B$, define $$(\tau!)_{(u,v)(u',v')} =
\tau_{\d_A(u,u'),\d_B(v,v')}.$$
By the definition of $F!$, $F!I_{\D!}$ is an $\E$-category with a
single object.  Thus there is a unique possible object map for
$t!:I_{\E!}\to F!I_{\D!}$.  $t!$ on homobjects must be a map from
$I_\E\to FI_\D$; define this map to be $t$.
\begin{lemma}
If $(F,\tau,t):\D\to\E$ is a morphism of $\SSM$ then so is
$(F!,\tau!,t!):\D!\to\E!$.
\end{lemma}
We omit the straightforward, though tedious, proof.
Finally, by checking that $!$ preserves composition and identities, we
obtain the following.
\begin{theorem}
! is an endofunctor on $\SSM$.
\end{theorem}
%\subsection{Enrichment as a Functor}
%We now define the action of ! on morphisms of $\SSM$.
%\def\Fcat{{F_{\hbox{cat}}}}
%{\bf Definition}
%Given a monoidal functor $F:\D\to \D'$, define the functor
%$F!:\D!\to\D'!$ as follows:
%For any \D-category $A$, we obtain the $\D'$-category $F!A=(V,\d,m,j)$ as
%$$\eqalign{V        &= V_A  {\rm ~~~~(that~is,~~} U_{\D!}=U_{\D'!}F!) \cr
%           \d(u,v)  &= F(\d_A(u,v))\cr
%           m_{uvw}  &= F(m^{A}_{uvw})\tau_{\d_A(u,v)\d_A(v,w)}\cr
%           j_u      &= F(j^A_u)t\cr
%For any \D-functor $G:A\to B$, we obtain a $\D'$-functor $F!G$ by
%using the same object function and by taking $(F!G)_{uv} =
%F(G_{uv})$.  Thus $F!$ acts only on the distances within a behavior, and
%on the ``distance comparison'' part of a morphism of behaviors.
%\begin{lemma}
%If $F:\D\to\D'$ is a morphism of $\SSM$ then so is $F!:\D!\to\D'!$.
%\end{lemma}
%We omit the straightforward proof.
%From these two lemmas we obtain the following.
%\begin{theorem}
%! is an endofunctor on $\SSM$.
%\end{theorem}
\subsection{Examples}
(1) Section 2 contains a figure illustrating the example
$(a;^3b)\otimes(c;^2d)$ of orthocurrence.
%(1)  We saw in Section 2 the example $010\otimes TR$ of a stream $010$
%of three messages flowing along a transmit-receive channel $TR$.  This
%example was located in $\Pom$.  If we relocate it to $\R\op!$ (ignoring
%labels) we may talk about upper bounds on delay.  For example
%$(0;^21;^30)\otimes(T;^7R)$ specifies a delay of at most 2 units between
%the first two messages and 3 between the last two, compounded with a
%delay of 7 units along the channel.  Pairs $u,v$ of events without a
%chain of edges from $u$ to $v$ are presumed to have an edge labeled
%$\infty$, corresponding to no constraint.
%$$\commdiag{
%0 & \rTo{2}{} & 1 & \rTo{3}{} & 0\cr
%\hskip1em \otimes \hskip1em
%\commdiag{
%T\cr
%\dTo{7}{}\cr
%R\cr
%\hskip2em = \hskip2em
%\commdiag{
%(0,T)& \rTo{2}{} & (1,T)     & \rTo{3}{} & (0,T) \cr
%\dTo{7}{}&       & \dTo{7}{} &           & \dTo{7}{} \cr
%(0,R)& \rTo{2}{} & (1,R) & \rTo{3}{} & (0,R) \cr
The triangle inequality requires the upper bounds on diagonals across
squares and rectangles to be at most the sum of the bounds encountered
along any path around the sides, e.g. 5 from $ac$ to $bd$.  This is
exactly the effect obtained by defining tensor product of spaces
(enriched categories) in terms of the addition (tensor product) of the
underlying metric.  Had we defined tensor product of spaces in terms of
ordinary product in the metric (min), we obtain the next example,
ordinary product of spaces.
(2) Consider the monoidal functor $F:\R\to\two$ which takes $-\infty$
to 0 and all else to 1.  Application of $F!$ to each of the illustrated
examples of Section 2 with vertex labels deleted to make them objects
of $\R!$, produces the corresponding object of $\two!$, a poset, in
effect by erasing the edge labels.
\subsection{Continuity of !}
We now show that ! enjoys certain continuity properties.  These will be
used in section~\ref{sec:langs} to show that all KL kinds are
bicomplete and closed, which in turn ensures that PSL is well-defined.
\begin{proposition} If {\D} has an initial object $0$ and a natural
isomorphism $A\otimes 0\cong 0$ then {\D!} has coproducts.
\end{proposition}
The natural isomorphism $A\otimes 0 \cong 0$ always exists when $\D$ is
closed.
A discrete category is a copower in $\Cat$ of 1, that is, the coproduct
of a set of one-object categories, yielding the following similar
result:
\begin{proposition}
If {\D} has an initial object $0$ and $0\otimes A\cong 0\cong A\otimes 0$,
then the forgetful functor $U_{\D!}:\D!\to\Set$ has a left adjoint
$D:\Set\to\D!$ taking a set $S$ to the corresponding {\rm discrete}
{\D}-category ($\d_{DS}(u,v)=I$ if $u=v$, 0 otherwise).
\end{proposition}
The dual result to this, though not with a dual proof, is:
\begin{proposition}
If {\D} has a final object $1$, $U_{\D!}:\D!\to\Set$ has a right adjoint
$E:\Set\to\D!$ taking the set $X$ to the corresponding chaotic
(codiscrete) {\D}-category ($\d_{DS}(u,v)=1$ for all $u,v$).
\end{proposition}
Meanwhile, for the case of general colimits we refer to a result of
\cite{BCSW}.
\begin{theorem}
If {\D} is cocomplete and {\D} is closed then {\D!} is cocomplete.
\end{theorem}
There is also a similar but much easier result about limits.  PSL needs
limits for local product and hence local concatenation.
\begin{theorem}
If {\D} has limits of (small) type {\cal J}, then so does {\D!}.
\end{theorem}
If any one theorem could be considered at the heart of enriched
categories it is the following.  Kelly's proof (\cite{Kel} p.55, see
also Lawvere \cite{Law} p.153) is dauntingly formal, to which we offer
an informal counterpart.
\begin{theorem}
If \D\ is complete and closed then $\D!$ is closed.
\end{theorem}
\begin{proof}
The objects of the $\D$-category $C^B$ are of course just the
$\D$-functors from $B$ to $C$.  What is less obvious is the appropriate
homobject $\d_{C^B}(U,V)$ abstracting the homset of natural
transformations between any two $\D$-functors $U,V$ of $C^B$.  The
natural {\it and unnatural} transformations are given by $\prod_{b\in
B}\d_C(Ub,Vb)$; we seek its subobject $\int_{b\in B}\d_C(Ub,Vb)$ (an
{\it end} \cite{Mac} p.219) consisting of just the natural ones.
Now for $\D=\Set$ such a transformation $\tau$ determines, for all
$b,b'$, two functions $\rho_\tau,\sigma_\tau:\d_B(b,b')\to
\d_C(Ub,Vb')$, that is, two elements of $\d_C(Ub,Vb')^{\d_B(b,b')}$.
Here $\rho_\tau$ takes $f:b\to b'$ to $V(f)\circ\tau_b$, while
$\sigma_\tau$ takes the same $f$ to $\tau_{b'}\circ U(f)$.  But these
are just the two sides of the square
$$\commdiag{
    Ub         & \rTo{\tau_b}{}    & Vb         \cr
    \dTo{Uf}{} &                   & \dTo{Vf}{} \cr
    Ub'        & \rTo{\tau_{b'}}{} & Vb'        \cr
which must be equal for $\tau$ to be natural.  Encapsulating ``for all
$b,b'$'' as a product over $b,b'\in B$ and generalizing to arbitrary
$\D$ (formalized in Kelly's proof), we may therefore obtain the desired
homobject $\d_{C^B}(U,V)$ as the equalizer of
$$    \d_{C^B}(U,V) \commdiag{\rTo{}{}}
    \prod_{b\in B}\d_C(Ub,Vb)
    \commdiag{\rTo{\rho}{}\cr\rTo{}{\sigma}}
    \prod_{b,b'\in B}\d_C(Ub,Vb')^{\d_B(b,b')}.$$
This construction required an exponential, two products, and an
equalizer, for which it suffices that $\D$ be complete and closed.
\end{proof}
\section{Comma Categories and the $\comma$ Operator}
\def\arrow#1{\stackrel{#1}{\longrightarrow}}
The ! operator creates categories of spaces with distances between
pairs of points.  We wish to interpret the points as events and the
distances as temporal constraints on the events.  To complete this
interpretation we must have some way to say what type of event each
point represents.
Given a labeling alphabet, a set $\Sigma$, we label the underlying set
$U(p)$ of points of a space $p$ with a function $\mu:U(p)\to\Sigma$.
For $p$ a poset this is the notion of pomset or partially ordered
multiset as a labeled partial order.
Our framework can be simplified by dropping the assumption that
$\Sigma$ is a pure set and instead associating with the category
supplying $\Sigma$ a forgetful functor $V$ that strips off any
unwanted structure to reveal its underlying set $V(\Sigma)$.  Our
labeling function then becomes $\mu:U(p)\to V(\Sigma)$.
But this is what it means to be an object of the comma category
$(U{\downarrow}V)$.  Moreover the morphisms of this comma category from
$\mu:U(p)\to V(\Sigma)$ to $\mu':U(p')\to V(\Sigma')$, namely pairs of
maps $f:p\to p'$ and $t:\Sigma\to\Sigma'$ such that $V(t)\mu =
\mu'U(f)$, turn out to be just what we need.
\subsection{The Function $\comma$}
Given categories $\D$, $\E$ in $\SSM$ (i.e., both symmetric monoidal
equipped with functors $U:\D\to\Set$, $V:\E\to\Set$, respectively), we
define $\D\comma\E$ to be the comma category $\UV$.  Recall
that this is the category whose objects are triples $\<x,\mu,u>$
where $\mu:Ux\to Vu$, and whose morphisms are pairs $\<f,g>$ such
that the following square commutes:
$$\commdiag{
        Ux  & \rTo{\mu}{} & Vu  \cr
        \dTo{Uf}{} &   & \dTo{Vg}{} \cr
        Ux' & \rTo{\mu'}{} & Vu'.
%define $\D\comma\E$ to be the comma category $(\UV)$, that is, the
%subcategory of $\D\times\SSM^\to\times\E$ whose objects $\<x,\mu,u>$
%satisfy $\mu:Ux\to Vu$ and similarly whose morphisms $\<f:x\to
%x',s,g:u\to u'>$ have for $s$ the commuting square
%$$\commdiag{
%    Ux  & \rTo{\mu}{} & Vu  \cr
%    \dTo{Uf}{} &   & \dTo{Vg}{} \cr
%    Ux' & \rTo{\mu'}{} & Vu'.
%In the following diagrams representing such morphisms $\<f:x\to
%x',s,g:u\to u'>$ we give only $s$, $f$ and $g$ being inferrable from $s$.
$\D\comma\E$ can be made symmetric monoidal by defining the tensor
product
    \commdiag{
    Ux  & \rTo{\mu}{} & Vu\cr
    \dTo{Uf}{} &   & \dTo{Vg}{} \cr
    Ux' & \rTo{\mu'}{} & Vu' }
    ~~~~~~~~\otimes~~~~~~~~
    \commdiag{
    Uy  & \rTo{\nu}{} & Vv \cr
    \dTo{Uh}{} &   & \dTo{Vk}{} \cr
    Uy' & \rTo{\nu'}{} & Vv'}
to be
\commdiag{
U(x\otimes y) & \lTo{\tau_U}{\congh} & Ux\times Uy & \rTo{\mu\times\nu}{} & Vu\times Vv
& \rTo{\tau_V}{\congh} & V(u\otimes v)\cr
\dTo{}{U(f\otimes h)} &
& \dTo{Uf\times Uh}{} & & \dTo{Vg\times Vk}{} & &  \dTo{V(g\otimes k)}{}
U(x'\otimes y') & \lTo{\tau_U}{\congh} & Ux'\times Uy' & \rTo{\mu'\times\nu'}{} & Vu\times Vv
& \rTo{\tau_V}{\congh} & V(u\otimes v)
The unit object of $D\comma \E$ is taken to be
$I_{\textstyle\D\comma\E}=\<I_{\D},h,I_{\E}>$, where $h=t_Vt_U^{-1}$
$$\commdiag{UI_{\D}&\lFrom{t_U}{\congh}&1&\rTo{t_V}{\congh}&VI_{\E}}$$
(In fact one may use these definitions for $\otimes$ and $I$ in the
case where $V$ is only lax monoidal; $U$ must still be strong monoidal).
Now we must show that this product is associative,
symmetric, and $I_{\textstyle\D\comma\E}$ is in fact an identity.  We outline
briefly the definition of the associativity natural transformation
$\alpha_{\textstyle\D\comma\E}$.  (Other required natural
transformations are defined similarly.)
We take
$\alpha_{{\textstyle\D\comma\E},\<x,\mu,u>\<x',\mu',u'>\<x'',\mu'',u''>}$
to be $\<\alpha_{\D,xx'x''},\alpha_{\E,uu'u''}>$.  This is a
well-defined morphism because $V(\alpha)(\mu\otimes(\mu' \otimes
\mu''))$ is equal to $((\mu \otimes \mu')\otimes \mu'')U(\alpha)$.
This requirement follows from properties of monoidal functors and
natural transformations.  The coherence conditions on
$\alpha_{\textstyle\D\comma\E}$ are established similarly.
We make $\D\comma\E$ semiconcrete by using the functor
$$\commdiag{\D\comma\E&\rTo{\pi_0}{}&\D&\rTo{U}{}&\Set}$$
This makes the underlying sets of objects of $\D\comma\E$ those of
objects of $\D$.  If the objects of $\D$ are spaces while those of
$\D\comma\E$ are labeled spaces, the underlying sets of the latter are
the same as those of the former, i.e. the labels are ignored.
\subsection{$\comma$ as a Functor}
To complete the description of the functor $\comma$ we describe its
action on morphisms (i.e., functors) $F,G$ of $\SSM$.
Recall that we impose the condition $U=U'F$ in the definition of the
morphisms $F$ of $\SSM$ as well as the condition that $F$ be strong monoidal.
The functor $F\comma G:\SSM~^2\to\SSM$ acts thus:
$$\commdiag{
\D        & \rTo{U}{}  & \Set     & \lFrom{V}{}  & \E        \cr
\dTo{}{F} &            & \vEq{}{} &              & \dTo{G}{} \cr
\D'       & \rTo{U'}{} & \Set     & \lFrom{V'}{} & \E'       \cr
\rMapsto{\comma}{}
\commdiag{
\D\comma\E        & \rTo{U\pi_0}{}   & \Set      \cr
\dTo{}{F\comma G} &              & \vEq{}{}  \cr
\D'\comma\E'      & \rTo{U'\pi_0'}{} & \Set      \cr
where $\pi_0$ projects onto $\D$ as before and $F\comma G$ takes each
morphism $\<f,g>$ of $\D\comma\E$ to $\<Ff,Gg>=\<U'Ff,V'Gg>$.
%morphism $\<f,s,g>$ of $\D\comma\E$ to $\<Ff,s,Gg>$ as shown, where
%$s$ denotes the innermost square of the following figure, and hence
%also the larger rectangle it is embedded in.
$$\commdiag{
U'Fx  & \hEq{}{} & Ux  & \rTo{\mu}{} & Vu  & \hEq{}{} & V'Gu\cr
\dTo{U'Ff}{}&&\dTo{Uf}{}&&\dTo{}{Vg}&&\dTo{}{V'Gg}\cr
U'Fx' & \hEq{}{} & Ux' & \rTo{\mu'}{} & Vu' & \hEq{}{} & V'Gu'\cr
We now need to verify that $F\comma G$ is strong monoidal.
This involves exhibiting a morphism
$\tau_{\textstyle F\comma G}:(F\comma G)\<x,\mu,u>\otimes(F\comma G)\<y,\nu,v>\to(F\comma G)(\<x,\mu,u>\otimes\<y,\nu,v>)$ of $\D'\comma\E'$
for any pair $\<x,\mu,u>$, $\<y,\nu,v>$ both in $\D\comma\E$,
namely that given by pairing $\tau_F:Fx\times Fy\to F(x\otimes y)$
with the corresponding $\tau_G$.
That this is indeed a morphism of $\D'\comma\E'$ depends on the
commutativity of the squares appearing in
$$\commdiag{
U'(Fx\otimes Fy)& \lFrom^{\tau_{U'}}_\cong & U'Fx\times U'Fy &&
V'Gu\times V'Gv & \rTo^{\tau_{V'}}_\cong & V'(Gu\otimes Gv) \cr
\VerticalMapExtraDepth14ex \dTo&& \vEq&
& \vEq&&\VerticalMapExtraDepth14ex \dTo\cr
U'\tau_F~\cong~~~~&& Ux\times Uy &
 ~~~~\stackrel{\mu\times\nu}{\longrightarrow}~~~~
&Vu\times Vv && ~~~~\cong~V\tau_G\cr
&&\dTo^{\tau_U}_\cong && \dTo^\cong_{\tau_V}&&\cr
U'F(x\otimes y)& \hEq & U(x\otimes y) &
&V(u\otimes v) & \hEq & V'G(u\otimes v)\cr
which follows from the $\tau_U=(U'\tau_F)\tau_{U'}$ condition in the
definition of $\SSM$.
That the morphisms $\tau_{\textstyle F\comma G}$ constitute a natural
transformation and that they satisfy the appropriate coherence
conditions directly follows from the corresponding naturality and
coherence conditions on $\tau_F$ and $\tau_G$.
\subsection{Continuity of $\comma$}\label{sec:comfunctors}
\def\J{J}
We now wish to lift limits and colimits that exist in the
component categories to comma categories defined from them.  To do this
we must deal with functors into comma categories.
The following lemma can be applied whenever functors into a comma
category are to be defined.  It states that defining a functor from a
category $\J$ into $(U{\downarrow}V)$, where $U:\A\to \C$ and $V:\B\to \C$,
is essentially equivalent to defining functors $F:\J\to \A$ and
$G:\J\to \B$ and a natural transformation from $UF$ to $VG$.
Furthermore, natural transformations between such functors are
essentially equivalent to a pair of natural transformations satisfying
a certain commutativity condition.
For any functor $F:\X\to\Y$
denote by $F^\J$ the functor from the functor category
$\X^\J$ to $\Y^\J$ defined by ``left-composition with $F$''.
Then we have:
\begin{lemma}\label{lem:functorcomma}
$\displaystyle (\UV)^\J \cong (U^\J \darrow V^\J).$
\end{lemma}
\begin{proofo}
The comma category $\UV$ has the projections
$\pi_0:\UV\to\A$ and $\pi_1:\UV\to\B$, and defines a natural transformation
$\nu:U\pi_0\to V\pi_1$.  (In fact this is an alternative definition
of the concept of a comma category.)
Hence, given a functor, $F:\J \to \UV$, we can define
functors $\pi_0F:\J\to\A$ and $\pi_1F:\J\to\B$, and a natural transformation
$\nu\circ F:U\pi_0F\to V\pi_1F$.  This defines an object of the
comma category $(U^\J \darrow V^\J)$.  It is routine to extend this
mapping to a functor
$\displaystyle (\UV)^\J \to (U^\J \darrow V^\J)$ and show that it
is an isomorphism of categories.
\end{proofo}
We can use this lemma to prove a basic result about limits in comma
categories.  (Note: Although this result is purely categorical we are
not aware of its having appeared in any textbook.  A marginally weaker
form was proven by Tarlecki in a rather different context~\cite{Tar85}
and Mac~Lane proved a special case as part of his proof of Freyd's
Adjoint Functor Theorem~\cite[page 123]{Mac}.)
\begin{theorem}\label{thm:comma}
Let $U:\A\to\C$ and $V:\B\to\C$ be functors, and $\J$ be a category.
If $\A$ and $\B$
have all $\J$-limits and $V$ preserves $\J$-limits then the comma
category $(U\darrow V)$ has all $\J$-limits
\end{theorem}
\begin{proof}
Let $F:\J\to (U\darrow V)$ be an $\J$-diagram in $(U\darrow V)$.  Then by
lemma~\ref{lem:functorcomma}, $F$ can
be considered as a triple, $\<F_1,\mu,F_2>$ where
\begin{eqnarray*}
F_1:\J\to\A\\
F_2:\J\to\B\\
\mu:UF_1\to VF_2
\end{eqnarray*}
Since $\A$ and $\B$ have $\J$-limits, both $F_1$ and $F_2$ have limits.
Denote their limiting cones by $\lambda^1:\lim F_1\to F_1$ and
$\lambda^2:\lim F_2 \to F_2$ respectively.
Since $V$ preserves $\J$-limits, $V(\lim F_2)$ is a limit of $VF_2$,
with limiting cone $V\lambda^2$.
Now the composite natural transformation
U(\lim F_1)\to{U\lambda^1} UF_1 \to{\mu} VF_2
is a cone from $U(\lim F_1)$ to $VF_2$, so by the universal property of
limits there exists a unique arrow $p$ such that the following diagram
of functors and natural transformations commutes.  (Note: in this and
the following diagrams an object of $C$ represents the constant functor
to that object and an arrow of $C$ represents the ``constant''
natural tranformation between such constant functors.)
\begin{center}\begin{picture}(125,65)
        \put(55,51){$\scriptstyle U\lambda^1$}
\put(0,45){$U(\lim F_1)$}\put(45,48){\vector(1,0){45}}\put(93,45){$UF_1$}
\put(9,25){$\scriptstyle p$}\put(15,42){\vector(0,-1){29}}
\put(105,42){\vector(0,-1){29}}\put(108,25){$\scriptstyle \mu$}
        \put(55,6){$\scriptstyle V\lambda^2$}
\put(0,0){$V(\lim F_2)$}\put(45,3){\vector(1,0){45}}\put(93,0){$VF_2$}
\end{picture}\end{center}
Now we claim that $\<\lim F_1,p,\lim F_2>$ is the limit of $F$, and that
the limiting cone is defined by the pair of natural transformations
$\<\lambda^1,\lambda^2>$.
For suppose we have an object, $\<A,f,B>$ and a cone
$\kappa:\<A,f,B>\to F$.  $\kappa$ can be considered as a pair
of natural transformations, $\kappa^1:A\to F_1$ and
$\kappa^2:B\to F_2$.  Since $F_1$ and $F_2$ have limits there
must exist unique maps $a:A\to \lim F_1$ and $b:B\to \lim F_2$
which factor $\kappa^1$ and $\kappa^2$ through $\lambda^1$ and
$\lambda^2$ respectively.
Consider the following diagram of natural transformations.
\begin{center}\begin{picture}(250,130)
             \put(120,116){$\scriptstyle f$}
\put(30,110){$UA$}\put(55,113){\vector(1,0){130}}\put(190,110){$VB$}
\put(47,102){\vector(1,-2){16}}\put(60,82){$\scriptstyle Ua$}
\put(186,102){\vector(-1,-2){16}}\put(160,82){$\scriptstyle Vb$}
         \put(110,61){$\scriptstyle p$}
\put(50,55){$U(\lim F_1)$}\put(97,58){\vector(1,0){37}}\put(145,55){$V(\lim F_2)$}
\put(63,50){\vector(-1,-2){16}}\put(60,25){$\scriptstyle U\lambda^1$}
\put(170,50){\vector(1,-2){16}}\put(160,25){$\scriptstyle V\lambda^2$}
             \put(110,6){$\scriptstyle \mu$}
\put(25,0){$UF_1$}\put(55,3){\vector(1,0){130}}\put(185,0){$VF_2$}
\put(15,55){$\scriptstyle U\kappa^1$}\put(35,102){\vector(0,-1){85}}
\put(203,55){$\scriptstyle V\kappa^2$}\put(200,100){\vector(0,-1){85}}
\end{picture}\end{center}
The outer square of this diagram commutes because $\kappa$ is  an
arrow in the comma category.  The two inner triangles commute by definition
of $a$ and $b$.  The lower inner square commutes by definition of $p$.
Now we wish to show that the upper inner square commutes.  We do this
by showing that the cone $(V\lambda^2).(Vb).f$ is identical to the cone
$(V\lambda^2).p.(Ua)$.  Since
there must be a {\em unique\/} arrow which
factors this cone through the limiting cone $V\lambda^2$, we can conclude
that the arrows $(Vb).f$ and $p.(Ua)$ must be identical.  This is the
required commutativity condition.  But we have
$$\begin{array}{rcll}
(V\lambda^2).(Vb).f &=& (V\kappa^2).f &\ \hbox{definition of $b$}\\
            &=& \mu.(U\kappa^1)&\ \hbox{outer square commutes}\\
            &=& \mu.(U\lambda^1).(Ua)&\ \hbox{definition of $a$}\\
            &=& (V\lambda^2).p.(Ua)&\ \hbox{lower square commutes}
\end{array}$$
This proves the required commutativity, which shows that $\<a,b>$ is
an arrow in $\UV$ and that it factors $\kappa$.  That $\<a,b>$ is
the unique such arrow follows from the fact that $a$ must factor
$\kappa^1$ through the limiting cone $\lambda^1$, so $a$ is the
unique such arrow.  Similarly, $b$ must factor $\kappa^2$
through $\lambda^2$, and so is unique.
\end{proof}
Note that the proof gives an explicit construction of limits in a
comma category when the conditions of the theorem are satisfied.
The same technique allows us to construct colimits:
\begin{corollary}
If $\A$ and $\B$ have all $\J$-colimits and $U$ preserves $\J$-colimits then
$\UV$ has all $\J$-colimits.
\end{corollary}
\begin{proof}
For any functor $U:\A \to C$, let $U\op$
be the corresponding functor $U\op: \A\op \to C\op$.  Observe that
    (U\darrow V)\op = (V\op\mathord{\darrow}U\op).
\end{proof}
With rather more work we may show that under appropriate conditions
$\UV$ is closed.
\begin{theorem}
Suppose that $\A$ and $\B$ are monoidal closed, and that $\C$ is monoidal.
Suppose further that $F:\A\to\C$ is a strong monoidal functor, that
$G:\B\to\C$ is (lax) monoidal, and that $\A$ has all pullbacks.  If $F$
admits a right adjoint, $R$, then $F\darrow G$ is closed.
\end{theorem}
\noindent{\it Proof Outline}:  The proof is in three stages.  Under
the assumptions of the theorem we show:
\begin{enumerate}
\item $R$ is monoidal and hence that $RG$ is monoidal;
\item $F\darrow G$ is isomorphic to $1_\A\darrow RG$; and finally
\item For any monoidal functor $H:\A\to\B$, $1_\A\darrow H$
        is closed.
\end{enumerate}
We adopt the following notation.  Suppose that $F \dashv R$.  For any
arrow $g:FA\to B$ denote the adjoint transpose by $g^\sharp: A\to RB$.
Dually, denote the adjoint transpose of $f:A\to RB$ by $f^\flat:FA \to B$.
Observe that for appropriate arrows $f,g$ and $g'$ we have
\begin{eqnarray*}
    (g'g)^\sharp &=& (Rg')g^\sharp\\
    \bigl(g(Ff)\bigr)^\sharp &=& g^\sharp f.
\end{eqnarray*}
The dual results, $(ff')^\flat = (f^\flat)(Ff')$ and
$\bigl((Rg')f\bigr)^\flat=g'f^\flat$ will also be useful.
We now proceed with the proofs of the three lemmas which prove the
theorem.
\begin{lemma}
Let $F:\A\to\C$ be strong monoidal and have a right adjoint, $R$.
Then $R$ is monoidal.
\end{lemma}
\begin{proof}
Let $\phi:FA\otimes FB \to F(A\otimes B)$ and $\widehat\phi: I \to FI$ be
the isomorphisms which make $F$ monoidal.
Define $\psi:RX\otimes RY \to R(X\otimes Y)$ to be the adjoint transpose
of the composite
    F(RX\otimes RY) \arrow{\phi^{-1}} FRX \otimes FRY \arrow{\epsilon\otimes\epsilon} X\otimes Y;
and $\widehat\psi:I\to RI$ to be $(\widehat\phi^{-1})^\sharp$.
To show that $\phi$ and $\widehat\phi$ make $R$ into a monoidal functor, we
must show that they satisfy the coherence conditions.  We give here the
proof of the associativity condition.  The proofs of the other two
conditions are similar.
$F$ is monoidal, so we know that the following commutes:
%                   phi*1                 phi
%   (FRX* FRY)*FRZ -------> F(RX*RY)*FRZ -------> F((RX*RY)*RZ)
%          |                                          |
%    alpha |                                          | F(alpha)
%          |                                          |
%          v        1*phi                 phi         v
%   FRX*(FRY*FRZ) -------> FRX*F(RY*RZ) -------> F(RX*(RY*RZ))
\begin{center}\setlength{\unitlength}{1.1pt}\begin{picture}(340,70)
\put(105,60){$\phi\otimes 1$} \put(230,60){$\phi$}
\put(0,50){$(FRX\otimes FRY)\otimes FRZ$}\put(105,53){\vector(1,0){20}}
    \put(130,50){$F(RX\otimes RY)\otimes FRZ$}
    \put(225,53){\vector(1,0){20}}
    \put(250,50){$F\bigl((RX \otimes RY) \otimes RZ\bigr)$}
\put(45,28){$\alpha$}\put(55,47){\vector(0,-1){35}}
\put(285,47){\vector(0,-1){35}}\put(290,28){$F\alpha$}
\put(105,10){$1 \otimes \phi$} \put(230,10){$\phi$}
\put(0,0){$FRX\otimes(FRY\otimes FRZ)$}\put(105,3){\vector(1,0){20}}
    \put(130,0){$FRX\otimes F(RY\otimes RZ)$}
    \put(225,3){\vector(1,0){20}}
    \put(250,0){$F\bigl(RX \otimes(RY \otimes RZ)\bigr)$}
\end{picture}\end{center}
Rearrange to obtain the equation
\alpha (\phi^{-1}\otimes 1) \phi^{-1} = (1\otimes \phi^{-1})\phi^{-1} F\alpha.
Compose both sides of the equation
with $\epsilon\otimes(\epsilon\otimes\epsilon)$.  Then the
left hand side of the new equation is:
\begin{eqnarray*}
\lefteqn{
\bigl(\epsilon\otimes(\epsilon\otimes\epsilon)\bigr)\alpha (\phi^{-1}\otimes 1)\phi^{-1}}\\
&=& \alpha (\psi^\flat \otimes \epsilon) \phi^{-1}\\
&=& \alpha ((\epsilon(F\psi)) \otimes \epsilon) \phi^{-1}\\
&=& \alpha (\epsilon\otimes\epsilon) \phi^{-1} F(\psi\otimes 1)\\
&=& \alpha \psi^\flat F(\psi\otimes 1)
\end{eqnarray*}
The right side of the new equation is
\begin{eqnarray*}
\lefteqn{\bigl(\epsilon\otimes(\epsilon\otimes\epsilon)\bigr) (1\otimes\phi^{-1}) \phi^{-1} (F\alpha)}\\
&=& (\epsilon \otimes \psi^\flat) \phi^{-1} (F\alpha)\\
&=& \bigl(\epsilon\otimes\bigl(\epsilon(F\psi)\bigr)\bigr)\phi^{-1}(F\alpha)\\
&=& (\epsilon\otimes\epsilon)\phi^{-1} F(1\otimes \psi) (F\alpha)\\
&=& \psi^\flat F(1\otimes \psi) (F\alpha)
\end{eqnarray*}
Apply $\sharp$ to both sides of the new equation and
simplify using the properties of $\sharp$ to obtain the required condition
$$ (R\alpha) \psi (\psi\otimes 1) =
    \psi (1\otimes \psi) \alpha.
\end{proof}
\begin{lemma}
Let $R:\C\to \A$ be a right adjoint of $F$, considered as monoidal
functor as described in the previous lemma.
Under the conditions of the theorem $F\darrow G$ and $1_\A \darrow RG$
are isomorphic monoidal categories.
\end{lemma}
\begin{proof}
To each object $FA \arrow{f} GB$ associate the corresponding object
$A \arrow{f^\sharp} RGB$.  It is straightforward to show that this
correspondence can be extended to an isomorphism of categories.
Now we show that the tensor product of the two categories coincide.
Let $\gamma$ be the natural transformation $GB_1 \otimes GB_2 \to
G(B_1\otimes B_2)$.  Let $\phi$ be the natural isomorphism $FA_1 \otimes
FA_2 \to F(A_1 \otimes A_2)$.  Denote the corresponding transformation for
$R$ by $\psi$, recalling that
$\psi=((\epsilon\otimes\epsilon)\phi^{-1})^\sharp$.  Hence, the
transformation for the composite functor $RG$ is $(R\gamma)\psi$.
Consider two objects, $FA_1 \arrow{f_1} GB_1$ and $FA_2 \arrow{f_2} GB_2$.
Applying $\sharp$ and then taking the tensor product in $1\darrow RG$
results in the composite arrow
A_1\otimes A_2\arrow{f_1^\sharp \otimes f_2^\sharp} RGB_1 \otimes RGB_2
    \arrow{(R\gamma)\psi} RG(B_1 \otimes B_2).
We want to show that this arrow is identical to the result of first
taking tensor product in $F\darrow G$ and then applying $\sharp$,
namely
    (\gamma (f_1 \otimes f_2) \phi^{-1})^\sharp.
But we have
\begin{array}{ll}
(R\gamma)\psi(f_1^\sharp \otimes f_2^\sharp)\\
= (R\gamma) ((\epsilon \otimes \epsilon) \phi^{-1})^\sharp (f_1^\sharp \otimes f_2^\sharp) & \mbox{definition of $\psi$}\\
= \bigl(\gamma (\epsilon \otimes \epsilon) \phi^{-1} F(f_1^\sharp \otimes f_2^\sharp)\bigr)^\sharp & \mbox{properties of $\sharp$}\\
= \bigl(\gamma (\epsilon \otimes \epsilon) (F(f_1^\sharp) \otimes F(f_2^\sharp)) \phi^{-1} \bigr)^\sharp & \mbox{$\phi$ is natural}\\
= \bigl(\gamma (\epsilon F(f_1^\sharp) \otimes \epsilon F(f_2^\sharp)) \phi^{-1} \bigr)^\sharp \\
= \bigl(\gamma (f_1 \otimes f_2) \phi^{-1}\bigr)^\sharp,\\
\end{array}
as required.
\end{proof}
We now turn to the final lemma.
\begin{lemma}
Let $\A$ and $\B$ be closed monoidal categories, and $H:\A\to\B$ be a
monoidal functor.  Suppose that $\A$ has pullbacks.  Then the monoidal
category $1_\A\darrow H$ is closed.
\end{lemma}
\begin{proof}
Denote the natural transformation $HB_1 \otimes HB_2 \to H(B_1 \otimes
B_2)$ by $\gamma$.
Let $\<A_1,f_1, B_1>$ and $\<A_2,f_2, B_2>$  be two objects of $1 \darrow H$.
We show that
tensor product has a right adjoint by constructing an object universal from the
functor $\<A_1,f_1, B_1> \otimes -$ to $\<A_2,f_2, B_2>$.
Consider the pullback
%                           pi2
%           X -------------------------------> H[B1,B2]
%           | |                                |
%           |--                                | (He gamma)#
%           |                                  v
%       pi1 |                               [HB1, HB2]
%           |                                  |
%           |                                  | [f1, 1]
%           v              [1,f2]              v
%         [A1, A2] -----------------------> [A1, HB2]
\begin{center}\setlength{\unitlength}{1.1pt}\begin{picture}(200,100)
\put(80,90){$\pi_2$}
\put(15,80){$X$}\put(25,82){\vector(1,0){95}}\put(125,80){$H[B_1,B_2]$}
\put(10,40){$\pi_1$}\put(20,78){\vector(0,-1){65}}
\put(145,75){\vector(0,-1){26}}\put(150,60){$((H\epsilon)\gamma)^\sharp$}
\put(125,40){$[HB_1,HB_2]$}
\put(145,35){\vector(0,-1){26}}\put(150,20){$[f_1,1]$}
\put(70,10){$[1,f_2]$}
\put(0,0){$[A_1,A_2]$}\put(35,5){\vector(1,0){85}}\put(125,0){$[A_1,HB_2]$}
\end{picture}\end{center}
We will show that the top line of this diagram is the required universal
object.  Firstly, we claim that the universal arrow to $\<A_2,f_2,B_2>$ is
given by
%                f1*pi2                 gamma
%        A1 * X -------> HB1 * H[B1,B2]-------> H(B1 * [B1,B2])
%           |                                      |
%           |                                      |
%     pi1 b |                                      | He
%           |                                      |
%           v                f2                    v
%           A2 ---------------------------------> HB2
\begin{center}\setlength{\unitlength}{1.1pt}\begin{picture}(250,80)
\put(40,70){$f_1\otimes\pi_2$}\put(165,70){$\gamma$}
\put(0,60){$A_1\otimes X$}\put(40,62){\vector(1,0){30}}
    \put(75,60){$HB_1\otimes H[B_1,B_2]$}\put(155,62){\vector(1,0){30}}
    \put(190,60){$H(B_1 \otimes [B_1,B_2])$}
\put(0,30){$\pi_1^\flat$}\put(15,58){\vector(0,-1){45}}
\put(225,58){\vector(0,-1){45}}\put(230,30){$H\epsilon$}
\put(120,6){$f_2$}
\put(10,0){$A_2$}\put(25,3){\vector(1,0){190}}\put(215,0){$HB_2$}
\end{picture}\end{center}
To see that this square commutes, apply $\flat$ to both directions around
the pullback square.  It is immediate that $([1,f_2] \pi_1)^\flat$ equals
$(f_2\pi_1^\flat)$.  For the other direction, observe from standard
properties of adjunctions that $[f_1,1] = (\epsilon(f_1 \otimes 1))^\sharp$.
Hence,
\begin{eqnarray*}
\lefteqn{ \bigl([f_1,1]((H\epsilon) \gamma)^\sharp \pi_2\bigr)^\flat}\\
&=& [f_1,1]^\flat (1\otimes ((H\epsilon)\gamma)^\sharp)(1\otimes \pi_2)\\
&=& \epsilon (1\otimes ((H\epsilon)\gamma)^\sharp)(f_1\otimes \pi_2)\\
&=& (H\epsilon) \gamma (f_1\otimes \pi_2),
\end{eqnarray*}
as required.
Suppose now that there exists a commuting square
%                f1*g              gamma
%        A1 * Y -------> HB1 * HC -------> H(B1 * C)
%           |                                   |
%           |                                   |
%         p |                                   | Hq
%           |                                   |
%           v                f2                 v
%           A2 ------------------------------> HB2
\begin{center}\setlength{\unitlength}{1.1pt}\begin{picture}(250,80)
\put(40,70){$f_1\otimes g$}\put(140,70){$\gamma$}
\put(0,60){$A_1\otimes Y$}\put(40,62){\vector(1,0){30}}
    \put(75,60){$HB_1\otimes HC$}\put(130,62){\vector(1,0){30}}
    \put(165,60){$H(B_1 \otimes C)$}
\put(0,30){$p$}\put(15,58){\vector(0,-1){45}}
\put(190,58){\vector(0,-1){45}}\put(195,30){$Hq$}
\put(90,6){$f_2$}
\put(10,0){$A_2$}\put(25,3){\vector(1,0){150}}\put(180,0){$HB_2$}
\end{picture}\end{center}
$\B$ is closed, so $q$ can be factored into
$\epsilon(1\otimes q^\sharp)$.  By the naturality of
$\gamma$, $\bigl(H(1\otimes q^\sharp)\bigr) \gamma$ is equal to
$\gamma (1 \otimes Hq^\sharp)$, so we obtain
    f_2p = (H\epsilon)\gamma \bigl(f_1\otimes(Hq^\sharp) g\bigr).
Applying $\sharp$ to both sides of this equation shows that the following
square commutes.
%                    g              Hq#
%           Y -------------> HC--------------> H[B1,B2]
%           |                                  |
%           |                                  | (f1*1)#
%           |                                  v
%         p#|                               [A1,HB1*H[B1,B2]]
%           |                                  |
%           |                                  | [1, (He) gamma]
%           v              [1,f2]              v
%         [A1, A2] -----------------------> [A1, HB2]
\begin{center}\setlength{\unitlength}{1.1pt}\begin{picture}(250,100)
\put(30,90){$g$}\put(85,90){$H(q^\sharp)$}
\put(15,80){$Y$}\put(25,82){\vector(1,0){25}}\put(55,80){$HC$}
    \put(70,82){\vector(1,0){35}}\put(110,80){$H[B_1,B_2]$}
\put(10,40){$p^\sharp$}\put(20,78){\vector(0,-1){65}}
\put(145,78){\vector(0,-1){26}}\put(150,60){$(f_1\otimes 1)^\sharp$}
\put(125,40){$[A_1,HB_1\otimes H[B_1,B_2]$}
\put(145,38){\vector(0,-1){26}}\put(150,20){$[1,(H\epsilon)\gamma]$}
\put(70,10){$[1,f_2]$}
\put(0,0){$[A_1,A_2]$}\put(30,5){\vector(1,0){90}}\put(125,0){$[A_1,HB_2]$}
\end{picture}\end{center}
Consider the right side of this square.  Observe that
    [1,(H\epsilon)\gamma](f_1\otimes 1)^\sharp
        = ((H\epsilon)\gamma(f_1 \otimes 1))^\sharp.
Now consider the right side of the pullback square
that defines $X$.
\begin{eqnarray*}
[f_1,1] ((H\epsilon)\gamma)^\sharp
    &=& (\epsilon(f_1\otimes 1))^\sharp ((H\epsilon)\gamma)^\sharp\\
    &=& (\epsilon(f_1\otimes 1)(1\otimes ((H\epsilon)\gamma)^\sharp))^\sharp\\
    &=& (\epsilon(1\otimes((H\epsilon)\gamma)^\sharp)(f_1\otimes 1))^\sharp\\
    &=& ((H\epsilon)\gamma(f_1\otimes 1))^\sharp
\end{eqnarray*}
So we know that the right arrow of this square is the same as the right
arrow of the pullback square defining $X$.  But then there must exist a
unique map $r:Y\to X$ such that $\pi_2 s = (Gq^\sharp) g$ and $\pi_1 s =
p^\sharp$.  The first equation is precisely the condition that
$\<s,q^\sharp>$ be a well-defined map from $\<Y,g,C>$ to
$\<X,\pi_2,[B_1,B_2]>$.  The second shows that $\<s,q^\sharp>$ factors the
original map $\<p,q>$ through the counit of the adjunction.  Uniqueness
follows from the unique factorization of $q$ through $\epsilon$ and
properties of pullbacks.
\end{proof}
A fine example related to this construction is provided by the
partially ordered multisets motivating this work.  A pomset
$p=\<P,\mu,\Sigma>$ is just a poset $P$, labeled by a function
$\mu:V(P)\to\Sigma$ for some set $\Sigma$.  This makes it an object of
$\Pom=\Pos\comma\Set$.  A morphism of pomsets
$f:\<P,\mu,\Sigma>\to\<P',\mu',\Sigma'>$ consists of a monotone event
map $f:P\to P'$ on the underlying posets together with an alphabet map
or {\it translation} $t:\Sigma\to\Sigma'$ from $\Sigma$ to $\Sigma'$,
such that $t\mu=\mu'f$ (i.e., the event map and translation are
consistent with respect to the labelings). We can view $\Pom$ as the
full subcategory of $\Prom = 2! \comma {\bf Set}$, the latter generalizing
the notion of pomsets by allowing $P$ to be a preorder.
%In this paper, since the construction that we emphasize is $\D
%\comma\E$, we are interested only in labels drawn from sets.
%When more elaborately structured label sources are needed, as for the
%category $\Pos\comma{\two}$ of order ideals, the comma must be taken
%over the appropriate common denominator, here \Pos\ (so that an order
%ideal is a triple $\<P,f,\two>$ for $f:P\to\two$ monotone).  Many of
%the principles developed in this paper transcend this choice of
%denominator; fixing it at \Set\ helps fix ideas.
\section{Abstract Specification of the Operations}
Having established the categorical framework for our abstract treatment
of time, we now define the operations of our algebras of behaviors.
The sense in which time is abstract is that a fixed category $\D$ of
spaces is assumed to be given as a parameter.  The definitions may
therefore refer to $\D$, but will not assume that $\D$ has any a priori
structure such as labels on points or a metric between points.  Each
choice of $\D$ determines an algebra of behaviors, really a class of
behaviors since we impose no cardinality bounds on the number of events
in a behavior, other than the requirement that the events of a behavior
form a set.
Most operations are of arity a small integer.  On occasion however,
e.g. when certain arguments are required to have the same domain or the
same codomain, the arity will be a graph, meaning that the arguments
will be organized as a functor from that graph.  For example if the
arity is the 3-vertex 2-edge graph of shape $<$ (two edges pointing to
the right) then the arguments are two morphisms with a common domain.
This is made uniform by regarding each integer arity $n$ as a discrete
(edge-less) graph with vertices 1 through $n$.
{\it Disjoint Concurrence,} {\tt dconcur}$(p,q)$, notation $p+q$.  The
{\it disjoint concurrence} of behaviors $p$ and $q$ performs both $p$
and $q$ {\it concurrently}, that is, unconstrained in time.  It is
defined as the coproduct $p+q$ in $\D$.
{\it Disjoint Concatenation,} {\tt dconcat}$(p,d,q)$, notation
$p;^dq$.  The {\it disjoint concatenation} of behaviors $p$ and $q$
{\it with delay} $d$ performs both $p$ and $q$ as in disjoint
concurrence, but in the order $p$, then a delay $d:I+I\to d_0$, then $q$.
It is defined by the pushout
$$\commdiag{
    (I+I)\otimes (p\times q)   & \rTo{\pi_p+\pi_q}{} & p+q      \cr
    \dTo{d\otimes 1}{}         &                    & \dTo{}{} \cr
    d_0\otimes (p\times q)     & \rTo{}{}           & p;^dq
where the top morphism is the sum $\pi_p+\pi_q:p\times q+p\times q\to
p+q$ of the two projections $\pi_p:p\times q\to p$ and $\pi_q:p\times
q\to q$ from $p\times q$, and $(I+I)\otimes r\cong I\otimes r+I\otimes
r\cong r+r$.
{\it Concurrence,} {\tt concur}$(p\to k\leftarrow q)$, notation
$p||_kq$, or $p||q$ when $k$ is supplied by context.  The {concurrence}
of behaviors $p$ and $q$ {\it over} $k$ performs both $p$ and $q$
concurrently, {\it coordinated by} $k$.  It is defined as the coproduct
of the morphisms $p\to k$ and $q\to k$ in $\D/k$, the comma or slice
category of morphisms to $k$ (``objects over'' $k$), itself a morphism
to $k$ and thus retaining the coordination.
{\it Concatenation,} {\tt concat}$((p,d,q)\to k)$, notation $p;^d_k
q$.  The {\it concatenation} of $p$ with $q$ performs both $p$ and $q$
concurrently, {\it coordinated by} $k$, but in the order $p$, then a
delay $d$, then $q$.  It is defined as for disjoint concatenation, with
the pushout formed in $\D/k$.
{\it Local disjoint concatenation,} {\tt ldconcat}$(d,p\to L\leftarrow
q)$, notation $p\lc^d_Lq$.  The {\it local disjoint concatenation} of
behaviors $p$ and $q$ with delay $d$ performs $p$ and $q$ concurrently
except that events of $p$ at a given location must be followed by a
delay $d:(I+I)\to d_0$ before performing events of $q$ at that location.
It is defined analogously to disjoint concatenation via the pushout
$$\commdiag{
    (I+I)\otimes(p\times_L q) & \rTo{(\pi_p+\pi_q)\circ L_=}{} & p+q \cr
    \dTo{d\otimes 1}{}        &                        & \dTo{}{} \cr
    d_0\otimes(p\times_L q)   & \rTo{}{}               & p\lc^d_Lq
where $L_=:p\times_L q\to p\times q$ is the standard embedding, namely
the equalizer $L_p\circ\pi_p$ and $L_q\circ\pi_q$, and the rest is as
for disjoint concatenation.
{\it Local concatenation,} $p\lc^d_{kL}q$, is the appropriate
combination of concatenation and local disjoint concatenation.
{\it Orthocurrence,} {\tt orthocur}$(p,q)$, notation $p\otimes q$.  The
{\it orthocurrence} of behaviors $p$ and $q$ consists of the flow of
$p$ and $q$ past each other.  It is defined as their tensor product
$p\otimes q$.
{\it Unit,} {\tt unit}, notation $I$.  The {\it unit} is a one-event
behavior that flows by unnoticed.  It is defined as the unit $I$ of
$\D$, being the unit for orthocurrence.
{\it Observation,} {\tt observe}$(q,r)$, notation $r^q$.  The {\it
observation} of behavior $q$ by behavior $r$ is the result of observing
every stage of every event of $q$, where the stages of an event of $q$
are defined as the events of $r$.  It is defined by the adjunction
$p\otimes q\to r\cong p\to r^q$, that is, ${-}^q$ is right adjoint to
${-}\otimes q$.
{\it Product,} {\tt product}$(p,q)$, notation $p\times q$.  The {\it
product} of behaviors $p$ and $q$ consists of all pairs $(a,b)$ of
constituents $a$ of $p$ and $b$ of $q$, with all the structure of $p$
and $q$ preserved coordinatewise.  It is defined as their ordinary
(categorical) product $p\times q$.
{\it Local product,} {\tt lproduct}$(p\to L\leftarrow q)$, notation
$p\times_L q$.  The {\it local product} of behaviors $p$ and $q$
consists of all pairs $(a,b)$ such that $a$ and $b$ are $L$-colocated
(conceptually, at the same location $l\in L$).  It is defined as the
pullback
$$\commdiag{
        p\times_L q &   \rTo{}{}   &    q     \cr
          \dTo{}{}  &         & \dTo{}{} \cr
            p       &   \rTo{}{}   &    L
\section{The Kind Language KL}\label{sec:langs}
The kind language KL consists of terms naming certain kinds in $\SSM$.
A KL term is either a constant denoting one of the ground kinds
$\one,\two,\three,\three',$ $\R$, $\R\op$, and $\SR$, or a compound
term $\D!$ or $\D\rhd\E$ where $\D$ and $\E$ are KL terms.
We make each ground kind semiconcrete by setting its underlying set
functor $U$ to 0 at 0 and 1 elsewhere.  The one exception is $\one$,
where $U(0)=1$, since $0=1$ in $\one$.
Some terms in this language are neither useful nor well-behaved, for
example $\two\rhd\one!$, which denotes a category that is not closed.
A {\it safe} term is defined by induction to be either a ground term, a
term $\D!$ where $\D$ is safe, or a term $\D!\rhd\E$ where $\D$ and
$\E$ are safe.  We then take a KL {\it kind} to be the denotation in
$\SSM$ of a safe KL term.
%***** Check that the definition of cosmon includes the requirement
%that forgetful functors have left adjoints in all cases (not just
%base cases).
%\begin{proof}
%Base categories are complete by fiat.  If $\D$ is complete, so is $\D!$.
%If $\D$ and $\E$ are complete then $\D\rhd\E$ must be complete because
%$U_\E$ has a left adjoint and so preserves all limits.
%\end{proof}
\begin{theorem}\label{thm:safemeansclosed}
Every safe KL kind is closed and bicomplete.
\end{theorem}
\begin{proof} This follows by induction on the structure of terms of
KL.  For the base case, ground kinds are closed and cocomplete by
definition.  For compound safe terms the theorem follows by induction
from Theorems 7, 8, 9, and 11, Corollary 12, Theorem 13, and the fact
that the forgetful functors of the basic kinds and those constructed by
! and $\comma$ have the necessary continuity properties and adjoints.
\end{proof}
KL kinds include $\one!$ = sets, $\one\comma\one!$ = pointed sets,
$\two!$ = preordered sets, $\one!\comma\one!$ = multisets,
$\two!\comma\one!$ = ordered multisets, $\one!!$ = categories, $\two!!$
= order-enriched categories, $\one!!!$ = 2-categories, $\three!$ =
causal spaces, $\three'!\comma\one!$ = prossets, and $\R\op!$ =
premetric spaces.  It should be straightforward to verify these
correspondences from what has been said thus far about the ground kinds
and the operations.
This language provides a succinct system of names for a usefully broad
range of categories of datatypes.  It suffices to name such a category
$\D$ to be assured of the presence of all operations definable by
universal constructions (limits, colimits, adjunctions, etc.) from the
monoidal category structure of $\D$.
\section{Conclusion}
\subsection{Directions For Further Work}
\def\Hom{\hbox{\rm Hom}}
We mention briefly some projects we have in mind.
{\it Working over $\Cat$.}  Our techniques would appear to extend
straightforwardly to monoidal 2-categories, where the forgetful
functors are not to $\Set$ but to $\Cat$.  This turns the labeling
function from the underlying set of a behavior to (the underlying set
of) an alphabet into a labeling {\it functor}.  Its functoriality can
be put to good use, as in conveniently naming the closed category of
order ideals.
{\it Extensions to KL.}  Currently, methods for specifying subkinds of
dynamic kinds are somewhat ad hoc, e.g., posets are acyclic
\two-categories.  It would be useful to have operators that would
produce subkinds for a wide variety of {\D}, such as a single approach
to producing partial orders (as opposed to preorders) and say symmetric
metric spaces.
It would also be useful to have operators for constructing new metrics.
Indeed the present supply of metrics has been constructed ad hoc.  Some
uniform way of constructing them would be useful.
Such operators would be additions to the kind language KL.  The only
operations we have admitted thus far to KL are ! and $\comma$.  We do
not however intend by any means that these be all.  To fit in with !
and $\comma$ however these operations would need similar continuity
properties.
{\it Stochastic delay.}  Another possible choice for {\D} is that of a
category of probability distributions.  In other words for each pair of
events $u,v$ we specify a probability density function $\rho_{uv}:{\bf
R}\to[0,1]$ for the associated delay.  Consecutive delays would be
combined using convolution
$$\rho_{uv}\otimes\rho_{vw}(y)=\int_{-\infty}^{\infty}\rho_{uv}(x)\rho_{vw}(y-x)dxdy$$
The main problems include finding a suitable ordering on
distributions and dealing with the fact that the various
distributions on delays are not independent.  There is also the
question of the proper treatment of distributions which are not well
behaved and continuous (e.g., the Dirac delta function).
\subsection{Summary}
We have described a model of concurrency consisting of two orthogonal
parts, one dealing with kinds of behaviors, the other with the
behaviors themselves.
Kinds are taken to be semiconcrete monoidal categories, objects of
$\SSM$.  A ``kind language'' KL is provided for naming a few basic
kinds and combining them with operations ! and $\comma$ to form
compound kinds.  The !  operation turns a metric into a category of
spaces with that metric.  The $\comma$ operation combines two kinds by
using one as a source of structures and the other as a source of
alphabets with which those structures may be labeled.  Kinds namable in
this way are called KL kinds.
Behaviors are taken to be objects of a given kind $\D$ an object of
$\SSM$.  A ``behavior language'' PSL is provided for naming basic
behaviors and combining them with a useful library of operations
suitable for concurrent programming. Although typical behaviors contain
much structure, including a metric and a labeling function, this is
{\it only} typical and not required.  In general nothing is assumed
about the ``internal'' structure of a behavior, which may well be just
a simple atomic value.  We are however given operations for assembling
behaviors to form larger behaviors, namely limits, colimits, and a
tensor product.  These operations belong to the language PSL.
PSL is thus a true algebra of behaviors.  Even though the PSL
operations are defined uniformly across the spectrum of KL kinds, their
action on complex KL kinds would appear to be as useful as if PSL had
been defined to operate explicitly on spaces with metrics and labeling
functions.  Yet the meaning of PSL is defined no differently for
``atomic'' behaviors than for behaviors with complex structures.  Thus
PSL acts as an algebra of behaviors in assuming no structure within its
elements yet being able to recreate that internal structure ``from
outside.''
The division of labor between KL and PSL is completely orthogonal.
``Motion'' via functors of $\SSM$, from which KL operations are drawn,
has no influence on the point sets of spaces and individual alphabets
making up any given object $\D$ of $\SSM$.  This independence finds its
expression in the identity $U=U'F$ relating underlying sets, which says
that underlying sets of points and functions between them pass through
$F$ completely unscathed.  Conversely, motion via functors of $\D$,
from which PSL operations are drawn, takes place relative to a fixed
$\D$ and hence has no influence on the metrics and alphabet kinds
making up $\SSM$.
That PSL operates on the ``individuals''---objects and arrows---of a
fixed $\D$ gives it the character of a first order language.  Since
formation of $\D$-functor spaces is an operation of PSL, the proper
analogy is with ZF as a first order theory, where sets of individuals
are also individuals.  That is, ZF and PSL are both ``internally
closed,'' both by virtue of working in a closed universe.
Unlike ZF however, which operates in the cartesian closed universe of
sets, PSL operates in a closed universe that is not presumed to be
cartesian closed, whence the need to distinguish between tensor product
$\otimes$ and ordinary product $\times$ in PSL.
This distinction arises in a natural and inevitable way from an
elementary and familiar observation: {\it the temporal accumulation
operator need not be product}.  That it is product (conjunction) in the
two-valued metric logic underlying ordered time is not a necessary
facet of the logic of time.
A recent noncartesian logic is Girard's linear logic \cite{Gir87}.
Like PSL, linear logic distinguishes ordinary and tensor product.  Like
Boolean logic but unlike PSL, Girard's linear logic is self-dual,
giving rise by de Morgan's law to two binary operations dual to the two
products.  This prompts the following question.
\begin{quotation}
{\em Why should self-duality survive the diverging of the two products?}
\end{quotation}
To bring the concepts of PSL together we have drawn heavily on some
basic techniques that have evolved in category theory within the past
three decades, most notably those of closed categories and enriched
categories.  These techniques in the dry context of a mathematics text
can seem dauntingly abstract.  But just as there are good and bad
cholesterols so it is with abstractions: the bad daunt and the good
clarify.  In adapting these techniques to computing practice we have
tried to leave the good abstractions intact, namely those that
simplified matters or seemed to bear on computation.
One defect of our account is that it has put relatively little emphasis
on the logical character of PSL.  The adjunctions and compositions
pervading our framework contain all the essential elements of a modern
logic, yet we have not made this logical character as explicit as we
might.  This may just be a reflection of the algebraic perspective
which nurtured this work.  We hope that the proper balance of algebra
and logic here will become clear in due course.
\section*{Acknowledgments}
We are indebted to F.W. Lawvere both for his paper \cite{Law}
clarifying the topic of enriched categories and for much helpful
advice.  We also appreciate the help we have received from the Sydney
Category Seminar, especially A.J. Power and R.F.C. Walters.  The paper
was typeset using D. Knuth's TeX, L. Lamport's LaTeX macros, and P.
Taylor's diagram macros.
\bibliographystyle{alpha}
\begin{thebibliography}{CCMP91}
\bibitem[AHU74]{AHU}
A.V. Aho, J.~E. Hopcroft, and J.D. Ullman.
\newblock {\em The Design and Analysis of Computer Algorithms}.
\newblock Addison-Wesley, Reading, Mass, 1974.
\bibitem[AM75]{AM}
M.~Arbib and E.~Manes.
\newblock {\em Arrows, Structures, and Functors: The Categorical Imperative}.
\newblock Academic Press, 1975.
\bibitem[BCSW83]{BCSW}
R.~Betti, A.~Carboni, R.~Street, and R.~Walters.
\newblock Variation through enrichment.
\newblock {\em J. Pure and Applied Algebra}, 29:109--127, 1983.
\bibitem[Bir37]{Birk37}
G.~Birkhoff.
\newblock An extended arithmetic.
\newblock {\em Duke Mathematical Journal}, 3(2), June 1937.
\bibitem[Bir42]{Birk42}
G.~Birkhoff.
\newblock Generalized arithmetic.
\newblock {\em Duke Mathematical Journal}, 9(2), June 1942.
\bibitem[CCMP91]{CCMP}
R.T Casley, R.F. Crew, J.~Meseguer, and V.R. Pratt.
\newblock Temporal structures.
\newblock {\em Math. Structures in Comp. Sci.}, 1(2):179--213, July 1991.
\bibitem[Con71]{Con}
J.H. Conway.
\newblock {\em Regular Algebra and Finite Machines}.
\newblock Chapman and Hall, London, 1971.
\bibitem[EK65]{EK66a}
Samuel Eilenberg and G.~Max Kelly.
\newblock Closed categories.
\newblock In S.~Eilenberg, D.~K. Harrison, S.~MacLane, and H.~R{\"o}hrl,
  editors, {\em Proceedings of the Conference on Categorical Algebra, La Jolla,
  1965}, pages 421--562. Springer-Verlag, 1965.
\bibitem[Flo62]{Flo62}
R.W. Floyd.
\newblock Algorithm 97: shortest path.
\newblock {\em Communications of the ACM}, 5(6):345, 1962.
\bibitem[Gai89]{Ga89}
H.~Gaifman.
\newblock Modeling concurrency by partial orders and nonlinear transition
  systems.
\newblock In {\em Proc. REX School/Workshop on Linear Time, Branching Time and
  Partial Order in Logics and Models for Concurrency}, pages 467--488,
  Noordwijkerhout, The Netherlands, 1989. Springer-Verlag.
\bibitem[Gir87]{Gir87}
J.-Y. Girard.
\newblock Linear logic.
\newblock {\em Theoretical Computer Science}, 50:1--102, 1987.
\bibitem[GP87]{GP}
H.~Gaifman and V.R. Pratt.
\newblock Partial order models of concurrency and the computation of functions.
\newblock In {\em Proc. 2nd Annual IEEE Symp. on Logic in Computer Science},
  pages 72--85, Ithaca, NY, June 1987.
\bibitem[Kel82]{Kel}
G.M. Kelly.
\newblock {\em Basic Concepts of Enriched Category Theory: London Math. Soc.
  Lecture Notes}.
\newblock 64. Cambridge University Press, 1982.
\bibitem[Koz80]{Koz80b}
D.~Kozen.
\newblock A representation theorem for models of *-free {PDL}.
\newblock In {\em Proc. 7th Colloq. on Automata, Languages, and Programming},
  pages 351--362, July 1980.
\bibitem[Koz81]{Koz81a}
D.~Kozen.
\newblock On induction vs. *-continuity.
\newblock In D.~Kozen, editor, {\em Proc. Workshop on Logics of Programs 1981,
  LNCS 131}, pages 167--176. Spring-Verlag, 1981.
\bibitem[Law73]{Law}
W.~Lawvere.
\newblock Metric spaces, generalized logic, and closed categories.
\newblock In {\em Rendiconti del Seminario Matematico e Fisico di Milano,
  XLIII}. Tipografia Fusi, Pavia, 1973.
\bibitem[Lew90]{Lew90}
H.~Lewis.
\newblock A logic of concrete time intervals.
\newblock In {\em Proc. 5th Annual IEEE Symp. on Logic in Computer Science},
  Philadelphia, July 1990.
\bibitem[Mac71]{Mac}
S.~Mac{ }Lane.
\newblock {\em Categories for the Working Mathematician}.
\newblock Springer-Verlag, 1971.
\bibitem[Pra84]{Pr84}
V.R. Pratt.
\newblock The pomset model of parallel processes: {Unifying} the temporal and
  the spatial.
\newblock In {\em Proc. CMU/SERC Workshop on Analysis of Concurrency, LNCS
  197}, pages 180--196, Pittsburgh, 1984. Springer-Verlag.
\bibitem[Pra86]{Pr86}
V.R. Pratt.
\newblock Modeling concurrency with partial orders.
\newblock {\em Int. J. of Parallel Programming}, 15(1):33--71, February 1986.
\bibitem[Pra89]{Pr89a}
V.R. Pratt.
\newblock Enriched categories and the {Floyd-Warshall} connection.
\newblock In {\em Proc. First International Conference on Algebraic Methodology
  and Software Technology}, pages 177--180, Iowa City, May 1989.
\bibitem[RF68]{RF}
P.~Robert and J.~Ferland.
\newblock G\'en\'eralisation de l'algorithme de {W}arshall.
\newblock {\em Revue francaise d'Informatique et de Recherche Operationnelle},
  2(7):13--25, 1968.
\bibitem[Roy59]{Roy59}
B.~Roy.
\newblock Transitivit\'e et connexit\'e.
\newblock {\em Comptes Rendues Acad. Sci.}, 249:216--218, 1959.
\bibitem[Tar85]{Tar85}
Andrzej Tarlecki.
\newblock Bits and pieces of the theory of institutions.
\newblock In {\em Category Theory and Computer Programming}, Lecture Notes in
  Computer Science~240, pages 334--363, Guildford, UK, 1985. Springer-Verlag.
\bibitem[Vic89]{Vic89}
S.~Vickers.
\newblock {\em Topology via Logic}.
\newblock Cambridge University Press, 1989.
\bibitem[War62]{War62}
S.~Warshall.
\newblock A theorem on {B}oolean matrices.
\newblock {\em Journal of the ACM}, 9(1):11--12, 1962.
\end{thebibliography}
\end{document}