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 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 \medskip 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 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 \medskip The paper will use the problem in Fig.\ref{fig-interactive} as a
247 \includegraphics[width=120mm]{fig/isac-Ztrans-math.png}
248 \caption{Step-wise problem solving guided by the TP-based program}
249 \label{fig-interactive}
252 The problem is from the domain of Signal Processing and requests to
253 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
254 also shows the beginning of the interactive construction of a solution
255 for the problem. This construction is done in the right window named
258 User-interaction on the Worksheet is {\em checked} and {\em guided} by
261 \item Formulas input by the user are {\em checked} by TP: such a
262 formula establishes a proof situation --- the prover has to derive the
263 formula from the logical context. The context is built up from the
264 formal specification of the problem (here hidden from the user) by the
266 \item If the user gets stuck, the program developed below in this
267 paper ``knows the next step'' from behind the scenes. How the latter
268 TP-service is exploited by dialogue authoring is out of scope of this
269 paper and can be studied in~\cite{gdaroczy-EP-13}.
270 \end{enumerate} It should be noted that the programmer using the
271 TP-based language is not concerned with interaction at all; we will
272 see that the program contains neither input-statements nor
273 output-statements. Rather, interaction is handled by services
274 generated automatically.
276 \medskip So there is a clear separation of concerns: Dialogues are
277 adapted by dialogue authors (in Java-based tools), using automatically
278 generated TP services, while the TP-based program is written by
279 mathematics experts (in Isabelle/ML). The latter is concern of this
282 \medskip The paper is structed as follows: The introduction
283 \S\ref{intro} is followed by a brief re-introduction of the TP-based
284 programming language in \S\ref{PL}, which extends the executable
285 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
286 play a specific role in Lucas-Interpretation and in providing the TP
287 services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes
288 the main steps in developing the program for the running example:
289 prepare domain knowledge, implement the formal specification of the
290 problem, prepare the environment for the program, implement the
291 program. The workflow of programming, debugging and testing is
292 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
293 give directions identified for future development.
296 \section{\isac's Prototype for a Programming Language}\label{PL}
297 The prototype's language extends the executable fragment in the
298 language of the theorem prover
299 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}
300 by tactics which have a specific role in Lucas-Interpretation.
302 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
303 The executable fragment consists of data-type and function
304 definitions. It's usability even suggests that fragment for
305 introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
306 whose type system resembles that of functional programming
307 languages. Thus there are
309 \item[base types,] in particular \textit{bool}, the type of truth
310 values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
311 natural, integer and complex numbers respectively in mathematics.
312 \item[type constructors] allow to define arbitrary types, from
313 \textit{set}, \textit{list} to advanced data-structures like
314 \textit{trees}, red-black-trees etc.
315 \item[function types,] denoted by $\Rightarrow$.
316 \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
317 type polymorphism. Isabelle automatically computes the type of each
318 variable in a term by use of Hindley-Milner type inference
319 \cite{pl:hind97,Milner-78}.
322 \textbf{Terms} are formed as in functional programming by applying
323 functions to arguments. If $f$ is a function of type
324 $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
325 $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
326 has type $\tau$. There are many predefined infix symbols like $+$ and
327 $\leq$ most of which are overloaded for various types.
329 HOL also supports some basic constructs from functional programming:
330 {\it\label{isabelle-stmts}
331 \begin{tabbing} 123\=\kill
332 \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
333 \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
334 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
335 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
337 \noindent \textit{The running example's program uses some of these elements
338 (marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt
339 let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for
340 lists and {\tt o} for functional (forward) composition in line
341 $10$. In fact, the whole program is an Isabelle term with specific
342 function constants like {\sc program}, {\sc Substitute} and {\sc
343 Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.}
345 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
346 % x. \; x$ is the identity function.
348 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
349 constants \textit{True} and \textit{False} and the usual logical
350 connectives (in decreasing order of precedence): $\neg, \land, \lor,
353 \textbf{Equality} is available in the form of the infix function $=$
354 of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
355 formulas, where it means ``if and only if''.
357 \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
358 P$. Quantifiers lead to non-executable functions, so functions do not
359 always correspond to programs, for instance, if comprising \\$(
360 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
363 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
364 The prototype extends Isabelle's language by specific statements
365 called tactics~\footnote{{\sisac}'s tactics are different from
366 Isabelle's tactics: the former concern steps in a calculation, the
367 latter concern proof steps.} and tacticals. For the programmer these
368 statements are functions with the following signatures:
371 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
372 term} * {\it term}\;{\it list}$:
373 this tactic appplies {\it theorem} to a {\it term} yielding a {\it
374 term} and a {\it term list}, the list are assumptions generated by
375 conditional rewriting. For instance, the {\it theorem}
376 $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
377 applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
378 $(\frac{2}{3}, [x\not=0])$.
380 \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
381 term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
382 this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
383 a confluent and terminating term rewrite system, in general. If
384 none of the rules ({\it theorem}s) is applicable on interpretation
385 of this tactic, an exception is thrown.
387 % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
388 % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
391 % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
392 % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
395 \item[Substitute:] ${\it substitution}\Rightarrow{\it
396 term}\Rightarrow{\it term}$:
398 \item[Take:] ${\it term}\Rightarrow{\it term}$:
399 this tactic has no effect in the program; but it creates a side-effect
400 by Lucas-Interpretation (see below) and writes {\it term} to the
403 \item[Subproblem:] ${\it theory} * {\it specification} * {\it
404 method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
405 this tactic allows to enter a phase of interactive specification
406 of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance,
407 a specific type of equation) and a method (for instance, solving an
408 equation symbolically or numerically).
411 The tactics play a specific role in
412 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
413 break-points and control is handed over to the user. The user is free
414 to investigate underlying knowledge, applicable theorems, etc. And
415 the user can proceed constructing a solution by input of a tactic to
416 be applied or by input of a formula; in the latter case the
417 Lucas-Interpreter has built up a logical context (initialised with the
418 precondition of the formal specification) such that Isabelle can
419 derive the formula from this context --- or give feedback, that no
420 derivation can be found.
422 \subsection{Tacticals for Control of Interpretation}
423 The flow of control in a program can be determined by {\tt if then else}
424 and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
425 by additional tacticals:
427 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
428 term}$: iterates over tactics which take a {\it term} as argument as
429 long as a tactic is applicable (for instance, {\it Rewrite\_Set} might
432 \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
433 if {\it tactic} is applicable, then it is applied to {\it term},
434 otherwise {\it term} is passed on unchanged.
436 \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
437 term}\Rightarrow{\it term}$:
440 \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
441 term}\Rightarrow{\it term}$:
443 \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
444 term}\Rightarrow{\it term}$:
448 no input / output --- Lucas-Interpretation
450 .\\.\\.\\TODO\\.\\.\\
452 \section{Development of a Program on Trial}\label{trial}
453 As mentioned above, {\sisac} is an experimental system for a proof of
454 concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
455 latter interprets a specific kind of TP-based programming language,
456 which is as experimental as the whole prototype --- so programming in
457 this language can be only ``on trial'', presently. However, as a
458 prototype, the language addresses essentials described below.
460 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
462 %WN was Fachleute unter obigem Titel interessiert findet
463 %WN unterhalb des auskommentierten Textes.
465 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
466 %WN auf Computer-Mathematiker fokussiert.
467 % \paragraph{As mentioned in the introduction,} a prototype of an
468 % educational math assistant called
469 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
470 % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
471 % the gap between (1) introducation and (2) application of mathematics:
472 % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
473 % requires each fact and each action justified by formal logic, so
474 % {{{\sisac}{}}} makes justifications transparent to students in
475 % interactive step-wise problem solving. By that way {{\sisac}} already
478 % \item Introduction of math stuff (in e.g. partial fraction
479 % decomposition) by stepwise explaining and exercising respective
480 % symbolic calculations with ``next step guidance (NSG)'' and rigorously
481 % checking steps freely input by students --- this also in context with
482 % advanced applications (where the stuff to be taught in higher
483 % semesters can be skimmed through by NSG), and
484 % \item Application of math stuff in advanced engineering courses
485 % (e.g. problems to be solved by inverse Z-transform in a Signal
486 % Processing Lab) and now without much ado about basic math techniques
487 % (like partial fraction decomposition): ``next step guidance'' supports
488 % students in independently (re-)adopting such techniques.
490 % Before the question is answers, how {{\sisac}}
491 % accomplishes this task from a technical point of view, some remarks on
492 % the state-of-the-art is given, therefor follow up Section~\ref{emas}.
494 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
496 % \paragraph{Educational software in mathematics} is, if at all, based
497 % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
498 % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
499 % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
500 % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
501 % base technologies are used to program math lessons and sometimes even
502 % exercises. The latter are cumbersome: the steps towards a solution of
503 % such an interactive exercise need to be provided with feedback, where
504 % at each step a wide variety of possible input has to be foreseen by
505 % the programmer - so such interactive exercises either require high
506 % development efforts or the exercises constrain possible inputs.
508 % \subparagraph{A new generation} of educational math assistants (EMAs)
509 % is emerging presently, which is based on Theorem Proving (TP). TP, for
510 % instance Isabelle and Coq, is a technology which requires each fact
511 % and each action justified by formal logic. Pushed by demands for
512 % \textit{proven} correctness of safety-critical software TP advances
513 % into software engineering; from these advancements computer
514 % mathematics benefits in general, and math education in particular. Two
515 % features of TP are immediately beneficial for learning:
517 % \paragraph{TP have knowledge in human readable format,} that is in
518 % standard predicate calculus. TP following the LCF-tradition have that
519 % knowledge down to the basic definitions of set, equality,
520 % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
521 % following the typical deductive development of math, natural numbers
522 % are defined and their properties
523 % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
524 % etc. Present knowledge mechanized in TP exceeds high-school
525 % mathematics by far, however by knowledge required in software
526 % technology, and not in other engineering sciences.
528 % \paragraph{TP can model the whole problem solving process} in
529 % mathematical problem solving {\em within} a coherent logical
530 % framework. This is already being done by three projects, by
531 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
533 % Having the whole problem solving process within a logical coherent
534 % system, such a design guarantees correctness of intermediate steps and
535 % of the result (which seems essential for math software); and the
536 % second advantage is that TP provides a wealth of theories which can be
537 % exploited for mechanizing other features essential for educational
540 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
542 % One essential feature for educational software is feedback to user
543 % input and assistance in coming to a solution.
545 % \paragraph{Checking user input} by ATP during stepwise problem solving
546 % is being accomplished by the three projects mentioned above
547 % exclusively. They model the whole problem solving process as mentioned
548 % above, so all what happens between formalized assumptions (or formal
549 % specification) and goal (or fulfilled postcondition) can be
550 % mechanized. Such mechanization promises to greatly extend the scope of
551 % educational software in stepwise problem solving.
553 % \paragraph{NSG (Next step guidance)} comprises the system's ability to
554 % propose a next step; this is a challenge for TP: either a radical
555 % restriction of the search space by restriction to very specific
556 % problem classes is required, or much care and effort is required in
557 % designing possible variants in the process of problem solving
558 % \cite{proof-strategies-11}.
560 % Another approach is restricted to problem solving in engineering
561 % domains, where a problem is specified by input, precondition, output
562 % and postcondition, and where the postcondition is proven by ATP behind
563 % the scenes: Here the possible variants in the process of problem
564 % solving are provided with feedback {\em automatically}, if the problem
565 % is described in a TP-based programing language: \cite{plmms10} the
566 % programmer only describes the math algorithm without caring about
567 % interaction (the respective program is functional and even has no
568 % input or output statements!); interaction is generated as a
569 % side-effect by the interpreter --- an efficient separation of concern
570 % between math programmers and dialog designers promising application
571 % all over engineering disciplines.
574 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
575 % Authoring new mathematics knowledge in {{\sisac}} can be compared with
576 % ``application programing'' of engineering problems; most of such
577 % programing uses CAS-based programing languages (CAS = Computer Algebra
578 % Systems; e.g. Mathematica's or Maple's programing language).
580 % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
581 % \cite{plmms10} for describing how to construct a solution to an
582 % engineering problem and for calling equation solvers, integration,
583 % etc~\footnote{Implementation of CAS-like functionality in TP is not
584 % primarily concerned with efficiency, but with a didactic question:
585 % What to decide for: for high-brow algorithms at the state-of-the-art
586 % or for elementary algorithms comprehensible for students?} within TP;
587 % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
588 % are impossible for CAS which have no logics underlying.
590 % \subparagraph{Authoring is perfect} by writing such TP based programs;
591 % the application programmer is not concerned with interaction or with
592 % user guidance: this is concern of a novel kind of program interpreter
593 % called Lucas-Interpreter. This interpreter hands over control to a
594 % dialog component at each step of calculation (like a debugger at
595 % breakpoints) and calls automated TP to check user input following
596 % personalized strategies according to a feedback module.
598 % However ``application programing with TP'' is not done with writing a
599 % program: according to the principles of TP, each step must be
600 % justified. Such justifications are given by theorems. So all steps
601 % must be related to some theorem, if there is no such theorem it must
602 % be added to the existing knowledge, which is organized in so-called
603 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
604 % Isabelle comprises a mechanism (called ``axiomatization''), which
605 % allows to omit proofs. Such a theorem is shown in
606 % Example~\ref{eg:neuper1}.
608 The running example, introduced by Fig.\ref{fig-interactive} on
609 p.\pageref{fig-interactive}, requires to determine the inverse $\cal
610 Z$-transform for a class of functions. The domain of Signal Processing
611 is accustomed to specific notation for the resulting functions, which
612 are absolutely summable and are called TODO: $u[n]$, where $u$ is the
613 function, $n$ is the argument and the brackets indicate that the
614 arguments are TODO. Surprisingly, Isabelle accepts the rules for
615 ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
616 experts might be particularly surprised, that the brackets do not
617 cause errors in typing (as lists).}:
621 {\small\begin{tabbing}
622 123\=123\=123\=123\=\kill
624 \>axiomatization where \\
625 \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
626 \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
627 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
629 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
631 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
633 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
639 These 6 rules can be used as conditional rewrite rules, depending on
640 the respective convergence radius. Satisfaction from notation
641 contrasts with the word {\em axiomatization}: As TP-based, the
642 programming language expects these rules as {\em proved} theorems, and
643 not as axioms implemented in the above brute force manner; otherwise
644 all the verification efforts envisaged (like proof of the
645 post-condition, see below) would be meaningless.
647 Isabelle provides a large body of knowledge, rigorously proven from
648 the basic axioms of mathematics~\footnote{This way of rigorously
649 deriving all knowledge from first principles is called the
650 LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
651 knowledge can be found in the theoris on Multivariate
652 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
653 building up knowledge such that a proof for the above rules would be
654 reasonably short and easily comprehensible, still requires lots of
655 work (and is definitely out of scope of our case study).
657 \medskip At the state-of-the-art in mechanization of knowledge in
658 engineering, the process does not stop with the mechanization of
659 mathematics. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
660 proceed to formal description of physical items. Signal Processing,
661 for instance is concerned with physical devices for signal acquisition
662 and reconstruction, which involve measuring a physical signal, storing
663 it, and possibly later rebuilding the original signal or an
664 approximation thereof. For digital systems, this typically includes
665 sampling and quantization; devices for signal compression, including
666 audio compression, image compression, and video compression, etc.
667 ``Domain engineering''\cite{db-domain-engineering} is concerned with
668 {\em specification} of these devices' components and features; this
669 part in the process of mechanization is only at the beginning.
671 \medskip TP-based programming, concern of this paper, adds a third
672 part of mechanisation, providing a third axis of ``algorithmic
673 knowledge'' in Fig.\ref{fig:mathuni} on p.\pageref{fig:mathuni}.
678 \includegraphics{fig/universe}
679 \caption{Didactic ``Math-Universe''\label{fig:mathuni}}
682 %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
683 %WN bitte folgende Bezeichnungen nehmen:
685 %WN axis 1: Algorithmic Knowledge (Programs)
686 %WN axis 2: Application-oriented Knowledge (Specifications)
687 %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
689 \subsection{Specification of the Problem}\label{spec}
690 %WN <--> \chapter 7 der Thesis
691 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
692 In order to provide TP with logical facts for checking user input, the
693 Lucas-Interpreter requires a \textbf{specification}. Such a
694 specification is shown in Example~\ref{eg:neuper2}.
696 -------------------------------------------------------------------
698 Hier brauchen wir die Spezifikation des 'running example' ...
703 {\small\begin{tabbing}
704 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
706 Specification no.1:\\
707 %\>input\>: $\{\;r={\it arbitraryFix}\;\}$ \\
708 \>input \>: $\{\;r\;\}$ \\
709 \>precond \>: $0 < r$ \\
710 \>output \>: $\{\;A,\; u,v\;\}$ \\
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$} \\
714 \>props\>: $\{\;A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\;\}$
720 ... und die Implementation in Isac (mit Kommentaren aus dem datatype)
722 %WN das w"urde ich in \sec\label{}
723 Such a specification is checked before the execution of a program is
724 started, the same applies for sub-programs. In the following example
725 (Example~\ref{eg:subprob}) shows the call of such a subproblem:
731 {\ttfamily \begin{tabbing}
732 ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
733 ``\>\>[linear,univariate,equation,test],'' \\
734 ``\>\>[Test,solve\_linear])'' \\
735 ``\>[BOOL equ, REAL z])'' \\
739 \noindent If a program requires a result which has to be
740 calculated first we can use a subproblem to do so. In our specific
741 case we wanted to calculate the zeros of a fraction and used a
742 subproblem to calculate the zeros of the denominator polynom.
747 \subsection{Implementation of the Method}\label{meth}
748 %WN <--> \chapter 7 der Thesis
750 \subsection{Preparation of ML-Functions for the Program}\label{funs}
751 %WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr}
754 \subsection{Implementation of the TP-based Program}\label{progr}
755 %WN <--> \chapter 8 der Thesis
758 \section{Workflow of Programming in the Prototype}\label{workflow}
759 -------------------------------------------------------------------
761 ``workflow'' heisst: das mache ich zuerst, dann das ...
763 \subsection{Preparations and Trials}\label{flow-prep}
764 TODO ... Build\_Inverse\_Z\_Transform.thy !!!
766 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
767 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
769 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
770 TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
772 -------------------------------------------------------------------
774 Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are
775 vermutlich auf andere sections aufzuteilen.
777 -------------------------------------------------------------------
779 \subsection{Formalization of missing knowledge in Isabelle}
781 \paragraph{A problem} behind is the mechanization of mathematic
782 theories in TP-bases languages. There is still a huge gap between
783 these algorithms and this what we want as a solution - in Example
790 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
793 \noindent A very simple example on this what we call gap is the
794 simplification above. It is needles to say that it is correct and also
795 Isabelle for fills it correct - \emph{always}. But sometimes we don't
796 want expand such terms, sometimes we want another structure of
797 them. Think of a problem were we now would need only the coefficients
798 of $X$ and $Y$. This is what we call the gap between mechanical
799 simplification and the solution.
804 \paragraph{We are not able to fill this gap,} until we have to live
805 with it but first have a look on the meaning of this statement:
806 Mechanized math starts from mathematical models and \emph{hopefully}
807 proceeds to match physics. Academic engineering starts from physics
808 (experimentation, measurement) and then proceeds to mathematical
809 modeling and formalization. The process from a physical observance to
810 a mathematical theory is unavoidable bound of setting up a big
811 collection of standards, rules, definition but also exceptions. These
812 are the things making mechanization that difficult.
821 \noindent Think about some units like that one's above. Behind
822 each unit there is a discerning and very accurate definition: One
823 Meter is the distance the light travels, in a vacuum, through the time
824 of 1 / 299.792.458 second; one kilogram is the weight of a
825 platinum-iridium cylinder in paris; and so on. But are these
826 definitions usable in a computer mechanized world?!
831 \paragraph{A computer} or a TP-System builds on programs with
832 predefined logical rules and does not know any mathematical trick
833 (follow up example \ref{eg:trick}) or recipe to walk around difficult
839 \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
840 \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
841 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
842 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
844 \noindent Sometimes it is also useful to be able to apply some
845 \emph{tricks} to get a beautiful and particularly meaningful result,
846 which we are able to interpret. But as seen in this example it can be
847 hard to find out what operations have to be done to transform a result
848 into a meaningful one.
853 \paragraph{The only possibility,} for such a system, is to work
854 through its known definitions and stops if none of these
855 fits. Specified on Signal Processing or any other application it is
856 often possible to walk through by doing simple creases. This creases
857 are in general based on simple math operational but the challenge is
858 to teach the machine \emph{all}\footnote{Its pride to call it
859 \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
860 reach a high level of \emph{all} but it in real it will still be a
861 survey of knowledge which links to other knowledge and {{\sisac}{}} a
862 trainer and helper but no human compensating calculator.
864 {{{\sisac}{}}} itself aims to adds an \emph{application} axis (formal
865 specifications of problems out of topics from Signal Processing, etc.)
866 and an \emph{algorithmic} axis to the \emph{deductive} axis of
867 physical knowledge. The result is a three-dimensional universe of
868 mathematics seen in Figure~\ref{fig:mathuni}.
873 \includegraphics{fig/universe}
874 \caption{Didactic ``Math-Universe''\label{fig:mathuni}}
878 \subsection{Notes on Problems with Traditional Notation}
880 \paragraph{During research} on these topic severely problems on
881 traditional notations have been discovered. Some of them have been
882 known in computer science for many years now and are still unsolved,
883 one of them aggregates with the so called \emph{Lambda Calculus},
884 Example~\ref{eg:lamda} provides a look on the problem that embarrassed
891 \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
894 \[ f(p)=\ldots\; p \in \quad R \]
897 \noindent Above we see two equations. The first equation aims to
898 be a mapping of an function from the reel range to the reel one, but
899 when we change only one letter we get the second equation which
900 usually aims to insert a reel point $p$ into the reel function. In
901 computer science now we have the problem to tell the machine (TP) the
902 difference between this two notations. This Problem is called
903 \emph{Lambda Calculus}.
908 \paragraph{An other problem} is that terms are not full simplified in
909 traditional notations, in {{\sisac}} we have to simplify them complete
910 to check weather results are compatible or not. in e.g. the solutions
911 of an second order linear equation is an rational in {{\sisac}} but in
912 tradition we keep fractions as long as possible and as long as they
913 aim to be \textit{beautiful} (1/8, 5/16,...).
914 \subparagraph{The math} which should be mechanized in Computer Theorem
915 Provers (\emph{TP}) has (almost) a problem with traditional notations
916 (predicate calculus) for axioms, definitions, lemmas, theorems as a
917 computer program or script is not able to interpret every Greek or
918 Latin letter and every Greek, Latin or whatever calculations
919 symbol. Also if we would be able to handle these symbols we still have
920 a problem to interpret them at all. (Follow up \hbox{Example
927 u\left[n\right] \ \ldots \ unitstep
930 \noindent The unitstep is something we need to solve Signal
931 Processing problem classes. But in {{{\sisac}{}}} the rectangular
932 brackets have a different meaning. So we abuse them for our
933 requirements. We get something which is not defined, but usable. The
934 Result is syntax only without semantic.
939 In different problems, symbols and letters have different meanings and
940 ask for different ways to get through. (Follow up \hbox{Example
947 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
950 \noindent For using exponents the three \texttt{widehat} symbols
951 are required. The reason for that is due the development of
952 {{{\sisac}{}}} the single \texttt{widehat} and also the double were
953 already in use for different operations.
958 \paragraph{Also the output} can be a problem. We are familiar with a
959 specified notations and style taught in university but a computer
960 program has no knowledge of the form proved by a professor and the
961 machines themselves also have not yet the possibilities to print every
962 symbol (correct) Recent developments provide proofs in a human
963 readable format but according to the fact that there is no money for
964 good working formal editors yet, the style is one thing we have to
967 \section{Problems rising out of the Development Environment}
969 fehlermeldungen! TODO
971 \section{Conclusion}\label{conclusion}
975 \bibliographystyle{alpha}
976 \bibliography{references}