=Paper=
{{Paper
|id=Vol-1454/ramics15-st_43-52
|storemode=property
|title=On a Monadic Encoding of Continuous Behaviour
|pdfUrl=https://ceur-ws.org/Vol-1454/ramics15-st_43-52.pdf
|volume=Vol-1454
}}
==On a Monadic Encoding of Continuous Behaviour==
https://ceur-ws.org/Vol-1454/ramics15-st_43-52.pdf
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.