doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex
author Jan Rocnik <jan.rocnik@student.tugraz.at>
Wed, 19 Oct 2011 23:11:45 +0200
branchdecompose-isar
changeset 42323 38bac98d960d
parent 42322 af49cb4959b6
child 42324 829d75932dc0
permissions -rwxr-xr-x
tuned
jan@42322
     1
%   Title:  bakkarbeit_jrocnik.tex
jan@42322
     2
%   Author: Jan Rocnik
jan@42322
     3
%   (c) copyright due to lincense terms.
jan@42322
     4
%2345678901234567890123456789012345678901234567890123456789012345678901234567890
jan@42322
     5
%       10        20        30        40        50        60        70        80
jan@42322
     6
jan@42322
     7
%TODO:
jan@42322
     8
%%\cite{proakis2004contemporary}
jan@42322
     9
%%--01-- pointer or label to related works
jan@42322
    10
jan@42322
    11
%define document class
jan@42307
    12
\documentclass[a4paper, 12pt]{article}
jan@42235
    13
jan@42322
    14
%packages for language and input
jan@42307
    15
\usepackage[english]{babel} 
jan@42235
    16
\usepackage[T1]{fontenc}
jan@42235
    17
\usepackage[latin1]{inputenc}
jan@42235
    18
jan@42322
    19
%generel packages
jan@42307
    20
\usepackage{url}
neuper@42073
    21
\usepackage{graphicx}
jan@42246
    22
\usepackage{endnotes}
jan@42246
    23
\usepackage{trfsigns}
jan@42246
    24
\usepackage{setspace}
jan@42307
    25
\usepackage[pdfpagelabels]{hyperref}
jan@42316
    26
\usepackage{longtable}
jan@42322
    27
jan@42322
    28
%isabelle relevant packages
jan@42316
    29
\usepackage{isabelle,isabellesym}
jan@42235
    30
jan@42322
    31
%define isac logos
neuper@42073
    32
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
neuper@42073
    33
\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
neuper@42073
    34
jan@42323
    35
jan@42322
    36
%----------// BEGIN DOCUMENT \\----------%
jan@42322
    37
neuper@42073
    38
\begin{document}
neuper@42073
    39
jan@42316
    40
%----------// INFO SETUP \\----------%
jan@42316
    41
jan@42235
    42
\title{
jan@42235
    43
	\Large{
jan@42235
    44
  	\bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
jan@42235
    45
  }
jan@42307
    46
	\sisac-Team in Cooperation with \\~\\
jan@42307
    47
	Institute for Software Technology\\
jan@42307
    48
	Institute of Signal Processing and Speech Communication\\~\\
jan@42276
    49
	Graz University of Technology\\
jan@42235
    50
	\vspace{0.7cm}
jan@42307
    51
	\normalsize{
jan@42316
    52
		Supervisor: Univ.-Prof. Dipl.-Ing. Dr.techn. Franz Wotawa
jan@42235
    53
	}
jan@42235
    54
}
jan@42307
    55
jan@42307
    56
\author{Jan Simon Rocnik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}}
jan@42235
    57
jan@42235
    58
\date{\today}
jan@42307
    59
jan@42316
    60
%----------// TITLE PAGE \\----------%
jan@42316
    61
jan@42307
    62
\begin{titlepage}
neuper@42073
    63
\maketitle
jan@42307
    64
\thispagestyle{empty}\end{titlepage}
neuper@42073
    65
\clearpage
jan@42307
    66
jan@42316
    67
%----------// THANKS \\----------%
jan@42316
    68
jan@42307
    69
\setcounter{page}{2}
jan@42307
    70
\begin{center}
jan@42307
    71
Special Thanks to\\
jan@42307
    72
\hfill \\
jan@42307
    73
\emph{Dr.techn. Walther Neuper}\\
jan@42307
    74
\emph{Dipl.-Ing. Bernhard Geiger}
jan@42307
    75
\end{center}
jan@42307
    76
\thispagestyle{empty}
jan@42307
    77
\clearpage
jan@42307
    78
jan@42316
    79
%----------// ABSTRACT \\----------%
jan@42307
    80
jan@42307
    81
\begin{abstract}
jan@42323
    82
The Baccalaureate Thesis creates interactive course material for Signal Processing based on the experimental math assistant Isabelle and provides it within {\sisac} (Isabelle for Calculations).
jan@42323
    83
