1 % Title: bakkarbeit_jrocnik.tex
3 % (c) copyright due to lincense terms.
4 %2345678901234567890123456789012345678901234567890123456789012345678901234567890
5 % 10 20 30 40 50 60 70 80
8 %%\cite{proakis2004contemporary}
11 %%structur: theory part ersetzt project undamentals
12 %% "mechanization of math in isac" ersetzt introduction
13 %% authoring math in isac ersetzt mechanization
15 %define document class
16 \documentclass[a4paper, 12pt]{article}
18 %packages for language and input
19 \usepackage[english]{babel}
20 \usepackage[T1]{fontenc}
21 \usepackage[latin1]{inputenc}
28 \usepackage[pdfpagelabels]{hyperref}
29 \usepackage{longtable}
31 \usepackage{float} %For restylefloat
32 \newfloat{example}{h}{} %self made floats
33 \floatname{example}{Example} %name for float
34 \restylefloat{table} %float tables
35 \floatstyle{ruled} %boxes around floats
36 \restylefloat{example} %float examples --> boxes
41 \definecolor{lgray}{RGB}{238,238,238}
43 %isabelle relevant packages
44 \usepackage{isabelle,isabellesym}
47 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
48 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
50 \newcommand{\HRule}{\rule{\linewidth}{0.2mm}}
52 %----------// BEGIN DOCUMENT \\----------%
56 %----------// TITLE PAGE \\----------%
58 \input{./bakkarbeit_titlepage.tex}
61 %----------// EMPTY PAGE \\----------%
65 %----------// THANKS \\----------%
71 \emph{Dr.techn. Walther Neuper}\\
72 \emph{Dipl.-Ing. Bernhard Geiger}
77 %----------// EMPTY PAGE \\----------%
81 %----------// ABSTRACT \\----------%
84 The Baccalaureate Thesis creates interactive course material for Signal Processing (SP) based on the experimental math assistant Isabelle and provides it within {\sisac} (Isabelle for Calculations).
85 \par The content of the course material is defined together with the Signal Processing and Speech Communication Laboratory (SPSC Lab) of Graz University of Technology (TUG). The content is planned to be used in specific lectures and labs of the SPSC and thus is thoroughly concerned with underlying mathematical and physical theory.
86 One challenge of this thesis is, that theory is not yet mechanized in Computer Theorem Provers (CTP); so this thesis will provide preliminary definitions in so-called \emph{theories} of the CTP Isabelle and theorems without proofs.
87 \par Another callenge is the implementation of interactive courses: this is done within the educational math assistant Isabelle/{\sisac}, which is under development at TU Graz. The present state of {\sisac{}} happens to provide the {\em first} occasion for authoring by a non-member of the {\sisac}-developer team. So this challenge involves alpha-testing of the underlying \emph{CTP-based programming language}, because error messages are still not user-friendly and need frequent contact with {\sisac}-developers.
88 So the practical outcome of this thesis is twofold:
90 \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
91 \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.
96 %----------// T O C \\----------%
99 This thesis is structured into a fundamental part introducing the thesis aswell as the {\sisac{}} project and describing the mathematic base. Further a automatically generated practical part representing the work on {\sisac{}} which can be extended.
102 \pagenumbering{arabic}
105 %----------// PART-1 \\----------%
107 \part{Project Fundamentals}
109 The goals of the thesis are finally defined in section \ref{sec:goals} which seems to be very late. The reason for this fact is that there has a lot of research to be done prior and a lot of this research has to be described in this thesis before we are able to define the proper goals. All this is neccessary for understanding the effort on this work.
111 \section{Introduction}
112 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.
113 \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 predefined formulas, notations and forumularsations we learn.
115 \subsection{Mechanization of Mathematics}
116 A problem behind is the mechanization of mathematic theories in CTP-bases languages. There is still a hugh gap between these theories and this what we call an applications - in Example Signal Processing.
119 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
122 \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 do simplificate these things, sometimes it is easyer for handling and understanding if we keep terms together. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between applications and theorem proofment.
124 \caption{Correct but not usefull}\label{eg:gap}
126 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:
127 \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.
133 \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?!
135 \caption{Units in measurement}\label{eg:units}
137 \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.
139 \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
140 \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
141 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
142 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
144 \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.
146 \caption{Mathematic tricks}\label{eg:trick}
148 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.
149 \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.
151 \subsubsection*{Notes on Mechanization of Mathematics}
152 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}.
153 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.
155 \subsection{Goals of the Thesis}\label{sec:goals}
156 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?
157 \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.
158 \par Another goal is to demonstrate the power and attractivity of {\sisac}.
160 \section{Mechanization of Signal Processing Problems}
161 \subsection{Relevant Knowledge available in Isabelle}
162 Isabelle is developed now for a long time and so we are able to access a huge range of theories and usefull snipsets. The main problem according this snipsets is that isabelle still is a theorem proofer and not an algebra system. But due the work of the {\sisac}-development team there are already also many calculation examples provided.
163 \par The SPSC provided a list of problems which are often done wrong or are missunderstood by studentsin term of the problem classes. Out of these tasks we tried to extract the core operations and looked up which parts are already implemented or usefull. The provided problems are:
165 \item Fourier-Transformation
167 \item Inverse z-Transformation and partial fraction decomposition
168 \item Indextransformation
170 Following the collection and evaluation of core operations collated with isabelle:
172 \paragraph{example FFT}, describe in detail !!!!
174 ? different meaning: FFT in Maple
176 gap between what is available and what is required (@)!
178 traditional notation ?
180 \subsection{Relevant Knowledge available in isac}
183 specifications (``application axis'') and methods (``algorithmic axis'')
185 partial fractions, cancellation of multivariate rational terms, ...
187 \subsection{Survey: Requiered Knowledge and Selected Problem(s)}
188 Following tables are showing the expected development effort for speciefic problems. The values are only very inaccurately approximations of the real work, but needed as a basis for descieding with which problem to start:
192 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
193 requirements & comments &effort\\ \hline\hline
194 solving Intrgrals & simple via propertie table & 20\\
195 & \emph{real} & MT\\ \hline
196 transformation table & simple transform & 20\\ \hline
197 visualisation & backend & 10\\ \hline
198 example collection & with explanations & 20\\ \hline\hline
199 \multicolumn{2}{c|}{} & 70-80\\
202 \caption{Fourier-Transformation development effort}
207 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
208 requirements & comments &effort\\ \hline\hline
209 simplify rationals & \sisac & 0\\ \hline
210 define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline
211 simplify sum & termorder & 10\\
212 & simplify rules & 20\\
213 & use simplify rationals& 0\\ \hline
214 index adjustments & with unit step & 10\\ \hline
215 example collection & with explanations & 20\\ \hline\hline
216 \multicolumn{2}{c|}{} & 70-90\\
219 \caption{Convolution Operations development effort}
224 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
225 requirements & comments &effort\\ \hline\hline
226 solve for part.fract. & \sisac: degree 2 & 0\\
227 & complex nomminators & 30\\
228 & degree > 2 & MT\\ \hline
229 simplify polynomial & \sisac & 0\\
230 simplify rational & \sisac & 0\\ \hline
231 partial fraction & degree 2, & 20\\
232 decomposition & specification, method& 30\\ \hline
233 ${\cal Z}^{-1}$ table & explanations, figures& 20\\ \hline
234 example collection & with explanations & 20\\ \hline\hline
235 \multicolumn{2}{c|}{} & 90-120\\
239 \caption{Z-Transformation development effort}
242 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}.
244 \subsection{Formalization of missing knowledge in Isabelle}
247 axiomatization ... where ... and
249 \subsection{Notes on Problems with Traditional Notation}
252 Due the thesis work we discorvers severell problems of traditional notations.
256 f x = why not f(x) ?!?!
260 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,...)
262 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}})
266 u\left[n\right] \ \ldots \ unitstep
269 \noindent The unitstep is something we need to solve Signal Processing problem classes. But in {\sisac{}} the rectangular breakets have a different meaning. So we abuse them for our requirements. We get something which is not defined, but useable. The Result is syntax only without semantic.
271 \caption{Expression Interpretation}\label{eg:symbint1}
274 \noindent In different problems, symbols and letters have different meanings and ask for different ways to get through. (Follow up \hbox{Example \ref{eg:symbint2}})
277 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
280 \noindent For using exponents the three widehat symbols are required. The reason for that is due the development of {\sisac{}} the single widehat and also the double were already in use for different operations.
282 \caption{Symbol Interpretation}\label{eg:symbint2}
284 Exclusive from the input, also the output can be a problem. We are familar with a specified notations and style taught in university but a computer programm has no knowledge of the form probved by a professor and the maschines themselve also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a humand readable format but according to the fact that there is no mony for good working formel editors yet, the style is one thing we have to live with.
286 \section{Milestones for the Thesis}
287 The thesis was splitted into six iterations
289 \item[(29.06. -- 27.07.)] Collection of detailed informations about different STEOP topics \ref{ssec:infcol}
290 \item[(27.07.)] First Prsentation - Decition on which Problems will be implemented \ref{ssec:pres1}
291 \item[(01.09. -- 11.11.)] Implementing the Problem Class in {\sisac{}} \ref{ssec:impl}
292 \item[(14.11. -- 02.12.)] Documentation of the Implementation \ref{ssec:doc}
293 \item[(05.12. -- todo)] Writting on the thesis \ref{ssec:thes}
294 \item[todo] Second Prsentation - Work review \ref{ssec:pres2}
297 \section{Detailed Milestone Description}
298 \subsection{Collection of detailed informations about different STEOP topics}\label{ssec:infcol}
299 identify problems relevant for certain SP lectures
300 estimate chances to realized them within the scope of this thesis
301 order for implementing the problems negotiated with lecturers
302 \subsection{First Prsentation - Decition on which Problems will be implemented}\label{ssec:pres1}
303 \subsection{Implementing the Problem Class in {\sisac}}\label{ssec:impl}
304 \subsection{Documentation of the Implementation}\label{ssec:doc}
305 \subsection{Writting on the thesis}\label{ssec:thes}
306 \subsection{Second Prsentation - Work review}\label{ssec:pres2}
308 \section{Related Work}\label{sec:related}
309 Unusual for a Baccalaureate Thesis, there is {\em no} related work; this requires explanation.
310 Of course, this thesis relies on front-of-the wave computer mathematics, on CTP. But {\sisac{}} uses CTP in a very specific way, which is too weakly related to other work: programming in the CTP-based language and rigorous formal specification of problems in Signal Processing where the main tasks in the practical part of this thesis. The major challenge for the practical work was given by the fact, that the work concerned alpha-testing of the CTP-based programming environment.
311 \par Another area of work could be considered as related work: authoring of e-learning content. However, {\sisac{}} provides division of concern such that the practical part of this thesis could focus on computer mathematics; this work was not concerned with interaction (the CTP-based programming language has neither input statements nor output statements), nor with dialog guidance nor with any kind of learning theory.
312 \par These two reasons are given for the unusual statement, that there is no related work to be discussed in this thesis.
316 \section{Open Questions}
318 \section{Conclusions}
323 %----------// PART 2 \\----------%
325 \part{Implementation}
327 \input{./preambleForGeneratedDocuments.tex}
329 %\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
334 %----------// APPENDIX \\-----------%
338 %----------// BIB \\-----------%
340 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section
341 \bibliographystyle{alpha}
342 \bibliography{references}
345 %----------// WORK TIME \\-----------%
347 \section{Stundenliste}
349 \begin{longtable}[h]{l p{6.5cm} c c r}
350 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\
353 29.06.2011 & Treffen mit Geiger und Neuper & 15:00 & 17:30 & 2,50\\
354 02.07.2011 & Beispielaufbereitung (Bsp. Geiger Mail) & 20:00 & 21:30 & 1,50\\
355 03.07.2011 & Beispielaufbereitung, Vorraussetzungsausw. & 21:00 & 22:45 & 1,75\\
356 05.07.2011 & Treffen mit Neuper, Informationsaustausch & 10:00 & 13:00 & 3,00\\
357 06.07.2011 & Isabelle Installation & 20:00 & 22:30 & 2,50\\
358 07.07.2011 & Treffen mit Neuper, Präsentationsvorbereitung & 14:45 & 16:15 & 1,50\\
359 18.07.2011 & Präsentationsvorbereitung - Struktur & 14:15 & 16:00 & 1,75\\
360 19.07.2011 & Präsentationsvorbereitung - Inhalt & 07:20 & 09:20 & 2,00\\
361 19.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\
362 21.07.2011 & HG Fehlersuche, Latex Ausarbeitung & 11:10 & 14:00 & 2,83\\
363 22.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\
364 23.07.2011 & Berechnungen in Latex fertigstellen & 13:45 & 16:30 & 2,75\\
365 24.07.2011 & Präsentation fertigstellen & 20:10 & 20:40 & 0,50\\
366 25.07.2011 & Treffen mit Neuper, Präsentation \& erste Tests & 15:15 & 17:55 & 2,67\\
367 26.07.2011 & Test\_Complex.thy erarbeiten & 10:45 & 12:10 & 1,42\\
368 27.07.2011 & present-1 mit Neuper, Geiger & 10:00 & 12:00 & 2,00\\
370 02.09.2011 & Treffen mit Neuper, Vorlage Bakk-Arbeit & 08:30 & 10:20 & 1,83\\
371 05.09.2011 & Treffen mit Neuper, Beginn Partialbruchzerlegung & 09:30 & 12:45 & 3,25\\
372 05.09.2011 & Partialbruchzerlegung & 17:10 & 18:30 & 1,33\\
373 06.09.2011 & Dokumentation Partialbruchzerlegung & 10:00 & 13:15 & 3,25\\
374 07.09.2011 & Treffen mit Neuper, Einführung Programmierung & 10:00 & 12:50 & 2,83\\
375 08.09.2011 & Latex Umgebung einrichten - Theory export & 19:00 & 22:45 & 3,75\\
376 09.09.2011 & Latex Umgebung einrichten - Makefile & 11:40 & 15:00 & 3,33\\
377 10.09.2011 & Treffen mit Neuper, HG Fehler, Skript Inv.-Z-Transf. & 10:00 & 12:00 & 2,00\\
378 14.09.2011 & Skript Inv.-Z-Transf Prgrammierung & 09:10 & 12:25 & 3,25\\
379 16.09.2011 & Informationssammlung Summen & 13:15 & 16:00 & 2,75\\
380 19.09.2011 & Programmierübung & 10:00 & 13:10 & 3,17\\
381 20.09.2011 & Trefffen mit Neuper, Unterstützung bei Program. & 15:30 & 18:10 & 2,67\\
382 23.09.2011 & Neukonfiguration IsaMakefile & 13:00 & 14:30 & 1,50\\
383 23.09.2011 & Treffen Neuper, Programmierung Build\_Inverse\_Z & 14:30 & 17:30 & 3,00\\
384 26.09.2011 & Skript Partialbruchzerlegung - getArgument & 13:30 & 16:15 & 2,75\\
385 27.09.2011 & Treffen mit Neuper, HG Fehler & 09:00 & 12:20 & 3,33\\
386 28.09.2011 & Treffen mit Neuper, Dateiumstrukturierung & 10:00 & 12:30 & 2,50\\
387 01.10.2011 & Testen & 10:00 & 11:00 & 1,00\\
388 02.10.2011 & Fehlersuche & 15:00 & 16:10 & 1,17\\
389 06.10.2011 & Treffen mit Neuper & 15:00 & 17:50 & 2,83\\
390 07.10.2011 & Treffen mit Neuper, Programmbesprechung & 15:00 & 16:50 & 1,83\\
391 09.10.2011 & Bakk. Arbeit & 16:30 & 18:45 & 2,25\\
392 11.10.2011 & Treffen mit Neuper, Programmbespr., Abstract & 14:10 & 17:10 & 3,00
396 \section{Calculations}