22 \usepackage{endnotes} |
22 \usepackage{endnotes} |
23 \usepackage{trfsigns} |
23 \usepackage{trfsigns} |
24 \usepackage{setspace} |
24 \usepackage{setspace} |
25 \usepackage[pdfpagelabels]{hyperref} |
25 \usepackage[pdfpagelabels]{hyperref} |
26 \usepackage{longtable} |
26 \usepackage{longtable} |
|
27 \usepackage{float} %For restylefloat |
|
28 \restylefloat{table} |
27 |
29 |
28 %isabelle relevant packages |
30 %isabelle relevant packages |
29 \usepackage{isabelle,isabellesym} |
31 \usepackage{isabelle,isabellesym} |
30 |
32 |
31 %define isac logos |
33 %define isac logos |
32 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
34 \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 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
34 |
|
35 |
36 |
36 %----------// BEGIN DOCUMENT \\----------% |
37 %----------// BEGIN DOCUMENT \\----------% |
37 |
38 |
38 \begin{document} |
39 \begin{document} |
39 |
40 |
105 |
106 |
106 \section{Introduction} |
107 \section{Introduction} |
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. |
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. |
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. |
109 \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. |
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. |
110 \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. |
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-- |
111 \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}. |
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. |
112 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. |
112 |
113 |
113 \subsection{Mechanization of Mathematics} |
114 \subsection{Mechanization of Mathematics} |
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: |
115 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: |
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. |
116 \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. |
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. |
118 \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. |
118 |
119 |
119 \subsection{Goals of the Thesis} |
120 \subsection{Goals of the Thesis} |
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? |
121 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? |
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. |
122 \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. |
122 |
123 \par Another goal is to demonstrate the power and attractivity of {\sisac}. |
123 \section{Mechanization of Mathematics for SP Problems} |
124 |
124 |
125 \section{Mechanization of Signal Processing Problems} |
125 \subsection{Relevant Knowledge available in Isabelle} |
126 \subsection{Relevant Knowledge available in Isabelle} |
126 todo |
127 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. |
|
128 \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: |
|
129 \begin{itemize} |
|
130 \item Fourier-Transformation |
|
131 \item Convolution |
|
132 \item Inverse z-Transformation and partial fraction decomposition |
|
133 \item Indextransformation |
|
134 \end{itemize} |
|
135 Following the collection and evaluation of core operations collated with isabelle: |
127 |
136 |
128 \paragraph{example FFT}, describe in detail !!!! |
137 \paragraph{example FFT}, describe in detail !!!! |
129 |
138 |
130 ? different meaning: FFT in Maple |
139 ? different meaning: FFT in Maple |
131 |
140 |
138 |
147 |
139 specifications (``application axis'') and methods (``algorithmic axis'') |
148 specifications (``application axis'') and methods (``algorithmic axis'') |
140 |
149 |
141 partial fractions, cancellation of multivariate rational terms, ... |
150 partial fractions, cancellation of multivariate rational terms, ... |
142 |
151 |
143 \subsection{Survey: Available Knowledge and Selected Problems} |
152 \subsection{Survey: Requiered Knowledge and Selected Problem(s)} |
144 todo |
153 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: |
145 |
154 |
146 estimate gap (@) for each problem (tables) |
155 \begin{table}[!H] |
147 |
156 \begin{centering} |
148 conclusion: following order for implementing the problems ... |
157 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
|
158 requirements & comments &effort\\ \hline\hline |
|
159 solving Intrgrals & simple via propertie table & 20\\ |
|
160 & \emph{real} & MT\\ \hline |
|
161 transformation table & simple transform & 20\\ \hline |
|
162 visualisation & backend & 10\\ \hline |
|
163 example collection & with explanations & 20\\ \hline\hline |
|
164 \multicolumn{2}{c|}{} & 70-80\\ |
|
165 \end{tabular} |
|
166 \par\end{centering} |
|
167 \caption{Fourier-Transformation development effort} |
|
168 \end{table} |
|
169 |
|
170 \begin{table}[H] |
|
171 \begin{centering} |
|
172 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
|
173 requirements & comments &effort\\ \hline\hline |
|
174 simplify rationals & \sisac & 0\\ \hline |
|
175 define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline |
|
176 simplify sum & termorder & 10\\ |
|
177 & simplify rules & 20\\ |
|
178 & use simplify rationals& 0\\ \hline |
|
179 index adjustments & with unit step & 10\\ \hline |
|
180 example collection & with explanations & 20\\ \hline\hline |
|
181 \multicolumn{2}{c|}{} & 70-90\\ |
|
182 \end{tabular} |
|
183 \par\end{centering} |
|
184 \caption{Convolution Operations development effort} |
|
185 \end{table} |
|
186 |
|
187 \begin{table}[H] |
|
188 \begin{centering} |
|
189 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
|
190 requirements & comments &effort\\ \hline\hline |
|
191 solve for part.fract. & \sisac: degree 2 & 0\\ |
|
192 & complex nomminators & 30\\ |
|
193 & degree > 2 & MT\\ \hline |
|
194 simplify polynomial & \sisac & 0\\ |
|
195 simplify rational & \sisac & 0\\ \hline |
|
196 partial fraction & degree 2, & 20\\ |
|
197 decomposition & specification, method& 30\\ \hline |
|
198 ${\cal Z}^{-1}$ table & explanations, figures& 20\\ \hline |
|
199 example collection & with explanations & 20\\ \hline\hline |
|
200 \multicolumn{2}{c|}{} & 90-120\\ |
|
201 % & & 1 MT |
|
202 \end{tabular} |
|
203 \par\end{centering} |
|
204 \caption{Z-Transformation development effort} |
|
205 \end{table} |
|
206 |
|
207 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}. |
149 |
208 |
150 \subsection{Formalization of missing knowledge in Isabelle} |
209 \subsection{Formalization of missing knowledge in Isabelle} |
151 todo |
210 todo |
152 |
211 |
153 axiomatization ... where ... and |
212 axiomatization ... where ... and |
213 |
272 |
214 \section{Beschreibung der Meilensteine}\label{ms-desc} |
273 \section{Beschreibung der Meilensteine}\label{ms-desc} |
215 todo |
274 todo |
216 \section{Bericht zum Projektverlauf} |
275 \section{Bericht zum Projektverlauf} |
217 todo |
276 todo |
218 |
277 \section{Abschliesende Bemerkungen} |
219 \section{Related Work and Open Questions} |
278 todo |
220 todo |
279 |
221 |
280 \clearpage |
|
281 |
|
282 %----------// RELATED \\-----------% |
|
283 |
|
284 \section{Related Work and Open Questions \label{sec:related}} |
|
285 List of related work |
222 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work |
286 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work |
223 |
287 \clearpage |
224 \section{Abschliesende Bemerkungen} |
288 |
225 todo |
289 %----------// BIB \\-----------% |
226 |
|
227 |
|
228 |
|
229 \clearpage |
|
230 |
290 |
231 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section |
291 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section |
232 \bibliographystyle{alpha} |
292 \bibliographystyle{alpha} |
233 \bibliography{references} |
293 \bibliography{references} |
234 |
294 \clearpage |
235 \clearpage |
|
236 |
|
237 |
295 |
238 %----------// APPENDIX \\-----------% |
296 %----------// APPENDIX \\-----------% |
239 |
297 |
240 \appendix |
298 \appendix |
241 |
299 |
|
300 %----------// WORK TIME \\-----------% |
242 |
301 |
243 \section{Stundenliste} |
302 \section{Stundenliste} |
244 \begin{footnotesize} |
303 \begin{footnotesize} |
245 \begin{longtable}[h]{l p{6.5cm} c c r} |
304 \begin{longtable}[h]{l p{6.5cm} c c r} |
246 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\ |
305 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\ |