\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.
jan@42307
    84
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.
jan@42323
    85
\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.
jan@42307
    86
So the practical outcome of this thesis is twofold:
jan@42323
    87
\begin{enumerate}
jan@42323
    88
\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
jan@42323
    89
\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. 
jan@42323
    90
\end{enumerate}
jan@42307
    91
\end{abstract}\clearpage
jan@42307
    92
jan@42323
    93
%----------// T O C \\----------%
jan@42307
    94
jan@42307
    95
\pagenumbering{Roman}
jan@42323
    96
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.
neuper@42073
    97
\tableofcontents
neuper@42073
    98
\clearpage
jan@42307
    99
\pagenumbering{arabic}
jan@42323
   100
\setcounter{page}{6}
jan@42316
   101
jan@42316
   102
%----------// PART-1 \\----------%
jan@42316
   103
jan@42316
   104
\part{Project Fundamentals}
neuper@42304
   105
jan@42322
   106
\section{Introduction}
jan@42322
   107
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.
jan@42322
   108
\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.
jan@42323
   109
\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.
jan@42322
   110
\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--
jan@42323
   111
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.
neuper@42304
   112
neuper@42240
   113
\subsection{Mechanization of Mathematics}
jan@42323
   114
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. 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:
jan@42323
   115
\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.
jan@42323
   116
\par A computer or a CTP-System builds on programms witth predefined logical ruels and does not know any mathematical trick or recipe to walk around difficult expressions. For such a system the only possibility is to work through its known definitions vulgo theories 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. 
jan@42323
   117
\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.
neuper@42240
   118
neuper@42240
   119
\subsection{Goals of the Thesis}
jan@42323
   120
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?
jan@42323
   121
\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.
neuper@42240
   122
neuper@42240
   123
\section{Mechanization of Mathematics for SP Problems}
neuper@42240
   124
neuper@42240
   125
\subsection{Relevant Knowledge available in Isabelle}
neuper@42240
   126
todo
neuper@42240
   127
neuper@42240
   128
\paragraph{example FFT}, describe in detail !!!! 
neuper@42240
   129
neuper@42240
   130
? different meaning: FFT in Maple
neuper@42240
   131
neuper@42240
   132
gap between what is available and what is required (@)!
neuper@42240
   133
neuper@42240
   134
traditional notation ?
neuper@42240
   135
jan@42307
   136
\subsection{Relevant Knowledge available in isac}
neuper@42240
   137
todo
neuper@42240
   138
neuper@42240
   139
specifications (``application axis'') and methods (``algorithmic axis'')
neuper@42240
   140
neuper@42240
   141
partial fractions, cancellation of multivariate rational terms, ...
neuper@42240
   142
neuper@42240
   143
\subsection{Survey: Available Knowledge and Selected Problems}
neuper@42240
   144
todo
neuper@42240
   145
neuper@42240
   146
estimate gap (@) for each problem (tables)
neuper@42240
   147
neuper@42240
   148
conclusion: following order for implementing the problems ...
neuper@42240
   149
neuper@42240
   150
\subsection{Formalization of missing knowledge in Isabelle}
neuper@42240
   151
todo
neuper@42240
   152
neuper@42240
   153
axiomatization ... where ... and
neuper@42240
   154
neuper@42240
   155
\subsection{Notes on Problems with Traditional Notation}
jan@42322
   156
Due the thesis work we discorvers severell problems of traditional notations.
neuper@42240
   157
neuper@42240
   158
u[n] !!
neuper@42240
   159
neuper@42240
   160
f x =  why not f(x) ?!?!
neuper@42240
   161
neuper@42240
   162
...
neuper@42240
   163
jan@42276
   164
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,...)
jan@42276
   165
jan@42323
   166
\clearpage
jan@42323
   167
jan@42316
   168
%----------// PART 2 \\----------%
jan@42316
   169
jan@42316
   170
\part{Implementation}
jan@42316
   171
jan@42316
   172
%\section{Implementation of Certain SP Problems}
jan@42316
   173
%tell why only choosen one problem given by geiger
jan@42316
   174
%
jan@42316
   175
%\subsection{Formal Specification of Problems}
jan@42316
   176
%todo
jan@42316
   177
%
jan@42316
   178
