Subversion Repositories TPPL


Rev 46 | Blame | Compare with Previous | Last modification | View Log | RSS feed

% aims
% * support for agreements in project planning:
%   * What is the TPPL prototype good for ?
%   * What are general directions of development for successors ?
%   * Reflect possibly different views of TP, software verification and CA
% * raw material for proposal


}                    %DISABLE FOR FINAL VERSION

\title{Design and Prototype for a \\
  TP-based Programming Language\\
  {\Large Draft for an FWF proposal}}



\bigskip \bigskip
\section{Theorem Proving underway to Engineering Practice
% This section picks out the note ``that the aim of this project is to
% provide a running prototype environment'' in \S\ref{mission} and goes
% beyond the mission stated there.
Interdisciplinary work as addressed in the proposal ``Design and
Prototype for a TP-based Programming Language (TP-PL)'' is best begun
by sharing visions between TP-PL developers and potential users. Such
visions shall be a fertile soil for joint work to identify applications
of TP-PL, which create a win-win situation for users and developers.
These notes shall
serve this purpose and start from a wider perspective going beyond the
proposal text.

\subsection{Engineers' attitudes towards mathematical software}
In applied sciences there are strong attitudes towards usage of
mathematical software which in turn are a constituent part of
professional values and ethics.

A first aspect of the attitudes reflects a great success of computer
mathematics, in numeric as well as in symbolic computation: Engineers
and experts in applied sciences have high expectations with regard to
computational power of tools like Mathematica, Mathlab or Maple, for
instance when solving huge equational systems, when performing
enormous numbers of computations or when simplifying large terms.

A second aspect of the attitudes addresses deficiencies of
mathematical software still considered inevitable: Engineers are
taught to be personally responsible for results of mathematical
software and to be always alert for casual inappropriate results due
to ill-conditioned systems, e.g.~numerical instabilities with floating
point numbers or issues related to multivalued functions
\cite{davenport-10:multivalued}~\footnote{Errors cited from
are $\int^1_{-1}{\sqrt{x^2}dx}=0$ instead of $=1$ (Maple, \url{}) and
$\int^1_{-1}{\frac{1}{\sqrt{x^2}}dx}=0$ instead of ``undefined''
(Mathematica, \url{}).}.

\medskip So these traditional attitudes and expectations have good
reasons and must be taken into account when TP is approaching
engineering practice.

\subsection{Computer Mathematics' approaches to engineering practice}
There are several success stories of rigorous formal approaches to
engineering problems with impact on practice.

TP is particularly successful in software verification \footnote{A representative
overview can be gained from the publication lists of the Verisoft project
at \url{}},
but has also gained revenue in mechanised proofs for sizable mathematical
problems, e.g.~the Kepler Conjecture\footnote{\url{}}
or the Four Colour Theorem \cite{DBLP:conf/ascm/Gonthier07}.

Success stories of certified and verified Computer Algebra are

\footnote{fixme[Further success stories of CA?]}

\bigskip Apart from the approaches by the dedicated academic
communities from TP and from CA respectively there are further
approaches with similar goals. One integrative approach from the side of computer
science is called ``Formal Methods
(FM)''~\cite{fm-03}~\footnote{}, an approach
which actually has been born in Austria and which is still alive as
``Vienna Development Method
This community promotes several successful projects, for instance the
COMPASS project~\footnote{} with the goal of
supporting the engineering of dependable systems-of-systems based on
contractual styles of interface specification. Proof support is under
development and ``is expected to build on HOL''~\fixme[Which HOL? Reference imprecise.]~\footnote{Deliverable
D33.2 ``Theorem Proving Support'' at}. These goals are
close to those of the TP-PL project such that the proposal has to
refer to such projects.

\medskip Another approach from the side of applied mathematics is
called ``Systems Modeling (SM)'' split into various directions from
Operational Research to such specific technologies like
``Vehicle Systems Model-ling and
These approaches build on graphical representations of problems and
solutions rather than on representation based on formal logic. From
this side come easy-to-adopt mathematical tools like Maple's
MapleSim~\footnote{} and
Mathematica's System

\subsection{What are the promises of  TP + CA?}
A generally promising aspect of the TP-PL proposal is that explicit
cooperation is established between two institutes, Theorem Proving
Group at TUM and Research Institute for Symbolic Computation at JKU,
each leading in the respective domain: The former develops Isabelle, a
cutting-edge tool, and promotes joint development of a rapidly growing
body of mechanised mathematics knowledge. The latter is not only a
center for excellence in CA, but also has lots of expertise in
industrial application of CA.

Before the TP-PL initiative focuses an a proposal text, it seems
appropriate to consider what expertise combined from both institutes
might promise. Such promises are the following.

\subsubsection{Prove properties of technical systems}\label{promise-prove}
Traditionally computers support engineering practice by their
computational power from CA systems or from domain specific
software. As mentioned already, deducing properties of systems from
properties of sub-systems and built-in software traditionally is
concern of personal expertise and common sense.

The progress of pervasive computing drives TP methodology more and
more into hardware systems alongside the integration of software. This
can be observed in mechanical engineering (e.g. autonomous robots
beginning to share the human living and working spaces), electrical
engineering (e.g. in railway signaling systems in the transition to
high-speed trains), etc.

From the users' side the dependability of systems and respective
safety standards create a tendency towards increased use of TP

\subsubsection{Improve comparability of algorithms and devices}\label{promise-domain}
Standardised bench-marks are used in disciplines, which are not yet
well settled, which are inherently complex and which are far off
standardisation otherwise. Another way, probably more appropriate with
respect to responsibilities imposed on a working engineer, is FM,
which promotes mechanisation of mathematical/physical theories in
respective axioms, definitions, theorems and proofs in TP technology;
also formal specification of physical entities together with a
thorough formal description of their properties; and also formal
specification of software algorithms together with a thorough formal
description of their properties.

In the academic field FM provides prerequisites for comparing
different kinds of hardware and software systems. Such comparison is
particularly valuable in emerging fields, where an abundance of
different algorithms in combination with various physical devices
are emerging.

\subsubsection{Support assembly of sub-systems}\label{promise-assembly}
Comparison of software algorithms and technical devices on a formal
level provides improved prerequisites for assembling systems from
sub-systems. The COMPASS
project~\footnote{\url{}} project even
states commercial reasons for FM: ``Although there are great
opportunities here, the design of innovative products and services
that take advantage of Systems of Systems (SoS) technology is hampered
by the complexity caused by the heterogeneity and independence of the
constituent systems, and the difficulty of communication between their
diverse stakeholders. Developers lack models and tools to help make
trade-off decisions during design and evolution leading to sub-optimal
design and rework during integration and in service. Our work is
inspired by the vision that complex SoSs can be successfully and
cost-effectively engineered using methods and tools that promote the
construction and early analysis of models.''

\subsubsection{Automatically generate verified code}\label{promise-codegen}
is an appealing
feature in engineering anytime. As soon as TP-based domain engineering
has created a sufficiently large and re-usable body of mechanised
knowledge, TP-based software development might become sufficiently
efficient for specific areas of engineering practice. However, a
program, as developed within a TP-based environment, is very
inefficient in execution time and memory consumption within the
TP-based environment.

So extension of Isabelle's code generator to the full range of the
TP-based programming language is a feature very appealing to

\subsection{Examples for promising TP-PL applications}
The previous section stated general promises of FM in a long-term
view; the TP-PL project, however, addresses only a small (however
crucial) part of FM, and also wants to have a successful short-term

So several institutes at Graz University of Technology have been
contacted during preparation of the TP-PL project. Presentation of the
general promises discussed in the previous section, identified some
topics in some institutes, which probably could lead to a reasonable
application of the TP-PL.  The following topics are notable.

\subsubsection{Electrical Capacitance Tomography}
``Electrical Capacitance Tomography (ECT) is a well-investigated and
well-documented method to non-invasively determine the permittivity
distribution in a pipe and to provide cross-sectional images of this
distribution. The permittivity distribution is obtained by measuring
the electrical capacitance between sets of electrodes placed on the
outer circumference of a non-conductive pipe section. This procedure
leads to a nonlinear and ill-posed inverse problem, where the number
of unknowns (i.e. pixel number) typically exceeds the number of
independent equations (i.e. different pairs of

``ECT is well-suited for industrial processes since materials
typically involved in industrial processes like multiphase flows show
good contrast in terms of the permittivity.  [..]. Examples of
processes including multiphase flow can be found in almost every
industry, e.g. food production, separation columns, fluidized beds,
chemical reactors, oil production, waste water treatment, mining
operations, and pneumatic
conveying.''~\cite{SpringerBuch-TODO-PERMISSION}. There are many other
applications of ECT, for instance distance sensing in automotive

\medskip The ill-posed inverse problem is tackled by various
mathematical methods in ECT. The ``forward problem'' is
\begin{equation} \label{ect-fwd-pbl}
Y=F(\epsilon)+w\;\;\;\;\;\epsilon\in E\;\;\;\;\;Y\in M
where $Y$ is the matrix of capacitances in the electrodes, an element
of the measurement space $M$, $\epsilon$ is a matrix in the set of
permittivity distribution spaces $E$, and $w$ represents the
inevitable measurement noise. So, $F$ computes the capacitances $Y$
from the permittivities $\epsilon$ for a certain configuration of
objects. Now, the result expected from ECT is solving the inverse
\begin{equation} \label{ect-inv-pbl}
where the configuration of objects (i.e. the respective permittivity
distribution $\epsilon$) is reconstructed from the measurements $Y$ in
the electrodes. Due to the ill-posedness of the problem and the
measurement noise $w$, a specific reconstruction $F^{-1}_i$ of a
specific distribution $\epsilon_i$ deviates to some
$\hat{\epsilon}_i$ and we get
\begin{equation} \label{ect-estimate}
where the \textit{expectation} $E$ for the \textit{mean square error}
(or some other quality measure) should be bounded by some
$\delta$. For tackling the inverse $F^{-1}$ various mathematical
methods and various combinations of methods are adopted: linear and
non-linear, iterative and non-iterative, analytic (e.g. derivatives)
and stochastic, continuous and discrete (e.g. the Finite Element
Method (FME)) methods.

As is typical for an emerging field, in ECT there is not yet agreement
on optimal methods for the many possibilities of configurations of
observables. Rather, a typical publication of yet another method
presents a configurations of observables, where this method is
superior --- but it can hardly be compared with other methods: general
investigations are still missing.  For instance, given a certain
$\delta$ in the inequality (\ref{ect-estimate}) above, for which kinds
of $Y$ which kinds of $F^{-1}_i$ are below $\delta$. Or is there a
$\delta$ such that for a given $Y$ we have $\forall
, i.e. there are technical reasons
which do not allow for this specific $Y$ to have a better
approximation then $\delta$? Or the other way round: for some $\delta$
and some reconstruction method $F^{-1}_i$, do we have $\forall
, i.e. the method $F^{-1}_i$ is limited to
an error above $\delta$? Even general knowledge would be useful like:
for a certain $Y$ and a certain $F^{-1}_i$ can we have $\exists
\delta.\; {\it max}\left(\hat{\epsilon}_i-\epsilon_i \right)$
i.e. can we expect reasonable data at all? Answering such questions
concerns hardware and software components included in $F^{-1}$.

\bigskip As an example, at TUG there is ongoing
research~\cite{zangl:ect-precomp-12} on a specific method, which
pre-computes a matrix $A$ such that process monitoring, as the very
task of ECT and probably implemented in large quantities of devices,
becomes simply
\begin{equation} \label{ect-online}
where $H$ contains the actual measurements subjected to
computationally cheap methods; so, monitoring does neither involve
iterations nor expensive methods like Gauss-Newton reconstruction. For
this method the experimental data are excellent when compared to the
state-of-the-art; general statements about the method's properties are
to be researched, hopefully supported by TP technology. Interesting
for practical application is validation of this method, which
specifies general questions asked above to $\exists
or more simple ${\it max}\left(\hat{\epsilon}_i-\epsilon_i

The method for calculating $A$ comprises hardware and software
components, the respective specification is as follows.
  %\begin{tabular}{ | l | l | p{8cm} |}
  \begin{tabular}{ | l | l | l |}
        & variable & property / \textit{explanation} \\\hline
  input &       &  \\\hline
        & $K_i$ & quadratic, positive semi-definite matrix \\
        &       & computed by a specific generator \cite{zangl:ect-precomp-12}~p.6, \\
        &       & \textit{which creates a specific PDF and which} \\
        &       & \textit{reflects the specific PDF with respect to a specific FEM geometry} \\\hline
        & $\tilde{K}$ & TODO \\\hline
        & $R$   & \textit{matrix of constraints;} \\
        &       & \textit{reflects the sensor geometry within a specific FEM geometry} \\\hline
        & $\hat{e}$ & \textit{matrix of estimated values in the image space $E$}\\\hline
  output&       &  \\\hline
        & $A$   & \textit{coefficient matrix for reconstruction of pixels} \\\hline
The calculation of $A$ follows equalities on matrices, in detail
$R=K\cdot U$ where $K=\Sigma_{i=1}^l e_i K_i$ and $H=\tilde{K}\cdot U$
where $\tilde{K}=\Sigma_{i=1}^l e_i \tilde{K_i}$, leading to
$A=(H^TH)^{-1}H^T\check{E}$ finally. By Monte Carlo Method (MCM) $l$
samples $\check{E}$ are generated; for $l=10.000$ the dimensions are
$121\times 316$ for $A$, $50.000\times 121$ for $H$ and $50.000\times
for $\check{E}$
%was ist $U$?
%H in (4) ist was anderes als H oberhalb

\bigskip Summary: ECT is a topic which promises some success in all points
addressee in the previous section:
\item \textit{Prove properties of technical systems,} (\S\ref{promise-prove}) this is
desirable for the example given above.
\item \textit{Improve comparability of algorithms and devices} (\S\ref{promise-domain}) is an
actual issue in the emerging field of ECT. Some initial contributions
by the TP-PL project seem possible.
\item \textit{Automatically generate verified code} (\S\ref{promise-codegen}) for software
meeting stardardisation criteria, that is an ongoing concern in
development of measurement devices.
\item \textit{Support assembly of sub-systems} (\S\ref{promise-assembly}) is beyond the scope of
the TP-PL project, but of principal interest: some applications like
automotive applications are subject to
dependability~\cite{zangl:auto-ect-11}, others are subject to
standards for measurement devices.

\subsubsection{Dependability issues in Robotics}
``When autonomous robots begin to share the human living and working
spaces, safety becomes paramount.  It is legally required that the
safety of such systems is ensured, e. g. by certification according
to relevant standards such as IEC 61508''~\footnote{Cited from

\medskip At TUG there are several activities in robotics.

\subsubsection{Non-Shannon-type inequalities}
Another domain where TP-PL seems to be able to serve actual research is
Information theory -- in spite the fact, that the Isabelle theory
\textit{Information.thy} in the release of 2012 covers only the first
50 pages of total 650 in a standard text book~\cite{info-thy-06}: the
final theorems in \textit{Information.thy} are
conditional\_entropy\_less\_eq\_entropy, entropy\_chain\_rule} and

What makes this topic promising, is request for automated provers for
so-called ``Shannon-type inequalities'' --- however, there are also
``non-Shannon-type inequalities''~\cite{non-shannon-01} which would
require interactive proof.

\subsection{Summary: Which goals are realisable in the TP-PL project~?}


  \begin{tabular}{l | l}
  ECT & electrical capacitance tomography \\
  FEM & finite element method \\
  MCM & monte carlo method \\
  PDF & probability density function \\
      & \\
      & \\