1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Wed Sep 05 11:55:10 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 06 21:54:54 2012 +0200
1.3 @@ -169,10 +169,10 @@
1.4
1.5 \section{Introduction}\label{intro}
1.6
1.7 -% \paragraph{Didactics of mathematics}
1.8 -%WN: wenn man in einem high-quality paper von 'didactics' spricht,
1.9 -%WN muss man am state-of-the-art ankn"upfen -- siehe
1.10 -%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
1.11 +% \paragraph{Didactics of mathematics}
1.12 +%WN: wenn man in einem high-quality paper von 'didactics' spricht,
1.13 +%WN muss man am state-of-the-art ankn"upfen -- siehe
1.14 +%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
1.15 % faces a specific issue, a gap
1.16 % between (1) introduction of math concepts and skills and (2)
1.17 % application of these concepts and skills, which usually are separated
1.18 @@ -197,16 +197,16 @@
1.19 % Signal Processing and Speech Communication (SPSC), the Institute for
1.20 % Structural Analysis and the Institute of Electrical Measurement and
1.21 % Measurement Signal Processing.
1.22 -%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
1.23 -%WN und damit zu verg"anglich.
1.24 +%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
1.25 +%WN und damit zu verg"anglich.
1.26 % \par This thesis is the first attempt to tackle the above mentioned
1.27 % issue, it focuses on Telematics, because these specific studies focus
1.28 % on mathematics in \emph{STEOP}, the introductory orientation phase in
1.29 % Austria. \emph{STEOP} is considered an opportunity to investigate the
1.30 % impact of {\sisac}'s prototype on the issue and others.
1.31 %
1.32 -
1.33 -Traditional course material in engineering disciplines lacks an
1.34 +
1.35 +\paragraph{Traditional course material} in engineering disciplines lacks an
1.36 important component, interactive support for step-wise problem
1.37 solving. Theorem-Proving (TP) technology can provide such support by
1.38 specific services. An important part of such services is called
1.39 @@ -222,7 +222,7 @@
1.40 interpreter will be briefly re-introduced in order to make the paper
1.41 self-contained.
1.42
1.43 -\medskip The main part of the paper is an account of first experiences
1.44 +\subparagraph{The main part} of the paper is an account of first experiences
1.45 with programming in this TP-based language. The experience was gained
1.46 in a case study by the author. The author was considered an ideal
1.47 candidate for this study for the following reasons: as a student in
1.48 @@ -232,29 +232,30 @@
1.49 {\sisac}'s programming language and interpeter, thus a novice to the
1.50 language.
1.51
1.52 -The goal of the case study was (1) some TP-based programs for
1.53 +\subparagraph{The goal} of the case study was (1) some TP-based programs for
1.54 interactive course material for a specific ``Adavanced Signal
1.55 Processing Lab'' in a higher semester, (2) respective program
1.56 development with as little advice from the {\sisac}-team and (3) records
1.57 and comments for the main steps of development in an Isabelle theory;
1.58 this theory should provide guidelines for future programmers. An
1.59 excerpt from this theory is the main part of this paper.
1.60 -
1.61 -\medskip The paper will use the problem in Fig.\ref{fig-interactive} as a
1.62 +\par
1.63 +The paper will use the problem in Fig.\ref{fig-interactive} as a
1.64 running example:
1.65 \begin{figure} [htb]
1.66 \begin{center}
1.67 -\includegraphics[width=120mm]{fig/isac-Ztrans-math.png}
1.68 +\includegraphics[width=140mm]{fig/isac-Ztrans-math}
1.69 \caption{Step-wise problem solving guided by the TP-based program}
1.70 \label{fig-interactive}
1.71 \end{center}
1.72 \end{figure}
1.73 -The problem is from the domain of Signal Processing and requests to
1.74 +
1.75 +\paragraph{The problem is} from the domain of Signal Processing and requests to
1.76 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
1.77 also shows the beginning of the interactive construction of a solution
1.78 for the problem. This construction is done in the right window named
1.79 ``Worksheet''.
1.80 -
1.81 +\par
1.82 User-interaction on the Worksheet is {\em checked} and {\em guided} by
1.83 TP services:
1.84 \begin{enumerate}
1.85 @@ -272,14 +273,14 @@
1.86 see that the program contains neither input-statements nor
1.87 output-statements. Rather, interaction is handled by services
1.88 generated automatically.
1.89 -
1.90 -\medskip So there is a clear separation of concerns: Dialogues are
1.91 +\par
1.92 +So there is a clear separation of concerns: Dialogues are
1.93 adapted by dialogue authors (in Java-based tools), using automatically
1.94 generated TP services, while the TP-based program is written by
1.95 mathematics experts (in Isabelle/ML). The latter is concern of this
1.96 paper.
1.97 -
1.98 -\medskip The paper is structed as follows: The introduction
1.99 +
1.100 +\paragraph{The paper is structed} as follows: The introduction
1.101 \S\ref{intro} is followed by a brief re-introduction of the TP-based
1.102 programming language in \S\ref{PL}, which extends the executable
1.103 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
1.104 @@ -345,6 +346,8 @@
1.105 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
1.106 % x. \; x$ is the identity function.
1.107
1.108 +%JR warum auskommentiert?
1.109 +
1.110 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
1.111 constants \textit{True} and \textit{False} and the usual logical
1.112 connectives (in decreasing order of precedence): $\neg, \land, \lor,
1.113 @@ -449,21 +452,21 @@
1.114
1.115 .\\.\\.\\TODO\\.\\.\\
1.116
1.117 -\section{Development of a Program on Trial}\label{trial}
1.118 -As mentioned above, {\sisac} is an experimental system for a proof of
1.119 -concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
1.120 -latter interprets a specific kind of TP-based programming language,
1.121 -which is as experimental as the whole prototype --- so programming in
1.122 -this language can be only ``on trial'', presently. However, as a
1.123 -prototype, the language addresses essentials described below.
1.124 -
1.125 -\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
1.126 -
1.127 -%WN was Fachleute unter obigem Titel interessiert findet
1.128 -%WN unterhalb des auskommentierten Textes.
1.129 -
1.130 -%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
1.131 -%WN auf Computer-Mathematiker fokussiert.
1.132 +\section{Development of a Program on Trial}\label{trial}
1.133 +As mentioned above, {\sisac} is an experimental system for a proof of
1.134 +concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
1.135 +latter interprets a specific kind of TP-based programming language,
1.136 +which is as experimental as the whole prototype --- so programming in
1.137 +this language can be only ``on trial'', presently. However, as a
1.138 +prototype, the language addresses essentials described below.
1.139 +
1.140 +\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
1.141 +
1.142 +%WN was Fachleute unter obigem Titel interessiert findet
1.143 +%WN unterhalb des auskommentierten Textes.
1.144 +
1.145 +%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
1.146 +%WN auf Computer-Mathematiker fokussiert.
1.147 % \paragraph{As mentioned in the introduction,} a prototype of an
1.148 % educational math assistant called
1.149 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
1.150 @@ -493,128 +496,128 @@
1.151 %
1.152 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
1.153 %
1.154 -% \paragraph{Educational software in mathematics} is, if at all, based
1.155 -% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
1.156 -% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
1.157 -% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
1.158 -% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
1.159 -% base technologies are used to program math lessons and sometimes even
1.160 -% exercises. The latter are cumbersome: the steps towards a solution of
1.161 -% such an interactive exercise need to be provided with feedback, where
1.162 -% at each step a wide variety of possible input has to be foreseen by
1.163 -% the programmer - so such interactive exercises either require high
1.164 +% \paragraph{Educational software in mathematics} is, if at all, based
1.165 +% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
1.166 +% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
1.167 +% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
1.168 +% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
1.169 +% base technologies are used to program math lessons and sometimes even
1.170 +% exercises. The latter are cumbersome: the steps towards a solution of
1.171 +% such an interactive exercise need to be provided with feedback, where
1.172 +% at each step a wide variety of possible input has to be foreseen by
1.173 +% the programmer - so such interactive exercises either require high
1.174 % development efforts or the exercises constrain possible inputs.
1.175 %
1.176 -% \subparagraph{A new generation} of educational math assistants (EMAs)
1.177 -% is emerging presently, which is based on Theorem Proving (TP). TP, for
1.178 -% instance Isabelle and Coq, is a technology which requires each fact
1.179 -% and each action justified by formal logic. Pushed by demands for
1.180 -% \textit{proven} correctness of safety-critical software TP advances
1.181 -% into software engineering; from these advancements computer
1.182 -% mathematics benefits in general, and math education in particular. Two
1.183 +% \subparagraph{A new generation} of educational math assistants (EMAs)
1.184 +% is emerging presently, which is based on Theorem Proving (TP). TP, for
1.185 +% instance Isabelle and Coq, is a technology which requires each fact
1.186 +% and each action justified by formal logic. Pushed by demands for
1.187 +% \textit{proven} correctness of safety-critical software TP advances
1.188 +% into software engineering; from these advancements computer
1.189 +% mathematics benefits in general, and math education in particular. Two
1.190 % features of TP are immediately beneficial for learning:
1.191 %
1.192 -% \paragraph{TP have knowledge in human readable format,} that is in
1.193 -% standard predicate calculus. TP following the LCF-tradition have that
1.194 -% knowledge down to the basic definitions of set, equality,
1.195 -% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
1.196 -% following the typical deductive development of math, natural numbers
1.197 -% are defined and their properties
1.198 -% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
1.199 -% etc. Present knowledge mechanized in TP exceeds high-school
1.200 -% mathematics by far, however by knowledge required in software
1.201 +% \paragraph{TP have knowledge in human readable format,} that is in
1.202 +% standard predicate calculus. TP following the LCF-tradition have that
1.203 +% knowledge down to the basic definitions of set, equality,
1.204 +% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
1.205 +% following the typical deductive development of math, natural numbers
1.206 +% are defined and their properties
1.207 +% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
1.208 +% etc. Present knowledge mechanized in TP exceeds high-school
1.209 +% mathematics by far, however by knowledge required in software
1.210 % technology, and not in other engineering sciences.
1.211 %
1.212 -% \paragraph{TP can model the whole problem solving process} in
1.213 -% mathematical problem solving {\em within} a coherent logical
1.214 -% framework. This is already being done by three projects, by
1.215 +% \paragraph{TP can model the whole problem solving process} in
1.216 +% mathematical problem solving {\em within} a coherent logical
1.217 +% framework. This is already being done by three projects, by
1.218 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
1.219 % \par
1.220 -% Having the whole problem solving process within a logical coherent
1.221 -% system, such a design guarantees correctness of intermediate steps and
1.222 -% of the result (which seems essential for math software); and the
1.223 -% second advantage is that TP provides a wealth of theories which can be
1.224 -% exploited for mechanizing other features essential for educational
1.225 +% Having the whole problem solving process within a logical coherent
1.226 +% system, such a design guarantees correctness of intermediate steps and
1.227 +% of the result (which seems essential for math software); and the
1.228 +% second advantage is that TP provides a wealth of theories which can be
1.229 +% exploited for mechanizing other features essential for educational
1.230 % software.
1.231 %
1.232 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
1.233 %
1.234 -% One essential feature for educational software is feedback to user
1.235 +% One essential feature for educational software is feedback to user
1.236 % input and assistance in coming to a solution.
1.237 %
1.238 -% \paragraph{Checking user input} by ATP during stepwise problem solving
1.239 -% is being accomplished by the three projects mentioned above
1.240 -% exclusively. They model the whole problem solving process as mentioned
1.241 -% above, so all what happens between formalized assumptions (or formal
1.242 -% specification) and goal (or fulfilled postcondition) can be
1.243 -% mechanized. Such mechanization promises to greatly extend the scope of
1.244 +% \paragraph{Checking user input} by ATP during stepwise problem solving
1.245 +% is being accomplished by the three projects mentioned above
1.246 +% exclusively. They model the whole problem solving process as mentioned
1.247 +% above, so all what happens between formalized assumptions (or formal
1.248 +% specification) and goal (or fulfilled postcondition) can be
1.249 +% mechanized. Such mechanization promises to greatly extend the scope of
1.250 % educational software in stepwise problem solving.
1.251 %
1.252 -% \paragraph{NSG (Next step guidance)} comprises the system's ability to
1.253 -% propose a next step; this is a challenge for TP: either a radical
1.254 -% restriction of the search space by restriction to very specific
1.255 -% problem classes is required, or much care and effort is required in
1.256 -% designing possible variants in the process of problem solving
1.257 +% \paragraph{NSG (Next step guidance)} comprises the system's ability to
1.258 +% propose a next step; this is a challenge for TP: either a radical
1.259 +% restriction of the search space by restriction to very specific
1.260 +% problem classes is required, or much care and effort is required in
1.261 +% designing possible variants in the process of problem solving
1.262 % \cite{proof-strategies-11}.
1.263 % \par
1.264 -% Another approach is restricted to problem solving in engineering
1.265 -% domains, where a problem is specified by input, precondition, output
1.266 -% and postcondition, and where the postcondition is proven by ATP behind
1.267 -% the scenes: Here the possible variants in the process of problem
1.268 -% solving are provided with feedback {\em automatically}, if the problem
1.269 -% is described in a TP-based programing language: \cite{plmms10} the
1.270 -% programmer only describes the math algorithm without caring about
1.271 -% interaction (the respective program is functional and even has no
1.272 -% input or output statements!); interaction is generated as a
1.273 -% side-effect by the interpreter --- an efficient separation of concern
1.274 -% between math programmers and dialog designers promising application
1.275 +% Another approach is restricted to problem solving in engineering
1.276 +% domains, where a problem is specified by input, precondition, output
1.277 +% and postcondition, and where the postcondition is proven by ATP behind
1.278 +% the scenes: Here the possible variants in the process of problem
1.279 +% solving are provided with feedback {\em automatically}, if the problem
1.280 +% is described in a TP-based programing language: \cite{plmms10} the
1.281 +% programmer only describes the math algorithm without caring about
1.282 +% interaction (the respective program is functional and even has no
1.283 +% input or output statements!); interaction is generated as a
1.284 +% side-effect by the interpreter --- an efficient separation of concern
1.285 +% between math programmers and dialog designers promising application
1.286 % all over engineering disciplines.
1.287 %
1.288 %
1.289 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
1.290 -% Authoring new mathematics knowledge in {{\sisac}} can be compared with
1.291 -% ``application programing'' of engineering problems; most of such
1.292 -% programing uses CAS-based programing languages (CAS = Computer Algebra
1.293 +% Authoring new mathematics knowledge in {{\sisac}} can be compared with
1.294 +% ``application programing'' of engineering problems; most of such
1.295 +% programing uses CAS-based programing languages (CAS = Computer Algebra
1.296 % Systems; e.g. Mathematica's or Maple's programing language).
1.297 %
1.298 -% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
1.299 -% \cite{plmms10} for describing how to construct a solution to an
1.300 -% engineering problem and for calling equation solvers, integration,
1.301 -% etc~\footnote{Implementation of CAS-like functionality in TP is not
1.302 -% primarily concerned with efficiency, but with a didactic question:
1.303 -% What to decide for: for high-brow algorithms at the state-of-the-art
1.304 -% or for elementary algorithms comprehensible for students?} within TP;
1.305 -% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
1.306 +% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
1.307 +% \cite{plmms10} for describing how to construct a solution to an
1.308 +% engineering problem and for calling equation solvers, integration,
1.309 +% etc~\footnote{Implementation of CAS-like functionality in TP is not
1.310 +% primarily concerned with efficiency, but with a didactic question:
1.311 +% What to decide for: for high-brow algorithms at the state-of-the-art
1.312 +% or for elementary algorithms comprehensible for students?} within TP;
1.313 +% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
1.314 % are impossible for CAS which have no logics underlying.
1.315 %
1.316 -% \subparagraph{Authoring is perfect} by writing such TP based programs;
1.317 -% the application programmer is not concerned with interaction or with
1.318 -% user guidance: this is concern of a novel kind of program interpreter
1.319 -% called Lucas-Interpreter. This interpreter hands over control to a
1.320 -% dialog component at each step of calculation (like a debugger at
1.321 -% breakpoints) and calls automated TP to check user input following
1.322 +% \subparagraph{Authoring is perfect} by writing such TP based programs;
1.323 +% the application programmer is not concerned with interaction or with
1.324 +% user guidance: this is concern of a novel kind of program interpreter
1.325 +% called Lucas-Interpreter. This interpreter hands over control to a
1.326 +% dialog component at each step of calculation (like a debugger at
1.327 +% breakpoints) and calls automated TP to check user input following
1.328 % personalized strategies according to a feedback module.
1.329 % \par
1.330 -% However ``application programing with TP'' is not done with writing a
1.331 -% program: according to the principles of TP, each step must be
1.332 -% justified. Such justifications are given by theorems. So all steps
1.333 -% must be related to some theorem, if there is no such theorem it must
1.334 -% be added to the existing knowledge, which is organized in so-called
1.335 -% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
1.336 -% Isabelle comprises a mechanism (called ``axiomatization''), which
1.337 -% allows to omit proofs. Such a theorem is shown in
1.338 +% However ``application programing with TP'' is not done with writing a
1.339 +% program: according to the principles of TP, each step must be
1.340 +% justified. Such justifications are given by theorems. So all steps
1.341 +% must be related to some theorem, if there is no such theorem it must
1.342 +% be added to the existing knowledge, which is organized in so-called
1.343 +% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
1.344 +% Isabelle comprises a mechanism (called ``axiomatization''), which
1.345 +% allows to omit proofs. Such a theorem is shown in
1.346 % Example~\ref{eg:neuper1}.
1.347 -
1.348 -The running example, introduced by Fig.\ref{fig-interactive} on
1.349 -p.\pageref{fig-interactive}, requires to determine the inverse $\cal
1.350 -Z$-transform for a class of functions. The domain of Signal Processing
1.351 -is accustomed to specific notation for the resulting functions, which
1.352 -are absolutely summable and are called TODO: $u[n]$, where $u$ is the
1.353 -function, $n$ is the argument and the brackets indicate that the
1.354 -arguments are TODO. Surprisingly, Isabelle accepts the rules for
1.355 -${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
1.356 -experts might be particularly surprised, that the brackets do not
1.357 -cause errors in typing (as lists).}:
1.358 +
1.359 +The running example, introduced by Fig.\ref{fig-interactive} on
1.360 +p.\pageref{fig-interactive}, requires to determine the inverse $\cal
1.361 +Z$-transform for a class of functions. The domain of Signal Processing
1.362 +is accustomed to specific notation for the resulting functions, which
1.363 +are absolutely summable and are called TODO: $u[n]$, where $u$ is the
1.364 +function, $n$ is the argument and the brackets indicate that the
1.365 +arguments are TODO. Surprisingly, Isabelle accepts the rules for
1.366 +${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
1.367 +experts might be particularly surprised, that the brackets do not
1.368 +cause errors in typing (as lists).}:
1.369 %\vbox{
1.370 % \begin{example}
1.371 \label{eg:neuper1}
1.372 @@ -624,187 +627,172 @@
1.373 \>axiomatization where \\
1.374 \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
1.375 \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
1.376 - \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
1.377 %TODO
1.378 - \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
1.379 %TODO
1.380 - \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
1.381 %TODO
1.382 - \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
1.383 %TODO
1.384 + \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
1.385 +%TODO
1.386 + \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
1.387 +%TODO
1.388 + \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
1.389 +%TODO
1.390 + \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
1.391 +%TODO
1.392 \end{tabbing}
1.393 }
1.394 % \end{example}
1.395 -%}
1.396 -These 6 rules can be used as conditional rewrite rules, depending on
1.397 -the respective convergence radius. Satisfaction from accordance with traditional notation
1.398 -contrasts with the above word {\em axiomatization}: As TP-based, the
1.399 -programming language expects these rules as {\em proved} theorems, and
1.400 -not as axioms implemented in the above brute force manner; otherwise
1.401 -all the verification efforts envisaged (like proof of the
1.402 -post-condition, see below) would be meaningless.
1.403 -
1.404 -Isabelle provides a large body of knowledge, rigorously proven from
1.405 -the basic axioms of mathematics~\footnote{This way of rigorously
1.406 -deriving all knowledge from first principles is called the
1.407 -LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
1.408 -knowledge can be found in the theoris on Multivariate
1.409 -Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
1.410 -building up knowledge such that a proof for the above rules would be
1.411 -reasonably short and easily comprehensible, still requires lots of
1.412 -work (and is definitely out of scope of our case study).
1.413 -
1.414 -\medskip At the state-of-the-art in mechanization of knowledge in
1.415 -engineering sciences, the process does not stop with the mechanization of
1.416 -mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
1.417 -are expected to proceed to formal and explicit description of physical items. Signal Processing,
1.418 -for instance is concerned with physical devices for signal acquisition
1.419 -and reconstruction, which involve measuring a physical signal, storing
1.420 -it, and possibly later rebuilding the original signal or an
1.421 -approximation thereof. For digital systems, this typically includes
1.422 -sampling and quantization; devices for signal compression, including
1.423 -audio compression, image compression, and video compression, etc.
1.424 -``Domain engineering''\cite{db-domain-engineering} is concerned with
1.425 -{\em specification} of these devices' components and features; this
1.426 -part in the process of mechanization is only at the beginning in domains
1.427 -like Signal Processing.
1.428 -
1.429 -\medskip TP-based programming, concern of this paper, is determined to
1.430 -add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
1.431 -p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.432 -starts with a formal {\em specification} of the problem to be solved.
1.433 -
1.434 - \begin{figure}
1.435 - \hfill \\
1.436 - \begin{center}
1.437 - \includegraphics{fig/universe}
1.438 - \caption{Didactic ``Math-Universe''\label{fig:mathuni}}
1.439 - \end{center}
1.440 - \end{figure}
1.441 -%WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1.442 -%WN bitte folgende Bezeichnungen nehmen:
1.443 -%WN
1.444 -%WN axis 1: Algorithmic Knowledge (Programs)
1.445 -%WN axis 2: Application-oriented Knowledge (Specifications)
1.446 -%WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1.447 -%WN
1.448 -%WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1.449 -%WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1.450 -%WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1.451 -
1.452 -
1.453 -\subsection{Specification of the Problem}\label{spec}
1.454 -%WN <--> \chapter 7 der Thesis
1.455 -%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1.456 -
1.457 -The problem of the running example is textually described in
1.458 -Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
1.459 -formal} specification of this problem, in traditional mathematical
1.460 -notation, could look lik is this:
1.461 -
1.462 --------------------------------------------------------------------------------
1.463 -
1.464 -Hier brauchen wir die Spezifikation des 'running example' ...
1.465 -
1.466 --------------------------------------------------------------------------------
1.467 +%}
1.468 +These 6 rules can be used as conditional rewrite rules, depending on
1.469 +the respective convergence radius. Satisfaction from accordance with traditional notation
1.470 +contrasts with the above word {\em axiomatization}: As TP-based, the
1.471 +programming language expects these rules as {\em proved} theorems, and
1.472 +not as axioms implemented in the above brute force manner; otherwise
1.473 +all the verification efforts envisaged (like proof of the
1.474 +post-condition, see below) would be meaningless.
1.475 +
1.476 +Isabelle provides a large body of knowledge, rigorously proven from
1.477 +the basic axioms of mathematics~\footnote{This way of rigorously
1.478 +deriving all knowledge from first principles is called the
1.479 +LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
1.480 +knowledge can be found in the theoris on Multivariate
1.481 +Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
1.482 +building up knowledge such that a proof for the above rules would be
1.483 +reasonably short and easily comprehensible, still requires lots of
1.484 +work (and is definitely out of scope of our case study).
1.485 +
1.486 +\paragraph{At the state-of-the-art in mechanization of knowledge} in
1.487 +engineering sciences, the process does not stop with the mechanization of
1.488 +mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
1.489 +are expected to proceed to formal and explicit description of physical items. Signal Processing,
1.490 +for instance is concerned with physical devices for signal acquisition
1.491 +and reconstruction, which involve measuring a physical signal, storing
1.492 +it, and possibly later rebuilding the original signal or an
1.493 +approximation thereof. For digital systems, this typically includes
1.494 +sampling and quantization; devices for signal compression, including
1.495 +audio compression, image compression, and video compression, etc.
1.496 +``Domain engineering''\cite{db-domain-engineering} is concerned with
1.497 +{\em specification} of these devices' components and features; this
1.498 +part in the process of mechanization is only at the beginning in domains
1.499 +like Signal Processing.
1.500 +
1.501 +\subparagraph{TP-based programming, concern of this paper,} is determined to
1.502 +add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
1.503 +p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.504 +starts with a formal {\em specification} of the problem to be solved.
1.505 +
1.506 +
1.507 +\subsection{Specification of the Problem}\label{spec}
1.508 +%WN <--> \chapter 7 der Thesis
1.509 +%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1.510 +
1.511 +The problem of the running example is textually described in
1.512 +Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
1.513 +formal} specification of this problem, in traditional mathematical
1.514 +notation, could look lik is this:
1.515 +
1.516 +%WN Hier brauchen wir die Spezifikation des 'running example' ...
1.517 +
1.518 +%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1.519 +%JR der post condition - die existiert für uns ja eigentlich nicht aka
1.520 +%JR haben sie bis jetzt nicht beachtet
1.521 +
1.522 \label{eg:neuper2}
1.523 {\small\begin{tabbing}
1.524 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1.525 \hfill \\
1.526 Specification:\\
1.527 - %\>input\>: $\{\;r={\it arbitraryFix}\;\}$ \\
1.528 - \>input \>: $\{\;r\;\}$ \\
1.529 - \>precond \>: $0 < r$ \\
1.530 - \>output \>: $\{\;A,\; u,v\;\}$ \\
1.531 + \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
1.532 + \>precond \>: filterExpression continius on $\mathbb{R}$ \\
1.533 + \>output \>: stepResponse $x[n]$ \\
1.534 \>postcond \>:{\small $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\
1.535 \> \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land
1.536 (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\
1.537 -% \>props\>: $\{\;A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\;\}$
1.538 \end{tabbing}
1.539 }
1.540 -
1.541 -And this is the implementation of the formal specification in the present
1.542 -prototype, still bar-bones without support for authoring:
1.543 -%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1.544 -{\footnotesize
1.545 -\begin{verbatim}
1.546 - 01 store_specification
1.547 - 02 (prepare_specification
1.548 - 03 ["Jan Rocnik"]
1.549 - 04 "pbl_SP_Ztrans_inv"
1.550 - 05 thy
1.551 - 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1.552 - 07 [ ("#Given", ["filterExpression X_eq"]),
1.553 - 08 ("#Pre" , ["X_eq is_continuous"]),
1.554 - 19 ("#Find" , ["stepResponse n_eq"]),
1.555 - 10 ("#Post" , [" TODO "])],
1.556 - 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
1.557 - 12 NONE,
1.558 - 13 [["SignalProcessing","Z_Transform","Inverse"]]));
1.559 -\end{verbatim}}
1.560 -Although the above details are partly very technical, we explain them
1.561 -in order to document some intricacies of TP-based programming in the
1.562 -present state of the {\sisac} prototype:
1.563 -\begin{description}
1.564 -\item[01..02]\textit{store\_specification:} stores the result of the
1.565 -function \textit{prep\_specification} in a global reference
1.566 -\textit{Unsynchronized.ref}, which causes principal conflicts with
1.567 -Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
1.568 -parallel execution~\cite{Makarius-09:parall-proof} and is under
1.569 -reconstruction already.
1.570 -
1.571 -\textit{prep\_pbt:} translates the specification to an internal format
1.572 -which allows efficient processing; see for instance line {\rm 07}
1.573 -below.
1.574 -\item[03..04] are the ``mathematics author'' holding the copy-rights
1.575 -and a unique identifier for the specification within {\sisac},
1.576 -complare line {\rm 06}.
1.577 -\item[05] is the Isabelle \textit{theory} required to parse the
1.578 -specification in lines {\rm 07..10}.
1.579 -\item[06] is a key into the tree of all specifications as presented to
1.580 -the user (where some branches might be hidden by the dialog
1.581 -component).
1.582 -\item[07..10] are the specification with input, pre-condition, output
1.583 -and post-condition respectively; the post-condition is not handled in
1.584 -the prototype presently.
1.585 -\item[11] creates a term rewriting system (abbreviated \textit{rls} in
1.586 -{\sisac}) which evaluates the pre-condition for the actual input data.
1.587 -Only if the evaluation yields \textit{True}, a program con be started.
1.588 -\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1.589 -problem associated to a function from Computer Algebra (like an
1.590 -equation solver) which is not the case here.
1.591 -\item[13] is the specific key into the tree of programs addressing a
1.592 -method which is able to find a solution which satiesfies the
1.593 -post-condition of the specification.
1.594 -\end{description}
1.595 -
1.596 -
1.597 -%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1.598 -%WN ...
1.599 -% type pbt =
1.600 -% {guh : guh, (*unique within this isac-knowledge*)
1.601 -% mathauthors: string list, (*copyright*)
1.602 -% init : pblID, (*to start refinement with*)
1.603 -% thy : theory, (* which allows to compile that pbt
1.604 -% TODO: search generalized for subthy (ref.p.69*)
1.605 -% (*^^^ WN050912 NOT used during application of the problem,
1.606 -% because applied terms may be from 'subthy' as well as from super;
1.607 -% thus we take 'maxthy'; see match_ags !*)
1.608 -% cas : term option,(*'CAS-command'*)
1.609 -% prls : rls, (* for preds in where_*)
1.610 -% where_: term list, (* where - predicates*)
1.611 -% ppc : pat list,
1.612 -% (*this is the model-pattern;
1.613 -% it contains "#Given","#Where","#Find","#Relate"-patterns
1.614 -% for constraints on identifiers see "fun cpy_nam"*)
1.615 -% met : metID list}; (* methods solving the pbt*)
1.616 -%
1.617 -%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1.618 -%WN oben selbst geschrieben.
1.619 -
1.620 -
1.621 -
1.622 -
1.623 -%WN das w"urde ich in \sec\label{progr} verschieben und
1.624 -%WN das SubProblem partial fractions zum Erkl"aren verwenden.
1.625 -% Such a specification is checked before the execution of a program is
1.626 -% started, the same applies for sub-programs. In the following example
1.627 +
1.628 +And this is the implementation of the formal specification in the present
1.629 +prototype, still bar-bones without support for authoring:
1.630 +%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1.631 +{\footnotesize
1.632 +\begin{verbatim}
1.633 + 01 store_specification
1.634 + 02 (prepare_specification
1.635 + 03 ["Jan Rocnik"]
1.636 + 04 "pbl_SP_Ztrans_inv"
1.637 + 05 thy
1.638 + 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1.639 + 07 [ ("#Given", ["filterExpression X_eq"]),
1.640 + 08 ("#Pre" , ["X_eq is_continuous"]),
1.641 + 19 ("#Find" , ["stepResponse n_eq"]),
1.642 + 10 ("#Post" , [" TODO "])],
1.643 + 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
1.644 + 12 NONE,
1.645 + 13 [["SignalProcessing","Z_Transform","Inverse"]]));
1.646 +\end{verbatim}}
1.647 +Although the above details are partly very technical, we explain them
1.648 +in order to document some intricacies of TP-based programming in the
1.649 +present state of the {\sisac} prototype:
1.650 +\begin{description}
1.651 +\item[01..02]\textit{store\_specification:} stores the result of the
1.652 +function \textit{prep\_specification} in a global reference
1.653 +\textit{Unsynchronized.ref}, which causes principal conflicts with
1.654 +Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
1.655 +parallel execution~\cite{Makarius-09:parall-proof} and is under
1.656 +reconstruction already.
1.657 +
1.658 +\textit{prep\_pbt:} translates the specification to an internal format
1.659 +which allows efficient processing; see for instance line {\rm 07}
1.660 +below.
1.661 +\item[03..04] are the ``mathematics author'' holding the copy-rights
1.662 +and a unique identifier for the specification within {\sisac},
1.663 +complare line {\rm 06}.
1.664 +\item[05] is the Isabelle \textit{theory} required to parse the
1.665 +specification in lines {\rm 07..10}.
1.666 +\item[06] is a key into the tree of all specifications as presented to
1.667 +the user (where some branches might be hidden by the dialog
1.668 +component).
1.669 +\item[07..10] are the specification with input, pre-condition, output
1.670 +and post-condition respectively; the post-condition is not handled in
1.671 +the prototype presently.
1.672 +\item[11] creates a term rewriting system (abbreviated \textit{rls} in
1.673 +{\sisac}) which evaluates the pre-condition for the actual input data.
1.674 +Only if the evaluation yields \textit{True}, a program con be started.
1.675 +\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1.676 +problem associated to a function from Computer Algebra (like an
1.677 +equation solver) which is not the case here.
1.678 +\item[13] is the specific key into the tree of programs addressing a
1.679 +method which is able to find a solution which satiesfies the
1.680 +post-condition of the specification.
1.681 +\end{description}
1.682 +
1.683 +
1.684 +%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1.685 +%WN ...
1.686 +% type pbt =
1.687 +% {guh : guh, (*unique within this isac-knowledge*)
1.688 +% mathauthors: string list, (*copyright*)
1.689 +% init : pblID, (*to start refinement with*)
1.690 +% thy : theory, (* which allows to compile that pbt
1.691 +% TODO: search generalized for subthy (ref.p.69*)
1.692 +% (*^^^ WN050912 NOT used during application of the problem,
1.693 +% because applied terms may be from 'subthy' as well as from super;
1.694 +% thus we take 'maxthy'; see match_ags !*)
1.695 +% cas : term option,(*'CAS-command'*)
1.696 +% prls : rls, (* for preds in where_*)
1.697 +% where_: term list, (* where - predicates*)
1.698 +% ppc : pat list,
1.699 +% (*this is the model-pattern;
1.700 +% it contains "#Given","#Where","#Find","#Relate"-patterns
1.701 +% for constraints on identifiers see "fun cpy_nam"*)
1.702 +% met : metID list}; (* methods solving the pbt*)
1.703 +%
1.704 +%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1.705 +%WN oben selbst geschrieben.
1.706 +
1.707 +
1.708 +
1.709 +
1.710 +%WN das w"urde ich in \sec\label{progr} verschieben und
1.711 +%WN das SubProblem partial fractions zum Erkl"aren verwenden.
1.712 +% Such a specification is checked before the execution of a program is
1.713 +% started, the same applies for sub-programs. In the following example
1.714 % (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1.715 %
1.716 % \vbox{
1.717 @@ -819,53 +807,134 @@
1.718 % \end{tabbing}
1.719 % }
1.720 % {\small\textit{
1.721 -% \noindent If a program requires a result which has to be
1.722 -% calculated first we can use a subproblem to do so. In our specific
1.723 -% case we wanted to calculate the zeros of a fraction and used a
1.724 +% \noindent If a program requires a result which has to be
1.725 +% calculated first we can use a subproblem to do so. In our specific
1.726 +% case we wanted to calculate the zeros of a fraction and used a
1.727 % subproblem to calculate the zeros of the denominator polynom.
1.728 % }}
1.729 % \end{example}
1.730 % }
1.731 -
1.732 -\subsection{Implementation of the Method}\label{meth}
1.733 -%WN <--> \chapter 7 der Thesis
1.734 -TODO
1.735 -\subsection{Preparation of Simplifiers for the Program}\label{simp}
1.736 -TODO
1.737 -\subsection{Preparation of ML-Functions}\label{funs}
1.738 -%WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr}
1.739 -%WN brauchst
1.740 -TODO
1.741 -\subsection{Implementation of the TP-based Program}\label{progr}
1.742 -%WN <--> \chapter 8 der Thesis
1.743 -TODO
1.744 -
1.745 +
1.746 +\subsection{Implementation of the Method}\label{meth}
1.747 +%WN <--> \chapter 7 der Thesis
1.748 +TODO
1.749 +\subsection{Preparation of Simplifiers for the Program}\label{simp}
1.750 +TODO
1.751 +\subsection{Preparation of ML-Functions}\label{funs}
1.752 +%WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr}
1.753 +%WN brauchst
1.754 +TODO
1.755 +\subsection{Implementation of the TP-based Program}\label{progr}
1.756 +%WN <--> \chapter 8 der Thesis
1.757 +TODO
1.758 +
1.759 \section{Workflow of Programming in the Prototype}\label{workflow}
1.760 --------------------------------------------------------------------
1.761 -
1.762 -``workflow'' heisst: das mache ich zuerst, dann das ...
1.763 -
1.764 -\subsection{Preparations and Trials}\label{flow-prep}
1.765 -TODO ... Build\_Inverse\_Z\_Transform.thy !!!
1.766 -
1.767 -\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.768 -TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
1.769 -
1.770 -\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1.771 -TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
1.772 -
1.773 --------------------------------------------------------------------
1.774 -
1.775 -Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are
1.776 -vermutlich auf andere sections aufzuteilen.
1.777 -
1.778 --------------------------------------------------------------------
1.779 -
1.780 +%WN ``workflow'' heisst: das mache ich zuerst, dann das ...
1.781 +\subsection{Preparations and Trials}\label{flow-prep}
1.782 +\subsubsection{Trials on Notation and Termination}
1.783 +
1.784 +\paragraph{Technical notations} are a big problem for our piece of software,
1.785 +but the reason for that isn't a fault of the software itself, one of the
1.786 +troubles comes out of the fact that different technical subtopics use different
1.787 +symbols and notations for a different purpose. The most famous example for such
1.788 +a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1.789 +math). In the specific part of signal processing one of this notation issues is
1.790 +the use of brackets --- we use round brackets for analoge signals and squared
1.791 +brackets for digital samples. Also if there is no problem for us to handle this
1.792 +fact, we have to tell the machine what notation leads to wich meaning and that
1.793 +this purpose seperation is only valid for this special topic - signal
1.794 +processing.
1.795 +\subparagraph{In the programming language} itself it is not possible to declare
1.796 +fractions, exponents, absolutes and other operators or remarks in a way to make
1.797 +them pretty to read; our only posssiblilty were ASCII characters and a handfull
1.798 +greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1.799 +\par
1.800 +With the upper collected knowledge it is possible to check if we were able to
1.801 +donate all required terms and expressions.
1.802 +
1.803 +\subsubsection{Definition and Usage of Rules}
1.804 +
1.805 +\paragraph{The core} of our implemented problem is the Z-Transformation, due
1.806 +the fact that the transformation itself would require higher math which isn't
1.807 +yet avaible in our system we decided to choose the way like it is applied in
1.808 +labratory and problem classes at our university - by applying transformation
1.809 +rules (collected in transformation tables).
1.810 +\paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1.811 +use of axiomatizations like shown in Example~\ref{eg:ruledef}
1.812 +
1.813 +\begin{example}
1.814 + \label{eg:ruledef}
1.815 + \hfill\\
1.816 + \begin{verbatim}
1.817 + axiomatization where
1.818 + rule1: ``1 = $\delta$[n]'' and
1.819 + rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1.820 + rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1.821 + \end{verbatim}
1.822 +\end{example}
1.823 +
1.824 +This rules can be collected in a ruleset and applied to a given expression as
1.825 +follows in Example~\ref{eg:ruleapp}.
1.826 +
1.827 +\begin{example}
1.828 + \hfill\\
1.829 + \label{eg:ruleapp}
1.830 + \begin{enumerate}
1.831 + \item Store rules in ruleset:
1.832 + \begin{verbatim}
1.833 + val inverse_Z = append_rls "inverse_Z" e_rls
1.834 + [ Thm ("rule1",num_str @{thm rule1}),
1.835 + Thm ("rule2",num_str @{thm rule2}),
1.836 + Thm ("rule3",num_str @{thm rule3})
1.837 + ];\end{verbatim}
1.838 + \item Define exression:
1.839 + \begin{verbatim}
1.840 + val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1.841 + \item Apply ruleset:
1.842 + \begin{verbatim}
1.843 + val SOME (sample_term', asm) =
1.844 + rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1.845 + \end{enumerate}
1.846 +\end{example}
1.847 +
1.848 +The use of rulesets makes it much easier to develop our designated applications,
1.849 +but the programmer has to be careful and patient. When applying rulesets
1.850 +two important issues have to be mentionend:
1.851 +\subparagraph{How often} the rules have to be applied? In case of
1.852 +transformations it is quite clear that we use them once but other fields
1.853 +reuqire to apply rules until a special condition is reached (e.g.
1.854 +a simplification is finished when there is nothing to be done left).
1.855 +\subparagraph{The order} in which rules are applied often takes a big effect
1.856 +and has to be evaluated for each purpose once again.
1.857 +\par
1.858 +In our special case of Signal Processing and the rules defined in
1.859 +Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1.860 +constants. After this step has been done it no mather which rule fit's next.
1.861 +
1.862 +\subsubsection{Helping Functions}
1.863 +%get denom, argument in
1.864 +\subsubsection{Trials on equation solving}
1.865 +%simple eq and problem with double fractions/negative exponents
1.866 +
1.867 +
1.868 +\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.869 +TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
1.870 +
1.871 +\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1.872 +TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
1.873 +
1.874 +-------------------------------------------------------------------
1.875 +
1.876 +Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are
1.877 +vermutlich auf andere sections aufzuteilen.
1.878 +
1.879 +-------------------------------------------------------------------
1.880 +
1.881 \subsection{Formalization of missing knowledge in Isabelle}
1.882
1.883 -\paragraph{A problem} behind is the mechanization of mathematic
1.884 -theories in TP-bases languages. There is still a huge gap between
1.885 -these algorithms and this what we want as a solution - in Example
1.886 +\paragraph{A problem} behind is the mechanization of mathematic
1.887 +theories in TP-bases languages. There is still a huge gap between
1.888 +these algorithms and this what we want as a solution - in Example
1.889 Signal Processing.
1.890
1.891 \vbox{
1.892 @@ -875,25 +944,25 @@
1.893 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1.894 \]
1.895 {\small\textit{
1.896 - \noindent A very simple example on this what we call gap is the
1.897 -simplification above. It is needles to say that it is correct and also
1.898 -Isabelle for fills it correct - \emph{always}. But sometimes we don't
1.899 -want expand such terms, sometimes we want another structure of
1.900 -them. Think of a problem were we now would need only the coefficients
1.901 -of $X$ and $Y$. This is what we call the gap between mechanical
1.902 + \noindent A very simple example on this what we call gap is the
1.903 +simplification above. It is needles to say that it is correct and also
1.904 +Isabelle for fills it correct - \emph{always}. But sometimes we don't
1.905 +want expand such terms, sometimes we want another structure of
1.906 +them. Think of a problem were we now would need only the coefficients
1.907 +of $X$ and $Y$. This is what we call the gap between mechanical
1.908 simplification and the solution.
1.909 }}
1.910 \end{example}
1.911 }
1.912
1.913 -\paragraph{We are not able to fill this gap,} until we have to live
1.914 -with it but first have a look on the meaning of this statement:
1.915 -Mechanized math starts from mathematical models and \emph{hopefully}
1.916 -proceeds to match physics. Academic engineering starts from physics
1.917 -(experimentation, measurement) and then proceeds to mathematical
1.918 -modeling and formalization. The process from a physical observance to
1.919 -a mathematical theory is unavoidable bound of setting up a big
1.920 -collection of standards, rules, definition but also exceptions. These
1.921 +\paragraph{We are not able to fill this gap,} until we have to live
1.922 +with it but first have a look on the meaning of this statement:
1.923 +Mechanized math starts from mathematical models and \emph{hopefully}
1.924 +proceeds to match physics. Academic engineering starts from physics
1.925 +(experimentation, measurement) and then proceeds to mathematical
1.926 +modeling and formalization. The process from a physical observance to
1.927 +a mathematical theory is unavoidable bound of setting up a big
1.928 +collection of standards, rules, definition but also exceptions. These
1.929 are the things making mechanization that difficult.
1.930
1.931 \vbox{
1.932 @@ -903,19 +972,19 @@
1.933 m,\ kg,\ s,\ldots
1.934 \]
1.935 {\small\textit{
1.936 - \noindent Think about some units like that one's above. Behind
1.937 -each unit there is a discerning and very accurate definition: One
1.938 -Meter is the distance the light travels, in a vacuum, through the time
1.939 -of 1 / 299.792.458 second; one kilogram is the weight of a
1.940 -platinum-iridium cylinder in paris; and so on. But are these
1.941 + \noindent Think about some units like that one's above. Behind
1.942 +each unit there is a discerning and very accurate definition: One
1.943 +Meter is the distance the light travels, in a vacuum, through the time
1.944 +of 1 / 299.792.458 second; one kilogram is the weight of a
1.945 +platinum-iridium cylinder in paris; and so on. But are these
1.946 definitions usable in a computer mechanized world?!
1.947 }}
1.948 \end{example}
1.949 }
1.950
1.951 -\paragraph{A computer} or a TP-System builds on programs with
1.952 -predefined logical rules and does not know any mathematical trick
1.953 -(follow up example \ref{eg:trick}) or recipe to walk around difficult
1.954 +\paragraph{A computer} or a TP-System builds on programs with
1.955 +predefined logical rules and does not know any mathematical trick
1.956 +(follow up example \ref{eg:trick}) or recipe to walk around difficult
1.957 expressions.
1.958
1.959 \vbox{
1.960 @@ -926,47 +995,63 @@
1.961 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1.962 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1.963 {\small\textit{
1.964 - \noindent Sometimes it is also useful to be able to apply some
1.965 -\emph{tricks} to get a beautiful and particularly meaningful result,
1.966 -which we are able to interpret. But as seen in this example it can be
1.967 -hard to find out what operations have to be done to transform a result
1.968 + \noindent Sometimes it is also useful to be able to apply some
1.969 +\emph{tricks} to get a beautiful and particularly meaningful result,
1.970 +which we are able to interpret. But as seen in this example it can be
1.971 +hard to find out what operations have to be done to transform a result
1.972 into a meaningful one.
1.973 }}
1.974 \end{example}
1.975 }
1.976
1.977 -\paragraph{The only possibility,} for such a system, is to work
1.978 -through its known definitions and stops if none of these
1.979 -fits. Specified on Signal Processing or any other application it is
1.980 -often possible to walk through by doing simple creases. This creases
1.981 -are in general based on simple math operational but the challenge is
1.982 -to teach the machine \emph{all}\footnote{Its pride to call it
1.983 -\emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1.984 -reach a high level of \emph{all} but it in real it will still be a
1.985 -survey of knowledge which links to other knowledge and {{\sisac}{}} a
1.986 +\paragraph{The only possibility,} for such a system, is to work
1.987 +through its known definitions and stops if none of these
1.988 +fits. Specified on Signal Processing or any other application it is
1.989 +often possible to walk through by doing simple creases. This creases
1.990 +are in general based on simple math operational but the challenge is
1.991 +to teach the machine \emph{all}\footnote{Its pride to call it
1.992 +\emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1.993 +reach a high level of \emph{all} but it in real it will still be a
1.994 +survey of knowledge which links to other knowledge and {{\sisac}{}} a
1.995 trainer and helper but no human compensating calculator.
1.996 \par
1.997 -{{{\sisac}{}}} itself aims to adds an \emph{application} axis (formal
1.998 -specifications of problems out of topics from Signal Processing, etc.)
1.999 -and an \emph{algorithmic} axis to the \emph{deductive} axis of
1.1000 -physical knowledge. The result is a three-dimensional universe of
1.1001 +{{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1.1002 +specifications of problems out of topics from Signal Processing, etc.)
1.1003 +and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1.1004 +physical knowledge. The result is a three-dimensional universe of
1.1005 mathematics seen in Figure~\ref{fig:mathuni}.
1.1006
1.1007 - \begin{figure}
1.1008 - \hfill \\
1.1009 - \begin{center}
1.1010 - \includegraphics{fig/universe}
1.1011 - \caption{Didactic ``Math-Universe''\label{fig:mathuni}}
1.1012 - \end{center}
1.1013 - \end{figure}
1.1014 +\begin{figure}
1.1015 + \begin{center}
1.1016 + \includegraphics{fig/universe}
1.1017 + \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1.1018 + combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1.1019 + leads to a three dimensional math universe.\label{fig:mathuni}}
1.1020 + \end{center}
1.1021 +\end{figure}
1.1022 +
1.1023 +%WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1.1024 +%WN bitte folgende Bezeichnungen nehmen:
1.1025 +%WN
1.1026 +%WN axis 1: Algorithmic Knowledge (Programs)
1.1027 +%WN axis 2: Application-oriented Knowledge (Specifications)
1.1028 +%WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1.1029 +%WN
1.1030 +%WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1.1031 +%WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1.1032 +%WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1.1033 +
1.1034 +%JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1.1035 +%JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1.1036 +%JR gefordert werden...
1.1037
1.1038 \subsection{Notes on Problems with Traditional Notation}
1.1039
1.1040 -\paragraph{During research} on these topic severely problems on
1.1041 -traditional notations have been discovered. Some of them have been
1.1042 -known in computer science for many years now and are still unsolved,
1.1043 -one of them aggregates with the so called \emph{Lambda Calculus},
1.1044 -Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1.1045 +\paragraph{During research} on these topic severely problems on
1.1046 +traditional notations have been discovered. Some of them have been
1.1047 +known in computer science for many years now and are still unsolved,
1.1048 +one of them aggregates with the so called \emph{Lambda Calculus},
1.1049 +Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1.1050 us.
1.1051
1.1052 \vbox{
1.1053 @@ -979,30 +1064,30 @@
1.1054 \[ f(p)=\ldots\; p \in \quad R \]
1.1055
1.1056 {\small\textit{
1.1057 - \noindent Above we see two equations. The first equation aims to
1.1058 -be a mapping of an function from the reel range to the reel one, but
1.1059 -when we change only one letter we get the second equation which
1.1060 -usually aims to insert a reel point $p$ into the reel function. In
1.1061 -computer science now we have the problem to tell the machine (TP) the
1.1062 -difference between this two notations. This Problem is called
1.1063 + \noindent Above we see two equations. The first equation aims to
1.1064 +be a mapping of an function from the reel range to the reel one, but
1.1065 +when we change only one letter we get the second equation which
1.1066 +usually aims to insert a reel point $p$ into the reel function. In
1.1067 +computer science now we have the problem to tell the machine (TP) the
1.1068 +difference between this two notations. This Problem is called
1.1069 \emph{Lambda Calculus}.
1.1070 }}
1.1071 \end{example}
1.1072 }
1.1073
1.1074 -\paragraph{An other problem} is that terms are not full simplified in
1.1075 -traditional notations, in {{\sisac}} we have to simplify them complete
1.1076 -to check weather results are compatible or not. in e.g. the solutions
1.1077 -of an second order linear equation is an rational in {{\sisac}} but in
1.1078 -tradition we keep fractions as long as possible and as long as they
1.1079 +\paragraph{An other problem} is that terms are not full simplified in
1.1080 +traditional notations, in {{\sisac}} we have to simplify them complete
1.1081 +to check weather results are compatible or not. in e.g. the solutions
1.1082 +of an second order linear equation is an rational in {{\sisac}} but in
1.1083 +tradition we keep fractions as long as possible and as long as they
1.1084 aim to be \textit{beautiful} (1/8, 5/16,...).
1.1085 -\subparagraph{The math} which should be mechanized in Computer Theorem
1.1086 -Provers (\emph{TP}) has (almost) a problem with traditional notations
1.1087 -(predicate calculus) for axioms, definitions, lemmas, theorems as a
1.1088 -computer program or script is not able to interpret every Greek or
1.1089 -Latin letter and every Greek, Latin or whatever calculations
1.1090 -symbol. Also if we would be able to handle these symbols we still have
1.1091 -a problem to interpret them at all. (Follow up \hbox{Example
1.1092 +\subparagraph{The math} which should be mechanized in Computer Theorem
1.1093 +Provers (\emph{TP}) has (almost) a problem with traditional notations
1.1094 +(predicate calculus) for axioms, definitions, lemmas, theorems as a
1.1095 +computer program or script is not able to interpret every Greek or
1.1096 +Latin letter and every Greek, Latin or whatever calculations
1.1097 +symbol. Also if we would be able to handle these symbols we still have
1.1098 +a problem to interpret them at all. (Follow up \hbox{Example
1.1099 \ref{eg:symbint1}})
1.1100
1.1101 \vbox{
1.1102 @@ -1012,17 +1097,17 @@
1.1103 u\left[n\right] \ \ldots \ unitstep
1.1104 \]
1.1105 {\small\textit{
1.1106 - \noindent The unitstep is something we need to solve Signal
1.1107 -Processing problem classes. But in {{{\sisac}{}}} the rectangular
1.1108 -brackets have a different meaning. So we abuse them for our
1.1109 -requirements. We get something which is not defined, but usable. The
1.1110 + \noindent The unitstep is something we need to solve Signal
1.1111 +Processing problem classes. But in {{{\sisac}{}}} the rectangular
1.1112 +brackets have a different meaning. So we abuse them for our
1.1113 +requirements. We get something which is not defined, but usable. The
1.1114 Result is syntax only without semantic.
1.1115 }}
1.1116 \end{example}
1.1117 }
1.1118
1.1119 -In different problems, symbols and letters have different meanings and
1.1120 -ask for different ways to get through. (Follow up \hbox{Example
1.1121 +In different problems, symbols and letters have different meanings and
1.1122 +ask for different ways to get through. (Follow up \hbox{Example
1.1123 \ref{eg:symbint2}})
1.1124
1.1125 \vbox{
1.1126 @@ -1032,21 +1117,21 @@
1.1127 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1.1128 \]
1.1129 {\small\textit{
1.1130 - \noindent For using exponents the three \texttt{widehat} symbols
1.1131 -are required. The reason for that is due the development of
1.1132 -{{{\sisac}{}}} the single \texttt{widehat} and also the double were
1.1133 + \noindent For using exponents the three \texttt{widehat} symbols
1.1134 +are required. The reason for that is due the development of
1.1135 +{{{\sisac}{}}} the single \texttt{widehat} and also the double were
1.1136 already in use for different operations.
1.1137 }}
1.1138 \end{example}
1.1139 }
1.1140
1.1141 -\paragraph{Also the output} can be a problem. We are familiar with a
1.1142 -specified notations and style taught in university but a computer
1.1143 -program has no knowledge of the form proved by a professor and the
1.1144 -machines themselves also have not yet the possibilities to print every
1.1145 -symbol (correct) Recent developments provide proofs in a human
1.1146 -readable format but according to the fact that there is no money for
1.1147 -good working formal editors yet, the style is one thing we have to
1.1148 +\paragraph{Also the output} can be a problem. We are familiar with a
1.1149 +specified notations and style taught in university but a computer
1.1150 +program has no knowledge of the form proved by a professor and the
1.1151 +machines themselves also have not yet the possibilities to print every
1.1152 +symbol (correct) Recent developments provide proofs in a human
1.1153 +readable format but according to the fact that there is no money for
1.1154 +good working formal editors yet, the style is one thing we have to
1.1155 live with.
1.1156
1.1157 \section{Problems rising out of the Development Environment}