1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 % Electronic Journal of Mathematics and Technology (eJMT) %
3 % style sheet for LaTeX. Please do not modify sections %
4 % or commands marked 'eJMT'. %
6 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10 \documentclass[12pt,a4paper]{article}% %
12 \usepackage{amsfonts,amsmath,amssymb} %
13 \usepackage[a4paper]{geometry} %
14 \usepackage{fancyhdr} %
16 \usepackage[pdftex]{hyperref} % see note below %
17 \usepackage{graphicx}% %
23 \newtheorem{theorem}{Theorem} %
24 \newtheorem{acknowledgement}[theorem]{Acknowledgement} %
25 \newtheorem{algorithm}[theorem]{Algorithm} %
26 \newtheorem{axiom}[theorem]{Axiom} %
27 \newtheorem{case}[theorem]{Case} %
28 \newtheorem{claim}[theorem]{Claim} %
29 \newtheorem{conclusion}[theorem]{Conclusion} %
30 \newtheorem{condition}[theorem]{Condition} %
31 \newtheorem{conjecture}[theorem]{Conjecture} %
32 \newtheorem{corollary}[theorem]{Corollary} %
33 \newtheorem{criterion}[theorem]{Criterion} %
34 \newtheorem{definition}[theorem]{Definition} %
35 \newtheorem{example}[theorem]{Example} %
36 \newtheorem{exercise}[theorem]{Exercise} %
37 \newtheorem{lemma}[theorem]{Lemma} %
38 \newtheorem{notation}[theorem]{Notation} %
39 \newtheorem{problem}[theorem]{Problem} %
40 \newtheorem{proposition}[theorem]{Proposition} %
41 \newtheorem{remark}[theorem]{Remark} %
42 \newtheorem{solution}[theorem]{Solution} %
43 \newtheorem{summary}[theorem]{Summary} %
44 \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } %
45 {\ \rule{0.5em}{0.5em}} %
47 % eJMT page dimensions %
49 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
51 % eJMT header & footer %
53 \newcounter{ejmtFirstpage} %
54 \setcounter{ejmtFirstpage}{1} %
56 \setlength{\headheight}{14pt} %
57 \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
58 \pagestyle{fancyplain} %
60 \fancyhead[c]{\small The Electronic Journal of Mathematics%
61 \ and Technology, Volume 1, Number 1, ISSN 1933-2823} %
63 \ifnum\value{ejmtFirstpage}=0% %
64 {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% %
65 \else\setcounter{ejmtFirstpage}{0}\fi% %
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
70 % Please place your own definitions here
72 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
73 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
76 \definecolor{lgray}{RGB}{238,238,238}
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 % How to use hyperref %
82 % ------------------- %
84 % Probably the only way you will need to use the hyperref %
85 % package is as follows. To make some text, say %
86 % "My Text Link", into a link to the URL %
87 % http://something.somewhere.com/mystuff, use %
89 % \href{http://something.somewhere.com/mystuff}{My Text Link}
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
97 \title{Trials with TP-based Programming
99 for Interactive Course Material}%
101 % Single author. Please supply at least your name,
102 % email address, and affiliation here.
104 \author{\begin{tabular}{c}
105 \textit{Jan Ro\v{c}nik} \\
106 jan.rocnik@student.tugraz.at \\
108 Graz University of Technologie\\
112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
114 % eJMT commands - do not change these %
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
125 Traditional course material in engineering disciplines lacks an
126 important component, interactive support for step-wise problem
127 solving. Theorem-Proving (TP) technology is appropriate for one part
128 of such support, in checking user-input. For the other part of such
129 support, guiding the learner towards a solution, another kind of
130 technology is required. %TODO ... connect to prototype ...
132 A prototype combines TP with a programming language, the latter
133 interpreted in a specific way: certain statements in a program, called
134 tactics, are treated as breakpoints where control is handed over to
135 the user. An input formula is checked by TP (using logical context
136 built up by the interpreter); and if a learner gets stuck, a program
137 describing the steps towards a solution of a problem ``knows the next
138 step''. This kind of interpretation is called Lucas-Interpretation for
139 \emph{TP-based programming languages}.
141 This paper describes the prototype's TP-based programming language
142 within a case study creating interactive material for an advanced
143 course in Signal Processing: implementation of definitions and
144 theorems in TP, formal specification of a problem and step-wise
145 development of the program solving the problem. Experiences with the
146 ork flow in iterative development with testing and identifying errors
147 are described, too. The description clarifies the components missing
148 in the prototype's language as well as deficiencies experienced during
151 These experiences are particularly notable, because the author is the
152 first programmer using the language beyond the core team which
153 developed the prototype's TP-based language interpreter.
157 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
161 \thispagestyle{fancy} %
163 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
165 % Please use the following to indicate sections, subsections,
166 % etc. Please also use \subsubsection{...}, \paragraph{...}
167 % and \subparagraph{...} as necessary.
170 \section{Introduction}\label{intro}
172 % \paragraph{Didactics of mathematics}
173 %WN: wenn man in einem high-quality paper von 'didactics' spricht,
174 %WN muss man am state-of-the-art ankn"upfen -- siehe
175 %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
176 % faces a specific issue, a gap
177 % between (1) introduction of math concepts and skills and (2)
178 % application of these concepts and skills, which usually are separated
179 % into different units in curricula (for good reasons). For instance,
180 % (1) teaching partial fraction decomposition is separated from (2)
181 % application for inverse Z-transform in signal processing.
183 % \par This gap is an obstacle for applying math as an fundamental
184 % thinking technology in engineering: In (1) motivation is lacking
185 % because the question ``What is this stuff good for?'' cannot be
186 % treated sufficiently, and in (2) the ``stuff'' is not available to
187 % students in higher semesters as widespread experience shows.
189 % \paragraph{Motivation} taken by this didactic issue on the one hand,
190 % and ongoing research and development on a novel kind of educational
191 % mathematics assistant at Graz University of
192 % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
193 % scope with this issue on the other hand, several institutes are
194 % planning to join their expertise: the Institute for Information
195 % Systems and Computer Media (IICM), the Institute for Software
196 % Technology (IST), the Institutes for Mathematics, the Institute for
197 % Signal Processing and Speech Communication (SPSC), the Institute for
198 % Structural Analysis and the Institute of Electrical Measurement and
199 % Measurement Signal Processing.
200 %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
201 %WN und damit zu verg"anglich.
202 % \par This thesis is the first attempt to tackle the above mentioned
203 % issue, it focuses on Telematics, because these specific studies focus
204 % on mathematics in \emph{STEOP}, the introductory orientation phase in
205 % Austria. \emph{STEOP} is considered an opportunity to investigate the
206 % impact of {\sisac}'s prototype on the issue and others.
209 \paragraph{Traditional course material} in engineering disciplines lacks an
210 important component, interactive support for step-wise problem
211 solving. Theorem-Proving (TP) technology can provide such support by
212 specific services. An important part of such services is called
213 ``next-step-guidance'', generated by a specific kind of ``TP-based
214 programming language''. In the
215 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
216 a language is prototyped in line with~\cite{plmms10} and built upon
218 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
219 The TP services are coordinated by a specific interpreter for the
220 programming language, called
221 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
222 interpreter will be briefly re-introduced in order to make the paper
225 \subparagraph{The main part} of the paper is an account of first experiences
226 with programming in this TP-based language. The experience was gained
227 in a case study by the author. The author was considered an ideal
228 candidate for this study for the following reasons: as a student in
229 Telematics (computer science with focus on Signal Processing) he had
230 general knowledge in programming as well as specific domain knowledge
231 in Signal Processing; and he was not involved in the development of
232 {\sisac}'s programming language and interpeter, thus a novice to the
235 \subparagraph{The goal} of the case study was (1) some TP-based programs for
236 interactive course material for a specific ``Adavanced Signal
237 Processing Lab'' in a higher semester, (2) respective program
238 development with as little advice from the {\sisac}-team and (3) records
239 and comments for the main steps of development in an Isabelle theory;
240 this theory should provide guidelines for future programmers. An
241 excerpt from this theory is the main part of this paper.
243 The paper will use the problem in Fig.\ref{fig-interactive} as a
247 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
248 %\includegraphics[width=140mm]{fig/isac-Ztrans-math}
249 \caption{Step-wise problem solving guided by the TP-based program}
250 \label{fig-interactive}
254 \paragraph{The problem is} from the domain of Signal Processing and requests to
255 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
256 also shows the beginning of the interactive construction of a solution
257 for the problem. This construction is done in the right window named
260 User-interaction on the Worksheet is {\em checked} and {\em guided} by
263 \item Formulas input by the user are {\em checked} by TP: such a
264 formula establishes a proof situation --- the prover has to derive the
265 formula from the logical context. The context is built up from the
266 formal specification of the problem (here hidden from the user) by the
268 \item If the user gets stuck, the program developed below in this
269 paper ``knows the next step'' from behind the scenes. How the latter
270 TP-service is exploited by dialogue authoring is out of scope of this
271 paper and can be studied in~\cite{gdaroczy-EP-13}.
272 \end{enumerate} It should be noted that the programmer using the
273 TP-based language is not concerned with interaction at all; we will
274 see that the program contains neither input-statements nor
275 output-statements. Rather, interaction is handled by services
276 generated automatically.
278 So there is a clear separation of concerns: Dialogues are
279 adapted by dialogue authors (in Java-based tools), using automatically
280 generated TP services, while the TP-based program is written by
281 mathematics experts (in Isabelle/ML). The latter is concern of this
284 \paragraph{The paper is structed} as follows: The introduction
285 \S\ref{intro} is followed by a brief re-introduction of the TP-based
286 programming language in \S\ref{PL}, which extends the executable
287 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
288 play a specific role in Lucas-Interpretation and in providing the TP
289 services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes
290 the main steps in developing the program for the running example:
291 prepare domain knowledge, implement the formal specification of the
292 problem, prepare the environment for the program, implement the
293 program. The workflow of programming, debugging and testing is
294 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
295 give directions identified for future development.
298 \section{\isac's Prototype for a Programming Language}\label{PL}
299 The prototype's language extends the executable fragment in the
300 language of the theorem prover
301 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}
302 by tactics which have a specific role in Lucas-Interpretation.
304 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
305 The executable fragment consists of data-type and function
306 definitions. It's usability even suggests that fragment for
307 introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
308 whose type system resembles that of functional programming
309 languages. Thus there are
311 \item[base types,] in particular \textit{bool}, the type of truth
312 values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
313 natural, integer and complex numbers respectively in mathematics.
314 \item[type constructors] allow to define arbitrary types, from
315 \textit{set}, \textit{list} to advanced data-structures like
316 \textit{trees}, red-black-trees etc.
317 \item[function types,] denoted by $\Rightarrow$.
318 \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
319 type polymorphism. Isabelle automatically computes the type of each
320 variable in a term by use of Hindley-Milner type inference
321 \cite{pl:hind97,Milner-78}.
324 \textbf{Terms} are formed as in functional programming by applying
325 functions to arguments. If $f$ is a function of type
326 $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
327 $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
328 has type $\tau$. There are many predefined infix symbols like $+$ and
329 $\leq$ most of which are overloaded for various types.
331 HOL also supports some basic constructs from functional programming:
332 {\it\label{isabelle-stmts}
333 \begin{tabbing} 123\=\kill
334 \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
335 \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
336 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
337 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
339 \noindent The running example's program uses some of these elements
340 (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
341 let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
342 is an Isabelle term with specific function constants like {\tt
343 program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
344 Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
347 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
348 % x. \; x$ is the identity function.
350 %JR warum auskommentiert? WN2...
351 %WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
352 %WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
353 %WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
355 %WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
356 %WN2 Platz f"ur Anderes weg.
358 \textbf{Formulae} are terms of type \textit{bool}. There are the basic
359 constants \textit{True} and \textit{False} and the usual logical
360 connectives (in decreasing order of precedence): $\neg, \land, \lor,
363 \textbf{Equality} is available in the form of the infix function $=$
364 of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
365 formulas, where it means ``if and only if''.
367 \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
368 P$. Quantifiers lead to non-executable functions, so functions do not
369 always correspond to programs, for instance, if comprising \\$(
370 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
373 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
374 The prototype extends Isabelle's language by specific statements
375 called tactics~\footnote{{\sisac}'s tactics are different from
376 Isabelle's tactics: the former concern steps in a calculation, the
377 latter concern proof steps.} and tacticals. For the programmer these
378 statements are functions with the following signatures:
381 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
382 term} * {\it term}\;{\it list}$:
383 this tactic appplies {\it theorem} to a {\it term} yielding a {\it
384 term} and a {\it term list}, the list are assumptions generated by
385 conditional rewriting. For instance, the {\it theorem}
386 $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
387 applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
388 $(\frac{2}{3}, [x\not=0])$.
390 \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
391 term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
392 this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
393 a confluent and terminating term rewrite system, in general. If
394 none of the rules ({\it theorem}s) is applicable on interpretation
395 of this tactic, an exception is thrown.
397 % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
398 % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
401 % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
402 % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
405 \item[Substitute:] ${\it substitution}\Rightarrow{\it
406 term}\Rightarrow{\it term}$: allows to access sub-terms.
408 \item[Take:] ${\it term}\Rightarrow{\it term}$:
409 this tactic has no effect in the program; but it creates a side-effect
410 by Lucas-Interpretation (see below) and writes {\it term} to the
413 \item[Subproblem:] ${\it theory} * {\it specification} * {\it
414 method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
415 this tactic is a generalisation of a function call: it takes an
416 \textit{argument list} as usual, and additionally a triple consisting
417 of an Isabelle \textit{theory}, an implicit \textit{specification} of the
418 program and a \textit{method} containing data for Lucas-Interpretation,
419 last not least a program (as an explicit specification)~\footnote{In
420 interactive tutoring these three items can be determined explicitly
423 The tactics play a specific role in
424 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
425 break-points where, as a side-effect, a line is added to a calculation
426 as a protocol for proceeding towards a solution in step-wise problem
427 solving. At the same points Lucas-Interpretation serves interactive
428 tutoring and control is handed over to the user. The user is free to
429 investigate underlying knowledge, applicable theorems, etc. And the
430 user can proceed constructing a solution by input of a tactic to be
431 applied or by input of a formula; in the latter case the
432 Lucas-Interpreter has built up a logical context (initialised with the
433 precondition of the formal specification) such that Isabelle can
434 derive the formula from this context --- or give feedback, that no
435 derivation can be found.
437 \subsection{Tacticals as Control Flow Statements}
438 The flow of control in a program can be determined by {\tt if then else}
439 and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
440 by additional tacticals:
442 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
443 term}$: iterates over tactics which take a {\it term} as argument as
444 long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
447 \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
448 if {\it tactic} is applicable, then it is applied to {\it term},
449 otherwise {\it term} is passed on without changes.
451 \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
452 term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
453 it is applied to the first {\it term} yielding another {\it term},
454 otherwise the second {\it tactic} is applied; if none is applicable an
457 \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
458 term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
459 first {\it term} yielding an intermediate term (not appearing in the
460 signature) to which the second {\it tactic} is applied.
462 \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
463 term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
464 {\it tactic} is applied to the first {\it term} yielding an
465 intermediate term (not appearing in the signature); the intermediate
466 term is added to the environment the first {\it term} is evaluated in
467 etc as long as the first {\it term} is true.
469 The tacticals are not treated as break-points by Lucas-Interpretation
470 and thus do not contribute to the calculation nor to interaction.
472 \section{Concepts and Tasks in TP-based Programming}\label{trial}
473 %\section{Development of a Program on Trial}
475 This section presents all the concepts involved in TP-based
476 programming and all the tasks to be accomplished by programmers. The
477 presentation uses the running example which has been introduced in
478 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
480 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
482 %WN was Fachleute unter obigem Titel interessiert findet sich
483 %WN unterhalb des auskommentierten Textes.
485 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
486 %WN auf Computer-Mathematiker fokussiert.
487 % \paragraph{As mentioned in the introduction,} a prototype of an
488 % educational math assistant called
489 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
490 % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
491 % the gap between (1) introducation and (2) application of mathematics:
492 % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
493 % requires each fact and each action justified by formal logic, so
494 % {{{\sisac}{}}} makes justifications transparent to students in
495 % interactive step-wise problem solving. By that way {{\sisac}} already
498 % \item Introduction of math stuff (in e.g. partial fraction
499 % decomposition) by stepwise explaining and exercising respective
500 % symbolic calculations with ``next step guidance (NSG)'' and rigorously
501 % checking steps freely input by students --- this also in context with
502 % advanced applications (where the stuff to be taught in higher
503 % semesters can be skimmed through by NSG), and
504 % \item Application of math stuff in advanced engineering courses
505 % (e.g. problems to be solved by inverse Z-transform in a Signal
506 % Processing Lab) and now without much ado about basic math techniques
507 % (like partial fraction decomposition): ``next step guidance'' supports
508 % students in independently (re-)adopting such techniques.
510 % Before the question is answers, how {{\sisac}}
511 % accomplishes this task from a technical point of view, some remarks on
512 % the state-of-the-art is given, therefor follow up Section~\ref{emas}.
514 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
516 % \paragraph{Educational software in mathematics} is, if at all, based
517 % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
518 % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
519 % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
520 % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
521 % base technologies are used to program math lessons and sometimes even
522 % exercises. The latter are cumbersome: the steps towards a solution of
523 % such an interactive exercise need to be provided with feedback, where
524 % at each step a wide variety of possible input has to be foreseen by
525 % the programmer - so such interactive exercises either require high
526 % development efforts or the exercises constrain possible inputs.
528 % \subparagraph{A new generation} of educational math assistants (EMAs)
529 % is emerging presently, which is based on Theorem Proving (TP). TP, for
530 % instance Isabelle and Coq, is a technology which requires each fact
531 % and each action justified by formal logic. Pushed by demands for
532 % \textit{proven} correctness of safety-critical software TP advances
533 % into software engineering; from these advancements computer
534 % mathematics benefits in general, and math education in particular. Two
535 % features of TP are immediately beneficial for learning:
537 % \paragraph{TP have knowledge in human readable format,} that is in
538 % standard predicate calculus. TP following the LCF-tradition have that
539 % knowledge down to the basic definitions of set, equality,
540 % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
541 % following the typical deductive development of math, natural numbers
542 % are defined and their properties
543 % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
544 % etc. Present knowledge mechanized in TP exceeds high-school
545 % mathematics by far, however by knowledge required in software
546 % technology, and not in other engineering sciences.
548 % \paragraph{TP can model the whole problem solving process} in
549 % mathematical problem solving {\em within} a coherent logical
550 % framework. This is already being done by three projects, by
551 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
553 % Having the whole problem solving process within a logical coherent
554 % system, such a design guarantees correctness of intermediate steps and
555 % of the result (which seems essential for math software); and the
556 % second advantage is that TP provides a wealth of theories which can be
557 % exploited for mechanizing other features essential for educational
560 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
562 % One essential feature for educational software is feedback to user
563 % input and assistance in coming to a solution.
565 % \paragraph{Checking user input} by ATP during stepwise problem solving
566 % is being accomplished by the three projects mentioned above
567 % exclusively. They model the whole problem solving process as mentioned
568 % above, so all what happens between formalized assumptions (or formal
569 % specification) and goal (or fulfilled postcondition) can be
570 % mechanized. Such mechanization promises to greatly extend the scope of
571 % educational software in stepwise problem solving.
573 % \paragraph{NSG (Next step guidance)} comprises the system's ability to
574 % propose a next step; this is a challenge for TP: either a radical
575 % restriction of the search space by restriction to very specific
576 % problem classes is required, or much care and effort is required in
577 % designing possible variants in the process of problem solving
578 % \cite{proof-strategies-11}.
580 % Another approach is restricted to problem solving in engineering
581 % domains, where a problem is specified by input, precondition, output
582 % and postcondition, and where the postcondition is proven by ATP behind
583 % the scenes: Here the possible variants in the process of problem
584 % solving are provided with feedback {\em automatically}, if the problem
585 % is described in a TP-based programing language: \cite{plmms10} the
586 % programmer only describes the math algorithm without caring about
587 % interaction (the respective program is functional and even has no
588 % input or output statements!); interaction is generated as a
589 % side-effect by the interpreter --- an efficient separation of concern
590 % between math programmers and dialog designers promising application
591 % all over engineering disciplines.
594 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
595 % Authoring new mathematics knowledge in {{\sisac}} can be compared with
596 % ``application programing'' of engineering problems; most of such
597 % programing uses CAS-based programing languages (CAS = Computer Algebra
598 % Systems; e.g. Mathematica's or Maple's programing language).
600 % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
601 % \cite{plmms10} for describing how to construct a solution to an
602 % engineering problem and for calling equation solvers, integration,
603 % etc~\footnote{Implementation of CAS-like functionality in TP is not
604 % primarily concerned with efficiency, but with a didactic question:
605 % What to decide for: for high-brow algorithms at the state-of-the-art
606 % or for elementary algorithms comprehensible for students?} within TP;
607 % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
608 % are impossible for CAS which have no logics underlying.
610 % \subparagraph{Authoring is perfect} by writing such TP based programs;
611 % the application programmer is not concerned with interaction or with
612 % user guidance: this is concern of a novel kind of program interpreter
613 % called Lucas-Interpreter. This interpreter hands over control to a
614 % dialog component at each step of calculation (like a debugger at
615 % breakpoints) and calls automated TP to check user input following
616 % personalized strategies according to a feedback module.
618 % However ``application programing with TP'' is not done with writing a
619 % program: according to the principles of TP, each step must be
620 % justified. Such justifications are given by theorems. So all steps
621 % must be related to some theorem, if there is no such theorem it must
622 % be added to the existing knowledge, which is organized in so-called
623 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
624 % Isabelle comprises a mechanism (called ``axiomatization''), which
625 % allows to omit proofs. Such a theorem is shown in
626 % Example~\ref{eg:neuper1}.
628 The running example requires to determine the inverse $\cal
629 Z$-transform for a class of functions. The domain of Signal Processing
630 is accustomed to specific notation for the resulting functions, which
631 are absolutely summable and are called TODO: $u[n]$, where $u$ is the
632 function, $n$ is the argument and the brackets indicate that the
633 arguments are TODO. Surprisingly, Isabelle accepts the rules for
634 ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
635 experts might be particularly surprised, that the brackets do not
636 cause errors in typing (as lists).}:
640 {\small\begin{tabbing}
641 123\=123\=123\=123\=\kill
643 \>axiomatization where \\
644 \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
645 \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
646 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
648 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
650 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
652 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
658 These 6 rules can be used as conditional rewrite rules, depending on
659 the respective convergence radius. Satisfaction from accordance with traditional notation
660 contrasts with the above word {\em axiomatization}: As TP-based, the
661 programming language expects these rules as {\em proved} theorems, and
662 not as axioms implemented in the above brute force manner; otherwise
663 all the verification efforts envisaged (like proof of the
664 post-condition, see below) would be meaningless.
666 Isabelle provides a large body of knowledge, rigorously proven from
667 the basic axioms of mathematics~\footnote{This way of rigorously
668 deriving all knowledge from first principles is called the
669 LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
670 knowledge can be found in the theoris on Multivariate
671 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
672 building up knowledge such that a proof for the above rules would be
673 reasonably short and easily comprehensible, still requires lots of
674 work (and is definitely out of scope of our case study).
676 At the state-of-the-art in mechanization of knowledge in engineering
677 sciences, the process does not stop with the mechanization of
678 mathematics traditionally used in these sciences. Rather, ``Formal
679 Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
680 description of physical items. Signal Processing, for instance is
681 concerned with physical devices for signal acquisition and
682 reconstruction, which involve measuring a physical signal, storing it,
683 and possibly later rebuilding the original signal or an approximation
684 thereof. For digital systems, this typically includes sampling and
685 quantization; devices for signal compression, including audio
686 compression, image compression, and video compression, etc. ``Domain
687 engineering''\cite{db:dom-eng} is concerned with {\em specification}
688 of these devices' components and features; this part in the process of
689 mechanization is only at the beginning in domains like Signal
692 TP-based programming, concern of this paper, is determined to
693 add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
694 p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
695 starts with a formal {\em specification} of the problem to be solved.
698 %\includegraphics[width=110mm]{fig/math-universe-small}
699 \caption{The three-dimensional universe of mathematics knowledge}
703 The language for both axes is defined in the axis at the bottom, deductive
704 knowledge, in {\sisac} represented by Isabelle's theories.
706 \subsection{Preparation of Simplifiers for the Program}\label{simp}
708 \paragraph{If it is clear} how the later calculation should look like and when
709 which mathematic rule should be applied, it can be started to find ways of
710 simplifications. This includes in e.g. the simplification of reational
711 expressions or also rewrites of an expession.
712 \subparagraph{Obligate is the use} of the function \texttt{drop\_questionmarks}
713 which excludes irrelevant symbols out of the expression. (Irrelevant symbols may
714 be result out of the system during the calculation. The function has to be
715 applied for two reasons. First two make every placeholder in a expression
716 useable as a constant and second to provide a better view at the frontend.)
717 \subparagraph{Most rewrites are represented} through rulesets this
718 rulesets tell the machine which terms have to be rewritten into which
719 representation. In the upcoming programm a rewrite can be applied only in using
720 such rulesets on existing terms.
721 \paragraph{The core} of our implemented problem is the Z-Transformation
722 (remember the description of the running example, introduced by
723 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the
724 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
725 transformation tables).
726 \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
727 use of axiomatizations like shown in Example~\ref{eg:ruledef}. This rules can be
728 collected in a ruleset (collection of rules) and applied to a given expression
729 as follows in the next example code.
736 rule1: ``1 = $\delta$[n]'' and
737 rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
738 rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
746 \item Store rules in ruleset:
748 val inverse_Z = append_rls "inverse_Z" e_rls
749 [ Thm ("rule1",num_str @{thm rule1}),
750 Thm ("rule2",num_str @{thm rule2}),
751 Thm ("rule3",num_str @{thm rule3})
754 \item Define exression:
756 val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";
760 val SOME (sample_term', asm) =
761 rewrite_set_ thy true inverse_Z sample_term;
766 The use of rulesets makes it much easier to develop our designated applications,
767 but the programmer has to be careful and patient. When applying rulesets
768 two important issues have to be mentionend:
769 \subparagraph{How often} the rules have to be applied? In case of
770 transformations it is quite clear that we use them once but other fields
771 reuqire to apply rules until a special condition is reached (e.g.
772 a simplification is finished when there is nothing to be done left).
773 \subparagraph{The order} in which rules are applied often takes a big effect
774 and has to be evaluated for each purpose once again.
776 In our special case of Signal Processing and the rules defined in
777 Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
778 constants. After this step has been done it no mather which rule fit's next.
780 \subsection{Preparation of ML-Functions}\label{funs}
781 The prototype's Lucas-Interpreter uses the {\sisac}-rewrite-engine for
782 all kinds of evaluation. Some functionality required in programming,
783 however, cannot be accomplished by rewriting. So the prototype has a
784 mechanism to call ML-functions during rewriting, and the programmer has
785 to use this mechanism.
787 In the running example's program on p.\pageref{s:impl} the lines {\rm
788 05} and {\rm 06} contain such functions; we go into the details with
789 \textit{argument\_in X\_z;}. This function fetches the argument from a
790 function application: Line {\rm 03} in the example calculation on
791 p.\pageref{exp-calc} is created by line {\rm 06} of the example
792 program on p.\pageref{s:impl} where the program's environment assigns
793 the value \textit{X z} to the variable \textit{X\_z}; so the function
794 shall extract the argument \textit{z}.
796 \medskip In order to be recognised as a function constant in the
797 program source the constant needs to be declared in a theory, here in
798 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
799 the context \textit{ctxt} of that theory:
803 argument'_in :: "real => real" ("argument'_in _" 10)
805 ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
807 val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
808 $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
811 \noindent Parsing produces a term \texttt{t} in internal
812 representation~\footnote{The attentive reader realizes the delicate
813 differences between interal and extermal representation even in the
814 strings, i.e \texttt{'\_}}, consisting of \texttt{Const
815 ("argument'\_in", type)} and the two variables \texttt{Free ("X",
816 type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
817 constructor. The function body below is implemented directly in ML,
818 i.e in an \texttt{ML \{* *\}} block; the function definition provides
819 a unique prefix \texttt{eval\_} to the function name:
824 fun eval_argument_in _
825 "Build_Inverse_Z_Transform.argument'_in"
826 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ =
827 if is_Free arg (*could be something to be simplified before*)
828 then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg)))
830 | eval_argument_in _ _ _ _ = NONE;
834 \noindent The function body creates either creates \texttt{NONE}
835 telling the rewrite-engine to search for the next redex, or creates an
836 ad-hoc theorem for rewriting, thus the programmer needs to adopt many
837 technicalities of Isabelle, for instance, the \textit{Trueprop}
840 \bigskip This sub-task particularly sheds light on basic issues in the
841 design of a programming language, the integration of diffent language
842 layers, the layer of Isabelle/Isar and Isabelle/ML.
844 Another point of improvement for the prototype is the rewrite-engine: The
845 program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
848 {\small\it\label{s:impl}
850 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
851 \>{\rm 05/6}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
854 \noindent because nested function calls would require creating redexes
855 inside-out; however, the prototype's rewrite-engine only works top down
856 from the root of a term down to the leaves.
858 How all these ugly technicalities are to be checked in the prototype is
859 shown in \S\ref{flow-prep} below.
861 % \paragraph{Explicit Problems} require explicit methods to solve them, and within
862 % this methods we have some explicit steps to do. This steps can be unique for
863 % a special problem or refindable in other problems. No mather what case, such
864 % steps often require some technical functions behind. For the solving process
865 % of the Inverse Z Transformation and the corresponding partial fraction it was
866 % neccessary to build helping functions like \texttt{get\_denominator},
867 % \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
868 % to filter the denominator or numerator out of a fraction, last one helps us to
869 % get to know the bound variable in a equation.
871 % By taking \texttt{get\_denominator} as an example, we want to explain how to
872 % implement new functions into the existing system and how we can later use them
875 % \subsubsection{Find a place to Store the Function}
877 % The whole system builds up on a well defined structure of Knowledge. This
878 % Knowledge sets up at the Path:
879 % \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
880 % For implementing the Function \texttt{get\_denominator} (which let us extract
881 % the denominator out of a fraction) we have choosen the Theory (file)
882 % \texttt{Rational.thy}.
884 % \subsubsection{Write down the new Function}
886 % In upper Theory we now define the new function and its purpose:
888 % get_denominator :: "real => real"
890 % This command tells the machine that a function with the name
891 % \texttt{get\_denominator} exists which gets a real expression as argument and
892 % returns once again a real expression. Now we are able to implement the function
893 % itself, upcoming example now shows the implementation of
894 % \texttt{get\_denominator}.
897 % \label{eg:getdenom}
901 % 02 *("get_denominator",
902 % 03 * ("Rational.get_denominator", eval_get_denominator ""))
904 % 05 fun eval_get_denominator (thmid:string) _
905 % 06 (t as Const ("Rational.get_denominator", _) $
906 % 07 (Const ("Rings.inverse_class.divide", _) $num
908 % 09 SOME (mk_thmid thmid ""
909 % 10 (Print_Mode.setmp []
910 % 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
911 % 12 Trueprop $ (mk_equality (t, denom)))
912 % 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
915 % Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
916 % there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
918 % into its two parts (\texttt{\$num \$denom}). The lines before are additionals
919 % commands for declaring the function and the lines after are modeling and
920 % returning a real variable out of \texttt{\$denom}.
922 % \subsubsection{Add a test for the new Function}
924 % \paragraph{Everytime when adding} a new function it is essential also to add
925 % a test for it. Tests for all functions are sorted in the same structure as the
926 % knowledge it self and can be found up from the path:
927 % \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
928 % This tests are nothing very special, as a first prototype the functionallity
929 % of a function can be checked by evaluating the result of a simple expression
930 % passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
931 % \textit{just} created function \texttt{get\_denominator}.
934 % \label{eg:getdenomtest}
937 % 01 val thy = @{theory Isac};
938 % 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
939 % 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
940 % 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
941 % 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
944 % \begin{description}
945 % \item[01] checks if the proofer set up on our {\sisac{}} System.
946 % \item[02] passes a simple expression (fraction) to our suddenly created
948 % \item[04] checks if the resulting variable is the correct one (in this case
949 % ``b'' the denominator) and returns.
950 % \item[05] handels the error case and reports that the function is not able to
951 % solve the given problem.
954 \subsection{Specification of the Problem}\label{spec}
955 %WN <--> \chapter 7 der Thesis
956 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
958 The problem of the running example is textually described in
959 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
960 formal} specification of this problem, in traditional mathematical
961 notation, could look like is this:
963 %WN Hier brauchen wir die Spezifikation des 'running example' ...
964 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
965 %JR der post condition - die existiert für uns ja eigentlich nicht aka
966 %JR haben sie bis jetzt nicht beachtet WN...
967 %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
971 {\small\begin{tabbing}
972 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
975 \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
976 \>precond \>: filterExpression continius on $\mathbb{R}$ \\
977 \>output \>: stepResponse $x[n]$ \\
978 \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
981 Defining the postcondition requires a high amount mathematical
982 knowledge, the difficult part in our case is not to set up this condition
983 nor it is more to define it in a way the interpreter is able to handle it.
984 Due the fact that implementing that mechanisms is quite the same amount as
985 creating the programm itself, it is not avaible in our prototype.
989 \paragraph{The implementation} of the formal specification in the present
990 prototype, still bar-bones without support for authoring:
991 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
992 {\footnotesize\label{exp-spec}
994 01 store_specification
995 02 (prepare_specification
997 04 "pbl_SP_Ztrans_inv"
999 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1000 07 [ ("#Given", ["filterExpression X_eq"]),
1001 08 ("#Pre" , ["X_eq is_continuous"]),
1002 09 ("#Find" , ["stepResponse n_eq"]),
1003 10 ("#Post" , [" TODO "])],
1004 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
1006 13 [["SignalProcessing","Z_Transform","Inverse"]]));
1008 Although the above details are partly very technical, we explain them
1009 in order to document some intricacies of TP-based programming in the
1010 present state of the {\sisac} prototype:
1012 \item[01..02]\textit{store\_specification:} stores the result of the
1013 function \textit{prep\_specification} in a global reference
1014 \textit{Unsynchronized.ref}, which causes principal conflicts with
1015 Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
1016 parallel execution~\cite{Makarius-09:parall-proof} and is under
1017 reconstruction already.
1019 \textit{prep\_pbt:} translates the specification to an internal format
1020 which allows efficient processing; see for instance line {\rm 07}
1022 \item[03..04] are the ``mathematics author'' holding the copy-rights
1023 and a unique identifier for the specification within {\sisac},
1024 complare line {\rm 06}.
1025 \item[05] is the Isabelle \textit{theory} required to parse the
1026 specification in lines {\rm 07..10}.
1027 \item[06] is a key into the tree of all specifications as presented to
1028 the user (where some branches might be hidden by the dialog
1030 \item[07..10] are the specification with input, pre-condition, output
1031 and post-condition respectively; the post-condition is not handled in
1032 the prototype presently. (Follow up Remark~\ref{rm:postcond})
1033 \item[11] creates a term rewriting system (abbreviated \textit{rls} in
1034 {\sisac}) which evaluates the pre-condition for the actual input data.
1035 Only if the evaluation yields \textit{True}, a program con be started.
1036 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1037 problem associated to a function from Computer Algebra (like an
1038 equation solver) which is not the case here.
1039 \item[13] is the specific key into the tree of programs addressing a
1040 method which is able to find a solution which satiesfies the
1041 post-condition of the specification.
1045 %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1048 % {guh : guh, (*unique within this isac-knowledge*)
1049 % mathauthors: string list, (*copyright*)
1050 % init : pblID, (*to start refinement with*)
1051 % thy : theory, (* which allows to compile that pbt
1052 % TODO: search generalized for subthy (ref.p.69*)
1053 % (*^^^ WN050912 NOT used during application of the problem,
1054 % because applied terms may be from 'subthy' as well as from super;
1055 % thus we take 'maxthy'; see match_ags !*)
1056 % cas : term option,(*'CAS-command'*)
1057 % prls : rls, (* for preds in where_*)
1058 % where_: term list, (* where - predicates*)
1060 % (*this is the model-pattern;
1061 % it contains "#Given","#Where","#Find","#Relate"-patterns
1062 % for constraints on identifiers see "fun cpy_nam"*)
1063 % met : metID list}; (* methods solving the pbt*)
1065 %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1066 %WN oben selbst geschrieben.
1071 %WN das w"urde ich in \sec\label{progr} verschieben und
1072 %WN das SubProblem partial fractions zum Erkl"aren verwenden.
1073 % Such a specification is checked before the execution of a program is
1074 % started, the same applies for sub-programs. In the following example
1075 % (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1079 % \label{eg:subprob}
1081 % {\ttfamily \begin{tabbing}
1082 % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
1083 % ``\>\>[linear,univariate,equation,test],'' \\
1084 % ``\>\>[Test,solve\_linear])'' \\
1085 % ``\>[BOOL equ, REAL z])'' \\
1089 % \noindent If a program requires a result which has to be
1090 % calculated first we can use a subproblem to do so. In our specific
1091 % case we wanted to calculate the zeros of a fraction and used a
1092 % subproblem to calculate the zeros of the denominator polynom.
1097 \subsection{Implementation of the Method}\label{meth}
1099 \paragraph{After specifieing the problem} we start to implement the method(s) of
1100 the problem. The methods represent the different ways a problem can be solved,
1101 this can include different mathematical tactics as well as different tactics
1102 taught in different courses.
1107 02 (prep_met thy "SP_InverseZTransformation_classic" [] e_metID
1108 03 (["SignalProcessing", "Z_Transform", "Inverse"],
1109 04 [("#Given" ,["filterExpression (X_eq::bool)"]),
1110 05 ("#Find" ,["stepResponse (n_eq::bool)"])],
1111 06 {rew_ord'="tless_true",
1123 The above code is again very technical and goes hard in detail. But to document
1124 and present the neccessary steps follow up the description of the above code:
1128 \item[01-02] this to lines store the method with the given name into the system
1129 \item[03] here, the path is specifiet; which capitel this method is belonging to
1130 \item[04-05] as the requirements for different methods can be different we
1131 specify again the \emph{given} and the \emph{find} element.
1140 \item[14] for this time we don't specify the programm itself and keep it empty.
1141 Follow up \S\ref{progr} for informations on how to implement this \textit{main}
1147 \subsection{Implementation of the TP-based Program}\label{progr}
1148 So finally all the prerequisites are described and the very topic can
1149 be addressed. The program below comes back to the running example: it
1150 computes a solution for the problem from Fig.\ref{fig-interactive} on
1151 p.\pageref{fig-interactive}. The reader is reminded of
1152 \S\ref{PL-isab}, the introduction of the programming language:
1153 {\small\it\label{s:impl}
1155 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1156 \>{\rm 00}\>val program =\\
1157 \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1158 \>{\rm 02}\>\> {\tt let} \\
1159 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1160 \>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
1161 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1162 \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1163 \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1164 \>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
1165 %\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
1166 \>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1167 \>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1168 \>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@ \\
1169 \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1170 \>{\rm 13}\>\> {\tt in } \\
1171 \>{\rm 14}\>\>\> X'\_eq"
1173 % ORIGINAL FROM Inverse_Z_Transform.thy
1174 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1175 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1176 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1177 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1178 % " (zzz::real) = argument_in X'_z; "^(* z *)
1179 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1181 % " (pbz::real) = (SubProblem (Isac', "^(**)
1182 % " [partial_fraction,rational,simplification], "^
1183 % " [simplification,of_rationals,to_partial_fraction]) "^
1184 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1186 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1187 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1188 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1189 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1190 % " 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]*)
1191 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1192 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1193 The program is represented as a string and part of the method in
1194 \S\ref{meth}. As mentioned in \S\ref{PL} the program is purely
1195 functional and lacks any input statements and output statements. So
1196 the steps of calculation towards a solution (and interactive tutoring
1197 in step-wise problem solving) are created as a side-effect by
1198 Lucas-Interpretation. The side-effects are triggered by the tactics
1199 \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
1200 \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1201 {\rm 12} respectively. These tactics produce the lines in the
1202 calculation on p.\pageref{flow-impl}.
1204 The above lines {\rm 05, 06} do not contain a tactics, so they do not
1205 immediately contribute to the calculation on p.\pageref{flow-impl};
1206 rather, they compute actual arguments for the \texttt{SubProblem} in
1207 line {\rm 09}~\footnote{The tactics also are break-points for the
1208 interpreter, where control is handed over to the user in interactive
1209 tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
1211 \medskip The above program also indicates the dominant role of interactive
1212 selection of knowledge in the three-dimensional universe of
1213 mathematics as depicted in Fig.\ref{fig:mathuni} on
1214 p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines
1215 {\rm 07..09} is more than a function call with the actual arguments
1216 \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
1220 \item the theory, in the example \textit{Isac} because different
1221 methods can be selected in Pt.3 below, which are defined in different
1222 theories with \textit{Isac} collecting them.
1223 \item the specification identified by \textit{[partial\_fraction,
1224 rational, simplification]} in the tree of specifications; this
1225 specification is analogous to the specification of the main program
1226 described in \S\ref{spec}; the problem is to find a ``partial fraction
1227 decomposition'' for a univariate rational polynomial.
1228 \item the method in the above example is \textit{[ ]}, i.e. empty,
1229 which supposes the interpreter to select one of the methods predefined
1230 in the specification, for instance in line {\rm 13} in the running
1231 example's specification on p.\pageref{exp-spec}~\footnote{The freedom
1232 (or obligation) for selection carries over to the student in
1233 interactive tutoring.}.
1236 The program code, above presented as a string, is parsed by Isabelle's
1237 parser --- the program is an Isabelle term. This fact is expected to
1238 simplify verification tasks in the future; on the other hand, this
1239 fact causes troubles in error detectetion which are discussed as part
1240 of the workflow in the subsequent section.
1242 \section{Workflow of Programming in the Prototype}\label{workflow}
1243 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
1244 step forward for interactive theory and proof development. The
1245 {\sisac}-prototype re-uses this IDE as a programming environment. The
1246 experiences from this re-use show, that the essential components are
1247 available from Isabelle/jEdit. However, additional tools and features
1248 are required to acchieve acceptable usability.
1250 So notable experiences are reported here, also as a requirement
1251 capture for further development of TP-based languages and respective
1254 \subsection{Preparations and Trials}\label{flow-prep}
1255 The many sub-tasks to be accomplished {\em before} the first line of
1256 program code can be written and tested suggest an approach which
1257 step-wise establishes the prerequisites. The case study underlying
1258 this paper~\cite{jrocnik-bakk} documents the approach in a separate
1260 \textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
1261 II in the study comprises this theory, \LaTeX ed from the theory by
1262 use of Isabelle's document preparation system. This paper resembles
1263 the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
1264 implementation work involves several iterations.
1266 \bigskip For instance, only the last step, implementing the program
1267 described in \S\ref{meth}, reveals details required. Let us assume,
1268 this is the ML-function \textit{argument\_in} required in line {\rm 06}
1269 of the example program on p.\pageref{s:impl}; how this function needs
1270 to be implemented in the prototype has been discussed in \S\ref{funs}
1273 Now let us assume, that calling this function from the program code
1274 does not work; so testing this function is required in order to find out
1275 the reason: type errors, a missing entry of the function somewhere or
1276 even more nasty technicalities \dots
1281 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1282 val SOME (str, t') = eval_argument_in ""
1283 "Build_Inverse_Z_Transform.argument'_in" t 0;
1288 val it = "(argument_in X z) = z": string
1291 \noindent So, this works: we get an ad-hoc theorem, which used in
1292 rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
1293 reduction and create a rule-set \texttt{rls} for that purpose:
1298 val rls = append_rls "test" e_rls
1299 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1302 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1304 val t' = Free ("z", "RealDef.real"): term
1305 val asm = []: term list
1308 \noindent The resulting term \texttt{t'} is \texttt{Free ("z",
1309 "RealDef.real")}, i.e the variable \texttt{z}, so all is
1310 perfect. Probably we have forgotten to store this function correctly~?
1311 We review the respective \texttt{calclist} (again an
1312 \textit{Unsynchronized.ref} to be removed in order to adjust to
1313 IsabelleIsar's asyncronous document model):
1317 calclist:= overwritel (! calclist,
1318 [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1323 \noindent The entry is perfect. So what is the reason~? Ah, probably there
1324 is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1325 right, the function \texttt{argument\_in} is not contained in the respective
1326 rule-set \textit{srls} \dots this just as an example of the intricacies in
1327 debugging a program in the present state of the prototype.
1329 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1330 Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
1331 usually developed within several iterations, the program can be
1332 assembled; on p.\pageref{s:impl} there is the complete program of the
1335 The completion of this program required efforts for several weeks
1336 (after some months of familiarisation with {\sisac}), caused by the
1337 abundance of intricacies indicated above. Also writing the program is
1338 not pleasant, given Isabelle/Isar/ without add-ons for
1339 programming. Already writing and parsing a few lines of program code
1340 is a challenge: the program is an Isabelle term; Isabelle's parser,
1341 however, is not meant for huge terms like the program of the running
1342 example. So reading out the specific error (usually type errors) from
1343 Isabelle's message is difficult.
1345 \medskip Testing the evaluation of the program has to rely on very
1346 simple tools. Step-wise execution is modelled by a function
1347 \texttt{me}, short for mathematics-engine~\footnote{The interface used
1348 by the fron-end which created the calculation on
1349 p.\pageref{fig-interactive} is different from this function}:
1350 %the following is a simplification of the actual function
1355 val it = tac -> ctree * pos -> mout * tac * ctree * pos
1358 \noindent This function takes as arguments a tactic \texttt{tac} which
1359 determines the next step, the step applied to the interpreter-state
1360 \texttt{ctree * pos} as last argument taken. The interpreter-state is
1361 a pair of a tree \texttt{ctree} representing the calculation created
1362 (see the example below) and a position \texttt{pos} in the
1363 calculation. The function delivers a quadrupel, beginning with the new
1364 formula \texttt{mout} and the next tactic followed by the new
1367 This function allows to stepwise check the program:
1373 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1374 "stepResponse (x[n::real]::bool)"];
1377 ["Inverse", "Z_Transform", "SignalProcessing"],
1378 ["SignalProcessing","Z_Transform","Inverse"]);
1380 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1381 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1382 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1383 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1387 \noindent Several douzens of calls for \texttt{me} are required to
1388 create the lines in the calculation below (including the sub-problems
1389 not shown). When an error occurs, the reason might be located
1390 many steps before: if evaluation by rewriting, as done by the prototype,
1391 fails, then first nothing happens --- the effects come later and
1392 cause unpleasant checks.
1394 The checks comprise watching the rewrite-engine for many different
1395 kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
1396 particular the environment and the context at the states position ---
1397 all checks have to rely on simple functions accessing the
1398 \texttt{ctree}. So getting the calculation below (which resembles the
1399 calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
1400 finished successfully is a relief:
1402 {\small\it\label{exp-calc}
1404 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1405 \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1406 \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
1407 \>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\
1408 \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
1409 \>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
1410 \>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
1411 \>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
1412 \>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
1413 \>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
1414 \>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
1415 \> \>\>\>\> \_\_\_ \`- - -\\
1416 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1417 \>{\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)}\\
1418 \>{\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} ruleYZ X'\_eq }\\
1419 \>{\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}\\
1420 \>{\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}}
1422 % ORIGINAL FROM Inverse_Z_Transform.thy
1423 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1424 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1425 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1426 % " (X'_z::real) = lhs X'; "^(* ?X' z*)
1427 % " (zzz::real) = argument_in X'_z; "^(* z *)
1428 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1430 % " (pbz::real) = (SubProblem (Isac', "^(**)
1431 % " [partial_fraction,rational,simplification], "^
1432 % " [simplification,of_rationals,to_partial_fraction]) "^
1433 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1435 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1436 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1437 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1438 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1439 % " 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]*)
1440 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1441 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1443 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1444 Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
1445 and the knowledge accumulated in it can be distributed to appropriate
1446 theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
1447 sub-problem accomplishing the partial fraction decomposition to
1448 \textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
1449 internals, this kind of distribution is not trivial. For instance, the
1450 function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
1451 string with the theory it has been defined in, so this string needs to
1452 be updated from \texttt{Build\_Inverse\_Z\_Transform} to
1453 \texttt{Atools} if that function is transferred to theory
1454 \textit{Atools.thy}.
1456 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.
1457 This process is also rather bare-bones without authoring tools and is
1458 described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
1461 % -------------------------------------------------------------------
1463 % Material, falls noch Platz bleibt ...
1465 % -------------------------------------------------------------------
1468 % \subsubsection{Trials on Notation and Termination}
1470 % \paragraph{Technical notations} are a big problem for our piece of software,
1471 % but the reason for that isn't a fault of the software itself, one of the
1472 % troubles comes out of the fact that different technical subtopics use different
1473 % symbols and notations for a different purpose. The most famous example for such
1474 % a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1475 % math). In the specific part of signal processing one of this notation issues is
1476 % the use of brackets --- we use round brackets for analoge signals and squared
1477 % brackets for digital samples. Also if there is no problem for us to handle this
1478 % fact, we have to tell the machine what notation leads to wich meaning and that
1479 % this purpose seperation is only valid for this special topic - signal
1481 % \subparagraph{In the programming language} itself it is not possible to declare
1482 % fractions, exponents, absolutes and other operators or remarks in a way to make
1483 % them pretty to read; our only posssiblilty were ASCII characters and a handfull
1484 % greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1486 % With the upper collected knowledge it is possible to check if we were able to
1487 % donate all required terms and expressions.
1489 % \subsubsection{Definition and Usage of Rules}
1491 % \paragraph{The core} of our implemented problem is the Z-Transformation, due
1492 % the fact that the transformation itself would require higher math which isn't
1493 % yet avaible in our system we decided to choose the way like it is applied in
1494 % labratory and problem classes at our university - by applying transformation
1495 % rules (collected in transformation tables).
1496 % \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1497 % use of axiomatizations like shown in Example~\ref{eg:ruledef}
1500 % \label{eg:ruledef}
1503 % axiomatization where
1504 % rule1: ``1 = $\delta$[n]'' and
1505 % rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1506 % rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1510 % This rules can be collected in a ruleset and applied to a given expression as
1511 % follows in Example~\ref{eg:ruleapp}.
1515 % \label{eg:ruleapp}
1517 % \item Store rules in ruleset:
1519 % val inverse_Z = append_rls "inverse_Z" e_rls
1520 % [ Thm ("rule1",num_str @{thm rule1}),
1521 % Thm ("rule2",num_str @{thm rule2}),
1522 % Thm ("rule3",num_str @{thm rule3})
1524 % \item Define exression:
1526 % val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1527 % \item Apply ruleset:
1529 % val SOME (sample_term', asm) =
1530 % rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1534 % The use of rulesets makes it much easier to develop our designated applications,
1535 % but the programmer has to be careful and patient. When applying rulesets
1536 % two important issues have to be mentionend:
1537 % \subparagraph{How often} the rules have to be applied? In case of
1538 % transformations it is quite clear that we use them once but other fields
1539 % reuqire to apply rules until a special condition is reached (e.g.
1540 % a simplification is finished when there is nothing to be done left).
1541 % \subparagraph{The order} in which rules are applied often takes a big effect
1542 % and has to be evaluated for each purpose once again.
1544 % In our special case of Signal Processing and the rules defined in
1545 % Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1546 % constants. After this step has been done it no mather which rule fit's next.
1548 % \subsubsection{Helping Functions}
1550 % \paragraph{New Programms require,} often new ways to get through. This new ways
1551 % means that we handle functions that have not been in use yet, they can be
1552 % something special and unique for a programm or something famous but unneeded in
1553 % the system yet. In our dedicated example it was for example neccessary to split
1554 % a fraction into numerator and denominator; the creation of such function and
1555 % even others is described in upper Sections~\ref{simp} and \ref{funs}.
1557 % \subsubsection{Trials on equation solving}
1558 % %simple eq and problem with double fractions/negative exponents
1559 % \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
1560 % equations degree one and two. Solving equations in the first degree is no
1561 % problem, wether for a student nor for our machine; but even second degree
1562 % equations can lead to big troubles. The origin of this troubles leads from
1563 % the build up process of our equation solving functions; they have been
1564 % implemented some time ago and of course they are not as good as we want them to
1565 % be. Wether or not following we only want to show how cruel it is to build up new
1566 % work on not well fundamentials.
1567 % \subparagraph{A simple equation solving,} can be set up as shown in the next
1574 % ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
1578 % val (dI',pI',mI') =
1580 % ["abcFormula","degree_2","polynomial","univariate","equation"],
1581 % ["no_met"]);\end{verbatim}
1584 % Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
1585 % a short overview on the commands; at first we set up the equation and tell the
1586 % machine what's the bound variable and where to store the solution. Second step
1587 % is to define the equation type and determine if we want to use a special method
1588 % to solve this type.) Simple checks tell us that the we will get two results for
1589 % this equation and this results will be real.
1590 % So far it is easy for us and for our machine to solve, but
1591 % mentioned that a unvariate equation second order can have three different types
1592 % of solutions it is getting worth.
1593 % \subparagraph{The solving of} all this types of solutions is not yet supported.
1594 % Luckily it was needed for us; but something which has been needed in this
1595 % context, would have been the solving of an euation looking like:
1596 % $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
1597 % before (remember that befor it was no problem to handle for the machine) but
1598 % now, after a simple equivalent transformation, we are not able to solve
1600 % \subparagraph{Error messages} we get when we try to solve something like upside
1601 % were very confusing and also leads us to no special hint about a problem.
1602 % \par The fault behind is, that we have no well error handling on one side and
1603 % no sufficient formed equation solving on the other side. This two facts are
1604 % making the implemention of new material very difficult.
1606 % \subsection{Formalization of missing knowledge in Isabelle}
1608 % \paragraph{A problem} behind is the mechanization of mathematic
1609 % theories in TP-bases languages. There is still a huge gap between
1610 % these algorithms and this what we want as a solution - in Example
1611 % Signal Processing.
1617 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1620 % \noindent A very simple example on this what we call gap is the
1621 % simplification above. It is needles to say that it is correct and also
1622 % Isabelle for fills it correct - \emph{always}. But sometimes we don't
1623 % want expand such terms, sometimes we want another structure of
1624 % them. Think of a problem were we now would need only the coefficients
1625 % of $X$ and $Y$. This is what we call the gap between mechanical
1626 % simplification and the solution.
1631 % \paragraph{We are not able to fill this gap,} until we have to live
1632 % with it but first have a look on the meaning of this statement:
1633 % Mechanized math starts from mathematical models and \emph{hopefully}
1634 % proceeds to match physics. Academic engineering starts from physics
1635 % (experimentation, measurement) and then proceeds to mathematical
1636 % modeling and formalization. The process from a physical observance to
1637 % a mathematical theory is unavoidable bound of setting up a big
1638 % collection of standards, rules, definition but also exceptions. These
1639 % are the things making mechanization that difficult.
1648 % \noindent Think about some units like that one's above. Behind
1649 % each unit there is a discerning and very accurate definition: One
1650 % Meter is the distance the light travels, in a vacuum, through the time
1651 % of 1 / 299.792.458 second; one kilogram is the weight of a
1652 % platinum-iridium cylinder in paris; and so on. But are these
1653 % definitions usable in a computer mechanized world?!
1658 % \paragraph{A computer} or a TP-System builds on programs with
1659 % predefined logical rules and does not know any mathematical trick
1660 % (follow up example \ref{eg:trick}) or recipe to walk around difficult
1666 % \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1667 % \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1668 % \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1669 % \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1671 % \noindent Sometimes it is also useful to be able to apply some
1672 % \emph{tricks} to get a beautiful and particularly meaningful result,
1673 % which we are able to interpret. But as seen in this example it can be
1674 % hard to find out what operations have to be done to transform a result
1675 % into a meaningful one.
1680 % \paragraph{The only possibility,} for such a system, is to work
1681 % through its known definitions and stops if none of these
1682 % fits. Specified on Signal Processing or any other application it is
1683 % often possible to walk through by doing simple creases. This creases
1684 % are in general based on simple math operational but the challenge is
1685 % to teach the machine \emph{all}\footnote{Its pride to call it
1686 % \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1687 % reach a high level of \emph{all} but it in real it will still be a
1688 % survey of knowledge which links to other knowledge and {{\sisac}{}} a
1689 % trainer and helper but no human compensating calculator.
1691 % {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1692 % specifications of problems out of topics from Signal Processing, etc.)
1693 % and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1694 % physical knowledge. The result is a three-dimensional universe of
1695 % mathematics seen in Figure~\ref{fig:mathuni}.
1699 % \includegraphics{fig/universe}
1700 % \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1701 % combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1702 % leads to a three dimensional math universe.\label{fig:mathuni}}
1706 % %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1707 % %WN bitte folgende Bezeichnungen nehmen:
1709 % %WN axis 1: Algorithmic Knowledge (Programs)
1710 % %WN axis 2: Application-oriented Knowledge (Specifications)
1711 % %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1713 % %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1714 % %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1715 % %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1717 % %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1718 % %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1719 % %JR gefordert werden WN2...
1720 % %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1721 % %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1722 % %WN2 zusammenschneiden um die R"ander weg zu bekommen)
1723 % %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1724 % %WN2 png + pdf figures mitzuschicken.
1726 % \subsection{Notes on Problems with Traditional Notation}
1728 % \paragraph{During research} on these topic severely problems on
1729 % traditional notations have been discovered. Some of them have been
1730 % known in computer science for many years now and are still unsolved,
1731 % one of them aggregates with the so called \emph{Lambda Calculus},
1732 % Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1739 % \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1742 % \[ f(p)=\ldots\; p \in \quad R \]
1745 % \noindent Above we see two equations. The first equation aims to
1746 % be a mapping of an function from the reel range to the reel one, but
1747 % when we change only one letter we get the second equation which
1748 % usually aims to insert a reel point $p$ into the reel function. In
1749 % computer science now we have the problem to tell the machine (TP) the
1750 % difference between this two notations. This Problem is called
1751 % \emph{Lambda Calculus}.
1756 % \paragraph{An other problem} is that terms are not full simplified in
1757 % traditional notations, in {{\sisac}} we have to simplify them complete
1758 % to check weather results are compatible or not. in e.g. the solutions
1759 % of an second order linear equation is an rational in {{\sisac}} but in
1760 % tradition we keep fractions as long as possible and as long as they
1761 % aim to be \textit{beautiful} (1/8, 5/16,...).
1762 % \subparagraph{The math} which should be mechanized in Computer Theorem
1763 % Provers (\emph{TP}) has (almost) a problem with traditional notations
1764 % (predicate calculus) for axioms, definitions, lemmas, theorems as a
1765 % computer program or script is not able to interpret every Greek or
1766 % Latin letter and every Greek, Latin or whatever calculations
1767 % symbol. Also if we would be able to handle these symbols we still have
1768 % a problem to interpret them at all. (Follow up \hbox{Example
1769 % \ref{eg:symbint1}})
1773 % \label{eg:symbint1}
1775 % u\left[n\right] \ \ldots \ unitstep
1778 % \noindent The unitstep is something we need to solve Signal
1779 % Processing problem classes. But in {{{\sisac}{}}} the rectangular
1780 % brackets have a different meaning. So we abuse them for our
1781 % requirements. We get something which is not defined, but usable. The
1782 % Result is syntax only without semantic.
1787 % In different problems, symbols and letters have different meanings and
1788 % ask for different ways to get through. (Follow up \hbox{Example
1789 % \ref{eg:symbint2}})
1793 % \label{eg:symbint2}
1795 % \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1798 % \noindent For using exponents the three \texttt{widehat} symbols
1799 % are required. The reason for that is due the development of
1800 % {{{\sisac}{}}} the single \texttt{widehat} and also the double were
1801 % already in use for different operations.
1806 % \paragraph{Also the output} can be a problem. We are familiar with a
1807 % specified notations and style taught in university but a computer
1808 % program has no knowledge of the form proved by a professor and the
1809 % machines themselves also have not yet the possibilities to print every
1810 % symbol (correct) Recent developments provide proofs in a human
1811 % readable format but according to the fact that there is no money for
1812 % good working formal editors yet, the style is one thing we have to
1815 % \section{Problems rising out of the Development Environment}
1817 % fehlermeldungen! TODO
1819 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
1821 \section{Conclusion}\label{conclusion}
1822 This paper gives a first experience report about programming with a
1823 TP-based programming language.
1825 \medskip A brief re-introduction of the novel kind of programming
1826 language by example of the {\sisac}-prototype makes the paper
1827 self-contained. The main section describes all the main concepts
1828 involved in TP-based programming and all the sub-tasks concerning
1829 respective implementation: mechanisation of mathematics and domain
1830 modelling, implementation of term rewriting systems for the
1831 rewriting-engine, formal (implicit) specification of the problem to be
1832 (explicitly) described by the program, implement the many components
1833 required for Lucas-Interpretation and finally implementation of the
1836 The many concepts and sub-tasks involved in programming require a
1837 comprehensive workflow; first experiences with the workflow as
1838 supported by the present prototype are described as well: Isabelle +
1839 Isar + jEdit provide appropriate components for establishing an
1840 efficient development environment integrating computation and
1841 deduction. However, the present state of the prototype is far off a
1842 state appropriate for wide-spread use: the prototype of the program
1843 language lacks expressiveness and elegance, the prototype of the
1844 development environment is hardly usable: error messages still address
1845 the developer of the prototype's interpreter rather than the
1846 application programmer, implementation of the many settings for the
1847 Lucas-Interpreter is cumbersome.
1849 From these experiences a successful proof of concept can be concluded:
1850 programming arbitrary problems from engineering sciences is possible,
1851 in principle even in the prototype. Furthermore the experiences allow
1852 to conclude detailed requirements for further development:
1854 \item Clarify underlying logics such that programming is smoothly
1855 integrated with verification of the program; the post-condition should
1856 be proved more or less automatically, otherwise working engineers
1857 would not encounter such programming.
1858 \item Combine the prototype's programming language with Isabelle's
1859 powerful function package and probably with more of SML's
1860 pattern-matching features; include parallel execution on multi-core
1861 machines into the language desing.
1862 \item Extend the prototype's Lucas-Interpreter such that it also
1863 handles functions defined by use of Isabelle's functions package; and
1864 generalize Isabelle's code generator such that efficient code for the
1865 whole of the defined programming language can be generated (for
1866 multi-core machines).
1867 \item Develop an efficient development environment with
1868 integration of programming and proving, with management not only of
1869 Isabelle theories, but also of large collections of specifications and
1872 Provided successful accomplishment, these points provide distinguished
1873 components for virtual workbenches appealing to practictioner of
1874 engineering in the near future.
1876 \medskip And all programming with a TP-based language will
1877 subsequently create interactive tutoring as a side-effect:
1878 Lucas-Interpretation not only provides an interactive programming
1879 environment, Lucas-Interpretation also can provide TP-based services
1880 for a flexible dialog component with adaptive user guidance for
1881 independent and inquiry-based learning.
1884 \bibliographystyle{alpha}
1885 \bibliography{references}