Added concrete par example from grammar. Added further elaboration on example. Other...
[firstyearreport:firstyearreport.git] / types-in-eq.lhs
1
2 %include polycode.fmt 
3 %include fhm-preamble.fmt
4 %include fhm-preamble-extras.fmt
5
6 \section{Types in Equation-Based Modelling}
7 \label{sect:types-in-eq}
8
9 This section reviews two language frameworks based on equation systems
10 for equation-based modelling. There are a large number of
11 equation-based languages in use today, such as Modelica, SysML,
12 VHDL-AMS, and Simu-link. This section examines Modelica and Functional
13 Hybrid Modelling (FHM) as these language frameworks are most pertinent
14 to the work presented in this report. The chosen languages also take
15 markedly different approaches, the former is based on an
16 object-oriented paradigm, whereas the latter is based on a functional
17 paradigm.
18
19 The two aforementioned languages are both designed for modelling and
20 simulation of physical systems. Such physical systems can often span
21 multiple physical domains; for example, hydraulic, astrophysical, or
22 electrical system. These languages also typically allow \emph{hybrid}
23 models, models which exhibit both continuous- and discrete-time
24 behaviour.
25
26 \subsection{Functional Hybrid Modelling}
27 \label{sect:types-in-eq:fhm}
28
29 Functional Hybrid Modelling (FHM) is an approach to equation-based
30 modelling languages based on functional programming. \emph{Hydra}
31 \cite{Nilsson03} is one such example of a functional hybrid modelling
32 language and we will adopt Hydra syntax throughout this paper when
33 describing modular equation systems.
34
35 \subsubsection{Functional Reactive Programming}
36
37 FHM is inspired by Functional Reactive Programming (FRP), in
38 particular the \emph{Yampa} framework. FHM can be viewed as a
39 generalisation of FRP (and Yampa), hence, we will begin by introducing
40 the two central concepts of Yampa: \emph{signals} and \emph{signal
41   functions}. Conceptually, a signal is a time-varying value: i.e: a
42 function from time to a value of type $\tau$:
43
44 \[
45 Signal~\tau~\approx~\mathbb{R}^+~\rightarrow~\tau
46 \]
47
48 Here, time is represented by $\mathbb{R}^+$, the continuous,
49 non-negative real numbers. The type of the time-varying value is
50 represented by $\tau$. Thus, a \emph{signal function} is simply a
51 function between signals:
52
53 \[
54 SF~\alpha~\beta~\approx~Signal~\alpha~\rightarrow~Signal~\beta
55 \]
56
57 The $\approx$ is used to emphasise the conceptual nature of the above
58 definitions, which are not used in the implementation of Yampa. In
59 particular, signal functions are required to be
60 \emph{temporally causal}: the output of a signal function at time $t$
61 may only depend on the input signal on the interval $[0,t]$. Despite
62 this, the conceptual definitions are still useful for developing an
63 intuition about the semantics of both FRP and FHM.
64
65 \subsubsection{Signal Relations}
66
67 The above definitions of signals and signal functions describe systems
68 that are inherently causal. Signal functions are \emph{directed},
69 taking an input signal and returning an output signal. FHM generalises
70 signal functions to \emph{signal relations}. Signal relations are
71 acausal: they do not distinguish between inputs and outputs but rather
72 express how signals are related to one another. A signal relation may
73 be viewed as a predicate on a signal:
74
75 \[
76 SR~\tau~\approx~Signal~\tau~\rightarrow~Prop
77 \]
78
79 To recovery binary (or n-ary) relations, one can observe the following
80 isomorphism: $\forall~\alpha~\beta .~Signal~\alpha \times Signal~\beta
81 ~\simeq~Signal~( \alpha\times\beta )$, making unary signal relations
82 sufficient to represent n-ary relations. For example, given a binary
83 predicate $\equiv$ on $\mathbb{R}$ we can construct a binary signal
84 relation:
85
86 > (sigeq)    ::  SR (Real, Real)
87 > (sigeq) s  =   forall (t : Time). ^^ fst (s t) == snd (s t)
88
89 \subsubsection{Hydra}
90 \label{sect:types-in-eq:hydra}
91
92 Hydra is a functional hybrid modelling language embedded in the
93 functional programming language Haskell \cite{Haskell98Report}. The
94 embedding creates two \emph{levels}: the signal level and the
95 functional level, the former contained within the latter. Functional
96 level objects can be referenced from within the signal level, but
97 signal level objects are not permitted to escape to the functional
98 level.
99
100 Signal relations are constructed using the |sigrel| primitive, marking
101 the boundary between the two levels:
102
103 > sigrel pattern where equations
104
105 Signal relations are first-class, function-level objects that
106 encapsulate a set of |equations|. These equations range over signal
107 variables introduced by the |pattern|, similar to the abstraction
108 mechanism presented in Sect. \ref{sect:modular-systems:abstraction}.
109 We refer to these signal variables as \emph{interface variables}.
110 Signal variables that occur in the set of equations but not in the
111 pattern are referred to as \emph{local variables}, and do not occur
112 anywhere else in the system. There are two forms of equations:
113 \begin{eqnarray}
114 e_1 = e_2 \\
115 sr \diamond e_3
116 \end{eqnarray}
117 Here, |sr| is a \emph{time-invariant} expression (signal variables
118 must not occur in it) denoting a signal relation, and |<>| denotes
119 signal relation application. To illustrate, consider a component
120 |twoPin| encapsulating equations common to all electrical components
121 with two pins.
122
123 \begin{code}
124 type Pin = (Real , Real)
125 ^^
126 twoPin  ::  SR (Pin , Pin , Voltage)
127 twoPin  =  sigrel ((sub(p)(i),sub(p)(v)),(sub(n)(i),sub(n)(v)),u) where
128     sub(p)(i) - sub(n)(i)  =  u
129     sub(p)(v) + sub(n)(v)  =  0
130 \end{code}
131
132 In the above, |Pin| is a pair of values representing an electrical
133 connection. Thus, |twoPin| describes how the two pins and voltage of
134 the component are related.
135
136 \begin{code}
137 resistor :: Resistance -> SR (Pin, Pin)
138 resistor r = sigrel ((sub(p)(i),sub(p)(v)),(sub(n)(i),sub(n)(v))) where
139     twoPin         <>  ((sub(p)(i),sub(p)(v)),(sub(n)(i),sub(n)(v)),u)
140     r * sub(p)(v)  =   u
141 \end{code}
142
143 The |resistor| component extends |twoPin| by adding an equation that
144 describes the behaviour of a resistor. The component shows how a
145 system can be parametrised by a coefficient, in this example by the
146 parameter |r|. Note that |u| is a local signal variable, whereas $r$
147 is a time-invariant, function-level parameter.
148
149 Since signal relations are first-class, it is also permitted to
150 parametrise one system of equations by another. For example,
151 duplicating a circuit component in parallel. The model |par| is
152 parametrised by another model |sr| representing a two-pinned
153 component; for example, a resistor.
154
155 \noindent
156 \begin{minipage}{0.55\linewidth}
157 \begin{code}
158 par :: SR (Pin , Pin) -> SR (Pin ,  Pin)
159 par sr =
160     sigrel ((pi, pv), (ni, nv)) where
161       sr <> ((p1i, p1v), (n1i, n1v))
162       sr <> ((p2i, p2v), (n2i, n2v))
163       pi + p1i + p2i = 0
164       ni + n1i + n2i = 0
165       pv = p1v = p2v
166       nv = n1v = n2v
167 \end{code}
168 \end{minipage}
169 \begin{minipage}{0.45\linewidth}
170 \includegraphics{twoParRes.eps}
171 \vspace{0.9cm}
172 \end{minipage}
173
174 Elaboration of Hydra models proceeds by substitution of variables
175 under signal relation application, resulting in either a flat set of
176 equations, or a $\lambda$-expression. To illustrate, consider the
177 modular system of equations in the relation |resistor 220|:
178
179 \begin{code}
180     twoPin           <>  ((sub(p)(i),sub(p)(v)),(sub(n)(i),sub(n)(v)))
181     220 * sub(p)(v)  =   u
182 \end{code}
183
184 A single step of unfolding eliminates the application of |twoPin|,
185 producing a flat set of 3 equations:
186
187 \begin{code}
188     sub(p)(i) - sub(n)(i)  =  u
189     sub(p)(v) - sub(p)(v)  =  0
190     220 * sub(p)(v)        =  u
191 \end{code}
192
193
194 \subsection{Modelica}
195 \label{sect:types-in-eq:modelica}
196
197 Modelica is an approach to hybrid modelling inspired by concepts
198 originating in object-oriented programming. While we do not make use
199 of Modelica in this report, it is used extensively by authors, not
200 least because it is one of the most mature acausal modelling languages
201 and is in widespread use in industry. In particular, the work by
202 Broman et al. \cite{Broman2006a} on \emph{balance checking} is
203 developed in a subset of Modelica called \emph{Featherweight
204   Modelica}.
205
206 The class concept is the basic structuring mechanism in
207 Modelica. There are a number of categories of classes, the following
208 being the most important:
209
210 \begin{itemize}
211
212   \item \textbf{model}: Analogous to signal relations in
213     FHM. Encapsulate \emph{elements} and equations. Instances of
214     models are often referred to as \emph{components}.
215
216   \item \textbf{record}: A class containing only elements and no
217     equations.
218
219   \item \textbf{connector}: A special record for use within
220     connections. 
221
222 \end{itemize}
223
224
225 As with other object-oriented languages, such as Smalltalk
226 \cite{Smalltalk}, classes may contain \emph{elements} (also known as
227 \emph{attributes}) which are instances of other classes or primitive
228 types. However, unlike most object-oriented languages with imperative
229 state, Modelica is declarative and the behaviour of a Modelica class
230 is described using equations as opposed to methods.
231
232 Equations can be specified using an explicit relation between elements
233 of the class, or by inheriting them from another class. Equations can
234 also be given implicitly in the case of connectors. So called
235 \emph{connect-equations} express coupling between two connectors and
236 are useful for specifying system topology. The equations of a class
237 are undirected, hence, Modelica supports acausal modelling.
238
239 \subsubsection{Type Equivalence}
240 \label{sect:tieq-type-equivalence}
241
242 Type equivalence is a fundamental property of a type system. Type
243 equivalence is used extensively during type checking and forms the
244 basis of type soundness. A nominal type system is one in which types
245 are identified by their \emph{names}. FHM is an example of a nominal
246 type system, a property inherited from it's host language Haskell. By
247 contrast, Modelica employs a \emph{structural} type system.
248
249 Structural type systems identify types by the structure of the values
250 that inhabit them. Hence, two types are equal if and only if their
251 values have the same structure. In Modelica, two types |tau| and
252 |sigma| are equivalent if they satisfy at least one of following
253 conditions:
254
255 \begin{itemize}
256
257   \item |tau| and |sigma| both denote the same primitive type.
258
259   \item If |tau| and |sigma| are classes, |tau| and |sigma| contain
260     the same public elements (nominally), and the types of the
261     corresponding elements in |tau| and |sigma| are equivalent.
262
263 \end{itemize}
264
265 Fig. \ref{fig:type-equiv-modelica} gives examples of Modelica models,
266 where model |A| is type equivalent to model |B|, but not to model |C|.
267 Note that in model |A|, the elements |p| and |q| are the \emph{public
268   elements}, and correspond to the interface variables of an FHM
269 signal relation.
270
271 \begin{figure}[h]
272 \begin{minipage}[t]{0.1\linewidth}
273  \hspace{0pt}
274 \end{minipage}
275 \begin{minipage}[t]{0.29\linewidth}
276 \modelicamodel
277     {A}
278     {Real |p|; \\ Real |q|;}
279     {|q = 4|; \\ |der(p) = p - q|;}
280 \end{minipage}
281 \begin{minipage}[t]{0.29\linewidth}
282 \modelicamodel
283     {B}
284     {Real |p|; \\ Real |q|;}
285     {|p = 3|;  \\ |q = 4|;}
286 \end{minipage}
287 \begin{minipage}[t]{0.29\linewidth}
288 \modelicamodel
289     {C}
290     {Real |c|; \\ Real |p|;}
291     {|q = 4|;  \\ |3c = 2q|;}
292 \end{minipage}
293 \caption{Related models.}
294 \label{fig:type-equiv-modelica}
295 \end{figure}
296
297 \subsubsection{Subtyping and Inheritance}
298
299 Modelica also supports subtyping and inheritance. The keyword
300 \textbf{extends} denotes inheritance of elements and equations from
301 one or more base classes. Fig. \ref{fig:two-pin-modelica} illustrates
302 the usage of extends with the familiar two-pinned component example.
303
304 \begin{figure}[h]
305 \begin{minipage}[t]{0.1\linewidth}
306 \hspace{0pt}
307 \end{minipage}
308 \begin{minipage}[t]{0.29\linewidth}
309   \modelicaconnector
310       {Pin}
311       {Real |v|; \\ \textbf{flow} Real |i|;}
312 \end{minipage}
313 \begin{minipage}[t]{0.29\linewidth}
314   \modelicamodel
315       {TwoPin}
316       {Pin |p|, |n|; \\ Voltage |v|; \\ Current |i|;}
317       {|v = p.v - n.v|; \\ |0 = p.i + n.i|; \\ |i = p.i|; }
318 \end{minipage}
319 \begin{minipage}[t]{0.29\linewidth}
320   \modelicamodel
321       {Resistor}
322       {\textbf{extends} TwoPin \\ Real r;}
323       {|r * i = v|;}
324 \end{minipage}
325 \caption{Two pinned components.}
326 \label{fig:two-pin-modelica}
327 \end{figure}
328
329 |Pin| is a \emph{connector} class, representing objects that are
330 coupled using connect equations to express the topology of a
331 system. Variables marked with the keyword \textbf{flow} are quantities
332 that respect certain equations that describe the flow of some value
333 between two point; for example, the voltage at and current through a
334 electrical pin. The necessary equations for flow variables are
335 implicitly generated by the compiler.
336
337 The |Resistor| model is a subtype of |TwoPin|. In general, we say that
338 |tau| is a subtype of |sigma|, written |tau <: sigma|, if one of the
339 following conditions hold:
340
341 \begin{itemize}
342
343 \item |tau| is type equivalent to |sigma|.
344
345 \item Every public element of |sigma| is also an element of |tau| and
346   each element in |tau| is a subtype of the corresponding element in
347   |sigma|.
348
349 \end{itemize}
350
351 It can be helpful to view |<:| as an ordering relation: it is
352 reflexive, transitive, and antisymmetric. 
353
354 It is also possible to modify the internal structure of an element
355 when extending it by making use of the
356 \textbf{replaceable}/\textbf{redeclare} mechanism. Redeclarations are
357 only permitted on components marked as replaceable, and only by
358 components that are subtypes of the component to be replaced. The
359 \textbf{replaceable}/\textbf{redeclare} syntax can be seen in
360 Fig. \ref{fig:replace-modelica}.
361
362 \begin{figure}[h]
363 \begin{minipage}[t]{0.1\linewidth}
364 \hspace{0pt}
365 \end{minipage}
366 \begin{minipage}[t]{0.4\linewidth}
367   \modelicarecord
368       {M}
369       {\textbf{replaceable} TwoPin |T|}
370 \end{minipage}
371 \begin{minipage}[t]{0.4\linewidth}
372   \modelicarecord
373       {N}
374       {\textbf{extends} M (\textbf{redeclare} Resistor |T|)}
375 \end{minipage}
376 \caption{Replaceable components.}
377 \label{fig:replace-modelica}
378 \end{figure}
379
380 \subsubsection{Elaboration}
381
382 For illustrative purposes, we will now show how to elaborate the model
383 |X| given in Fig. \ref{fig:modelica-elaboration-1}.
384
385 \begin{figure}[h]
386 \begin{minipage}[t]{0.1\linewidth}
387 \hspace{0pt}
388 \end{minipage}
389 \begin{minipage}[t]{0.29\linewidth}
390   \modelicamodel
391       {X}
392       {\textbf{extends} Z; \\ Real |a|; \\ Y |y|;}
393       {|a = 0|;}
394 \end{minipage}
395 \begin{minipage}[t]{0.29\linewidth}
396   \modelicamodel
397       {Y}
398       {Real |a|; \\ Real |b|;}
399       {|a = der(b)|;}
400 \end{minipage}
401 \begin{minipage}[t]{0.29\linewidth}
402   \modelicamodel
403       {Z}
404       {Real |m|; \\ Real |n|;}
405       {|m + 2 = n * 4|;}
406 \end{minipage}
407
408 \caption{Replaceable components.}
409 \label{fig:modelica-elaboration-1}
410 \end{figure}
411
412 The first thing to note is that model |X| extends model |Z|, hence we
413 need to copy the elements and equations of |Z| into |X|. The unfolded
414 model is shown in Fig. \ref{fig:modelica-elaboration-2}, called |XZ|.
415
416 \begin{figure}[h]
417 \begin{minipage}[t]{0.2\linewidth}
418 \hspace{0pt}
419 \end{minipage}
420 \begin{minipage}[t]{0.4\linewidth}
421   \modelicamodel
422       {XZ}
423       {Real |m|; \\ Real |n|; \\ Real |a|; \\ Y |y|;}
424       {|a = 0|; \\ |m + 2 = n * 4|;}
425 \end{minipage}
426 \begin{minipage}[t]{0.3\linewidth}
427   \modelicamodel
428       {Flat}
429       {Real |m|; \\ Real |n|; \\ Real |a|; \\ Real |y.a|; \\ Real |y.b|;}
430       {|a = 0|; \\ |m + 2 = n * 4|; \\ |y.a = der(y.b)|;}
431 \end{minipage}
432 \caption{Stages of elaboration.}
433 \label{fig:modelica-elaboration-2}
434 \end{figure}
435
436 The second step is to eliminate all non-primitive elements from the
437 model |XZ|. The component |y| is an instance of the model |Y| and must
438 be elaborated. The elements and equations of |Y| are copied into |XZ|,
439 taking care to rename the elements with the prefix |y| to avoid name
440 clashes. The completely elaborated model is given in
441 Fig. \ref{fig:modelica-elaboration-2} as Flat.
442
443 %% . Class and object types?
444 %% . Modification equations ( not too important? )
445
446
447
448
449
450
451