1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 % Electronic Journal of Mathematics and Technology (eJMT) %
3 % style sheet for LaTeX. Please do not modify sections %
4 % or commands marked 'eJMT'. %
6 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10 \documentclass[12pt,a4paper]{article}% %
12 \usepackage{amsfonts,amsmath,amssymb} %
13 \usepackage[a4paper]{geometry} %
14 \usepackage{fancyhdr} %
16 \usepackage[pdftex]{hyperref} % see note below %
17 \usepackage{graphicx}% %
23 \newtheorem{theorem}{Theorem} %
24 \newtheorem{acknowledgement}[theorem]{Acknowledgement} %
25 \newtheorem{algorithm}[theorem]{Algorithm} %
26 \newtheorem{axiom}[theorem]{Axiom} %
27 \newtheorem{case}[theorem]{Case} %
28 \newtheorem{claim}[theorem]{Claim} %
29 \newtheorem{conclusion}[theorem]{Conclusion} %
30 \newtheorem{condition}[theorem]{Condition} %
31 \newtheorem{conjecture}[theorem]{Conjecture} %
32 \newtheorem{corollary}[theorem]{Corollary} %
33 \newtheorem{criterion}[theorem]{Criterion} %
34 \newtheorem{definition}[theorem]{Definition} %
35 \newtheorem{example}[theorem]{Example} %
36 \newtheorem{exercise}[theorem]{Exercise} %
37 \newtheorem{lemma}[theorem]{Lemma} %
38 \newtheorem{notation}[theorem]{Notation} %
39 \newtheorem{problem}[theorem]{Problem} %
40 \newtheorem{proposition}[theorem]{Proposition} %
41 \newtheorem{remark}[theorem]{Remark} %
42 \newtheorem{solution}[theorem]{Solution} %
43 \newtheorem{summary}[theorem]{Summary} %
44 \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } %
45 {\ \rule{0.5em}{0.5em}} %
47 % eJMT page dimensions %
49 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
51 % eJMT header & footer %
53 \newcounter{ejmtFirstpage} %
54 \setcounter{ejmtFirstpage}{1} %
56 \setlength{\headheight}{14pt} %
57 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
58 \pagestyle{fancyplain} %
60 \fancyhead[c]{\small The Electronic Journal of Mathematics%
61 \ and Technology, Volume 1, Number 1, ISSN 1933-2823} %
63 \ifnum\value{ejmtFirstpage}=0% %
64 {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% %
65 \else\setcounter{ejmtFirstpage}{0}\fi% %
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
70 % Please place your own definitions here
72 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
73 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
76 \definecolor{lgray}{RGB}{238,238,238}
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 % How to use hyperref %
82 % ------------------- %
84 % Probably the only way you will need to use the hyperref %
85 % package is as follows. To make some text, say %
86 % "My Text Link", into a link to the URL %
87 % http://something.somewhere.com/mystuff, use %
89 % \href{http://something.somewhere.com/mystuff}{My Text Link}
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
97 \title{Trials with TP-based Programming
99 for Interactive Course Material}%
101 % Single author. Please supply at least your name,
102 % email address, and affiliation here.
104 \author{\begin{tabular}{c}
105 \textit{Jan Ro\v{c}nik} \\
106 jan.rocnik@student.tugraz.at \\
108 Graz University of Technologie\\
112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
114 % eJMT commands - do not change these %
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
125 Traditional course material in engineering disciplines lacks an
126 important component, interactive support for step-wise problem
127 solving. Theorem-Proving (TP) technology is appropriate for one part
128 of such support, in checking user-input. For the other part of such
129 support, guiding the learner towards a solution, another kind of
130 technology is required. %TODO ... connect to prototype ...
132 Both kinds of support can be acchieved 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 insuggicient 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. Theorem-Proving (TP) technology can provide such support by
207 specific services. An important part of such services is called
208 ``next-step-guidance'', generated by a specific kind of ``TP-based
209 programming language''. In the
210 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
211 a language is prototyped in line with~\cite{plmms10} and built upon
213 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
214 The TP services are coordinated by a specific interpreter for the
215 programming language, called
216 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
217 interpreter will be briefly re-introduced in order to make the paper
220 The main part of the paper is an account of first experiences
221 with programming in this TP-based language. The experience was gained
222 in a case study by the author. The author was considered an ideal
223 candidate for this study for the following reasons: as a student in
224 Telematics (computer science with focus on Signal Processing) he had
225 general knowledge in programming as well as specific domain knowledge
226 in Signal Processing; and he was {\em not} involved in the development of
227 {\sisac}'s programming language and interpeter, thus a novice to the
230 The goal of the case study was (1) some TP-based programs for
231 interactive course material for a specific ``Adavanced Signal
232 Processing Lab'' in a higher semester, (2) respective program
233 development with as little advice from the {\sisac}-team and (3) records
234 and comments for the main steps of development in an Isabelle theory;
235 this theory should provide guidelines for future programmers. An
236 excerpt from this theory is the main part of this paper.
238 The paper will use the problem in Fig.\ref{fig-interactive} as a
242 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
243 %\includegraphics[width=140mm]{fig/isac-Ztrans-math}
244 \caption{Step-wise problem solving guided by the TP-based program}
245 \label{fig-interactive}
249 The problem is from the domain of Signal Processing and requests to
250 determine the inverse ${\cal Z}$-transform for a given term. Fig.\ref{fig-interactive}
251 also shows the beginning of the interactive construction of a solution
252 for the problem. This construction is done in the right window named
255 User-interaction on the Worksheet is {\em checked} and {\em guided} by
258 \item Formulas input by the user are {\em checked} by TP: such a
259 formula establishes a proof situation --- the prover has to derive the
260 formula from the logical context. The context is built up from the
261 formal specification of the problem (here hidden from the user) by the
263 \item If the user gets stuck, the program developed below in this
264 paper ``knows the next step'' and Lucas-Interpretation provides services
265 featuring so-called ``next-step-guidance''; this is out of scope of this
266 paper and can be studied in~\cite{gdaroczy-EP-13}.
267 \end{enumerate} It should be noted that the programmer using the
268 TP-based language is not concerned with interaction at all; we will
269 see that the program contains neither input-statements nor
270 output-statements. Rather, interaction is handled by the interpreter
273 So there is a clear separation of concerns: Dialogues are adapted by
274 dialogue authors (in Java-based tools), using TP services provided by
275 Lucas-Interpretation. The latter acts on programs developed by
276 mathematics-authors (in Isabelle/ML); their task is concern of this
279 \paragraph{The paper is structed} as follows: The introduction
280 \S\ref{intro} is followed by a brief re-introduction of the TP-based
281 programming language in \S\ref{PL}, which extends the executable
282 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
283 play a specific role in Lucas-Interpretation and in providing the TP
284 services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
285 the main steps in developing the program for the running example:
286 prepare domain knowledge, implement the formal specification of the
287 problem, prepare the environment for the interpreter, implement the
288 program in \S\ref{isabisac} to \S\ref{progr} respectively.
289 The workflow of programming, debugging and testing is
290 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
291 give directions identified for future development.
294 \section{\isac's Prototype for a Programming Language}\label{PL}
295 The prototype of the language and of the Lucas-Interpreter are briefly
296 described from the point of view of a programmer. The language extends
297 the executable fragment in the language of the theorem prover
298 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
300 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
301 The executable fragment consists of data-type and function
302 definitions. It's usability even suggests that fragment for
303 introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
304 whose type system resembles that of functional programming
305 languages. Thus there are
307 \item[base types,] in particular \textit{bool}, the type of truth
308 values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
309 natural, integer and complex numbers respectively in mathematics.
310 \item[type constructors] allow to define arbitrary types, from
311 \textit{set}, \textit{list} to advanced data-structures like
312 \textit{trees}, red-black-trees etc.
313 \item[function types,] denoted by $\Rightarrow$.
314 \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
315 type polymorphism. Isabelle automatically computes the type of each
316 variable in a term by use of Hindley-Milner type inference
317 \cite{pl:hind97,Milner-78}.
320 \textbf{Terms} are formed as in functional programming by applying
321 functions to arguments. If $f$ is a function of type
322 $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
323 $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
324 has type $\tau$. There are many predefined infix symbols like $+$ and
325 $\leq$ most of which are overloaded for various types.
327 HOL also supports some basic constructs from functional programming:
328 {\it\label{isabelle-stmts}
329 \begin{tabbing} 123\=\kill
330 \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
331 \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
332 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
333 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
335 \noindent The running example's program uses some of these elements
336 (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
337 let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
338 is an Isabelle term with specific function constants like {\tt
339 program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
340 Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
343 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
344 % x. \; x$ is the identity function.
346 %JR warum auskommentiert? WN2...
347 %WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
348 %WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
349 %WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
351 %WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
352 %WN2 Platz f"ur Anderes weg.
354 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
355 constants \textit{True} and \textit{False} and the usual logical
356 connectives (in decreasing order of precedence): $\neg, \land, \lor,
359 \textbf{Equality} is available in the form of the infix function $=$
360 of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
361 formulas, where it means ``if and only if''.
363 \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
364 P$. Quantifiers lead to non-executable functions, so functions do not
365 always correspond to programs, for instance, if comprising \\$(
366 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
369 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
370 The prototype extends Isabelle's language by specific statements
371 called tactics~\footnote{{\sisac}'s tactics are different from
372 Isabelle's tactics: the former concern steps in a calculation, the
373 latter concern proofs.} and tacticals. For the programmer these
374 statements are functions with the following signatures:
377 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
378 term} * {\it term}\;{\it list}$:
379 this tactic appplies {\it theorem} to a {\it term} yielding a {\it
380 term} and a {\it term list}, the list are assumptions generated by
381 conditional rewriting. For instance, the {\it theorem}
382 $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
383 applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
384 $(\frac{2}{3}, [x\not=0])$.
386 \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
387 term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
388 this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
389 a confluent and terminating term rewrite system, in general. If
390 none of the rules ({\it theorem}s) is applicable on interpretation
391 of this tactic, an exception is thrown.
393 % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
394 % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
397 % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
398 % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
402 \item[Substitute:] ${\it substitution}\Rightarrow{\it
403 term}\Rightarrow{\it term}$: allows to access sub-terms.
406 \item[Take:] ${\it term}\Rightarrow{\it term}$:
407 this tactic has no effect in the program; but it creates a side-effect
408 by Lucas-Interpretation (see below) and writes {\it term} to the
411 \item[Subproblem:] ${\it theory} * {\it specification} * {\it
412 method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
413 this tactic is a generalisation of a function call: it takes an
414 \textit{argument list} as usual, and additionally a triple consisting
415 of an Isabelle \textit{theory}, an implicit \textit{specification} of the
416 program and a \textit{method} containing data for Lucas-Interpretation,
417 last not least a program (as an explicit specification)~\footnote{In
418 interactive tutoring these three items can be determined explicitly
421 The tactics play a specific role in
422 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
423 break-points where, as a side-effect, a line is added to a calculation
424 as a protocol for proceeding towards a solution in step-wise problem
425 solving. At the same points Lucas-Interpretation serves interactive
426 tutoring and hands over control to the user. The user is free to
427 investigate underlying knowledge, applicable theorems, etc. And the
428 user can proceed constructing a solution by input of a tactic to be
429 applied or by input of a formula; in the latter case the
430 Lucas-Interpreter has built up a logical context (initialised with the
431 precondition of the formal specification) such that Isabelle can
432 derive the formula from this context --- or give feedback, that no
433 derivation can be found.
435 \subsection{Tacticals as Control Flow Statements}
436 The flow of control in a program can be determined by {\tt if then else}
437 and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
438 by additional tacticals:
440 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
441 term}$: iterates over tactics which take a {\it term} as argument as
442 long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
445 \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
446 if {\it tactic} is applicable, then it is applied to {\it term},
447 otherwise {\it term} is passed on without changes.
449 \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
450 term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
451 it is applied to the first {\it term} yielding another {\it term},
452 otherwise the second {\it tactic} is applied; if none is applicable an
455 \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
456 term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
457 first {\it term} yielding an intermediate term (not appearing in the
458 signature) to which the second {\it tactic} is applied.
460 \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
461 term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
462 {\it tactic} is applied to the first {\it term} yielding an
463 intermediate term (not appearing in the signature); the intermediate
464 term is added to the environment the first {\it term} is evaluated in
465 etc as long as the first {\it term} is true.
467 The tacticals are not treated as break-points by Lucas-Interpretation
468 and thus do neither contribute to the calculation nor to interaction.
470 \section{Concepts and Tasks in TP-based Programming}\label{trial}
471 %\section{Development of a Program on Trial}
473 This section presents all the concepts involved in TP-based
474 programming and all the tasks to be accomplished by programmers. The
475 presentation uses the running example from
476 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
478 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
480 %WN was Fachleute unter obigem Titel interessiert findet sich
481 %WN unterhalb des auskommentierten Textes.
483 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
484 %WN auf Computer-Mathematiker fokussiert.
485 % \paragraph{As mentioned in the introduction,} a prototype of an
486 % educational math assistant called
487 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
488 % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
489 % the gap between (1) introducation and (2) application of mathematics:
490 % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
491 % requires each fact and each action justified by formal logic, so
492 % {{{\sisac}{}}} makes justifications transparent to students in
493 % interactive step-wise problem solving. By that way {{\sisac}} already
496 % \item Introduction of math stuff (in e.g. partial fraction
497 % decomposition) by stepwise explaining and exercising respective
498 % symbolic calculations with ``next step guidance (NSG)'' and rigorously
499 % checking steps freely input by students --- this also in context with
500 % advanced applications (where the stuff to be taught in higher
501 % semesters can be skimmed through by NSG), and
502 % \item Application of math stuff in advanced engineering courses
503 % (e.g. problems to be solved by inverse Z-transform in a Signal
504 % Processing Lab) and now without much ado about basic math techniques
505 % (like partial fraction decomposition): ``next step guidance'' supports
506 % students in independently (re-)adopting such techniques.
508 % Before the question is answers, how {{\sisac}}
509 % accomplishes this task from a technical point of view, some remarks on
510 % the state-of-the-art is given, therefor follow up Section~\ref{emas}.
512 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
514 % \paragraph{Educational software in mathematics} is, if at all, based
515 % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
516 % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
517 % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
518 % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
519 % base technologies are used to program math lessons and sometimes even
520 % exercises. The latter are cumbersome: the steps towards a solution of
521 % such an interactive exercise need to be provided with feedback, where
522 % at each step a wide variety of possible input has to be foreseen by
523 % the programmer - so such interactive exercises either require high
524 % development efforts or the exercises constrain possible inputs.
526 % \subparagraph{A new generation} of educational math assistants (EMAs)
527 % is emerging presently, which is based on Theorem Proving (TP). TP, for
528 % instance Isabelle and Coq, is a technology which requires each fact
529 % and each action justified by formal logic. Pushed by demands for
530 % \textit{proven} correctness of safety-critical software TP advances
531 % into software engineering; from these advancements computer
532 % mathematics benefits in general, and math education in particular. Two
533 % features of TP are immediately beneficial for learning:
535 % \paragraph{TP have knowledge in human readable format,} that is in
536 % standard predicate calculus. TP following the LCF-tradition have that
537 % knowledge down to the basic definitions of set, equality,
538 % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
539 % following the typical deductive development of math, natural numbers
540 % are defined and their properties
541 % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
542 % etc. Present knowledge mechanized in TP exceeds high-school
543 % mathematics by far, however by knowledge required in software
544 % technology, and not in other engineering sciences.
546 % \paragraph{TP can model the whole problem solving process} in
547 % mathematical problem solving {\em within} a coherent logical
548 % framework. This is already being done by three projects, by
549 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
551 % Having the whole problem solving process within a logical coherent
552 % system, such a design guarantees correctness of intermediate steps and
553 % of the result (which seems essential for math software); and the
554 % second advantage is that TP provides a wealth of theories which can be
555 % exploited for mechanizing other features essential for educational
558 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
560 % One essential feature for educational software is feedback to user
561 % input and assistance in coming to a solution.
563 % \paragraph{Checking user input} by ATP during stepwise problem solving
564 % is being accomplished by the three projects mentioned above
565 % exclusively. They model the whole problem solving process as mentioned
566 % above, so all what happens between formalized assumptions (or formal
567 % specification) and goal (or fulfilled postcondition) can be
568 % mechanized. Such mechanization promises to greatly extend the scope of
569 % educational software in stepwise problem solving.
571 % \paragraph{NSG (Next step guidance)} comprises the system's ability to
572 % propose a next step; this is a challenge for TP: either a radical
573 % restriction of the search space by restriction to very specific
574 % problem classes is required, or much care and effort is required in
575 % designing possible variants in the process of problem solving
576 % \cite{proof-strategies-11}.
578 % Another approach is restricted to problem solving in engineering
579 % domains, where a problem is specified by input, precondition, output
580 % and postcondition, and where the postcondition is proven by ATP behind
581 % the scenes: Here the possible variants in the process of problem
582 % solving are provided with feedback {\em automatically}, if the problem
583 % is described in a TP-based programing language: \cite{plmms10} the
584 % programmer only describes the math algorithm without caring about
585 % interaction (the respective program is functional and even has no
586 % input or output statements!); interaction is generated as a
587 % side-effect by the interpreter --- an efficient separation of concern
588 % between math programmers and dialog designers promising application
589 % all over engineering disciplines.
592 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
593 % Authoring new mathematics knowledge in {{\sisac}} can be compared with
594 % ``application programing'' of engineering problems; most of such
595 % programing uses CAS-based programing languages (CAS = Computer Algebra
596 % Systems; e.g. Mathematica's or Maple's programing language).
598 % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
599 % \cite{plmms10} for describing how to construct a solution to an
600 % engineering problem and for calling equation solvers, integration,
601 % etc~\footnote{Implementation of CAS-like functionality in TP is not
602 % primarily concerned with efficiency, but with a didactic question:
603 % What to decide for: for high-brow algorithms at the state-of-the-art
604 % or for elementary algorithms comprehensible for students?} within TP;
605 % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
606 % are impossible for CAS which have no logics underlying.
608 % \subparagraph{Authoring is perfect} by writing such TP based programs;
609 % the application programmer is not concerned with interaction or with
610 % user guidance: this is concern of a novel kind of program interpreter
611 % called Lucas-Interpreter. This interpreter hands over control to a
612 % dialog component at each step of calculation (like a debugger at
613 % breakpoints) and calls automated TP to check user input following
614 % personalized strategies according to a feedback module.
616 % However ``application programing with TP'' is not done with writing a
617 % program: according to the principles of TP, each step must be
618 % justified. Such justifications are given by theorems. So all steps
619 % must be related to some theorem, if there is no such theorem it must
620 % be added to the existing knowledge, which is organized in so-called
621 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
622 % Isabelle comprises a mechanism (called ``axiomatization''), which
623 % allows to omit proofs. Such a theorem is shown in
624 % Example~\ref{eg:neuper1}.
626 The running example requires to determine the inverse $\cal
627 Z$-transform for a class of functions. The domain of Signal Processing
628 is accustomed to specific notation for the resulting functions, which
629 are absolutely summable and are called step-response: $u[n]$, where $u$ is the
630 function, $n$ is the argument and the brackets indicate that the
631 arguments are discrete. Surprisingly, Isabelle accepts the rules for
632 ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
633 experts might be particularly surprised, that the brackets do not
634 cause errors in typing (as lists).}:
638 {\small\begin{tabbing}
639 123\=123\=123\=123\=\kill
641 \>axiomatization where \\
642 \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
643 \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
644 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
646 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
648 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
650 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
656 These 6 rules can be used as conditional rewrite rules, depending on
657 the respective convergence radius. Satisfaction from accordance with traditional notation
658 contrasts with the above word {\em axiomatization}: As TP-based, the
659 programming language expects these rules as {\em proved} theorems, and
660 not as axioms implemented in the above brute force manner; otherwise
661 all the verification efforts envisaged (like proof of the
662 post-condition, see below) would be meaningless.
664 Isabelle provides a large body of knowledge, rigorously proven from
665 the basic axioms of mathematics~\footnote{This way of rigorously
666 deriving all knowledge from first principles is called the
667 LCF-paradigm in TP.}. In the case of the ${\cal Z}$-Transform the most advanced
668 knowledge can be found in the theoris on Multivariate
669 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
670 building up knowledge such that a proof for the above rules would be
671 reasonably short and easily comprehensible, still requires lots of
672 work (and is definitely out of scope of our case study).
674 At the state-of-the-art in mechanization of knowledge in engineering
675 sciences, the process does not stop with the mechanization of
676 mathematics traditionally used in these sciences. Rather, ``Formal
677 Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
678 description of physical items. Signal Processing, for instance is
679 concerned with physical devices for signal acquisition and
680 reconstruction, which involve measuring a physical signal, storing it,
681 and possibly later rebuilding the original signal or an approximation
682 thereof. For digital systems, this typically includes sampling and
683 quantization; devices for signal compression, including audio
684 compression, image compression, and video compression, etc. ``Domain
685 engineering''\cite{db:dom-eng} is concerned with {\em specification}
686 of these devices' components and features; this part in the process of
687 mechanization is only at the beginning in domains like Signal
690 TP-based programming, concern of this paper, is determined to
691 add ``algorithmic knowledge'' to the mechanised body of knowledge.
692 % in Fig.\ref{fig:mathuni} on
693 % p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
694 % starts with a formal {\em specification} of the problem to be solved.
697 % \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
698 % \caption{The three-dimensional universe of mathematics knowledge}
699 % \label{fig:mathuni}
702 % The language for both axes is defined in the axis at the bottom, deductive
703 % knowledge, in {\sisac} represented by Isabelle's theories.
705 \subsection{Preparation of Simplifiers for the Program}\label{simp}
707 All evaluation in the prototyp's Lucas-Interpreter is done by term rewriting on
708 Isabelle's terms, see \S\ref{meth} below; in this section some of respective
709 preparations are described. In order to work reliably with term rewriting, the
710 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
711 then they are called (canonical) simplifiers. These properties do not go without
712 saying, their establishment is a difficult task for the programmer; this task is
713 not yet supported in the prototype.\par
715 % If it is clear how the later calculation should look like
716 % %WN3 ... Allgem.<-->Konkret ist gut: aber hier ist 'calculation'
717 % %WN3 zu weit weg: der Satz geh"ort bestenfalls gleich an den
718 % %WN3 Anfang von \sect.3
720 % %WN3 Im Folgenden sind einige Ungenauigkeiten:
722 % which mathematic rule
723 % %WN3 rewrite-rule oder theorem ! Ein Paper enth"alt viele Begriffe
724 % %WN3 und man versucht, die Anzahl so gering wie m"oglich zu halten
725 % %WN3 und die verbleibenden so pr"azise zu definieren wie m"oglich;
726 % %WN3 das Vermeiden von Wiederholungen muss mit anderen Mitteln erfolgen,
727 % %WN3 als dieselbe Sache mit verschiedenen Namen zu benennen;
728 % %WN3 das gilt insbesonders f"ur technische Begriffe wie oben
729 % should be applied, it can be started to find ways of
731 % %WN3 ... zu allgemein. Das Folgende w"urde durch einen Verweis in
732 % %WN3 das Programm auf S.12 gewinnen.
733 % This includes in e.g. the simplification of reational
734 % expressions or also rewrites of an expession.
736 % %WN3 das Folgende habe ich aus dem Beispielprogramm auf S.12
737 % %WN3 gestrichen, weil es aus prinzipiellen Gr"unden unsch"on ist.
738 % %WN3 Und es ist so kompliziert dass es mehr Platz zum Erkl"aren
739 % %WN3 braucht, als es wert ist ...
740 % Obligate is the use of the function \texttt{drop\_questionmarks}
741 % which excludes irrelevant symbols out of the expression. (Irrelevant symbols may
742 % be result out of the system during the calculation. The function has to be
743 % applied for two reasons. First two make every placeholder in a expression
744 % useable as a constant and second to provide a better view at the frontend.)
746 % %WN3 Da kommt eine ganze Reihe von Ungenauigkeiten:
747 % Most rewrites are represented through rulesets
748 % %WN3 ... das ist schlicht falsch:
749 % %WN3 _alle_ rewrites werden durch rule-sets erzeugt (per definition
750 % %WN3 dieser W"orter).
752 % rulesets tell the machine which terms have to be rewritten into which
754 % %WN3 ... ist ein besonders "uberzeugendes Beispiel von Allgem.<-->Konkret:
755 % %WN3 so allgemein, wie es hier steht, ist es
756 % %WN3 # f"ur einen Fachmann klar und nicht ganz fachgem"ass formuliert
757 % %WN3 (a rule-set rewrites a certain term into another with certain properties)
758 % %WN3 # f"ur einen Nicht-Fachmann trotz allem unverst"andlich.
760 % %WN3 Wenn schon allgemeine S"atze, dann unmittelbar auf das Beispiel
761 % %WN3 unten verweisen,
762 % %WN3 oder besser: den Satz dorthin schreiben, wo er unmittelbar vom
763 % %WN3 Beispiel gefolgt wird.
764 % In the upcoming programm a rewrite can be applied only in using
765 % such rulesets on existing terms.
766 % %WN3 Du willst wohl soetwas sagen wie ...
767 % %WN3 rewriting is the main concept to step-wise create and transform
768 % %WN3 formulas in order to proceed towards a solution of a problem
770 % \paragraph{The core} of our implemented problem is the Z-Transformation
771 % %WN3 ^^^^^ ist nicht gut: was soll THE CORE vermitteln, wenn man die
772 % %WN3 Seite "uberfliegt ? Dass hier das Zentrum Deiner Arbeit liegt ?
774 % %WN3 Das Folgende ist eine allgemeine Design-"Uberlegung, die entweder
775 % %WN3 vorne zur Einf"uhrung des Beispiels geh"ort,
776 % %WN3 oder zur konkreten L"osung durch die Rechnung auf S.15/16.
777 % (remember the description of the running example, introduced by
778 % Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the
779 % transformation itself would require higher math which isn't yet avaible in our system we decided to choose the way like it is applied in labratory and problem classes at our university - by applying transformation rules (collected in
780 % transformation tables).
782 % %WN3 Zum Folgenden: 'axiomatization' ist schon in 3.1. angesprochen:
783 % %WN3 entweder dort erg"anzen, wenn's wichtig ist, oder weglassen.
784 % Rules, in {\sisac{}}'s programming language can be designed by the use of
785 % axiomatization. In this axiomatization we declare how a term has to look like
786 % (left side) to be rewritten into another form (right side). Every line of this
787 % axiomatizations starts with the name of the rule.
789 The prototype rewrites using theorems only. Axioms which are theorems as well
790 have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
791 assemble them in a rule-set and apply them as follows:
793 % %WN3 Die folgenden Zeilen nehmen Platz weg: von hier auf S.6 verweisen
799 % axiomatization where
800 % rule1: ``1 = $\delta$[n]'' and
801 % rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
802 % rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
807 % Rules can be summarized in a ruleset (collection of rules) and afterwards tried % to be applied to a given expression as puttet over in following code.
808 %WN3 ... ist schon mehrmals gesagt worden. 1-mal pr"azise sagen gen"ugt.
810 %WN3 mit dem append_rls unten verbirgst Du die ganze Komplexit"at von
811 %WN3 rule-sets --- ich w"urde diese hier ausbreiten, damit man die
812 %WN3 Schwierigkeit von TP-based programming ermessen kann.
813 %WN3 Eine Erkl"arung wie in 3.4 und 3.5 braucht viel Platz, der sich
814 %WN3 meines Erachtens mehr auszahlt als die allgemeinen S"atze
815 %WN3 am Ende von 3.2 auf S.8.
817 %WN3 mache ein 'grep -r "and rls";
818 %WN3 auch in Build_Inverse_Z_Transform.thy hast Du 'Rls'
826 \item Store rules in ruleset:
827 {\footnotesize\begin{verbatim}
828 01 val inverse_Z = append_rls "inverse_Z" e_rls
829 02 [ Thm ("rule1",num_str @{thm rule1}),
830 03 Thm ("rule2",num_str @{thm rule2}),
831 04 Thm ("rule3",num_str @{thm rule3})
834 \item Define exression:
835 {\footnotesize\begin{verbatim}
836 06 val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}}
839 %WN3 vergleiche bitte obige Zeile mit den letzten 3 Zeilen aus S.8,
840 %WN3 diese entsprechen dem g"angigen functional-programming Stil.
845 %WN3 Super w"ar's, wenn Du hier schon die interne Darstellung von
846 %WN3 Isabelle Termen zeigen k"onntest, dann w"urde ich den entsprechenden Teil
847 %WN3 am Ende von S.8 und Anfang S.9 (erste 2.1 Zeilen) l"oschen.
849 %JR ich habe einige male über seite acht gelesen, finde aber dass der teil über
850 %JR die interne representation dorthin besser passt da diese in unserem
851 %JR gezeigten beispiel ja in direkter verbindung zur gezeigtem funktion besteht
852 %JR und so der übergang exzellent ist.
855 {\footnotesize\begin{verbatim}
856 07 val SOME (sample_term', asm) =
857 08 rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}}
862 %WN3 Wie oben gesagt, die folgenden allgemeinen S"atze scheinen
863 %WN3 weniger wert als eine konkrete Beschreibung der rls-Struktur.
865 %WN3 Ich nehme an, wir l"oschen das Folgende
866 %WN3 und ich spare mir Kommentare (ausser Du hast noch Zeit/Energie
867 %WN3 daf"ur und fragst extra nach).
869 % The use of rulesets makes it much easier to develop our designated applications,
870 % but the programmer has to be careful and patient. When applying rulesets
871 % two important issues have to be mentionend:
873 % \item How often the rules have to be applied? In case of
874 % transformations it is quite clear that we use them once but other fields
875 % reuqire to apply rules until a special condition is reached (e.g.
876 % a simplification is finished when there is nothing to be done left).
877 % \item The order in which rules are applied often takes a big effect
878 % and has to be evaluated for each purpose once again.
880 % In the special case of Signal Processing the rules defined in the
881 % Example upwards have to be applied in a dedicated order to transform all
882 % constants first of all. After this first transformation step has been done it no
883 % mather which rule fit's next.
885 %WN3 Beim Paper-Schreiben ist mir aufgefallen, dass eine Konstante ZZ_1
886 %WN3 (f"ur ${\cal Z}^{-1}$) die eben beschriebenen Probleme gel"ost
887 %WN3 h"atte: auf S.6 in rule1, auf S.12 in line 10 und in der Rechnung S.16
888 %WN3 hab' ich die Konstante schon eingef"uhrt.
890 %WN3 Bite bei der rewrite_set_ demo oben bitte schummeln !
892 %JR TODO es is klein z bitte auf S.6 in rule1, auf S.12 in line 10 ausbessern
896 In the first step of upper code we extend the method's own ruleset with
897 the predefined rules.\par
898 When adding rules to this set we already have to take care on the order the
899 rules we be applied in later context, this can be an important point when it
900 comes to a case where one rule has to be applied explicite before an other.
901 \par Rules are added to the ruleset with an unique name and a reference to their
902 defined theorem. After summerizing this rules we still have the posibility to
903 pick out a single one.
904 \par In upper example we define an expression, as it comes up in our running
905 example, it can be useful to take a look at \S\ref{funs} on p.\pageref{funs} to
906 get to know {\sisac}'s' internal representation of variables.
907 \par Upper step three is the final use of a ruleset for rewriting expression.
908 The inline declared \ttfamily sample\_term' \normalfont is the result of applying the upper
909 rule set one time to the before defined \texttt{sample\_term'}.
912 \subsection{Preparation of ML-Functions}\label{funs}
913 Some functionality required in programming, cannot be accomplished by
914 rewriting. So the prototype has a mechanism to call functions within
915 the rewrite-engine: certain redexes in Isabelle terms call these
916 functions written in SML~\cite{pl:milner97}, the implementation {\em
917 and} meta-language of Isabelle. The programmer has to use this
920 In the running example's program on p.\pageref{s:impl} the lines {\rm
921 05} and {\rm 06} contain such functions; we go into the details with
922 \textit{argument\_in X\_z;}. This function fetches the argument from a
923 function application: Line {\rm 03} in the example calculation on
924 p.\pageref{exp-calc} is created by line {\rm 06} of the example
925 program on p.\pageref{s:impl} where the program's environment assigns
926 the value \textit{X z} to the variable \textit{X\_z}; so the function
927 shall extract the argument \textit{z}.
929 \medskip In order to be recognised as a function constant in the
930 program source the constant needs to be declared in a theory, here in
931 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
932 the context \textit{ctxt} of that theory:
937 argument'_in :: "real => real" ("argument'_in _" 10)
940 %^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
941 %^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
942 %^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
943 %^3.2^ \end{verbatim}}
945 %^3.2^ \noindent Parsing produces a term \texttt{t} in internal
946 %^3.2^ representation~\footnote{The attentive reader realizes the
947 %^3.2^ differences between interal and extermal representation even in the
948 %^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
949 %^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
950 %^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
952 The function body below is implemented directly in SML,
953 i.e in an \texttt{ML \{* *\}} block; the function definition provides
954 a unique prefix \texttt{eval\_} to the function name:
959 fun eval_argument_in _
960 "Build_Inverse_Z_Transform.argument'_in"
961 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ =
962 if is_Free arg (*could be something to be simplified before*)
963 then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg)))
965 | eval_argument_in _ _ _ _ = NONE;
969 \noindent The function body creates either creates \texttt{NONE}
970 telling the rewrite-engine to search for the next redex, or creates an
971 ad-hoc theorem for rewriting, thus the programmer needs to adopt many
972 technicalities of Isabelle, for instance, the \textit{Trueprop}
975 \bigskip This sub-task particularly sheds light on basic issues in the
976 design of a programming language, the integration of diffent language
977 layers, the layer of Isabelle/Isar and Isabelle/ML.
979 Another point of improvement for the prototype is the rewrite-engine: The
980 program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
983 {\small\it\label{s:impl}
985 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
986 \>{\rm 05/6}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
989 \noindent because nested function calls would require creating redexes
990 inside-out; however, the prototype's rewrite-engine only works top down
991 from the root of a term down to the leaves.
993 How all these technicalities are to be checked in the prototype is
994 shown in \S\ref{flow-prep} below.
996 % \paragraph{Explicit Problems} require explicit methods to solve them, and within
997 % this methods we have some explicit steps to do. This steps can be unique for
998 % a special problem or refindable in other problems. No mather what case, such
999 % steps often require some technical functions behind. For the solving process
1000 % of the Inverse Z Transformation and the corresponding partial fraction it was
1001 % neccessary to build helping functions like \texttt{get\_denominator},
1002 % \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
1003 % to filter the denominator or numerator out of a fraction, last one helps us to
1004 % get to know the bound variable in a equation.
1006 % By taking \texttt{get\_denominator} as an example, we want to explain how to
1007 % implement new functions into the existing system and how we can later use them
1010 % \subsubsection{Find a place to Store the Function}
1012 % The whole system builds up on a well defined structure of Knowledge. This
1013 % Knowledge sets up at the Path:
1014 % \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
1015 % For implementing the Function \texttt{get\_denominator} (which let us extract
1016 % the denominator out of a fraction) we have choosen the Theory (file)
1017 % \texttt{Rational.thy}.
1019 % \subsubsection{Write down the new Function}
1021 % In upper Theory we now define the new function and its purpose:
1023 % get_denominator :: "real => real"
1025 % This command tells the machine that a function with the name
1026 % \texttt{get\_denominator} exists which gets a real expression as argument and
1027 % returns once again a real expression. Now we are able to implement the function
1028 % itself, upcoming example now shows the implementation of
1029 % \texttt{get\_denominator}.
1032 % \label{eg:getdenom}
1036 % 02 *("get_denominator",
1037 % 03 * ("Rational.get_denominator", eval_get_denominator ""))
1039 % 05 fun eval_get_denominator (thmid:string) _
1040 % 06 (t as Const ("Rational.get_denominator", _) $
1041 % 07 (Const ("Rings.inverse_class.divide", _) $num
1043 % 09 SOME (mk_thmid thmid ""
1044 % 10 (Print_Mode.setmp []
1045 % 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1046 % 12 Trueprop $ (mk_equality (t, denom)))
1047 % 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
1050 % Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
1051 % there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
1053 % into its two parts (\texttt{\$num \$denom}). The lines before are additionals
1054 % commands for declaring the function and the lines after are modeling and
1055 % returning a real variable out of \texttt{\$denom}.
1057 % \subsubsection{Add a test for the new Function}
1059 % \paragraph{Everytime when adding} a new function it is essential also to add
1060 % a test for it. Tests for all functions are sorted in the same structure as the
1061 % knowledge it self and can be found up from the path:
1062 % \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
1063 % This tests are nothing very special, as a first prototype the functionallity
1064 % of a function can be checked by evaluating the result of a simple expression
1065 % passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
1066 % \textit{just} created function \texttt{get\_denominator}.
1069 % \label{eg:getdenomtest}
1072 % 01 val thy = @{theory Isac};
1073 % 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1074 % 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1075 % 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1076 % 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
1079 % \begin{description}
1080 % \item[01] checks if the proofer set up on our {\sisac{}} System.
1081 % \item[02] passes a simple expression (fraction) to our suddenly created
1083 % \item[04] checks if the resulting variable is the correct one (in this case
1084 % ``b'' the denominator) and returns.
1085 % \item[05] handels the error case and reports that the function is not able to
1086 % solve the given problem.
1089 \subsection{Specification of the Problem}\label{spec}
1090 %WN <--> \chapter 7 der Thesis
1091 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1093 Mechanical treatment requires to translate a textual problem
1094 description like in Fig.\ref{fig-interactive} on
1095 p.\pageref{fig-interactive} into a {\em formal} specification. The
1096 formal specification of the running example could look like is this:
1098 %WN Hier brauchen wir die Spezifikation des 'running example' ...
1099 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1100 %JR der post condition - die existiert für uns ja eigentlich nicht aka
1101 %JR haben sie bis jetzt nicht beachtet WN...
1102 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1106 {\small\begin{tabbing}
1107 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1110 \> \>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}\}$\\
1111 \>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
1112 \>\>output \>: stepResponse $x[n]$ \\
1113 \>\>postcond \>: TODO
1116 %JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt"
1119 % Defining the postcondition requires a high amount mathematical
1120 % knowledge, the difficult part in our case is not to set up this condition
1121 % nor it is more to define it in a way the interpreter is able to handle it.
1122 % Due the fact that implementing that mechanisms is quite the same amount as
1123 % creating the programm itself, it is not avaible in our prototype.
1124 % \label{rm:postcond}
1127 The implementation of the formal specification in the present
1128 prototype, still bar-bones without support for authoring, is done
1130 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1132 {\footnotesize\label{exp-spec}
1135 01 store_specification
1136 02 (prepare_specification
1137 03 "pbl_SP_Ztrans_inv"
1140 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1141 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1142 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1143 09 ("#Find" , ["stepResponse n_eq"]),
1144 10 ("#Post" , [" TODO "])])
1147 13 [["SignalProcessing","Z_Transform","Inverse"]]);
1151 Although the above details are partly very technical, we explain them
1152 in order to document some intricacies of TP-based programming in the
1153 present state of the {\sisac} prototype:
1155 \item[01..02]\textit{store\_specification:} stores the result of the
1156 function \textit{prep\_specification} in a global reference
1157 \textit{Unsynchronized.ref}, which causes principal conflicts with
1158 Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
1159 parallel execution~\cite{Makarius-09:parall-proof} and is under
1160 reconstruction already.
1162 \textit{prep\_specification:} translates the specification to an internal format
1163 which allows efficient processing; see for instance line {\rm 07}
1165 \item[03..04] are a unique identifier for the specification within {\sisac}
1166 and the ``mathematics author'' holding the copy-rights.
1167 \item[05] is the Isabelle \textit{theory} required to parse the
1168 specification in lines {\rm 07..10}.
1169 \item[06] is a key into the tree of all specifications as presented to
1170 the user (where some branches might be hidden by the dialog
1172 \item[07..10] are the specification with input, pre-condition, output
1173 and post-condition respectively; note that the specification contains
1174 variables to be instantiated with concrete values for a concrete problem ---
1175 thus the specification actually captures a class of problems. The post-condition is not handled in
1176 the prototype presently.
1177 \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
1178 rewriting determined by rule-sets.
1179 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1180 problem associated to a function from Computer Algebra (like an
1181 equation solver) which is not the case here.
1182 \item[13] is a list of methods solving the specified problem (here
1183 only one list item) represented analogously to {\rm 06}.
1187 %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1190 % {guh : guh, (*unique within this isac-knowledge*)
1191 % mathauthors: string list, (*copyright*)
1192 % init : pblID, (*to start refinement with*)
1193 % thy : theory, (* which allows to compile that pbt
1194 % TODO: search generalized for subthy (ref.p.69*)
1195 % (*^^^ WN050912 NOT used during application of the problem,
1196 % because applied terms may be from 'subthy' as well as from super;
1197 % thus we take 'maxthy'; see match_ags !*)
1198 % cas : term option,(*'CAS-command'*)
1199 % prls : rls, (* for preds in where_*)
1200 % where_: term list, (* where - predicates*)
1202 % (*this is the model-pattern;
1203 % it contains "#Given","#Where","#Find","#Relate"-patterns
1204 % for constraints on identifiers see "fun cpy_nam"*)
1205 % met : metID list}; (* methods solving the pbt*)
1207 %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1208 %WN oben selbst geschrieben.
1213 %WN das w"urde ich in \sec\label{progr} verschieben und
1214 %WN das SubProblem partial fractions zum Erkl"aren verwenden.
1215 % Such a specification is checked before the execution of a program is
1216 % started, the same applies for sub-programs. In the following example
1217 % (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1221 % \label{eg:subprob}
1223 % {\ttfamily \begin{tabbing}
1224 % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
1225 % ``\>\>[linear,univariate,equation,test],'' \\
1226 % ``\>\>[Test,solve\_linear])'' \\
1227 % ``\>[BOOL equ, REAL z])'' \\
1231 % \noindent If a program requires a result which has to be
1232 % calculated first we can use a subproblem to do so. In our specific
1233 % case we wanted to calculate the zeros of a fraction and used a
1234 % subproblem to calculate the zeros of the denominator polynom.
1239 \subsection{Implementation of the Method}\label{meth}
1240 A method collects all data required to interpret a certain program by
1241 Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
1242 the running example is embedded on the last line in the following method:
1243 %The methods represent the different ways a problem can be solved. This can
1244 %include mathematical tactics as well as tactics taught in different courses.
1245 %Declaring the Method itself gives us the possibilities to describe the way of
1246 %calculation in deep, as well we get the oppertunities to build in different
1254 03 "SP_InverseZTransformation_classic"
1257 06 ( ["SignalProcessing", "Z_Transform", "Inverse"],
1258 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1259 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1260 09 ("#Find" , ["stepResponse n_eq"]),
1268 \noindent The above code stores the whole structure analogously to a
1269 specification as described above:
1271 \item[01..06] are identical to those for the example specification on
1272 p.\pageref{exp-spec}.
1274 \item[07..09] show something looking like the specification; this is a
1275 {\em guard}: as long as not all \textit{Given} items are present and
1276 the \textit{Pre}-conditions is not true, interpretation of the program
1279 \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
1280 \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
1281 \textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
1282 \textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analoguous to the specification in line 11 on p.\pageref{exp-spec}
1283 and (c) is required for the derivation-machinery checking user-input formulas.
1285 \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}.
1287 The many rule-sets above cause considerable efforts for the
1288 programmers, in particular, because there are no tools for checking
1289 essential features of rule-sets.
1291 % is again very technical and goes hard in detail. Unfortunataly
1292 % most declerations are not essential for a basic programm but leads us to a huge
1293 % range of powerful possibilities.
1295 % \begin{description}
1296 % \item[01..02] stores the method with the given name into the system under a global
1298 % \item[03] specifies the topic within which context the method can be found.
1299 % \item[04..05] as the requirements for different methods can be deviant we
1300 % declare what is \emph{given} and and what to \emph{find} for this specific method.
1301 % The code again helds on the topic of the case studie, where the inverse
1302 % z-transformation does a switch between a term describing a electrical filter into
1303 % its step response. Also the datatype has to be declared (bool - due the fact that
1304 % we handle equations).
1305 % \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
1306 % theorem of it is used for rewriting one single step.
1307 % \item[07] \texttt{rls} is the currently used ruleset for this method. This set
1308 % has already been defined before.
1309 % \item[08] we would have the possiblitiy to add this method to a predefined tree of
1310 % calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
1312 % \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
1314 % \item[10] \emph{predicates ruleset} can be used to indicates predicates within
1316 % \item[11] The \emph{check ruleset} summarizes rules for checking formulas
1318 % \item[12] \emph{error patterns} which are expected in this kind of method can be
1319 % pre-specified to recognize them during the method.
1320 % \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
1321 % of the specific method.
1322 % \item[14] for this code snipset we don't specify the programm itself and keep it
1323 % empty. Follow up \S\ref{progr} for informations on how to implement this
1324 % \textit{main} part.
1327 \subsection{Implementation of the TP-based Program}\label{progr}
1328 So finally all the prerequisites are described and the final task can
1329 be addressed. The program below comes back to the running example: it
1330 computes a solution for the problem from Fig.\ref{fig-interactive} on
1331 p.\pageref{fig-interactive}. The reader is reminded of
1332 \S\ref{PL-isab}, the introduction of the programming language:
1334 {\footnotesize\it\label{s:impl}
1336 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1337 \>{\rm 00}\>ML \{*\\
1338 \>{\rm 00}\>val program =\\
1339 \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1340 \>{\rm 02}\>\> {\tt let} \\
1341 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1342 \>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
1343 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1344 \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1345 \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1346 \>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
1347 %\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
1348 \>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1349 \>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1350 \>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@ \\
1351 \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1352 \>{\rm 13}\>\> {\tt in } \\
1353 \>{\rm 14}\>\>\> X'\_eq"\\
1356 % ORIGINAL FROM Inverse_Z_Transform.thy
1357 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1358 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1359 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1360 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1361 % " (zzz::real) = argument_in X'_z; "^(* z *)
1362 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1364 % " (pbz::real) = (SubProblem (Isac', "^(**)
1365 % " [partial_fraction,rational,simplification], "^
1366 % " [simplification,of_rationals,to_partial_fraction]) "^
1367 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1369 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1370 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1371 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1372 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1373 % " 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]*)
1374 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1375 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1376 The program is represented as a string and part of the method in
1377 \S\ref{meth}. As mentioned in \S\ref{PL} the program is purely
1378 functional and lacks any input statements and output statements. So
1379 the steps of calculation towards a solution (and interactive tutoring
1380 in step-wise problem solving) are created as a side-effect by
1381 Lucas-Interpretation. The side-effects are triggered by the tactics
1382 \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
1383 \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1384 {\rm 12} respectively. These tactics produce the respective lines in the
1385 calculation on p.\pageref{flow-impl}.
1387 The above lines {\rm 05, 06} do not contain a tactics, so they do not
1388 immediately contribute to the calculation on p.\pageref{flow-impl};
1389 rather, they compute actual arguments for the \texttt{SubProblem} in
1390 line {\rm 09}~\footnote{The tactics also are break-points for the
1391 interpreter, where control is handed over to the user in interactive
1392 tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
1394 \medskip The above program also indicates the dominant role of interactive
1395 selection of knowledge in the three-dimensional universe of
1396 mathematics as depicted in Fig.\ref{fig:mathuni} on
1397 p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines
1398 {\rm 07..09} is more than a function call with the actual arguments
1399 \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
1403 \item the theory, in the example \textit{Isac} because different
1404 methods can be selected in Pt.3 below, which are defined in different
1405 theories with \textit{Isac} collecting them.
1406 \item the specification identified by \textit{[partial\_fraction,
1407 rational, simplification]} in the tree of specifications; this
1408 specification is analogous to the specification of the main program
1409 described in \S\ref{spec}; the problem is to find a ``partial fraction
1410 decomposition'' for a univariate rational polynomial.
1411 \item the method in the above example is \textit{[ ]}, i.e. empty,
1412 which supposes the interpreter to select one of the methods predefined
1413 in the specification, for instance in line {\rm 13} in the running
1414 example's specification on p.\pageref{exp-spec}~\footnote{The freedom
1415 (or obligation) for selection carries over to the student in
1416 interactive tutoring.}.
1419 The program code, above presented as a string, is parsed by Isabelle's
1420 parser --- the program is an Isabelle term. This fact is expected to
1421 simplify verification tasks in the future; on the other hand, this
1422 fact causes troubles in error detectetion which are discussed as part
1423 of the workflow in the subsequent section.
1425 \section{Workflow of Programming in the Prototype}\label{workflow}
1426 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
1427 step forward for interactive theory and proof development. The
1428 {\sisac}-prototype re-uses this IDE as a programming environment. The
1429 experiences from this re-use show, that the essential components are
1430 available from Isabelle/jEdit. However, additional tools and features
1431 are required to acchieve acceptable usability.
1433 So notable experiences are reported here, also as a requirement
1434 capture for further development of TP-based languages and respective
1437 \subsection{Preparations and Trials}\label{flow-prep}
1438 The many sub-tasks to be accomplished {\em before} the first line of
1439 program code can be written and tested suggest an approach which
1440 step-wise establishes the prerequisites. The case study underlying
1441 this paper~\cite{jrocnik-bakk} documents the approach in a separate
1443 \textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
1444 II in the study comprises this theory, \LaTeX ed from the theory by
1445 use of Isabelle's document preparation system. This paper resembles
1446 the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
1447 implementation work involves several iterations.
1449 \bigskip For instance, only the last step, implementing the program
1450 described in \S\ref{meth}, reveals details required. Let us assume,
1451 this is the ML-function \textit{argument\_in} required in line {\rm 06}
1452 of the example program on p.\pageref{s:impl}; how this function needs
1453 to be implemented in the prototype has been discussed in \S\ref{funs}
1456 Now let us assume, that calling this function from the program code
1457 does not work; so testing this function is required in order to find out
1458 the reason: type errors, a missing entry of the function somewhere or
1459 even more nasty technicalities \dots
1464 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1465 val SOME (str, t') = eval_argument_in ""
1466 "Build_Inverse_Z_Transform.argument'_in" t 0;
1471 val it = "(argument_in X z) = z": string
1474 \noindent So, this works: we get an ad-hoc theorem, which used in
1475 rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
1476 reduction and create a rule-set \texttt{rls} for that purpose:
1481 val rls = append_rls "test" e_rls
1482 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1485 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1487 val t' = Free ("z", "RealDef.real"): term
1488 val asm = []: term list
1491 \noindent The resulting term \texttt{t'} is \texttt{Free ("z",
1492 "RealDef.real")}, i.e the variable \texttt{z}, so all is
1493 perfect. Probably we have forgotten to store this function correctly~?
1494 We review the respective \texttt{calclist} (again an
1495 \textit{Unsynchronized.ref} to be removed in order to adjust to
1496 IsabelleIsar's asyncronous document model):
1500 calclist:= overwritel (! calclist,
1501 [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1506 \noindent The entry is perfect. So what is the reason~? Ah, probably there
1507 is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1508 right, the function \texttt{argument\_in} is not contained in the respective
1509 rule-set \textit{srls} \dots this just as an example of the intricacies in
1510 debugging a program in the present state of the prototype.
1512 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1513 Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
1514 usually developed within several iterations, the program can be
1515 assembled; on p.\pageref{s:impl} there is the complete program of the
1518 The completion of this program required efforts for several weeks
1519 (after some months of familiarisation with {\sisac}), caused by the
1520 abundance of intricacies indicated above. Also writing the program is
1521 not pleasant, given Isabelle/Isar/ without add-ons for
1522 programming. Already writing and parsing a few lines of program code
1523 is a challenge: the program is an Isabelle term; Isabelle's parser,
1524 however, is not meant for huge terms like the program of the running
1525 example. So reading out the specific error (usually type errors) from
1526 Isabelle's message is difficult.
1528 \medskip Testing the evaluation of the program has to rely on very
1529 simple tools. Step-wise execution is modelled by a function
1530 \texttt{me}, short for mathematics-engine~\footnote{The interface used
1531 by the fron-end which created the calculation on
1532 p.\pageref{fig-interactive} is different from this function}:
1533 %the following is a simplification of the actual function
1538 val it = tac -> ctree * pos -> mout * tac * ctree * pos
1541 \noindent This function takes as arguments a tactic \texttt{tac} which
1542 determines the next step, the step applied to the interpreter-state
1543 \texttt{ctree * pos} as last argument taken. The interpreter-state is
1544 a pair of a tree \texttt{ctree} representing the calculation created
1545 (see the example below) and a position \texttt{pos} in the
1546 calculation. The function delivers a quadrupel, beginning with the new
1547 formula \texttt{mout} and the next tactic followed by the new
1550 This function allows to stepwise check the program:
1556 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1557 "stepResponse (x[n::real]::bool)"];
1560 ["Inverse", "Z_Transform", "SignalProcessing"],
1561 ["SignalProcessing","Z_Transform","Inverse"]);
1563 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1564 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1565 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1566 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1570 \noindent Several douzens of calls for \texttt{me} are required to
1571 create the lines in the calculation below (including the sub-problems
1572 not shown). When an error occurs, the reason might be located
1573 many steps before: if evaluation by rewriting, as done by the prototype,
1574 fails, then first nothing happens --- the effects come later and
1575 cause unpleasant checks.
1577 The checks comprise watching the rewrite-engine for many different
1578 kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
1579 particular the environment and the context at the states position ---
1580 all checks have to rely on simple functions accessing the
1581 \texttt{ctree}. So getting the calculation below (which resembles the
1582 calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
1583 is the result of several weeks of development:
1585 {\small\it\label{exp-calc}
1587 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1588 \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1589 \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
1590 \>{\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}\\
1591 \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
1592 \>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
1593 \>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
1594 \>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
1595 \>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
1596 \>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
1597 \>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
1598 \> \>\>\>\> \_\_\_ \`- - -\\
1599 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1600 \>{\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)}\\
1601 \>{\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 }\\
1602 \>{\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}\\
1603 \>{\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}}
1605 The tactics on the right margin of the above calculation are those in
1606 the program on p.\pageref{s:impl} which create the respective formulas
1608 % ORIGINAL FROM Inverse_Z_Transform.thy
1609 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1610 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1611 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1612 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1613 % " (zzz::real) = argument_in X'_z; "^(* z *)
1614 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1616 % " (pbz::real) = (SubProblem (Isac', "^(**)
1617 % " [partial_fraction,rational,simplification], "^
1618 % " [simplification,of_rationals,to_partial_fraction]) "^
1619 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1621 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1622 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1623 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1624 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1625 % " 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]*)
1626 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1627 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1629 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1630 Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
1631 and the knowledge accumulated in it can be distributed to appropriate
1632 theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
1633 sub-problem accomplishing the partial fraction decomposition to
1634 \textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
1635 internals, this kind of distribution is not trivial. For instance, the
1636 function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
1637 string with the theory it has been defined in, so this string needs to
1638 be updated from \texttt{Build\_Inverse\_Z\_Transform} to
1639 \texttt{Atools} if that function is transferred to theory
1640 \textit{Atools.thy}.
1642 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.
1643 This process is also rather bare-bones without authoring tools and is
1644 described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
1647 % -------------------------------------------------------------------
1649 % Material, falls noch Platz bleibt ...
1651 % -------------------------------------------------------------------
1654 % \subsubsection{Trials on Notation and Termination}
1656 % \paragraph{Technical notations} are a big problem for our piece of software,
1657 % but the reason for that isn't a fault of the software itself, one of the
1658 % troubles comes out of the fact that different technical subtopics use different
1659 % symbols and notations for a different purpose. The most famous example for such
1660 % a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1661 % math). In the specific part of signal processing one of this notation issues is
1662 % the use of brackets --- we use round brackets for analoge signals and squared
1663 % brackets for digital samples. Also if there is no problem for us to handle this
1664 % fact, we have to tell the machine what notation leads to wich meaning and that
1665 % this purpose seperation is only valid for this special topic - signal
1667 % \subparagraph{In the programming language} itself it is not possible to declare
1668 % fractions, exponents, absolutes and other operators or remarks in a way to make
1669 % them pretty to read; our only posssiblilty were ASCII characters and a handfull
1670 % greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1672 % With the upper collected knowledge it is possible to check if we were able to
1673 % donate all required terms and expressions.
1675 % \subsubsection{Definition and Usage of Rules}
1677 % \paragraph{The core} of our implemented problem is the Z-Transformation, due
1678 % the fact that the transformation itself would require higher math which isn't
1679 % yet avaible in our system we decided to choose the way like it is applied in
1680 % labratory and problem classes at our university - by applying transformation
1681 % rules (collected in transformation tables).
1682 % \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1683 % use of axiomatizations like shown in Example~\ref{eg:ruledef}
1686 % \label{eg:ruledef}
1689 % axiomatization where
1690 % rule1: ``1 = $\delta$[n]'' and
1691 % rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1692 % rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1696 % This rules can be collected in a ruleset and applied to a given expression as
1697 % follows in Example~\ref{eg:ruleapp}.
1701 % \label{eg:ruleapp}
1703 % \item Store rules in ruleset:
1705 % val inverse_Z = append_rls "inverse_Z" e_rls
1706 % [ Thm ("rule1",num_str @{thm rule1}),
1707 % Thm ("rule2",num_str @{thm rule2}),
1708 % Thm ("rule3",num_str @{thm rule3})
1710 % \item Define exression:
1712 % val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1713 % \item Apply ruleset:
1715 % val SOME (sample_term', asm) =
1716 % rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1720 % The use of rulesets makes it much easier to develop our designated applications,
1721 % but the programmer has to be careful and patient. When applying rulesets
1722 % two important issues have to be mentionend:
1723 % \subparagraph{How often} the rules have to be applied? In case of
1724 % transformations it is quite clear that we use them once but other fields
1725 % reuqire to apply rules until a special condition is reached (e.g.
1726 % a simplification is finished when there is nothing to be done left).
1727 % \subparagraph{The order} in which rules are applied often takes a big effect
1728 % and has to be evaluated for each purpose once again.
1730 % In our special case of Signal Processing and the rules defined in
1731 % Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1732 % constants. After this step has been done it no mather which rule fit's next.
1734 % \subsubsection{Helping Functions}
1736 % \paragraph{New Programms require,} often new ways to get through. This new ways
1737 % means that we handle functions that have not been in use yet, they can be
1738 % something special and unique for a programm or something famous but unneeded in
1739 % the system yet. In our dedicated example it was for example neccessary to split
1740 % a fraction into numerator and denominator; the creation of such function and
1741 % even others is described in upper Sections~\ref{simp} and \ref{funs}.
1743 % \subsubsection{Trials on equation solving}
1744 % %simple eq and problem with double fractions/negative exponents
1745 % \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
1746 % equations degree one and two. Solving equations in the first degree is no
1747 % problem, wether for a student nor for our machine; but even second degree
1748 % equations can lead to big troubles. The origin of this troubles leads from
1749 % the build up process of our equation solving functions; they have been
1750 % implemented some time ago and of course they are not as good as we want them to
1751 % be. Wether or not following we only want to show how cruel it is to build up new
1752 % work on not well fundamentials.
1753 % \subparagraph{A simple equation solving,} can be set up as shown in the next
1760 % ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
1764 % val (dI',pI',mI') =
1766 % ["abcFormula","degree_2","polynomial","univariate","equation"],
1767 % ["no_met"]);\end{verbatim}
1770 % Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
1771 % a short overview on the commands; at first we set up the equation and tell the
1772 % machine what's the bound variable and where to store the solution. Second step
1773 % is to define the equation type and determine if we want to use a special method
1774 % to solve this type.) Simple checks tell us that the we will get two results for
1775 % this equation and this results will be real.
1776 % So far it is easy for us and for our machine to solve, but
1777 % mentioned that a unvariate equation second order can have three different types
1778 % of solutions it is getting worth.
1779 % \subparagraph{The solving of} all this types of solutions is not yet supported.
1780 % Luckily it was needed for us; but something which has been needed in this
1781 % context, would have been the solving of an euation looking like:
1782 % $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
1783 % before (remember that befor it was no problem to handle for the machine) but
1784 % now, after a simple equivalent transformation, we are not able to solve
1786 % \subparagraph{Error messages} we get when we try to solve something like upside
1787 % were very confusing and also leads us to no special hint about a problem.
1788 % \par The fault behind is, that we have no well error handling on one side and
1789 % no sufficient formed equation solving on the other side. This two facts are
1790 % making the implemention of new material very difficult.
1792 % \subsection{Formalization of missing knowledge in Isabelle}
1794 % \paragraph{A problem} behind is the mechanization of mathematic
1795 % theories in TP-bases languages. There is still a huge gap between
1796 % these algorithms and this what we want as a solution - in Example
1797 % Signal Processing.
1803 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1806 % \noindent A very simple example on this what we call gap is the
1807 % simplification above. It is needles to say that it is correct and also
1808 % Isabelle for fills it correct - \emph{always}. But sometimes we don't
1809 % want expand such terms, sometimes we want another structure of
1810 % them. Think of a problem were we now would need only the coefficients
1811 % of $X$ and $Y$. This is what we call the gap between mechanical
1812 % simplification and the solution.
1817 % \paragraph{We are not able to fill this gap,} until we have to live
1818 % with it but first have a look on the meaning of this statement:
1819 % Mechanized math starts from mathematical models and \emph{hopefully}
1820 % proceeds to match physics. Academic engineering starts from physics
1821 % (experimentation, measurement) and then proceeds to mathematical
1822 % modeling and formalization. The process from a physical observance to
1823 % a mathematical theory is unavoidable bound of setting up a big
1824 % collection of standards, rules, definition but also exceptions. These
1825 % are the things making mechanization that difficult.
1834 % \noindent Think about some units like that one's above. Behind
1835 % each unit there is a discerning and very accurate definition: One
1836 % Meter is the distance the light travels, in a vacuum, through the time
1837 % of 1 / 299.792.458 second; one kilogram is the weight of a
1838 % platinum-iridium cylinder in paris; and so on. But are these
1839 % definitions usable in a computer mechanized world?!
1844 % \paragraph{A computer} or a TP-System builds on programs with
1845 % predefined logical rules and does not know any mathematical trick
1846 % (follow up example \ref{eg:trick}) or recipe to walk around difficult
1852 % \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1853 % \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1854 % \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1855 % \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1857 % \noindent Sometimes it is also useful to be able to apply some
1858 % \emph{tricks} to get a beautiful and particularly meaningful result,
1859 % which we are able to interpret. But as seen in this example it can be
1860 % hard to find out what operations have to be done to transform a result
1861 % into a meaningful one.
1866 % \paragraph{The only possibility,} for such a system, is to work
1867 % through its known definitions and stops if none of these
1868 % fits. Specified on Signal Processing or any other application it is
1869 % often possible to walk through by doing simple creases. This creases
1870 % are in general based on simple math operational but the challenge is
1871 % to teach the machine \emph{all}\footnote{Its pride to call it
1872 % \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1873 % reach a high level of \emph{all} but it in real it will still be a
1874 % survey of knowledge which links to other knowledge and {{\sisac}{}} a
1875 % trainer and helper but no human compensating calculator.
1877 % {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1878 % specifications of problems out of topics from Signal Processing, etc.)
1879 % and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1880 % physical knowledge. The result is a three-dimensional universe of
1881 % mathematics seen in Figure~\ref{fig:mathuni}.
1885 % \includegraphics{fig/universe}
1886 % \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1887 % combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1888 % leads to a three dimensional math universe.\label{fig:mathuni}}
1892 % %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1893 % %WN bitte folgende Bezeichnungen nehmen:
1895 % %WN axis 1: Algorithmic Knowledge (Programs)
1896 % %WN axis 2: Application-oriented Knowledge (Specifications)
1897 % %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1899 % %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1900 % %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1901 % %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1903 % %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1904 % %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1905 % %JR gefordert werden WN2...
1906 % %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1907 % %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1908 % %WN2 zusammenschneiden um die R"ander weg zu bekommen)
1909 % %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1910 % %WN2 png + pdf figures mitzuschicken.
1912 % \subsection{Notes on Problems with Traditional Notation}
1914 % \paragraph{During research} on these topic severely problems on
1915 % traditional notations have been discovered. Some of them have been
1916 % known in computer science for many years now and are still unsolved,
1917 % one of them aggregates with the so called \emph{Lambda Calculus},
1918 % Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1925 % \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1928 % \[ f(p)=\ldots\; p \in \quad R \]
1931 % \noindent Above we see two equations. The first equation aims to
1932 % be a mapping of an function from the reel range to the reel one, but
1933 % when we change only one letter we get the second equation which
1934 % usually aims to insert a reel point $p$ into the reel function. In
1935 % computer science now we have the problem to tell the machine (TP) the
1936 % difference between this two notations. This Problem is called
1937 % \emph{Lambda Calculus}.
1942 % \paragraph{An other problem} is that terms are not full simplified in
1943 % traditional notations, in {{\sisac}} we have to simplify them complete
1944 % to check weather results are compatible or not. in e.g. the solutions
1945 % of an second order linear equation is an rational in {{\sisac}} but in
1946 % tradition we keep fractions as long as possible and as long as they
1947 % aim to be \textit{beautiful} (1/8, 5/16,...).
1948 % \subparagraph{The math} which should be mechanized in Computer Theorem
1949 % Provers (\emph{TP}) has (almost) a problem with traditional notations
1950 % (predicate calculus) for axioms, definitions, lemmas, theorems as a
1951 % computer program or script is not able to interpret every Greek or
1952 % Latin letter and every Greek, Latin or whatever calculations
1953 % symbol. Also if we would be able to handle these symbols we still have
1954 % a problem to interpret them at all. (Follow up \hbox{Example
1955 % \ref{eg:symbint1}})
1959 % \label{eg:symbint1}
1961 % u\left[n\right] \ \ldots \ unitstep
1964 % \noindent The unitstep is something we need to solve Signal
1965 % Processing problem classes. But in {{{\sisac}{}}} the rectangular
1966 % brackets have a different meaning. So we abuse them for our
1967 % requirements. We get something which is not defined, but usable. The
1968 % Result is syntax only without semantic.
1973 % In different problems, symbols and letters have different meanings and
1974 % ask for different ways to get through. (Follow up \hbox{Example
1975 % \ref{eg:symbint2}})
1979 % \label{eg:symbint2}
1981 % \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1984 % \noindent For using exponents the three \texttt{widehat} symbols
1985 % are required. The reason for that is due the development of
1986 % {{{\sisac}{}}} the single \texttt{widehat} and also the double were
1987 % already in use for different operations.
1992 % \paragraph{Also the output} can be a problem. We are familiar with a
1993 % specified notations and style taught in university but a computer
1994 % program has no knowledge of the form proved by a professor and the
1995 % machines themselves also have not yet the possibilities to print every
1996 % symbol (correct) Recent developments provide proofs in a human
1997 % readable format but according to the fact that there is no money for
1998 % good working formal editors yet, the style is one thing we have to
2001 % \section{Problems rising out of the Development Environment}
2003 % fehlermeldungen! TODO
2005 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
2007 \section{Conclusion}\label{conclusion}
2008 This paper gives a first experience report about programming with a
2009 TP-based programming language.
2011 \medskip A brief re-introduction of the novel kind of programming
2012 language by example of the {\sisac}-prototype makes the paper
2013 self-contained. The main section describes all the main concepts
2014 involved in TP-based programming and all the sub-tasks concerning
2015 respective implementation: mechanisation of mathematics and domain
2016 modelling, implementation of term rewriting systems for the
2017 rewriting-engine, formal (implicit) specification of the problem to be
2018 (explicitly) described by the program, implementation of the many components
2019 required for Lucas-Interpretation and finally implementation of the
2022 The many concepts and sub-tasks involved in programming require a
2023 comprehensive workflow; first experiences with the workflow as
2024 supported by the present prototype are described as well: Isabelle +
2025 Isar + jEdit provide appropriate components for establishing an
2026 efficient development environment integrating computation and
2027 deduction. However, the present state of the prototype is far off a
2028 state appropriate for wide-spread use: the prototype of the program
2029 language lacks expressiveness and elegance, the prototype of the
2030 development environment is hardly usable: error messages still address
2031 the developer of the prototype's interpreter rather than the
2032 application programmer, implementation of the many settings for the
2033 Lucas-Interpreter is cumbersome.
2035 From these experiences a successful proof of concept can be concluded:
2036 programming arbitrary problems from engineering sciences is possible,
2037 in principle even in the prototype. Furthermore the experiences allow
2038 to conclude detailed requirements for further development:
2040 \item Clarify underlying logics such that programming is smoothly
2041 integrated with verification of the program; the post-condition should
2042 be proved more or less automatically, otherwise working engineers
2043 would not encounter such programming.
2044 \item Combine the prototype's programming language with Isabelle's
2045 powerful function package and probably with more of SML's
2046 pattern-matching features; include parallel execution on multi-core
2047 machines into the language desing.
2048 \item Extend the prototype's Lucas-Interpreter such that it also
2049 handles functions defined by use of Isabelle's functions package; and
2050 generalize Isabelle's code generator such that efficient code for the
2051 whole definition of the programming language can be generated (for
2052 multi-core machines).
2053 \item Develop an efficient development environment with
2054 integration of programming and proving, with management not only of
2055 Isabelle theories, but also of large collections of specifications and
2058 Provided successful accomplishment, these points provide distinguished
2059 components for virtual workbenches appealing to practictioner of
2060 engineering in the near future.
2062 \medskip Interactive couse material, as addressed by the title, then
2063 can comprise step-wise problem solving created as a side-effect of a
2064 TP-based program: Lucas-Interpretation not only provides an
2065 interactive programming environment, Lucas-Interpretation also can
2066 provide TP-based services for a flexible dialog component with
2067 adaptive user guidance for independent and inquiry-based learning.
2070 \bibliographystyle{alpha}
2071 {\small\bibliography{references}}