%\subsection{Methods Solving the Problems}
jan@42316
   179
%todo
jan@42316
   180
%
jan@42316
   181
%\subsection{Integration of Subproblems available in isac}
jan@42316
   182
%todo
jan@42316
   183
%
jan@42316
   184
%\subsection{Examples and Multimedia Content}
jan@42316
   185
%todo
jan@42316
   186
jan@42316
   187
{\center todo}
jan@42322
   188
\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
jan@42316
   189
jan@42316
   190
\clearpage
jan@42316
   191
jan@42316
   192
%----------// PART 3 \\----------%
jan@42316
   193
jan@42316
   194
\part{Project Management}
jan@42316
   195
jan@42316
   196
\section{Milestones for the Project}
jan@42316
   197
Die Planung des Projekts teilt sich in folgende Iterationen:
jan@42316
   198
\begin{enumerate}
jan@42316
   199
\item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
jan@42316
   200
identify problems relevant for certain SP lectures
jan@42316
   201
jan@42316
   202
estimate chances to realized them within the scope of this thesis
jan@42316
   203
jan@42316
   204
order for implementing the problems negotiated with lecturers
jan@42316
   205
jan@42316
   206
jan@42316
   207
\item \textbf{1. Prsentation - Auswhlen der realisierbaren Themengebiete} (27.07.)
jan@42316
   208
\item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
jan@42316
   209
\item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
jan@42316
   210
\item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
jan@42316
   211
\item \textbf{2. Prsentation - Abschluss der Arbeit} (todo)
jan@42316
   212
\end{enumerate}
jan@42316
   213
jan@42316
   214
\section{Beschreibung der Meilensteine}\label{ms-desc}
neuper@42240
   215
todo
jan@42316
   216
\section{Bericht zum Projektverlauf}
neuper@42240
   217
todo
neuper@42240
   218
neuper@42240
   219
\section{Related Work and Open Questions}
neuper@42240
   220
todo
neuper@42240
   221
neuper@42240
   222
See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
neuper@42240
   223
jan@42235
   224
\section{Abschliesende Bemerkungen}
jan@42235
   225
todo
neuper@42073
   226
jan@42316
   227
jan@42316
   228
neuper@42073
   229
\clearpage
neuper@42073
   230
jan@42309
   231
\renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section
jan@42309
   232
\bibliographystyle{alpha}
jan@42309
   233
\bibliography{references}
neuper@42073
   234
neuper@42073
   235
\clearpage
neuper@42073
   236
jan@42316
   237
jan@42316
   238
%----------// APPENDIX \\-----------%
jan@42316
   239
neuper@42073
   240
\appendix
jan@42251
   241
neuper@42073
   242
neuper@42073
   243
\section{Stundenliste}
jan@42316
   244
\begin{footnotesize}
jan@42316
   245
