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}
9 %%--01-- pointer or label to related works
11 %define document class
12 \documentclass[a4paper, 12pt]{article}
14 %packages for language and input
15 \usepackage[english]{babel}
16 \usepackage[T1]{fontenc}
17 \usepackage[latin1]{inputenc}
25 \usepackage[pdfpagelabels]{hyperref}
26 \usepackage{longtable}
28 %isabelle relevant packages
29 \usepackage{isabelle,isabellesym}
32 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
33 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
35 %----------// BEGIN DOCUMENT \\----------%
39 %----------// INFO SETUP \\----------%
43 \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
45 \sisac-Team in Cooperation with \\~\\
46 Institute for Software Technology\\
47 Institute of Signal Processing and Speech Communication\\~\\
48 Graz University of Technology\\
51 Supervisor: Univ.-Prof. Dipl.-Ing. Dr.techn. Franz Wotawa
55 \author{Jan Simon Rocnik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}}
59 %----------// TITLE PAGE \\----------%
63 \thispagestyle{empty}\end{titlepage}
66 %----------// THANKS \\----------%
72 \emph{Dr.techn. Walther Neuper}\\
73 \emph{Dipl.-Ing. Bernhard Geiger}
78 %----------// ABSTRACT \\----------%
81 The Baccalaureate Thesis creates interactive course material for Signal Processing based on the experimental math assistant Isabelle/\sisac.
83 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.
85 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 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 ``CTP-based programming language'', because error messages are still not user-friendly and need frequent contact with \sisac-developers.
89 So the practical outcome of this thesis is twofold:
91 (1) 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
93 (2) 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.
94 \end{abstract}\clearpage
100 \pagenumbering{arabic}
104 This thesis is structured into a generell part describing the math fundamentals, a practical part including the work on \cal{ISAC} and finally the management part overviewing the work process.
106 %----------// PART-1 \\----------%
108 \part{Project Fundamentals}
110 \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 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.
114 \par Mathematics mechanized in Computer Theorem Provers \emph{(CTP)} has (almost) a problem with traditional mathematical 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 would have a problem to interpret them correctly. In different problems, symbols and letters have different meanings and ask for different ways to get through. 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.
115 \par This thesis tries to \empg{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. For others see related works. %--01--
116 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 hand.
118 \subsection{Mechanization of Mathematics}
122 hughe theories of mathematics
124 still a hugh gap between these theories and ``real applications'' e.g. in SP
126 ? academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modelling --- mechanized math starts from mathematical models and (hopefully !) proceeds to match physics.
128 CTP Isabelle ... survey of knowledge, links to knowledge
133 adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics.
135 \subsection{Goals of the Thesis}
140 \subsection{Structure of the Thesis}
144 \section{Mechanization of Mathematics for SP Problems}
147 \subsection{Relevant Knowledge available in Isabelle}
150 \paragraph{example FFT}, describe in detail !!!!
152 ? different meaning: FFT in Maple
154 gap between what is available and what is required (@)!
156 traditional notation ?
158 \subsection{Relevant Knowledge available in isac}
161 specifications (``application axis'') and methods (``algorithmic axis'')
163 partial fractions, cancellation of multivariate rational terms, ...
165 \subsection{Survey: Available Knowledge and Selected Problems}
168 estimate gap (@) for each problem (tables)
170 conclusion: following order for implementing the problems ...
172 \subsection{Formalization of missing knowledge in Isabelle}
175 axiomatization ... where ... and
177 \subsection{Notes on Problems with Traditional Notation}
178 Due the thesis work we discorvers severell problems of traditional notations.
182 f x = why not f(x) ?!?!
186 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,...)
188 %----------// PART 2 \\----------%
190 \part{Implementation}
192 %\section{Implementation of Certain SP Problems}
193 %tell why only choosen one problem given by geiger
195 %\subsection{Formal Specification of Problems}
198 %\subsection{Methods Solving the Problems}
201 %\subsection{Integration of Subproblems available in isac}
204 %\subsection{Examples and Multimedia Content}
208 \input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
212 %----------// PART 3 \\----------%
214 \part{Project Management}
216 \section{Milestones for the Project}
217 Die Planung des Projekts teilt sich in folgende Iterationen:
219 \item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
220 identify problems relevant for certain SP lectures
222 estimate chances to realized them within the scope of this thesis
224 order for implementing the problems negotiated with lecturers
227 \item \textbf{1. Prsentation - Auswhlen der realisierbaren Themengebiete} (27.07.)
228 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
229 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
230 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
231 \item \textbf{2. Prsentation - Abschluss der Arbeit} (todo)
234 \section{Beschreibung der Meilensteine}\label{ms-desc}
236 \section{Bericht zum Projektverlauf}
239 \section{Related Work and Open Questions}
242 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
244 \section{Abschliesende Bemerkungen}
251 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section
252 \bibliographystyle{alpha}
253 \bibliography{references}
258 %----------// APPENDIX \\-----------%
263 \section{Stundenliste}
265 \begin{longtable}[h]{l p{6.5cm} c c r}
266 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\
269 29.06.2011 & Treffen mit Geiger und Neuper & 15:00 & 17:30 & 2,50\\
270 02.07.2011 & Beispielaufbereitung (Bsp. Geiger Mail) & 20:00 & 21:30 & 1,50\\
271 03.07.2011 & Beispielaufbereitung, Vorraussetzungsausw. & 21:00 & 22:45 & 1,75\\
272 05.07.2011 & Treffen mit Neuper, Informationsaustausch & 10:00 & 13:00 & 3,00\\
273 06.07.2011 & Isabelle Installation & 20:00 & 22:30 & 2,50\\
274 07.07.2011 & Treffen mit Neuper, Präsentationsvorbereitung & 14:45 & 16:15 & 1,50\\
275 18.07.2011 & Präsentationsvorbereitung - Struktur & 14:15 & 16:00 & 1,75\\
276 19.07.2011 & Präsentationsvorbereitung - Inhalt & 07:20 & 09:20 & 2,00\\
277 19.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\
278 21.07.2011 & HG Fehlersuche, Latex Ausarbeitung & 11:10 & 14:00 & 2,83\\
279 22.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\
280 23.07.2011 & Berechnungen in Latex fertigstellen & 13:45 & 16:30 & 2,75\\
281 24.07.2011 & Präsentation fertigstellen & 20:10 & 20:40 & 0,50\\
282 25.07.2011 & Treffen mit Neuper, Präsentation \& erste Tests & 15:15 & 17:55 & 2,67\\
283 26.07.2011 & Test\_Complex.thy erarbeiten & 10:45 & 12:10 & 1,42\\
284 27.07.2011 & present-1 mit Neuper, Geiger & 10:00 & 12:00 & 2,00\\
286 02.09.2011 & Treffen mit Neuper, Vorlage Bakk-Arbeit & 08:30 & 10:20 & 1,83\\
287 05.09.2011 & Treffen mit Neuper, Beginn Partialbruchzerlegung & 09:30 & 12:45 & 3,25\\
288 05.09.2011 & Partialbruchzerlegung & 17:10 & 18:30 & 1,33\\
289 06.09.2011 & Dokumentation Partialbruchzerlegung & 10:00 & 13:15 & 3,25\\
290 07.09.2011 & Treffen mit Neuper, Einführung Programmierung & 10:00 & 12:50 & 2,83\\
291 08.09.2011 & Latex Umgebung einrichten - Theory export & 19:00 & 22:45 & 3,75\\
292 09.09.2011 & Latex Umgebung einrichten - Makefile & 11:40 & 15:00 & 3,33\\
293 10.09.2011 & Treffen mit Neuper, HG Fehler, Skript Inv.-Z-Transf. & 10:00 & 12:00 & 2,00\\
294 14.09.2011 & Skript Inv.-Z-Transf Prgrammierung & 09:10 & 12:25 & 3,25\\
295 16.09.2011 & Informationssammlung Summen & 13:15 & 16:00 & 2,75\\
296 19.09.2011 & Programmierübung & 10:00 & 13:10 & 3,17\\
297 20.09.2011 & Trefffen mit Neuper, Unterstützung bei Program. & 15:30 & 18:10 & 2,67\\
298 23.09.2011 & Neukonfiguration IsaMakefile & 13:00 & 14:30 & 1,50\\
299 23.09.2011 & Treffen Neuper, Programmierung Build\_Inverse\_Z & 14:30 & 17:30 & 3,00\\
300 26.09.2011 & Skript Partialbruchzerlegung - getArgument & 13:30 & 16:15 & 2,75\\
301 27.09.2011 & Treffen mit Neuper, HG Fehler & 09:00 & 12:20 & 3,33\\
302 28.09.2011 & Treffen mit Neuper, Dateiumstrukturierung & 10:00 & 12:30 & 2,50\\
303 01.10.2011 & Testen & 10:00 & 11:00 & 1,00\\
304 02.10.2011 & Fehlersuche & 15:00 & 16:10 & 1,17\\
305 06.10.2011 & Treffen mit Neuper & 15:00 & 17:50 & 2,83\\
306 07.10.2011 & Treffen mit Neuper, Programmbesprechung & 15:00 & 16:50 & 1,83\\
307 09.10.2011 & Bakk. Arbeit & 16:30 & 18:45 & 2,25\\
308 11.10.2011 & Treffen mit Neuper, Programmbespr., Abstract & 14:10 & 17:10 & 3,00
312 \section{Calculations}