102 %----------// PART-1 \\----------% |
102 %----------// PART-1 \\----------% |
103 |
103 |
104 \part{Project Fundamentals} |
104 \part{Project Fundamentals} |
105 |
105 |
106 \section{Introduction} |
106 \section{Introduction} |
107 %TODO personal decision no workds like feeling |
|
108 %The motivation to this thesis mainly takes it source from the feeling of understanding difficult signal processing tasks and the will to help others to get this feeling to. |
|
109 %\par Signal Processing (SP) requieres a huge range of mathematic knowledge as well as a feeling for simplification and number tricks but even though this fact, the operations themself are no higher ones. The main task is to understand. Aside this description we think of the classic math ideas and techniques, consisting of... |
|
110 % |
|
111 Didactics of mathematics faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which ususally are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing. |
107 Didactics of mathematics faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which ususally are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing. |
112 |
108 |
113 This gap is an obstacle for applying math as an foundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for~?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows. |
109 This gap is an obstacle for applying math as an foundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for~?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows. |
114 |
110 |
115 \medskip |
111 \medskip |
116 Motivated by this didactical issue on the one hand, and ongoing R\&D on a novel kind of educational mathematics assistant at Graz University of Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to cope with this issue on the other hand, several institutes are planning to join their expertise: the Institutes for Institute for Information Systems and Computer Media (IICM), the Institute for Software Technology (IST), the Institutes for Mathematics, the Signal Processing and Speech Communication Laboratory (SPSC Lab), the Institute for Structural Analysis and the Institute of Electrical Measurement and Measurement Signal Processing. |
112 Motivated by this didactical issue on the one hand, and ongoing R\&D on a novel kind of educational mathematics assistant at Graz University of Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to cope with this issue on the other hand, several institutes are planning to join their expertise: the Institutes for Institute for Information Systems and Computer Media (IICM), the Institute for Software Technology (IST), the Institutes for Mathematics, the Signal Processing and Speech Communication Institute (SPSC), the Institute for Structural Analysis and the Institute of Electrical Measurement and Measurement Signal Processing. |
117 |
113 \par This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in STEOP, the introductory orientation phase. STEOP is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. |
118 This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in STEOP, the introductory orientation phase. STEOP is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. |
|
119 |
114 |
120 \medskip |
115 \medskip |
121 The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part. |
116 The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part. |
122 |
117 \par In part I, Section~\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (Section~\ref{emas}) and introduces the notions required for the implementation work (Section~\ref{math-auth}). In particular, Section~\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to Section~\ref{sec:goals}. |
123 In part I, Section~\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (Section~\ref{emas}) and introduces the notions required for the implementation work (Section~\ref{math-auth}). In particular, Section~\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to Section~\ref{sec:goals}. |
118 \par Section~\ref{sp} analyzes a problems defined by the SPSC for the knowledge already provided (Section~\ref{know-isab}, Section~\ref{know-isac}), discusses the selection of problems for implementation (Section~\ref{know-missing}) TODO: further structure ? |
124 |
|
125 Section~\ref{sp} analyzes ten (TODO: exact no?) problems defined by the SPSC Lab for the knowledge already provided (Section~\ref{know-isab}, Section~\ref{know-isac}), discusses the selection of problems for implementation (Section~\ref{know-missing}) TODO: further structure ? |
|
126 %(\S\ref{}) |
119 %(\S\ref{}) |
127 |
120 |
128 \section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac} |
121 \section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac} |
129 %no CTP!!! |
122 |
130 %A problem behind is the mechanization of mathematic theories in CTP-bases languages. There is still a huge gap between these algoritms and this what we want as a solution - in Example Signal Processing. |
|
131 %\begin{example} |
|
132 % \[ |
|
133 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY |
|
134 % \] |
|
135 % {\small\textit{ |
|
136 % \noindent A very simple example on this what we call gap is the simplification above. It is needles to say that it is correct and also isabell forfills it correct - \emph{always}. But sometimes we don't want expand such terms, sometimes we want another structure of them. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between mechanical simplification and the solution. |
|
137 % }} |
|
138 % \caption{Correct but not usefull}\label{eg:gap} |
|
139 %\end{example} |
|
140 %Until we are not able to fill this gap we have to live with it but first have a look on the meaning of this statement: |
|
141 %\par Mechanized math starts from mathematical models and \emph{hopefully} proceeds to match physics. Academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modelling and formalization. The process from a physical observance to a mathematical theory is unavoidable bound of setting up a big collection of standards, rules, definition but also exceptions. These are the things making mechanization that difficult. |
|
142 %\begin{example} |
|
143 % \[ |
|
144 % m,\ kg,\ s,\ldots |
|
145 % \] |
|
146 % {\small\textit{ |
|
147 % \noindent Think about some units like that one's above. Behind each unit there is a discerning and very accurate definition: One Meter is the distance the light travels, in a vacuum, through the time of 1 / 299.792.458 second; one kilogramm is the weight of a platinum-iridium cylindar in paris; and so on. But are these definitions useable in a computer mechanized world?! |
|
148 % }} |
|
149 % \caption{Units in measurement}\label{eg:units} |
|
150 %\end{example} |
|
151 %\par A computer or a CTP-System builds on programms witth predefined logical ruels and does not know any mathematical trick (follow up example \ref{eg:trick}) or recipe to walk around difficult expressions. |
|
152 %\begin{example} |
|
153 %\[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] |
|
154 %\[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= |
|
155 % \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] |
|
156 %\[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] |
|
157 % {\small\textit{ |
|
158 % \noindent Sometimes it is also usefull to be able to apply some \emph{tricks} to get a beautiful and particulary meaningful result, which we are able to interpret. But as seen in this example it can be hard to find out what operations have to be done to transform a result into a meaningful one. |
|
159 % }} |
|
160 % \caption{Mathematic tricks}\label{eg:trick} |
|
161 %\end{example} |
|
162 %For such a system the only possibility is to work through its known definitions and stops if none of these fits. Specified on Signal Processing or any other application it is often possible to walk through by doing simple creases. This creases are in generell based on simple math operatiopms but the challange is to teach the machine \emph{all}\footnote{Its pride to call it \emph{all}.} of them. Unfortunataly the goal of CTP Isabelle is to reach a high level of \emph{all} but it in real it will still be a survey of knowledge which links to other knowledge and {{\sisac{}}} a trainer and helper but no human compensating calulator. |
|
163 %\par {{\sisac{}}} itselfs aims to adds an \emph{application} axis (formal specifications of problems outof topics from Signal Processing, etc.) and an \emph{algorithmic} axis to the \emph{deductive} axis of physical knowledge. The result is a three-dimensional universe of mathematics. |
|
164 % |
|
165 %\subsubsection*{Notes on Mechanization of Mathematics} |
123 %\subsubsection*{Notes on Mechanization of Mathematics} |
166 %This thesis tries to \emph{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. As we are still in a eary part of development, this is the first thesis dealing within this topic and there is \emph{no} related work to guid through. A more detailed description about this fact can be found in Section \ref{sec:related}. |
124 %This thesis tries to \emph{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. As we are still in a eary part of development, this is the first thesis dealing within this topic and there is \emph{no} related work to guid through. A more detailed description about this fact can be found in Section \ref{sec:related}. |
167 %The major challenge of the practical part, of this thesis, is, that "connecting the two worlds" involves programming in a CTP-based programming language which is in a very early state of prototyping. There is no concrete experience data ready to grep. |
125 %The major challenge of the practical part, of this thesis, is, that "connecting the two worlds" involves programming in a CTP-based programming language which is in a very early state of prototyping. There is no concrete experience data ready to grep. |
168 % |
126 % |
169 As mentioned in the introduction, a prototype of an educational math assistant called {\sisac}\footnote{{\sisac}=\textbf{Isa}belle \cite{Nipkow-Paulson-Wenzel:2002} for \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges the gap between (1) introducation and (2) application of mathematics: {\sisac} is based on Computer Theorem Proving (CTP), a technology which requires each fact and each action justified by formal logic, so {{\sisac{}}} makes justifications transparent to students in interactive step-wise problem solving. By that way {\sisac} already can serve both: |
127 As mentioned in the introduction, a prototype of an educational math assistant called {\sisac}\footnote{{\sisac}=\textbf{Isa}belle \cite{Nipkow-Paulson-Wenzel:2002} for \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges the gap between (1) introducation and (2) application of mathematics: {\sisac} is based on Computer Theorem Proving (CTP), a technology which requires each fact and each action justified by formal logic, so {{\sisac{}}} makes justifications transparent to students in interactive step-wise problem solving. By that way {\sisac} already can serve both: |
170 \begin{enumerate} |
128 \begin{enumerate} |
171 \item Introduction of math stuff (e.g. partial fraction decomposition) by stepwise explaining and exercising respective symbolic calculations with ``next step guidance (NSG)'' and rigorously checking steps freely input by students --- this also in context with advanced applications (where the stuff to be taught in higher semesters can be skimmed through by NSG), and |
129 \item Introduction of math stuff (in e.g. partial fraction decomposition) by stepwise explaining and exercising respective symbolic calculations with ``next step guidance (NSG)'' and rigorously checking steps freely input by students --- this also in context with advanced applications (where the stuff to be taught in higher semesters can be skimmed through by NSG), and |
172 \item Application of math stuff in advanced engineering courses (e.g. problems to be solved by inverse Z-transform in a Signal Processing Lab) --- and now without much ado about basic math techniques (like partical fraction decomposition): ``next step guidance'' supports students in independenly (re-)adopting such techniques. |
130 \item Application of math stuff in advanced engineering courses (e.g. problems to be solved by inverse Z-transform in a Signal Processing Lab) --- and now without much ado about basic math techniques (like partical fraction decomposition): ``next step guidance'' supports students in independenly (re-)adopting such techniques. |
173 \end{enumerate} |
131 \end{enumerate} |
174 Before the question is answers, how {\sisac} accoplishes this task from a technical point of view, some remarks on the state-of-the-art is given: |
132 Before the question is answers, how {\sisac} accoplishes this task from a technical point of view, some remarks on the state-of-the-art is given, therefor follow up Section~\ref{emas}. |
175 |
133 |
176 \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} |
134 \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} |
177 Educational software in mathematics is, if at all, based on Computer Algebra Systems (CAS, for instance \cite{progr-mathematica,prog-maple06}), Dynamic Geometry Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org, Cinderella http://www.cinderella.de/, GCLC http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These base technologies are used to program math lessons and sometimes even exercises. The latter are cumbersome: the steps towards a solution of such an interactive exercise need to be provided with feedback, where at each step a wide variety of possible input has to be foreseen by the programmer --- so such interactive exercises either require high development efforts or the exercises constrain possible inputs. |
135 Educational software in mathematics is, if at all, based on Computer Algebra Systems (CAS, for instance \cite{progr-mathematica,prog-maple06}), Dynamic Geometry Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org, Cinderella http://www.cinderella.de/, GCLC http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These base technologies are used to program math lessons and sometimes even exercises. The latter are cumbersome: the steps towards a solution of such an interactive exercise need to be provided with feedback, where at each step a wide variety of possible input has to be foreseen by the programmer --- so such interactive exercises either require high development efforts or the exercises constrain possible inputs. |
178 |
136 |
179 A new generation of educational math assistants (EMAs) is emerging presently, which is based on Computer Theorem Proving (CTP). CTP, for instance Isabelle \cite{Nipkow-Paulson-Wenzel:2002} and Coq \cite{Huet_all:94}, is a technology which requires each fact and each action justified by formal logic. Pushed by demands for \textit{proven} correctness of safety-critical software CTP advances into software engineering; from these advancements computer mathematics benefits in general, and math education in particular. Two features of CTP are immediately beneficial for learning: |
137 A new generation of educational math assistants (EMAs) is emerging presently, which is based on Computer Theorem Proving (CTP). CTP, for instance Isabelle \cite{Nipkow-Paulson-Wenzel:2002} and Coq \cite{Huet_all:94}, is a technology which requires each fact and each action justified by formal logic. Pushed by demands for \textit{proven} correctness of safety-critical software CTP advances into software engineering; from these advancements computer mathematics benefits in general, and math education in particular. Two features of CTP are immediately beneficial for learning: |
200 {\sisac}, however, uses a novel type of CTP-based language \cite{plmms10} for describing how to constuct a solution to an engineering problem and for calling equation solvers, integration, etc~\footnote{Implementation of CAS-like functionality in CTP is not primarily concerned with efficiency, but with a didactic question: What to decide for: for high-brow algorithms at the state-of-the-art or for elementary algorithms comprehensible for students~?} within CTP; CTP can ensure ``systems that never make a mistake'' \cite{casproto} --- are impossible for CAS which have no logics underlying. |
158 {\sisac}, however, uses a novel type of CTP-based language \cite{plmms10} for describing how to constuct a solution to an engineering problem and for calling equation solvers, integration, etc~\footnote{Implementation of CAS-like functionality in CTP is not primarily concerned with efficiency, but with a didactic question: What to decide for: for high-brow algorithms at the state-of-the-art or for elementary algorithms comprehensible for students~?} within CTP; CTP can ensure ``systems that never make a mistake'' \cite{casproto} --- are impossible for CAS which have no logics underlying. |
201 |
159 |
202 With writing such CTP-based programs authoring is perfect, the application programmer is not concerned with interaction or with user guidance: this is concern of a novel kind of program interpreter called Lucas-Interpreter \cite{wn:lucas-interp-12}. This interpreter hands over control to a dialog component at each step of calculation (like a debugger at breakpoints) and calls automated CTP to check user input following personalized strategies according to a feedback module. |
160 With writing such CTP-based programs authoring is perfect, the application programmer is not concerned with interaction or with user guidance: this is concern of a novel kind of program interpreter called Lucas-Interpreter \cite{wn:lucas-interp-12}. This interpreter hands over control to a dialog component at each step of calculation (like a debugger at breakpoints) and calls automated CTP to check user input following personalized strategies according to a feedback module. |
203 |
161 |
204 \medskip |
162 \medskip |
205 However ``application programming with CTP'' is not done with writing a program: according to the principles of CTP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is, for instance %TODO: take your example ! |
163 However ``application programming with CTP'' is not done with writing a program: according to the principles of CTP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is shown in Example~\ref{eg:neuper1}. %TODO: take your example ! |
|
164 |
|
165 \begin{example} |
206 {\small\begin{tabbing} |
166 {\small\begin{tabbing} |
207 123\=123\=123\=123\=\kill |
167 123\=123\=123\=123\=\kill |
|
168 \hfill \\ |
208 \>axiomatization where \\ |
169 \>axiomatization where \\ |
209 \>\> rule1: "1 = $\delta$ [n]" and\\ |
170 \>\> rule1: "1 = $\delta$ [n]" and\\ |
210 \>\> rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and\\ |
171 \>\> rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and\\ |
211 \>\> rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and \\ |
172 \>\> rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and \\ |
212 \>\> rule4: "|| z || > || $\alpha$ || ==> z / (z - $\alpha$) = $\alpha^n$ * u [n]" and\\ |
173 \>\> rule4: "|| z || > || $\alpha$ || ==> z / (z - $\alpha$) = $\alpha^n$ * u [n]" and\\ |
213 \>\> rule5: "|| z || < || $\alpha$ || ==> z / (z - $\alpha$) = -($\alpha^n$) * u [-n - 1]" and\\ |
174 \>\> rule5: "|| z || < || $\alpha$ || ==> z / (z - $\alpha$) = -($\alpha^n$) * u [-n - 1]" and\\ |
214 \>\> rule6: "|| z || > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]"\\ |
175 \>\> rule6: "|| z || > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]" |
215 \end{tabbing} |
176 \end{tabbing} |
216 } |
177 } |
217 |
178 \caption{Axiomatization in Isabelle\label{eg:neuper1}} |
218 In order to provide CTP with logical facts for checking user input, the Lucas-Interpreter requires a \textbf{specification}. Such a specification is for instance |
179 \end{example} |
|
180 |
|
181 In order to provide CTP with logical facts for checking user input, the Lucas-Interpreter requires a \textbf{specification}. Such a specification is shown in Example~ref{eg:neuper2}. |
|
182 |
|
183 \begin{example} |
219 {\small\begin{tabbing} |
184 {\small\begin{tabbing} |
220 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill |
185 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill |
|
186 \hfill \\ |
221 Specification no.1:\\ |
187 Specification no.1:\\ |
222 %\>input\>: $\{\;r={\it arbitraryFix}\;\}$ \\ |
188 %\>input\>: $\{\;r={\it arbitraryFix}\;\}$ \\ |
223 \>input \>: $\{\;r\;\}$ \\ |
189 \>input \>: $\{\;r\;\}$ \\ |
224 \>precond \>: $0 < r$ \\ |
190 \>precond \>: $0 < r$ \\ |
225 \>output \>: $\{\;A,\; u,v\;\}$ \\ |
191 \>output \>: $\{\;A,\; u,v\;\}$ \\ |
227 \> \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land |
193 \> \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land |
228 (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\ |
194 (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\ |
229 \>props\>: $\{\;A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\;\}$ |
195 \>props\>: $\{\;A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\;\}$ |
230 \end{tabbing} |
196 \end{tabbing} |
231 } |
197 } |
232 Such a specification is checked before the execution of a program is started, the same applies for sub-programs. In the following example program the sub-programs are designated by {\tt SubProblem}: TODO one example. |
198 \caption{Specification for the Lucas-Interpreter\label{eg:neuper2}} |
|
199 \end{example} |
|
200 |
|
201 Such a specification is checked before the execution of a program is started, the same applies for sub-programs. In the following example program (Example~\ref{eg:subprob}) the sub-programs are designated by \ttfamily SubProblem \normalfont: |
|
202 |
|
203 \begin{example} |
|
204 \hfill \\ |
|
205 {\ttfamily \begin{tabbing} |
|
206 ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\ |
|
207 ``\>\>[linear,univariate,equation,test],'' \\ |
|
208 ``\>\>[Test,solve\_linear])'' \\ |
|
209 ``\>[BOOL equ, REAL z])'' \\ |
|
210 \end{tabbing} |
|
211 } |
|
212 {\small\textit{ |
|
213 \noindent If a programm requires a result which has to be calculated first we can use a subproblem to do so. In our specific case we wanted to calculate the zeros of a fraction and used a subproblem to calculate the zeros of the denominator polynom. |
|
214 }} |
|
215 \caption{Ussage of Subproblems in Programms\label{eg:subprob}} |
|
216 \end{example} |
233 |
217 |
234 |
218 |
235 \subsection{Goals of the Thesis}\label{sec:goals} |
219 \subsection{Goals of the Thesis}\label{sec:goals} |
236 %Imagine a piece of software would be able to support you by understanding every problem class, upcoming in the first years attending university - wouldn't it be great? |
220 Imagine a piece of software would be able to support you by understanding every problem class, upcoming in the first years attending university - wouldn't it be great? |
237 %\par {{\sisac{}}} tries to do that, but the current state of the art is miles away from this goal and a single implementation of a problem is not enough to cahnge this circumstamce. Through this fact it is all the more essential to try, test, research and document the implementation of problem classes from "`real world"' applications. Responding to the abstract at the begin of this document the thesis has two folds; on the one hand certainly to provide interactiv course material for Signal Processing (which means to implement a single problem provided by the Institute of Signal Processing and Speech Communication (SPSC); follow up Calulcations), and to extract experience data respectively help the {{\sisac{}}}-team by setting up a detailed description of technicalities hacking {{\sisac{}}} on the other hand. |
221 \par {{\sisac{}}} tries to do that, but the current state of the art is miles away from this goal and a single implementation of a problem is not enough to cahnge this circumstamce. Through this fact it is all the more essential to try, test, research and document the implementation of problem classes from "`real world"' applications. Responding to the abstract at the begin of this document the thesis has two folds; on the one hand certainly to provide interactiv course material for Signal Processing (which means to implement a single problem provided by the Institute of Signal Processing and Speech Communication (SPSC); follow up Calulcations), and to extract experience data respectively help the {{\sisac{}}}-team by setting up a detailed description of technicalities hacking {{\sisac{}}} on the other hand. |
238 %\par Another goal is to demonstrate the power and attractivity of {\sisac}. |
222 |
239 Now all the notions are in place to describe the task ``Interactive Course Material for Signal Processing based on Isabelle/{\sisac}'' appropriately by the following points: |
223 All the notions are in place to describe the task ``Interactive Course Material for Signal Processing based on Isabelle/{\sisac}'', the main task of this thesis, appropriately by the following points: |
240 \begin{enumerate} |
224 \begin{enumerate} |
241 \item Analyze the problems given by the SPSC Lab for mathematics \textbf{knowledge required}, search the knowledge already available in Isabelle/{\sisac}, estimate efforts required to fill the gap between knowledge required and knowledge available, and finally select problems for implementation accordingly. |
225 \item Analyze the problems given by the SPSC Lab for mathematics \textbf{knowledge required}, search the knowledge already available in Isabelle/{\sisac}, estimate efforts required to fill the gap between knowledge required and knowledge available, and finally select problems for implementation accordingly. |
242 \item Implement the selected problems in Isabelle/{\sisac}, which means, in appropriate Isabelle theories \textbf{for each problem} implement: |
226 \item Implement the selected problems in Isabelle/{\sisac}, which means, in appropriate Isabelle theories \textbf{for each problem} implement: |
243 \begin{enumerate} |
227 \begin{enumerate} |
244 \item \textbf{Definitions and theorems} required within the specification (including ``descriptions'' for input variables and output variables) and the program (proofs omitted via ``axiomaization'') |
228 \item \textbf{Definitions and theorems} required within the specification (including ``descriptions'' for input variables and output variables) and the program (proofs omitted via ``axiomaization'') |
246 \item \textbf{A program} describing the algorithm which solves the problem, i.e. which constructs output meeting the postcondition. Programming involves identifying the steps (tactics~!) which create the calculation and calling CAS-functions (simplification, equation solvers, etc) appropriately. Modularization of programs into {\tt SubProblems} has to prepare for re-use of code. |
230 \item \textbf{A program} describing the algorithm which solves the problem, i.e. which constructs output meeting the postcondition. Programming involves identifying the steps (tactics~!) which create the calculation and calling CAS-functions (simplification, equation solvers, etc) appropriately. Modularization of programs into {\tt SubProblems} has to prepare for re-use of code. |
247 \end{enumerate} |
231 \end{enumerate} |
248 \item Add \textbf{multimedia explanations} to each problem (i.e. to specific definitions, theorems, the specification and the program) such that non-expert students (e.g. within STEOP, the introductory orientation phase at TUG) get an idea the problem is about. |
232 \item Add \textbf{multimedia explanations} to each problem (i.e. to specific definitions, theorems, the specification and the program) such that non-expert students (e.g. within STEOP, the introductory orientation phase at TUG) get an idea the problem is about. |
249 \item \textbf{Document the implementation} such that |
233 \item \textbf{Document the implementation} such that |
250 \begin{enumerate} |
234 \begin{enumerate} |
251 % \item Interactive course material hopefully useful in education within the SPSC Lab and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and |
235 \item Interactive course material hopefully useful in education within the SPSC and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and |
252 % \item A detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and {\sisac}-developers with feedback in usability of the CTP-based program language. |
236 \item A detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and {\sisac}-developers with feedback in usability of the CTP-based program language. |
253 \item subsequent application programmers have guidelines for further implementation of interactive course material in SPSC and other engineering sciences |
237 \item subsequent application programmers have guidelines for further implementation of interactive course material in SPSC and other engineering sciences |
254 \item {\sisac{}} developers get feedback for ongoing improvement of the CTP-based programming language, the respective development environment and the respective program interpreter (called Lucas-Interpreter) |
238 \item {\sisac{}} developers get feedback for ongoing improvement of the CTP-based programming language, the respective development environment and the respective program interpreter (called Lucas-Interpreter) |
255 \item development of knowledge for engineering sciences is being motivated in the Isabelle community. |
239 \item development of knowledge for engineering sciences is being motivated in the Isabelle community. |
256 \end{enumerate} |
240 \end{enumerate} |
257 \end{enumerate} |
241 \end{enumerate} |
340 \end{table} |
324 \end{table} |
341 |
325 |
342 As conclusion of the summerized efforts it is evident that only one topic can be tried to realized as a baccalaureate thesis. In accord with Dr. Neuper we decided after some practical tests to start with the implementation of the (Inverse) Z-Transformation. The Reason is that this topic can mostly be done with knowledge which was already tried to be mechanized in {\sisac}. |
326 As conclusion of the summerized efforts it is evident that only one topic can be tried to realized as a baccalaureate thesis. In accord with Dr. Neuper we decided after some practical tests to start with the implementation of the (Inverse) Z-Transformation. The Reason is that this topic can mostly be done with knowledge which was already tried to be mechanized in {\sisac}. |
343 |
327 |
344 \subsection{Formalization of missing knowledge in Isabelle} |
328 \subsection{Formalization of missing knowledge in Isabelle} |
|
329 |
|
330 A problem behind is the mechanization of mathematic theories in CTP-bases languages. There is still a huge gap between these algoritms and this what we want as a solution - in Example Signal Processing. |
|
331 \begin{example} |
|
332 \[ |
|
333 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY |
|
334 \] |
|
335 {\small\textit{ |
|
336 \noindent A very simple example on this what we call gap is the simplification above. It is needles to say that it is correct and also isabell forfills it correct - \emph{always}. But sometimes we don't want expand such terms, sometimes we want another structure of them. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between mechanical simplification and the solution. |
|
337 }} |
|
338 \caption{Correct but not usefull}\label{eg:gap} |
|
339 \end{example} |
|
340 Until we are not able to fill this gap we have to live with it but first have a look on the meaning of this statement: |
|
341 \par Mechanized math starts from mathematical models and \emph{hopefully} proceeds to match physics. Academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modelling and formalization. The process from a physical observance to a mathematical theory is unavoidable bound of setting up a big collection of standards, rules, definition but also exceptions. These are the things making mechanization that difficult. |
|
342 \begin{example} |
|
343 \[ |
|
344 m,\ kg,\ s,\ldots |
|
345 \] |
|
346 {\small\textit{ |
|
347 \noindent Think about some units like that one's above. Behind each unit there is a discerning and very accurate definition: One Meter is the distance the light travels, in a vacuum, through the time of 1 / 299.792.458 second; one kilogramm is the weight of a platinum-iridium cylindar in paris; and so on. But are these definitions useable in a computer mechanized world?! |
|
348 }} |
|
349 \caption{Units in measurement}\label{eg:units} |
|
350 \end{example} |
|
351 \par A computer or a CTP-System builds on programms witth predefined logical ruels and does not know any mathematical trick (follow up example \ref{eg:trick}) or recipe to walk around difficult expressions. |
|
352 \begin{example} |
|
353 \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] |
|
354 \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= |
|
355 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] |
|
356 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] |
|
357 {\small\textit{ |
|
358 \noindent Sometimes it is also usefull to be able to apply some \emph{tricks} to get a beautiful and particulary meaningful result, which we are able to interpret. But as seen in this example it can be hard to find out what operations have to be done to transform a result into a meaningful one. |
|
359 }} |
|
360 \caption{Mathematic tricks}\label{eg:trick} |
|
361 \end{example} |
|
362 For such a system the only possibility is to work through its known definitions and stops if none of these fits. Specified on Signal Processing or any other application it is often possible to walk through by doing simple creases. This creases are in generell based on simple math operatiopms but the challange is to teach the machine \emph{all}\footnote{Its pride to call it \emph{all}.} of them. Unfortunataly the goal of CTP Isabelle is to reach a high level of \emph{all} but it in real it will still be a survey of knowledge which links to other knowledge and {{\sisac{}}} a trainer and helper but no human compensating calulator. |
|
363 \par {{\sisac{}}} itselfs aims to adds an \emph{application} axis (formal specifications of problems outof topics from Signal Processing, etc.) and an \emph{algorithmic} axis to the \emph{deductive} axis of physical knowledge. The result is a three-dimensional universe of mathematics. |
|
364 |
|
365 |
|
366 |
345 todo |
367 todo |
346 |
368 |
347 axiomatization ... where ... and |
369 axiomatization ... where ... and |
348 |
370 |
349 \subsection{Notes on Problems with Traditional Notation} |
371 \subsection{Notes on Problems with Traditional Notation} |
350 {\footnotesize |
372 %{\footnotesize |
351 \textbf{TODO} |
373 %\textbf{TODO} |
352 Due the thesis work we discorvers severell problems of traditional notations. |
374 %Due the thesis work we discorvers severell problems of traditional notations. |
353 |
375 % |
354 u[n] !! |
376 %u[n] !! |
355 |
377 % |
356 f x = why not f(x) ?!?! |
378 %f x = why not f(x) ?!?! |
357 |
379 % |
358 ... |
380 %... |
359 |
381 % |
360 terms are not full simplified in traditional notations, in isac we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in isac but in tradition we keep fractions as long as possible and as long as they are 'beautiful' (1/8, 5/16,...) |
382 %terms are not full simplified in traditional notations, in isac we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in isac but in tradition we keep fractions as long as possible and as long as they are 'beautiful' (1/8, 5/16,...) |
361 }\\ |
383 %}\\ |
|
384 |
362 The math which should be mechanized in Computer Theorem Provers (\emph{CTP}) has (almost) a problem with traditional notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer programm or script is not able to interpret every greek or latin letter and every greek, latin or whatever calculations symbol. Also if we would be able to handle thehse symbols we still have a problem to interpret them at all. (Follow up \hbox{Example \ref{eg:symbint1}}) |
385 The math which should be mechanized in Computer Theorem Provers (\emph{CTP}) has (almost) a problem with traditional notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer programm or script is not able to interpret every greek or latin letter and every greek, latin or whatever calculations symbol. Also if we would be able to handle thehse symbols we still have a problem to interpret them at all. (Follow up \hbox{Example \ref{eg:symbint1}}) |
363 |
386 |
364 \begin{example} |
387 \begin{example} |
365 \[ |
388 \[ |
366 u\left[n\right] \ \ldots \ unitstep |
389 u\left[n\right] \ \ldots \ unitstep |