\begin{longtable}[h]{l p{6.5cm} c c r}
jan@42316
   246
{\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\
jan@42316
   247
\hline \hline
jan@42316
   248
\endhead
jan@42316
   249
29.06.2011 & Treffen mit Geiger und Neuper & 15:00 & 17:30 & 2,50\\ 
jan@42316
   250
02.07.2011 & Beispielaufbereitung (Bsp. Geiger Mail) & 20:00 & 21:30 & 1,50\\ 
jan@42316
   251
03.07.2011 & Beispielaufbereitung, Vorraussetzungsausw. & 21:00 & 22:45 & 1,75\\ 
jan@42316
   252
05.07.2011 & Treffen mit Neuper, Informationsaustausch & 10:00 & 13:00 & 3,00\\ 
jan@42316
   253
06.07.2011 & Isabelle Installation & 20:00 & 22:30 & 2,50\\ 
jan@42316
   254
07.07.2011 & Treffen mit Neuper, Präsentationsvorbereitung & 14:45 & 16:15 & 1,50\\ 
jan@42316
   255
18.07.2011 & Präsentationsvorbereitung - Struktur & 14:15 & 16:00 & 1,75\\ 
jan@42316
   256
19.07.2011 & Präsentationsvorbereitung - Inhalt & 07:20 & 09:20 & 2,00\\ 
jan@42316
   257
19.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\ 
jan@42316
   258
21.07.2011 & HG Fehlersuche, Latex Ausarbeitung & 11:10 & 14:00 & 2,83\\ 
jan@42316
   259
22.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\ 
jan@42316
   260
23.07.2011 & Berechnungen in Latex fertigstellen & 13:45 & 16:30 & 2,75\\ 
jan@42316
   261
24.07.2011 & Präsentation fertigstellen & 20:10 & 20:40 & 0,50\\ 
jan@42316
   262
25.07.2011 & Treffen mit Neuper, Präsentation \& erste Tests & 15:15 & 17:55 & 2,67\\ 
jan@42316
   263
26.07.2011 & Test\_Complex.thy erarbeiten & 10:45 & 12:10 & 1,42\\ 
jan@42316
   264
27.07.2011 & present-1 mit Neuper, Geiger & 10:00 & 12:00 & 2,00\\
jan@42316
   265
\hline 
jan@42316
   266
02.09.2011 & Treffen mit Neuper, Vorlage Bakk-Arbeit & 08:30 & 10:20 & 1,83\\ 
jan@42316
   267
05.09.2011 & Treffen mit Neuper, Beginn Partialbruchzerlegung & 09:30 & 12:45 & 3,25\\ 
jan@42316
   268
05.09.2011 & Partialbruchzerlegung & 17:10 & 18:30 & 1,33\\ 
jan@42316
   269
06.09.2011 & Dokumentation Partialbruchzerlegung & 10:00 & 13:15 & 3,25\\ 
jan@42316
   270
07.09.2011 & Treffen mit Neuper, Einführung Programmierung & 10:00 & 12:50 & 2,83\\ 
jan@42316
   271
08.09.2011 & Latex Umgebung einrichten - Theory export & 19:00 & 22:45 & 3,75\\ 
jan@42316
   272
09.09.2011 & Latex Umgebung einrichten - Makefile & 11:40 & 15:00 & 3,33\\ 
jan@42316
   273
10.09.2011 & Treffen mit Neuper, HG Fehler, Skript Inv.-Z-Transf. & 10:00 & 12:00 & 2,00\\ 
jan@42316
   274
14.09.2011 & Skript Inv.-Z-Transf Prgrammierung & 09:10 & 12:25 & 3,25\\ 
jan@42316
   275
16.09.2011 & Informationssammlung Summen & 13:15 & 16:00 & 2,75\\ 
jan@42316
   276
19.09.2011 & Programmierübung & 10:00 & 13:10 & 3,17\\ 
jan@42316
   277
20.09.2011 & Trefffen mit Neuper, Unterstützung bei Program. & 15:30 & 18:10 & 2,67\\ 
jan@42316
   278
23.09.2011 & Neukonfiguration IsaMakefile & 13:00 & 14:30 & 1,50\\ 
jan@42316
   279
23.09.2011 & Treffen Neuper, Programmierung Build\_Inverse\_Z & 14:30 & 17:30 & 3,00\\ 
jan@42316
   280
26.09.2011 & Skript Partialbruchzerlegung - getArgument & 13:30 & 16:15 & 2,75\\ 
jan@42316
   281
27.09.2011 & Treffen mit Neuper, HG Fehler & 09:00 & 12:20 & 3,33\\ 
jan@42316
   282
28.09.2011 & Treffen mit Neuper, Dateiumstrukturierung & 10:00 & 12:30 & 2,50\\ 
jan@42316
   283
01.10.2011 & Testen & 10:00 & 11:00 & 1,00\\ 
jan@42316
   284
02.10.2011 & Fehlersuche & 15:00 & 16:10 & 1,17\\ 
jan@42316
   285
06.10.2011 & Treffen mit Neuper & 15:00 & 17:50 & 2,83\\ 
jan@42316
   286
07.10.2011 & Treffen mit Neuper, Programmbesprechung & 15:00 & 16:50 & 1,83\\ 
jan@42316
   287
09.10.2011 & Bakk. Arbeit & 16:30 & 18:45 & 2,25\\ 
jan@42316
   288
11.10.2011 & Treffen mit Neuper, Programmbespr., Abstract & 14:10 & 17:10 & 3,00
jan@42316
   289
\end{longtable}
jan@42316
   290
\end{footnotesize}
neuper@42073
   291
jan@42246
   292
\section{Calculations}
jan@42251
   293
\input{calulations}
neuper@42073
   294
\end{document}