1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 % Electronic Journal of Mathematics and Technology (eJMT) %
3 % style sheet for LaTeX. Please do not modify sections %
4 % or commands marked 'eJMT'. %
6 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10 \documentclass[12pt,a4paper]{article}% %
12 \usepackage{amsfonts,amsmath,amssymb} %
13 \usepackage[a4paper]{geometry} %
14 \usepackage{fancyhdr} %
16 \usepackage[pdftex]{hyperref} % see note below %
17 \usepackage{graphicx}% %
23 \newtheorem{theorem}{Theorem} %
24 \newtheorem{acknowledgement}[theorem]{Acknowledgement} %
25 \newtheorem{algorithm}[theorem]{Algorithm} %
26 \newtheorem{axiom}[theorem]{Axiom} %
27 \newtheorem{case}[theorem]{Case} %
28 \newtheorem{claim}[theorem]{Claim} %
29 \newtheorem{conclusion}[theorem]{Conclusion} %
30 \newtheorem{condition}[theorem]{Condition} %
31 \newtheorem{conjecture}[theorem]{Conjecture} %
32 \newtheorem{corollary}[theorem]{Corollary} %
33 \newtheorem{criterion}[theorem]{Criterion} %
34 \newtheorem{definition}[theorem]{Definition} %
35 \newtheorem{example}[theorem]{Example} %
36 \newtheorem{exercise}[theorem]{Exercise} %
37 \newtheorem{lemma}[theorem]{Lemma} %
38 \newtheorem{notation}[theorem]{Notation} %
39 \newtheorem{problem}[theorem]{Problem} %
40 \newtheorem{proposition}[theorem]{Proposition} %
41 \newtheorem{remark}[theorem]{Remark} %
42 \newtheorem{solution}[theorem]{Solution} %
43 \newtheorem{summary}[theorem]{Summary} %
44 \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } %
45 {\ \rule{0.5em}{0.5em}} %
47 % eJMT page dimensions %
49 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
51 % eJMT header & footer %
53 \newcounter{ejmtFirstpage} %
54 \setcounter{ejmtFirstpage}{1} %
56 \setlength{\headheight}{14pt} %
57 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
58 \pagestyle{fancyplain} %
60 \fancyhead[c]{\small The Electronic Journal of Mathematics%
61 \ and Technology, Volume 1, Number 1, ISSN 1933-2823} %
63 \ifnum\value{ejmtFirstpage}=0% %
64 {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% %
65 \else\setcounter{ejmtFirstpage}{0}\fi% %
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
70 % Please place your own definitions here
72 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
73 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
76 \definecolor{lgray}{RGB}{238,238,238}
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 % How to use hyperref %
82 % ------------------- %
84 % Probably the only way you will need to use the hyperref %
85 % package is as follows. To make some text, say %
86 % "My Text Link", into a link to the URL %
87 % http://something.somewhere.com/mystuff, use %
89 % \href{http://something.somewhere.com/mystuff}{My Text Link}
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
97 \title{Trials with TP-based Programming
99 for Interactive Course Material}%
101 % Single author. Please supply at least your name,
102 % email address, and affiliation here.
104 \author{\begin{tabular}{c}
105 \textit{Jan Ro\v{c}nik} \\
106 jan.rocnik@student.tugraz.at \\
108 Graz University of Technologie\\
112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
114 % eJMT commands - do not change these %
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
125 Traditional course material in engineering disciplines lacks an
126 important component, interactive support for step-wise problem
127 solving. Theorem-Proving (TP) technology is appropriate for one part
128 of such support, in checking user-input. For the other part of such
129 support, guiding the learner towards a solution, another kind of
130 technology is required. %TODO ... connect to prototype ...
132 A prototype combines TP with a programming language, the latter
133 interpreted in a specific way: certain statements in a program, called
134 tactics, are treated as breakpoints where control is handed over to
135 the user. An input formula is checked by TP (using logical context
136 built up by the interpreter); and if a learner gets stuck, a program
137 describing the steps towards a solution of a problem ``knows the next
138 step''. This kind of interpretation is called Lucas-Interpretation for
139 \emph{TP-based programming languages}.
141 This paper describes the prototype's TP-based programming language
142 within a case study creating interactive material for an advanced
143 course in Signal Processing: implementation of definitions and
144 theorems in TP, formal specification of a problem and step-wise
145 development of the program solving the problem. Experiences with the
146 ork flow in iterative development with testing and identifying errors
147 are described, too. The description clarifies the components missing
148 in the prototype's language as well as deficiencies experienced during
151 These experiences are particularly notable, because the author is the
152 first programmer using the language beyond the core team which
153 developed the prototype's TP-based language interpreter.
157 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
161 \thispagestyle{fancy} %
163 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
165 % Please use the following to indicate sections, subsections,
166 % etc. Please also use \subsubsection{...}, \paragraph{...}
167 % and \subparagraph{...} as necessary.
170 \section{Introduction}\label{intro}
172 % \paragraph{Didactics of mathematics}
173 %WN: wenn man in einem high-quality paper von 'didactics' spricht,
174 %WN muss man am state-of-the-art ankn"upfen -- siehe
175 %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
176 % faces a specific issue, a gap
177 % between (1) introduction of math concepts and skills and (2)
178 % application of these concepts and skills, which usually are separated
179 % into different units in curricula (for good reasons). For instance,
180 % (1) teaching partial fraction decomposition is separated from (2)
181 % application for inverse Z-transform in signal processing.
183 % \par This gap is an obstacle for applying math as an fundamental
184 % thinking technology in engineering: In (1) motivation is lacking
185 % because the question ``What is this stuff good for?'' cannot be
186 % treated sufficiently, and in (2) the ``stuff'' is not available to
187 % students in higher semesters as widespread experience shows.
189 % \paragraph{Motivation} taken by this didactic issue on the one hand,
190 % and ongoing research and development on a novel kind of educational
191 % mathematics assistant at Graz University of
192 % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
193 % scope with this issue on the other hand, several institutes are
194 % planning to join their expertise: the Institute for Information
195 % Systems and Computer Media (IICM), the Institute for Software
196 % Technology (IST), the Institutes for Mathematics, the Institute for
197 % Signal Processing and Speech Communication (SPSC), the Institute for
198 % Structural Analysis and the Institute of Electrical Measurement and
199 % Measurement Signal Processing.
200 %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
201 %WN und damit zu verg"anglich.
202 % \par This thesis is the first attempt to tackle the above mentioned
203 % issue, it focuses on Telematics, because these specific studies focus
204 % on mathematics in \emph{STEOP}, the introductory orientation phase in
205 % Austria. \emph{STEOP} is considered an opportunity to investigate the
206 % impact of {\sisac}'s prototype on the issue and others.
209 \paragraph{Traditional course material} in engineering disciplines lacks an
210 important component, interactive support for step-wise problem
211 solving. Theorem-Proving (TP) technology can provide such support by
212 specific services. An important part of such services is called
213 ``next-step-guidance'', generated by a specific kind of ``TP-based
214 programming language''. In the
215 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
216 a language is prototyped in line with~\cite{plmms10} and built upon
218 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
219 The TP services are coordinated by a specific interpreter for the
220 programming language, called
221 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
222 interpreter will be briefly re-introduced in order to make the paper
225 \subparagraph{The main part} of the paper is an account of first experiences
226 with programming in this TP-based language. The experience was gained
227 in a case study by the author. The author was considered an ideal
228 candidate for this study for the following reasons: as a student in
229 Telematics (computer science with focus on Signal Processing) he had
230 general knowledge in programming as well as specific domain knowledge
231 in Signal Processing; and he was not involved in the development of
232 {\sisac}'s programming language and interpeter, thus a novice to the
235 \subparagraph{The goal} of the case study was (1) some TP-based programs for
236 interactive course material for a specific ``Adavanced Signal
237 Processing Lab'' in a higher semester, (2) respective program
238 development with as little advice from the {\sisac}-team and (3) records
239 and comments for the main steps of development in an Isabelle theory;
240 this theory should provide guidelines for future programmers. An
241 excerpt from this theory is the main part of this paper.
243 The paper will use the problem in Fig.\ref{fig-interactive} as a
247 \includegraphics[width=140mm]{fig/isac-Ztrans-math}
248 \caption{Step-wise problem solving guided by the TP-based program}
249 \label{fig-interactive}
253 \paragraph{The problem is} from the domain of Signal Processing and requests to
254 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
255 also shows the beginning of the interactive construction of a solution
256 for the problem. This construction is done in the right window named
259 User-interaction on the Worksheet is {\em checked} and {\em guided} by
262 \item Formulas input by the user are {\em checked} by TP: such a
263 formula establishes a proof situation --- the prover has to derive the
264 formula from the logical context. The context is built up from the
265 formal specification of the problem (here hidden from the user) by the
267 \item If the user gets stuck, the program developed below in this
268 paper ``knows the next step'' from behind the scenes. How the latter
269 TP-service is exploited by dialogue authoring is out of scope of this
270 paper and can be studied in~\cite{gdaroczy-EP-13}.
271 \end{enumerate} It should be noted that the programmer using the
272 TP-based language is not concerned with interaction at all; we will
273 see that the program contains neither input-statements nor
274 output-statements. Rather, interaction is handled by services
275 generated automatically.
277 So there is a clear separation of concerns: Dialogues are
278 adapted by dialogue authors (in Java-based tools), using automatically
279 generated TP services, while the TP-based program is written by
280 mathematics experts (in Isabelle/ML). The latter is concern of this
283 \paragraph{The paper is structed} as follows: The introduction
284 \S\ref{intro} is followed by a brief re-introduction of the TP-based
285 programming language in \S\ref{PL}, which extends the executable
286 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
287 play a specific role in Lucas-Interpretation and in providing the TP
288 services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes
289 the main steps in developing the program for the running example:
290 prepare domain knowledge, implement the formal specification of the
291 problem, prepare the environment for the program, implement the
292 program. The workflow of programming, debugging and testing is
293 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
294 give directions identified for future development.
297 \section{\isac's Prototype for a Programming Language}\label{PL}
298 The prototype's language extends the executable fragment in the
299 language of the theorem prover
300 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}
301 by tactics which have a specific role in Lucas-Interpretation.
303 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
304 The executable fragment consists of data-type and function
305 definitions. It's usability even suggests that fragment for
306 introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
307 whose type system resembles that of functional programming
308 languages. Thus there are
310 \item[base types,] in particular \textit{bool}, the type of truth
311 values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
312 natural, integer and complex numbers respectively in mathematics.
313 \item[type constructors] allow to define arbitrary types, from
314 \textit{set}, \textit{list} to advanced data-structures like
315 \textit{trees}, red-black-trees etc.
316 \item[function types,] denoted by $\Rightarrow$.
317 \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
318 type polymorphism. Isabelle automatically computes the type of each
319 variable in a term by use of Hindley-Milner type inference
320 \cite{pl:hind97,Milner-78}.
323 \textbf{Terms} are formed as in functional programming by applying
324 functions to arguments. If $f$ is a function of type
325 $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
326 $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
327 has type $\tau$. There are many predefined infix symbols like $+$ and
328 $\leq$ most of which are overloaded for various types.
330 HOL also supports some basic constructs from functional programming:
331 {\it\label{isabelle-stmts}
332 \begin{tabbing} 123\=\kill
333 \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
334 \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
335 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
336 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
338 \noindent \textit{The running example's program uses some of these elements
339 (marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt
340 let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for
341 lists and {\tt o} for functional (forward) composition in line
342 $10$. In fact, the whole program is an Isabelle term with specific
343 function constants like {\sc program}, {\sc Substitute} and {\sc
344 Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.}
346 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
347 % x. \; x$ is the identity function.
349 %JR warum auskommentiert? WN2...
350 %WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
351 %WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
352 %WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
354 %WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
355 %WN2 Platz f"ur Anderes weg.
357 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
358 constants \textit{True} and \textit{False} and the usual logical
359 connectives (in decreasing order of precedence): $\neg, \land, \lor,
362 \textbf{Equality} is available in the form of the infix function $=$
363 of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
364 formulas, where it means ``if and only if''.
366 \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
367 P$. Quantifiers lead to non-executable functions, so functions do not
368 always correspond to programs, for instance, if comprising \\$(
369 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
372 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
373 The prototype extends Isabelle's language by specific statements
374 called tactics~\footnote{{\sisac}'s tactics are different from
375 Isabelle's tactics: the former concern steps in a calculation, the
376 latter concern proof steps.} and tacticals. For the programmer these
377 statements are functions with the following signatures:
380 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
381 term} * {\it term}\;{\it list}$:
382 this tactic appplies {\it theorem} to a {\it term} yielding a {\it
383 term} and a {\it term list}, the list are assumptions generated by
384 conditional rewriting. For instance, the {\it theorem}
385 $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
386 applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
387 $(\frac{2}{3}, [x\not=0])$.
389 \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
390 term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
391 this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
392 a confluent and terminating term rewrite system, in general. If
393 none of the rules ({\it theorem}s) is applicable on interpretation
394 of this tactic, an exception is thrown.
396 % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
397 % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
400 % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
401 % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
404 \item[Substitute:] ${\it substitution}\Rightarrow{\it
405 term}\Rightarrow{\it term}$:
407 \item[Take:] ${\it term}\Rightarrow{\it term}$:
408 this tactic has no effect in the program; but it creates a side-effect
409 by Lucas-Interpretation (see below) and writes {\it term} to the
412 \item[Subproblem:] ${\it theory} * {\it specification} * {\it
413 method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
414 this tactic allows to enter a phase of interactive specification
415 of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance,
416 a specific type of equation) and a method (for instance, solving an
417 equation symbolically or numerically).
420 The tactics play a specific role in
421 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
422 break-points and control is handed over to the user. The user is free
423 to investigate underlying knowledge, applicable theorems, etc. And
424 the user can proceed constructing a solution by input of a tactic to
425 be applied or by input of a formula; in the latter case the
426 Lucas-Interpreter has built up a logical context (initialised with the
427 precondition of the formal specification) such that Isabelle can
428 derive the formula from this context --- or give feedback, that no
429 derivation can be found.
431 \subsection{Tacticals for Control of Interpretation}
432 The flow of control in a program can be determined by {\tt if then else}
433 and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
434 by additional tacticals:
436 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
437 term}$: iterates over tactics which take a {\it term} as argument as
438 long as a tactic is applicable (for instance, {\it Rewrite\_Set} might
441 \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
442 if {\it tactic} is applicable, then it is applied to {\it term},
443 otherwise {\it term} is passed on unchanged.
445 \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
446 term}\Rightarrow{\it term}$:
449 \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
450 term}\Rightarrow{\it term}$:
452 \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
453 term}\Rightarrow{\it term}$:
457 no input / output --- Lucas-Interpretation
459 .\\.\\.\\TODO\\.\\.\\
461 \section{Development of a Program on Trial}\label{trial}
462 As mentioned above, {\sisac} is an experimental system for a proof of
463 concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
464 latter interprets a specific kind of TP-based programming language,
465 which is as experimental as the whole prototype --- so programming in
466 this language can be only ``on trial'', presently. However, as a
467 prototype, the language addresses essentials described below.
469 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
471 %WN was Fachleute unter obigem Titel interessiert findet sich
472 %WN unterhalb des auskommentierten Textes.
474 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
475 %WN auf Computer-Mathematiker fokussiert.
476 % \paragraph{As mentioned in the introduction,} a prototype of an
477 % educational math assistant called
478 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
479 % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
480 % the gap between (1) introducation and (2) application of mathematics:
481 % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
482 % requires each fact and each action justified by formal logic, so
483 % {{{\sisac}{}}} makes justifications transparent to students in
484 % interactive step-wise problem solving. By that way {{\sisac}} already
487 % \item Introduction of math stuff (in e.g. partial fraction
488 % decomposition) by stepwise explaining and exercising respective
489 % symbolic calculations with ``next step guidance (NSG)'' and rigorously
490 % checking steps freely input by students --- this also in context with
491 % advanced applications (where the stuff to be taught in higher
492 % semesters can be skimmed through by NSG), and
493 % \item Application of math stuff in advanced engineering courses
494 % (e.g. problems to be solved by inverse Z-transform in a Signal
495 % Processing Lab) and now without much ado about basic math techniques
496 % (like partial fraction decomposition): ``next step guidance'' supports
497 % students in independently (re-)adopting such techniques.
499 % Before the question is answers, how {{\sisac}}
500 % accomplishes this task from a technical point of view, some remarks on
501 % the state-of-the-art is given, therefor follow up Section~\ref{emas}.
503 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
505 % \paragraph{Educational software in mathematics} is, if at all, based
506 % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
507 % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
508 % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
509 % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
510 % base technologies are used to program math lessons and sometimes even
511 % exercises. The latter are cumbersome: the steps towards a solution of
512 % such an interactive exercise need to be provided with feedback, where
513 % at each step a wide variety of possible input has to be foreseen by
514 % the programmer - so such interactive exercises either require high
515 % development efforts or the exercises constrain possible inputs.
517 % \subparagraph{A new generation} of educational math assistants (EMAs)
518 % is emerging presently, which is based on Theorem Proving (TP). TP, for
519 % instance Isabelle and Coq, is a technology which requires each fact
520 % and each action justified by formal logic. Pushed by demands for
521 % \textit{proven} correctness of safety-critical software TP advances
522 % into software engineering; from these advancements computer
523 % mathematics benefits in general, and math education in particular. Two
524 % features of TP are immediately beneficial for learning:
526 % \paragraph{TP have knowledge in human readable format,} that is in
527 % standard predicate calculus. TP following the LCF-tradition have that
528 % knowledge down to the basic definitions of set, equality,
529 % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
530 % following the typical deductive development of math, natural numbers
531 % are defined and their properties
532 % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
533 % etc. Present knowledge mechanized in TP exceeds high-school
534 % mathematics by far, however by knowledge required in software
535 % technology, and not in other engineering sciences.
537 % \paragraph{TP can model the whole problem solving process} in
538 % mathematical problem solving {\em within} a coherent logical
539 % framework. This is already being done by three projects, by
540 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
542 % Having the whole problem solving process within a logical coherent
543 % system, such a design guarantees correctness of intermediate steps and
544 % of the result (which seems essential for math software); and the
545 % second advantage is that TP provides a wealth of theories which can be
546 % exploited for mechanizing other features essential for educational
549 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
551 % One essential feature for educational software is feedback to user
552 % input and assistance in coming to a solution.
554 % \paragraph{Checking user input} by ATP during stepwise problem solving
555 % is being accomplished by the three projects mentioned above
556 % exclusively. They model the whole problem solving process as mentioned
557 % above, so all what happens between formalized assumptions (or formal
558 % specification) and goal (or fulfilled postcondition) can be
559 % mechanized. Such mechanization promises to greatly extend the scope of
560 % educational software in stepwise problem solving.
562 % \paragraph{NSG (Next step guidance)} comprises the system's ability to
563 % propose a next step; this is a challenge for TP: either a radical
564 % restriction of the search space by restriction to very specific
565 % problem classes is required, or much care and effort is required in
566 % designing possible variants in the process of problem solving
567 % \cite{proof-strategies-11}.
569 % Another approach is restricted to problem solving in engineering
570 % domains, where a problem is specified by input, precondition, output
571 % and postcondition, and where the postcondition is proven by ATP behind
572 % the scenes: Here the possible variants in the process of problem
573 % solving are provided with feedback {\em automatically}, if the problem
574 % is described in a TP-based programing language: \cite{plmms10} the
575 % programmer only describes the math algorithm without caring about
576 % interaction (the respective program is functional and even has no
577 % input or output statements!); interaction is generated as a
578 % side-effect by the interpreter --- an efficient separation of concern
579 % between math programmers and dialog designers promising application
580 % all over engineering disciplines.
583 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
584 % Authoring new mathematics knowledge in {{\sisac}} can be compared with
585 % ``application programing'' of engineering problems; most of such
586 % programing uses CAS-based programing languages (CAS = Computer Algebra
587 % Systems; e.g. Mathematica's or Maple's programing language).
589 % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
590 % \cite{plmms10} for describing how to construct a solution to an
591 % engineering problem and for calling equation solvers, integration,
592 % etc~\footnote{Implementation of CAS-like functionality in TP is not
593 % primarily concerned with efficiency, but with a didactic question:
594 % What to decide for: for high-brow algorithms at the state-of-the-art
595 % or for elementary algorithms comprehensible for students?} within TP;
596 % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
597 % are impossible for CAS which have no logics underlying.
599 % \subparagraph{Authoring is perfect} by writing such TP based programs;
600 % the application programmer is not concerned with interaction or with
601 % user guidance: this is concern of a novel kind of program interpreter
602 % called Lucas-Interpreter. This interpreter hands over control to a
603 % dialog component at each step of calculation (like a debugger at
604 % breakpoints) and calls automated TP to check user input following
605 % personalized strategies according to a feedback module.
607 % However ``application programing with TP'' is not done with writing a
608 % program: according to the principles of TP, each step must be
609 % justified. Such justifications are given by theorems. So all steps
610 % must be related to some theorem, if there is no such theorem it must
611 % be added to the existing knowledge, which is organized in so-called
612 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
613 % Isabelle comprises a mechanism (called ``axiomatization''), which
614 % allows to omit proofs. Such a theorem is shown in
615 % Example~\ref{eg:neuper1}.
617 The running example, introduced by Fig.\ref{fig-interactive} on
618 p.\pageref{fig-interactive}, requires to determine the inverse $\cal
619 Z$-transform for a class of functions. The domain of Signal Processing
620 is accustomed to specific notation for the resulting functions, which
621 are absolutely summable and are called TODO: $u[n]$, where $u$ is the
622 function, $n$ is the argument and the brackets indicate that the
623 arguments are TODO. Surprisingly, Isabelle accepts the rules for
624 ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
625 experts might be particularly surprised, that the brackets do not
626 cause errors in typing (as lists).}:
630 {\small\begin{tabbing}
631 123\=123\=123\=123\=\kill
633 \>axiomatization where \\
634 \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
635 \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
636 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
638 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
640 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
642 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
648 These 6 rules can be used as conditional rewrite rules, depending on
649 the respective convergence radius. Satisfaction from accordance with traditional notation
650 contrasts with the above word {\em axiomatization}: As TP-based, the
651 programming language expects these rules as {\em proved} theorems, and
652 not as axioms implemented in the above brute force manner; otherwise
653 all the verification efforts envisaged (like proof of the
654 post-condition, see below) would be meaningless.
656 Isabelle provides a large body of knowledge, rigorously proven from
657 the basic axioms of mathematics~\footnote{This way of rigorously
658 deriving all knowledge from first principles is called the
659 LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
660 knowledge can be found in the theoris on Multivariate
661 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
662 building up knowledge such that a proof for the above rules would be
663 reasonably short and easily comprehensible, still requires lots of
664 work (and is definitely out of scope of our case study).
666 \paragraph{At the state-of-the-art in mechanization of knowledge} in
667 engineering sciences, the process does not stop with the mechanization of
668 mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
669 are expected to proceed to formal and explicit description of physical items. Signal Processing,
670 for instance is concerned with physical devices for signal acquisition
671 and reconstruction, which involve measuring a physical signal, storing
672 it, and possibly later rebuilding the original signal or an
673 approximation thereof. For digital systems, this typically includes
674 sampling and quantization; devices for signal compression, including
675 audio compression, image compression, and video compression, etc.
676 ``Domain engineering''\cite{db-domain-engineering} is concerned with
677 {\em specification} of these devices' components and features; this
678 part in the process of mechanization is only at the beginning in domains
679 like Signal Processing.
681 \subparagraph{TP-based programming, concern of this paper,} is determined to
682 add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
683 p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
684 starts with a formal {\em specification} of the problem to be solved.
687 \subsection{Specification of the Problem}\label{spec}
688 %WN <--> \chapter 7 der Thesis
689 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
691 The problem of the running example is textually described in
692 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
693 formal} specification of this problem, in traditional mathematical
694 notation, could look lik is this:
696 %WN Hier brauchen wir die Spezifikation des 'running example' ...
698 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
699 %JR der post condition - die existiert für uns ja eigentlich nicht aka
700 %JR haben sie bis jetzt nicht beachtet WN...
701 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
704 {\small\begin{tabbing}
705 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
708 \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
709 \>precond \>: filterExpression continius on $\mathbb{R}$ \\
710 \>output \>: stepResponse $x[n]$ \\
711 \>postcond \>:{\small $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\
712 \> \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land
713 (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\
717 And this is the implementation of the formal specification in the present
718 prototype, still bar-bones without support for authoring:
719 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
722 01 store_specification
723 02 (prepare_specification
725 04 "pbl_SP_Ztrans_inv"
727 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
728 07 [ ("#Given", ["filterExpression X_eq"]),
729 08 ("#Pre" , ["X_eq is_continuous"]),
730 19 ("#Find" , ["stepResponse n_eq"]),
731 10 ("#Post" , [" TODO "])],
732 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
734 13 [["SignalProcessing","Z_Transform","Inverse"]]));
736 Although the above details are partly very technical, we explain them
737 in order to document some intricacies of TP-based programming in the
738 present state of the {\sisac} prototype:
740 \item[01..02]\textit{store\_specification:} stores the result of the
741 function \textit{prep\_specification} in a global reference
742 \textit{Unsynchronized.ref}, which causes principal conflicts with
743 Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
744 parallel execution~\cite{Makarius-09:parall-proof} and is under
745 reconstruction already.
747 \textit{prep\_pbt:} translates the specification to an internal format
748 which allows efficient processing; see for instance line {\rm 07}
750 \item[03..04] are the ``mathematics author'' holding the copy-rights
751 and a unique identifier for the specification within {\sisac},
752 complare line {\rm 06}.
753 \item[05] is the Isabelle \textit{theory} required to parse the
754 specification in lines {\rm 07..10}.
755 \item[06] is a key into the tree of all specifications as presented to
756 the user (where some branches might be hidden by the dialog
758 \item[07..10] are the specification with input, pre-condition, output
759 and post-condition respectively; the post-condition is not handled in
760 the prototype presently.
761 \item[11] creates a term rewriting system (abbreviated \textit{rls} in
762 {\sisac}) which evaluates the pre-condition for the actual input data.
763 Only if the evaluation yields \textit{True}, a program con be started.
764 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
765 problem associated to a function from Computer Algebra (like an
766 equation solver) which is not the case here.
767 \item[13] is the specific key into the tree of programs addressing a
768 method which is able to find a solution which satiesfies the
769 post-condition of the specification.
773 %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
776 % {guh : guh, (*unique within this isac-knowledge*)
777 % mathauthors: string list, (*copyright*)
778 % init : pblID, (*to start refinement with*)
779 % thy : theory, (* which allows to compile that pbt
780 % TODO: search generalized for subthy (ref.p.69*)
781 % (*^^^ WN050912 NOT used during application of the problem,
782 % because applied terms may be from 'subthy' as well as from super;
783 % thus we take 'maxthy'; see match_ags !*)
784 % cas : term option,(*'CAS-command'*)
785 % prls : rls, (* for preds in where_*)
786 % where_: term list, (* where - predicates*)
788 % (*this is the model-pattern;
789 % it contains "#Given","#Where","#Find","#Relate"-patterns
790 % for constraints on identifiers see "fun cpy_nam"*)
791 % met : metID list}; (* methods solving the pbt*)
793 %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
794 %WN oben selbst geschrieben.
799 %WN das w"urde ich in \sec\label{progr} verschieben und
800 %WN das SubProblem partial fractions zum Erkl"aren verwenden.
801 % Such a specification is checked before the execution of a program is
802 % started, the same applies for sub-programs. In the following example
803 % (Example~\ref{eg:subprob}) shows the call of such a subproblem:
809 % {\ttfamily \begin{tabbing}
810 % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
811 % ``\>\>[linear,univariate,equation,test],'' \\
812 % ``\>\>[Test,solve\_linear])'' \\
813 % ``\>[BOOL equ, REAL z])'' \\
817 % \noindent If a program requires a result which has to be
818 % calculated first we can use a subproblem to do so. In our specific
819 % case we wanted to calculate the zeros of a fraction and used a
820 % subproblem to calculate the zeros of the denominator polynom.
825 \subsection{Implementation of the Method}\label{meth}
826 %WN <--> \chapter 7 der Thesis
828 \subsection{Preparation of Simplifiers for the Program}\label{simp}
830 \subsection{Preparation of ML-Functions}\label{funs}
831 %WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr}
834 \subsection{Implementation of the TP-based Program}\label{progr}
835 %WN <--> \chapter 8 der Thesis
838 {\small\it\begin{tabbing}
839 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill
840 \>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\
841 \>{\rm 02}\>\> {\tt LET} \\
842 \>{\rm 03}\>\>\> X = {\tt Take} X\_eq ; \\
843 \>{\rm 04}\>\>\> X' = {\tt Rewrite} ruleZY X ; \\
844 \>{\rm 05}\>\>\> (X'\_z::real) = lhs X' ; \\
845 \>{\rm 06}\>\>\> (zzz::real) = argument\_in X'\_z; \\
846 \>{\rm 07}\>\>\> (funterm::real) = rhs X’; \\
847 \>{\rm 07}\>\>\> (pbz::real) = {\tt SubProblem} \\
848 \>{\rm 08}\>\>\>\>\>\>\>\> ( \> Inverse\_Z\_Transform, \\
849 \>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction,rational,simplification]\\
850 \>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\
851 \>{\rm 10}\>\>\>\>\>\>\>\> [ funterm::real, zzz::real ]; \\
852 \>{\rm 12}\>\>\> (pbz\_eq::bool) = {\tt Take} (X'\_z = pbz) ; \\
854 \>{\rm 12}\>\>\> pbz\_eq = {\tt Rewrite} ruleYZ pbz\_eq ; \\
855 \>{\rm 13}\>\>\> pbz\_eq = drop\_questionmarks pbz\_eq ; \\
856 \>{\rm 14}\>\>\> (X\_zeq::bool) = {\tt Take} (X\_z = rhs pbz\_eq) ; \\
857 \>{\rm 15}\>\>\> n\_eq = {\tt Rewrite\_Set} inverse\_z X\_zeq ; \\
858 \>{\rm 15}\>\>\> n\_eq = drop\_questionmarks n\_eq \\
859 \>{\rm 16}\>\> {\tt IN } \\
860 \>{\rm 15}\>\>\> n\_eq
863 {\small\it\begin{tabbing}
864 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill\label{exp-calc}
865 \>{\rm 01}\> $\bullet$\> {\tt Problem } [maximum\_by, calculus] \`- - -\\
866 \>{\rm 02}\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$ \`- - -\\
867 \>{\rm 03}\>\> $\bullet$\> {\tt Problem } [make, diffable, function] \`- - -\\
868 \>{\rm 04}\>\> \dots\> $\widetilde{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$ \`- - -\\
871 \>{\rm 18}\>\> $\bullet$\> {\tt Problem} [find\_values, tool] \`- - -\\
872 % \`{\tt Apply\_Method} [tool, find\_values]\\
873 \>{\rm 19}\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] \`- - -\\
874 % \`{\tt Check\_Postcond}\\
875 \>{\rm 20}\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate !
883 "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
884 "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
885 " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
886 " (X'_z::real) = lhs X'; "^(* ?X' z*)
887 " (zzz::real) = argument_in X'_z; "^(* z *)
888 " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
890 " (pbz::real) = (SubProblem (Isac', "^(**)
891 " [partial_fraction,rational,simplification], "^
892 " [simplification,of_rationals,to_partial_fraction]) "^
893 " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
895 " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
896 " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
897 " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
898 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
899 " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
900 " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
901 "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
904 \section{Workflow of Programming in the Prototype}\label{workflow}
905 %WN ``workflow'' heisst: das mache ich zuerst, dann das ...
906 \subsection{Preparations and Trials}\label{flow-prep}
907 \subsubsection{Trials on Notation and Termination}
909 \paragraph{Technical notations} are a big problem for our piece of software,
910 but the reason for that isn't a fault of the software itself, one of the
911 troubles comes out of the fact that different technical subtopics use different
912 symbols and notations for a different purpose. The most famous example for such
913 a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
914 math). In the specific part of signal processing one of this notation issues is
915 the use of brackets --- we use round brackets for analoge signals and squared
916 brackets for digital samples. Also if there is no problem for us to handle this
917 fact, we have to tell the machine what notation leads to wich meaning and that
918 this purpose seperation is only valid for this special topic - signal
920 \subparagraph{In the programming language} itself it is not possible to declare
921 fractions, exponents, absolutes and other operators or remarks in a way to make
922 them pretty to read; our only posssiblilty were ASCII characters and a handfull
923 greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
925 With the upper collected knowledge it is possible to check if we were able to
926 donate all required terms and expressions.
928 \subsubsection{Definition and Usage of Rules}
930 \paragraph{The core} of our implemented problem is the Z-Transformation, due
931 the fact that the transformation itself would require higher math which isn't
932 yet avaible in our system we decided to choose the way like it is applied in
933 labratory and problem classes at our university - by applying transformation
934 rules (collected in transformation tables).
935 \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
936 use of axiomatizations like shown in Example~\ref{eg:ruledef}
943 rule1: ``1 = $\delta$[n]'' and
944 rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
945 rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
949 This rules can be collected in a ruleset and applied to a given expression as
950 follows in Example~\ref{eg:ruleapp}.
956 \item Store rules in ruleset:
958 val inverse_Z = append_rls "inverse_Z" e_rls
959 [ Thm ("rule1",num_str @{thm rule1}),
960 Thm ("rule2",num_str @{thm rule2}),
961 Thm ("rule3",num_str @{thm rule3})
963 \item Define exression:
965 val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
968 val SOME (sample_term', asm) =
969 rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
973 The use of rulesets makes it much easier to develop our designated applications,
974 but the programmer has to be careful and patient. When applying rulesets
975 two important issues have to be mentionend:
976 \subparagraph{How often} the rules have to be applied? In case of
977 transformations it is quite clear that we use them once but other fields
978 reuqire to apply rules until a special condition is reached (e.g.
979 a simplification is finished when there is nothing to be done left).
980 \subparagraph{The order} in which rules are applied often takes a big effect
981 and has to be evaluated for each purpose once again.
983 In our special case of Signal Processing and the rules defined in
984 Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
985 constants. After this step has been done it no mather which rule fit's next.
987 \subsubsection{Helping Functions}
988 %get denom, argument in
989 \subsubsection{Trials on equation solving}
990 %simple eq and problem with double fractions/negative exponents
993 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
994 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
996 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
997 TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
999 -------------------------------------------------------------------
1001 Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are
1002 vermutlich auf andere sections aufzuteilen.
1004 -------------------------------------------------------------------
1006 \subsection{Formalization of missing knowledge in Isabelle}
1008 \paragraph{A problem} behind is the mechanization of mathematic
1009 theories in TP-bases languages. There is still a huge gap between
1010 these algorithms and this what we want as a solution - in Example
1017 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1020 \noindent A very simple example on this what we call gap is the
1021 simplification above. It is needles to say that it is correct and also
1022 Isabelle for fills it correct - \emph{always}. But sometimes we don't
1023 want expand such terms, sometimes we want another structure of
1024 them. Think of a problem were we now would need only the coefficients
1025 of $X$ and $Y$. This is what we call the gap between mechanical
1026 simplification and the solution.
1031 \paragraph{We are not able to fill this gap,} until we have to live
1032 with it but first have a look on the meaning of this statement:
1033 Mechanized math starts from mathematical models and \emph{hopefully}
1034 proceeds to match physics. Academic engineering starts from physics
1035 (experimentation, measurement) and then proceeds to mathematical
1036 modeling and formalization. The process from a physical observance to
1037 a mathematical theory is unavoidable bound of setting up a big
1038 collection of standards, rules, definition but also exceptions. These
1039 are the things making mechanization that difficult.
1048 \noindent Think about some units like that one's above. Behind
1049 each unit there is a discerning and very accurate definition: One
1050 Meter is the distance the light travels, in a vacuum, through the time
1051 of 1 / 299.792.458 second; one kilogram is the weight of a
1052 platinum-iridium cylinder in paris; and so on. But are these
1053 definitions usable in a computer mechanized world?!
1058 \paragraph{A computer} or a TP-System builds on programs with
1059 predefined logical rules and does not know any mathematical trick
1060 (follow up example \ref{eg:trick}) or recipe to walk around difficult
1066 \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1067 \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1068 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1069 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1071 \noindent Sometimes it is also useful to be able to apply some
1072 \emph{tricks} to get a beautiful and particularly meaningful result,
1073 which we are able to interpret. But as seen in this example it can be
1074 hard to find out what operations have to be done to transform a result
1075 into a meaningful one.
1080 \paragraph{The only possibility,} for such a system, is to work
1081 through its known definitions and stops if none of these
1082 fits. Specified on Signal Processing or any other application it is
1083 often possible to walk through by doing simple creases. This creases
1084 are in general based on simple math operational but the challenge is
1085 to teach the machine \emph{all}\footnote{Its pride to call it
1086 \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1087 reach a high level of \emph{all} but it in real it will still be a
1088 survey of knowledge which links to other knowledge and {{\sisac}{}} a
1089 trainer and helper but no human compensating calculator.
1091 {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1092 specifications of problems out of topics from Signal Processing, etc.)
1093 and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1094 physical knowledge. The result is a three-dimensional universe of
1095 mathematics seen in Figure~\ref{fig:mathuni}.
1099 \includegraphics{fig/universe}
1100 \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1101 combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1102 leads to a three dimensional math universe.\label{fig:mathuni}}
1106 %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1107 %WN bitte folgende Bezeichnungen nehmen:
1109 %WN axis 1: Algorithmic Knowledge (Programs)
1110 %WN axis 2: Application-oriented Knowledge (Specifications)
1111 %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1113 %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1114 %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1115 %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1117 %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1118 %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1119 %JR gefordert werden WN2...
1120 %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1121 %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1122 %WN2 zusammenschneiden um die R"ander weg zu bekommen)
1123 %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1124 %WN2 png + pdf figures mitzuschicken.
1126 \subsection{Notes on Problems with Traditional Notation}
1128 \paragraph{During research} on these topic severely problems on
1129 traditional notations have been discovered. Some of them have been
1130 known in computer science for many years now and are still unsolved,
1131 one of them aggregates with the so called \emph{Lambda Calculus},
1132 Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1139 \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1142 \[ f(p)=\ldots\; p \in \quad R \]
1145 \noindent Above we see two equations. The first equation aims to
1146 be a mapping of an function from the reel range to the reel one, but
1147 when we change only one letter we get the second equation which
1148 usually aims to insert a reel point $p$ into the reel function. In
1149 computer science now we have the problem to tell the machine (TP) the
1150 difference between this two notations. This Problem is called
1151 \emph{Lambda Calculus}.
1156 \paragraph{An other problem} is that terms are not full simplified in
1157 traditional notations, in {{\sisac}} we have to simplify them complete
1158 to check weather results are compatible or not. in e.g. the solutions
1159 of an second order linear equation is an rational in {{\sisac}} but in
1160 tradition we keep fractions as long as possible and as long as they
1161 aim to be \textit{beautiful} (1/8, 5/16,...).
1162 \subparagraph{The math} which should be mechanized in Computer Theorem
1163 Provers (\emph{TP}) has (almost) a problem with traditional notations
1164 (predicate calculus) for axioms, definitions, lemmas, theorems as a
1165 computer program or script is not able to interpret every Greek or
1166 Latin letter and every Greek, Latin or whatever calculations
1167 symbol. Also if we would be able to handle these symbols we still have
1168 a problem to interpret them at all. (Follow up \hbox{Example
1175 u\left[n\right] \ \ldots \ unitstep
1178 \noindent The unitstep is something we need to solve Signal
1179 Processing problem classes. But in {{{\sisac}{}}} the rectangular
1180 brackets have a different meaning. So we abuse them for our
1181 requirements. We get something which is not defined, but usable. The
1182 Result is syntax only without semantic.
1187 In different problems, symbols and letters have different meanings and
1188 ask for different ways to get through. (Follow up \hbox{Example
1195 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1198 \noindent For using exponents the three \texttt{widehat} symbols
1199 are required. The reason for that is due the development of
1200 {{{\sisac}{}}} the single \texttt{widehat} and also the double were
1201 already in use for different operations.
1206 \paragraph{Also the output} can be a problem. We are familiar with a
1207 specified notations and style taught in university but a computer
1208 program has no knowledge of the form proved by a professor and the
1209 machines themselves also have not yet the possibilities to print every
1210 symbol (correct) Recent developments provide proofs in a human
1211 readable format but according to the fact that there is no money for
1212 good working formal editors yet, the style is one thing we have to
1215 \section{Problems rising out of the Development Environment}
1217 fehlermeldungen! TODO
1219 \section{Conclusion}\label{conclusion}
1223 \bibliographystyle{alpha}
1224 \bibliography{references}