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}
81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
83 % How to use hyperref %
84 % ------------------- %
86 % Probably the only way you will need to use the hyperref %
87 % package is as follows. To make some text, say %
88 % "My Text Link", into a link to the URL %
89 % http://something.somewhere.com/mystuff, use %
91 % \href{http://something.somewhere.com/mystuff}{My Text Link}
93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
99 \title{Trials with TP-based Programming
101 for Interactive Course Material}%
103 % Single author. Please supply at least your name,
104 % email address, and affiliation here.
106 \author{\begin{tabular}{c}
107 \textit{Jan Ro\v{c}nik} \\
108 jan.rocnik@student.tugraz.at \\
110 Graz University of Technology\\
114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
116 % eJMT commands - do not change these %
121 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
127 Traditional course material in engineering disciplines lacks an
128 important component, interactive support for step-wise problem
129 solving. Theorem-Proving (TP) technology is appropriate for one part
130 of such support, in checking user-input. For the other part of such
131 support, guiding the learner towards a solution, another kind of
132 technology is required.
134 Both kinds of support can be achieved by so-called
135 Lucas-Interpretation which combines deduction and computation and, for
136 the latter, uses a novel kind of programming language. This language
137 is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
138 programming language''.
140 This paper is the experience report of the first ``application
141 programmer'' using this language for creating exercises in step-wise
142 problem solving for an advanced lab in Signal Processing. The tasks
143 involved in TP-based programming are described together with the
144 experience gained from a prototype of the programming language and of
147 The report concludes with a positive proof of concept, states
148 insufficiency usability of the prototype and captures the requirements
149 for further development of both, the programming language and the
154 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
158 \thispagestyle{fancy} %
160 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
162 % Please use the following to indicate sections, subsections,
163 % etc. Please also use \subsubsection{...}, \paragraph{...}
164 % and \subparagraph{...} as necessary.
167 \section{Introduction}\label{intro}
169 % \paragraph{Didactics of mathematics}
170 %WN: wenn man in einem high-quality paper von 'didactics' spricht,
171 %WN muss man am state-of-the-art ankn"upfen -- siehe
172 %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
173 % faces a specific issue, a gap
174 % between (1) introduction of math concepts and skills and (2)
175 % application of these concepts and skills, which usually are separated
176 % into different units in curricula (for good reasons). For instance,
177 % (1) teaching partial fraction decomposition is separated from (2)
178 % application for inverse Z-transform in signal processing.
180 % \par This gap is an obstacle for applying math as an fundamental
181 % thinking technology in engineering: In (1) motivation is lacking
182 % because the question ``What is this stuff good for?'' cannot be
183 % treated sufficiently, and in (2) the ``stuff'' is not available to
184 % students in higher semesters as widespread experience shows.
186 % \paragraph{Motivation} taken by this didactic issue on the one hand,
187 % and ongoing research and development on a novel kind of educational
188 % mathematics assistant at Graz University of
189 % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
190 % scope with this issue on the other hand, several institutes are
191 % planning to join their expertise: the Institute for Information
192 % Systems and Computer Media (IICM), the Institute for Software
193 % Technology (IST), the Institutes for Mathematics, the Institute for
194 % Signal Processing and Speech Communication (SPSC), the Institute for
195 % Structural Analysis and the Institute of Electrical Measurement and
196 % Measurement Signal Processing.
197 %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
198 %WN und damit zu verg"anglich.
199 % \par This thesis is the first attempt to tackle the above mentioned
200 % issue, it focuses on Telematics, because these specific studies focus
201 % on mathematics in \emph{STEOP}, the introductory orientation phase in
202 % Austria. \emph{STEOP} is considered an opportunity to investigate the
203 % impact of {\sisac}'s prototype on the issue and others.
206 Traditional course material in engineering disciplines lacks an
207 important component, interactive support for step-wise problem
208 solving. The lack becomes evident by comparing existing course
209 material with the sheets collected from written exams (in case solving
210 engineering problems is {\em not} deteriorated to multiple choice
211 tests) on the topics addressed by the materials.
212 Theorem-Proving (TP) technology can provide such support by
213 specific services. An important part of such services is called
214 ``next-step-guidance'', generated by a specific kind of ``TP-based
215 programming language''. In the
216 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
217 a language is prototyped in line with~\cite{plmms10} and built upon
218 the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}
219 \footnote{http://isabelle.in.tum.de/}.
220 The TP services are coordinated by a specific interpreter for the
221 programming language, called
222 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language
223 will be briefly re-introduced in order to make the paper
226 The main part of the paper is an account of first experiences
227 with programming in this TP-based language. The experience was gained
228 in a case study by the author. The author was considered an ideal
229 candidate for this study for the following reasons: as a student in
230 Telematics (computer science with focus on Signal Processing) he had
231 general knowledge in programming as well as specific domain knowledge
232 in Signal Processing; and he was {\em not} involved in the development of
233 {\sisac}'s programming language and interpreter, thus being a novice to the
236 The goals of the case study were: (1) to identify some TP-based programs for
237 interactive course material for a specific ``Advanced Signal
238 Processing Lab'' in a higher semester, (2) respective program
239 development with as little advice as possible from the {\sisac}-team and (3)
240 to document records and comments for the main steps of development in an
241 Isabelle theory; this theory should provide guidelines for future programmers.
242 An excerpt from this theory is the main part of this paper.
245 \medskip The major example resulting from the case study will be used
246 as running example throughout this paper. This example requires a
247 program resembling the size of real-world applications in engineering;
248 such a size was considered essential for the case study, since there
249 are many small programs for a long time (mainly concerned with
250 elementary Computer Algebra like simplification, equation solving,
251 calculus, etc.~\footnote{The programs existing in the {\sisac}
252 prototype are found at
253 http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})
255 \paragraph{The mathematical background of the running example} is the
256 following: In Signal Processing, ``the ${\cal Z}$-transform for
257 discrete-time signals is the counterpart of the Laplace transform for
258 continuous-time signals, and they each have a similar relationship to
259 the corresponding Fourier transform. One motivation for introducing
260 this generalization is that the Fourier transform does not converge
261 for all sequences, and it is useful to have a generalization of the
262 Fourier transform that encompasses a broader class of signals. A
263 second advantage is that in analytic problems, the ${\cal Z}$-transform
264 notation is often more convenient than the Fourier transform
265 notation.'' ~\cite[p. 128]{oppenheim2010discrete}. The ${\cal Z}$-transform
268 X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}
270 where a discrete time sequence $x[n]$ is transformed into the function
271 $X(z)$ where $z$ is a continuous complex variable. The inverse
272 function is addressed in the running example and can be determined by
275 x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz
277 where the letter $C$ represents a contour within the range of
278 convergence of the ${\cal Z}$-transform. The unit circle can be a special
279 case of this contour. Remember that $j$ is the complex number in the
280 domain of engineering. As this transform requires high effort to
281 be solved, tables of commonly used transform pairs are used in
282 education as well as in engineering practice; such tables can be found
283 at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.
284 A completely solved and more detailed example can be found at
285 ~\cite[p. 149f]{oppenheim2010discrete}.
287 Following conventions in engineering education and in practice, the
288 running example solves the problem by use of a table.
290 \paragraph{Support for interactive stepwise problem solving} in the
291 {\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,
292 the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:
293 A student inputs formulas line by line on the \textit{``Worksheet''},
294 and each step (i.e. each formula on completion) is immediately checked
295 by the system, such that at most {\em one inconsistent} formula can reside on
296 the Worksheet (on the input line, marked by the red $\otimes$).
299 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
300 %\includegraphics[width=140mm]{fig/isac-Ztrans-math}
301 \caption{Step-wise problem solving guided by the TP-based program
302 \label{fig-interactive}}
305 If the student gets stuck and does not know the formula to proceed
306 with, there is the button \framebox{NEXT} presenting the next formula
307 on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the
308 final result in case the student is not interested in intermediate
311 Adaptive dialogue guidance is already under
312 construction~\cite{gdaroczy-EP-13} and the two buttons will disappear,
313 since their presence is not wanted in many learning scenarios (in
314 particular, {\em not} in written exams).
316 The buttons \framebox{Theories}, \framebox{Problems} and
317 \framebox{Methods} are the entry points for interactive lookup of the
318 underlying knowledge. For instance, pushing \framebox{Theories} in
319 the configuration shown in Fig.\ref{fig-interactive}, pops up a
320 ``Theory browser'' displaying the theorem(s) justifying the current
321 step. The browser allows to lookup all other theories, thus
322 supporting indepentend investigation of underlying definitions,
323 theorems, proofs --- where the HTML representation of the browsers is
324 ready for arbitrary multimedia add-ons. Likewise, the browsers for
325 \framebox{Problems} and \framebox{Methods} support context sensitive
326 as well as interactive access to specifications and programs
329 There is also a simple web-based representation of knowledge items;
330 the items under consideration in this paper can be looked up as
332 ~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Inverse\_Z\_Transform.thy}}}
333 ~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Partial\_Fractions.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Partial\_Fractions.thy}}}
334 ~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Build\_Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Build\_Inverse\_Z\_Transform.thy}}}.
336 % can be explained by having a look at
337 % Fig.\ref{fig-interactive} which shows the beginning of the interactive
338 % construction of a solution for the problem. This construction is done in the
339 % right window named ``Worksheet''.
341 % User-interaction on the Worksheet is {\em checked} and {\em guided} by
344 % \item Formulas input by the user are {\em checked} by TP: such a
345 % formula establishes a proof situation --- the prover has to derive the
346 % formula from the logical context. The context is built up from the
347 % formal specification of the problem (here hidden from the user) by the
349 % \item If the user gets stuck, the program developed below in this
350 % paper ``knows the next step'' and Lucas-Interpretation provides services
351 % featuring so-called ``next-step-guidance''; this is out of scope of this
352 % paper and can be studied in~\cite{gdaroczy-EP-13}.
353 % \end{enumerate} It should be noted that the programmer using the
354 % TP-based language is not concerned with interaction at all; we will
355 % see that the program contains neither input-statements nor
356 % output-statements. Rather, interaction is handled by the interpreter
359 % So there is a clear separation of concerns: Dialogues are adapted by
360 % dialogue authors (in Java-based tools), using TP services provided by
361 % Lucas-Interpretation. The latter acts on programs developed by
362 % mathematics-authors (in Isabelle/ML); their task is concern of this
365 \bigskip The paper is structured as follows: The introduction
366 \S\ref{intro} is followed by a brief re-introduction of the TP-based
367 programming language in \S\ref{PL}, which extends the executable
368 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
369 play a specific role in Lucas-Interpretation and in providing the TP
370 services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
371 the main steps in developing the program for the running example:
372 prepare domain knowledge, implement the formal specification of the
373 problem, prepare the environment for the interpreter, implement the
374 program in \S\ref{isabisac} to \S\ref{progr} respectively.
375 The work-flow of programming, debugging and testing is
376 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
377 give directions identified for future development.
380 \section{\isac's Prototype for a Programming Language}\label{PL}
381 The prototype of the language and of the Lucas-Interpreter is briefly
382 described from the point of view of a programmer. The language extends
383 the executable fragment of Higher-Order Logic (HOL) in the theorem prover
384 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
386 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
387 The executable fragment consists of data-type and function
388 definitions. It's usability even suggests that fragment for
389 introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming
390 languages. Thus there are
392 \item[base types,] in particular \textit{bool}, the type of truth
393 values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
394 natural, integer and complex numbers respectively in mathematics.
395 \item[type constructors] allow to define arbitrary types, from
396 \textit{set}, \textit{list} to advanced data-structures like
397 \textit{trees}, red-black-trees etc.
398 \item[function types,] denoted by $\Rightarrow$.
399 \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
400 type polymorphism. Isabelle automatically computes the type of each
401 variable in a term by use of Hindley-Milner type inference
402 \cite{pl:hind97,Milner-78}.
405 \textbf{Terms} are formed as in functional programming by applying
406 functions to arguments. If $f$ is a function of type
407 $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
408 $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
409 has type $\tau$. There are many predefined infix symbols like $+$ and
410 $\leq$ most of which are overloaded for various types.
412 HOL also supports some basic constructs from functional programming:
413 {\footnotesize\it\label{isabelle-stmts}
414 \begin{tabbing} 123\=\kill
415 01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
416 02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
417 03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
418 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
420 \noindent The running example's program uses some of these elements
421 (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
422 let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
423 is an Isabelle term with specific function constants like {\tt
424 program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
425 Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
428 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
429 % x. \; x$ is the identity function.
431 %JR warum auskommentiert? WN2...
432 %WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
433 %WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
434 %WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
436 %WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
437 %WN2 Platz f"ur Anderes weg.
439 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
440 constants \textit{True} and \textit{False} and the usual logical
441 connectives (in decreasing order of precedence): $\neg, \land, \lor,
444 \textbf{Equality} is available in the form of the infix function $=$
445 of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
446 formulas, where it means ``if and only if''.
448 \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
449 P$. Quantifiers lead to non-executable functions, so functions do not
450 always correspond to programs, for instance, if comprising \\$(
451 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
454 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
455 The prototype extends Isabelle's language by specific statements
456 called tactics~\footnote{{\sisac}'s. These tactics are different from
457 Isabelle's tactics: the former concern steps in a calculation, the
458 latter concern proofs.}. For the programmer these
459 statements are functions with the following signatures:
462 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
463 term} * {\it term}\;{\it list}$:
464 this tactic applies {\it theorem} to a {\it term} yielding a {\it
465 term} and a {\it term list}, the list are assumptions generated by
466 conditional rewriting. For instance, the {\it theorem}
467 $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
468 applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
469 $(\frac{2}{3}, [x\not=0])$.
471 \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
472 term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
473 this tactic applies {\it ruleset} to a {\it term}; {\it ruleset} is
474 a confluent and terminating term rewrite system, in general. If
475 none of the rules ({\it theorem}s) is applicable on interpretation
476 of this tactic, an exception is thrown.
478 % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
479 % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
482 % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
483 % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
487 \item[Substitute:] ${\it substitution}\Rightarrow{\it
488 term}\Rightarrow{\it term}$: allows to access sub-terms.
491 \item[Take:] ${\it term}\Rightarrow{\it term}$:
492 this tactic has no effect in the program; but it creates a side-effect
493 by Lucas-Interpretation (see below) and writes {\it term} to the
496 \item[Subproblem:] ${\it theory} * {\it specification} * {\it
497 method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
498 this tactic is a generalisation of a function call: it takes an
499 \textit{argument list} as usual, and additionally a triple consisting
500 of an Isabelle \textit{theory}, an implicit \textit{specification} of the
501 program and a \textit{method} containing data for Lucas-Interpretation,
502 last not least a program (as an explicit specification)~\footnote{In
503 interactive tutoring these three items can be determined explicitly
506 The tactics play a specific role in
507 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
508 break-points where, as a side-effect, a line is added to a calculation
509 as a protocol for proceeding towards a solution in step-wise problem
510 solving. At the same points Lucas-Interpretation serves interactive
511 tutoring and hands over control to the user. The user is free to
512 investigate underlying knowledge, applicable theorems, etc. And the
513 user can proceed constructing a solution by input of a tactic to be
514 applied or by input of a formula; in the latter case the
515 Lucas-Interpreter has built up a logical context (initialised with the
516 precondition of the formal specification) such that Isabelle can
517 derive the formula from this context --- or give feedback, that no
518 derivation can be found.
520 \subsection{Tactics as Control Flow Statements}
521 The flow of control in a program can be determined by {\tt if then else}
522 and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
523 by additional tactics:
525 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
526 term}$: iterates over tactics which take a {\it term} as argument as
527 long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
530 \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
531 if {\it tactic} is applicable, then it is applied to {\it term},
532 otherwise {\it term} is passed on without changes.
534 \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
535 term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
536 it is applied to the first {\it term} yielding another {\it term},
537 otherwise the second {\it tactic} is applied; if none is applicable an
540 \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
541 term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
542 first {\it term} yielding an intermediate term (not appearing in the
543 signature) to which the second {\it tactic} is applied.
545 \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
546 term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
547 {\it tactic} is applied to the first {\it term} yielding an
548 intermediate term (not appearing in the signature); the intermediate
549 term is added to the environment the first {\it term} is evaluated in
550 etc. as long as the first {\it term} is true.
552 The tactics are not treated as break-points by Lucas-Interpretation
553 and thus do neither contribute to the calculation nor to interaction.
555 \section{Concepts and Tasks in TP-based Programming}\label{trial}
556 %\section{Development of a Program on Trial}
558 This section presents all the concepts involved in TP-based
559 programming and all the tasks to be accomplished by programmers. The
560 presentation uses the running example from
561 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
563 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
565 %WN was Fachleute unter obigem Titel interessiert findet sich
566 %WN unterhalb des auskommentierten Textes.
568 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
569 %WN auf Computer-Mathematiker fokussiert.
570 % \paragraph{As mentioned in the introduction,} a prototype of an
571 % educational math assistant called
572 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
573 % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
574 % the gap between (1) introducation and (2) application of mathematics:
575 % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
576 % requires each fact and each action justified by formal logic, so
577 % {{{\sisac}{}}} makes justifications transparent to students in
578 % interactive step-wise problem solving. By that way {{\sisac}} already
581 % \item Introduction of math stuff (in e.g. partial fraction
582 % decomposition) by stepwise explaining and exercising respective
583 % symbolic calculations with ``next step guidance (NSG)'' and rigorously
584 % checking steps freely input by students --- this also in context with
585 % advanced applications (where the stuff to be taught in higher
586 % semesters can be skimmed through by NSG), and
587 % \item Application of math stuff in advanced engineering courses
588 % (e.g. problems to be solved by inverse Z-transform in a Signal
589 % Processing Lab) and now without much ado about basic math techniques
590 % (like partial fraction decomposition): ``next step guidance'' supports
591 % students in independently (re-)adopting such techniques.
593 % Before the question is answers, how {{\sisac}}
594 % accomplishes this task from a technical point of view, some remarks on
595 % the state-of-the-art is given, therefor follow up Section~\ref{emas}.
597 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
599 % \paragraph{Educational software in mathematics} is, if at all, based
600 % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
601 % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
602 % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
603 % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
604 % base technologies are used to program math lessons and sometimes even
605 % exercises. The latter are cumbersome: the steps towards a solution of
606 % such an interactive exercise need to be provided with feedback, where
607 % at each step a wide variety of possible input has to be foreseen by
608 % the programmer - so such interactive exercises either require high
609 % development efforts or the exercises constrain possible inputs.
611 % \subparagraph{A new generation} of educational math assistants (EMAs)
612 % is emerging presently, which is based on Theorem Proving (TP). TP, for
613 % instance Isabelle and Coq, is a technology which requires each fact
614 % and each action justified by formal logic. Pushed by demands for
615 % \textit{proven} correctness of safety-critical software TP advances
616 % into software engineering; from these advancements computer
617 % mathematics benefits in general, and math education in particular. Two
618 % features of TP are immediately beneficial for learning:
620 % \paragraph{TP have knowledge in human readable format,} that is in
621 % standard predicate calculus. TP following the LCF-tradition have that
622 % knowledge down to the basic definitions of set, equality,
623 % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
624 % following the typical deductive development of math, natural numbers
625 % are defined and their properties
626 % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
627 % etc. Present knowledge mechanized in TP exceeds high-school
628 % mathematics by far, however by knowledge required in software
629 % technology, and not in other engineering sciences.
631 % \paragraph{TP can model the whole problem solving process} in
632 % mathematical problem solving {\em within} a coherent logical
633 % framework. This is already being done by three projects, by
634 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
636 % Having the whole problem solving process within a logical coherent
637 % system, such a design guarantees correctness of intermediate steps and
638 % of the result (which seems essential for math software); and the
639 % second advantage is that TP provides a wealth of theories which can be
640 % exploited for mechanizing other features essential for educational
643 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
645 % One essential feature for educational software is feedback to user
646 % input and assistance in coming to a solution.
648 % \paragraph{Checking user input} by ATP during stepwise problem solving
649 % is being accomplished by the three projects mentioned above
650 % exclusively. They model the whole problem solving process as mentioned
651 % above, so all what happens between formalized assumptions (or formal
652 % specification) and goal (or fulfilled postcondition) can be
653 % mechanized. Such mechanization promises to greatly extend the scope of
654 % educational software in stepwise problem solving.
656 % \paragraph{NSG (Next step guidance)} comprises the system's ability to
657 % propose a next step; this is a challenge for TP: either a radical
658 % restriction of the search space by restriction to very specific
659 % problem classes is required, or much care and effort is required in
660 % designing possible variants in the process of problem solving
661 % \cite{proof-strategies-11}.
663 % Another approach is restricted to problem solving in engineering
664 % domains, where a problem is specified by input, precondition, output
665 % and postcondition, and where the postcondition is proven by ATP behind
666 % the scenes: Here the possible variants in the process of problem
667 % solving are provided with feedback {\em automatically}, if the problem
668 % is described in a TP-based programing language: \cite{plmms10} the
669 % programmer only describes the math algorithm without caring about
670 % interaction (the respective program is functional and even has no
671 % input or output statements!); interaction is generated as a
672 % side-effect by the interpreter --- an efficient separation of concern
673 % between math programmers and dialog designers promising application
674 % all over engineering disciplines.
677 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
678 % Authoring new mathematics knowledge in {{\sisac}} can be compared with
679 % ``application programing'' of engineering problems; most of such
680 % programing uses CAS-based programing languages (CAS = Computer Algebra
681 % Systems; e.g. Mathematica's or Maple's programing language).
683 % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
684 % \cite{plmms10} for describing how to construct a solution to an
685 % engineering problem and for calling equation solvers, integration,
686 % etc~\footnote{Implementation of CAS-like functionality in TP is not
687 % primarily concerned with efficiency, but with a didactic question:
688 % What to decide for: for high-brow algorithms at the state-of-the-art
689 % or for elementary algorithms comprehensible for students?} within TP;
690 % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
691 % are impossible for CAS which have no logics underlying.
693 % \subparagraph{Authoring is perfect} by writing such TP based programs;
694 % the application programmer is not concerned with interaction or with
695 % user guidance: this is concern of a novel kind of program interpreter
696 % called Lucas-Interpreter. This interpreter hands over control to a
697 % dialog component at each step of calculation (like a debugger at
698 % breakpoints) and calls automated TP to check user input following
699 % personalized strategies according to a feedback module.
701 % However ``application programing with TP'' is not done with writing a
702 % program: according to the principles of TP, each step must be
703 % justified. Such justifications are given by theorems. So all steps
704 % must be related to some theorem, if there is no such theorem it must
705 % be added to the existing knowledge, which is organized in so-called
706 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
707 % Isabelle comprises a mechanism (called ``axiomatization''), which
708 % allows to omit proofs. Such a theorem is shown in
709 % Example~\ref{eg:neuper1}.
711 The running example requires to determine the inverse ${\cal Z}$-transform
712 for a class of functions. The domain of Signal Processing
713 is accustomed to specific notation for the resulting functions, which
714 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
715 function, $n$ is the argument and the brackets indicate that the
716 arguments are discrete. Surprisingly, Isabelle accepts the rules for
717 $z^{-1}$ in this traditional notation~\footnote{Isabelle
718 experts might be particularly surprised, that the brackets do not
719 cause errors in typing (as lists).}:
723 {\footnotesize\begin{tabbing}
724 123\=123\=123\=123\=\kill
726 01\>axiomatization where \\
727 02\>\> rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\
728 03\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\
729 04\>\> rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\
730 05\>\> rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\
731 06\>\> rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\
732 07\>\> rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''
736 These 6 rules can be used as conditional rewrite rules, depending on
737 the respective convergence radius. Satisfaction from accordance with traditional
738 notation contrasts with the above word {\em axiomatization}: As TP-based, the
739 programming language expects these rules as {\em proved} theorems, and
740 not as axioms implemented in the above brute force manner; otherwise
741 all the verification efforts envisaged (like proof of the
742 post-condition, see below) would be meaningless.
744 Isabelle provides a large body of knowledge, rigorously proved from
745 the basic axioms of mathematics~\footnote{This way of rigorously
746 deriving all knowledge from first principles is called the
747 LCF-paradigm in TP.}. In the case of the ${\cal Z}$-transform the most advanced
748 knowledge can be found in the theories on Multivariate
749 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
750 building up knowledge such that a proof for the above rules would be
751 reasonably short and easily comprehensible, still requires lots of
752 work (and is definitely out of scope of our case study).
754 %REMOVED DUE TO SPACE CONSTRAINTS
755 %At the state-of-the-art in mechanization of knowledge in engineering
756 %sciences, the process does not stop with the mechanization of
757 %mathematics traditionally used in these sciences. Rather, ``Formal
758 %Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
759 %description of physical items. Signal Processing, for instance is
760 %concerned with physical devices for signal acquisition and
761 %reconstruction, which involve measuring a physical signal, storing it,
762 %and possibly later rebuilding the original signal or an approximation
763 %thereof. For digital systems, this typically includes sampling and
764 %quantization; devices for signal compression, including audio
765 %compression, image compression, and video compression, etc. ``Domain
766 %engineering''\cite{db:dom-eng} is concerned with {\em specification}
767 %of these devices' components and features; this part in the process of
768 %mechanization is only at the beginning in domains like Signal
771 %TP-based programming, concern of this paper, is determined to
772 %add ``algorithmic knowledge'' to the mechanised body of knowledge.
773 %% in Fig.\ref{fig:mathuni} on
774 %% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
775 %% starts with a formal {\em specification} of the problem to be solved.
778 %% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
779 %% \caption{The three-dimensional universe of mathematics knowledge}
780 %% \label{fig:mathuni}
783 %% The language for both axes is defined in the axis at the bottom, deductive
784 %% knowledge, in {\sisac} represented by Isabelle's theories.
786 \subsection{Preparation of Simplifiers for the Program}\label{simp}
788 All evaluation in the prototype's Lucas-Interpreter is done by term rewriting on
789 Isabelle's terms, see \S\ref{meth} below; in this section some of respective
790 preparations are described. In order to work reliably with term rewriting, the
791 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
792 then they are called (canonical) simplifiers. These properties do not go without
793 saying, their establishment is a difficult task for the programmer; this task is
794 not yet supported in the prototype.
796 The prototype rewrites using theorems only. Axioms which are theorems as well
797 have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
798 assemble them in a rule-set and apply them in ML as follows:
802 01 val inverse_z = Rls
803 02 {id = "inverse_z",
804 03 rew_ord = dummy_ord,
806 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
807 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
808 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
813 \noindent The items, line by line, in the above record have the following purpose:
815 \item[01..02] the ML-value \textit{inverse\_z} stores it's identifier
816 as a string for ``reflection'' when switching between the language
817 layers of Isabelle/ML (like in the Lucas-Interpreter) and
818 Isabelle/Isar (like in the example program on p.\pageref{s:impl} on
821 \item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
822 \textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
823 (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
824 and (b) the assumptions of the \textit{rules} need not be evaluated
825 (they just go into the context during rewriting).
827 \item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
828 also ML-functions (\S\ref{funs}) can come into this list as shown in
829 \S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm}
830 and \textit{Calc} respectively; for the purpose of reflection both
831 contain their identifiers.
833 \item[08..09] are error-patterns not discussed here and \textit{scr}
834 is prepared to get a program, automatically generated by {\sisac} for
835 producing intermediate rewrites when requested by the user.
839 %OUTCOMMENTED DUE TO SPACE RESTRICTIONS
840 % \noindent It is advisable to immediately test rule-sets; for that
841 % purpose an appropriate term has to be created; \textit{parse} takes a
842 % context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
843 % Z}^{-1}$) and creates a term:
848 % 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
850 % 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1",
851 % 05 "RealDef.real => RealDef.real => RealDef.real") $
852 % 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...)
855 % \noindent The internal representation of the term, as required for
856 % rewriting, consists of \textit{Const}ants, a pair of a string
857 % \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
858 % \textit{Free} and the respective constructor \textit{\$}. Now the
859 % term can be rewritten by the rule-set \textit{inverse\_z}:
864 % 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
868 % 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
869 % 07 val it = "|| z || > 1 & || z || > </alpha>" : string
872 % \noindent The resulting term \textit{t} and the assumptions
873 % \textit{asm} are converted to readable strings by \textit{term2str}
874 % and \textit{terms2str}.
876 \subsection{Preparation of ML-Functions}\label{funs}
877 Some functionality required in programming, cannot be accomplished by
878 rewriting. So the prototype has a mechanism to call functions within
879 the rewrite-engine: certain redexes in Isabelle terms call these
880 functions written in SML~\cite{pl:milner97}, the implementation {\em
881 and} meta-language of Isabelle. The programmer has to use this
884 In the running example's program on p.\pageref{s:impl} the lines {\rm
885 05} and {\rm 06} contain such functions; we go into the details with
886 \textit{argument\_in X\_z;}. This function fetches the argument from a
887 function application: Line {\rm 03} in the example calculation on
888 p.\pageref{exp-calc} is created by line {\rm 06} of the example
889 program on p.\pageref{s:impl} where the program's environment assigns
890 the value \textit{X z} to the variable \textit{X\_z}; so the function
891 shall extract the argument \textit{z}.
893 \medskip In order to be recognised as a function constant in the
894 program source the constant needs to be declared in a theory, here in
895 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
896 the context \textit{ctxt} of that theory:
901 02 argument'_in :: "real => real" ("argument'_in _" 10)
904 %^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
905 %^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
906 %^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
907 %^3.2^ \end{verbatim}}
909 %^3.2^ \noindent Parsing produces a term \texttt{t} in internal
910 %^3.2^ representation~\footnote{The attentive reader realizes the
911 %^3.2^ differences between interal and extermal representation even in the
912 %^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
913 %^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
914 %^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
916 The function body below is implemented directly in SML,
917 i.e in an \texttt{ML \{* *\}} block; the function definition provides
918 a unique prefix \texttt{eval\_} to the function name:
923 02 fun eval_argument_in _
924 03 "Build_Inverse_Z_Transform.argument'_in"
925 04 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
926 05 if is_Free arg (*could be something to be simplified before*)
927 06 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
929 08 | eval_argument_in _ _ _ _ = NONE;
933 \noindent The function body creates either \texttt{NONE}
934 telling the rewrite-engine to search for the next redex, or creates an
935 ad-hoc theorem for rewriting, thus the programmer needs to adopt many
936 technicalities of Isabelle, for instance, the \textit{Trueprop}
939 \bigskip This sub-task particularly sheds light on basic issues in the
940 design of a programming language, the integration of differential language
941 layers, the layer of Isabelle/Isar and Isabelle/ML.
943 Another point of improvement for the prototype is the rewrite-engine: The
944 program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
947 {\small\it\label{s:impl}
949 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
950 \>{\rm 05/06}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
953 \noindent because nested function calls would require creating redexes
954 inside-out; however, the prototype's rewrite-engine only works top down
955 from the root of a term down to the leaves.
957 How all these technicalities are to be checked in the prototype is
958 shown in \S\ref{flow-prep} below.
960 % \paragraph{Explicit Problems} require explicit methods to solve them, and within
961 % this methods we have some explicit steps to do. This steps can be unique for
962 % a special problem or refindable in other problems. No mather what case, such
963 % steps often require some technical functions behind. For the solving process
964 % of the Inverse Z Transformation and the corresponding partial fraction it was
965 % neccessary to build helping functions like \texttt{get\_denominator},
966 % \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
967 % to filter the denominator or numerator out of a fraction, last one helps us to
968 % get to know the bound variable in a equation.
970 % By taking \texttt{get\_denominator} as an example, we want to explain how to
971 % implement new functions into the existing system and how we can later use them
974 % \subsubsection{Find a place to Store the Function}
976 % The whole system builds up on a well defined structure of Knowledge. This
977 % Knowledge sets up at the Path:
978 % \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
979 % For implementing the Function \texttt{get\_denominator} (which let us extract
980 % the denominator out of a fraction) we have choosen the Theory (file)
981 % \texttt{Rational.thy}.
983 % \subsubsection{Write down the new Function}
985 % In upper Theory we now define the new function and its purpose:
987 % get_denominator :: "real => real"
989 % This command tells the machine that a function with the name
990 % \texttt{get\_denominator} exists which gets a real expression as argument and
991 % returns once again a real expression. Now we are able to implement the function
992 % itself, upcoming example now shows the implementation of
993 % \texttt{get\_denominator}.
996 % \label{eg:getdenom}
1000 % 02 *("get_denominator",
1001 % 03 * ("Rational.get_denominator", eval_get_denominator ""))
1003 % 05 fun eval_get_denominator (thmid:string) _
1004 % 06 (t as Const ("Rational.get_denominator", _) $
1005 % 07 (Const ("Rings.inverse_class.divide", _) $num
1007 % 09 SOME (mk_thmid thmid ""
1008 % 10 (Print_Mode.setmp []
1009 % 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1010 % 12 Trueprop $ (mk_equality (t, denom)))
1011 % 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
1014 % Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
1015 % there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
1017 % into its two parts (\texttt{\$num \$denom}). The lines before are additionals
1018 % commands for declaring the function and the lines after are modeling and
1019 % returning a real variable out of \texttt{\$denom}.
1021 % \subsubsection{Add a test for the new Function}
1023 % \paragraph{Everytime when adding} a new function it is essential also to add
1024 % a test for it. Tests for all functions are sorted in the same structure as the
1025 % knowledge it self and can be found up from the path:
1026 % \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
1027 % This tests are nothing very special, as a first prototype the functionallity
1028 % of a function can be checked by evaluating the result of a simple expression
1029 % passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
1030 % \textit{just} created function \texttt{get\_denominator}.
1033 % \label{eg:getdenomtest}
1036 % 01 val thy = @{theory Isac};
1037 % 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1038 % 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1039 % 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1040 % 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
1043 % \begin{description}
1044 % \item[01] checks if the proofer set up on our {\sisac{}} System.
1045 % \item[02] passes a simple expression (fraction) to our suddenly created
1047 % \item[04] checks if the resulting variable is the correct one (in this case
1048 % ``b'' the denominator) and returns.
1049 % \item[05] handels the error case and reports that the function is not able to
1050 % solve the given problem.
1053 \subsection{Specification of the Problem}\label{spec}
1054 %WN <--> \chapter 7 der Thesis
1055 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1057 Mechanical treatment requires to translate a textual problem
1058 description like in Fig.\ref{fig-interactive} on
1059 p.\pageref{fig-interactive} into a {\em formal} specification. The
1060 formal specification of the running example could look like is this
1061 ~\footnote{The ``TODO'' in the postcondition indicates, that postconditions
1062 are not yet handled in the prototype; in particular, the postcondition, i.e.
1063 the correctness of the result is not yet automatically proved.}:
1065 %WN Hier brauchen wir die Spezifikation des 'running example' ...
1066 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1067 %JR der post condition - die existiert für uns ja eigentlich nicht aka
1068 %JR haben sie bis jetzt nicht beachtet WN...
1069 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1073 {\small\begin{tabbing}
1074 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1077 \> \>input \>: ${\it filterExpression} \;\;X\;z=\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}, \;{\it domain}\;\mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$\\
1078 \>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
1079 \>\>output \>: stepResponse $x[n]$ \\
1080 \>\>postcond \>: TODO
1083 %JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt"
1086 % Defining the postcondition requires a high amount mathematical
1087 % knowledge, the difficult part in our case is not to set up this condition
1088 % nor it is more to define it in a way the interpreter is able to handle it.
1089 % Due the fact that implementing that mechanisms is quite the same amount as
1090 % creating the programm itself, it is not avaible in our prototype.
1091 % \label{rm:postcond}
1094 The implementation of the formal specification in the present
1095 prototype, still bar-bones without support for authoring, is done
1097 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1099 {\footnotesize\label{exp-spec}
1102 01 store_specification
1103 02 (prepare_specification
1104 03 "pbl_SP_Ztrans_inv"
1107 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1108 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1109 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1110 09 ("#Find" , ["stepResponse n_eq"]),
1111 10 ("#Post" , [" TODO "])])
1114 13 [["SignalProcessing","Z_Transform","Inverse"]]);
1118 Although the above details are partly very technical, we explain them
1119 in order to document some intricacies of TP-based programming in the
1120 present state of the {\sisac} prototype:
1122 \item[01..02]\textit{store\_specification:} stores the result of the
1123 function \textit{prep\_specification} in a global reference
1124 \textit{Unsynchronized.ref}, which causes principal conflicts with
1125 Isabelle's asynchronous document model~\cite{Wenzel-11:doc-orient} and
1126 parallel execution~\cite{Makarius-09:parall-proof} and is under
1127 reconstruction already.
1129 \textit{prep\_specification:} translates the specification to an internal format
1130 which allows efficient processing; see for instance line {\rm 07}
1132 \item[03..04] are a unique identifier for the specification within {\sisac}
1133 and the ``mathematics author'' holding the copy-rights.
1134 \item[05] is the Isabelle \textit{theory} required to parse the
1135 specification in lines {\rm 07..10}.
1136 \item[06] is a key into the tree of all specifications as presented to
1137 the user (where some branches might be hidden by the dialogue
1139 \item[07..10] are the specification with input, pre-condition, output
1140 and post-condition respectively; note that the specification contains
1141 variables to be instantiated with concrete values for a concrete problem ---
1142 thus the specification actually captures a class of problems. The post-condition is not handled in
1143 the prototype presently.
1144 \item[11] is a rule-set (defined elsewhere) for evaluation of the pre-condition: \textit{(rhs X\_eq) is\_continuous\_in D}, instantiated with the values of a concrete problem, evaluates to true or false --- and all evaluation is done by
1145 rewriting determined by rule-sets.
1146 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1147 problem associated to a function from Computer Algebra (like an
1148 equation solver) which is not the case here.
1149 \item[13] is a list of methods solving the specified problem (here
1150 only one list item) represented analogously to {\rm 06}.
1154 %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1157 % {guh : guh, (*unique within this isac-knowledge*)
1158 % mathauthors: string list, (*copyright*)
1159 % init : pblID, (*to start refinement with*)
1160 % thy : theory, (* which allows to compile that pbt
1161 % TODO: search generalized for subthy (ref.p.69*)
1162 % (*^^^ WN050912 NOT used during application of the problem,
1163 % because applied terms may be from 'subthy' as well as from super;
1164 % thus we take 'maxthy'; see match_ags !*)
1165 % cas : term option,(*'CAS-command'*)
1166 % prls : rls, (* for preds in where_*)
1167 % where_: term list, (* where - predicates*)
1169 % (*this is the model-pattern;
1170 % it contains "#Given","#Where","#Find","#Relate"-patterns
1171 % for constraints on identifiers see "fun copy_name"*)
1172 % met : metID list}; (* methods solving the pbt*)
1174 %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1175 %WN oben selbst geschrieben.
1180 %WN das w"urde ich in \sec\label{progr} verschieben und
1181 %WN das SubProblem partial fractions zum Erkl"aren verwenden.
1182 % Such a specification is checked before the execution of a program is
1183 % started, the same applies for sub-programs. In the following example
1184 % (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1188 % \label{eg:subprob}
1190 % {\ttfamily \begin{tabbing}
1191 % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
1192 % ``\>\>[linear,univariate,equation,test],'' \\
1193 % ``\>\>[Test,solve\_linear])'' \\
1194 % ``\>[BOOL equ, REAL z])'' \\
1198 % \noindent If a program requires a result which has to be
1199 % calculated first we can use a subproblem to do so. In our specific
1200 % case we wanted to calculate the zeros of a fraction and used a
1201 % subproblem to calculate the zeros of the denominator polynom.
1206 \subsection{Implementation of the Method}\label{meth}
1207 A method collects all data required to interpret a certain program by
1208 Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
1209 the running example is embedded on the last line in the following method:
1210 %The methods represent the different ways a problem can be solved. This can
1211 %include mathematical tactics as well as tactics taught in different courses.
1212 %Declaring the Method itself gives us the possibilities to describe the way of
1213 %calculation in deep, as well we get the oppertunities to build in different
1221 03 "SP_InverseZTransformation_classic"
1224 06 ( ["SignalProcessing", "Z_Transform", "Inverse"],
1225 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1226 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1227 09 ("#Find" , ["stepResponse n_eq"]),
1235 \noindent The above code stores the whole structure analogously to a
1236 specification as described above:
1238 \item[01..06] are identical to those for the example specification on
1239 p.\pageref{exp-spec}.
1241 \item[07..09] show something looking like the specification; this is a
1242 {\em guard}: as long as not all \textit{Given} items are present and
1243 the \textit{Pre}-conditions is not true, interpretation of the program
1246 \item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case
1247 \textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets
1248 \textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
1249 \textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec}
1250 and (c) is required for the derivation-machinery checking user-input formulas.
1252 \item[12..13] \textit{errpats} are error-patterns~\cite{gdaroczy-EP-13} for this method and \textit{program} is the variable holding the example from p.\pageref {s:impl}.
1254 The many rule-sets above cause considerable efforts for the
1255 programmers, in particular, because there are no tools for checking
1256 essential features of rule-sets.
1258 % is again very technical and goes hard in detail. Unfortunataly
1259 % most declerations are not essential for a basic programm but leads us to a huge
1260 % range of powerful possibilities.
1262 % \begin{description}
1263 % \item[01..02] stores the method with the given name into the system under a global
1265 % \item[03] specifies the topic within which context the method can be found.
1266 % \item[04..05] as the requirements for different methods can be deviant we
1267 % declare what is \emph{given} and and what to \emph{find} for this specific method.
1268 % The code again helds on the topic of the case studie, where the inverse
1269 % z-transformation does a switch between a term describing a electrical filter into
1270 % its step response. Also the datatype has to be declared (bool - due the fact that
1271 % we handle equations).
1272 % \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
1273 % theorem of it is used for rewriting one single step.
1274 % \item[07] \texttt{rls} is the currently used ruleset for this method. This set
1275 % has already been defined before.
1276 % \item[08] we would have the possiblitiy to add this method to a predefined tree of
1277 % calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
1279 % \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
1281 % \item[10] \emph{predicates ruleset} can be used to indicates predicates within
1283 % \item[11] The \emph{check ruleset} summarizes rules for checking formulas
1285 % \item[12] \emph{error patterns} which are expected in this kind of method can be
1286 % pre-specified to recognize them during the method.
1287 % \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
1288 % of the specific method.
1289 % \item[14] for this code snipset we don't specify the programm itself and keep it
1290 % empty. Follow up \S\ref{progr} for informations on how to implement this
1291 % \textit{main} part.
1294 \subsection{Implementation of the TP-based Program}\label{progr}
1295 So finally all the prerequisites are described and the final task can
1296 be addressed. The program below comes back to the running example: it
1297 computes a solution for the problem from Fig.\ref{fig-interactive} on
1298 p.\pageref{fig-interactive}. The reader is reminded of
1299 \S\ref{PL-isab}, the introduction of the programming language:
1301 {\footnotesize\it\label{s:impl}
1303 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1304 \>{\rm 00}\>ML \{*\\
1305 \>{\rm 00}\>val program =\\
1306 \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1307 \>{\rm 02}\>\> {\tt let} \\
1308 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1309 \>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
1310 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1311 \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1312 \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1313 \>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
1314 %\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
1315 \>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1316 \>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1317 \>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@ \\
1318 \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1319 \>{\rm 13}\>\> {\tt in } \\
1320 \>{\rm 14}\>\>\> X'\_eq"\\
1323 % ORIGINAL FROM Inverse_Z_Transform.thy
1324 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1325 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1326 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1327 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1328 % " (zzz::real) = argument_in X'_z; "^(* z *)
1329 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1331 % " (pbz::real) = (SubProblem (Isac', "^(**)
1332 % " [partial_fraction,rational,simplification], "^
1333 % " [simplification,of_rationals,to_partial_fraction]) "^
1334 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1336 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1337 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1338 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1339 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1340 % " 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]*)
1341 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1342 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1343 The program is represented as a string and part of the method in
1344 \S\ref{meth}. As mentioned in \S\ref{PL} the program is purely
1345 functional and lacks any input statements and output statements. So
1346 the steps of calculation towards a solution (and interactive tutoring
1347 in step-wise problem solving) are created as a side-effect by
1348 Lucas-Interpretation. The side-effects are triggered by the tactics
1349 \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
1350 \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1351 {\rm 12} respectively. These tactics produce the respective lines in the
1352 calculation on p.\pageref{flow-impl}.
1354 The above lines {\rm 05, 06} do not contain a tactics, so they do not
1355 immediately contribute to the calculation on p.\pageref{flow-impl};
1356 rather, they compute actual arguments for the \texttt{SubProblem} in
1357 line {\rm 09}~\footnote{The tactics also are break-points for the
1358 interpreter, where control is handed over to the user in interactive
1359 tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
1361 \medskip The above program also indicates the dominant role of interactive
1362 selection of knowledge in the three-dimensional universe of
1363 mathematics. The \texttt{SubProblem} in the above lines
1364 {\rm 07..09} is more than a function call with the actual arguments
1365 \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
1369 \item the theory, in the example \textit{Isac} because different
1370 methods can be selected in Pt.3 below, which are defined in different
1371 theories with \textit{Isac} collecting them.
1372 \item the specification identified by \textit{[partial\_fraction,
1373 rational, simplification]} in the tree of specifications; this
1374 specification is analogous to the specification of the main program
1375 described in \S\ref{spec}; the problem is to find a ``partial fraction
1376 decomposition'' for a univariate rational polynomial.
1377 \item the method in the above example is \textit{[ ]}, i.e. empty,
1378 which supposes the interpreter to select one of the methods predefined
1379 in the specification, for instance in line {\rm 13} in the running
1380 example's specification on p.\pageref{exp-spec}~\footnote{The freedom
1381 (or obligation) for selection carries over to the student in
1382 interactive tutoring.}.
1385 The program code, above presented as a string, is parsed by Isabelle's
1386 parser --- the program is an Isabelle term. This fact is expected to
1387 simplify verification tasks in the future; on the other hand, this
1388 fact causes troubles in error detection which are discussed as part
1389 of the work-flow in the subsequent section.
1391 \section{Work-flow of Programming in the Prototype}\label{workflow}
1392 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
1393 step forward for interactive theory and proof development. The
1394 {\sisac}-prototype re-uses this IDE as a programming environment. The
1395 experiences from this re-use show, that the essential components are
1396 available from Isabelle/jEdit. However, additional tools and features
1397 are required to achieve acceptable usability.
1399 So notable experiences are reported here, also as a requirement
1400 capture for further development of TP-based languages and respective
1403 \subsection{Preparations and Trials}\label{flow-prep}
1404 The many sub-tasks to be accomplished {\em before} the first line of
1405 program code can be written and tested suggest an approach which
1406 step-wise establishes the prerequisites. The case study underlying
1407 this paper~\cite{jrocnik-bakk} documents the approach in a separate
1409 \textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
1410 II in the study comprises this theory, \LaTeX ed from the theory by
1411 use of Isabelle's document preparation system. This paper resembles
1412 the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
1413 implementation work involves several iterations.
1415 \bigskip For instance, only the last step, implementing the program
1416 described in \S\ref{meth}, reveals details required. Let us assume,
1417 this is the ML-function \textit{argument\_in} required in line {\rm 06}
1418 of the example program on p.\pageref{s:impl}; how this function needs
1419 to be implemented in the prototype has been discussed in \S\ref{funs}
1422 Now let us assume, that calling this function from the program code
1423 does not work; so testing this function is required in order to find out
1424 the reason: type errors, a missing entry of the function somewhere or
1425 even more nasty technicalities \dots
1430 02 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1431 03 val SOME (str, t') = eval_argument_in ""
1432 04 "Build_Inverse_Z_Transform.argument'_in" t 0;
1435 07 val it = "(argument_in X z) = z": string\end{verbatim}}
1437 \noindent So, this works: we get an ad-hoc theorem, which used in
1438 rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
1439 reduction and create a rule-set \texttt{rls} for that purpose:
1444 02 val rls = append_rls "test" e_rls
1445 03 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1446 04 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1448 06 val t' = Free ("z", "RealDef.real"): term
1449 07 val asm = []: term list\end{verbatim}}
1451 \noindent The resulting term \texttt{t'} is \texttt{Free ("z",
1452 "RealDef.real")}, i.e the variable \texttt{z}, so all is
1453 perfect. Probably we have forgotten to store this function correctly~?
1454 We review the respective \texttt{calclist} (again an
1455 \textit{Unsynchronized.ref} to be removed in order to adjust to
1456 Isabelle/Isar's asynchronous document model):
1460 01 calclist:= overwritel (! calclist,
1462 03 ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1464 05 ]);\end{verbatim}}
1466 \noindent The entry is perfect. So what is the reason~? Ah, probably there
1467 is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1468 right, the function \texttt{argument\_in} is not contained in the respective
1469 rule-set \textit{srls} \dots this just as an example of the intricacies in
1470 debugging a program in the present state of the prototype.
1472 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1473 Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
1474 usually developed within several iterations, the program can be
1475 assembled; on p.\pageref{s:impl} there is the complete program of the
1478 The completion of this program required efforts for several weeks
1479 (after some months of familiarisation with {\sisac}), caused by the
1480 abundance of intricacies indicated above. Also writing the program is
1481 not pleasant, given Isabelle/Isar/ without add-ons for
1482 programming. Already writing and parsing a few lines of program code
1483 is a challenge: the program is an Isabelle term; Isabelle's parser,
1484 however, is not meant for huge terms like the program of the running
1485 example. So reading out the specific error (usually type errors) from
1486 Isabelle's message is difficult.
1488 \medskip Testing the evaluation of the program has to rely on very
1489 simple tools. Step-wise execution is modeled by a function
1490 \texttt{me}, short for mathematics-engine~\footnote{The interface used
1491 by the front-end which created the calculation on
1492 p.\pageref{fig-interactive} is different from this function}:
1493 %the following is a simplification of the actual function
1498 02 val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}}
1500 \noindent This function takes as arguments a tactic \texttt{tac} which
1501 determines the next step, the step applied to the interpreter-state
1502 \texttt{ctree * pos} as last argument taken. The interpreter-state is
1503 a pair of a tree \texttt{ctree} representing the calculation created
1504 (see the example below) and a position \texttt{pos} in the
1505 calculation. The function delivers a quadruple, beginning with the new
1506 formula \texttt{mout} and the next tactic followed by the new
1509 This function allows to stepwise check the program:
1511 {\footnotesize\label{ml-check-program}
1515 03 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1516 04 "stepResponse (x[n::real]::bool)"];
1519 07 ["Inverse", "Z_Transform", "SignalProcessing"],
1520 08 ["SignalProcessing","Z_Transform","Inverse"]);
1521 09 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1522 10 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1523 11 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1524 12 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1528 \noindent Several dozens of calls for \texttt{me} are required to
1529 create the lines in the calculation below (including the sub-problems
1530 not shown). When an error occurs, the reason might be located
1531 many steps before: if evaluation by rewriting, as done by the prototype,
1532 fails, then first nothing happens --- the effects come later and
1533 cause unpleasant checks.
1535 The checks comprise watching the rewrite-engine for many different
1536 kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
1537 particular the environment and the context at the states position ---
1538 all checks have to rely on simple functions accessing the
1539 \texttt{ctree}. So getting the calculation below (which resembles the
1540 calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
1541 is the result of several weeks of development:
1543 {\small\it\label{exp-calc}
1545 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1546 \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1547 \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
1548 \>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} prep\_for\_part\_frac X\_eq}\\
1549 \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
1550 \>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
1551 \>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
1552 \>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
1553 \>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
1554 \>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
1555 \>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
1556 \> \>\>\>\> \_\_\_ \`- - -\\
1557 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1558 \>{\rm 12}\>\> $X^\prime z = {\cal z}^{-1} (\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}})$ \`{\footnotesize {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac)}\\
1559 \>{\rm 13}\>\> $X^\prime z = {\cal z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} prep\_for\_inverse\_z X'\_eq }\\
1560 \>{\rm 14}\>\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Rewrite\_Set} inverse\_z X'\_eq}\\
1561 \>{\rm 15}\> \dots\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Check\_Postcond}}
1563 The tactics on the right margin of the above calculation are those in
1564 the program on p.\pageref{s:impl} which create the respective formulas
1566 % ORIGINAL FROM Inverse_Z_Transform.thy
1567 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1568 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1569 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1570 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1571 % " (zzz::real) = argument_in X'_z; "^(* z *)
1572 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1574 % " (pbz::real) = (SubProblem (Isac', "^(**)
1575 % " [partial_fraction,rational,simplification], "^
1576 % " [simplification,of_rationals,to_partial_fraction]) "^
1577 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1579 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1580 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1581 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1582 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1583 % " 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]*)
1584 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1585 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1587 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1588 Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
1589 and the knowledge accumulated in it can be distributed to appropriate
1590 theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
1591 sub-problem accomplishing the partial fraction decomposition to
1592 \textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
1593 internals, this kind of distribution is not trivial. For instance, the
1594 function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
1595 string with the theory it has been defined in, so this string needs to
1596 be updated from \texttt{Build\_Inverse\_Z\_Transform} to
1597 \texttt{Atools} if that function is transferred to theory
1598 \textit{Atools.thy}.
1600 In order to obtain the functionality presented in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive} data must be exported from SML-structures to XML.
1601 This process is also rather bare-bones without authoring tools and is
1602 described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
1605 % -------------------------------------------------------------------
1607 % Material, falls noch Platz bleibt ...
1609 % -------------------------------------------------------------------
1612 % \subsubsection{Trials on Notation and Termination}
1614 % \paragraph{Technical notations} are a big problem for our piece of software,
1615 % but the reason for that isn't a fault of the software itself, one of the
1616 % troubles comes out of the fact that different technical subtopics use different
1617 % symbols and notations for a different purpose. The most famous example for such
1618 % a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1619 % math). In the specific part of signal processing one of this notation issues is
1620 % the use of brackets --- we use round brackets for analoge signals and squared
1621 % brackets for digital samples. Also if there is no problem for us to handle this
1622 % fact, we have to tell the machine what notation leads to wich meaning and that
1623 % this purpose seperation is only valid for this special topic - signal
1625 % \subparagraph{In the programming language} itself it is not possible to declare
1626 % fractions, exponents, absolutes and other operators or remarks in a way to make
1627 % them pretty to read; our only posssiblilty were ASCII characters and a handfull
1628 % greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1630 % With the upper collected knowledge it is possible to check if we were able to
1631 % donate all required terms and expressions.
1633 % \subsubsection{Definition and Usage of Rules}
1635 % \paragraph{The core} of our implemented problem is the Z-Transformation, due
1636 % the fact that the transformation itself would require higher math which isn't
1637 % yet avaible in our system we decided to choose the way like it is applied in
1638 % labratory and problem classes at our university - by applying transformation
1639 % rules (collected in transformation tables).
1640 % \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1641 % use of axiomatizations like shown in Example~\ref{eg:ruledef}
1644 % \label{eg:ruledef}
1647 % axiomatization where
1648 % rule1: ``1 = $\delta$[n]'' and
1649 % rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1650 % rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1654 % This rules can be collected in a ruleset and applied to a given expression as
1655 % follows in Example~\ref{eg:ruleapp}.
1659 % \label{eg:ruleapp}
1661 % \item Store rules in ruleset:
1663 % val inverse_Z = append_rls "inverse_Z" e_rls
1664 % [ Thm ("rule1",num_str @{thm rule1}),
1665 % Thm ("rule2",num_str @{thm rule2}),
1666 % Thm ("rule3",num_str @{thm rule3})
1668 % \item Define exression:
1670 % val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1671 % \item Apply ruleset:
1673 % val SOME (sample_term', asm) =
1674 % rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1678 % The use of rulesets makes it much easier to develop our designated applications,
1679 % but the programmer has to be careful and patient. When applying rulesets
1680 % two important issues have to be mentionend:
1681 % \subparagraph{How often} the rules have to be applied? In case of
1682 % transformations it is quite clear that we use them once but other fields
1683 % reuqire to apply rules until a special condition is reached (e.g.
1684 % a simplification is finished when there is nothing to be done left).
1685 % \subparagraph{The order} in which rules are applied often takes a big effect
1686 % and has to be evaluated for each purpose once again.
1688 % In our special case of Signal Processing and the rules defined in
1689 % Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1690 % constants. After this step has been done it no mather which rule fit's next.
1692 % \subsubsection{Helping Functions}
1694 % \paragraph{New Programms require,} often new ways to get through. This new ways
1695 % means that we handle functions that have not been in use yet, they can be
1696 % something special and unique for a programm or something famous but unneeded in
1697 % the system yet. In our dedicated example it was for example neccessary to split
1698 % a fraction into numerator and denominator; the creation of such function and
1699 % even others is described in upper Sections~\ref{simp} and \ref{funs}.
1701 % \subsubsection{Trials on equation solving}
1702 % %simple eq and problem with double fractions/negative exponents
1703 % \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
1704 % equations degree one and two. Solving equations in the first degree is no
1705 % problem, wether for a student nor for our machine; but even second degree
1706 % equations can lead to big troubles. The origin of this troubles leads from
1707 % the build up process of our equation solving functions; they have been
1708 % implemented some time ago and of course they are not as good as we want them to
1709 % be. Wether or not following we only want to show how cruel it is to build up new
1710 % work on not well fundamentials.
1711 % \subparagraph{A simple equation solving,} can be set up as shown in the next
1718 % ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
1722 % val (dI',pI',mI') =
1724 % ["abcFormula","degree_2","polynomial","univariate","equation"],
1725 % ["no_met"]);\end{verbatim}
1728 % Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
1729 % a short overview on the commands; at first we set up the equation and tell the
1730 % machine what's the bound variable and where to store the solution. Second step
1731 % is to define the equation type and determine if we want to use a special method
1732 % to solve this type.) Simple checks tell us that the we will get two results for
1733 % this equation and this results will be real.
1734 % So far it is easy for us and for our machine to solve, but
1735 % mentioned that a unvariate equation second order can have three different types
1736 % of solutions it is getting worth.
1737 % \subparagraph{The solving of} all this types of solutions is not yet supported.
1738 % Luckily it was needed for us; but something which has been needed in this
1739 % context, would have been the solving of an euation looking like:
1740 % $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
1741 % before (remember that befor it was no problem to handle for the machine) but
1742 % now, after a simple equivalent transformation, we are not able to solve
1744 % \subparagraph{Error messages} we get when we try to solve something like upside
1745 % were very confusing and also leads us to no special hint about a problem.
1746 % \par The fault behind is, that we have no well error handling on one side and
1747 % no sufficient formed equation solving on the other side. This two facts are
1748 % making the implemention of new material very difficult.
1750 % \subsection{Formalization of missing knowledge in Isabelle}
1752 % \paragraph{A problem} behind is the mechanization of mathematic
1753 % theories in TP-bases languages. There is still a huge gap between
1754 % these algorithms and this what we want as a solution - in Example
1755 % Signal Processing.
1761 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1764 % \noindent A very simple example on this what we call gap is the
1765 % simplification above. It is needles to say that it is correct and also
1766 % Isabelle for fills it correct - \emph{always}. But sometimes we don't
1767 % want expand such terms, sometimes we want another structure of
1768 % them. Think of a problem were we now would need only the coefficients
1769 % of $X$ and $Y$. This is what we call the gap between mechanical
1770 % simplification and the solution.
1775 % \paragraph{We are not able to fill this gap,} until we have to live
1776 % with it but first have a look on the meaning of this statement:
1777 % Mechanized math starts from mathematical models and \emph{hopefully}
1778 % proceeds to match physics. Academic engineering starts from physics
1779 % (experimentation, measurement) and then proceeds to mathematical
1780 % modeling and formalization. The process from a physical observance to
1781 % a mathematical theory is unavoidable bound of setting up a big
1782 % collection of standards, rules, definition but also exceptions. These
1783 % are the things making mechanization that difficult.
1792 % \noindent Think about some units like that one's above. Behind
1793 % each unit there is a discerning and very accurate definition: One
1794 % Meter is the distance the light travels, in a vacuum, through the time
1795 % of 1 / 299.792.458 second; one kilogram is the weight of a
1796 % platinum-iridium cylinder in paris; and so on. But are these
1797 % definitions usable in a computer mechanized world?!
1802 % \paragraph{A computer} or a TP-System builds on programs with
1803 % predefined logical rules and does not know any mathematical trick
1804 % (follow up example \ref{eg:trick}) or recipe to walk around difficult
1810 % \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1811 % \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1812 % \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1813 % \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1815 % \noindent Sometimes it is also useful to be able to apply some
1816 % \emph{tricks} to get a beautiful and particularly meaningful result,
1817 % which we are able to interpret. But as seen in this example it can be
1818 % hard to find out what operations have to be done to transform a result
1819 % into a meaningful one.
1824 % \paragraph{The only possibility,} for such a system, is to work
1825 % through its known definitions and stops if none of these
1826 % fits. Specified on Signal Processing or any other application it is
1827 % often possible to walk through by doing simple creases. This creases
1828 % are in general based on simple math operational but the challenge is
1829 % to teach the machine \emph{all}\footnote{Its pride to call it
1830 % \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1831 % reach a high level of \emph{all} but it in real it will still be a
1832 % survey of knowledge which links to other knowledge and {{\sisac}{}} a
1833 % trainer and helper but no human compensating calculator.
1835 % {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1836 % specifications of problems out of topics from Signal Processing, etc.)
1837 % and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1838 % physical knowledge. The result is a three-dimensional universe of
1839 % mathematics seen in Figure~\ref{fig:mathuni}.
1843 % \includegraphics{fig/universe}
1844 % \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1845 % combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1846 % leads to a three dimensional math universe.\label{fig:mathuni}}
1850 % %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1851 % %WN bitte folgende Bezeichnungen nehmen:
1853 % %WN axis 1: Algorithmic Knowledge (Programs)
1854 % %WN axis 2: Application-oriented Knowledge (Specifications)
1855 % %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1857 % %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1858 % %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1859 % %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1861 % %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1862 % %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1863 % %JR gefordert werden WN2...
1864 % %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1865 % %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1866 % %WN2 zusammenschneiden um die R"ander weg zu bekommen)
1867 % %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1868 % %WN2 png + pdf figures mitzuschicken.
1870 % \subsection{Notes on Problems with Traditional Notation}
1872 % \paragraph{During research} on these topic severely problems on
1873 % traditional notations have been discovered. Some of them have been
1874 % known in computer science for many years now and are still unsolved,
1875 % one of them aggregates with the so called \emph{Lambda Calculus},
1876 % Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1883 % \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1886 % \[ f(p)=\ldots\; p \in \quad R \]
1889 % \noindent Above we see two equations. The first equation aims to
1890 % be a mapping of an function from the reel range to the reel one, but
1891 % when we change only one letter we get the second equation which
1892 % usually aims to insert a reel point $p$ into the reel function. In
1893 % computer science now we have the problem to tell the machine (TP) the
1894 % difference between this two notations. This Problem is called
1895 % \emph{Lambda Calculus}.
1900 % \paragraph{An other problem} is that terms are not full simplified in
1901 % traditional notations, in {{\sisac}} we have to simplify them complete
1902 % to check weather results are compatible or not. in e.g. the solutions
1903 % of an second order linear equation is an rational in {{\sisac}} but in
1904 % tradition we keep fractions as long as possible and as long as they
1905 % aim to be \textit{beautiful} (1/8, 5/16,...).
1906 % \subparagraph{The math} which should be mechanized in Computer Theorem
1907 % Provers (\emph{TP}) has (almost) a problem with traditional notations
1908 % (predicate calculus) for axioms, definitions, lemmas, theorems as a
1909 % computer program or script is not able to interpret every Greek or
1910 % Latin letter and every Greek, Latin or whatever calculations
1911 % symbol. Also if we would be able to handle these symbols we still have
1912 % a problem to interpret them at all. (Follow up \hbox{Example
1913 % \ref{eg:symbint1}})
1917 % \label{eg:symbint1}
1919 % u\left[n\right] \ \ldots \ unitstep
1922 % \noindent The unitstep is something we need to solve Signal
1923 % Processing problem classes. But in {{{\sisac}{}}} the rectangular
1924 % brackets have a different meaning. So we abuse them for our
1925 % requirements. We get something which is not defined, but usable. The
1926 % Result is syntax only without semantic.
1931 % In different problems, symbols and letters have different meanings and
1932 % ask for different ways to get through. (Follow up \hbox{Example
1933 % \ref{eg:symbint2}})
1937 % \label{eg:symbint2}
1939 % \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1942 % \noindent For using exponents the three \texttt{widehat} symbols
1943 % are required. The reason for that is due the development of
1944 % {{{\sisac}{}}} the single \texttt{widehat} and also the double were
1945 % already in use for different operations.
1950 % \paragraph{Also the output} can be a problem. We are familiar with a
1951 % specified notations and style taught in university but a computer
1952 % program has no knowledge of the form proved by a professor and the
1953 % machines themselves also have not yet the possibilities to print every
1954 % symbol (correct) Recent developments provide proofs in a human
1955 % readable format but according to the fact that there is no money for
1956 % good working formal editors yet, the style is one thing we have to
1959 % \section{Problems rising out of the Development Environment}
1961 % fehlermeldungen! TODO
1963 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
1965 \section{Summary and Conclusions}\label{conclusion}
1969 %This paper gives a first experience report about programming with a
1970 %TP-based programming language.
1972 A brief re-introduction of the novel kind of programming
1973 language by example of the {\sisac}-prototype makes the paper
1974 self-contained. The main section describes all the main concepts
1975 involved in TP-based programming and all the sub-tasks concerning
1976 respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain
1977 modeling, implementation of term rewriting systems for the
1978 rewriting-engine, formal (implicit) specification of the problem to be
1979 (explicitly) described by the program, implementation of the many components
1980 required for Lucas-Interpretation and finally implementation of the
1983 The many concepts and sub-tasks involved in programming require a
1984 comprehensive work-flow; first experiences with the work-flow as
1985 supported by the present prototype are described as well: Isabelle +
1986 Isar + jEdit provide appropriate components for establishing an
1987 efficient development environment integrating computation and
1988 deduction. However, the present state of the prototype is far off a
1989 state appropriate for wide-spread use: the prototype of the program
1990 language lacks expressiveness and elegance, the prototype of the
1991 development environment is hardly usable: error messages still address
1992 the developer of the prototype's interpreter rather than the
1993 application programmer, implementation of the many settings for the
1994 Lucas-Interpreter is cumbersome.
1996 \subsection{Conclusions for Future Development}
1997 From the above mentioned experiences a successful proof of concept can be concluded:
1998 programming arbitrary problems from engineering sciences is possible,
1999 in principle even in the prototype. Furthermore the experiences allow
2000 to conclude detailed requirements for further development:
2002 \item Clarify underlying logics such that programming is smoothly
2003 integrated with verification of the program; the post-condition should
2004 be proved more or less automatically, otherwise working engineers
2005 would not encounter such programming.
2006 \item Combine the prototype's programming language with Isabelle's
2007 powerful function package and probably with more of SML's
2008 pattern-matching features; include parallel execution on multi-core
2009 machines into the language design.
2010 \item Extend the prototype's Lucas-Interpreter such that it also
2011 handles functions defined by use of Isabelle's functions package; and
2012 generalize Isabelle's code generator such that efficient code for the
2013 whole definition of the programming language can be generated (for
2014 multi-core machines).
2015 \item Develop an efficient development environment with
2016 integration of programming and proving, with management not only of
2017 Isabelle theories, but also of large collections of specifications and
2019 \item\label{CAS} Extend Isabelle's computational features in direction of
2020 \textit{verfied} Computer Algebra: simplification extended by
2021 algorithms beyond rewriting (cancellation of multivariate rationals,
2022 factorisation, partial fraction decomposition, etc), equation solving
2025 Provided successful accomplishment, these points provide distinguished
2026 components for virtual workbenches appealing to practitioners of
2027 engineering in the near future.
2029 \subsection{Preview to Development of Course Material}
2030 Interactive course material, as addressed by the title,
2031 can comprise step-wise problem solving created as a side-effect of a
2032 TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an
2033 interactive programming environment, Lucas-Interpretation also can
2034 provide TP-based services for a flexible dialogue component with
2035 adaptive user guidance for independent and inquiry-based learning.
2037 However, the {\sisac} prototype is not ready for use in field-tests,
2038 not only due to the above five requirements not sufficiently
2039 accomplished, but also due to usability of the fron-end, in particular
2040 the lack of an editor for formulas in 2-dimension representation.
2042 Nevertheless, the experiences from the case study described in this
2043 paper, allow to give a preview to the development of course material,
2044 if based on Lucas-Interpretation:
2046 \paragraph{Development of material from scratch} is too much effort
2047 just for e-learning; this has become clear with the case study. For
2048 getting support for stepwise problem solving just in {\em one} example
2049 class, the one presented in this paper, involved the following tasks:
2051 \item Adapt the equation solver; since that was too laborous, the
2052 program has been adapted in an unelegant way.
2053 \item Implement an algorithms for partial fraction decomposition,
2054 which is considered a standard normal form in Computer Algebra.
2055 \item Implement a specification for partial fraction decomposition and
2056 locate it appropriately in the hierarchy of specification.
2057 \item Declare definitions and theorems within the theory of
2058 ${\cal Z}$-transform, and prove the theorems (which was not done in the
2061 On the other hand, for the one the class of problems implemented,
2062 adding an arbitrary number of examples within this class requires a
2063 few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an
2064 example is called from an HTML-file by an URL, which addresses an
2065 XML-structure holding the respective data as shown on
2066 p.\pageref{ml-check-program}.} and the support for individual stepwise
2067 problem solving comes for free.
2069 \paragraph{E-learning benefits from Formal Domain Engineering} which can be
2070 expected for various domains in the near future. In order to cope with
2071 increasing complexity in domain of technology, specific domain
2072 knowledge is beeing mechanised, not only for software technology
2073 \footnote{For instance, the Archive of Formal Proofs
2074 http://afp.sourceforge.net/} but also for other engineering domains
2075 \cite{Dehbonei&94,Hansen94b,db:dom-eng}. This fairly new part of
2076 engineering sciences is called ``domain engineering'' in
2077 \cite{db:SW-engIII}.
2079 Given this kind of mechanised knowledge including mathematical
2080 theories, domain specific definitions, specifications and algorithms,
2081 theorems and proofs, then e-learning with support for individual
2082 stepwise problem solving will not be much ado anymore; then e-learning
2083 media in technology education can be derived from this knowledge with
2086 \paragraph{Development differentiates into tasks} more separated than
2087 without Lucas-Interpretation and more challenginging in specific
2088 expertise. These are the kinds of experts expected to cooperate in
2091 \item ``Domain engineers'', who accomplish fairly novel tasks
2092 described in this paper.
2093 \item Course designers, who provide the instructional design according
2094 to curricula, together with usability experts and media designers, are
2095 indispensable in production of e-learning media at the state-of-the
2097 \item ``Dialog designers'', whose part of development is clearly
2098 separated from the part of domain engineers as a consequence of
2099 Lucas-Interpretation: TP-based programs are functional, as mentioned,
2100 and are only concerned with describing mathematics --- and not at all
2101 concerned with interaction, psychology, learning theory and the like,
2102 because there are no in/output statements. Dialog designers can expect
2103 a high-level rule-based language~\cite{gdaroczy-EP-13} for describing
2107 % response-to-referees:
2108 % (2.1) details of novel technology in order to estimate the impact
2109 % (2.2) which kinds of expertise are required for production of e-learning media (instructional design, math authoring, dialog authoring, media design)
2110 % (2.3) what in particular is required for programming new exercises supported by next-step-guidance (expertise / efforts)
2111 % (2.4) estimation of break-even points for development of next-step-guidance
2112 % (2.5) usability of ISAC prototype at the present state
2114 % The points (1.*) seem to be well covered in the paper, the points (2.*) are not. So I decided to address the points (2.*) in a separate section §5.1."".
2116 \bigskip\noindent For this decade there seems to be a window of opportunity opening from
2117 one side inreasing demand for formal domain engineering and from the
2118 other side from TP more and more gaining industrial relevance. Within
2119 this window, development of TP-based educational software can take
2120 benefit from the fact, that the TPs leading in Europe, Coq~\cite{coq-team-10} and
2121 Isabelle are still open source together with the major part of
2122 mechanised knowledge.%~\footnote{NICTA}.
2124 \bibliographystyle{alpha}
2125 {\small\bibliography{references}}
2128 % LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
2129 % LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised
2130 % LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
2131 % LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
2132 % LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
2133 % LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq
2134 % LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
2135 % LocalWords: mechanisation multi