1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 % Electronic Journal of Mathematics and Technology (eJMT) %
3 % style sheet for LaTeX. Please do not modify sections %
4 % or commands marked 'eJMT'. %
6 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10 \documentclass[12pt,a4paper]{article}% %
12 \usepackage{amsfonts,amsmath,amssymb} %
13 \usepackage[a4paper]{geometry} %
14 \usepackage{fancyhdr} %
16 \usepackage[pdftex]{hyperref} % see note below %
17 \usepackage{graphicx}% %
23 \newtheorem{theorem}{Theorem} %
24 \newtheorem{acknowledgement}[theorem]{Acknowledgement} %
25 \newtheorem{algorithm}[theorem]{Algorithm} %
26 \newtheorem{axiom}[theorem]{Axiom} %
27 \newtheorem{case}[theorem]{Case} %
28 \newtheorem{claim}[theorem]{Claim} %
29 \newtheorem{conclusion}[theorem]{Conclusion} %
30 \newtheorem{condition}[theorem]{Condition} %
31 \newtheorem{conjecture}[theorem]{Conjecture} %
32 \newtheorem{corollary}[theorem]{Corollary} %
33 \newtheorem{criterion}[theorem]{Criterion} %
34 \newtheorem{definition}[theorem]{Definition} %
35 \newtheorem{example}[theorem]{Example} %
36 \newtheorem{exercise}[theorem]{Exercise} %
37 \newtheorem{lemma}[theorem]{Lemma} %
38 \newtheorem{notation}[theorem]{Notation} %
39 \newtheorem{problem}[theorem]{Problem} %
40 \newtheorem{proposition}[theorem]{Proposition} %
41 \newtheorem{remark}[theorem]{Remark} %
42 \newtheorem{solution}[theorem]{Solution} %
43 \newtheorem{summary}[theorem]{Summary} %
44 \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } %
45 {\ \rule{0.5em}{0.5em}} %
47 % eJMT page dimensions %
49 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
51 % eJMT header & footer %
53 \newcounter{ejmtFirstpage} %
54 \setcounter{ejmtFirstpage}{1} %
56 \setlength{\headheight}{14pt} %
57 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
58 \pagestyle{fancyplain} %
60 \fancyhead[c]{\small The Electronic Journal of Mathematics%
61 \ and Technology, Volume 1, Number 1, ISSN 1933-2823} %
63 \ifnum\value{ejmtFirstpage}=0% %
64 {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% %
65 \else\setcounter{ejmtFirstpage}{0}\fi% %
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
70 % Please place your own definitions here
72 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
73 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
76 \definecolor{lgray}{RGB}{238,238,238}
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 % How to use hyperref %
82 % ------------------- %
84 % Probably the only way you will need to use the hyperref %
85 % package is as follows. To make some text, say %
86 % "My Text Link", into a link to the URL %
87 % http://something.somewhere.com/mystuff, use %
89 % \href{http://something.somewhere.com/mystuff}{My Text Link}
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
97 \title{Trials with TP-based Programming
99 for Interactive Course Material}%
101 % Single author. Please supply at least your name,
102 % email address, and affiliation here.
104 \author{\begin{tabular}{c}
105 \textit{Jan Ro\v{c}nik} \\
106 jan.rocnik@student.tugraz.at \\
108 Graz University of Technology\\
112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
114 % eJMT commands - do not change these %
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
125 Traditional course material in engineering disciplines lacks an
126 important component, interactive support for step-wise problem
127 solving. Theorem-Proving (TP) technology is appropriate for one part
128 of such support, in checking user-input. For the other part of such
129 support, guiding the learner towards a solution, another kind of
130 technology is required.
132 Both kinds of support can be achieved by so-called
133 Lucas-Interpretation which combines deduction and computation and, for
134 the latter, uses a novel kind of programming language. This language
135 is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
136 programming language''.
138 This paper is the experience report of the first ``application
139 programmer'' using this language for creating exercises in step-wise
140 problem solving for an advanced lab in Signal Processing. The tasks
141 involved in TP-based programming are described together with the
142 experience gained from a prototype of the programming language and of
145 The report concludes with a positive proof of concept, states
146 insufficiency usability of the prototype and captures the requirements
147 for further development of both, the programming language and the
152 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
156 \thispagestyle{fancy} %
158 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
160 % Please use the following to indicate sections, subsections,
161 % etc. Please also use \subsubsection{...}, \paragraph{...}
162 % and \subparagraph{...} as necessary.
165 \section{Introduction}\label{intro}
167 % \paragraph{Didactics of mathematics}
168 %WN: wenn man in einem high-quality paper von 'didactics' spricht,
169 %WN muss man am state-of-the-art ankn"upfen -- siehe
170 %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
171 % faces a specific issue, a gap
172 % between (1) introduction of math concepts and skills and (2)
173 % application of these concepts and skills, which usually are separated
174 % into different units in curricula (for good reasons). For instance,
175 % (1) teaching partial fraction decomposition is separated from (2)
176 % application for inverse Z-transform in signal processing.
178 % \par This gap is an obstacle for applying math as an fundamental
179 % thinking technology in engineering: In (1) motivation is lacking
180 % because the question ``What is this stuff good for?'' cannot be
181 % treated sufficiently, and in (2) the ``stuff'' is not available to
182 % students in higher semesters as widespread experience shows.
184 % \paragraph{Motivation} taken by this didactic issue on the one hand,
185 % and ongoing research and development on a novel kind of educational
186 % mathematics assistant at Graz University of
187 % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
188 % scope with this issue on the other hand, several institutes are
189 % planning to join their expertise: the Institute for Information
190 % Systems and Computer Media (IICM), the Institute for Software
191 % Technology (IST), the Institutes for Mathematics, the Institute for
192 % Signal Processing and Speech Communication (SPSC), the Institute for
193 % Structural Analysis and the Institute of Electrical Measurement and
194 % Measurement Signal Processing.
195 %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
196 %WN und damit zu verg"anglich.
197 % \par This thesis is the first attempt to tackle the above mentioned
198 % issue, it focuses on Telematics, because these specific studies focus
199 % on mathematics in \emph{STEOP}, the introductory orientation phase in
200 % Austria. \emph{STEOP} is considered an opportunity to investigate the
201 % impact of {\sisac}'s prototype on the issue and others.
204 Traditional course material in engineering disciplines lacks an
205 important component, interactive support for step-wise problem
206 solving. The lack becomes evident by comparing existing course
207 material with the sheets collected from written exams (in case solving
208 engineering problems is {\em not} deteriorated to multiple choice
209 tests) on the topics addressed by the materials.
210 Theorem-Proving (TP) technology can provide such support by
211 specific services. An important part of such services is called
212 ``next-step-guidance'', generated by a specific kind of ``TP-based
213 programming language''. In the
214 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
215 a language is prototyped in line with~\cite{plmms10} and built upon
216 the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}
217 \footnote{http://isabelle.in.tum.de/}.
218 The TP services are coordinated by a specific interpreter for the
219 programming language, called
220 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language
221 will be briefly re-introduced in order to make the paper
224 The main part of the paper is an account of first experiences
225 with programming in this TP-based language. The experience was gained
226 in a case study by the author. The author was considered an ideal
227 candidate for this study for the following reasons: as a student in
228 Telematics (computer science with focus on Signal Processing) he had
229 general knowledge in programming as well as specific domain knowledge
230 in Signal Processing; and he was {\em not} involved in the development of
231 {\sisac}'s programming language and interpreter, thus being a novice to the
234 The goals of the case study were: (1) to identify some TP-based programs for
235 interactive course material for a specific ``Advanced Signal
236 Processing Lab'' in a higher semester, (2) respective program
237 development with as little advice as possible from the {\sisac}-team and (3)
238 to document records and comments for the main steps of development in an
239 Isabelle theory; this theory should provide guidelines for future programmers.
240 An excerpt from this theory is the main part of this paper.
243 \medskip The major example resulting from the case study will be used
244 as running example throughout this paper. This example requires a
245 program resembling the size of real-world applications in engineering;
246 such a size was considered essential for the case study, since there
247 are many small programs for a long time (mainly concerned with
248 elementary Computer Algebra like simplification, equation solving,
249 calculus, etc.~\footnote{The programs existing in the {\sisac}
250 prototype are found at
251 http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})
253 \paragraph{The mathematical background of the running example} is the
254 following: In Signal Processing, ``the ${\cal Z}$-transform for
255 discrete-time signals is the counterpart of the Laplace transform for
256 continuous-time signals, and they each have a similar relationship to
257 the corresponding Fourier transform. One motivation for introducing
258 this generalization is that the Fourier transform does not converge
259 for all sequences, and it is useful to have a generalization of the
260 Fourier transform that encompasses a broader class of signals. A
261 second advantage is that in analytic problems, the ${\cal Z}$-transform
262 notation is often more convenient than the Fourier transform
263 notation.'' ~\cite[p. 128]{oppenheim2010discrete}. The ${\cal Z}$-transform
266 X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}
268 where a discrete time sequence $x[n]$ is transformed into the function
269 $X(z)$ where $z$ is a continuous complex variable. The inverse
270 function is addressed in the running example and can be determined by
273 x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz
275 where the letter $C$ represents a contour within the range of
276 convergence of the ${\cal Z}$-transform. The unit circle can be a special
277 case of this contour. Remember that $j$ is the complex number in the
278 domain of engineering. As this transform requires high effort to
279 be solved, tables of commonly used transform pairs are used in
280 education as well as in engineering practice; such tables can be found
281 at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.
282 A completely solved and more detailed example can be found at
283 ~\cite[p. 149f]{oppenheim2010discrete}.
285 Following conventions in engineering education and in practice, the
286 running example solves the problem by use of a table.
288 \paragraph{Support for interactive stepwise problem solving} in the
289 {\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,
290 the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:
291 A student inputs formulas line by line on the \textit{``Worksheet''},
292 and each step (i.e. each formula on completion) is immediately checked
293 by the system, such that at most {\em one inconsistent} formula can reside on
294 the Worksheet (on the input line, marked by the red $\otimes$).
297 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
298 %\includegraphics[width=140mm]{fig/isac-Ztrans-math}
299 \caption{Step-wise problem solving guided by the TP-based program
300 \label{fig-interactive}}
303 If the student gets stuck and does not know the formula to proceed
304 with, there is the button \framebox{NEXT} presenting the next formula
305 on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the
306 final result in case the student is not interested in intermediate
309 Adaptive dialogue guidance is already under
310 construction~\cite{gdaroczy-EP-13} and the two buttons will disappear,
311 since their presence is not wanted in many learning scenarios (in
312 particular, {\em not} in written exams).
314 The buttons \framebox{Theories}, \framebox{Problems} and
315 \framebox{Methods} are the entry points for interactive lookup of the
316 underlying knowledge. For instance, pushing \framebox{Theories} in
317 the configuration shown in Fig.\ref{fig-interactive}, pops up a
318 ``Theory browser'' displaying the theorem(s) justifying the current
319 step. The browser allows to lookup all other theories, thus
320 supporting indepentend investigation of underlying definitions,
321 theorems, proofs --- where the HTML representation of the browsers is
322 ready for arbitrary multimedia add-ons. Likewise, the browsers for
323 \framebox{Problems} and \framebox{Methods} support context sensitive
324 as well as interactive access to specifications and programs
327 There is also a simple web-based representation of knowledge items;
328 the items under consideration in this paper can be looked up as
329 well~\footnote{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Inverse\_Z\_Transform.thy}}~\footnote{
330 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Partial\_Fractions.thy}}~\footnote{
331 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Build\_Inverse\_Z\_Transform.thy}}.
333 % can be explained by having a look at
334 % Fig.\ref{fig-interactive} which shows the beginning of the interactive
335 % construction of a solution for the problem. This construction is done in the
336 % right window named ``Worksheet''.
338 % User-interaction on the Worksheet is {\em checked} and {\em guided} by
341 % \item Formulas input by the user are {\em checked} by TP: such a
342 % formula establishes a proof situation --- the prover has to derive the
343 % formula from the logical context. The context is built up from the
344 % formal specification of the problem (here hidden from the user) by the
346 % \item If the user gets stuck, the program developed below in this
347 % paper ``knows the next step'' and Lucas-Interpretation provides services
348 % featuring so-called ``next-step-guidance''; this is out of scope of this
349 % paper and can be studied in~\cite{gdaroczy-EP-13}.
350 % \end{enumerate} It should be noted that the programmer using the
351 % TP-based language is not concerned with interaction at all; we will
352 % see that the program contains neither input-statements nor
353 % output-statements. Rather, interaction is handled by the interpreter
356 % So there is a clear separation of concerns: Dialogues are adapted by
357 % dialogue authors (in Java-based tools), using TP services provided by
358 % Lucas-Interpretation. The latter acts on programs developed by
359 % mathematics-authors (in Isabelle/ML); their task is concern of this
362 \bigskip The paper is structured as follows: The introduction
363 \S\ref{intro} is followed by a brief re-introduction of the TP-based
364 programming language in \S\ref{PL}, which extends the executable
365 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
366 play a specific role in Lucas-Interpretation and in providing the TP
367 services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
368 the main steps in developing the program for the running example:
369 prepare domain knowledge, implement the formal specification of the
370 problem, prepare the environment for the interpreter, implement the
371 program in \S\ref{isabisac} to \S\ref{progr} respectively.
372 The work-flow of programming, debugging and testing is
373 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
374 give directions identified for future development.
377 \section{\isac's Prototype for a Programming Language}\label{PL}
378 The prototype of the language and of the Lucas-Interpreter is briefly
379 described from the point of view of a programmer. The language extends
380 the executable fragment of Higher-Order Logic (HOL) in the theorem prover
381 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
383 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
384 The executable fragment consists of data-type and function
385 definitions. It's usability even suggests that fragment for
386 introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming
387 languages. Thus there are
389 \item[base types,] in particular \textit{bool}, the type of truth
390 values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
391 natural, integer and complex numbers respectively in mathematics.
392 \item[type constructors] allow to define arbitrary types, from
393 \textit{set}, \textit{list} to advanced data-structures like
394 \textit{trees}, red-black-trees etc.
395 \item[function types,] denoted by $\Rightarrow$.
396 \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
397 type polymorphism. Isabelle automatically computes the type of each
398 variable in a term by use of Hindley-Milner type inference
399 \cite{pl:hind97,Milner-78}.
402 \textbf{Terms} are formed as in functional programming by applying
403 functions to arguments. If $f$ is a function of type
404 $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
405 $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
406 has type $\tau$. There are many predefined infix symbols like $+$ and
407 $\leq$ most of which are overloaded for various types.
409 HOL also supports some basic constructs from functional programming:
410 {\footnotesize\it\label{isabelle-stmts}
411 \begin{tabbing} 123\=\kill
412 01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
413 02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
414 03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
415 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
417 \noindent The running example's program uses some of these elements
418 (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
419 let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
420 is an Isabelle term with specific function constants like {\tt
421 program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
422 Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
425 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
426 % x. \; x$ is the identity function.
428 %JR warum auskommentiert? WN2...
429 %WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
430 %WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
431 %WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
433 %WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
434 %WN2 Platz f"ur Anderes weg.
436 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
437 constants \textit{True} and \textit{False} and the usual logical
438 connectives (in decreasing order of precedence): $\neg, \land, \lor,
441 \textbf{Equality} is available in the form of the infix function $=$
442 of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
443 formulas, where it means ``if and only if''.
445 \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
446 P$. Quantifiers lead to non-executable functions, so functions do not
447 always correspond to programs, for instance, if comprising \\$(
448 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
451 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
452 The prototype extends Isabelle's language by specific statements
453 called tactics~\footnote{{\sisac}'s. These tactics are different from
454 Isabelle's tactics: the former concern steps in a calculation, the
455 latter concern proofs.}. For the programmer these
456 statements are functions with the following signatures:
459 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
460 term} * {\it term}\;{\it list}$:
461 this tactic applies {\it theorem} to a {\it term} yielding a {\it
462 term} and a {\it term list}, the list are assumptions generated by
463 conditional rewriting. For instance, the {\it theorem}
464 $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
465 applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
466 $(\frac{2}{3}, [x\not=0])$.
468 \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
469 term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
470 this tactic applies {\it ruleset} to a {\it term}; {\it ruleset} is
471 a confluent and terminating term rewrite system, in general. If
472 none of the rules ({\it theorem}s) is applicable on interpretation
473 of this tactic, an exception is thrown.
475 % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
476 % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
479 % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
480 % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
484 \item[Substitute:] ${\it substitution}\Rightarrow{\it
485 term}\Rightarrow{\it term}$: allows to access sub-terms.
488 \item[Take:] ${\it term}\Rightarrow{\it term}$:
489 this tactic has no effect in the program; but it creates a side-effect
490 by Lucas-Interpretation (see below) and writes {\it term} to the
493 \item[Subproblem:] ${\it theory} * {\it specification} * {\it
494 method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
495 this tactic is a generalisation of a function call: it takes an
496 \textit{argument list} as usual, and additionally a triple consisting
497 of an Isabelle \textit{theory}, an implicit \textit{specification} of the
498 program and a \textit{method} containing data for Lucas-Interpretation,
499 last not least a program (as an explicit specification)~\footnote{In
500 interactive tutoring these three items can be determined explicitly
503 The tactics play a specific role in
504 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
505 break-points where, as a side-effect, a line is added to a calculation
506 as a protocol for proceeding towards a solution in step-wise problem
507 solving. At the same points Lucas-Interpretation serves interactive
508 tutoring and hands over control to the user. The user is free to
509 investigate underlying knowledge, applicable theorems, etc. And the
510 user can proceed constructing a solution by input of a tactic to be
511 applied or by input of a formula; in the latter case the
512 Lucas-Interpreter has built up a logical context (initialised with the
513 precondition of the formal specification) such that Isabelle can
514 derive the formula from this context --- or give feedback, that no
515 derivation can be found.
517 \subsection{Tactics as Control Flow Statements}
518 The flow of control in a program can be determined by {\tt if then else}
519 and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
520 by additional tactics:
522 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
523 term}$: iterates over tactics which take a {\it term} as argument as
524 long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
527 \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
528 if {\it tactic} is applicable, then it is applied to {\it term},
529 otherwise {\it term} is passed on without changes.
531 \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
532 term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
533 it is applied to the first {\it term} yielding another {\it term},
534 otherwise the second {\it tactic} is applied; if none is applicable an
537 \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
538 term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
539 first {\it term} yielding an intermediate term (not appearing in the
540 signature) to which the second {\it tactic} is applied.
542 \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
543 term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
544 {\it tactic} is applied to the first {\it term} yielding an
545 intermediate term (not appearing in the signature); the intermediate
546 term is added to the environment the first {\it term} is evaluated in
547 etc. as long as the first {\it term} is true.
549 The tactics are not treated as break-points by Lucas-Interpretation
550 and thus do neither contribute to the calculation nor to interaction.
552 \section{Concepts and Tasks in TP-based Programming}\label{trial}
553 %\section{Development of a Program on Trial}
555 This section presents all the concepts involved in TP-based
556 programming and all the tasks to be accomplished by programmers. The
557 presentation uses the running example from
558 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
560 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
562 %WN was Fachleute unter obigem Titel interessiert findet sich
563 %WN unterhalb des auskommentierten Textes.
565 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
566 %WN auf Computer-Mathematiker fokussiert.
567 % \paragraph{As mentioned in the introduction,} a prototype of an
568 % educational math assistant called
569 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
570 % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
571 % the gap between (1) introducation and (2) application of mathematics:
572 % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
573 % requires each fact and each action justified by formal logic, so
574 % {{{\sisac}{}}} makes justifications transparent to students in
575 % interactive step-wise problem solving. By that way {{\sisac}} already
578 % \item Introduction of math stuff (in e.g. partial fraction
579 % decomposition) by stepwise explaining and exercising respective
580 % symbolic calculations with ``next step guidance (NSG)'' and rigorously
581 % checking steps freely input by students --- this also in context with
582 % advanced applications (where the stuff to be taught in higher
583 % semesters can be skimmed through by NSG), and
584 % \item Application of math stuff in advanced engineering courses
585 % (e.g. problems to be solved by inverse Z-transform in a Signal
586 % Processing Lab) and now without much ado about basic math techniques
587 % (like partial fraction decomposition): ``next step guidance'' supports
588 % students in independently (re-)adopting such techniques.
590 % Before the question is answers, how {{\sisac}}
591 % accomplishes this task from a technical point of view, some remarks on
592 % the state-of-the-art is given, therefor follow up Section~\ref{emas}.
594 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
596 % \paragraph{Educational software in mathematics} is, if at all, based
597 % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
598 % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
599 % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
600 % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
601 % base technologies are used to program math lessons and sometimes even
602 % exercises. The latter are cumbersome: the steps towards a solution of
603 % such an interactive exercise need to be provided with feedback, where
604 % at each step a wide variety of possible input has to be foreseen by
605 % the programmer - so such interactive exercises either require high
606 % development efforts or the exercises constrain possible inputs.
608 % \subparagraph{A new generation} of educational math assistants (EMAs)
609 % is emerging presently, which is based on Theorem Proving (TP). TP, for
610 % instance Isabelle and Coq, is a technology which requires each fact
611 % and each action justified by formal logic. Pushed by demands for
612 % \textit{proven} correctness of safety-critical software TP advances
613 % into software engineering; from these advancements computer
614 % mathematics benefits in general, and math education in particular. Two
615 % features of TP are immediately beneficial for learning:
617 % \paragraph{TP have knowledge in human readable format,} that is in
618 % standard predicate calculus. TP following the LCF-tradition have that
619 % knowledge down to the basic definitions of set, equality,
620 % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
621 % following the typical deductive development of math, natural numbers
622 % are defined and their properties
623 % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
624 % etc. Present knowledge mechanized in TP exceeds high-school
625 % mathematics by far, however by knowledge required in software
626 % technology, and not in other engineering sciences.
628 % \paragraph{TP can model the whole problem solving process} in
629 % mathematical problem solving {\em within} a coherent logical
630 % framework. This is already being done by three projects, by
631 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
633 % Having the whole problem solving process within a logical coherent
634 % system, such a design guarantees correctness of intermediate steps and
635 % of the result (which seems essential for math software); and the
636 % second advantage is that TP provides a wealth of theories which can be
637 % exploited for mechanizing other features essential for educational
640 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
642 % One essential feature for educational software is feedback to user
643 % input and assistance in coming to a solution.
645 % \paragraph{Checking user input} by ATP during stepwise problem solving
646 % is being accomplished by the three projects mentioned above
647 % exclusively. They model the whole problem solving process as mentioned
648 % above, so all what happens between formalized assumptions (or formal
649 % specification) and goal (or fulfilled postcondition) can be
650 % mechanized. Such mechanization promises to greatly extend the scope of
651 % educational software in stepwise problem solving.
653 % \paragraph{NSG (Next step guidance)} comprises the system's ability to
654 % propose a next step; this is a challenge for TP: either a radical
655 % restriction of the search space by restriction to very specific
656 % problem classes is required, or much care and effort is required in
657 % designing possible variants in the process of problem solving
658 % \cite{proof-strategies-11}.
660 % Another approach is restricted to problem solving in engineering
661 % domains, where a problem is specified by input, precondition, output
662 % and postcondition, and where the postcondition is proven by ATP behind
663 % the scenes: Here the possible variants in the process of problem
664 % solving are provided with feedback {\em automatically}, if the problem
665 % is described in a TP-based programing language: \cite{plmms10} the
666 % programmer only describes the math algorithm without caring about
667 % interaction (the respective program is functional and even has no
668 % input or output statements!); interaction is generated as a
669 % side-effect by the interpreter --- an efficient separation of concern
670 % between math programmers and dialog designers promising application
671 % all over engineering disciplines.
674 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
675 % Authoring new mathematics knowledge in {{\sisac}} can be compared with
676 % ``application programing'' of engineering problems; most of such
677 % programing uses CAS-based programing languages (CAS = Computer Algebra
678 % Systems; e.g. Mathematica's or Maple's programing language).
680 % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
681 % \cite{plmms10} for describing how to construct a solution to an
682 % engineering problem and for calling equation solvers, integration,
683 % etc~\footnote{Implementation of CAS-like functionality in TP is not
684 % primarily concerned with efficiency, but with a didactic question:
685 % What to decide for: for high-brow algorithms at the state-of-the-art
686 % or for elementary algorithms comprehensible for students?} within TP;
687 % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
688 % are impossible for CAS which have no logics underlying.
690 % \subparagraph{Authoring is perfect} by writing such TP based programs;
691 % the application programmer is not concerned with interaction or with
692 % user guidance: this is concern of a novel kind of program interpreter
693 % called Lucas-Interpreter. This interpreter hands over control to a
694 % dialog component at each step of calculation (like a debugger at
695 % breakpoints) and calls automated TP to check user input following
696 % personalized strategies according to a feedback module.
698 % However ``application programing with TP'' is not done with writing a
699 % program: according to the principles of TP, each step must be
700 % justified. Such justifications are given by theorems. So all steps
701 % must be related to some theorem, if there is no such theorem it must
702 % be added to the existing knowledge, which is organized in so-called
703 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
704 % Isabelle comprises a mechanism (called ``axiomatization''), which
705 % allows to omit proofs. Such a theorem is shown in
706 % Example~\ref{eg:neuper1}.
708 The running example requires to determine the inverse ${\cal Z}$-transform
709 for a class of functions. The domain of Signal Processing
710 is accustomed to specific notation for the resulting functions, which
711 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
712 function, $n$ is the argument and the brackets indicate that the
713 arguments are discrete. Surprisingly, Isabelle accepts the rules for
714 $z^{-1}$ in this traditional notation~\footnote{Isabelle
715 experts might be particularly surprised, that the brackets do not
716 cause errors in typing (as lists).}:
720 {\footnotesize\begin{tabbing}
721 123\=123\=123\=123\=\kill
723 01\>axiomatization where \\
724 02\>\> rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\
725 03\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\
726 04\>\> rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\
727 05\>\> rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\
728 06\>\> rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\
729 07\>\> rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''
733 These 6 rules can be used as conditional rewrite rules, depending on
734 the respective convergence radius. Satisfaction from accordance with traditional
735 notation contrasts with the above word {\em axiomatization}: As TP-based, the
736 programming language expects these rules as {\em proved} theorems, and
737 not as axioms implemented in the above brute force manner; otherwise
738 all the verification efforts envisaged (like proof of the
739 post-condition, see below) would be meaningless.
741 Isabelle provides a large body of knowledge, rigorously proved from
742 the basic axioms of mathematics~\footnote{This way of rigorously
743 deriving all knowledge from first principles is called the
744 LCF-paradigm in TP.}. In the case of the ${\cal Z}$-transform the most advanced
745 knowledge can be found in the theories on Multivariate
746 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
747 building up knowledge such that a proof for the above rules would be
748 reasonably short and easily comprehensible, still requires lots of
749 work (and is definitely out of scope of our case study).
751 %REMOVED DUE TO SPACE CONSTRAINTS
752 %At the state-of-the-art in mechanization of knowledge in engineering
753 %sciences, the process does not stop with the mechanization of
754 %mathematics traditionally used in these sciences. Rather, ``Formal
755 %Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
756 %description of physical items. Signal Processing, for instance is
757 %concerned with physical devices for signal acquisition and
758 %reconstruction, which involve measuring a physical signal, storing it,
759 %and possibly later rebuilding the original signal or an approximation
760 %thereof. For digital systems, this typically includes sampling and
761 %quantization; devices for signal compression, including audio
762 %compression, image compression, and video compression, etc. ``Domain
763 %engineering''\cite{db:dom-eng} is concerned with {\em specification}
764 %of these devices' components and features; this part in the process of
765 %mechanization is only at the beginning in domains like Signal
768 %TP-based programming, concern of this paper, is determined to
769 %add ``algorithmic knowledge'' to the mechanised body of knowledge.
770 %% in Fig.\ref{fig:mathuni} on
771 %% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
772 %% starts with a formal {\em specification} of the problem to be solved.
775 %% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
776 %% \caption{The three-dimensional universe of mathematics knowledge}
777 %% \label{fig:mathuni}
780 %% The language for both axes is defined in the axis at the bottom, deductive
781 %% knowledge, in {\sisac} represented by Isabelle's theories.
783 \subsection{Preparation of Simplifiers for the Program}\label{simp}
785 All evaluation in the prototype's Lucas-Interpreter is done by term rewriting on
786 Isabelle's terms, see \S\ref{meth} below; in this section some of respective
787 preparations are described. In order to work reliably with term rewriting, the
788 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
789 then they are called (canonical) simplifiers. These properties do not go without
790 saying, their establishment is a difficult task for the programmer; this task is
791 not yet supported in the prototype.
793 The prototype rewrites using theorems only. Axioms which are theorems as well
794 have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
795 assemble them in a rule-set and apply them in ML as follows:
799 01 val inverse_z = Rls
800 02 {id = "inverse_z",
801 03 rew_ord = dummy_ord,
803 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
804 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
805 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
810 \noindent The items, line by line, in the above record have the following purpose:
812 \item[01..02] the ML-value \textit{inverse\_z} stores it's identifier
813 as a string for ``reflection'' when switching between the language
814 layers of Isabelle/ML (like in the Lucas-Interpreter) and
815 Isabelle/Isar (like in the example program on p.\pageref{s:impl} on
818 \item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
819 \textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
820 (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
821 and (b) the assumptions of the \textit{rules} need not be evaluated
822 (they just go into the context during rewriting).
824 \item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
825 also ML-functions (\S\ref{funs}) can come into this list as shown in
826 \S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm}
827 and \textit{Calc} respectively; for the purpose of reflection both
828 contain their identifiers.
830 \item[08..09] are error-patterns not discussed here and \textit{scr}
831 is prepared to get a program, automatically generated by {\sisac} for
832 producing intermediate rewrites when requested by the user.
836 %OUTCOMMENTED DUE TO SPACE RESTRICTIONS
837 % \noindent It is advisable to immediately test rule-sets; for that
838 % purpose an appropriate term has to be created; \textit{parse} takes a
839 % context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
840 % Z}^{-1}$) and creates a term:
845 % 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
847 % 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1",
848 % 05 "RealDef.real => RealDef.real => RealDef.real") $
849 % 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...)
852 % \noindent The internal representation of the term, as required for
853 % rewriting, consists of \textit{Const}ants, a pair of a string
854 % \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
855 % \textit{Free} and the respective constructor \textit{\$}. Now the
856 % term can be rewritten by the rule-set \textit{inverse\_z}:
861 % 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
865 % 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
866 % 07 val it = "|| z || > 1 & || z || > </alpha>" : string
869 % \noindent The resulting term \textit{t} and the assumptions
870 % \textit{asm} are converted to readable strings by \textit{term2str}
871 % and \textit{terms2str}.
873 \subsection{Preparation of ML-Functions}\label{funs}
874 Some functionality required in programming, cannot be accomplished by
875 rewriting. So the prototype has a mechanism to call functions within
876 the rewrite-engine: certain redexes in Isabelle terms call these
877 functions written in SML~\cite{pl:milner97}, the implementation {\em
878 and} meta-language of Isabelle. The programmer has to use this
881 In the running example's program on p.\pageref{s:impl} the lines {\rm
882 05} and {\rm 06} contain such functions; we go into the details with
883 \textit{argument\_in X\_z;}. This function fetches the argument from a
884 function application: Line {\rm 03} in the example calculation on
885 p.\pageref{exp-calc} is created by line {\rm 06} of the example
886 program on p.\pageref{s:impl} where the program's environment assigns
887 the value \textit{X z} to the variable \textit{X\_z}; so the function
888 shall extract the argument \textit{z}.
890 \medskip In order to be recognised as a function constant in the
891 program source the constant needs to be declared in a theory, here in
892 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
893 the context \textit{ctxt} of that theory:
898 02 argument'_in :: "real => real" ("argument'_in _" 10)
901 %^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
902 %^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
903 %^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
904 %^3.2^ \end{verbatim}}
906 %^3.2^ \noindent Parsing produces a term \texttt{t} in internal
907 %^3.2^ representation~\footnote{The attentive reader realizes the
908 %^3.2^ differences between interal and extermal representation even in the
909 %^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
910 %^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
911 %^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
913 The function body below is implemented directly in SML,
914 i.e in an \texttt{ML \{* *\}} block; the function definition provides
915 a unique prefix \texttt{eval\_} to the function name:
920 02 fun eval_argument_in _
921 03 "Build_Inverse_Z_Transform.argument'_in"
922 04 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
923 05 if is_Free arg (*could be something to be simplified before*)
924 06 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
926 08 | eval_argument_in _ _ _ _ = NONE;
930 \noindent The function body creates either \texttt{NONE}
931 telling the rewrite-engine to search for the next redex, or creates an
932 ad-hoc theorem for rewriting, thus the programmer needs to adopt many
933 technicalities of Isabelle, for instance, the \textit{Trueprop}
936 \bigskip This sub-task particularly sheds light on basic issues in the
937 design of a programming language, the integration of differential language
938 layers, the layer of Isabelle/Isar and Isabelle/ML.
940 Another point of improvement for the prototype is the rewrite-engine: The
941 program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
944 {\small\it\label{s:impl}
946 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
947 \>{\rm 05/06}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
950 \noindent because nested function calls would require creating redexes
951 inside-out; however, the prototype's rewrite-engine only works top down
952 from the root of a term down to the leaves.
954 How all these technicalities are to be checked in the prototype is
955 shown in \S\ref{flow-prep} below.
957 % \paragraph{Explicit Problems} require explicit methods to solve them, and within
958 % this methods we have some explicit steps to do. This steps can be unique for
959 % a special problem or refindable in other problems. No mather what case, such
960 % steps often require some technical functions behind. For the solving process
961 % of the Inverse Z Transformation and the corresponding partial fraction it was
962 % neccessary to build helping functions like \texttt{get\_denominator},
963 % \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
964 % to filter the denominator or numerator out of a fraction, last one helps us to
965 % get to know the bound variable in a equation.
967 % By taking \texttt{get\_denominator} as an example, we want to explain how to
968 % implement new functions into the existing system and how we can later use them
971 % \subsubsection{Find a place to Store the Function}
973 % The whole system builds up on a well defined structure of Knowledge. This
974 % Knowledge sets up at the Path:
975 % \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
976 % For implementing the Function \texttt{get\_denominator} (which let us extract
977 % the denominator out of a fraction) we have choosen the Theory (file)
978 % \texttt{Rational.thy}.
980 % \subsubsection{Write down the new Function}
982 % In upper Theory we now define the new function and its purpose:
984 % get_denominator :: "real => real"
986 % This command tells the machine that a function with the name
987 % \texttt{get\_denominator} exists which gets a real expression as argument and
988 % returns once again a real expression. Now we are able to implement the function
989 % itself, upcoming example now shows the implementation of
990 % \texttt{get\_denominator}.
993 % \label{eg:getdenom}
997 % 02 *("get_denominator",
998 % 03 * ("Rational.get_denominator", eval_get_denominator ""))
1000 % 05 fun eval_get_denominator (thmid:string) _
1001 % 06 (t as Const ("Rational.get_denominator", _) $
1002 % 07 (Const ("Rings.inverse_class.divide", _) $num
1004 % 09 SOME (mk_thmid thmid ""
1005 % 10 (Print_Mode.setmp []
1006 % 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1007 % 12 Trueprop $ (mk_equality (t, denom)))
1008 % 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
1011 % Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
1012 % there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
1014 % into its two parts (\texttt{\$num \$denom}). The lines before are additionals
1015 % commands for declaring the function and the lines after are modeling and
1016 % returning a real variable out of \texttt{\$denom}.
1018 % \subsubsection{Add a test for the new Function}
1020 % \paragraph{Everytime when adding} a new function it is essential also to add
1021 % a test for it. Tests for all functions are sorted in the same structure as the
1022 % knowledge it self and can be found up from the path:
1023 % \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
1024 % This tests are nothing very special, as a first prototype the functionallity
1025 % of a function can be checked by evaluating the result of a simple expression
1026 % passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
1027 % \textit{just} created function \texttt{get\_denominator}.
1030 % \label{eg:getdenomtest}
1033 % 01 val thy = @{theory Isac};
1034 % 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1035 % 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1036 % 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1037 % 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
1040 % \begin{description}
1041 % \item[01] checks if the proofer set up on our {\sisac{}} System.
1042 % \item[02] passes a simple expression (fraction) to our suddenly created
1044 % \item[04] checks if the resulting variable is the correct one (in this case
1045 % ``b'' the denominator) and returns.
1046 % \item[05] handels the error case and reports that the function is not able to
1047 % solve the given problem.
1050 \subsection{Specification of the Problem}\label{spec}
1051 %WN <--> \chapter 7 der Thesis
1052 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1054 Mechanical treatment requires to translate a textual problem
1055 description like in Fig.\ref{fig-interactive} on
1056 p.\pageref{fig-interactive} into a {\em formal} specification. The
1057 formal specification of the running example could look like is this
1058 ~\footnote{The ``TODO'' in the postcondition indicates, that postconditions
1059 are not yet handled in the prototype; in particular, the postcondition, i.e.
1060 the correctness of the result is not yet automatically proved.}:
1062 %WN Hier brauchen wir die Spezifikation des 'running example' ...
1063 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1064 %JR der post condition - die existiert für uns ja eigentlich nicht aka
1065 %JR haben sie bis jetzt nicht beachtet WN...
1066 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1070 {\small\begin{tabbing}
1071 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1074 \> \>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}\}$\\
1075 \>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
1076 \>\>output \>: stepResponse $x[n]$ \\
1077 \>\>postcond \>: TODO
1080 %JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt"
1083 % Defining the postcondition requires a high amount mathematical
1084 % knowledge, the difficult part in our case is not to set up this condition
1085 % nor it is more to define it in a way the interpreter is able to handle it.
1086 % Due the fact that implementing that mechanisms is quite the same amount as
1087 % creating the programm itself, it is not avaible in our prototype.
1088 % \label{rm:postcond}
1091 The implementation of the formal specification in the present
1092 prototype, still bar-bones without support for authoring, is done
1094 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1096 {\footnotesize\label{exp-spec}
1099 01 store_specification
1100 02 (prepare_specification
1101 03 "pbl_SP_Ztrans_inv"
1104 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1105 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1106 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1107 09 ("#Find" , ["stepResponse n_eq"]),
1108 10 ("#Post" , [" TODO "])])
1111 13 [["SignalProcessing","Z_Transform","Inverse"]]);
1115 Although the above details are partly very technical, we explain them
1116 in order to document some intricacies of TP-based programming in the
1117 present state of the {\sisac} prototype:
1119 \item[01..02]\textit{store\_specification:} stores the result of the
1120 function \textit{prep\_specification} in a global reference
1121 \textit{Unsynchronized.ref}, which causes principal conflicts with
1122 Isabelle's asynchronous document model~\cite{Wenzel-11:doc-orient} and
1123 parallel execution~\cite{Makarius-09:parall-proof} and is under
1124 reconstruction already.
1126 \textit{prep\_specification:} translates the specification to an internal format
1127 which allows efficient processing; see for instance line {\rm 07}
1129 \item[03..04] are a unique identifier for the specification within {\sisac}
1130 and the ``mathematics author'' holding the copy-rights.
1131 \item[05] is the Isabelle \textit{theory} required to parse the
1132 specification in lines {\rm 07..10}.
1133 \item[06] is a key into the tree of all specifications as presented to
1134 the user (where some branches might be hidden by the dialogue
1136 \item[07..10] are the specification with input, pre-condition, output
1137 and post-condition respectively; note that the specification contains
1138 variables to be instantiated with concrete values for a concrete problem ---
1139 thus the specification actually captures a class of problems. The post-condition is not handled in
1140 the prototype presently.
1141 \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
1142 rewriting determined by rule-sets.
1143 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1144 problem associated to a function from Computer Algebra (like an
1145 equation solver) which is not the case here.
1146 \item[13] is a list of methods solving the specified problem (here
1147 only one list item) represented analogously to {\rm 06}.
1151 %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1154 % {guh : guh, (*unique within this isac-knowledge*)
1155 % mathauthors: string list, (*copyright*)
1156 % init : pblID, (*to start refinement with*)
1157 % thy : theory, (* which allows to compile that pbt
1158 % TODO: search generalized for subthy (ref.p.69*)
1159 % (*^^^ WN050912 NOT used during application of the problem,
1160 % because applied terms may be from 'subthy' as well as from super;
1161 % thus we take 'maxthy'; see match_ags !*)
1162 % cas : term option,(*'CAS-command'*)
1163 % prls : rls, (* for preds in where_*)
1164 % where_: term list, (* where - predicates*)
1166 % (*this is the model-pattern;
1167 % it contains "#Given","#Where","#Find","#Relate"-patterns
1168 % for constraints on identifiers see "fun cpy_nam"*)
1169 % met : metID list}; (* methods solving the pbt*)
1171 %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1172 %WN oben selbst geschrieben.
1177 %WN das w"urde ich in \sec\label{progr} verschieben und
1178 %WN das SubProblem partial fractions zum Erkl"aren verwenden.
1179 % Such a specification is checked before the execution of a program is
1180 % started, the same applies for sub-programs. In the following example
1181 % (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1185 % \label{eg:subprob}
1187 % {\ttfamily \begin{tabbing}
1188 % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
1189 % ``\>\>[linear,univariate,equation,test],'' \\
1190 % ``\>\>[Test,solve\_linear])'' \\
1191 % ``\>[BOOL equ, REAL z])'' \\
1195 % \noindent If a program requires a result which has to be
1196 % calculated first we can use a subproblem to do so. In our specific
1197 % case we wanted to calculate the zeros of a fraction and used a
1198 % subproblem to calculate the zeros of the denominator polynom.
1203 \subsection{Implementation of the Method}\label{meth}
1204 A method collects all data required to interpret a certain program by
1205 Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
1206 the running example is embedded on the last line in the following method:
1207 %The methods represent the different ways a problem can be solved. This can
1208 %include mathematical tactics as well as tactics taught in different courses.
1209 %Declaring the Method itself gives us the possibilities to describe the way of
1210 %calculation in deep, as well we get the oppertunities to build in different
1218 03 "SP_InverseZTransformation_classic"
1221 06 ( ["SignalProcessing", "Z_Transform", "Inverse"],
1222 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1223 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1224 09 ("#Find" , ["stepResponse n_eq"]),
1232 \noindent The above code stores the whole structure analogously to a
1233 specification as described above:
1235 \item[01..06] are identical to those for the example specification on
1236 p.\pageref{exp-spec}.
1238 \item[07..09] show something looking like the specification; this is a
1239 {\em guard}: as long as not all \textit{Given} items are present and
1240 the \textit{Pre}-conditions is not true, interpretation of the program
1243 \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
1244 \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
1245 \textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
1246 \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}
1247 and (c) is required for the derivation-machinery checking user-input formulas.
1249 \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}.
1251 The many rule-sets above cause considerable efforts for the
1252 programmers, in particular, because there are no tools for checking
1253 essential features of rule-sets.
1255 % is again very technical and goes hard in detail. Unfortunataly
1256 % most declerations are not essential for a basic programm but leads us to a huge
1257 % range of powerful possibilities.
1259 % \begin{description}
1260 % \item[01..02] stores the method with the given name into the system under a global
1262 % \item[03] specifies the topic within which context the method can be found.
1263 % \item[04..05] as the requirements for different methods can be deviant we
1264 % declare what is \emph{given} and and what to \emph{find} for this specific method.
1265 % The code again helds on the topic of the case studie, where the inverse
1266 % z-transformation does a switch between a term describing a electrical filter into
1267 % its step response. Also the datatype has to be declared (bool - due the fact that
1268 % we handle equations).
1269 % \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
1270 % theorem of it is used for rewriting one single step.
1271 % \item[07] \texttt{rls} is the currently used ruleset for this method. This set
1272 % has already been defined before.
1273 % \item[08] we would have the possiblitiy to add this method to a predefined tree of
1274 % calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
1276 % \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
1278 % \item[10] \emph{predicates ruleset} can be used to indicates predicates within
1280 % \item[11] The \emph{check ruleset} summarizes rules for checking formulas
1282 % \item[12] \emph{error patterns} which are expected in this kind of method can be
1283 % pre-specified to recognize them during the method.
1284 % \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
1285 % of the specific method.
1286 % \item[14] for this code snipset we don't specify the programm itself and keep it
1287 % empty. Follow up \S\ref{progr} for informations on how to implement this
1288 % \textit{main} part.
1291 \subsection{Implementation of the TP-based Program}\label{progr}
1292 So finally all the prerequisites are described and the final task can
1293 be addressed. The program below comes back to the running example: it
1294 computes a solution for the problem from Fig.\ref{fig-interactive} on
1295 p.\pageref{fig-interactive}. The reader is reminded of
1296 \S\ref{PL-isab}, the introduction of the programming language:
1298 {\footnotesize\it\label{s:impl}
1300 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1301 \>{\rm 00}\>ML \{*\\
1302 \>{\rm 00}\>val program =\\
1303 \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1304 \>{\rm 02}\>\> {\tt let} \\
1305 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1306 \>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
1307 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1308 \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1309 \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1310 \>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
1311 %\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
1312 \>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1313 \>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1314 \>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@ \\
1315 \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1316 \>{\rm 13}\>\> {\tt in } \\
1317 \>{\rm 14}\>\>\> X'\_eq"\\
1320 % ORIGINAL FROM Inverse_Z_Transform.thy
1321 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1322 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1323 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1324 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1325 % " (zzz::real) = argument_in X'_z; "^(* z *)
1326 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1328 % " (pbz::real) = (SubProblem (Isac', "^(**)
1329 % " [partial_fraction,rational,simplification], "^
1330 % " [simplification,of_rationals,to_partial_fraction]) "^
1331 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1333 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1334 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1335 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1336 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1337 % " 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]*)
1338 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1339 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1340 The program is represented as a string and part of the method in
1341 \S\ref{meth}. As mentioned in \S\ref{PL} the program is purely
1342 functional and lacks any input statements and output statements. So
1343 the steps of calculation towards a solution (and interactive tutoring
1344 in step-wise problem solving) are created as a side-effect by
1345 Lucas-Interpretation. The side-effects are triggered by the tactics
1346 \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
1347 \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1348 {\rm 12} respectively. These tactics produce the respective lines in the
1349 calculation on p.\pageref{flow-impl}.
1351 The above lines {\rm 05, 06} do not contain a tactics, so they do not
1352 immediately contribute to the calculation on p.\pageref{flow-impl};
1353 rather, they compute actual arguments for the \texttt{SubProblem} in
1354 line {\rm 09}~\footnote{The tactics also are break-points for the
1355 interpreter, where control is handed over to the user in interactive
1356 tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
1358 \medskip The above program also indicates the dominant role of interactive
1359 selection of knowledge in the three-dimensional universe of
1360 mathematics. The \texttt{SubProblem} in the above lines
1361 {\rm 07..09} is more than a function call with the actual arguments
1362 \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
1366 \item the theory, in the example \textit{Isac} because different
1367 methods can be selected in Pt.3 below, which are defined in different
1368 theories with \textit{Isac} collecting them.
1369 \item the specification identified by \textit{[partial\_fraction,
1370 rational, simplification]} in the tree of specifications; this
1371 specification is analogous to the specification of the main program
1372 described in \S\ref{spec}; the problem is to find a ``partial fraction
1373 decomposition'' for a univariate rational polynomial.
1374 \item the method in the above example is \textit{[ ]}, i.e. empty,
1375 which supposes the interpreter to select one of the methods predefined
1376 in the specification, for instance in line {\rm 13} in the running
1377 example's specification on p.\pageref{exp-spec}~\footnote{The freedom
1378 (or obligation) for selection carries over to the student in
1379 interactive tutoring.}.
1382 The program code, above presented as a string, is parsed by Isabelle's
1383 parser --- the program is an Isabelle term. This fact is expected to
1384 simplify verification tasks in the future; on the other hand, this
1385 fact causes troubles in error detection which are discussed as part
1386 of the work-flow in the subsequent section.
1388 \section{Work-flow of Programming in the Prototype}\label{workflow}
1389 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
1390 step forward for interactive theory and proof development. The
1391 {\sisac}-prototype re-uses this IDE as a programming environment. The
1392 experiences from this re-use show, that the essential components are
1393 available from Isabelle/jEdit. However, additional tools and features
1394 are required to achieve acceptable usability.
1396 So notable experiences are reported here, also as a requirement
1397 capture for further development of TP-based languages and respective
1400 \subsection{Preparations and Trials}\label{flow-prep}
1401 The many sub-tasks to be accomplished {\em before} the first line of
1402 program code can be written and tested suggest an approach which
1403 step-wise establishes the prerequisites. The case study underlying
1404 this paper~\cite{jrocnik-bakk} documents the approach in a separate
1406 \textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
1407 II in the study comprises this theory, \LaTeX ed from the theory by
1408 use of Isabelle's document preparation system. This paper resembles
1409 the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
1410 implementation work involves several iterations.
1412 \bigskip For instance, only the last step, implementing the program
1413 described in \S\ref{meth}, reveals details required. Let us assume,
1414 this is the ML-function \textit{argument\_in} required in line {\rm 06}
1415 of the example program on p.\pageref{s:impl}; how this function needs
1416 to be implemented in the prototype has been discussed in \S\ref{funs}
1419 Now let us assume, that calling this function from the program code
1420 does not work; so testing this function is required in order to find out
1421 the reason: type errors, a missing entry of the function somewhere or
1422 even more nasty technicalities \dots
1427 02 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1428 03 val SOME (str, t') = eval_argument_in ""
1429 04 "Build_Inverse_Z_Transform.argument'_in" t 0;
1432 07 val it = "(argument_in X z) = z": string\end{verbatim}}
1434 \noindent So, this works: we get an ad-hoc theorem, which used in
1435 rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
1436 reduction and create a rule-set \texttt{rls} for that purpose:
1441 02 val rls = append_rls "test" e_rls
1442 03 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1443 04 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1445 06 val t' = Free ("z", "RealDef.real"): term
1446 07 val asm = []: term list\end{verbatim}}
1448 \noindent The resulting term \texttt{t'} is \texttt{Free ("z",
1449 "RealDef.real")}, i.e the variable \texttt{z}, so all is
1450 perfect. Probably we have forgotten to store this function correctly~?
1451 We review the respective \texttt{calclist} (again an
1452 \textit{Unsynchronized.ref} to be removed in order to adjust to
1453 Isabelle/Isar's asynchronous document model):
1457 01 calclist:= overwritel (! calclist,
1459 03 ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1461 05 ]);\end{verbatim}}
1463 \noindent The entry is perfect. So what is the reason~? Ah, probably there
1464 is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1465 right, the function \texttt{argument\_in} is not contained in the respective
1466 rule-set \textit{srls} \dots this just as an example of the intricacies in
1467 debugging a program in the present state of the prototype.
1469 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1470 Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
1471 usually developed within several iterations, the program can be
1472 assembled; on p.\pageref{s:impl} there is the complete program of the
1475 The completion of this program required efforts for several weeks
1476 (after some months of familiarisation with {\sisac}), caused by the
1477 abundance of intricacies indicated above. Also writing the program is
1478 not pleasant, given Isabelle/Isar/ without add-ons for
1479 programming. Already writing and parsing a few lines of program code
1480 is a challenge: the program is an Isabelle term; Isabelle's parser,
1481 however, is not meant for huge terms like the program of the running
1482 example. So reading out the specific error (usually type errors) from
1483 Isabelle's message is difficult.
1485 \medskip Testing the evaluation of the program has to rely on very
1486 simple tools. Step-wise execution is modeled by a function
1487 \texttt{me}, short for mathematics-engine~\footnote{The interface used
1488 by the front-end which created the calculation on
1489 p.\pageref{fig-interactive} is different from this function}:
1490 %the following is a simplification of the actual function
1495 02 val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}}
1497 \noindent This function takes as arguments a tactic \texttt{tac} which
1498 determines the next step, the step applied to the interpreter-state
1499 \texttt{ctree * pos} as last argument taken. The interpreter-state is
1500 a pair of a tree \texttt{ctree} representing the calculation created
1501 (see the example below) and a position \texttt{pos} in the
1502 calculation. The function delivers a quadruple, beginning with the new
1503 formula \texttt{mout} and the next tactic followed by the new
1506 This function allows to stepwise check the program:
1508 {\footnotesize\label{ml-check-program}
1512 03 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1513 04 "stepResponse (x[n::real]::bool)"];
1516 07 ["Inverse", "Z_Transform", "SignalProcessing"],
1517 08 ["SignalProcessing","Z_Transform","Inverse"]);
1518 09 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1519 10 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1520 11 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1521 12 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1525 \noindent Several dozens of calls for \texttt{me} are required to
1526 create the lines in the calculation below (including the sub-problems
1527 not shown). When an error occurs, the reason might be located
1528 many steps before: if evaluation by rewriting, as done by the prototype,
1529 fails, then first nothing happens --- the effects come later and
1530 cause unpleasant checks.
1532 The checks comprise watching the rewrite-engine for many different
1533 kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
1534 particular the environment and the context at the states position ---
1535 all checks have to rely on simple functions accessing the
1536 \texttt{ctree}. So getting the calculation below (which resembles the
1537 calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
1538 is the result of several weeks of development:
1540 {\small\it\label{exp-calc}
1542 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1543 \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1544 \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
1545 \>{\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}\\
1546 \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
1547 \>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
1548 \>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
1549 \>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
1550 \>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
1551 \>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
1552 \>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
1553 \> \>\>\>\> \_\_\_ \`- - -\\
1554 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1555 \>{\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)}\\
1556 \>{\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 }\\
1557 \>{\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}\\
1558 \>{\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}}
1560 The tactics on the right margin of the above calculation are those in
1561 the program on p.\pageref{s:impl} which create the respective formulas
1563 % ORIGINAL FROM Inverse_Z_Transform.thy
1564 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1565 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1566 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1567 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1568 % " (zzz::real) = argument_in X'_z; "^(* z *)
1569 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1571 % " (pbz::real) = (SubProblem (Isac', "^(**)
1572 % " [partial_fraction,rational,simplification], "^
1573 % " [simplification,of_rationals,to_partial_fraction]) "^
1574 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1576 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1577 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1578 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1579 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1580 % " 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]*)
1581 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1582 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1584 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1585 Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
1586 and the knowledge accumulated in it can be distributed to appropriate
1587 theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
1588 sub-problem accomplishing the partial fraction decomposition to
1589 \textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
1590 internals, this kind of distribution is not trivial. For instance, the
1591 function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
1592 string with the theory it has been defined in, so this string needs to
1593 be updated from \texttt{Build\_Inverse\_Z\_Transform} to
1594 \texttt{Atools} if that function is transferred to theory
1595 \textit{Atools.thy}.
1597 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.
1598 This process is also rather bare-bones without authoring tools and is
1599 described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
1602 % -------------------------------------------------------------------
1604 % Material, falls noch Platz bleibt ...
1606 % -------------------------------------------------------------------
1609 % \subsubsection{Trials on Notation and Termination}
1611 % \paragraph{Technical notations} are a big problem for our piece of software,
1612 % but the reason for that isn't a fault of the software itself, one of the
1613 % troubles comes out of the fact that different technical subtopics use different
1614 % symbols and notations for a different purpose. The most famous example for such
1615 % a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1616 % math). In the specific part of signal processing one of this notation issues is
1617 % the use of brackets --- we use round brackets for analoge signals and squared
1618 % brackets for digital samples. Also if there is no problem for us to handle this
1619 % fact, we have to tell the machine what notation leads to wich meaning and that
1620 % this purpose seperation is only valid for this special topic - signal
1622 % \subparagraph{In the programming language} itself it is not possible to declare
1623 % fractions, exponents, absolutes and other operators or remarks in a way to make
1624 % them pretty to read; our only posssiblilty were ASCII characters and a handfull
1625 % greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1627 % With the upper collected knowledge it is possible to check if we were able to
1628 % donate all required terms and expressions.
1630 % \subsubsection{Definition and Usage of Rules}
1632 % \paragraph{The core} of our implemented problem is the Z-Transformation, due
1633 % the fact that the transformation itself would require higher math which isn't
1634 % yet avaible in our system we decided to choose the way like it is applied in
1635 % labratory and problem classes at our university - by applying transformation
1636 % rules (collected in transformation tables).
1637 % \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1638 % use of axiomatizations like shown in Example~\ref{eg:ruledef}
1641 % \label{eg:ruledef}
1644 % axiomatization where
1645 % rule1: ``1 = $\delta$[n]'' and
1646 % rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1647 % rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1651 % This rules can be collected in a ruleset and applied to a given expression as
1652 % follows in Example~\ref{eg:ruleapp}.
1656 % \label{eg:ruleapp}
1658 % \item Store rules in ruleset:
1660 % val inverse_Z = append_rls "inverse_Z" e_rls
1661 % [ Thm ("rule1",num_str @{thm rule1}),
1662 % Thm ("rule2",num_str @{thm rule2}),
1663 % Thm ("rule3",num_str @{thm rule3})
1665 % \item Define exression:
1667 % val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1668 % \item Apply ruleset:
1670 % val SOME (sample_term', asm) =
1671 % rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1675 % The use of rulesets makes it much easier to develop our designated applications,
1676 % but the programmer has to be careful and patient. When applying rulesets
1677 % two important issues have to be mentionend:
1678 % \subparagraph{How often} the rules have to be applied? In case of
1679 % transformations it is quite clear that we use them once but other fields
1680 % reuqire to apply rules until a special condition is reached (e.g.
1681 % a simplification is finished when there is nothing to be done left).
1682 % \subparagraph{The order} in which rules are applied often takes a big effect
1683 % and has to be evaluated for each purpose once again.
1685 % In our special case of Signal Processing and the rules defined in
1686 % Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1687 % constants. After this step has been done it no mather which rule fit's next.
1689 % \subsubsection{Helping Functions}
1691 % \paragraph{New Programms require,} often new ways to get through. This new ways
1692 % means that we handle functions that have not been in use yet, they can be
1693 % something special and unique for a programm or something famous but unneeded in
1694 % the system yet. In our dedicated example it was for example neccessary to split
1695 % a fraction into numerator and denominator; the creation of such function and
1696 % even others is described in upper Sections~\ref{simp} and \ref{funs}.
1698 % \subsubsection{Trials on equation solving}
1699 % %simple eq and problem with double fractions/negative exponents
1700 % \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
1701 % equations degree one and two. Solving equations in the first degree is no
1702 % problem, wether for a student nor for our machine; but even second degree
1703 % equations can lead to big troubles. The origin of this troubles leads from
1704 % the build up process of our equation solving functions; they have been
1705 % implemented some time ago and of course they are not as good as we want them to
1706 % be. Wether or not following we only want to show how cruel it is to build up new
1707 % work on not well fundamentials.
1708 % \subparagraph{A simple equation solving,} can be set up as shown in the next
1715 % ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
1719 % val (dI',pI',mI') =
1721 % ["abcFormula","degree_2","polynomial","univariate","equation"],
1722 % ["no_met"]);\end{verbatim}
1725 % Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
1726 % a short overview on the commands; at first we set up the equation and tell the
1727 % machine what's the bound variable and where to store the solution. Second step
1728 % is to define the equation type and determine if we want to use a special method
1729 % to solve this type.) Simple checks tell us that the we will get two results for
1730 % this equation and this results will be real.
1731 % So far it is easy for us and for our machine to solve, but
1732 % mentioned that a unvariate equation second order can have three different types
1733 % of solutions it is getting worth.
1734 % \subparagraph{The solving of} all this types of solutions is not yet supported.
1735 % Luckily it was needed for us; but something which has been needed in this
1736 % context, would have been the solving of an euation looking like:
1737 % $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
1738 % before (remember that befor it was no problem to handle for the machine) but
1739 % now, after a simple equivalent transformation, we are not able to solve
1741 % \subparagraph{Error messages} we get when we try to solve something like upside
1742 % were very confusing and also leads us to no special hint about a problem.
1743 % \par The fault behind is, that we have no well error handling on one side and
1744 % no sufficient formed equation solving on the other side. This two facts are
1745 % making the implemention of new material very difficult.
1747 % \subsection{Formalization of missing knowledge in Isabelle}
1749 % \paragraph{A problem} behind is the mechanization of mathematic
1750 % theories in TP-bases languages. There is still a huge gap between
1751 % these algorithms and this what we want as a solution - in Example
1752 % Signal Processing.
1758 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1761 % \noindent A very simple example on this what we call gap is the
1762 % simplification above. It is needles to say that it is correct and also
1763 % Isabelle for fills it correct - \emph{always}. But sometimes we don't
1764 % want expand such terms, sometimes we want another structure of
1765 % them. Think of a problem were we now would need only the coefficients
1766 % of $X$ and $Y$. This is what we call the gap between mechanical
1767 % simplification and the solution.
1772 % \paragraph{We are not able to fill this gap,} until we have to live
1773 % with it but first have a look on the meaning of this statement:
1774 % Mechanized math starts from mathematical models and \emph{hopefully}
1775 % proceeds to match physics. Academic engineering starts from physics
1776 % (experimentation, measurement) and then proceeds to mathematical
1777 % modeling and formalization. The process from a physical observance to
1778 % a mathematical theory is unavoidable bound of setting up a big
1779 % collection of standards, rules, definition but also exceptions. These
1780 % are the things making mechanization that difficult.
1789 % \noindent Think about some units like that one's above. Behind
1790 % each unit there is a discerning and very accurate definition: One
1791 % Meter is the distance the light travels, in a vacuum, through the time
1792 % of 1 / 299.792.458 second; one kilogram is the weight of a
1793 % platinum-iridium cylinder in paris; and so on. But are these
1794 % definitions usable in a computer mechanized world?!
1799 % \paragraph{A computer} or a TP-System builds on programs with
1800 % predefined logical rules and does not know any mathematical trick
1801 % (follow up example \ref{eg:trick}) or recipe to walk around difficult
1807 % \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1808 % \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1809 % \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1810 % \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1812 % \noindent Sometimes it is also useful to be able to apply some
1813 % \emph{tricks} to get a beautiful and particularly meaningful result,
1814 % which we are able to interpret. But as seen in this example it can be
1815 % hard to find out what operations have to be done to transform a result
1816 % into a meaningful one.
1821 % \paragraph{The only possibility,} for such a system, is to work
1822 % through its known definitions and stops if none of these
1823 % fits. Specified on Signal Processing or any other application it is
1824 % often possible to walk through by doing simple creases. This creases
1825 % are in general based on simple math operational but the challenge is
1826 % to teach the machine \emph{all}\footnote{Its pride to call it
1827 % \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1828 % reach a high level of \emph{all} but it in real it will still be a
1829 % survey of knowledge which links to other knowledge and {{\sisac}{}} a
1830 % trainer and helper but no human compensating calculator.
1832 % {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1833 % specifications of problems out of topics from Signal Processing, etc.)
1834 % and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1835 % physical knowledge. The result is a three-dimensional universe of
1836 % mathematics seen in Figure~\ref{fig:mathuni}.
1840 % \includegraphics{fig/universe}
1841 % \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1842 % combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1843 % leads to a three dimensional math universe.\label{fig:mathuni}}
1847 % %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1848 % %WN bitte folgende Bezeichnungen nehmen:
1850 % %WN axis 1: Algorithmic Knowledge (Programs)
1851 % %WN axis 2: Application-oriented Knowledge (Specifications)
1852 % %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1854 % %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1855 % %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1856 % %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1858 % %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1859 % %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1860 % %JR gefordert werden WN2...
1861 % %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1862 % %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1863 % %WN2 zusammenschneiden um die R"ander weg zu bekommen)
1864 % %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1865 % %WN2 png + pdf figures mitzuschicken.
1867 % \subsection{Notes on Problems with Traditional Notation}
1869 % \paragraph{During research} on these topic severely problems on
1870 % traditional notations have been discovered. Some of them have been
1871 % known in computer science for many years now and are still unsolved,
1872 % one of them aggregates with the so called \emph{Lambda Calculus},
1873 % Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1880 % \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1883 % \[ f(p)=\ldots\; p \in \quad R \]
1886 % \noindent Above we see two equations. The first equation aims to
1887 % be a mapping of an function from the reel range to the reel one, but
1888 % when we change only one letter we get the second equation which
1889 % usually aims to insert a reel point $p$ into the reel function. In
1890 % computer science now we have the problem to tell the machine (TP) the
1891 % difference between this two notations. This Problem is called
1892 % \emph{Lambda Calculus}.
1897 % \paragraph{An other problem} is that terms are not full simplified in
1898 % traditional notations, in {{\sisac}} we have to simplify them complete
1899 % to check weather results are compatible or not. in e.g. the solutions
1900 % of an second order linear equation is an rational in {{\sisac}} but in
1901 % tradition we keep fractions as long as possible and as long as they
1902 % aim to be \textit{beautiful} (1/8, 5/16,...).
1903 % \subparagraph{The math} which should be mechanized in Computer Theorem
1904 % Provers (\emph{TP}) has (almost) a problem with traditional notations
1905 % (predicate calculus) for axioms, definitions, lemmas, theorems as a
1906 % computer program or script is not able to interpret every Greek or
1907 % Latin letter and every Greek, Latin or whatever calculations
1908 % symbol. Also if we would be able to handle these symbols we still have
1909 % a problem to interpret them at all. (Follow up \hbox{Example
1910 % \ref{eg:symbint1}})
1914 % \label{eg:symbint1}
1916 % u\left[n\right] \ \ldots \ unitstep
1919 % \noindent The unitstep is something we need to solve Signal
1920 % Processing problem classes. But in {{{\sisac}{}}} the rectangular
1921 % brackets have a different meaning. So we abuse them for our
1922 % requirements. We get something which is not defined, but usable. The
1923 % Result is syntax only without semantic.
1928 % In different problems, symbols and letters have different meanings and
1929 % ask for different ways to get through. (Follow up \hbox{Example
1930 % \ref{eg:symbint2}})
1934 % \label{eg:symbint2}
1936 % \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1939 % \noindent For using exponents the three \texttt{widehat} symbols
1940 % are required. The reason for that is due the development of
1941 % {{{\sisac}{}}} the single \texttt{widehat} and also the double were
1942 % already in use for different operations.
1947 % \paragraph{Also the output} can be a problem. We are familiar with a
1948 % specified notations and style taught in university but a computer
1949 % program has no knowledge of the form proved by a professor and the
1950 % machines themselves also have not yet the possibilities to print every
1951 % symbol (correct) Recent developments provide proofs in a human
1952 % readable format but according to the fact that there is no money for
1953 % good working formal editors yet, the style is one thing we have to
1956 % \section{Problems rising out of the Development Environment}
1958 % fehlermeldungen! TODO
1960 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
1962 \section{Summary and Conclusions}\label{conclusion}
1966 %This paper gives a first experience report about programming with a
1967 %TP-based programming language.
1969 A brief re-introduction of the novel kind of programming
1970 language by example of the {\sisac}-prototype makes the paper
1971 self-contained. The main section describes all the main concepts
1972 involved in TP-based programming and all the sub-tasks concerning
1973 respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain
1974 modeling, implementation of term rewriting systems for the
1975 rewriting-engine, formal (implicit) specification of the problem to be
1976 (explicitly) described by the program, implementation of the many components
1977 required for Lucas-Interpretation and finally implementation of the
1980 The many concepts and sub-tasks involved in programming require a
1981 comprehensive work-flow; first experiences with the work-flow as
1982 supported by the present prototype are described as well: Isabelle +
1983 Isar + jEdit provide appropriate components for establishing an
1984 efficient development environment integrating computation and
1985 deduction. However, the present state of the prototype is far off a
1986 state appropriate for wide-spread use: the prototype of the program
1987 language lacks expressiveness and elegance, the prototype of the
1988 development environment is hardly usable: error messages still address
1989 the developer of the prototype's interpreter rather than the
1990 application programmer, implementation of the many settings for the
1991 Lucas-Interpreter is cumbersome.
1993 \subsection{Conclusions for Future Development}
1994 From the above mentioned experiences a successful proof of concept can be concluded:
1995 programming arbitrary problems from engineering sciences is possible,
1996 in principle even in the prototype. Furthermore the experiences allow
1997 to conclude detailed requirements for further development:
1999 \item Clarify underlying logics such that programming is smoothly
2000 integrated with verification of the program; the post-condition should
2001 be proved more or less automatically, otherwise working engineers
2002 would not encounter such programming.
2003 \item Combine the prototype's programming language with Isabelle's
2004 powerful function package and probably with more of SML's
2005 pattern-matching features; include parallel execution on multi-core
2006 machines into the language design.
2007 \item Extend the prototype's Lucas-Interpreter such that it also
2008 handles functions defined by use of Isabelle's functions package; and
2009 generalize Isabelle's code generator such that efficient code for the
2010 whole definition of the programming language can be generated (for
2011 multi-core machines).
2012 \item Develop an efficient development environment with
2013 integration of programming and proving, with management not only of
2014 Isabelle theories, but also of large collections of specifications and
2016 \item\label{CAS} Extend Isabelle's computational features in direction of
2017 \textit{verfied} Computer Algebra: simplification extended by
2018 algorithms beyond rewriting (cancellation of multivariate rationals,
2019 factorisation, partial fraction decomposition, etc), equation solving
2022 Provided successful accomplishment, these points provide distinguished
2023 components for virtual workbenches appealing to practitioners of
2024 engineering in the near future.
2026 \subsection{Preview to Development of Course Material}
2027 Interactive course material, as addressed by the title,
2028 can comprise step-wise problem solving created as a side-effect of a
2029 TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an
2030 interactive programming environment, Lucas-Interpretation also can
2031 provide TP-based services for a flexible dialogue component with
2032 adaptive user guidance for independent and inquiry-based learning.
2034 However, the {\sisac} prototype is not ready for use in field-tests,
2035 not only due to the above five requirements not sufficiently
2036 accomplished, but also due to usability of the fron-end, in particular
2037 the lack of an editor for formulas in 2-dimension representation.
2039 Nevertheless, the experiences from the case study described in this
2040 paper, allow to give a preview to the development of course material,
2041 if based on Lucas-Interpretation:
2043 \paragraph{Development of material from scratch} is too much effort
2044 just for e-learning; this has become clear with the case study. For
2045 getting support for stepwise problem solving just in {\em one} example
2046 class, the one presented in this paper, involved the following tasks:
2048 \item Adapt the equation solver; since that was too laborous, the
2049 program has been adapted in an unelegant way.
2050 \item Implement an algorithms for partial fraction decomposition,
2051 which is considered a standard normal form in Computer Algebra.
2052 \item Implement a specification for partial fraction decomposition and
2053 locate it appropriately in the hierarchy of specification.
2054 \item Declare definitions and theorems within the theory of
2055 ${\cal Z}$-transform, and prove the theorems (which was not done in the
2058 On the other hand, for the one the class of problems implemented,
2059 adding an arbitrary number of examples within this class requires a
2060 few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an
2061 example is called from an HTML-file by an URL, which addresses an
2062 XML-structure holding the respective data as shown on
2063 p.\pageref{ml-check-program}.} and the support for individual stepwise
2064 problem solving comes for free.
2066 \paragraph{E-learning benefits from Formal Domain Engineering} which can be
2067 expected for various domains in the near future. In order to cope with
2068 increasing complexity in domain of technology, specific domain
2069 knowledge is beeing mechanised, not only for software technology
2070 \footnote{For instance, the Archive of Formal Proofs
2071 http://afp.sourceforge.net/} but also for other engineering domains
2072 \cite{Dehbonei&94,Hansen94b,db:dom-eng}. This fairly new part of
2073 engineering sciences is called ``domain engineering'' in
2074 \cite{db:SW-engIII}.
2076 Given this kind of mechanised knowledge including mathematical
2077 theories, domain specific definitions, specifications and algorithms,
2078 theorems and proofs, then e-learning with support for individual
2079 stepwise problem solving will not be much ado anymore; then e-learning
2080 media in technology education can be derived from this knowledge with
2083 \paragraph{Development differentiates into tasks} more separated than
2084 without Lucas-Interpretation and more challenginging in specific
2085 expertise. These are the kinds of experts expected to cooperate in
2088 \item ``Domain engineers'', who accomplish fairly novel tasks
2089 described in this paper.
2090 \item Course designers, who provide the instructional design according
2091 to curricula, together with usability experts and media designers, are
2092 indispensable in production of e-learning media at the state-of-the
2094 \item ``Dialog designers'', whose part of development is clearly
2095 separated from the part of domain engineers as a consequence of
2096 Lucas-Interpretation: TP-based programs are functional, as mentioned,
2097 and are only concerned with describing mathematics --- and not at all
2098 concerned with interaction, psychology, learning theory and the like,
2099 because there are no in/output statements. Dialog designers can expect
2100 a high-level rule-based language~\cite{gdaroczy-EP-13} for describing
2104 % response-to-referees:
2105 % (2.1) details of novel technology in order to estimate the impact
2106 % (2.2) which kinds of expertise are required for production of e-learning media (instructional design, math authoring, dialog authoring, media design)
2107 % (2.3) what in particular is required for programming new exercises supported by next-step-guidance (expertise / efforts)
2108 % (2.4) estimation of break-even points for development of next-step-guidance
2109 % (2.5) usability of ISAC prototype at the present state
2111 % 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."".
2113 \bigskip\noindent For this decade there seems to be a window of opportunity opening from
2114 one side inreasing demand for formal domain engineering and from the
2115 other side from TP more and more gaining industrial relevance. Within
2116 this window, development of TP-based educational software can take
2117 benefit from the fact, that the TPs leading in Europe, Coq~\cite{coq-team-10} and
2118 Isabelle are still open source together with the major part of
2119 mechanised knowledge.%~\footnote{NICTA}.
2121 \bibliographystyle{alpha}
2122 {\small\bibliography{references}}
2125 % LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
2126 % LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised
2127 % LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
2128 % LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
2129 % LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
2130 % LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq
2131 % LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
2132 % LocalWords: mechanisation multi