51 |
43 |
52 %----------// BEGIN DOCUMENT \\----------% |
44 %----------// BEGIN DOCUMENT \\----------% |
53 |
45 |
54 \begin{document} |
46 \begin{document} |
55 |
47 |
56 %----------// TITLE PAGE \\----------% |
48 %----------// TITLE PAGE \\----------%1 |
57 |
49 |
58 \input{./bakkarbeit_titlepage.tex} |
50 \input{./bakkarbeit_titlepage.tex} |
59 \cleardoublepage |
51 \newpage |
60 |
52 |
61 %----------// EMPTY PAGE \\----------% |
53 %----------// EMPTY PAGE \\----------%2 |
62 |
|
63 %todo |
|
64 |
|
65 %----------// THANKS \\----------% |
|
66 |
54 |
67 \setcounter{page}{2} |
55 \setcounter{page}{2} |
|
56 \thispagestyle{empty}\mbox{}\newpage |
|
57 |
|
58 %----------// THANKS \\----------%3 |
|
59 |
|
60 \setcounter{page}{3} |
68 \begin{center} |
61 \begin{center} |
69 Special Thanks to\\ |
62 Special Thanks to\\ |
70 \hfill \\ |
63 \hfill \\ |
71 \emph{Dr.techn. Walther Neuper}\\ |
64 \emph{Dr.techn. Walther Neuper}\\ |
72 \emph{Dipl.-Ing. Bernhard Geiger} |
65 \emph{Dipl.-Ing. Bernhard Geiger} |
73 \end{center} |
66 \end{center} |
74 \thispagestyle{empty} |
67 \thispagestyle{empty} |
75 \cleardoublepage |
68 \newpage |
76 |
69 |
77 %----------// EMPTY PAGE \\----------% |
70 %----------// EMPTY PAGE \\----------%4 |
78 |
71 |
79 %todo |
72 \thispagestyle{empty}\mbox{}\newpage |
80 |
73 |
81 %----------// ABSTRACT \\----------% |
74 %----------// ABSTRACT \\----------%5 |
82 |
75 |
83 \begin{abstract} |
76 \begin{abstract} |
84 The Baccalaureate Thesis creates interactive course material for Signal Processing (SP) based on the experimental educational math assistant Isabelle/{\sisac} ({\em Isa}belle for Transparent {\em C}alculations in Applied Mathematics). |
77 The Baccalaureate Thesis creates interactive course material for Signal Processing (SP) based on the experimental educational math assistant Isabelle/{\sisac} ({\em Isa}belle for Transparent {\em C}alculations in Applied Mathematics). |
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. |
78 \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 much theory required for SPSC is not yet mechanized in Computer Theorem Provers (CTP); so this thesis will provide preliminary definitions and theorems (without proofs~!) implemented in Isabelle \emph{theories}. |
79 One challenge of this thesis is, that much theory required for SPSC is not yet mechanized in Computer Theorem Provers (CTP); so this thesis will provide preliminary definitions and theorems (without proofs~!) implemented in Isabelle \emph{theories}. |
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. |
80 \par Another challenge 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: |
81 So the practical outcome of this thesis is twofold: |
89 \begin{enumerate} |
82 \begin{enumerate} |
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 |
83 \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. |
84 \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. |
92 \end{enumerate} |
85 \end{enumerate} |
93 \end{abstract} |
86 \end{abstract} |
94 \clearpage |
87 \clearpage |
95 |
88 |
96 %----------// T O C \\----------% |
89 %----------// EMPTY PAGE \\----------%6 |
|
90 |
|
91 \thispagestyle{empty}\mbox{}\newpage |
|
92 |
|
93 %----------// T O C \\----------%7 |
97 |
94 |
98 \pagenumbering{Roman} |
95 \pagenumbering{Roman} |
99 %This thesis is structured into a fundamental part introducing the motivation, the basic notions concerning 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. |
96 %This thesis is structured into a fundamental part introducing the motivation, the basic notions concerning 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. |
100 \tableofcontents |
97 \tableofcontents |
101 \clearpage |
98 \clearpage |
102 \pagenumbering{arabic} |
99 \pagenumbering{arabic} |
103 \setcounter{page}{6} |
100 \setcounter{page}{8} |
104 |
101 |
105 %----------// PART-1 \\----------% |
102 %----------// PART-1 \\----------% |
106 |
103 |
107 \part{Project Fundamentals} |
104 \part{Project Fundamentals} |
108 |
105 |
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. |
|
110 |
|
111 \section{Introduction} |
106 \section{Introduction} |
|
107 %TODO personal decision no workds like feeling |
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. |
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. |
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. |
109 %\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... |
114 % |
110 % |
115 Didactics of mathematics faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which ususally are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing. |
111 Didactics of mathematics faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which ususally are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing. |
116 |
112 |
117 This gap is an obstacle for applying math as an foundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for~?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows. |
113 This gap is an obstacle for applying math as an foundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for~?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows. |
118 |
114 |
122 This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in STEOP, the introductory orientation phase. STEOP is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. |
118 This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in STEOP, the introductory orientation phase. STEOP is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. |
123 |
119 |
124 \medskip |
120 \medskip |
125 The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part. |
121 The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part. |
126 |
122 |
127 In part I, \S\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (\S\ref{emas}) and introduces the notions required for the implementation work (\S\ref{math-auth}). In particular, \S\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to \S\ref{sec:goals}. |
123 In part I, Section~\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (Section~\ref{emas}) and introduces the notions required for the implementation work (Section~\ref{math-auth}). In particular, Section~\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to Section~\ref{sec:goals}. |
128 |
124 |
129 \S\ref{sp} analyzes ten (TODO: exact no?) problems defined by the SPSC Lab for the knowledge already provided (\S\ref{know-isab}, \S\ref{know-isac}), discusses the selection of problems for implementation (\S\ref{know-missing}) TODO: further structure ? |
125 Section~\ref{sp} analyzes ten (TODO: exact no?) problems defined by the SPSC Lab for the knowledge already provided (Section~\ref{know-isab}, Section~\ref{know-isac}), discusses the selection of problems for implementation (Section~\ref{know-missing}) TODO: further structure ? |
130 %(\S\ref{}) |
126 %(\S\ref{}) |
131 |
127 |
132 \section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac} |
128 \section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac} |
133 %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. |
129 %no CTP!!! |
|
130 %A problem behind is the mechanization of mathematic theories in CTP-bases languages. There is still a huge gap between these algoritms and this what we want as a solution - in Example Signal Processing. |
134 %\begin{example} |
131 %\begin{example} |
135 % \[ |
132 % \[ |
136 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY |
133 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY |
137 % \] |
134 % \] |
138 % {\small\textit{ |
135 % {\small\textit{ |
139 % \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. |
136 % \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 expand such terms, sometimes we want another structure of them. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between mechanical simplification and the solution. |
140 % }} |
137 % }} |
141 % \caption{Correct but not usefull}\label{eg:gap} |
138 % \caption{Correct but not usefull}\label{eg:gap} |
142 %\end{example} |
139 %\end{example} |
143 %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: |
140 %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: |
144 %\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. |
141 %\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. |
286 specifications (``application axis'') and methods (``algorithmic axis'') |
283 specifications (``application axis'') and methods (``algorithmic axis'') |
287 |
284 |
288 partial fractions, cancellation of multivariate rational terms, ... |
285 partial fractions, cancellation of multivariate rational terms, ... |
289 |
286 |
290 \subsection{Survey: Requiered Knowledge and Selected Problem(s)}\label{know-missing} |
287 \subsection{Survey: Requiered Knowledge and Selected Problem(s)}\label{know-missing} |
291 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: |
288 Following tables (Table~\ref{tab:eff-four},~\ref{tab:eff-conv},~\ref{tab:eff-ztrans}) 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: |
292 |
289 |
293 \begin{table}[!H] |
290 \begin{table}[h] |
294 \begin{centering} |
291 \begin{centering} |
295 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
292 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
296 requirements & comments &effort\\ \hline\hline |
293 requirements & comments &effort\\ \hline\hline |
297 solving Intrgrals & simple via propertie table & 20\\ |
294 solving Intrgrals & simple via propertie table & 20\\ |
298 & \emph{real} & MT\\ \hline |
295 & \emph{real} & MT\\ \hline |