Added concrete par example from grammar. Added further elaboration on example. Other...
[firstyearreport:firstyearreport.git] / balance.lhs
1
2 %include polycode.fmt
3 %include fhm-preamble.fmt
4 %include fhm-preamble-extras.fmt
5
6 \section{Related Work}
7 \label{sect:balance}
8
9 The aim of this report is to investigate the role types play in
10 equation-based programming languages. In particular, we hope to
11 motivate the development of novel type system features that will aid
12 in the construction of correct equation-based programs. The primary
13 focus of this section is to outline certain basic properties of
14 equation systems and review related work. However, this section also
15 covered material that is relevant to future work proposed in
16 Sect. \ref{sect:future}. The scope of this section is not to cover
17 every aspect of related work, but instead to review the work of those
18 authors that have had a prominent impact on the development of our own
19 system.
20
21 This section forms the basis for Sect. \ref{sect:refined}, where we
22 present a new approach \cite{CapperNilsson} to capturing structural
23 properties that overcomes several weaknesses of the existing methods
24 outlined in this section.
25
26 \subsection{Simple Structural Properties}
27 \label{sect:balance:eq-balance}
28
29 An important question regarding systems of equations is whether a
30 system possess a solution and if such a solution is unique. In
31 general, one can only answer this question by studying a complete
32 system of equations where all coefficients are known. Unfortunately,
33 requiring a system to be fully assembled is in direct opposition to
34 the modular approach discussed in Sect. \ref{sect:modular-systems},
35 ruling out the possibility of checking components in
36 isolation. Furthermore, due to the generality of our approach, one
37 cannot hope to create a decidable type theory capable of determining
38 if an arbitrary modular system of equations possess a solution.
39
40 However, there are simple criteria that if violated are indicative of
41 problems, or that may even imply that an attempt to solve a system by
42 a specific method will necessarily fail. Below is a weak and stronger
43 condition that is often used
44 \cite{Nilsson2008,Broman2006a,Bunus2002,ModelicaSpec,
45   CapperNilsson}. Note that these criteria are only useful heuristics
46 and are not necessary or sufficient conditions for solvability.
47 \begin{enumerate}
48
49   \item \label{property:balance}Variable-equation balance (weak): the
50     number of \emph{unknowns} or variables must equal the number of
51     equations.
52
53   \item \label{property:struct-singular}Structurally non-singular
54     (strong): it must be possible to pair each variable with an
55     equation in which it occurs (A bijection between variables and
56     equations).
57
58 \end{enumerate}
59 Since there will always be a finite number of variables and equations,
60 property \ref{property:struct-singular} implies property
61 \ref{property:balance}. In the example below, there is a bijection
62 between the set of variables $\{x,y,z\}$, and the set of equations
63 $\{\ref{equation:1},\ref{equation:2},\ref{equation:3}\}$ given by $\{x
64 \mapsto \ref{equation:2}, y \mapsto \ref{equation:3} , z \mapsto
65 \ref{equation:1} \}$. Thus, the system given below is both balanced
66 and structurally non-singular.
67 \begin{eqnarray}
68 %% x = 9 ; y = -4 ; z = 5
69 x + y    &=&  z \label{equation:1} \\  
70 x + 3    &=&  12 \label{equation:2} \\
71 y^2 + 9  &=&  z^2 \label{equation:3} 
72 \end{eqnarray}
73
74 The criteria stem from the fact that a \emph{linear} system of
75 equations has a unique solution if and only if the equations are
76 independent and the number of equations and variables
77 agree. Intuitively, one could interpret each variable as a degree of
78 freedom and each equation as a constraint that eliminates a degree of
79 freedom. Hence, for a system to possess a unique solution, one would
80 expect an equal number of variables and equations.
81
82 If a linear system of equations has more variables than independent
83 equations, it is said to be \emph{under-determined}. Conversely, if
84 there are more equations than variables, it is said to be
85 \emph{over-determined}. The difference between the number of variables
86 and equations is often referred to as the \emph{equation-variable}
87 balance. By analogy, we will refer to a system with positive
88 equation-variable balance as \emph{over-constrained}, and one with
89 negative balance as \emph{under-constrained}, regardless of whether
90 the equations are actually independent or even linear.
91
92 As the section title indicates, the above properties are strictly
93 structural. No assumptions can be made about the nature of the equations
94 besides the set of variables they \emph{mention}.
95
96 It is import to emphasise that these properties are only useful
97 heuristics in general; it is easy to construct an example of a system
98 of equations that, whilst formally violating the above criteria, still
99 possess a solution. Consider the following example:
100 \begin{eqnarray*}
101 x        &=&  2 \\
102 x^2 + 1  &=&  5
103 \end{eqnarray*}
104 This system is neither balanced, nor structurally singular, yet still
105 clearly has a solution at |x = 2|. Nevertheless, enforcing the above
106 properties is still considered very useful in practise. For example,
107 Modelica insists that complete models are balanced. Indeed,
108 translation to simulation code will fail if a system is unbalanced.
109
110 \subsubsection{Modelica Association}
111 \label{sect:balance:modelica}
112
113 As of version 3.0 of the Modelica specification \cite{ModelicaSpec}
114 models are required to be locally balanced. A model is locally
115 balanced if it locally declares or inherits the same number of
116 variables and equations. Requiring every model to be locally balanced
117 guarantees that a Modelica program will be globally balanced.
118
119 The Modelica approach is very restrictive: there are good reasons for
120 why components sometimes need to be locally unbalanced; importantly, a
121 combination of locally unbalance components may form a globally
122 balanced system. Due to this, a component may be declared to be
123 \textbf{partial}, disabling balance checking for that component.
124
125 The Modelica specification does not identify any further requirements
126 for modular checking of structural properties, such as the detection
127 of structural singularities.
128
129 \subsubsection{Bunus \& Fritzson} 
130 \label{sect:balance:bunus}
131
132 Bunus and Fritzon \cite{Bunus2002} describe a static analysis
133 technique for pinpointing problems with systems of equations developed
134 in equation-based languages such as Modelica. The primary motivation
135 for their work is towards developing effective debugging techniques
136 for equation systems. They are concerned with structural properties,
137 as we are, but, allowing systems to be flattened before analysis
138 grants them the capacity to perform a much more fine-grained
139 localisation of problems.
140
141 The main contribution of the work is the localisation and reporting of
142 program errors in a method consistent with the programmers perception
143 of the system. An efficient technique for annotating equations for
144 future analysis is also outlined. The methods discussed are robust,
145 even in the face of program optimisations that may change the
146 intermediate structure of the modular system of equations.
147
148 Since the methods outlined are intended to be used after a system has
149 been elaborated, they are in many ways complimentary to the type
150 system presented in Sect. \ref{sect:refined}. The methods could even
151 be performed during simulation, making them potentially very useful
152 for analysis of iteratively-staged, structurally-dynamic systems
153 discussed in Sect. \ref{sect:balance:meta}.
154
155 \subsubsection{Broman, Nystr\"{o}m \& Fritzson}
156 \label{sect:balance:broman}
157
158 Broman et al. \cite{Broman2006a} have developed a more refined
159 approach to modular balance checking than the approach described by
160 the current Modelica specification \cite{ModelicaSpec}. Most notably,
161 models are not required to be locally balanced provided that the fully
162 assembled system is balanced. The type system, dubbed Structural
163 Constraint Delta ($C_{\Delta}$), is developed for a subset of Modelica
164 called \emph{Featherweight Modelica}.
165
166 The core idea behind $C_{\Delta}$ is to refine the notion of type
167 equality such that two models are only equal if they are equal under
168 the Modelica interpretation (see \ref{sect:tieq-type-equivalence}) and
169 have the same variable-equation balance. This idea is extended to
170 subtyping relationships where |S <: C| holds only when |S| is a
171 Modelica subtype of |C|, and |S| and |C| have the same
172 variable-equation balance. This refinement is motivated by the
173 principle of safe substitution, in this instance, stating that it is
174 only safe to replace one class by another if the replacement preserves
175 the global balance of a system.
176
177 The refined notion of type equality is realised by annotating the type
178 of a class with a defined integer, which represents the difference
179 between the total number of defined equations and variables. The
180 annotation is a concrete value as Featherweight Modelica classes are
181 not first-class entities; the information required to compute the
182 annotation is always manifest in the structure of the object being
183 analysed. Hence, the $C_{\Delta}$ may always be computed in a
184 bottom-up fashion.
185
186 Broman et al. present a type inference algorithm for computing
187 $C_{\Delta}$ and give a number of examples demonstrating the
188 usefulness of the type system for both error detection and error
189 localisation. To our knowledge, the idea of incorporating balance
190 checking into the type system of a non-causal modelling language was
191 suggested independently by Nilsson et al. \cite{Nilsson2008} and
192 Broman, with the latter giving the first detailed account.
193
194 By contrast, the type system discussed in Sect. \ref{sect:refined}
195 lifts a number of restrictions inherent to $C_{\Delta}$. Our approach
196 permits first-class models, hence, we do not rely on manifest type
197 information as the structure of a model may be partially or even
198 completely unknown. Furthermore, parameterised models are parameteric
199 in their balance; a model may be instantiated with different values
200 for its parameters, resulting in distinct balances for each usage of
201 the model within the same context.
202
203 The approach taken by Broman is strictly balance oriented. In
204 contrast, our system captures some structural properties beyond simple
205 balance. For example, signal relations are valid only when they do not
206 over- or under-constrain their local variables.
207
208 %% Should an example of $C_{\Delta}$ appear in this section?
209
210 \subsubsection{Nilsson}
211 \label{sect:balance:nilsson}
212
213 Nilsson et al. \cite{Nilsson2008} outline an approach to static
214 checking that makes stronger guarantees about the structure of
215 equations and variables beyond that of simple balance. In many cases,
216 Nilsson's \emph{structural types} are able to rule out systems with
217 structural singularities that would otherwise be accepted under a
218 simple balance checking approach. As with the system developed in
219 Sect. \ref{sect:refined}, Nilsson develops his approach for the FHM
220 framework.
221
222 The incidence matrix of a system of equations represents the
223 occurrence of variables in equations. By approximating incidence
224 matrices in the types of signal relations and equations, Nilsson
225 approaches the capabilities of Bunus and Fritzon's technique, while
226 retaining the capability of checking fragments in isolation.
227
228 To demonstrate, consider the simply typed example given below:
229
230 \begin{code}
231 sig :: SR (Real , Real , Real)
232 sig = sigrel (x1 , x2 , x3) where
233     sub f 1 x1 x2  =  0
234     sub f 2 x2 x3  =  0
235 \end{code}
236
237 The type of the signal relation is augmented with an incidence matrix
238 computed from the structure of the signal relation. The matrix has 2
239 rows; one for each equation, and 3 columns; one for each unknown. The
240 occurrence of a variable is indicated by a 1. For further technical
241 details, consult Nilsson's notes.
242 \[sig :: SR ( |Real| , |Real| ,  |Real| ) 
243     \bordermatrix{ & x_1 & x_2 & x_3 \cr
244                    & 1   & 1   & 0   \cr
245                    & 0   & 1   & 1   }\]
246 Nilsson's work is a preliminary investigation into structural types,
247 opting to focus on the handling of static models. Nilsson does not
248 consider first-class models or methods by which to communicate type
249 errors to the programmer. By contrast, our type system does handle
250 first-class models, but is not able to detect as many structural
251 problems.
252
253  
254 \subsection{Multi-staged Programming}
255 \label{sect:balance:meta}
256
257 Multi-staged programming is an approach to solving complex problems by
258 combining runtime program generation and multi-level partial
259 evaluation. Multi-staged programming techniques can be used to
260 implement structurally dynamic systems, making it a topic of interest
261 in equation-based language communities.
262
263 \subsubsection{Giorgidze \& Nilsson}
264 \label{sect:balance:meta:giorgidze}
265
266 Giorgidze and Nilsson \cite{Giorgidze2009a} achieve structural
267 dynamism in FHM through the use of special |switch| statements that
268 allows major changes in the behaviour of a system to be
269 expressed. Giorgidze et al. describe how highly-structurally dynamic
270 systems; systems that have a large, or even potentially unbounded 
271 number of configurations can be modelled and simulated.
272
273 The |switch| construct accounts for the passing of state between
274 system configurations, and is of the following form:
275 \begin{code}
276 switch :: SR (a , E b) -> (b -> SR a) -> SR a
277 \end{code}
278 The |switch| takes an initial model configuration and an event
279 |E|. When the event occurs, the current system state is applied to the
280 second parameter and the resulting model is taken as the new
281 configuration. The |switch| statement is an example of higher-order
282 modelling or \emph{meta-modelling}.
283
284 \subsubsection{Taha}
285
286 Taha et al. \cite{Taha1997,Taha1998,Taha2003,Taha2007} have looked in
287 depth at type theories and semantics for multi-staged languages. In
288 particular, they have examined \emph{heterogeneous} multi-staged
289 languages, of which FHM could be considered an instance.
290
291 The typical approach taken by Taha et al. is to stratify a language
292 based upon the iteration in which a given expression is to be
293 evaluated. The meta-theory of such systems is well developed, and
294 could form the basis of a semantics for a highly structurally dynamic
295 system such as FHM.
296
297 \subsection{Units-of-Measure Checking}
298 \label{sect:balance:units}
299
300 Units of measurement are critical in engineering and in the
301 application of physical systems. Errors in the correct usage of
302 measurement units can have disastrous consequences, the most notable
303 of which is the loss of NASA's Mars Climate Orbiter probe in September
304 1999 \cite{NASA}, which was directly caused by confusion between the
305 newtons and pound-force units-of-measure.
306
307 A variety of techniques for mechanically checking the consistency of
308 units-of-measure in programming languages have been suggested
309 \cite{Karr1978,Dreiheller1986,Wand1991}. This section reviews some of
310 the most recent and relevant work.
311
312 \subsubsection{Kennedy}
313
314 Kennedy et al. \cite{Kennedy2008a, Kennedy2008b, Kennedy2010,
315   Kennedy1997, Kennedy1994} have looked in depth at developing type
316 theories for unit-of-measure checking. The work by Kennedy improves on
317 existing approaches in a number of ways; most notably, they develop a
318 theory that permits expressions to be polymorphic in their dimensions.
319 Furthermore, a full type inference algorithm capable of inferring a
320 most general dimension for expressions is given. The meta-theory of
321 Kennedy's system is well developed and could provide a solid basis
322 from which to begin work on theories for equation-based languages.
323
324 \subsubsection{Aronsson \& Broman}
325
326 Aronsson and Broman give an informal review of unit-of-measure
327 checking in Modelica \cite{Aronsson2008}. They explore the
328 possibilities of checking units-of-measure statically during
329 elaboration based on annotations by the programmer. They present a
330 partial algorithm for determining if models are dimensionally
331 consistent, but must admit to dimensionless cases where the
332 annotations are insufficient to determine exact dimensions. The method
333 presented permits dimension polymorphic expressions but in a more
334 restricted form than the work by Kennedy.
335  
336 Aronsson et al. also investigate ways to report inconsistent dimension
337 errors to the user \cite{Aronsson2009}.