1.1 --- a/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Thu Oct 20 19:42:34 2011 +0200
1.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Tue Oct 25 23:50:45 2011 +0200
1.3 @@ -6,7 +6,11 @@
1.4
1.5 %TODO:
1.6 %%\cite{proakis2004contemporary}
1.7 -%%--01-- pointer or label to related works
1.8 +%%
1.9 +%%patch:
1.10 +%%structur: theory part ersetzt project undamentals
1.11 +%% "mechanization of math in isac" ersetzt introduction
1.12 +%% authoring math in isac ersetzt mechanization
1.13
1.14 %define document class
1.15 \documentclass[a4paper, 12pt]{article}
1.16 @@ -24,8 +28,13 @@
1.17 \usepackage{setspace}
1.18 \usepackage[pdfpagelabels]{hyperref}
1.19 \usepackage{longtable}
1.20 +
1.21 \usepackage{float} %For restylefloat
1.22 -\restylefloat{table}
1.23 +\newfloat{example}{h}{} %self made floats
1.24 +\floatname{example}{Example} %name for float
1.25 +\restylefloat{table} %float tables
1.26 +\floatstyle{ruled} %boxes around floats
1.27 +\restylefloat{example} %float examples --> boxes
1.28
1.29 %isabelle relevant packages
1.30 \usepackage{isabelle,isabellesym}
1.31 @@ -34,53 +43,41 @@
1.32 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.33 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.34
1.35 +\newcommand{\HRule}{\rule{\linewidth}{0.2mm}}
1.36 +
1.37 %----------// BEGIN DOCUMENT \\----------%
1.38
1.39 \begin{document}
1.40
1.41 -%----------// INFO SETUP \\----------%
1.42 -
1.43 -\title{
1.44 - \Large{
1.45 - \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
1.46 - }
1.47 - \sisac-Team in Cooperation with \\~\\
1.48 - Institute for Software Technology\\
1.49 - Institute of Signal Processing and Speech Communication\\~\\
1.50 - Graz University of Technology\\
1.51 - \vspace{0.7cm}
1.52 - \normalsize{
1.53 - Supervisor: Univ.-Prof. Dipl.-Ing. Dr.techn. Franz Wotawa
1.54 - }
1.55 -}
1.56 -
1.57 -\author{Jan Simon Rocnik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}}
1.58 -
1.59 -\date{\today}
1.60 -
1.61 %----------// TITLE PAGE \\----------%
1.62
1.63 -\begin{titlepage}
1.64 -\maketitle
1.65 -\thispagestyle{empty}\end{titlepage}
1.66 -\clearpage
1.67 +\input{./bakkarbeit_titlepage.tex}
1.68 +\cleardoublepage
1.69 +
1.70 +%----------// EMPTY PAGE \\----------%
1.71 +
1.72 +%todo
1.73
1.74 %----------// THANKS \\----------%
1.75
1.76 \setcounter{page}{2}
1.77 \begin{center}
1.78 -Special Thanks to\\
1.79 -\hfill \\
1.80 -\emph{Dr.techn. Walther Neuper}\\
1.81 -\emph{Dipl.-Ing. Bernhard Geiger}
1.82 + Special Thanks to\\
1.83 + \hfill \\
1.84 + \emph{Dr.techn. Walther Neuper}\\
1.85 + \emph{Dipl.-Ing. Bernhard Geiger}
1.86 \end{center}
1.87 \thispagestyle{empty}
1.88 -\clearpage
1.89 +\cleardoublepage
1.90 +
1.91 +%----------// EMPTY PAGE \\----------%
1.92 +
1.93 +%todo
1.94
1.95 %----------// ABSTRACT \\----------%
1.96
1.97 \begin{abstract}
1.98 -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).
1.99 +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).
1.100 \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.
1.101 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.
1.102 \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.
1.103 @@ -89,12 +86,13 @@
1.104 \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
1.105 \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.
1.106 \end{enumerate}
1.107 -\end{abstract}\clearpage
1.108 +\end{abstract}
1.109 +\clearpage
1.110
1.111 %----------// T O C \\----------%
1.112
1.113 \pagenumbering{Roman}
1.114 -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.
1.115 +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.
1.116 \tableofcontents
1.117 \clearpage
1.118 \pagenumbering{arabic}
1.119 @@ -104,10 +102,34 @@
1.120
1.121 \part{Project Fundamentals}
1.122
1.123 +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.
1.124 +
1.125 \section{Introduction}
1.126 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.
1.127 -\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.
1.128 -\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.
1.129 +\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.
1.130 +\par 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}})
1.131 +
1.132 +\begin{example}
1.133 + \begin{center}
1.134 + \begin{math}u\left[n\right] \ldots unitstep \end{math}
1.135 + \end{center}
1.136 + {\small\emph{
1.137 + The unitstep is something we need to solve Signal Processing problem classes. But in {\sisac{}} the rectangular brekats have already a meaning. So we abuse them for our requirements. We get something which is not defined but useable. The Result is only syntax without semantic.}
1.138 + }
1.139 + \caption{Symbol Interpretation}\label{eg:symbint1}
1.140 +\end{example}
1.141 +
1.142 +\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}})
1.143 +\begin{example}
1.144 + \begin{center}
1.145 +todo
1.146 + \end{center}
1.147 + {\small\emph{
1.148 + The unitstep is something we need to solve Signal Processing problem classes. But in {\sisac{}} the rectangular brekats have already a meaning. So we abuse them for our requirements. We get something which is not defined but useable. The Result is only syntax without semantic.}
1.149 + }
1.150 + \caption{Symbol Interpretation}\label{eg:symbint2}
1.151 +\end{example}
1.152 +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.
1.153 \par This thesis tries to \emph{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. For others see related works in section \ref{sec:related}.
1.154 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.
1.155
1.156 @@ -117,7 +139,7 @@
1.157 \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.
1.158 \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.
1.159
1.160 -\subsection{Goals of the Thesis}
1.161 +\subsection{Goals of the Thesis}\label{sec:goals}
1.162 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?
1.163 \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.
1.164 \par Another goal is to demonstrate the power and attractivity of {\sisac}.
1.165 @@ -222,59 +244,31 @@
1.166
1.167 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,...)
1.168
1.169 -\clearpage
1.170 +\section{Milestones for the Thesis}
1.171 +The thesis was splitted into six iterations
1.172 +\begin{description}
1.173 +\item[(29.06. -- 27.07.)] Collection of detailed informations about different STEOP topics \ref{ssec:infcol}
1.174 +\item[(27.07.)] First Prsentation - Decition on which Problems will be implemented \ref{ssec:pres1}
1.175 +\item[(01.09. -- 11.11.)] Implementing the Problem Class in {\sisac{}} \ref{ssec:impl}
1.176 +\item[(14.11. -- 02.12.)] Documentation of the Implementation \ref{ssec:doc}
1.177 +\item[(05.12. -- todo)] Writting on the thesis \ref{ssec:thes}
1.178 +\item[todo] Second Prsentation - Work review \ref{ssec:pres2}
1.179 +\end{description}
1.180
1.181 -%----------// PART 2 \\----------%
1.182 +\section{Detailed Milestone Description}
1.183 +\subsection{Collection of detailed informations about different STEOP topics}\label{ssec:infcol}
1.184 +identify problems relevant for certain SP lectures
1.185 +estimate chances to realized them within the scope of this thesis
1.186 +order for implementing the problems negotiated with lecturers
1.187 +\subsection{First Prsentation - Decition on which Problems will be implemented}\label{ssec:pres1}
1.188 +\subsection{Implementing the Problem Class in {\sisac}}\label{ssec:impl}
1.189 +\subsection{Documentation of the Implementation}\label{ssec:doc}
1.190 +\subsection{Writting on the thesis}\label{ssec:thes}
1.191 +\subsection{Second Prsentation - Work review}\label{ssec:pres2}
1.192
1.193 -\part{Implementation}
1.194 -
1.195 -%\section{Implementation of Certain SP Problems}
1.196 -%tell why only choosen one problem given by geiger
1.197 -%
1.198 -%\subsection{Formal Specification of Problems}
1.199 -%todo
1.200 -%
1.201 -%\subsection{Methods Solving the Problems}
1.202 -%todo
1.203 -%
1.204 -%\subsection{Integration of Subproblems available in isac}
1.205 -%todo
1.206 -%
1.207 -%\subsection{Examples and Multimedia Content}
1.208 -%todo
1.209 -
1.210 -{\center todo}
1.211 -\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
1.212 -
1.213 -\clearpage
1.214 -
1.215 -%----------// PART 3 \\----------%
1.216 -
1.217 -\part{Project Management}
1.218 -
1.219 -\section{Milestones for the Project}
1.220 -Die Planung des Projekts teilt sich in folgende Iterationen:
1.221 -\begin{enumerate}
1.222 -\item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
1.223 -identify problems relevant for certain SP lectures
1.224 -
1.225 -estimate chances to realized them within the scope of this thesis
1.226 -
1.227 -order for implementing the problems negotiated with lecturers
1.228 -
1.229 -
1.230 -\item \textbf{1. Prsentation - Auswhlen der realisierbaren Themengebiete} (27.07.)
1.231 -\item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
1.232 -\item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
1.233 -\item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
1.234 -\item \textbf{2. Prsentation - Abschluss der Arbeit} (todo)
1.235 -\end{enumerate}
1.236 -
1.237 -\section{Beschreibung der Meilensteine}\label{ms-desc}
1.238 +\section{Review}
1.239 todo
1.240 -\section{Bericht zum Projektverlauf}
1.241 -todo
1.242 -\section{Abschliesende Bemerkungen}
1.243 +\section{Conclusions}
1.244 todo
1.245
1.246 \clearpage
1.247 @@ -286,6 +280,21 @@
1.248 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
1.249 \clearpage
1.250
1.251 +%----------// PART 2 \\----------%
1.252 +
1.253 +\part{Implementation}
1.254 +
1.255 +\input{./preambleForGeneratedDocuments.tex}
1.256 +\HRule
1.257 +%\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
1.258 +
1.259 +\clearpage
1.260 +
1.261 +
1.262 +%----------// APPENDIX \\-----------%
1.263 +
1.264 +\appendix
1.265 +
1.266 %----------// BIB \\-----------%
1.267
1.268 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section
1.269 @@ -293,10 +302,6 @@
1.270 \bibliography{references}
1.271 \clearpage
1.272
1.273 -%----------// APPENDIX \\-----------%
1.274 -
1.275 -\appendix
1.276 -
1.277 %----------// WORK TIME \\-----------%
1.278
1.279 \section{Stundenliste}