Added concrete par example from grammar. Added further elaboration on example. Other...
[firstyearreport:firstyearreport.git] / modular-systems.lhs
1
2 %include fhm-preamble.fmt
3 %include fhm-preamble-extras.fmt
4
5 \section{Modular Systems of Equations}
6 \label{sect:modular-systems}
7
8 %% ∙ Should be able to use a lot of the material from the paper -
9 %%   section 2.
10 %% ∙ Of general use, but we will specifically discuss hybrid, acausal
11 %%   modelling languages.
12 %% ∙ Parameterised systems of equations
13 %% ∙ Elaboration of a system of equations? How will this fit in, maybe
14 %%   this should be mentioned in passing in a non-technical sense, and
15 %%   then each section is free to talk *specifically* how that systems
16 %%   performs elaboration.
17
18 This section introduces the idea of modular systems of equations in
19 more detail. The section covers preliminary theory and introduces the
20 concepts of modularity and abstraction over systems of equations.
21
22 %% As \emph{Functional Hybrid Modelling} (FHM) provided the
23 %% immediate motivation for this work, we will draw on FHM for examples
24 %% and we will adopt a concrete syntax derived from Hydra, an FHM
25 %% language currently being developed. Further detail on FHM can be found
26 %% in Sect.~\ref{sect:fhm}.
27
28 \subsection{Preliminaries}
29 \label{sect:modular-systems:prelims}
30
31 A \emph{system of equations} is a set of equations over a set of
32 \emph{variables} or \emph{unknowns}. It has a solution if every
33 variable in the system can be instantiated with a value such that all
34 the equations are simultaneously satisfied. The domain of the
35 variables and signatures for equations is mostly orthogonal to the
36 work presented in this report. However, in the interests of working
37 with a tangible domain, we choose the domain of reals, $\mathbb{R}$,
38 or time-varying reals, unless stated otherwise.
39
40 The following is an example of a (very) simple system consisting of
41 two equations and two \emph{unknowns}.
42 \begin{eqnarray}
43   x^2 + y &=& 0 \label{eqn-a}  \\
44   3x      &=& 10 \label{eqn-b}
45 \end{eqnarray}
46 There exist a number of techniques for solving the above system of
47 equations. Here (\ref{eqn-b}) can be used to solve for $x$, and the
48 value of $x$ can then be substituted into (\ref{eqn-a}), enabling it
49 to be used to solve for $y$. However, this technique may no longer be
50 suitable for solving the following parameterised system of which the
51 above system is a specific instance.
52 \begin{eqnarray}
53   x^2 + y &=& 0 \label{eqn-a2}  \\
54   \boldsymbol{c}x      &=& 10 \label{eqn-b2}
55 \end{eqnarray}
56 Note that the system is now parametrised on a coefficient
57 $\boldsymbol{c}$. The solvability of the system now depends on the
58 value of $\boldsymbol{c}$; for example, when $\boldsymbol{c} = 0$, no
59 solution exists.
60
61 Solvability is clearly an important property of an equation system.
62 There are also a number of weaker properties that when violated are
63 indicative of problems; for example, requiring that the number of
64 equations and unknowns agree. Sect.~\ref{sect:balance} introduces a
65 number of these related properties, and Sect.~\ref{sect:refined}
66 discusses a type system extension for capturing said properties. The
67 work presented in these two sections is based upon ongoing work by
68 Capper and Nilsson \cite{CapperNilsson}.
69
70
71 \subsection{Abstraction over Systems of Equations}
72 \label{sect:modular-systems:abstraction}
73
74 The equation systems needed to describe real-world problems are
75 usually large and complicated. On the other hand, there tends to be a
76 lot of repetitive structure \cite{Cellier} making it beneficial to
77 describe the systems in terms of reusable equation system
78 fragments. For example, consider an electrical circuit comprising
79 resistors, capacitors, and inductors. Each component can be described
80 by a small equation system, and the entire circuit can then be
81 described \emph{modularly} by composition of \emph{instances} of these
82 for specific values of the components.
83
84 While the exact syntactic details vary between languages, the idea is
85 to encapsulate a set of equations as a component with a well-defined
86 interface. Let us illustrate with an example, temporarily borrowing
87 the syntax of the $\lambda$-calculus for the abstraction mechanism:
88 \begin{figure}[h]
89 \[
90 r \equiv \; \; \lambda (x,y) \rightarrow
91                          \begin{array}{rcl}
92                              x + y + z & = & 0 \\
93                              x - z     & = & 1
94                          \end{array}\]
95 \vspace{-2em}
96 \caption{Abstracting over two unknowns.}
97 \label{fig:abs-a}
98 \end{figure}
99
100 This makes the abstraction in Fig.~\ref{fig:abs-a} a relation that
101 constrains the possible values of the two \emph{interface variables}
102 $x$ and $y$ according to the encapsulated equations. The variable $z$
103 is \emph{local}, and is not visible from outside the abstraction.
104
105 The relation $r$ can now be used as a building block by
106 \emph{instantiating} it: substituting expressions for the interface
107 variables and renaming local variables as necessary to avoid name
108 clashes. We express this as application, denoted by |<>|:
109 \begin{eqnarray*}
110     u + v + w & =    & 10      \\
111     r         & |<>| & (u,v)   \\
112     r         & |<>| & (v,w+7)
113 \end{eqnarray*}
114 After unfolding and renaming, often referred to as \emph{flattening}
115 or \emph{elaboration}, the following unstructured (as opposed to
116 modular) set of equations is produced:
117 \begin{eqnarray*}
118     u + v + w         & = & 10 \\
119     u + v + z_1       & = & 0  \\
120     u - z_1           & = & 1  \\
121     v + (w + 7) + z_2 & = & 0  \\
122     v - z_2           & = & 1
123 \end{eqnarray*}
124 The relation |r| contributes 2 equations for each application.
125 Including the top-level equation, the fully elaborated system thus
126 consists of 5 equations in total over 5 unknowns. Note the need to
127 rename the local variable |z| when unfolding |r| to avoid name
128 clashes.
129
130 \subsection{Causality}
131
132 A causal system is one in which the cause-and-effect relationship
133 between variables is explicit. For example, such a system might be
134 described by a set of ordinary differential equations (ODEs) in
135 explicit form. Conversely, acausal systems do not distinguish between
136 inputs and outputs but rather express how unknowns are related. An
137 example of an acausal system might be one described by differential
138 algebraic equations (DAEs) \cite{Cellier}. A system of equations is
139 said to be acausal if the order of how the unknowns are solved is not
140 decided at modelling time.
141
142 As an example, consider Pell's equation \cite{Barbeau} over the two
143 unknowns |x| and |y| and parameterised by an integer |n|:
144 \[
145 x^2 - ny^2 = \pm 1
146 \]
147 The above equation is clearly in an acausal form. Depending on which
148 variable is known, the equation can be translated into two different
149 \emph{assignments}:
150 \begin{eqnarray*}
151 x &:=& \sqrt{\pm 1 + ny^2}\\
152 y &:=& \sqrt{\frac{x^2 \pm 1}{n}}
153 \end{eqnarray*}
154 In a causal setting, the \emph{assignment form} would need to be
155 determined and fixed during modelling. If both |x| and |y| were
156 required then both causal equations would need to be
157 provided. However, in an acausal system the original equation could be
158 used to compute either of the unknowns. Note that a causal system of
159 equations is trivially an instance of an acausal system in which all
160 equations happen to be an assignment form.
161
162 %% Acausal systems have proven to be very useful in practise, in
163 %% particular for equation-based modelling. Describing components becomes
164 %% more natural as equations can be directly transcribed without needing
165 %% to be rearranged into explicit form. The \emph{same} system of
166 %% equations can then be used to solve for different variables as
167 %% required by the context.
168
169 %% As an example, consider the acausal equation for \emph{Ohm's law}.
170 %% Ohm's law states that the current ($i$) through a conductor between
171 %% two points is directly proportional to the potential difference or
172 %% voltage ($v$) across the two points, and inversely proportional to the
173 %% resistance ($R$) between them \cite{Consoliver}. Ohm's law is given
174 %% below, where unknowns appear on both sides of the equation.
175 %% \[
176 %% i = \frac{v}{R}
177 %% \]
178 %% In a causal setting, this equation could only be used to compute the
179 %% unknown current $i$ from \emph{known} values for $v$ and $R$. If it
180 %% turned out that another part of the system needed to compute the
181 %% unknown voltage from known values of $i$ and $R$ then the equation
182 %% would need to be rewritten in a rearranged form. However, in an
183 %% acausal system the one equation could be used to compute for any of
184 %% the unknowns.
185
186 %% %% Comments about Block diagrams?
187
188 \subsection{Structural Dynamism}
189
190 The equations that describe a system of equations can be changed
191 during simulation to model major changes in its behaviour. A system
192 with multiple runtime configurations is known as structurally dynamic.
193
194 Structurally dynamic systems offer greater expressivity when modelling
195 but also create problems during simulation. Errors in a system with a
196 large or possibly even unbounded number of configurations may take a
197 very long time to surface. For example, suppose a faulty component --
198 a component that violates certain required structural invariants -- is
199 used in a very small number of possible system configurations. Only
200 when such a configuration is encountered will an error be raised, and
201 even then, identifying the responsible component could be extremely
202 difficult. Thus, enforcing even simple invariants could help with the
203 early detection of broken component.
204
205