%include polycode.fmt
%include fhm-preamble.fmt
%include fhm-preamble-extras.fmt
\section{Related Work}
\label{sect:balance}
The aim of this report is to investigate the role types play in
equation-based programming languages. In particular, we hope to
motivate the development of novel type system features that will aid
in the construction of correct equation-based programs. The primary
focus of this section is to outline certain basic properties of
equation systems and review related work. However, this section also
covered material that is relevant to future work proposed in
Sect. \ref{sect:future}. The scope of this section is not to cover
every aspect of related work, but instead to review the work of those
authors that have had a prominent impact on the development of our own
system.
This section forms the basis for Sect. \ref{sect:refined}, where we
present a new approach \cite{CapperNilsson} to capturing structural
properties that overcomes several weaknesses of the existing methods
outlined in this section.
\subsection{Simple Structural Properties}
\label{sect:balance:eq-balance}
An important question regarding systems of equations is whether a
system possess a solution and if such a solution is unique. In
general, one can only answer this question by studying a complete
system of equations where all coefficients are known. Unfortunately,
requiring a system to be fully assembled is in direct opposition to
the modular approach discussed in Sect. \ref{sect:modular-systems},
ruling out the possibility of checking components in
isolation. Furthermore, due to the generality of our approach, one
cannot hope to create a decidable type theory capable of determining
if an arbitrary modular system of equations possess a solution.
However, there are simple criteria that if violated are indicative of
problems, or that may even imply that an attempt to solve a system by
a specific method will necessarily fail. Below is a weak and stronger
condition that is often used
\cite{Nilsson2008,Broman2006a,Bunus2002,ModelicaSpec,
CapperNilsson}. Note that these criteria are only useful heuristics
and are not necessary or sufficient conditions for solvability.
\begin{enumerate}
\item \label{property:balance}Variable-equation balance (weak): the
number of \emph{unknowns} or variables must equal the number of
equations.
\item \label{property:struct-singular}Structurally non-singular
(strong): it must be possible to pair each variable with an
equation in which it occurs (A bijection between variables and
equations).
\end{enumerate}
Since there will always be a finite number of variables and equations,
property \ref{property:struct-singular} implies property
\ref{property:balance}. In the example below, there is a bijection
between the set of variables $\{x,y,z\}$, and the set of equations
$\{\ref{equation:1},\ref{equation:2},\ref{equation:3}\}$ given by $\{x
\mapsto \ref{equation:2}, y \mapsto \ref{equation:3} , z \mapsto
\ref{equation:1} \}$. Thus, the system given below is both balanced
and structurally non-singular.
\begin{eqnarray}
%% x = 9 ; y = -4 ; z = 5
x + y &=& z \label{equation:1} \\
x + 3 &=& 12 \label{equation:2} \\
y^2 + 9 &=& z^2 \label{equation:3}
\end{eqnarray}
The criteria stem from the fact that a \emph{linear} system of
equations has a unique solution if and only if the equations are
independent and the number of equations and variables
agree. Intuitively, one could interpret each variable as a degree of
freedom and each equation as a constraint that eliminates a degree of
freedom. Hence, for a system to possess a unique solution, one would
expect an equal number of variables and equations.
If a linear system of equations has more variables than independent
equations, it is said to be \emph{under-determined}. Conversely, if
there are more equations than variables, it is said to be
\emph{over-determined}. The difference between the number of variables
and equations is often referred to as the \emph{equation-variable}
balance. By analogy, we will refer to a system with positive
equation-variable balance as \emph{over-constrained}, and one with
negative balance as \emph{under-constrained}, regardless of whether
the equations are actually independent or even linear.
As the section title indicates, the above properties are strictly
structural. No assumptions can be made about the nature of the equations
besides the set of variables they \emph{mention}.
It is import to emphasise that these properties are only useful
heuristics in general; it is easy to construct an example of a system
of equations that, whilst formally violating the above criteria, still
possess a solution. Consider the following example:
\begin{eqnarray*}
x &=& 2 \\
x^2 + 1 &=& 5
\end{eqnarray*}
This system is neither balanced, nor structurally singular, yet still
clearly has a solution at |x = 2|. Nevertheless, enforcing the above
properties is still considered very useful in practise. For example,
Modelica insists that complete models are balanced. Indeed,
translation to simulation code will fail if a system is unbalanced.
\subsubsection{Modelica Association}
\label{sect:balance:modelica}
As of version 3.0 of the Modelica specification \cite{ModelicaSpec}
models are required to be locally balanced. A model is locally
balanced if it locally declares or inherits the same number of
variables and equations. Requiring every model to be locally balanced
guarantees that a Modelica program will be globally balanced.
The Modelica approach is very restrictive: there are good reasons for
why components sometimes need to be locally unbalanced; importantly, a
combination of locally unbalance components may form a globally
balanced system. Due to this, a component may be declared to be
\textbf{partial}, disabling balance checking for that component.
The Modelica specification does not identify any further requirements
for modular checking of structural properties, such as the detection
of structural singularities.
\subsubsection{Bunus \& Fritzson}
\label{sect:balance:bunus}
Bunus and Fritzon \cite{Bunus2002} describe a static analysis
technique for pinpointing problems with systems of equations developed
in equation-based languages such as Modelica. The primary motivation
for their work is towards developing effective debugging techniques
for equation systems. They are concerned with structural properties,
as we are, but, allowing systems to be flattened before analysis
grants them the capacity to perform a much more fine-grained
localisation of problems.
The main contribution of the work is the localisation and reporting of
program errors in a method consistent with the programmers perception
of the system. An efficient technique for annotating equations for
future analysis is also outlined. The methods discussed are robust,
even in the face of program optimisations that may change the
intermediate structure of the modular system of equations.
Since the methods outlined are intended to be used after a system has
been elaborated, they are in many ways complimentary to the type
system presented in Sect. \ref{sect:refined}. The methods could even
be performed during simulation, making them potentially very useful
for analysis of iteratively-staged, structurally-dynamic systems
discussed in Sect. \ref{sect:balance:meta}.
\subsubsection{Broman, Nystr\"{o}m \& Fritzson}
\label{sect:balance:broman}
Broman et al. \cite{Broman2006a} have developed a more refined
approach to modular balance checking than the approach described by
the current Modelica specification \cite{ModelicaSpec}. Most notably,
models are not required to be locally balanced provided that the fully
assembled system is balanced. The type system, dubbed Structural
Constraint Delta ($C_{\Delta}$), is developed for a subset of Modelica
called \emph{Featherweight Modelica}.
The core idea behind $C_{\Delta}$ is to refine the notion of type
equality such that two models are only equal if they are equal under
the Modelica interpretation (see \ref{sect:tieq-type-equivalence}) and
have the same variable-equation balance. This idea is extended to
subtyping relationships where |S <: C| holds only when |S| is a
Modelica subtype of |C|, and |S| and |C| have the same
variable-equation balance. This refinement is motivated by the
principle of safe substitution, in this instance, stating that it is
only safe to replace one class by another if the replacement preserves
the global balance of a system.
The refined notion of type equality is realised by annotating the type
of a class with a defined integer, which represents the difference
between the total number of defined equations and variables. The
annotation is a concrete value as Featherweight Modelica classes are
not first-class entities; the information required to compute the
annotation is always manifest in the structure of the object being
analysed. Hence, the $C_{\Delta}$ may always be computed in a
bottom-up fashion.
Broman et al. present a type inference algorithm for computing
$C_{\Delta}$ and give a number of examples demonstrating the
usefulness of the type system for both error detection and error
localisation. To our knowledge, the idea of incorporating balance
checking into the type system of a non-causal modelling language was
suggested independently by Nilsson et al. \cite{Nilsson2008} and
Broman, with the latter giving the first detailed account.
By contrast, the type system discussed in Sect. \ref{sect:refined}
lifts a number of restrictions inherent to $C_{\Delta}$. Our approach
permits first-class models, hence, we do not rely on manifest type
information as the structure of a model may be partially or even
completely unknown. Furthermore, parameterised models are parameteric
in their balance; a model may be instantiated with different values
for its parameters, resulting in distinct balances for each usage of
the model within the same context.
The approach taken by Broman is strictly balance oriented. In
contrast, our system captures some structural properties beyond simple
balance. For example, signal relations are valid only when they do not
over- or under-constrain their local variables.
%% Should an example of $C_{\Delta}$ appear in this section?
\subsubsection{Nilsson}
\label{sect:balance:nilsson}
Nilsson et al. \cite{Nilsson2008} outline an approach to static
checking that makes stronger guarantees about the structure of
equations and variables beyond that of simple balance. In many cases,
Nilsson's \emph{structural types} are able to rule out systems with
structural singularities that would otherwise be accepted under a
simple balance checking approach. As with the system developed in
Sect. \ref{sect:refined}, Nilsson develops his approach for the FHM
framework.
The incidence matrix of a system of equations represents the
occurrence of variables in equations. By approximating incidence
matrices in the types of signal relations and equations, Nilsson
approaches the capabilities of Bunus and Fritzon's technique, while
retaining the capability of checking fragments in isolation.
To demonstrate, consider the simply typed example given below:
\begin{code}
sig :: SR (Real , Real , Real)
sig = sigrel (x1 , x2 , x3) where
sub f 1 x1 x2 = 0
sub f 2 x2 x3 = 0
\end{code}
The type of the signal relation is augmented with an incidence matrix
computed from the structure of the signal relation. The matrix has 2
rows; one for each equation, and 3 columns; one for each unknown. The
occurrence of a variable is indicated by a 1. For further technical
details, consult Nilsson's notes.
\[sig :: SR ( |Real| , |Real| , |Real| )
\bordermatrix{ & x_1 & x_2 & x_3 \cr
& 1 & 1 & 0 \cr
& 0 & 1 & 1 }\]
Nilsson's work is a preliminary investigation into structural types,
opting to focus on the handling of static models. Nilsson does not
consider first-class models or methods by which to communicate type
errors to the programmer. By contrast, our type system does handle
first-class models, but is not able to detect as many structural
problems.
\subsection{Multi-staged Programming}
\label{sect:balance:meta}
Multi-staged programming is an approach to solving complex problems by
combining runtime program generation and multi-level partial
evaluation. Multi-staged programming techniques can be used to
implement structurally dynamic systems, making it a topic of interest
in equation-based language communities.
\subsubsection{Giorgidze \& Nilsson}
\label{sect:balance:meta:giorgidze}
Giorgidze and Nilsson \cite{Giorgidze2009a} achieve structural
dynamism in FHM through the use of special |switch| statements that
allows major changes in the behaviour of a system to be
expressed. Giorgidze et al. describe how highly-structurally dynamic
systems; systems that have a large, or even potentially unbounded
number of configurations can be modelled and simulated.
The |switch| construct accounts for the passing of state between
system configurations, and is of the following form:
\begin{code}
switch :: SR (a , E b) -> (b -> SR a) -> SR a
\end{code}
The |switch| takes an initial model configuration and an event
|E|. When the event occurs, the current system state is applied to the
second parameter and the resulting model is taken as the new
configuration. The |switch| statement is an example of higher-order
modelling or \emph{meta-modelling}.
\subsubsection{Taha}
Taha et al. \cite{Taha1997,Taha1998,Taha2003,Taha2007} have looked in
depth at type theories and semantics for multi-staged languages. In
particular, they have examined \emph{heterogeneous} multi-staged
languages, of which FHM could be considered an instance.
The typical approach taken by Taha et al. is to stratify a language
based upon the iteration in which a given expression is to be
evaluated. The meta-theory of such systems is well developed, and
could form the basis of a semantics for a highly structurally dynamic
system such as FHM.
\subsection{Units-of-Measure Checking}
\label{sect:balance:units}
Units of measurement are critical in engineering and in the
application of physical systems. Errors in the correct usage of
measurement units can have disastrous consequences, the most notable
of which is the loss of NASA's Mars Climate Orbiter probe in September
1999 \cite{NASA}, which was directly caused by confusion between the
newtons and pound-force units-of-measure.
A variety of techniques for mechanically checking the consistency of
units-of-measure in programming languages have been suggested
\cite{Karr1978,Dreiheller1986,Wand1991}. This section reviews some of
the most recent and relevant work.
\subsubsection{Kennedy}
Kennedy et al. \cite{Kennedy2008a, Kennedy2008b, Kennedy2010,
Kennedy1997, Kennedy1994} have looked in depth at developing type
theories for unit-of-measure checking. The work by Kennedy improves on
existing approaches in a number of ways; most notably, they develop a
theory that permits expressions to be polymorphic in their dimensions.
Furthermore, a full type inference algorithm capable of inferring a
most general dimension for expressions is given. The meta-theory of
Kennedy's system is well developed and could provide a solid basis
from which to begin work on theories for equation-based languages.
\subsubsection{Aronsson \& Broman}
Aronsson and Broman give an informal review of unit-of-measure
checking in Modelica \cite{Aronsson2008}. They explore the
possibilities of checking units-of-measure statically during
elaboration based on annotations by the programmer. They present a
partial algorithm for determining if models are dimensionally
consistent, but must admit to dimensionless cases where the
annotations are insufficient to determine exact dimensions. The method
presented permits dimension polymorphic expressions but in a more
restricted form than the work by Kennedy.
Aronsson et al. also investigate ways to report inconsistent dimension
errors to the user \cite{Aronsson2009}.