On a Monadic Encoding of Continuous Behaviour (extended abstract) Renato Neves INESC TEC (HASLab) & University of Minho, Portugal rjneves@inescporto.pt Abstract. 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 (con- tinuous) 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 com- positional development of hybrid systems, may play a role similar to the one played by the maybe, powerset, and distribution monads in the char- acterisation of partial, non deterministic and probabilistic components, respectively. Keywords: Monads, components, hybrid systems, control theory 1 Introduction 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 com- position and synchronisation mechanisms. More and more, however, compo- nents are not limited to traditional information processing units, but encapsu- late 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 con- strained, and cooperate to achieve specific goals. One way of looking at components, proposed in [1, 2], emphasises an ob- servational semantics, through a signature of observers and methods, making them amenable to a coalgebraic [3] characterisation as (generalisations of) ab- stract Mealy machines. The resulting calculus is parametric on whatever be- havioural model underlies a component specification. This captures, for exam- ple, partial, non deterministic or probabilistic evolution of a component’s dy- namics by encoding such behavioural effects as strong monads [4, 5]. This paper summarises a number of results developed in the context of the author’s PhD project [6]. Namely, the introduction of a strong monad H [7] that 44 Renato Neves subsumes continuous behaviour and the study of the corresponding Kleisli cat- egory [8] as the mathematical space in which the underlying behaviour can be isolated and its effect over different forms of composition studied. This work may pave the way to the development of a coalgebraic calculus of hybrid compo- nents. Related work. A few categorial models for hybrid systems have been proposed. For example, document [9] introduced an institution – in essence, a categorial rendering of logic – for hybrid systems and provided basic forms of compo- sition. Around the same time, Jacobs [10] suggested a coalgebraic framework where hybrid systems are viewed as coalgebras equipped with a monoid ac- tion. Some years later Haghverdi et. al [11] provided a formalisation of hybrid systems using a conceptual framework that is closer to the coalgebraic perspec- tive. The monad reported in this paper captures the typical continuous behaviour of hybrid systems. Actually, there is a close relationship between the work re- ported here and Peter Höfner’s algebra of hybrid systems [12]: the latter’s main operator and its laws are embedded in the (sequential) composition of KlH, the Kleisli category for monad H. Since our approach, differently from Höfner’s calculus, is structured around a monad that encodes continuous evolution, a number of canonical construc- tions 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 correspond- ing Kleisli category Kl H, characterising composition and some (co)limits. Fi- nally, conclusions and possible future research directions are discussed in Sec- tion 5. In this paper many calculations adopt a pointfree style in the spirit of the Bird-Meertens formalism [13]. 2 Preliminaries 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 X Y comes with the exponential topology [14]. In this context, given a continuous function f : X × Y → Z where Y is core–compact, we denote its curried version by On a monadic encoding of continuous behaviour 45 λf : X → Z Y . Moreover, we will use the following isomorphisms in Top: αl : (X × Y ) × Z ∼ = X × (Y × Z) ∼ sw : X × Y = Y × X i : (X × Y )R0 ∼ = X R0 × 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 x px (f C p B g) x = (f x C p x B g 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 in- finity. 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, |C| denotes the corre- sponding class of objects. 3 A Monad for Continuity Formally, we see continuous systems as arrows of the type I → O R0 × 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 ∈ D. Definition 1 H : Top → Top is a functor such that, for any objects X, Y ∈ |Top| and any continuous function g : X → Y , HX = { (f, d) ∈ X R0 × D | f · fd = f } Hg = g · × id 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 ∈ R0 such that r > d, f r = f d. Hence, continuous systems become arrows of the type I → HO 46 Renato Neves also denoted as I → · O. The crucial step now is to equip H with a monad structure, i.e. with natural transformations · · η : Id → H, µ : HH → H. First, Definition 2 Given any X ∈ |Top|, define ηX : X → HX such that ηX x = (x, i1 0) in pointfree notation ηX = hλπ1 , i1 · 0i. The definition of µ is more demanding. Definition 3 Define the continuous functions g : HHX × R0 → X R0 , h : HHX × R0 → R0 such that g((f, d), r) = (π1 · f ) (r f d), h((f, d), r) = r  d Next, we have f l1 : HHX → X R0 where f l1 = λ(ev · hg, hi). In pointwise notation, f l1 is defined as f l1 (f, d) = ev · hπ1 · f · fd , d i Then, define function f l2 : H2 X → D such that f l2 (f, d) = ((π2 · f ) d C (d 6∈ 1) B i2 ?) + d Finally, we define for any X ∈ |Top|, µX = hf l1 , f l2 i. Intuitively, operation µX ‘concatenates’ functions: given a pair (f, d) ∈ HHX, µX concatenates function (π1 · f ) - 0 : [0, d] → X with (π1 · f ) d - : [0, d0 ] → X, and sums the corresponding durations. Theorem 1 The triple hH, η, µi forms a monad. Proof. In document [7]. 4 The Category of Continuous Behaviours 4.1 Kleisli Composition The Kleisli category for H (KlH) provides an interesting setting to study the re- quirements placed by continuity over different forms of composition; actually, the envisaged component calculus for hybrid systems is essentially its calculus. This motivates the study of Kl H, summmarised in the current section. The definition of Kleisli composition in Kl H suggests a relevant distinction between continuous systems. On a monadic encoding of continuous behaviour 47 Definition 4 A continuous system c : I → HI is passive if the following diagram commutes I fc / I R0 ev·hid,0i id  I 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 composi- tion we obtain component c2 • c1 : I → HO whose behaviour is computed as follows: π1 · (c2 • c1 ) x = { Kleisli composition } π1 · µ · Hc2 · c1 x = { Cancellation × } f l1 · Hc2 · c1 x = { Definition of H ( taking d = (π2 · c1 ) x ) } f l1 (c2 · (fc1 x), d) = { Application } ev · hπ1 · c2 · (fc1 x) · fd , d i = { Notation } ev · hfc2 · (fc1 x) · fd , d i Going pointwise, ev · hfc2 · (fc1 x) · fd , d i t = { Application }  fc2 fc1 x (t f d) (t  d) = { Notation }   fc2 fc1 x t 0 C ( t ≤ d ) B fc2 fc1 x d (t − d) = { If c2 is passive }  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 ∈ I the resulting evolution corresponds to the evolution of the first component 48 Renato Neves 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 c1 r = (r + sin - , 3π), c2 r = (r + sin (3 × - ), 3π) the signal given by c1 • (c2 • c1 ) 0 yields the plot below c1 • (c2 • c1 ) 0 2 0 y −2 0 5 10 15 20 25 x This type of signal is common in the domain of frequency modulation, where the varying frequency is used to encode information for electromagnetic transmis- sion. 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 - ), ∞ ), 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 monadic encoding of continuous behaviour 49 c2 • c1 10 c3 • c2 • c1 10 25 25 20 20 y y 15 15 10 10 0 5 10 15 20 25 30 0 5 10 15 20 25 30 x x On a different note, for any X ∈ |Top|, arrow ηX is a trivial system in the sense that its evolutions always have duration zero and the only point in the trajecto- ries 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 = c1 (1) c1 • copy = c1 (2) (c3 • c2 ) • c1 = c3 • (c2 • c1 ) (3) 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 [c1 , c2 ] : I1 + I2 → HO behaves as c1 if input I1 is chosen, and as c2 otherwise. Diagrammatically, I1 pi1 q · / I1 + I2 o pi2 q · I2 · · [c1 ,c2 ] · c1 c2 '  w O where, for any continuous function f : X → Y , symbol pf q denotes copy · f . 50 Renato Neves Since the choice operator comes from a colimit, a number of laws are given; one example is the following equation c3 • [c1 , c2 ] = [c3 • c1 , c3 • c2 ] (4) An important limit of Kl H is the pullback below, which brings parallelism up front. c2 · I γ·hc1 ,c2 i · "  K ×O pπ2 q · /O c1 · pπ1 q · · p!q   +K · /1 p!q for γ((f1 , d), (f2 , d)) = (hf1 , f2 i, 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 , c2 i whose output corresponds to the (paired) evolutions of c1 and c2 . Note that functions pπ1 q, pπ2 q 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 , c2 ii = γ · hc1 , c2 i : 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 , c2 ii • 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 , c2 ii 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 , c2 ii yields the plot shown below, on the right. On a monadic encoding of continuous behaviour 51 hhc1 , c2 ii 0 c3 • hhc1 , c2 ii 0 2 2 0 0 y y −2 −2 0 5 10 15 20 0 5 10 15 20 x x 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 hy- brid components. Definition 7 Tensorial strength for monad H is a natural transformation · τ : HX × Y → H(X × Y ) defined as τ = hf1 , f2 i where f1 : HX × Y → (X × Y )R0 , f1 ((f, d), y) = hf, yi, and f2 : HX × Y → D, f2 ((f, d), y) = d. Theorem 2 hH, η, µi is a strong monad. Proof. In document [7]. 5 Conclusions and future work Software systems are becoming prevalently intertwined with (continuous) phys- ical processes. This renders their rigorous design (and analysis) a difficult chal- lenge that calls for a wide, uniform framework where ‘Continuous’ Mathemat- ics and Computer Science must work together. As a first step towards a calculus of hybrid components in the spirit of [2], this paper showed how continuous be- haviour can be encoded in the form of a strong topological monad, and briefly explored the corresponding Kleisli category. 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 [2] to hybrid systems. Acknowledgements. This work is funded by ERDF - European Regional De- velopment 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. 52 Renato Neves References 1. L. S. Barbosa, Components as coalgebras, Ph.D. thesis, DI, Minho University (2001). 2. L. S. Barbosa, Towards a calculus of state-based software components, Journal of Universal Computer Science 9 (2003) 891–909. 3. J. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science 249 (1) (2000) 3 – 80, modern Algebra. 4. A. Kock, Strong functors and monoidal monads, Archiv der Mathematik 23 (1) (1972) 113–120. 5. E. Moggi, Notions of computation and monads, Information and computation 93 (1) (1991) 55–92. 6. R. Neves, Logics and calculi for hybrid components, Ph.D. thesis, DI, Universidade do Minho (2017). 7. R. Neves, L. S. Barbosa, D. Hofmann, M. A. Martins, Continuity as a computational effect, CoRR abs/1507.03219. URL http://arxiv.org/abs/1507.03219 8. R. Neves, L. S. Barbosa, M. A. Martins, A kleisli category for hybrid components, in: Formal Aspects of Component Software (FACS) 2015, submitted. 9. H. Lourenço, A. Sernadas, An institution of hybrid systems, in: D. Bert, C. Choppy, P. Mosses (Eds.), Recent Trends in Algebraic Development Techniques, Vol. 1827 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2000, pp. 219–236. doi:10.1007/978-3-540-44616-3 13. URL http://dx.doi.org/10.1007/978-3-540-44616-3 13 10. B. Jacobs, Object-oriented hybrid systems of coalgebras plus monoid actions, Theoretical Computer Science 239 (1) (2000) 41 – 95. doi:http://dx.doi.org/10.1016/S0304-3975(99)00213-3. URL http://www.sciencedirect.com/science/article/pii/S0304397599002133 11. E. Haghverdi, P. Tabuada, G. J. Pappas, Bisimulation relations for dynami- cal, control, and hybrid systems, Theor. Comput. Sci. 342 (2-3) (2005) 229–261. doi:10.1016/j.tcs.2005.03.045. URL http://dx.doi.org/10.1016/j.tcs.2005.03.045 12. P. Höfner, Algebraic calculi for hybrid systems, Ph.D. thesis, University of Augsburg (2009). 13. R. Bird, O. de Moor, The Algebra of Programming, Prentice-Hall, 1996. URL http://www.cs.ox.ac.uk/publications/books/algebra/ 14. M. Escardó, R. Heckmann, Topologies on spaces of continuous functions, in: Topol- ogy Proceedings, Vol. 26, 2001, pp. 545–564.