1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 13:11:45 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 14:54:30 2012 +0200
1.3 @@ -666,7 +666,8 @@
1.4
1.5 \paragraph{At the state-of-the-art in mechanization of knowledge} in
1.6 engineering sciences, the process does not stop with the mechanization of
1.7 -mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
1.8 +mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{
1.9 +fm-03}
1.10 are expected to proceed to formal and explicit description of physical items. Signal Processing,
1.11 for instance is concerned with physical devices for signal acquisition
1.12 and reconstruction, which involve measuring a physical signal, storing
1.13 @@ -674,7 +675,7 @@
1.14 approximation thereof. For digital systems, this typically includes
1.15 sampling and quantization; devices for signal compression, including
1.16 audio compression, image compression, and video compression, etc.
1.17 -``Domain engineering''\cite{db-domain-engineering} is concerned with
1.18 +``Domain engineering''\cite{db:dom-eng} is concerned with
1.19 {\em specification} of these devices' components and features; this
1.20 part in the process of mechanization is only at the beginning in domains
1.21 like Signal Processing.
1.22 @@ -683,6 +684,17 @@
1.23 add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
1.24 p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.25 starts with a formal {\em specification} of the problem to be solved.
1.26 +\begin{figure}
1.27 + \begin{center}
1.28 + \includegraphics{fig/universe}
1.29 + \caption{Didactic ``Math-Universe'': Algorithmic Knowledge
1.30 +(Programs) is combined with Application-oriented Knowledge
1.31 +(Specifications) and Deductive Knowledge (Axioms, Definitions,
1.32 +Theorems). The Result leads to a three dimensional math
1.33 +universe.}
1.34 + \label{fig:mathuni}
1.35 + \end{center}
1.36 +\end{figure}
1.37
1.38
1.39 \subsection{Specification of the Problem}\label{spec}
1.40 @@ -933,19 +945,15 @@
1.41 solve the given problem.
1.42 \end{description}
1.43
1.44 -\subsection{Implementation of the TP-based Program}\label{progr}
1.45 -
1.46 -\paragraph{After introducing} neccesarry informations about the {\sisac{}}
1.47 -System, the main part of a implementation in the TP-bases language can be shown.
1.48 -\par
1.49 -Solution~\ref{s:impl} shows us the implementation of the
1.50 -Inverse-Z-Transformation, a description on the code is given afterwards.
1.51 -
1.52 -\begin{solution}
1.53 -\label{s:impl}
1.54 -\begin{tabbing}
1.55 -\small\it
1.56 -123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill
1.57 +\subsection{Implementation of the TP-based Program}\label{progr}
1.58 +So finally all the prerequisites are described and the program can be
1.59 +presented which computes a solution for the problem of the running
1.60 +example from p.\pageref{fig-interactive}. The reader remembering the
1.61 +introduction of the programming language in \S\ref{PL-isab} might
1.62 +immediately comprehend the program:
1.63 +{\small\it
1.64 +\begin{tabbing}\label{s:impl}
1.65 +123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.66 \> \\
1.67 \> \\
1.68 \>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\
1.69 @@ -955,19 +963,16 @@
1.70 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1.71 \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1.72 \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1.73 -\>{\rm 08}\>\>\>\>\>\>\>\> ( \> Isac, \\
1.74 -\>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction, rational, simplification]\\
1.75 -\>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\
1.76 -\>{\rm 10}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1.77 -\>{\rm 12}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1.78 +\>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
1.79 +%\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
1.80 +\>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1.81 +\>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1.82
1.83 -\>{\rm 12}\>\>\> X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ; \\
1.84 -\>{\rm 15}\>\>\> X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\
1.85 -\>{\rm 16}\>\> {\tt IN } \\
1.86 -\>{\rm 15}\>\>\> X'\_eq
1.87 -\end{tabbing}
1.88 -\end{solution}
1.89 -
1.90 +\>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@ \\
1.91 +\>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1.92 +\>{\rm 13}\>\> {\tt IN } \\
1.93 +\>{\rm 14}\>\>\> X'\_eq\\
1.94 +\end{tabbing}}
1.95 % ORIGINAL FROM Inverse_Z_Transform.thy
1.96 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.97 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.98 @@ -988,6 +993,33 @@
1.99 % " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.100 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.101 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.102 +As mentioned in \S\ref{PL} the program is purely functional and lacks
1.103 +any input statements and output statements. So the steps of
1.104 +calculation towards a solution (and interactive tutoring in step-wise
1.105 +problem solving) are created as a side-effect by Lucas-Interpretation.
1.106 +The break-points for the interpreter are the tactics \textit{Take},
1.107 +\textit{Rewrite}, \textit{SubProblem} and \textit{Rewrite\_Set} in the
1.108 +above lines {\rm 03, 04, 07, 10, 11} and {\rm 12} respectively. These
1.109 +tactics produce the lines in the calculation on p.\pageref{flow-impl}.
1.110 +
1.111 +The above program also indicates the dominant role of interactive
1.112 +selection of knowledge in the three-dimensional universe of
1.113 +mathematics as depicted in Fig.\ref{fig:mathuni} on
1.114 +p.\pageref{fig:mathuni}, The \textit{SubProblem} in the above lines
1.115 +{\rm 07..09} is more than a function call with the actual arguments
1.116 +\textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
1.117 +three items:
1.118 +\begin{enumerate}
1.119 +\item the theory, in the example \textit{Isac} because different
1.120 +methods can be selected in Pt.3 below, which are defined in different
1.121 +theories with \textit{Isac} collecting them.
1.122 +\item the specification identified by \textit{[partial\_fraction, rational, simplification]} in the tree of specifications; this specification is analogous to the specification of the main program described in \S\ref{spec}.
1.123 +\item the method in the above example is \textit{[ ]}, i.e. empty, which allows
1.124 +the interpreter to select one of the methods predefined in the specification
1.125 +\end{enumerate}
1.126 +
1.127 +.\\.\\.\\
1.128 +
1.129
1.130 \section{Workflow of Programming in the Prototype}\label{workflow}
1.131
1.132 @@ -1065,364 +1097,364 @@
1.133
1.134
1.135
1.136 -\newpage
1.137 --------------------------------------------------------------------
1.138 -
1.139 -Material, falls noch Platz bleibt ...
1.140 -
1.141 --------------------------------------------------------------------
1.142 -
1.143 -
1.144 -\subsubsection{Trials on Notation and Termination}
1.145 -
1.146 -\paragraph{Technical notations} are a big problem for our piece of software,
1.147 -but the reason for that isn't a fault of the software itself, one of the
1.148 -troubles comes out of the fact that different technical subtopics use different
1.149 -symbols and notations for a different purpose. The most famous example for such
1.150 -a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1.151 -math). In the specific part of signal processing one of this notation issues is
1.152 -the use of brackets --- we use round brackets for analoge signals and squared
1.153 -brackets for digital samples. Also if there is no problem for us to handle this
1.154 -fact, we have to tell the machine what notation leads to wich meaning and that
1.155 -this purpose seperation is only valid for this special topic - signal
1.156 -processing.
1.157 -\subparagraph{In the programming language} itself it is not possible to declare
1.158 -fractions, exponents, absolutes and other operators or remarks in a way to make
1.159 -them pretty to read; our only posssiblilty were ASCII characters and a handfull
1.160 -greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1.161 -\par
1.162 -With the upper collected knowledge it is possible to check if we were able to
1.163 -donate all required terms and expressions.
1.164 -
1.165 -\subsubsection{Definition and Usage of Rules}
1.166 -
1.167 -\paragraph{The core} of our implemented problem is the Z-Transformation, due
1.168 -the fact that the transformation itself would require higher math which isn't
1.169 -yet avaible in our system we decided to choose the way like it is applied in
1.170 -labratory and problem classes at our university - by applying transformation
1.171 -rules (collected in transformation tables).
1.172 -\paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1.173 -use of axiomatizations like shown in Example~\ref{eg:ruledef}
1.174 -
1.175 -\begin{example}
1.176 - \label{eg:ruledef}
1.177 - \hfill\\
1.178 - \begin{verbatim}
1.179 - axiomatization where
1.180 - rule1: ``1 = $\delta$[n]'' and
1.181 - rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1.182 - rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1.183 - \end{verbatim}
1.184 -\end{example}
1.185 -
1.186 -This rules can be collected in a ruleset and applied to a given expression as
1.187 -follows in Example~\ref{eg:ruleapp}.
1.188 -
1.189 -\begin{example}
1.190 - \hfill\\
1.191 - \label{eg:ruleapp}
1.192 - \begin{enumerate}
1.193 - \item Store rules in ruleset:
1.194 - \begin{verbatim}
1.195 - val inverse_Z = append_rls "inverse_Z" e_rls
1.196 - [ Thm ("rule1",num_str @{thm rule1}),
1.197 - Thm ("rule2",num_str @{thm rule2}),
1.198 - Thm ("rule3",num_str @{thm rule3})
1.199 - ];\end{verbatim}
1.200 - \item Define exression:
1.201 - \begin{verbatim}
1.202 - val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1.203 - \item Apply ruleset:
1.204 - \begin{verbatim}
1.205 - val SOME (sample_term', asm) =
1.206 - rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1.207 - \end{enumerate}
1.208 -\end{example}
1.209 -
1.210 -The use of rulesets makes it much easier to develop our designated applications,
1.211 -but the programmer has to be careful and patient. When applying rulesets
1.212 -two important issues have to be mentionend:
1.213 -\subparagraph{How often} the rules have to be applied? In case of
1.214 -transformations it is quite clear that we use them once but other fields
1.215 -reuqire to apply rules until a special condition is reached (e.g.
1.216 -a simplification is finished when there is nothing to be done left).
1.217 -\subparagraph{The order} in which rules are applied often takes a big effect
1.218 -and has to be evaluated for each purpose once again.
1.219 -\par
1.220 -In our special case of Signal Processing and the rules defined in
1.221 -Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1.222 -constants. After this step has been done it no mather which rule fit's next.
1.223 -
1.224 -\subsubsection{Helping Functions}
1.225 -
1.226 -\paragraph{New Programms require,} often new ways to get through. This new ways
1.227 -means that we handle functions that have not been in use yet, they can be
1.228 -something special and unique for a programm or something famous but unneeded in
1.229 -the system yet. In our dedicated example it was for example neccessary to split
1.230 -a fraction into numerator and denominator; the creation of such function and
1.231 -even others is described in upper Sections~\ref{simp} and \ref{funs}.
1.232 -
1.233 -\subsubsection{Trials on equation solving}
1.234 -%simple eq and problem with double fractions/negative exponents
1.235 -\paragraph{The Inverse Z-Transformation} makes it neccessary to solve
1.236 -equations degree one and two. Solving equations in the first degree is no
1.237 -problem, wether for a student nor for our machine; but even second degree
1.238 -equations can lead to big troubles. The origin of this troubles leads from
1.239 -the build up process of our equation solving functions; they have been
1.240 -implemented some time ago and of course they are not as good as we want them to
1.241 -be. Wether or not following we only want to show how cruel it is to build up new
1.242 -work on not well fundamentials.
1.243 -\subparagraph{A simple equation solving,} can be set up as shown in the next
1.244 -example:
1.245 -
1.246 -\begin{example}
1.247 -\begin{verbatim}
1.248 -
1.249 - val fmz =
1.250 - ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
1.251 - "solveFor z",
1.252 - "solutions L"];
1.253 -
1.254 - val (dI',pI',mI') =
1.255 - ("Isac",
1.256 - ["abcFormula","degree_2","polynomial","univariate","equation"],
1.257 - ["no_met"]);\end{verbatim}
1.258 -\end{example}
1.259 -
1.260 -Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
1.261 -a short overview on the commands; at first we set up the equation and tell the
1.262 -machine what's the bound variable and where to store the solution. Second step
1.263 -is to define the equation type and determine if we want to use a special method
1.264 -to solve this type.) Simple checks tell us that the we will get two results for
1.265 -this equation and this results will be real.
1.266 -So far it is easy for us and for our machine to solve, but
1.267 -mentioned that a unvariate equation second order can have three different types
1.268 -of solutions it is getting worth.
1.269 -\subparagraph{The solving of} all this types of solutions is not yet supported.
1.270 -Luckily it was needed for us; but something which has been needed in this
1.271 -context, would have been the solving of an euation looking like:
1.272 -$-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
1.273 -before (remember that befor it was no problem to handle for the machine) but
1.274 -now, after a simple equivalent transformation, we are not able to solve
1.275 -it anymore.
1.276 -\subparagraph{Error messages} we get when we try to solve something like upside
1.277 -were very confusing and also leads us to no special hint about a problem.
1.278 -\par The fault behind is, that we have no well error handling on one side and
1.279 -no sufficient formed equation solving on the other side. This two facts are
1.280 -making the implemention of new material very difficult.
1.281 -
1.282 -\subsection{Formalization of missing knowledge in Isabelle}
1.283 -
1.284 -\paragraph{A problem} behind is the mechanization of mathematic
1.285 -theories in TP-bases languages. There is still a huge gap between
1.286 -these algorithms and this what we want as a solution - in Example
1.287 -Signal Processing.
1.288 -
1.289 -\vbox{
1.290 - \begin{example}
1.291 - \label{eg:gap}
1.292 - \[
1.293 - X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1.294 - \]
1.295 - {\small\textit{
1.296 - \noindent A very simple example on this what we call gap is the
1.297 -simplification above. It is needles to say that it is correct and also
1.298 -Isabelle for fills it correct - \emph{always}. But sometimes we don't
1.299 -want expand such terms, sometimes we want another structure of
1.300 -them. Think of a problem were we now would need only the coefficients
1.301 -of $X$ and $Y$. This is what we call the gap between mechanical
1.302 -simplification and the solution.
1.303 - }}
1.304 - \end{example}
1.305 -}
1.306 -
1.307 -\paragraph{We are not able to fill this gap,} until we have to live
1.308 -with it but first have a look on the meaning of this statement:
1.309 -Mechanized math starts from mathematical models and \emph{hopefully}
1.310 -proceeds to match physics. Academic engineering starts from physics
1.311 -(experimentation, measurement) and then proceeds to mathematical
1.312 -modeling and formalization. The process from a physical observance to
1.313 -a mathematical theory is unavoidable bound of setting up a big
1.314 -collection of standards, rules, definition but also exceptions. These
1.315 -are the things making mechanization that difficult.
1.316 -
1.317 -\vbox{
1.318 - \begin{example}
1.319 - \label{eg:units}
1.320 - \[
1.321 - m,\ kg,\ s,\ldots
1.322 - \]
1.323 - {\small\textit{
1.324 - \noindent Think about some units like that one's above. Behind
1.325 -each unit there is a discerning and very accurate definition: One
1.326 -Meter is the distance the light travels, in a vacuum, through the time
1.327 -of 1 / 299.792.458 second; one kilogram is the weight of a
1.328 -platinum-iridium cylinder in paris; and so on. But are these
1.329 -definitions usable in a computer mechanized world?!
1.330 - }}
1.331 - \end{example}
1.332 -}
1.333 -
1.334 -\paragraph{A computer} or a TP-System builds on programs with
1.335 -predefined logical rules and does not know any mathematical trick
1.336 -(follow up example \ref{eg:trick}) or recipe to walk around difficult
1.337 -expressions.
1.338 -
1.339 -\vbox{
1.340 - \begin{example}
1.341 - \label{eg:trick}
1.342 - \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1.343 - \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1.344 - \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1.345 - \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1.346 - {\small\textit{
1.347 - \noindent Sometimes it is also useful to be able to apply some
1.348 -\emph{tricks} to get a beautiful and particularly meaningful result,
1.349 -which we are able to interpret. But as seen in this example it can be
1.350 -hard to find out what operations have to be done to transform a result
1.351 -into a meaningful one.
1.352 - }}
1.353 - \end{example}
1.354 -}
1.355 -
1.356 -\paragraph{The only possibility,} for such a system, is to work
1.357 -through its known definitions and stops if none of these
1.358 -fits. Specified on Signal Processing or any other application it is
1.359 -often possible to walk through by doing simple creases. This creases
1.360 -are in general based on simple math operational but the challenge is
1.361 -to teach the machine \emph{all}\footnote{Its pride to call it
1.362 -\emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1.363 -reach a high level of \emph{all} but it in real it will still be a
1.364 -survey of knowledge which links to other knowledge and {{\sisac}{}} a
1.365 -trainer and helper but no human compensating calculator.
1.366 -\par
1.367 -{{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1.368 -specifications of problems out of topics from Signal Processing, etc.)
1.369 -and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1.370 -physical knowledge. The result is a three-dimensional universe of
1.371 -mathematics seen in Figure~\ref{fig:mathuni}.
1.372 -
1.373 -\begin{figure}
1.374 - \begin{center}
1.375 - \includegraphics{fig/universe}
1.376 - \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1.377 - combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1.378 - leads to a three dimensional math universe.\label{fig:mathuni}}
1.379 - \end{center}
1.380 -\end{figure}
1.381 -
1.382 -%WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1.383 -%WN bitte folgende Bezeichnungen nehmen:
1.384 -%WN
1.385 -%WN axis 1: Algorithmic Knowledge (Programs)
1.386 -%WN axis 2: Application-oriented Knowledge (Specifications)
1.387 -%WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1.388 -%WN
1.389 -%WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1.390 -%WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1.391 -%WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1.392 -
1.393 -%JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1.394 -%JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1.395 -%JR gefordert werden WN2...
1.396 -%WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1.397 -%WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1.398 -%WN2 zusammenschneiden um die R"ander weg zu bekommen)
1.399 -%WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1.400 -%WN2 png + pdf figures mitzuschicken.
1.401 -
1.402 -\subsection{Notes on Problems with Traditional Notation}
1.403 -
1.404 -\paragraph{During research} on these topic severely problems on
1.405 -traditional notations have been discovered. Some of them have been
1.406 -known in computer science for many years now and are still unsolved,
1.407 -one of them aggregates with the so called \emph{Lambda Calculus},
1.408 -Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1.409 -us.
1.410 -
1.411 -\vbox{
1.412 - \begin{example}
1.413 - \label{eg:lamda}
1.414 -
1.415 - \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1.416 -
1.417 -
1.418 - \[ f(p)=\ldots\; p \in \quad R \]
1.419 -
1.420 - {\small\textit{
1.421 - \noindent Above we see two equations. The first equation aims to
1.422 -be a mapping of an function from the reel range to the reel one, but
1.423 -when we change only one letter we get the second equation which
1.424 -usually aims to insert a reel point $p$ into the reel function. In
1.425 -computer science now we have the problem to tell the machine (TP) the
1.426 -difference between this two notations. This Problem is called
1.427 -\emph{Lambda Calculus}.
1.428 - }}
1.429 - \end{example}
1.430 -}
1.431 -
1.432 -\paragraph{An other problem} is that terms are not full simplified in
1.433 -traditional notations, in {{\sisac}} we have to simplify them complete
1.434 -to check weather results are compatible or not. in e.g. the solutions
1.435 -of an second order linear equation is an rational in {{\sisac}} but in
1.436 -tradition we keep fractions as long as possible and as long as they
1.437 -aim to be \textit{beautiful} (1/8, 5/16,...).
1.438 -\subparagraph{The math} which should be mechanized in Computer Theorem
1.439 -Provers (\emph{TP}) has (almost) a problem with traditional notations
1.440 -(predicate calculus) for axioms, definitions, lemmas, theorems as a
1.441 -computer program or script is not able to interpret every Greek or
1.442 -Latin letter and every Greek, Latin or whatever calculations
1.443 -symbol. Also if we would be able to handle these symbols we still have
1.444 -a problem to interpret them at all. (Follow up \hbox{Example
1.445 -\ref{eg:symbint1}})
1.446 -
1.447 -\vbox{
1.448 - \begin{example}
1.449 - \label{eg:symbint1}
1.450 - \[
1.451 - u\left[n\right] \ \ldots \ unitstep
1.452 - \]
1.453 - {\small\textit{
1.454 - \noindent The unitstep is something we need to solve Signal
1.455 -Processing problem classes. But in {{{\sisac}{}}} the rectangular
1.456 -brackets have a different meaning. So we abuse them for our
1.457 -requirements. We get something which is not defined, but usable. The
1.458 -Result is syntax only without semantic.
1.459 - }}
1.460 - \end{example}
1.461 -}
1.462 -
1.463 -In different problems, symbols and letters have different meanings and
1.464 -ask for different ways to get through. (Follow up \hbox{Example
1.465 -\ref{eg:symbint2}})
1.466 -
1.467 -\vbox{
1.468 - \begin{example}
1.469 - \label{eg:symbint2}
1.470 - \[
1.471 - \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1.472 - \]
1.473 - {\small\textit{
1.474 - \noindent For using exponents the three \texttt{widehat} symbols
1.475 -are required. The reason for that is due the development of
1.476 -{{{\sisac}{}}} the single \texttt{widehat} and also the double were
1.477 -already in use for different operations.
1.478 - }}
1.479 - \end{example}
1.480 -}
1.481 -
1.482 -\paragraph{Also the output} can be a problem. We are familiar with a
1.483 -specified notations and style taught in university but a computer
1.484 -program has no knowledge of the form proved by a professor and the
1.485 -machines themselves also have not yet the possibilities to print every
1.486 -symbol (correct) Recent developments provide proofs in a human
1.487 -readable format but according to the fact that there is no money for
1.488 -good working formal editors yet, the style is one thing we have to
1.489 -live with.
1.490 -
1.491 -\section{Problems rising out of the Development Environment}
1.492 -
1.493 -fehlermeldungen! TODO
1.494 +% \newpage
1.495 +% -------------------------------------------------------------------
1.496 +%
1.497 +% Material, falls noch Platz bleibt ...
1.498 +%
1.499 +% -------------------------------------------------------------------
1.500 +%
1.501 +%
1.502 +% \subsubsection{Trials on Notation and Termination}
1.503 +%
1.504 +% \paragraph{Technical notations} are a big problem for our piece of software,
1.505 +% but the reason for that isn't a fault of the software itself, one of the
1.506 +% troubles comes out of the fact that different technical subtopics use different
1.507 +% symbols and notations for a different purpose. The most famous example for such
1.508 +% a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1.509 +% math). In the specific part of signal processing one of this notation issues is
1.510 +% the use of brackets --- we use round brackets for analoge signals and squared
1.511 +% brackets for digital samples. Also if there is no problem for us to handle this
1.512 +% fact, we have to tell the machine what notation leads to wich meaning and that
1.513 +% this purpose seperation is only valid for this special topic - signal
1.514 +% processing.
1.515 +% \subparagraph{In the programming language} itself it is not possible to declare
1.516 +% fractions, exponents, absolutes and other operators or remarks in a way to make
1.517 +% them pretty to read; our only posssiblilty were ASCII characters and a handfull
1.518 +% greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1.519 +% \par
1.520 +% With the upper collected knowledge it is possible to check if we were able to
1.521 +% donate all required terms and expressions.
1.522 +%
1.523 +% \subsubsection{Definition and Usage of Rules}
1.524 +%
1.525 +% \paragraph{The core} of our implemented problem is the Z-Transformation, due
1.526 +% the fact that the transformation itself would require higher math which isn't
1.527 +% yet avaible in our system we decided to choose the way like it is applied in
1.528 +% labratory and problem classes at our university - by applying transformation
1.529 +% rules (collected in transformation tables).
1.530 +% \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1.531 +% use of axiomatizations like shown in Example~\ref{eg:ruledef}
1.532 +%
1.533 +% \begin{example}
1.534 +% \label{eg:ruledef}
1.535 +% \hfill\\
1.536 +% \begin{verbatim}
1.537 +% axiomatization where
1.538 +% rule1: ``1 = $\delta$[n]'' and
1.539 +% rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1.540 +% rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1.541 +% \end{verbatim}
1.542 +% \end{example}
1.543 +%
1.544 +% This rules can be collected in a ruleset and applied to a given expression as
1.545 +% follows in Example~\ref{eg:ruleapp}.
1.546 +%
1.547 +% \begin{example}
1.548 +% \hfill\\
1.549 +% \label{eg:ruleapp}
1.550 +% \begin{enumerate}
1.551 +% \item Store rules in ruleset:
1.552 +% \begin{verbatim}
1.553 +% val inverse_Z = append_rls "inverse_Z" e_rls
1.554 +% [ Thm ("rule1",num_str @{thm rule1}),
1.555 +% Thm ("rule2",num_str @{thm rule2}),
1.556 +% Thm ("rule3",num_str @{thm rule3})
1.557 +% ];\end{verbatim}
1.558 +% \item Define exression:
1.559 +% \begin{verbatim}
1.560 +% val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1.561 +% \item Apply ruleset:
1.562 +% \begin{verbatim}
1.563 +% val SOME (sample_term', asm) =
1.564 +% rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1.565 +% \end{enumerate}
1.566 +% \end{example}
1.567 +%
1.568 +% The use of rulesets makes it much easier to develop our designated applications,
1.569 +% but the programmer has to be careful and patient. When applying rulesets
1.570 +% two important issues have to be mentionend:
1.571 +% \subparagraph{How often} the rules have to be applied? In case of
1.572 +% transformations it is quite clear that we use them once but other fields
1.573 +% reuqire to apply rules until a special condition is reached (e.g.
1.574 +% a simplification is finished when there is nothing to be done left).
1.575 +% \subparagraph{The order} in which rules are applied often takes a big effect
1.576 +% and has to be evaluated for each purpose once again.
1.577 +% \par
1.578 +% In our special case of Signal Processing and the rules defined in
1.579 +% Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1.580 +% constants. After this step has been done it no mather which rule fit's next.
1.581 +%
1.582 +% \subsubsection{Helping Functions}
1.583 +%
1.584 +% \paragraph{New Programms require,} often new ways to get through. This new ways
1.585 +% means that we handle functions that have not been in use yet, they can be
1.586 +% something special and unique for a programm or something famous but unneeded in
1.587 +% the system yet. In our dedicated example it was for example neccessary to split
1.588 +% a fraction into numerator and denominator; the creation of such function and
1.589 +% even others is described in upper Sections~\ref{simp} and \ref{funs}.
1.590 +%
1.591 +% \subsubsection{Trials on equation solving}
1.592 +% %simple eq and problem with double fractions/negative exponents
1.593 +% \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
1.594 +% equations degree one and two. Solving equations in the first degree is no
1.595 +% problem, wether for a student nor for our machine; but even second degree
1.596 +% equations can lead to big troubles. The origin of this troubles leads from
1.597 +% the build up process of our equation solving functions; they have been
1.598 +% implemented some time ago and of course they are not as good as we want them to
1.599 +% be. Wether or not following we only want to show how cruel it is to build up new
1.600 +% work on not well fundamentials.
1.601 +% \subparagraph{A simple equation solving,} can be set up as shown in the next
1.602 +% example:
1.603 +%
1.604 +% \begin{example}
1.605 +% \begin{verbatim}
1.606 +%
1.607 +% val fmz =
1.608 +% ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
1.609 +% "solveFor z",
1.610 +% "solutions L"];
1.611 +%
1.612 +% val (dI',pI',mI') =
1.613 +% ("Isac",
1.614 +% ["abcFormula","degree_2","polynomial","univariate","equation"],
1.615 +% ["no_met"]);\end{verbatim}
1.616 +% \end{example}
1.617 +%
1.618 +% Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
1.619 +% a short overview on the commands; at first we set up the equation and tell the
1.620 +% machine what's the bound variable and where to store the solution. Second step
1.621 +% is to define the equation type and determine if we want to use a special method
1.622 +% to solve this type.) Simple checks tell us that the we will get two results for
1.623 +% this equation and this results will be real.
1.624 +% So far it is easy for us and for our machine to solve, but
1.625 +% mentioned that a unvariate equation second order can have three different types
1.626 +% of solutions it is getting worth.
1.627 +% \subparagraph{The solving of} all this types of solutions is not yet supported.
1.628 +% Luckily it was needed for us; but something which has been needed in this
1.629 +% context, would have been the solving of an euation looking like:
1.630 +% $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
1.631 +% before (remember that befor it was no problem to handle for the machine) but
1.632 +% now, after a simple equivalent transformation, we are not able to solve
1.633 +% it anymore.
1.634 +% \subparagraph{Error messages} we get when we try to solve something like upside
1.635 +% were very confusing and also leads us to no special hint about a problem.
1.636 +% \par The fault behind is, that we have no well error handling on one side and
1.637 +% no sufficient formed equation solving on the other side. This two facts are
1.638 +% making the implemention of new material very difficult.
1.639 +%
1.640 +% \subsection{Formalization of missing knowledge in Isabelle}
1.641 +%
1.642 +% \paragraph{A problem} behind is the mechanization of mathematic
1.643 +% theories in TP-bases languages. There is still a huge gap between
1.644 +% these algorithms and this what we want as a solution - in Example
1.645 +% Signal Processing.
1.646 +%
1.647 +% \vbox{
1.648 +% \begin{example}
1.649 +% \label{eg:gap}
1.650 +% \[
1.651 +% X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1.652 +% \]
1.653 +% {\small\textit{
1.654 +% \noindent A very simple example on this what we call gap is the
1.655 +% simplification above. It is needles to say that it is correct and also
1.656 +% Isabelle for fills it correct - \emph{always}. But sometimes we don't
1.657 +% want expand such terms, sometimes we want another structure of
1.658 +% them. Think of a problem were we now would need only the coefficients
1.659 +% of $X$ and $Y$. This is what we call the gap between mechanical
1.660 +% simplification and the solution.
1.661 +% }}
1.662 +% \end{example}
1.663 +% }
1.664 +%
1.665 +% \paragraph{We are not able to fill this gap,} until we have to live
1.666 +% with it but first have a look on the meaning of this statement:
1.667 +% Mechanized math starts from mathematical models and \emph{hopefully}
1.668 +% proceeds to match physics. Academic engineering starts from physics
1.669 +% (experimentation, measurement) and then proceeds to mathematical
1.670 +% modeling and formalization. The process from a physical observance to
1.671 +% a mathematical theory is unavoidable bound of setting up a big
1.672 +% collection of standards, rules, definition but also exceptions. These
1.673 +% are the things making mechanization that difficult.
1.674 +%
1.675 +% \vbox{
1.676 +% \begin{example}
1.677 +% \label{eg:units}
1.678 +% \[
1.679 +% m,\ kg,\ s,\ldots
1.680 +% \]
1.681 +% {\small\textit{
1.682 +% \noindent Think about some units like that one's above. Behind
1.683 +% each unit there is a discerning and very accurate definition: One
1.684 +% Meter is the distance the light travels, in a vacuum, through the time
1.685 +% of 1 / 299.792.458 second; one kilogram is the weight of a
1.686 +% platinum-iridium cylinder in paris; and so on. But are these
1.687 +% definitions usable in a computer mechanized world?!
1.688 +% }}
1.689 +% \end{example}
1.690 +% }
1.691 +%
1.692 +% \paragraph{A computer} or a TP-System builds on programs with
1.693 +% predefined logical rules and does not know any mathematical trick
1.694 +% (follow up example \ref{eg:trick}) or recipe to walk around difficult
1.695 +% expressions.
1.696 +%
1.697 +% \vbox{
1.698 +% \begin{example}
1.699 +% \label{eg:trick}
1.700 +% \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1.701 +% \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1.702 +% \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1.703 +% \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1.704 +% {\small\textit{
1.705 +% \noindent Sometimes it is also useful to be able to apply some
1.706 +% \emph{tricks} to get a beautiful and particularly meaningful result,
1.707 +% which we are able to interpret. But as seen in this example it can be
1.708 +% hard to find out what operations have to be done to transform a result
1.709 +% into a meaningful one.
1.710 +% }}
1.711 +% \end{example}
1.712 +% }
1.713 +%
1.714 +% \paragraph{The only possibility,} for such a system, is to work
1.715 +% through its known definitions and stops if none of these
1.716 +% fits. Specified on Signal Processing or any other application it is
1.717 +% often possible to walk through by doing simple creases. This creases
1.718 +% are in general based on simple math operational but the challenge is
1.719 +% to teach the machine \emph{all}\footnote{Its pride to call it
1.720 +% \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1.721 +% reach a high level of \emph{all} but it in real it will still be a
1.722 +% survey of knowledge which links to other knowledge and {{\sisac}{}} a
1.723 +% trainer and helper but no human compensating calculator.
1.724 +% \par
1.725 +% {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1.726 +% specifications of problems out of topics from Signal Processing, etc.)
1.727 +% and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1.728 +% physical knowledge. The result is a three-dimensional universe of
1.729 +% mathematics seen in Figure~\ref{fig:mathuni}.
1.730 +%
1.731 +% \begin{figure}
1.732 +% \begin{center}
1.733 +% \includegraphics{fig/universe}
1.734 +% \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1.735 +% combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1.736 +% leads to a three dimensional math universe.\label{fig:mathuni}}
1.737 +% \end{center}
1.738 +% \end{figure}
1.739 +%
1.740 +% %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1.741 +% %WN bitte folgende Bezeichnungen nehmen:
1.742 +% %WN
1.743 +% %WN axis 1: Algorithmic Knowledge (Programs)
1.744 +% %WN axis 2: Application-oriented Knowledge (Specifications)
1.745 +% %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1.746 +% %WN
1.747 +% %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1.748 +% %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1.749 +% %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1.750 +%
1.751 +% %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1.752 +% %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1.753 +% %JR gefordert werden WN2...
1.754 +% %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1.755 +% %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1.756 +% %WN2 zusammenschneiden um die R"ander weg zu bekommen)
1.757 +% %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1.758 +% %WN2 png + pdf figures mitzuschicken.
1.759 +%
1.760 +% \subsection{Notes on Problems with Traditional Notation}
1.761 +%
1.762 +% \paragraph{During research} on these topic severely problems on
1.763 +% traditional notations have been discovered. Some of them have been
1.764 +% known in computer science for many years now and are still unsolved,
1.765 +% one of them aggregates with the so called \emph{Lambda Calculus},
1.766 +% Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1.767 +% us.
1.768 +%
1.769 +% \vbox{
1.770 +% \begin{example}
1.771 +% \label{eg:lamda}
1.772 +%
1.773 +% \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1.774 +%
1.775 +%
1.776 +% \[ f(p)=\ldots\; p \in \quad R \]
1.777 +%
1.778 +% {\small\textit{
1.779 +% \noindent Above we see two equations. The first equation aims to
1.780 +% be a mapping of an function from the reel range to the reel one, but
1.781 +% when we change only one letter we get the second equation which
1.782 +% usually aims to insert a reel point $p$ into the reel function. In
1.783 +% computer science now we have the problem to tell the machine (TP) the
1.784 +% difference between this two notations. This Problem is called
1.785 +% \emph{Lambda Calculus}.
1.786 +% }}
1.787 +% \end{example}
1.788 +% }
1.789 +%
1.790 +% \paragraph{An other problem} is that terms are not full simplified in
1.791 +% traditional notations, in {{\sisac}} we have to simplify them complete
1.792 +% to check weather results are compatible or not. in e.g. the solutions
1.793 +% of an second order linear equation is an rational in {{\sisac}} but in
1.794 +% tradition we keep fractions as long as possible and as long as they
1.795 +% aim to be \textit{beautiful} (1/8, 5/16,...).
1.796 +% \subparagraph{The math} which should be mechanized in Computer Theorem
1.797 +% Provers (\emph{TP}) has (almost) a problem with traditional notations
1.798 +% (predicate calculus) for axioms, definitions, lemmas, theorems as a
1.799 +% computer program or script is not able to interpret every Greek or
1.800 +% Latin letter and every Greek, Latin or whatever calculations
1.801 +% symbol. Also if we would be able to handle these symbols we still have
1.802 +% a problem to interpret them at all. (Follow up \hbox{Example
1.803 +% \ref{eg:symbint1}})
1.804 +%
1.805 +% \vbox{
1.806 +% \begin{example}
1.807 +% \label{eg:symbint1}
1.808 +% \[
1.809 +% u\left[n\right] \ \ldots \ unitstep
1.810 +% \]
1.811 +% {\small\textit{
1.812 +% \noindent The unitstep is something we need to solve Signal
1.813 +% Processing problem classes. But in {{{\sisac}{}}} the rectangular
1.814 +% brackets have a different meaning. So we abuse them for our
1.815 +% requirements. We get something which is not defined, but usable. The
1.816 +% Result is syntax only without semantic.
1.817 +% }}
1.818 +% \end{example}
1.819 +% }
1.820 +%
1.821 +% In different problems, symbols and letters have different meanings and
1.822 +% ask for different ways to get through. (Follow up \hbox{Example
1.823 +% \ref{eg:symbint2}})
1.824 +%
1.825 +% \vbox{
1.826 +% \begin{example}
1.827 +% \label{eg:symbint2}
1.828 +% \[
1.829 +% \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1.830 +% \]
1.831 +% {\small\textit{
1.832 +% \noindent For using exponents the three \texttt{widehat} symbols
1.833 +% are required. The reason for that is due the development of
1.834 +% {{{\sisac}{}}} the single \texttt{widehat} and also the double were
1.835 +% already in use for different operations.
1.836 +% }}
1.837 +% \end{example}
1.838 +% }
1.839 +%
1.840 +% \paragraph{Also the output} can be a problem. We are familiar with a
1.841 +% specified notations and style taught in university but a computer
1.842 +% program has no knowledge of the form proved by a professor and the
1.843 +% machines themselves also have not yet the possibilities to print every
1.844 +% symbol (correct) Recent developments provide proofs in a human
1.845 +% readable format but according to the fact that there is no money for
1.846 +% good working formal editors yet, the style is one thing we have to
1.847 +% live with.
1.848 +%
1.849 +% \section{Problems rising out of the Development Environment}
1.850 +%
1.851 +% fehlermeldungen! TODO
1.852
1.853 \section{Conclusion}\label{conclusion}
1.854