The original purpose of component-based development was to provide techniques to master complex software, through composition, reuse, and parametrisation. However, such systems are rapidly moving towards a level in which they become prevalently intertwined with (continuous) physical processes. A possible way to accommodate the latter in component calculi relies on a suitable encoding of continuous behaviour as (yet another) computational effect. This paper reports such an encoding through a monad which, in the compositional development of hybrid systems, may play a role similar to the one played by the maybe, powerset, and distribution monads in the characterisation of partial, non deterministic and probabilistic components, respectively.
Component-based software development is often explained through a visual metaphor: a palette of computational units, and a blank canvas in which they are dropped and interconnected by drawing wires abstracting different composition and synchronisation mechanisms. More and more, however, components are not limited to traditional information processing units, but encapsulate some form of interaction with physical processes. The resulting systems, referred to as hybrid, exhibit a complex dynamics in which loci of computation, coordination, and control of physical processes interact, become mutually constrained, and cooperate to achieve specific goals.
One way of looking at components, proposed in [
This paper summarises a number of results developed in the context of the
author’s PhD project [
Related work. A few categorial models for hybrid systems have been proposed.
For example, document [
The monad reported in this paper captures the typical continuous behaviour
of hybrid systems. Actually, there is a close relationship between the work
reported here and Peter H o¨fner’s algebra of hybrid systems [
Since our approach, differently from Ho¨ fner’s calculus, is structured around a monad that encodes continuous evolution, a number of canonical constructions come for free. Moreover, the integration with other behavioural effects, such as non determinism or probabilistic evolution, becomes more systematic. Roadmap. After a brief detour on preliminaries and notation in Section 2, monad H is described in Section 3. Section 4 gives some details about the corresponding Kleisli category Kl H, characterising composition and some (co)limits. Finally, conclusions and possible future research directions are discussed in Section 5. In this paper many calculations adopt a pointfree style in the spirit of the
2.1 The category of topological spaces
The typical continuous behaviour of hybrid systems suggests the category Top of
topological spaces and continuous functions as a suitable working environment
for developing the aforementioned results. In the sequel, if the context is clear,
a topological space will be denoted just by its underlying set. Also, assume
that spaces X Y , X + Y correspond to the canonical product and coproduct
of X; Y , respectively, and that whenever Y is core-compact, space XY comes
with the exponential topology [
Y )
Z = X (Y
Z) Y = Y
X Y )R0 = XR0
Y R0 2.2
Notation Arrows X ! 1 to the final object in Top will be denoted by !, and a function constantly yielding a value x by x. Given two functions f; g : X ! Y , and a predicate p, conditional expression f C p B g : X ! Y is defined by (f C p B g) x = (f x C p x B g x) = (f x p x g x otherwise The continuous functions minimum f : R (R+1) ! R and truncated subtraction : R (R + 1) ! R play a key role in the sequel. They are defined as follows r f (i1 s) = ( 1 C ( ) B 2) (r; s) r (i1 s) = (( ) C (>) B 0) (r; s) r f (i2 ?) = r r (i2 ?) = 0 where ; > are the usual ordering relations over the reals, and 1 introduces infinity. Set R0 denotes the non–negative real numbers. Then, we have (fd) r = r f d and (d) r = r d. Finally, for any category C, jCj denotes the corresponding class of objects. 3
I ! OR0
D where D = R0 + 1 and I; O are the input and output spaces, respectively. The intuition is that outputs of such systems are continuous evolutions (also known as trajectories) with a specific (possibly infinite) duration d 2 D.
Definition 1 H : Top ! Top is a functor such that, for any objects X; Y 2 jTopj and any continuous function g : X ! Y ,
HX = f (f; d) 2 XR0 Hg = g id
D j f fd = f g where (g ) h = g h. Condition f fd = f tells that function f must become constant after reaching its duration; more formally, for any r 2 R0 such that r > d, f r = f d. Hence, continuous systems become arrows of the type
I ! HO also denoted as I ! O.
The crucial step now is to equip H with a monad structure, i.e. with natural transformations
Definition 2 Given any X 2 jTopj, define X : X ! HX such that : Id ! H;
: HH ! H:
X x = (x; i1 0) in pointfree notation X = h Next, we have f l1 : HHX ! XR0 where f l1 = (ev hg; hi). In pointwise notation, f l1 is defined as f l1(f; d) = ev h 1 f fd; di Then, define function f l2 : H2X ! D such that
f l2 (f; d) = (( 2 f ) d C (d 62 1) B i2 ?) + d Finally, we define for any X 2 jTopj, X = hf l1; f l2i.
Intuitively, operation X ‘concatenates’ functions: given a pair (f; d) 2 HHX,
X concatenates function ( 1 f ) - 0 : [0; d] ! X with ( 1 f ) d - : [0; d0] ! X, and sums the corresponding durations.
R0 ! XR0 , h : HHX Theorem 1 The triple hH; ; i forms a monad.
4 4.1
Kleisli Composition The Kleisli category for H (Kl H) provides an interesting setting to study the requirements placed by continuity over different forms of composition; actually, the envisaged component calculus for hybrid systems is essentially its calculus.
The definition of Kleisli composition in Kl H suggests a relevant distinction between continuous systems. Definition 4 A continuous system c : I ! HI is passive if the following diagram commutes
I
fc / IR0 id
I ev hid;0i where fc = 1 c. It is active otherwise.
Intuitively, the diagram tells that any evolution triggered by c ‘starts’ at the point given as input. To see why such a distinction is relevant, let us consider two continuous systems c1 : I ! HK, c2 : K ! HO. Through Kleisli composition we obtain component c2 c1 : I ! HO whose behaviour is computed as follows: Going pointwise,
f Definition of H ( taking d = ( 2 c1) x ) g = = = = = 1 (c2
c1) x f Kleisli composition g 1
Hc2 c1 x f Cancellation
g f l1 Hc2 c1 x f l1 (c2 (fc1 x); d)
f Application g ev h 1 c2 (fc1 x) fd; di
f Notation g ev hfc2 (fc1 x) fd; di ev hfc2 (fc1 x) fd; di t = = = fc2 fc2 f Application g fc1 x (t f d) (t d) f Notation g f If c2 is passive g fc1 x t 0 C ( t d ) B fc2 fc1 x d (t d) fc1 x t C ( t d ) B fc2 fc1 x d (t d) Assuming that c2 is passive, the last expression tells that given an input i 2 I the resulting evolution corresponds to the evolution of the first component fc1 i ensued by the evolution of the second, which receives as input the ‘last’ point of evolution fc1 i. Therefore, when c2 is passive Kleisli composition may be alternatively called sequential composition or concatenation. On the other hand if c2 is active, Kleisli composition tells that c2 can alter the evolution of c1 and then proceed with its own evolution. This is illustrated in the following examples.
Example 1. Given two signal generators c1; c2 : R ! HR defined as the signal given by c1 (c2
c1) 0 yields the plot below c1 r = (r + sin - ; 3 ); c2 r = (r + sin (3
- ); 3 ) 15 x This type of signal is common in the domain of frequency modulation, where the varying frequency is used to encode information for electromagnetic transmission.
Example 2. Suppose the temperature of a room is to be regulated according to the following discipline: starting at 10 C, seek to reach and maintain 20 C, but in no case surpass 20:5 C. To realise such a system, three components have to work together: c1 to raise the temperature to 20 C, component c2 to maintain a given temperature, and component c3 to ensure the temperature never goes over 20:5 C. Formally, c1 x = ( (x + - ); 20 x ); c2 x = ( x + (sin - ); 1 ); c3 x = ( x C (x 20:5) B 20:5 ; 0 ) One may then compose c2; c1 into c2 c1, which results in a component able to read the current temperature, raise it to 20 C, and then keep it stable, as shown by the plot below on the left. If, however, temperatures over 20:5 C occur, composition c3 c2 c1 puts the system back into the right track as the plot below on the right illustrates. On a different note, for any X 2 jTopj, arrow X is a trivial system in the sense that its evolutions always have duration zero and the only point in the trajectories is the input given. For this reason we will refer to X by copyX , and often omit the subscript. Setting up Kl H yields the following laws copy c1 (c3
c1 = c1 copy = c1 c2) c1 = c3 (c2 c1) (1) (2) (3) 15 x
I1 for any arrows c1; c2; c3 in Kl H. 4.2 (Co)limits and Tensorial Strength (Co)limits are a main tool to build ‘new’ arrows from ‘old’ ones, which in the case of Kl H translates to new forms of (continuous) component composition. One important colimit is the coproduct, which provides the choice operator: Definition 5 Given two components c1 : I1 ! HO, c2 : I2 ! HO component behaves as c1 if input I1 is chosen, and as c2 otherwise. Diagrammatically, [c1; c2] : I1 + I2 ! HO pi1q c1 / I1 + I2 o
[c1;c2] ' O w pi2q c2
I2 where, for any continuous function f : X ! Y , symbol pf q denotes copy f . Since the choice operator comes from a colimit, a number of laws are given; one example is the following equation c3 [c1; c2] = [c3 An important limit of Kl H is the pullback below, which brings parallelism up front.
I c1 hc1;c2i
"
K p 1q + K
O c2 p 2q p!q / O for ((f1; d); (f2; d)) = (hf1; f2i; d).
Intuitively, the diagrams states that whenever two components c1; c2 are compatible – in the sense that for any input the duration of their evolutions coincide (commutativity of the outer square) – we can define component hc1; c2i whose output corresponds to the (paired) evolutions of c1 and c2.
Note that functions p 1q; p 2q introduce trajectory elimination, due to their ability to remove one side of the paired evolution. Note also that p4q : X ! H(X X) duplicates trajectories, for 4 : X ! (X X) the diagonal function, and pswq swaps evolutions.
Definition 6 Given two compatible components c1 : I ! HO1, c2 : I ! HO2 component hhc1; c2ii = hc1; c2i : I ! H(O1
O2) is the parallel execution of c1; c2.
Since parallelism comes from a limit, we have again a number of laws for free; for instance hhc1; c2ii d = hhc1 d; c2 dii (5) Example 3. Consider two signal generators, c1; c2 such that c1 x = ( x + (sin - ); 20 ); c2 x = ( x + sin (3 - ); 20 ) For input 0, their parallel evolution hhc1; c2ii is illustrated in the plot below on the left. Moreover, we can combine signals. For example, to add incoming signals, take the active component c3, formally defined as c3(x; y) = (x + y; 0). For input 0, the system c3 hhc1; c2ii yields the plot shown below, on the right.
y 0 2 2 We close this section introducing a tensorial strength for monad H — which turns out to be an essential mechanism for the generation of a calculus for hybrid components.
Definition 7 Tensorial strength for monad H is a natural transformation : HX
Y ! H(X
Y ! (X
Y ) Y )R0 , f1((f; d); y) = hf; yi, and defined as = hf1; f2i where f1 : HX f2 : HX Y ! D, f2((f; d); y) = d.
Theorem 2 hH; ; i is a strong monad.
Software systems are becoming prevalently intertwined with (continuous)
physical processes. This renders their rigorous design (and analysis) a difficult
challenge that calls for a wide, uniform framework where ‘Continuous’
Mathematics and Computer Science must work together. As a first step towards a calculus
of hybrid components in the spirit of [
Our current research investigates how hybrid behaviour can be rendered
by arrows typed as hc; pi : S I ! S HO, where c : S I ! S is a discrete
arrow (S comes equipped with the discrete topology) and p : S I ! HO is a
continuous system. This paves the way to extending the component calculus in
[
Acknowledgements. This work is funded by ERDF - European Regional Development Fund, through the COMPETE Programme, and by National Funds through FCT within project FCOMP-01-0124-FEDER-028923. The author is also sponsored by FCT grant SFRH/BD/52234/2013.