1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,2135 @@
1.4 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.5 +% Electronic Journal of Mathematics and Technology (eJMT) %
1.6 +% style sheet for LaTeX. Please do not modify sections %
1.7 +% or commands marked 'eJMT'. %
1.8 +% %
1.9 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.10 +% %
1.11 +% eJMT commands %
1.12 +% %
1.13 +\documentclass[12pt,a4paper]{article}% %
1.14 +\usepackage{times} %
1.15 +\usepackage{amsfonts,amsmath,amssymb} %
1.16 +\usepackage[a4paper]{geometry} %
1.17 +\usepackage{fancyhdr} %
1.18 +\usepackage{color} %
1.19 +\usepackage[pdftex]{hyperref} % see note below %
1.20 +\usepackage{graphicx}% %
1.21 +\hypersetup{ %
1.22 + a4paper, %
1.23 + breaklinks %
1.24 +} %
1.25 +% %
1.26 +\newtheorem{theorem}{Theorem} %
1.27 +\newtheorem{acknowledgement}[theorem]{Acknowledgement} %
1.28 +\newtheorem{algorithm}[theorem]{Algorithm} %
1.29 +\newtheorem{axiom}[theorem]{Axiom} %
1.30 +\newtheorem{case}[theorem]{Case} %
1.31 +\newtheorem{claim}[theorem]{Claim} %
1.32 +\newtheorem{conclusion}[theorem]{Conclusion} %
1.33 +\newtheorem{condition}[theorem]{Condition} %
1.34 +\newtheorem{conjecture}[theorem]{Conjecture} %
1.35 +\newtheorem{corollary}[theorem]{Corollary} %
1.36 +\newtheorem{criterion}[theorem]{Criterion} %
1.37 +\newtheorem{definition}[theorem]{Definition} %
1.38 +\newtheorem{example}[theorem]{Example} %
1.39 +\newtheorem{exercise}[theorem]{Exercise} %
1.40 +\newtheorem{lemma}[theorem]{Lemma} %
1.41 +\newtheorem{notation}[theorem]{Notation} %
1.42 +\newtheorem{problem}[theorem]{Problem} %
1.43 +\newtheorem{proposition}[theorem]{Proposition} %
1.44 +\newtheorem{remark}[theorem]{Remark} %
1.45 +\newtheorem{solution}[theorem]{Solution} %
1.46 +\newtheorem{summary}[theorem]{Summary} %
1.47 +\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } %
1.48 +{\ \rule{0.5em}{0.5em}} %
1.49 +% %
1.50 +% eJMT page dimensions %
1.51 +% %
1.52 +\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
1.53 +% %
1.54 +% eJMT header & footer %
1.55 +% %
1.56 +\newcounter{ejmtFirstpage} %
1.57 +\setcounter{ejmtFirstpage}{1} %
1.58 +\pagestyle{empty} %
1.59 +\setlength{\headheight}{14pt} %
1.60 +\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
1.61 +\pagestyle{fancyplain} %
1.62 +\fancyhf{} %
1.63 +\fancyhead[c]{\small The Electronic Journal of Mathematics%
1.64 +\ and Technology, Volume 1, Number 1, ISSN 1933-2823} %
1.65 +\cfoot{% %
1.66 + \ifnum\value{ejmtFirstpage}=0% %
1.67 + {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% %
1.68 + \else\setcounter{ejmtFirstpage}{0}\fi% %
1.69 +} %
1.70 +% %
1.71 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.72 +%
1.73 +% Please place your own definitions here
1.74 +%
1.75 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.76 +\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.77 +
1.78 +\usepackage{color}
1.79 +\definecolor{lgray}{RGB}{238,238,238}
1.80 +
1.81 +\usepackage{hyperref}
1.82 +
1.83 +%
1.84 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.85 +% %
1.86 +% How to use hyperref %
1.87 +% ------------------- %
1.88 +% %
1.89 +% Probably the only way you will need to use the hyperref %
1.90 +% package is as follows. To make some text, say %
1.91 +% "My Text Link", into a link to the URL %
1.92 +% http://something.somewhere.com/mystuff, use %
1.93 +% %
1.94 +% \href{http://something.somewhere.com/mystuff}{My Text Link}
1.95 +% %
1.96 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.97 +%
1.98 +\begin{document}
1.99 +%
1.100 +% document title
1.101 +%
1.102 +\title{Trials with TP-based Programming
1.103 +\\
1.104 +for Interactive Course Material}%
1.105 +%
1.106 +% Single author. Please supply at least your name,
1.107 +% email address, and affiliation here.
1.108 +%
1.109 +\author{\begin{tabular}{c}
1.110 +\textit{Jan Ro\v{c}nik} \\
1.111 +jan.rocnik@student.tugraz.at \\
1.112 +IST, SPSC\\
1.113 +Graz University of Technology\\
1.114 +Austria\end{tabular}
1.115 +}%
1.116 +%
1.117 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.118 +% %
1.119 +% eJMT commands - do not change these %
1.120 +% %
1.121 +\date{} %
1.122 +\maketitle %
1.123 +% %
1.124 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.125 +%
1.126 +% abstract
1.127 +%
1.128 +\begin{abstract}
1.129 +
1.130 +Traditional course material in engineering disciplines lacks an
1.131 +important component, interactive support for step-wise problem
1.132 +solving. Theorem-Proving (TP) technology is appropriate for one part
1.133 +of such support, in checking user-input. For the other part of such
1.134 +support, guiding the learner towards a solution, another kind of
1.135 +technology is required.
1.136 +
1.137 +Both kinds of support can be achieved by so-called
1.138 +Lucas-Interpretation which combines deduction and computation and, for
1.139 +the latter, uses a novel kind of programming language. This language
1.140 +is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
1.141 +programming language''.
1.142 +
1.143 +This paper is the experience report of the first ``application
1.144 +programmer'' using this language for creating exercises in step-wise
1.145 +problem solving for an advanced lab in Signal Processing. The tasks
1.146 +involved in TP-based programming are described together with the
1.147 +experience gained from a prototype of the programming language and of
1.148 +it's interpreter.
1.149 +
1.150 +The report concludes with a positive proof of concept, states
1.151 +insufficiency usability of the prototype and captures the requirements
1.152 +for further development of both, the programming language and the
1.153 +interpreter.
1.154 +%
1.155 +\end{abstract}%
1.156 +%
1.157 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.158 +% %
1.159 +% eJMT command %
1.160 +% %
1.161 +\thispagestyle{fancy} %
1.162 +% %
1.163 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.164 +%
1.165 +% Please use the following to indicate sections, subsections,
1.166 +% etc. Please also use \subsubsection{...}, \paragraph{...}
1.167 +% and \subparagraph{...} as necessary.
1.168 +%
1.169 +
1.170 +\section{Introduction}\label{intro}
1.171 +
1.172 +% \paragraph{Didactics of mathematics}
1.173 +%WN: wenn man in einem high-quality paper von 'didactics' spricht,
1.174 +%WN muss man am state-of-the-art ankn"upfen -- siehe
1.175 +%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
1.176 +% faces a specific issue, a gap
1.177 +% between (1) introduction of math concepts and skills and (2)
1.178 +% application of these concepts and skills, which usually are separated
1.179 +% into different units in curricula (for good reasons). For instance,
1.180 +% (1) teaching partial fraction decomposition is separated from (2)
1.181 +% application for inverse Z-transform in signal processing.
1.182 +%
1.183 +% \par This gap is an obstacle for applying math as an fundamental
1.184 +% thinking technology in engineering: In (1) motivation is lacking
1.185 +% because the question ``What is this stuff good for?'' cannot be
1.186 +% treated sufficiently, and in (2) the ``stuff'' is not available to
1.187 +% students in higher semesters as widespread experience shows.
1.188 +%
1.189 +% \paragraph{Motivation} taken by this didactic issue on the one hand,
1.190 +% and ongoing research and development on a novel kind of educational
1.191 +% mathematics assistant at Graz University of
1.192 +% Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
1.193 +% scope with this issue on the other hand, several institutes are
1.194 +% planning to join their expertise: the Institute for Information
1.195 +% Systems and Computer Media (IICM), the Institute for Software
1.196 +% Technology (IST), the Institutes for Mathematics, the Institute for
1.197 +% Signal Processing and Speech Communication (SPSC), the Institute for
1.198 +% Structural Analysis and the Institute of Electrical Measurement and
1.199 +% Measurement Signal Processing.
1.200 +%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
1.201 +%WN und damit zu verg"anglich.
1.202 +% \par This thesis is the first attempt to tackle the above mentioned
1.203 +% issue, it focuses on Telematics, because these specific studies focus
1.204 +% on mathematics in \emph{STEOP}, the introductory orientation phase in
1.205 +% Austria. \emph{STEOP} is considered an opportunity to investigate the
1.206 +% impact of {\sisac}'s prototype on the issue and others.
1.207 +%
1.208 +
1.209 +Traditional course material in engineering disciplines lacks an
1.210 +important component, interactive support for step-wise problem
1.211 +solving. The lack becomes evident by comparing existing course
1.212 +material with the sheets collected from written exams (in case solving
1.213 +engineering problems is {\em not} deteriorated to multiple choice
1.214 +tests) on the topics addressed by the materials.
1.215 +Theorem-Proving (TP) technology can provide such support by
1.216 +specific services. An important part of such services is called
1.217 +``next-step-guidance'', generated by a specific kind of ``TP-based
1.218 +programming language''. In the
1.219 +{\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
1.220 +a language is prototyped in line with~\cite{plmms10} and built upon
1.221 +the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}
1.222 +\footnote{http://isabelle.in.tum.de/}.
1.223 +The TP services are coordinated by a specific interpreter for the
1.224 +programming language, called
1.225 +Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language
1.226 + will be briefly re-introduced in order to make the paper
1.227 +self-contained.
1.228 +
1.229 +The main part of the paper is an account of first experiences
1.230 +with programming in this TP-based language. The experience was gained
1.231 +in a case study by the author. The author was considered an ideal
1.232 +candidate for this study for the following reasons: as a student in
1.233 +Telematics (computer science with focus on Signal Processing) he had
1.234 +general knowledge in programming as well as specific domain knowledge
1.235 +in Signal Processing; and he was {\em not} involved in the development of
1.236 +{\sisac}'s programming language and interpreter, thus being a novice to the
1.237 +language.
1.238 +
1.239 +The goals of the case study were: (1) to identify some TP-based programs for
1.240 +interactive course material for a specific ``Advanced Signal
1.241 +Processing Lab'' in a higher semester, (2) respective program
1.242 +development with as little advice as possible from the {\sisac}-team and (3)
1.243 +to document records and comments for the main steps of development in an
1.244 +Isabelle theory; this theory should provide guidelines for future programmers.
1.245 +An excerpt from this theory is the main part of this paper.
1.246 +\par
1.247 +
1.248 +\medskip The major example resulting from the case study will be used
1.249 +as running example throughout this paper. This example requires a
1.250 +program resembling the size of real-world applications in engineering;
1.251 +such a size was considered essential for the case study, since there
1.252 +are many small programs for a long time (mainly concerned with
1.253 +elementary Computer Algebra like simplification, equation solving,
1.254 +calculus, etc.~\footnote{The programs existing in the {\sisac}
1.255 +prototype are found at
1.256 +http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})
1.257 +
1.258 +\paragraph{The mathematical background of the running example} is the
1.259 +following: In Signal Processing, ``the ${\cal Z}$-transform for
1.260 +discrete-time signals is the counterpart of the Laplace transform for
1.261 +continuous-time signals, and they each have a similar relationship to
1.262 +the corresponding Fourier transform. One motivation for introducing
1.263 +this generalization is that the Fourier transform does not converge
1.264 +for all sequences, and it is useful to have a generalization of the
1.265 +Fourier transform that encompasses a broader class of signals. A
1.266 +second advantage is that in analytic problems, the ${\cal Z}$-transform
1.267 +notation is often more convenient than the Fourier transform
1.268 +notation.'' ~\cite[p. 128]{oppenheim2010discrete}. The ${\cal Z}$-transform
1.269 +is defined as
1.270 +\begin{equation*}
1.271 +X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}
1.272 +\end{equation*}
1.273 +where a discrete time sequence $x[n]$ is transformed into the function
1.274 +$X(z)$ where $z$ is a continuous complex variable. The inverse
1.275 +function is addressed in the running example and can be determined by
1.276 +the integral
1.277 +\begin{equation*}
1.278 +x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz
1.279 +\end{equation*}
1.280 +where the letter $C$ represents a contour within the range of
1.281 +convergence of the ${\cal Z}$-transform. The unit circle can be a special
1.282 +case of this contour. Remember that $j$ is the complex number in the
1.283 +domain of engineering. As this transform requires high effort to
1.284 +be solved, tables of commonly used transform pairs are used in
1.285 +education as well as in engineering practice; such tables can be found
1.286 +at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.
1.287 +A completely solved and more detailed example can be found at
1.288 +~\cite[p. 149f]{oppenheim2010discrete}.
1.289 +
1.290 +Following conventions in engineering education and in practice, the
1.291 +running example solves the problem by use of a table.
1.292 +
1.293 +\paragraph{Support for interactive stepwise problem solving} in the
1.294 +{\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,
1.295 +the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:
1.296 +A student inputs formulas line by line on the \textit{``Worksheet''},
1.297 +and each step (i.e. each formula on completion) is immediately checked
1.298 +by the system, such that at most {\em one inconsistent} formula can reside on
1.299 +the Worksheet (on the input line, marked by the red $\otimes$).
1.300 +\begin{figure} [htb]
1.301 +\begin{center}
1.302 +\includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
1.303 +%\includegraphics[width=140mm]{fig/isac-Ztrans-math}
1.304 +\caption{Step-wise problem solving guided by the TP-based program
1.305 +\label{fig-interactive}}
1.306 +\end{center}
1.307 +\end{figure}
1.308 +If the student gets stuck and does not know the formula to proceed
1.309 +with, there is the button \framebox{NEXT} presenting the next formula
1.310 +on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the
1.311 +final result in case the student is not interested in intermediate
1.312 +steps.
1.313 +
1.314 +Adaptive dialogue guidance is already under
1.315 +construction~\cite{gdaroczy-EP-13} and the two buttons will disappear,
1.316 +since their presence is not wanted in many learning scenarios (in
1.317 +particular, {\em not} in written exams).
1.318 +
1.319 +The buttons \framebox{Theories}, \framebox{Problems} and
1.320 +\framebox{Methods} are the entry points for interactive lookup of the
1.321 +underlying knowledge. For instance, pushing \framebox{Theories} in
1.322 +the configuration shown in Fig.\ref{fig-interactive}, pops up a
1.323 +``Theory browser'' displaying the theorem(s) justifying the current
1.324 +step. The browser allows to lookup all other theories, thus
1.325 +supporting indepentend investigation of underlying definitions,
1.326 +theorems, proofs --- where the HTML representation of the browsers is
1.327 +ready for arbitrary multimedia add-ons. Likewise, the browsers for
1.328 +\framebox{Problems} and \framebox{Methods} support context sensitive
1.329 +as well as interactive access to specifications and programs
1.330 +respectively.
1.331 +
1.332 +There is also a simple web-based representation of knowledge items;
1.333 +the items under consideration in this paper can be looked up as
1.334 +well
1.335 +~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Inverse\_Z\_Transform.thy}}}
1.336 +~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Partial\_Fractions.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Partial\_Fractions.thy}}}
1.337 +~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Build\_Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Build\_Inverse\_Z\_Transform.thy}}}.
1.338 +
1.339 +% can be explained by having a look at
1.340 +% Fig.\ref{fig-interactive} which shows the beginning of the interactive
1.341 +% construction of a solution for the problem. This construction is done in the
1.342 +% right window named ``Worksheet''.
1.343 +% \par
1.344 +% User-interaction on the Worksheet is {\em checked} and {\em guided} by
1.345 +% TP services:
1.346 +% \begin{enumerate}
1.347 +% \item Formulas input by the user are {\em checked} by TP: such a
1.348 +% formula establishes a proof situation --- the prover has to derive the
1.349 +% formula from the logical context. The context is built up from the
1.350 +% formal specification of the problem (here hidden from the user) by the
1.351 +% Lucas-Interpreter.
1.352 +% \item If the user gets stuck, the program developed below in this
1.353 +% paper ``knows the next step'' and Lucas-Interpretation provides services
1.354 +% featuring so-called ``next-step-guidance''; this is out of scope of this
1.355 +% paper and can be studied in~\cite{gdaroczy-EP-13}.
1.356 +% \end{enumerate} It should be noted that the programmer using the
1.357 +% TP-based language is not concerned with interaction at all; we will
1.358 +% see that the program contains neither input-statements nor
1.359 +% output-statements. Rather, interaction is handled by the interpreter
1.360 +% of the language.
1.361 +%
1.362 +% So there is a clear separation of concerns: Dialogues are adapted by
1.363 +% dialogue authors (in Java-based tools), using TP services provided by
1.364 +% Lucas-Interpretation. The latter acts on programs developed by
1.365 +% mathematics-authors (in Isabelle/ML); their task is concern of this
1.366 +% paper.
1.367 +
1.368 +\bigskip The paper is structured as follows: The introduction
1.369 +\S\ref{intro} is followed by a brief re-introduction of the TP-based
1.370 +programming language in \S\ref{PL}, which extends the executable
1.371 +fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
1.372 +play a specific role in Lucas-Interpretation and in providing the TP
1.373 +services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
1.374 +the main steps in developing the program for the running example:
1.375 +prepare domain knowledge, implement the formal specification of the
1.376 +problem, prepare the environment for the interpreter, implement the
1.377 +program in \S\ref{isabisac} to \S\ref{progr} respectively.
1.378 +The work-flow of programming, debugging and testing is
1.379 +described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
1.380 +give directions identified for future development.
1.381 +
1.382 +
1.383 +\section{\isac's Prototype for a Programming Language}\label{PL}
1.384 +The prototype of the language and of the Lucas-Interpreter is briefly
1.385 +described from the point of view of a programmer. The language extends
1.386 +the executable fragment of Higher-Order Logic (HOL) in the theorem prover
1.387 +Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
1.388 +
1.389 +\subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
1.390 +The executable fragment consists of data-type and function
1.391 +definitions. It's usability even suggests that fragment for
1.392 +introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming
1.393 +languages. Thus there are
1.394 +\begin{description}
1.395 +\item[base types,] in particular \textit{bool}, the type of truth
1.396 +values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
1.397 +natural, integer and complex numbers respectively in mathematics.
1.398 +\item[type constructors] allow to define arbitrary types, from
1.399 +\textit{set}, \textit{list} to advanced data-structures like
1.400 +\textit{trees}, red-black-trees etc.
1.401 +\item[function types,] denoted by $\Rightarrow$.
1.402 +\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
1.403 +type polymorphism. Isabelle automatically computes the type of each
1.404 +variable in a term by use of Hindley-Milner type inference
1.405 +\cite{pl:hind97,Milner-78}.
1.406 +\end{description}
1.407 +
1.408 +\textbf{Terms} are formed as in functional programming by applying
1.409 +functions to arguments. If $f$ is a function of type
1.410 +$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
1.411 +$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
1.412 +has type $\tau$. There are many predefined infix symbols like $+$ and
1.413 +$\leq$ most of which are overloaded for various types.
1.414 +
1.415 +HOL also supports some basic constructs from functional programming:
1.416 +{\footnotesize\it\label{isabelle-stmts}
1.417 +\begin{tabbing} 123\=\kill
1.418 +01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
1.419 +02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
1.420 +03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
1.421 + \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
1.422 +\end{tabbing}}
1.423 +\noindent The running example's program uses some of these elements
1.424 +(marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
1.425 +let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
1.426 +is an Isabelle term with specific function constants like {\tt
1.427 +program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
1.428 +Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
1.429 +respectively.
1.430 +
1.431 +% Terms may also contain $\lambda$-abstractions. For example, $\lambda
1.432 +% x. \; x$ is the identity function.
1.433 +
1.434 +%JR warum auskommentiert? WN2...
1.435 +%WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
1.436 +%WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
1.437 +%WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
1.438 +%WN2 gel"oscht.
1.439 +%WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
1.440 +%WN2 Platz f"ur Anderes weg.
1.441 +
1.442 +\textbf{Formulae} are terms of type \textit{bool}. There are the basic
1.443 +constants \textit{True} and \textit{False} and the usual logical
1.444 +connectives (in decreasing order of precedence): $\neg, \land, \lor,
1.445 +\rightarrow$.
1.446 +
1.447 +\textbf{Equality} is available in the form of the infix function $=$
1.448 +of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
1.449 +formulas, where it means ``if and only if''.
1.450 +
1.451 +\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
1.452 +P$. Quantifiers lead to non-executable functions, so functions do not
1.453 +always correspond to programs, for instance, if comprising \\$(
1.454 +\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
1.455 +\;)$.
1.456 +
1.457 +\subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
1.458 +The prototype extends Isabelle's language by specific statements
1.459 +called tactics~\footnote{{\sisac}'s. These tactics are different from
1.460 +Isabelle's tactics: the former concern steps in a calculation, the
1.461 +latter concern proofs.}. For the programmer these
1.462 +statements are functions with the following signatures:
1.463 +
1.464 +\begin{description}
1.465 +\item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
1.466 +term} * {\it term}\;{\it list}$:
1.467 +this tactic applies {\it theorem} to a {\it term} yielding a {\it
1.468 +term} and a {\it term list}, the list are assumptions generated by
1.469 +conditional rewriting. For instance, the {\it theorem}
1.470 +$b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
1.471 +applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
1.472 +$(\frac{2}{3}, [x\not=0])$.
1.473 +
1.474 +\item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
1.475 +term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
1.476 +this tactic applies {\it ruleset} to a {\it term}; {\it ruleset} is
1.477 +a confluent and terminating term rewrite system, in general. If
1.478 +none of the rules ({\it theorem}s) is applicable on interpretation
1.479 +of this tactic, an exception is thrown.
1.480 +
1.481 +% \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
1.482 +% theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
1.483 +% list}$:
1.484 +%
1.485 +% \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
1.486 +% ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
1.487 +% list}$:
1.488 +
1.489 +%SPACEvvv
1.490 +\item[Substitute:] ${\it substitution}\Rightarrow{\it
1.491 +term}\Rightarrow{\it term}$: allows to access sub-terms.
1.492 +%SPACE^^^
1.493 +
1.494 +\item[Take:] ${\it term}\Rightarrow{\it term}$:
1.495 +this tactic has no effect in the program; but it creates a side-effect
1.496 +by Lucas-Interpretation (see below) and writes {\it term} to the
1.497 +Worksheet.
1.498 +
1.499 +\item[Subproblem:] ${\it theory} * {\it specification} * {\it
1.500 +method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
1.501 +this tactic is a generalisation of a function call: it takes an
1.502 +\textit{argument list} as usual, and additionally a triple consisting
1.503 +of an Isabelle \textit{theory}, an implicit \textit{specification} of the
1.504 +program and a \textit{method} containing data for Lucas-Interpretation,
1.505 +last not least a program (as an explicit specification)~\footnote{In
1.506 +interactive tutoring these three items can be determined explicitly
1.507 +by the user.}.
1.508 +\end{description}
1.509 +The tactics play a specific role in
1.510 +Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
1.511 +break-points where, as a side-effect, a line is added to a calculation
1.512 +as a protocol for proceeding towards a solution in step-wise problem
1.513 +solving. At the same points Lucas-Interpretation serves interactive
1.514 +tutoring and hands over control to the user. The user is free to
1.515 +investigate underlying knowledge, applicable theorems, etc. And the
1.516 +user can proceed constructing a solution by input of a tactic to be
1.517 +applied or by input of a formula; in the latter case the
1.518 +Lucas-Interpreter has built up a logical context (initialised with the
1.519 +precondition of the formal specification) such that Isabelle can
1.520 +derive the formula from this context --- or give feedback, that no
1.521 +derivation can be found.
1.522 +
1.523 +\subsection{Tactics as Control Flow Statements}
1.524 +The flow of control in a program can be determined by {\tt if then else}
1.525 +and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
1.526 +by additional tactics:
1.527 +\begin{description}
1.528 +\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
1.529 +term}$: iterates over tactics which take a {\it term} as argument as
1.530 +long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
1.531 +not be applicable).
1.532 +
1.533 +\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
1.534 +if {\it tactic} is applicable, then it is applied to {\it term},
1.535 +otherwise {\it term} is passed on without changes.
1.536 +
1.537 +\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
1.538 +term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
1.539 +it is applied to the first {\it term} yielding another {\it term},
1.540 +otherwise the second {\it tactic} is applied; if none is applicable an
1.541 +exception is raised.
1.542 +
1.543 +\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
1.544 +term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
1.545 +first {\it term} yielding an intermediate term (not appearing in the
1.546 +signature) to which the second {\it tactic} is applied.
1.547 +
1.548 +\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
1.549 +term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
1.550 +{\it tactic} is applied to the first {\it term} yielding an
1.551 +intermediate term (not appearing in the signature); the intermediate
1.552 +term is added to the environment the first {\it term} is evaluated in
1.553 +etc. as long as the first {\it term} is true.
1.554 +\end{description}
1.555 +The tactics are not treated as break-points by Lucas-Interpretation
1.556 +and thus do neither contribute to the calculation nor to interaction.
1.557 +
1.558 +\section{Concepts and Tasks in TP-based Programming}\label{trial}
1.559 +%\section{Development of a Program on Trial}
1.560 +
1.561 +This section presents all the concepts involved in TP-based
1.562 +programming and all the tasks to be accomplished by programmers. The
1.563 +presentation uses the running example from
1.564 +Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
1.565 +
1.566 +\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
1.567 +
1.568 +%WN was Fachleute unter obigem Titel interessiert findet sich
1.569 +%WN unterhalb des auskommentierten Textes.
1.570 +
1.571 +%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
1.572 +%WN auf Computer-Mathematiker fokussiert.
1.573 +% \paragraph{As mentioned in the introduction,} a prototype of an
1.574 +% educational math assistant called
1.575 +% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
1.576 +% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
1.577 +% the gap between (1) introducation and (2) application of mathematics:
1.578 +% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
1.579 +% requires each fact and each action justified by formal logic, so
1.580 +% {{{\sisac}{}}} makes justifications transparent to students in
1.581 +% interactive step-wise problem solving. By that way {{\sisac}} already
1.582 +% can serve both:
1.583 +% \begin{enumerate}
1.584 +% \item Introduction of math stuff (in e.g. partial fraction
1.585 +% decomposition) by stepwise explaining and exercising respective
1.586 +% symbolic calculations with ``next step guidance (NSG)'' and rigorously
1.587 +% checking steps freely input by students --- this also in context with
1.588 +% advanced applications (where the stuff to be taught in higher
1.589 +% semesters can be skimmed through by NSG), and
1.590 +% \item Application of math stuff in advanced engineering courses
1.591 +% (e.g. problems to be solved by inverse Z-transform in a Signal
1.592 +% Processing Lab) and now without much ado about basic math techniques
1.593 +% (like partial fraction decomposition): ``next step guidance'' supports
1.594 +% students in independently (re-)adopting such techniques.
1.595 +% \end{enumerate}
1.596 +% Before the question is answers, how {{\sisac}}
1.597 +% accomplishes this task from a technical point of view, some remarks on
1.598 +% the state-of-the-art is given, therefor follow up Section~\ref{emas}.
1.599 +%
1.600 +% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
1.601 +%
1.602 +% \paragraph{Educational software in mathematics} is, if at all, based
1.603 +% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
1.604 +% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
1.605 +% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
1.606 +% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
1.607 +% base technologies are used to program math lessons and sometimes even
1.608 +% exercises. The latter are cumbersome: the steps towards a solution of
1.609 +% such an interactive exercise need to be provided with feedback, where
1.610 +% at each step a wide variety of possible input has to be foreseen by
1.611 +% the programmer - so such interactive exercises either require high
1.612 +% development efforts or the exercises constrain possible inputs.
1.613 +%
1.614 +% \subparagraph{A new generation} of educational math assistants (EMAs)
1.615 +% is emerging presently, which is based on Theorem Proving (TP). TP, for
1.616 +% instance Isabelle and Coq, is a technology which requires each fact
1.617 +% and each action justified by formal logic. Pushed by demands for
1.618 +% \textit{proven} correctness of safety-critical software TP advances
1.619 +% into software engineering; from these advancements computer
1.620 +% mathematics benefits in general, and math education in particular. Two
1.621 +% features of TP are immediately beneficial for learning:
1.622 +%
1.623 +% \paragraph{TP have knowledge in human readable format,} that is in
1.624 +% standard predicate calculus. TP following the LCF-tradition have that
1.625 +% knowledge down to the basic definitions of set, equality,
1.626 +% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
1.627 +% following the typical deductive development of math, natural numbers
1.628 +% are defined and their properties
1.629 +% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
1.630 +% etc. Present knowledge mechanized in TP exceeds high-school
1.631 +% mathematics by far, however by knowledge required in software
1.632 +% technology, and not in other engineering sciences.
1.633 +%
1.634 +% \paragraph{TP can model the whole problem solving process} in
1.635 +% mathematical problem solving {\em within} a coherent logical
1.636 +% framework. This is already being done by three projects, by
1.637 +% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
1.638 +% \par
1.639 +% Having the whole problem solving process within a logical coherent
1.640 +% system, such a design guarantees correctness of intermediate steps and
1.641 +% of the result (which seems essential for math software); and the
1.642 +% second advantage is that TP provides a wealth of theories which can be
1.643 +% exploited for mechanizing other features essential for educational
1.644 +% software.
1.645 +%
1.646 +% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
1.647 +%
1.648 +% One essential feature for educational software is feedback to user
1.649 +% input and assistance in coming to a solution.
1.650 +%
1.651 +% \paragraph{Checking user input} by ATP during stepwise problem solving
1.652 +% is being accomplished by the three projects mentioned above
1.653 +% exclusively. They model the whole problem solving process as mentioned
1.654 +% above, so all what happens between formalized assumptions (or formal
1.655 +% specification) and goal (or fulfilled postcondition) can be
1.656 +% mechanized. Such mechanization promises to greatly extend the scope of
1.657 +% educational software in stepwise problem solving.
1.658 +%
1.659 +% \paragraph{NSG (Next step guidance)} comprises the system's ability to
1.660 +% propose a next step; this is a challenge for TP: either a radical
1.661 +% restriction of the search space by restriction to very specific
1.662 +% problem classes is required, or much care and effort is required in
1.663 +% designing possible variants in the process of problem solving
1.664 +% \cite{proof-strategies-11}.
1.665 +% \par
1.666 +% Another approach is restricted to problem solving in engineering
1.667 +% domains, where a problem is specified by input, precondition, output
1.668 +% and postcondition, and where the postcondition is proven by ATP behind
1.669 +% the scenes: Here the possible variants in the process of problem
1.670 +% solving are provided with feedback {\em automatically}, if the problem
1.671 +% is described in a TP-based programing language: \cite{plmms10} the
1.672 +% programmer only describes the math algorithm without caring about
1.673 +% interaction (the respective program is functional and even has no
1.674 +% input or output statements!); interaction is generated as a
1.675 +% side-effect by the interpreter --- an efficient separation of concern
1.676 +% between math programmers and dialog designers promising application
1.677 +% all over engineering disciplines.
1.678 +%
1.679 +%
1.680 +% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
1.681 +% Authoring new mathematics knowledge in {{\sisac}} can be compared with
1.682 +% ``application programing'' of engineering problems; most of such
1.683 +% programing uses CAS-based programing languages (CAS = Computer Algebra
1.684 +% Systems; e.g. Mathematica's or Maple's programing language).
1.685 +%
1.686 +% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
1.687 +% \cite{plmms10} for describing how to construct a solution to an
1.688 +% engineering problem and for calling equation solvers, integration,
1.689 +% etc~\footnote{Implementation of CAS-like functionality in TP is not
1.690 +% primarily concerned with efficiency, but with a didactic question:
1.691 +% What to decide for: for high-brow algorithms at the state-of-the-art
1.692 +% or for elementary algorithms comprehensible for students?} within TP;
1.693 +% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
1.694 +% are impossible for CAS which have no logics underlying.
1.695 +%
1.696 +% \subparagraph{Authoring is perfect} by writing such TP based programs;
1.697 +% the application programmer is not concerned with interaction or with
1.698 +% user guidance: this is concern of a novel kind of program interpreter
1.699 +% called Lucas-Interpreter. This interpreter hands over control to a
1.700 +% dialog component at each step of calculation (like a debugger at
1.701 +% breakpoints) and calls automated TP to check user input following
1.702 +% personalized strategies according to a feedback module.
1.703 +% \par
1.704 +% However ``application programing with TP'' is not done with writing a
1.705 +% program: according to the principles of TP, each step must be
1.706 +% justified. Such justifications are given by theorems. So all steps
1.707 +% must be related to some theorem, if there is no such theorem it must
1.708 +% be added to the existing knowledge, which is organized in so-called
1.709 +% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
1.710 +% Isabelle comprises a mechanism (called ``axiomatization''), which
1.711 +% allows to omit proofs. Such a theorem is shown in
1.712 +% Example~\ref{eg:neuper1}.
1.713 +
1.714 +The running example requires to determine the inverse ${\cal Z}$-transform
1.715 +for a class of functions. The domain of Signal Processing
1.716 +is accustomed to specific notation for the resulting functions, which
1.717 +are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
1.718 +function, $n$ is the argument and the brackets indicate that the
1.719 +arguments are discrete. Surprisingly, Isabelle accepts the rules for
1.720 +$z^{-1}$ in this traditional notation~\footnote{Isabelle
1.721 +experts might be particularly surprised, that the brackets do not
1.722 +cause errors in typing (as lists).}:
1.723 +%\vbox{
1.724 +% \begin{example}
1.725 + \label{eg:neuper1}
1.726 + {\footnotesize\begin{tabbing}
1.727 + 123\=123\=123\=123\=\kill
1.728 +
1.729 + 01\>axiomatization where \\
1.730 + 02\>\> rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\
1.731 + 03\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\
1.732 + 04\>\> rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\
1.733 + 05\>\> rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\
1.734 + 06\>\> rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\
1.735 + 07\>\> rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''
1.736 + \end{tabbing}}
1.737 +% \end{example}
1.738 +%}
1.739 +These 6 rules can be used as conditional rewrite rules, depending on
1.740 +the respective convergence radius. Satisfaction from accordance with traditional
1.741 +notation contrasts with the above word {\em axiomatization}: As TP-based, the
1.742 +programming language expects these rules as {\em proved} theorems, and
1.743 +not as axioms implemented in the above brute force manner; otherwise
1.744 +all the verification efforts envisaged (like proof of the
1.745 +post-condition, see below) would be meaningless.
1.746 +
1.747 +Isabelle provides a large body of knowledge, rigorously proved from
1.748 +the basic axioms of mathematics~\footnote{This way of rigorously
1.749 +deriving all knowledge from first principles is called the
1.750 +LCF-paradigm in TP.}. In the case of the ${\cal Z}$-transform the most advanced
1.751 +knowledge can be found in the theories on Multivariate
1.752 +Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
1.753 +building up knowledge such that a proof for the above rules would be
1.754 +reasonably short and easily comprehensible, still requires lots of
1.755 +work (and is definitely out of scope of our case study).
1.756 +
1.757 +%REMOVED DUE TO SPACE CONSTRAINTS
1.758 +%At the state-of-the-art in mechanization of knowledge in engineering
1.759 +%sciences, the process does not stop with the mechanization of
1.760 +%mathematics traditionally used in these sciences. Rather, ``Formal
1.761 +%Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
1.762 +%description of physical items. Signal Processing, for instance is
1.763 +%concerned with physical devices for signal acquisition and
1.764 +%reconstruction, which involve measuring a physical signal, storing it,
1.765 +%and possibly later rebuilding the original signal or an approximation
1.766 +%thereof. For digital systems, this typically includes sampling and
1.767 +%quantization; devices for signal compression, including audio
1.768 +%compression, image compression, and video compression, etc. ``Domain
1.769 +%engineering''\cite{db:dom-eng} is concerned with {\em specification}
1.770 +%of these devices' components and features; this part in the process of
1.771 +%mechanization is only at the beginning in domains like Signal
1.772 +%Processing.
1.773 +%
1.774 +%TP-based programming, concern of this paper, is determined to
1.775 +%add ``algorithmic knowledge'' to the mechanised body of knowledge.
1.776 +%% in Fig.\ref{fig:mathuni} on
1.777 +%% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.778 +%% starts with a formal {\em specification} of the problem to be solved.
1.779 +%% \begin{figure}
1.780 +%% \begin{center}
1.781 +%% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
1.782 +%% \caption{The three-dimensional universe of mathematics knowledge}
1.783 +%% \label{fig:mathuni}
1.784 +%% \end{center}
1.785 +%% \end{figure}
1.786 +%% The language for both axes is defined in the axis at the bottom, deductive
1.787 +%% knowledge, in {\sisac} represented by Isabelle's theories.
1.788 +
1.789 +\subsection{Preparation of Simplifiers for the Program}\label{simp}
1.790 +
1.791 +All evaluation in the prototype's Lucas-Interpreter is done by term rewriting on
1.792 +Isabelle's terms, see \S\ref{meth} below; in this section some of respective
1.793 +preparations are described. In order to work reliably with term rewriting, the
1.794 +respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
1.795 +then they are called (canonical) simplifiers. These properties do not go without
1.796 +saying, their establishment is a difficult task for the programmer; this task is
1.797 +not yet supported in the prototype.
1.798 +
1.799 +The prototype rewrites using theorems only. Axioms which are theorems as well
1.800 +have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
1.801 +assemble them in a rule-set and apply them in ML as follows:
1.802 +
1.803 +{\footnotesize
1.804 +\begin{verbatim}
1.805 + 01 val inverse_z = Rls
1.806 + 02 {id = "inverse_z",
1.807 + 03 rew_ord = dummy_ord,
1.808 + 04 erls = Erls,
1.809 + 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
1.810 + 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
1.811 + 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
1.812 + 08 errpatts = [],
1.813 + 09 scr = ""}
1.814 +\end{verbatim}}
1.815 +
1.816 +\noindent The items, line by line, in the above record have the following purpose:
1.817 +\begin{description}
1.818 +\item[01..02] the ML-value \textit{inverse\_z} stores it's identifier
1.819 +as a string for ``reflection'' when switching between the language
1.820 +layers of Isabelle/ML (like in the Lucas-Interpreter) and
1.821 +Isabelle/Isar (like in the example program on p.\pageref{s:impl} on
1.822 +line {\rm 12}).
1.823 +
1.824 +\item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
1.825 +\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
1.826 +(a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
1.827 +and (b) the assumptions of the \textit{rules} need not be evaluated
1.828 +(they just go into the context during rewriting).
1.829 +
1.830 +\item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
1.831 +also ML-functions (\S\ref{funs}) can come into this list as shown in
1.832 +\S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm}
1.833 +and \textit{Calc} respectively; for the purpose of reflection both
1.834 +contain their identifiers.
1.835 +
1.836 +\item[08..09] are error-patterns not discussed here and \textit{scr}
1.837 +is prepared to get a program, automatically generated by {\sisac} for
1.838 +producing intermediate rewrites when requested by the user.
1.839 +
1.840 +\end{description}
1.841 +
1.842 +%OUTCOMMENTED DUE TO SPACE RESTRICTIONS
1.843 +% \noindent It is advisable to immediately test rule-sets; for that
1.844 +% purpose an appropriate term has to be created; \textit{parse} takes a
1.845 +% context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
1.846 +% Z}^{-1}$) and creates a term:
1.847 +%
1.848 +% {\footnotesize
1.849 +% \begin{verbatim}
1.850 +% 01 ML {*
1.851 +% 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
1.852 +% 03 *}
1.853 +% 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1",
1.854 +% 05 "RealDef.real => RealDef.real => RealDef.real") $
1.855 +% 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...)
1.856 +% \end{verbatim}}
1.857 +%
1.858 +% \noindent The internal representation of the term, as required for
1.859 +% rewriting, consists of \textit{Const}ants, a pair of a string
1.860 +% \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
1.861 +% \textit{Free} and the respective constructor \textit{\$}. Now the
1.862 +% term can be rewritten by the rule-set \textit{inverse\_z}:
1.863 +%
1.864 +% {\footnotesize
1.865 +% \begin{verbatim}
1.866 +% 01 ML {*
1.867 +% 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
1.868 +% 03 term2str t';
1.869 +% 04 terms2str asm;
1.870 +% 05 *}
1.871 +% 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
1.872 +% 07 val it = "|| z || > 1 & || z || > </alpha>" : string
1.873 +% \end{verbatim}}
1.874 +%
1.875 +% \noindent The resulting term \textit{t} and the assumptions
1.876 +% \textit{asm} are converted to readable strings by \textit{term2str}
1.877 +% and \textit{terms2str}.
1.878 +
1.879 +\subsection{Preparation of ML-Functions}\label{funs}
1.880 +Some functionality required in programming, cannot be accomplished by
1.881 +rewriting. So the prototype has a mechanism to call functions within
1.882 +the rewrite-engine: certain redexes in Isabelle terms call these
1.883 +functions written in SML~\cite{pl:milner97}, the implementation {\em
1.884 +and} meta-language of Isabelle. The programmer has to use this
1.885 +mechanism.
1.886 +
1.887 +In the running example's program on p.\pageref{s:impl} the lines {\rm
1.888 +05} and {\rm 06} contain such functions; we go into the details with
1.889 +\textit{argument\_in X\_z;}. This function fetches the argument from a
1.890 +function application: Line {\rm 03} in the example calculation on
1.891 +p.\pageref{exp-calc} is created by line {\rm 06} of the example
1.892 +program on p.\pageref{s:impl} where the program's environment assigns
1.893 +the value \textit{X z} to the variable \textit{X\_z}; so the function
1.894 +shall extract the argument \textit{z}.
1.895 +
1.896 +\medskip In order to be recognised as a function constant in the
1.897 +program source the constant needs to be declared in a theory, here in
1.898 +\textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
1.899 +the context \textit{ctxt} of that theory:
1.900 +
1.901 +{\footnotesize
1.902 +\begin{verbatim}
1.903 +01 consts
1.904 +02 argument'_in :: "real => real" ("argument'_in _" 10)
1.905 +\end{verbatim}}
1.906 +
1.907 +%^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
1.908 +%^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
1.909 +%^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
1.910 +%^3.2^ \end{verbatim}}
1.911 +%^3.2^
1.912 +%^3.2^ \noindent Parsing produces a term \texttt{t} in internal
1.913 +%^3.2^ representation~\footnote{The attentive reader realizes the
1.914 +%^3.2^ differences between interal and extermal representation even in the
1.915 +%^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
1.916 +%^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
1.917 +%^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
1.918 +%^3.2^ constructor.
1.919 +The function body below is implemented directly in SML,
1.920 +i.e in an \texttt{ML \{* *\}} block; the function definition provides
1.921 +a unique prefix \texttt{eval\_} to the function name:
1.922 +
1.923 +{\footnotesize
1.924 +\begin{verbatim}
1.925 +01 ML {*
1.926 +02 fun eval_argument_in _
1.927 +03 "Build_Inverse_Z_Transform.argument'_in"
1.928 +04 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
1.929 +05 if is_Free arg (*could be something to be simplified before*)
1.930 +06 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
1.931 +07 else NONE
1.932 +08 | eval_argument_in _ _ _ _ = NONE;
1.933 +09 *}
1.934 +\end{verbatim}}
1.935 +
1.936 +\noindent The function body creates either \texttt{NONE}
1.937 +telling the rewrite-engine to search for the next redex, or creates an
1.938 +ad-hoc theorem for rewriting, thus the programmer needs to adopt many
1.939 +technicalities of Isabelle, for instance, the \textit{Trueprop}
1.940 +constant.
1.941 +
1.942 +\bigskip This sub-task particularly sheds light on basic issues in the
1.943 +design of a programming language, the integration of differential language
1.944 +layers, the layer of Isabelle/Isar and Isabelle/ML.
1.945 +
1.946 +Another point of improvement for the prototype is the rewrite-engine: The
1.947 +program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
1.948 +and {\rm 06} to
1.949 +
1.950 +{\small\it\label{s:impl}
1.951 +\begin{tabbing}
1.952 +123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.953 +\>{\rm 05/06}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
1.954 +\end{tabbing}}
1.955 +
1.956 +\noindent because nested function calls would require creating redexes
1.957 +inside-out; however, the prototype's rewrite-engine only works top down
1.958 +from the root of a term down to the leaves.
1.959 +
1.960 +How all these technicalities are to be checked in the prototype is
1.961 +shown in \S\ref{flow-prep} below.
1.962 +
1.963 +% \paragraph{Explicit Problems} require explicit methods to solve them, and within
1.964 +% this methods we have some explicit steps to do. This steps can be unique for
1.965 +% a special problem or refindable in other problems. No mather what case, such
1.966 +% steps often require some technical functions behind. For the solving process
1.967 +% of the Inverse Z Transformation and the corresponding partial fraction it was
1.968 +% neccessary to build helping functions like \texttt{get\_denominator},
1.969 +% \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
1.970 +% to filter the denominator or numerator out of a fraction, last one helps us to
1.971 +% get to know the bound variable in a equation.
1.972 +% \par
1.973 +% By taking \texttt{get\_denominator} as an example, we want to explain how to
1.974 +% implement new functions into the existing system and how we can later use them
1.975 +% in our program.
1.976 +%
1.977 +% \subsubsection{Find a place to Store the Function}
1.978 +%
1.979 +% The whole system builds up on a well defined structure of Knowledge. This
1.980 +% Knowledge sets up at the Path:
1.981 +% \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
1.982 +% For implementing the Function \texttt{get\_denominator} (which let us extract
1.983 +% the denominator out of a fraction) we have choosen the Theory (file)
1.984 +% \texttt{Rational.thy}.
1.985 +%
1.986 +% \subsubsection{Write down the new Function}
1.987 +%
1.988 +% In upper Theory we now define the new function and its purpose:
1.989 +% \begin{verbatim}
1.990 +% get_denominator :: "real => real"
1.991 +% \end{verbatim}
1.992 +% This command tells the machine that a function with the name
1.993 +% \texttt{get\_denominator} exists which gets a real expression as argument and
1.994 +% returns once again a real expression. Now we are able to implement the function
1.995 +% itself, upcoming example now shows the implementation of
1.996 +% \texttt{get\_denominator}.
1.997 +%
1.998 +% %\begin{example}
1.999 +% \label{eg:getdenom}
1.1000 +% \begin{verbatim}
1.1001 +%
1.1002 +% 01 (*
1.1003 +% 02 *("get_denominator",
1.1004 +% 03 * ("Rational.get_denominator", eval_get_denominator ""))
1.1005 +% 04 *)
1.1006 +% 05 fun eval_get_denominator (thmid:string) _
1.1007 +% 06 (t as Const ("Rational.get_denominator", _) $
1.1008 +% 07 (Const ("Rings.inverse_class.divide", _) $num
1.1009 +% 08 $denom)) thy =
1.1010 +% 09 SOME (mk_thmid thmid ""
1.1011 +% 10 (Print_Mode.setmp []
1.1012 +% 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1.1013 +% 12 Trueprop $ (mk_equality (t, denom)))
1.1014 +% 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
1.1015 +% %\end{example}
1.1016 +%
1.1017 +% Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
1.1018 +% there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
1.1019 +% splittet
1.1020 +% into its two parts (\texttt{\$num \$denom}). The lines before are additionals
1.1021 +% commands for declaring the function and the lines after are modeling and
1.1022 +% returning a real variable out of \texttt{\$denom}.
1.1023 +%
1.1024 +% \subsubsection{Add a test for the new Function}
1.1025 +%
1.1026 +% \paragraph{Everytime when adding} a new function it is essential also to add
1.1027 +% a test for it. Tests for all functions are sorted in the same structure as the
1.1028 +% knowledge it self and can be found up from the path:
1.1029 +% \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
1.1030 +% This tests are nothing very special, as a first prototype the functionallity
1.1031 +% of a function can be checked by evaluating the result of a simple expression
1.1032 +% passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
1.1033 +% \textit{just} created function \texttt{get\_denominator}.
1.1034 +%
1.1035 +% %\begin{example}
1.1036 +% \label{eg:getdenomtest}
1.1037 +% \begin{verbatim}
1.1038 +%
1.1039 +% 01 val thy = @{theory Isac};
1.1040 +% 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1.1041 +% 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1.1042 +% 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1.1043 +% 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
1.1044 +% %\end{example}
1.1045 +%
1.1046 +% \begin{description}
1.1047 +% \item[01] checks if the proofer set up on our {\sisac{}} System.
1.1048 +% \item[02] passes a simple expression (fraction) to our suddenly created
1.1049 +% function.
1.1050 +% \item[04] checks if the resulting variable is the correct one (in this case
1.1051 +% ``b'' the denominator) and returns.
1.1052 +% \item[05] handels the error case and reports that the function is not able to
1.1053 +% solve the given problem.
1.1054 +% \end{description}
1.1055 +
1.1056 +\subsection{Specification of the Problem}\label{spec}
1.1057 +%WN <--> \chapter 7 der Thesis
1.1058 +%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
1.1059 +
1.1060 +Mechanical treatment requires to translate a textual problem
1.1061 +description like in Fig.\ref{fig-interactive} on
1.1062 +p.\pageref{fig-interactive} into a {\em formal} specification. The
1.1063 +formal specification of the running example could look like is this
1.1064 +~\footnote{The ``TODO'' in the postcondition indicates, that postconditions
1.1065 +are not yet handled in the prototype; in particular, the postcondition, i.e.
1.1066 +the correctness of the result is not yet automatically proved.}:
1.1067 +
1.1068 +%WN Hier brauchen wir die Spezifikation des 'running example' ...
1.1069 +%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
1.1070 +%JR der post condition - die existiert für uns ja eigentlich nicht aka
1.1071 +%JR haben sie bis jetzt nicht beachtet WN...
1.1072 +%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
1.1073 +%JR2 done
1.1074 +
1.1075 +\label{eg:neuper2}
1.1076 +{\small\begin{tabbing}
1.1077 + 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1.1078 + %\hfill \\
1.1079 + \>Specification:\\
1.1080 + \> \>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}\}$\\
1.1081 + \>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
1.1082 + \>\>output \>: stepResponse $x[n]$ \\
1.1083 + \>\>postcond \>: TODO
1.1084 +\end{tabbing}}
1.1085 +
1.1086 +%JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt"
1.1087 +
1.1088 +% \begin{remark}
1.1089 +% Defining the postcondition requires a high amount mathematical
1.1090 +% knowledge, the difficult part in our case is not to set up this condition
1.1091 +% nor it is more to define it in a way the interpreter is able to handle it.
1.1092 +% Due the fact that implementing that mechanisms is quite the same amount as
1.1093 +% creating the programm itself, it is not avaible in our prototype.
1.1094 +% \label{rm:postcond}
1.1095 +% \end{remark}
1.1096 +
1.1097 +The implementation of the formal specification in the present
1.1098 +prototype, still bar-bones without support for authoring, is done
1.1099 +like that:
1.1100 +%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
1.1101 +
1.1102 +{\footnotesize\label{exp-spec}
1.1103 +\begin{verbatim}
1.1104 + 00 ML {*
1.1105 + 01 store_specification
1.1106 + 02 (prepare_specification
1.1107 + 03 "pbl_SP_Ztrans_inv"
1.1108 + 04 ["Jan Rocnik"]
1.1109 + 05 thy
1.1110 + 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1.1111 + 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1.1112 + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1.1113 + 09 ("#Find" , ["stepResponse n_eq"]),
1.1114 + 10 ("#Post" , [" TODO "])])
1.1115 + 11 prls
1.1116 + 12 NONE
1.1117 + 13 [["SignalProcessing","Z_Transform","Inverse"]]);
1.1118 + 14 *}
1.1119 +\end{verbatim}}
1.1120 +
1.1121 +Although the above details are partly very technical, we explain them
1.1122 +in order to document some intricacies of TP-based programming in the
1.1123 +present state of the {\sisac} prototype:
1.1124 +\begin{description}
1.1125 +\item[01..02]\textit{store\_specification:} stores the result of the
1.1126 +function \textit{prep\_specification} in a global reference
1.1127 +\textit{Unsynchronized.ref}, which causes principal conflicts with
1.1128 +Isabelle's asynchronous document model~\cite{Wenzel-11:doc-orient} and
1.1129 +parallel execution~\cite{Makarius-09:parall-proof} and is under
1.1130 +reconstruction already.
1.1131 +
1.1132 +\textit{prep\_specification:} translates the specification to an internal format
1.1133 +which allows efficient processing; see for instance line {\rm 07}
1.1134 +below.
1.1135 +\item[03..04] are a unique identifier for the specification within {\sisac}
1.1136 +and the ``mathematics author'' holding the copy-rights.
1.1137 +\item[05] is the Isabelle \textit{theory} required to parse the
1.1138 +specification in lines {\rm 07..10}.
1.1139 +\item[06] is a key into the tree of all specifications as presented to
1.1140 +the user (where some branches might be hidden by the dialogue
1.1141 +component).
1.1142 +\item[07..10] are the specification with input, pre-condition, output
1.1143 +and post-condition respectively; note that the specification contains
1.1144 +variables to be instantiated with concrete values for a concrete problem ---
1.1145 +thus the specification actually captures a class of problems. The post-condition is not handled in
1.1146 +the prototype presently.
1.1147 +\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
1.1148 +rewriting determined by rule-sets.
1.1149 +\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1.1150 +problem associated to a function from Computer Algebra (like an
1.1151 +equation solver) which is not the case here.
1.1152 +\item[13] is a list of methods solving the specified problem (here
1.1153 +only one list item) represented analogously to {\rm 06}.
1.1154 +\end{description}
1.1155 +
1.1156 +
1.1157 +%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
1.1158 +%WN ...
1.1159 +% type pbt =
1.1160 +% {guh : guh, (*unique within this isac-knowledge*)
1.1161 +% mathauthors: string list, (*copyright*)
1.1162 +% init : pblID, (*to start refinement with*)
1.1163 +% thy : theory, (* which allows to compile that pbt
1.1164 +% TODO: search generalized for subthy (ref.p.69*)
1.1165 +% (*^^^ WN050912 NOT used during application of the problem,
1.1166 +% because applied terms may be from 'subthy' as well as from super;
1.1167 +% thus we take 'maxthy'; see match_ags !*)
1.1168 +% cas : term option,(*'CAS-command'*)
1.1169 +% prls : rls, (* for preds in where_*)
1.1170 +% where_: term list, (* where - predicates*)
1.1171 +% ppc : pat list,
1.1172 +% (*this is the model-pattern;
1.1173 +% it contains "#Given","#Where","#Find","#Relate"-patterns
1.1174 +% for constraints on identifiers see "fun cpy_nam"*)
1.1175 +% met : metID list}; (* methods solving the pbt*)
1.1176 +%
1.1177 +%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
1.1178 +%WN oben selbst geschrieben.
1.1179 +
1.1180 +
1.1181 +
1.1182 +
1.1183 +%WN das w"urde ich in \sec\label{progr} verschieben und
1.1184 +%WN das SubProblem partial fractions zum Erkl"aren verwenden.
1.1185 +% Such a specification is checked before the execution of a program is
1.1186 +% started, the same applies for sub-programs. In the following example
1.1187 +% (Example~\ref{eg:subprob}) shows the call of such a subproblem:
1.1188 +%
1.1189 +% \vbox{
1.1190 +% \begin{example}
1.1191 +% \label{eg:subprob}
1.1192 +% \hfill \\
1.1193 +% {\ttfamily \begin{tabbing}
1.1194 +% ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
1.1195 +% ``\>\>[linear,univariate,equation,test],'' \\
1.1196 +% ``\>\>[Test,solve\_linear])'' \\
1.1197 +% ``\>[BOOL equ, REAL z])'' \\
1.1198 +% \end{tabbing}
1.1199 +% }
1.1200 +% {\small\textit{
1.1201 +% \noindent If a program requires a result which has to be
1.1202 +% calculated first we can use a subproblem to do so. In our specific
1.1203 +% case we wanted to calculate the zeros of a fraction and used a
1.1204 +% subproblem to calculate the zeros of the denominator polynom.
1.1205 +% }}
1.1206 +% \end{example}
1.1207 +% }
1.1208 +
1.1209 +\subsection{Implementation of the Method}\label{meth}
1.1210 +A method collects all data required to interpret a certain program by
1.1211 +Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
1.1212 +the running example is embedded on the last line in the following method:
1.1213 +%The methods represent the different ways a problem can be solved. This can
1.1214 +%include mathematical tactics as well as tactics taught in different courses.
1.1215 +%Declaring the Method itself gives us the possibilities to describe the way of
1.1216 +%calculation in deep, as well we get the oppertunities to build in different
1.1217 +%rulesets.
1.1218 +
1.1219 +{\footnotesize
1.1220 +\begin{verbatim}
1.1221 + 00 ML {*
1.1222 + 01 store_method
1.1223 + 02 (prep_method
1.1224 + 03 "SP_InverseZTransformation_classic"
1.1225 + 04 ["Jan Rocnik"]
1.1226 + 05 thy
1.1227 + 06 ( ["SignalProcessing", "Z_Transform", "Inverse"],
1.1228 + 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1.1229 + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1.1230 + 09 ("#Find" , ["stepResponse n_eq"]),
1.1231 + 10 rew_ord erls
1.1232 + 11 srls prls nrls
1.1233 + 12 errpats
1.1234 + 13 program);
1.1235 + 14 *}
1.1236 +\end{verbatim}}
1.1237 +
1.1238 +\noindent The above code stores the whole structure analogously to a
1.1239 +specification as described above:
1.1240 +\begin{description}
1.1241 +\item[01..06] are identical to those for the example specification on
1.1242 +p.\pageref{exp-spec}.
1.1243 +
1.1244 +\item[07..09] show something looking like the specification; this is a
1.1245 +{\em guard}: as long as not all \textit{Given} items are present and
1.1246 +the \textit{Pre}-conditions is not true, interpretation of the program
1.1247 +is not started.
1.1248 +
1.1249 +\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
1.1250 +\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
1.1251 +\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
1.1252 +\textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec}
1.1253 +and (c) is required for the derivation-machinery checking user-input formulas.
1.1254 +
1.1255 +\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}.
1.1256 +\end{description}
1.1257 +The many rule-sets above cause considerable efforts for the
1.1258 +programmers, in particular, because there are no tools for checking
1.1259 +essential features of rule-sets.
1.1260 +
1.1261 +% is again very technical and goes hard in detail. Unfortunataly
1.1262 +% most declerations are not essential for a basic programm but leads us to a huge
1.1263 +% range of powerful possibilities.
1.1264 +%
1.1265 +% \begin{description}
1.1266 +% \item[01..02] stores the method with the given name into the system under a global
1.1267 +% reference.
1.1268 +% \item[03] specifies the topic within which context the method can be found.
1.1269 +% \item[04..05] as the requirements for different methods can be deviant we
1.1270 +% declare what is \emph{given} and and what to \emph{find} for this specific method.
1.1271 +% The code again helds on the topic of the case studie, where the inverse
1.1272 +% z-transformation does a switch between a term describing a electrical filter into
1.1273 +% its step response. Also the datatype has to be declared (bool - due the fact that
1.1274 +% we handle equations).
1.1275 +% \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
1.1276 +% theorem of it is used for rewriting one single step.
1.1277 +% \item[07] \texttt{rls} is the currently used ruleset for this method. This set
1.1278 +% has already been defined before.
1.1279 +% \item[08] we would have the possiblitiy to add this method to a predefined tree of
1.1280 +% calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
1.1281 +% independend.
1.1282 +% \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
1.1283 +% the source.
1.1284 +% \item[10] \emph{predicates ruleset} can be used to indicates predicates within
1.1285 +% model patterns.
1.1286 +% \item[11] The \emph{check ruleset} summarizes rules for checking formulas
1.1287 +% elementwise.
1.1288 +% \item[12] \emph{error patterns} which are expected in this kind of method can be
1.1289 +% pre-specified to recognize them during the method.
1.1290 +% \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
1.1291 +% of the specific method.
1.1292 +% \item[14] for this code snipset we don't specify the programm itself and keep it
1.1293 +% empty. Follow up \S\ref{progr} for informations on how to implement this
1.1294 +% \textit{main} part.
1.1295 +% \end{description}
1.1296 +
1.1297 +\subsection{Implementation of the TP-based Program}\label{progr}
1.1298 +So finally all the prerequisites are described and the final task can
1.1299 +be addressed. The program below comes back to the running example: it
1.1300 +computes a solution for the problem from Fig.\ref{fig-interactive} on
1.1301 +p.\pageref{fig-interactive}. The reader is reminded of
1.1302 +\S\ref{PL-isab}, the introduction of the programming language:
1.1303 +
1.1304 +{\footnotesize\it\label{s:impl}
1.1305 +\begin{tabbing}
1.1306 +123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.1307 +\>{\rm 00}\>ML \{*\\
1.1308 +\>{\rm 00}\>val program =\\
1.1309 +\>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1.1310 +\>{\rm 02}\>\> {\tt let} \\
1.1311 +\>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1.1312 +\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
1.1313 +\>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1.1314 +\>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1.1315 +\>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1.1316 +\>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
1.1317 +%\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
1.1318 +\>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1.1319 +\>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1.1320 +\>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@ \\
1.1321 +\>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1.1322 +\>{\rm 13}\>\> {\tt in } \\
1.1323 +\>{\rm 14}\>\>\> X'\_eq"\\
1.1324 +\>{\rm 15}\>*\}
1.1325 +\end{tabbing}}
1.1326 +% ORIGINAL FROM Inverse_Z_Transform.thy
1.1327 +% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.1328 +% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.1329 +% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.1330 +% " (X'_z::real) = lhs X'; "^(* ?X' z*)
1.1331 +% " (zzz::real) = argument_in X'_z; "^(* z *)
1.1332 +% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.1333 +%
1.1334 +% " (pbz::real) = (SubProblem (Isac', "^(**)
1.1335 +% " [partial_fraction,rational,simplification], "^
1.1336 +% " [simplification,of_rationals,to_partial_fraction]) "^
1.1337 +% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.1338 +%
1.1339 +% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.1340 +% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.1341 +% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.1342 +% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.1343 +% " 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]*)
1.1344 +% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.1345 +% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.1346 +The program is represented as a string and part of the method in
1.1347 +\S\ref{meth}. As mentioned in \S\ref{PL} the program is purely
1.1348 +functional and lacks any input statements and output statements. So
1.1349 +the steps of calculation towards a solution (and interactive tutoring
1.1350 +in step-wise problem solving) are created as a side-effect by
1.1351 +Lucas-Interpretation. The side-effects are triggered by the tactics
1.1352 +\texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
1.1353 +\texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1.1354 +{\rm 12} respectively. These tactics produce the respective lines in the
1.1355 +calculation on p.\pageref{flow-impl}.
1.1356 +
1.1357 +The above lines {\rm 05, 06} do not contain a tactics, so they do not
1.1358 +immediately contribute to the calculation on p.\pageref{flow-impl};
1.1359 +rather, they compute actual arguments for the \texttt{SubProblem} in
1.1360 +line {\rm 09}~\footnote{The tactics also are break-points for the
1.1361 +interpreter, where control is handed over to the user in interactive
1.1362 +tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
1.1363 +
1.1364 +\medskip The above program also indicates the dominant role of interactive
1.1365 +selection of knowledge in the three-dimensional universe of
1.1366 +mathematics. The \texttt{SubProblem} in the above lines
1.1367 +{\rm 07..09} is more than a function call with the actual arguments
1.1368 +\textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
1.1369 +three items:
1.1370 +
1.1371 +\begin{enumerate}
1.1372 +\item the theory, in the example \textit{Isac} because different
1.1373 +methods can be selected in Pt.3 below, which are defined in different
1.1374 +theories with \textit{Isac} collecting them.
1.1375 +\item the specification identified by \textit{[partial\_fraction,
1.1376 +rational, simplification]} in the tree of specifications; this
1.1377 +specification is analogous to the specification of the main program
1.1378 +described in \S\ref{spec}; the problem is to find a ``partial fraction
1.1379 +decomposition'' for a univariate rational polynomial.
1.1380 +\item the method in the above example is \textit{[ ]}, i.e. empty,
1.1381 +which supposes the interpreter to select one of the methods predefined
1.1382 +in the specification, for instance in line {\rm 13} in the running
1.1383 +example's specification on p.\pageref{exp-spec}~\footnote{The freedom
1.1384 +(or obligation) for selection carries over to the student in
1.1385 +interactive tutoring.}.
1.1386 +\end{enumerate}
1.1387 +
1.1388 +The program code, above presented as a string, is parsed by Isabelle's
1.1389 +parser --- the program is an Isabelle term. This fact is expected to
1.1390 +simplify verification tasks in the future; on the other hand, this
1.1391 +fact causes troubles in error detection which are discussed as part
1.1392 +of the work-flow in the subsequent section.
1.1393 +
1.1394 +\section{Work-flow of Programming in the Prototype}\label{workflow}
1.1395 +The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
1.1396 +step forward for interactive theory and proof development. The
1.1397 +{\sisac}-prototype re-uses this IDE as a programming environment. The
1.1398 +experiences from this re-use show, that the essential components are
1.1399 +available from Isabelle/jEdit. However, additional tools and features
1.1400 +are required to achieve acceptable usability.
1.1401 +
1.1402 +So notable experiences are reported here, also as a requirement
1.1403 +capture for further development of TP-based languages and respective
1.1404 +IDEs.
1.1405 +
1.1406 +\subsection{Preparations and Trials}\label{flow-prep}
1.1407 +The many sub-tasks to be accomplished {\em before} the first line of
1.1408 +program code can be written and tested suggest an approach which
1.1409 +step-wise establishes the prerequisites. The case study underlying
1.1410 +this paper~\cite{jrocnik-bakk} documents the approach in a separate
1.1411 +Isabelle theory,
1.1412 +\textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
1.1413 +II in the study comprises this theory, \LaTeX ed from the theory by
1.1414 +use of Isabelle's document preparation system. This paper resembles
1.1415 +the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
1.1416 +implementation work involves several iterations.
1.1417 +
1.1418 +\bigskip For instance, only the last step, implementing the program
1.1419 +described in \S\ref{meth}, reveals details required. Let us assume,
1.1420 +this is the ML-function \textit{argument\_in} required in line {\rm 06}
1.1421 +of the example program on p.\pageref{s:impl}; how this function needs
1.1422 +to be implemented in the prototype has been discussed in \S\ref{funs}
1.1423 +already.
1.1424 +
1.1425 +Now let us assume, that calling this function from the program code
1.1426 +does not work; so testing this function is required in order to find out
1.1427 +the reason: type errors, a missing entry of the function somewhere or
1.1428 +even more nasty technicalities \dots
1.1429 +
1.1430 +{\footnotesize
1.1431 +\begin{verbatim}
1.1432 +01 ML {*
1.1433 +02 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1.1434 +03 val SOME (str, t') = eval_argument_in ""
1.1435 +04 "Build_Inverse_Z_Transform.argument'_in" t 0;
1.1436 +05 term2str t';
1.1437 +06 *}
1.1438 +07 val it = "(argument_in X z) = z": string\end{verbatim}}
1.1439 +
1.1440 +\noindent So, this works: we get an ad-hoc theorem, which used in
1.1441 +rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
1.1442 +reduction and create a rule-set \texttt{rls} for that purpose:
1.1443 +
1.1444 +{\footnotesize
1.1445 +\begin{verbatim}
1.1446 +01 ML {*
1.1447 +02 val rls = append_rls "test" e_rls
1.1448 +03 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1.1449 +04 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1.1450 +05 *}
1.1451 +06 val t' = Free ("z", "RealDef.real"): term
1.1452 +07 val asm = []: term list\end{verbatim}}
1.1453 +
1.1454 +\noindent The resulting term \texttt{t'} is \texttt{Free ("z",
1.1455 +"RealDef.real")}, i.e the variable \texttt{z}, so all is
1.1456 +perfect. Probably we have forgotten to store this function correctly~?
1.1457 +We review the respective \texttt{calclist} (again an
1.1458 +\textit{Unsynchronized.ref} to be removed in order to adjust to
1.1459 +Isabelle/Isar's asynchronous document model):
1.1460 +
1.1461 +{\footnotesize
1.1462 +\begin{verbatim}
1.1463 +01 calclist:= overwritel (! calclist,
1.1464 +02 [("argument_in",
1.1465 +03 ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1.1466 +04 ...
1.1467 +05 ]);\end{verbatim}}
1.1468 +
1.1469 +\noindent The entry is perfect. So what is the reason~? Ah, probably there
1.1470 +is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1.1471 +right, the function \texttt{argument\_in} is not contained in the respective
1.1472 +rule-set \textit{srls} \dots this just as an example of the intricacies in
1.1473 +debugging a program in the present state of the prototype.
1.1474 +
1.1475 +\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.1476 +Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
1.1477 +usually developed within several iterations, the program can be
1.1478 +assembled; on p.\pageref{s:impl} there is the complete program of the
1.1479 +running example.
1.1480 +
1.1481 +The completion of this program required efforts for several weeks
1.1482 +(after some months of familiarisation with {\sisac}), caused by the
1.1483 +abundance of intricacies indicated above. Also writing the program is
1.1484 +not pleasant, given Isabelle/Isar/ without add-ons for
1.1485 +programming. Already writing and parsing a few lines of program code
1.1486 +is a challenge: the program is an Isabelle term; Isabelle's parser,
1.1487 +however, is not meant for huge terms like the program of the running
1.1488 +example. So reading out the specific error (usually type errors) from
1.1489 +Isabelle's message is difficult.
1.1490 +
1.1491 +\medskip Testing the evaluation of the program has to rely on very
1.1492 +simple tools. Step-wise execution is modeled by a function
1.1493 +\texttt{me}, short for mathematics-engine~\footnote{The interface used
1.1494 +by the front-end which created the calculation on
1.1495 +p.\pageref{fig-interactive} is different from this function}:
1.1496 +%the following is a simplification of the actual function
1.1497 +
1.1498 +{\footnotesize
1.1499 +\begin{verbatim}
1.1500 +01 ML {* me; *}
1.1501 +02 val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}}
1.1502 +
1.1503 +\noindent This function takes as arguments a tactic \texttt{tac} which
1.1504 +determines the next step, the step applied to the interpreter-state
1.1505 +\texttt{ctree * pos} as last argument taken. The interpreter-state is
1.1506 +a pair of a tree \texttt{ctree} representing the calculation created
1.1507 +(see the example below) and a position \texttt{pos} in the
1.1508 +calculation. The function delivers a quadruple, beginning with the new
1.1509 +formula \texttt{mout} and the next tactic followed by the new
1.1510 +interpreter-state.
1.1511 +
1.1512 +This function allows to stepwise check the program:
1.1513 +
1.1514 +{\footnotesize\label{ml-check-program}
1.1515 +\begin{verbatim}
1.1516 +01 ML {*
1.1517 +02 val fmz =
1.1518 +03 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1.1519 +04 "stepResponse (x[n::real]::bool)"];
1.1520 +05 val (dI,pI,mI) =
1.1521 +06 ("Isac",
1.1522 +07 ["Inverse", "Z_Transform", "SignalProcessing"],
1.1523 +08 ["SignalProcessing","Z_Transform","Inverse"]);
1.1524 +09 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1.1525 +10 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.1526 +11 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.1527 +12 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.1528 +13 ...
1.1529 +\end{verbatim}}
1.1530 +
1.1531 +\noindent Several dozens of calls for \texttt{me} are required to
1.1532 +create the lines in the calculation below (including the sub-problems
1.1533 +not shown). When an error occurs, the reason might be located
1.1534 +many steps before: if evaluation by rewriting, as done by the prototype,
1.1535 +fails, then first nothing happens --- the effects come later and
1.1536 +cause unpleasant checks.
1.1537 +
1.1538 +The checks comprise watching the rewrite-engine for many different
1.1539 +kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
1.1540 +particular the environment and the context at the states position ---
1.1541 +all checks have to rely on simple functions accessing the
1.1542 +\texttt{ctree}. So getting the calculation below (which resembles the
1.1543 +calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
1.1544 +is the result of several weeks of development:
1.1545 +
1.1546 +{\small\it\label{exp-calc}
1.1547 +\begin{tabbing}
1.1548 +123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1.1549 +\>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1.1550 +\>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
1.1551 +\>{\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}\\
1.1552 +\>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
1.1553 +\>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
1.1554 +\>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
1.1555 +\>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
1.1556 +\>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
1.1557 +\>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
1.1558 +\>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
1.1559 +\> \>\>\>\> \_\_\_ \`- - -\\
1.1560 +\>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1.1561 +\>{\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)}\\
1.1562 +\>{\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 }\\
1.1563 +\>{\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}\\
1.1564 +\>{\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}}
1.1565 +\end{tabbing}}
1.1566 +The tactics on the right margin of the above calculation are those in
1.1567 +the program on p.\pageref{s:impl} which create the respective formulas
1.1568 +on the left.
1.1569 +% ORIGINAL FROM Inverse_Z_Transform.thy
1.1570 +% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.1571 +% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.1572 +% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.1573 +% " (X'_z::real) = lhs X'; "^(* ?X' z*)
1.1574 +% " (zzz::real) = argument_in X'_z; "^(* z *)
1.1575 +% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.1576 +%
1.1577 +% " (pbz::real) = (SubProblem (Isac', "^(**)
1.1578 +% " [partial_fraction,rational,simplification], "^
1.1579 +% " [simplification,of_rationals,to_partial_fraction]) "^
1.1580 +% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.1581 +%
1.1582 +% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.1583 +% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.1584 +% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.1585 +% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.1586 +% " 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]*)
1.1587 +% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.1588 +% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.1589 +
1.1590 +\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1.1591 +Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
1.1592 +and the knowledge accumulated in it can be distributed to appropriate
1.1593 +theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
1.1594 +sub-problem accomplishing the partial fraction decomposition to
1.1595 +\textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
1.1596 +internals, this kind of distribution is not trivial. For instance, the
1.1597 +function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
1.1598 +string with the theory it has been defined in, so this string needs to
1.1599 +be updated from \texttt{Build\_Inverse\_Z\_Transform} to
1.1600 +\texttt{Atools} if that function is transferred to theory
1.1601 +\textit{Atools.thy}.
1.1602 +
1.1603 +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.
1.1604 +This process is also rather bare-bones without authoring tools and is
1.1605 +described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
1.1606 +
1.1607 +% \newpage
1.1608 +% -------------------------------------------------------------------
1.1609 +%
1.1610 +% Material, falls noch Platz bleibt ...
1.1611 +%
1.1612 +% -------------------------------------------------------------------
1.1613 +%
1.1614 +%
1.1615 +% \subsubsection{Trials on Notation and Termination}
1.1616 +%
1.1617 +% \paragraph{Technical notations} are a big problem for our piece of software,
1.1618 +% but the reason for that isn't a fault of the software itself, one of the
1.1619 +% troubles comes out of the fact that different technical subtopics use different
1.1620 +% symbols and notations for a different purpose. The most famous example for such
1.1621 +% a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
1.1622 +% math). In the specific part of signal processing one of this notation issues is
1.1623 +% the use of brackets --- we use round brackets for analoge signals and squared
1.1624 +% brackets for digital samples. Also if there is no problem for us to handle this
1.1625 +% fact, we have to tell the machine what notation leads to wich meaning and that
1.1626 +% this purpose seperation is only valid for this special topic - signal
1.1627 +% processing.
1.1628 +% \subparagraph{In the programming language} itself it is not possible to declare
1.1629 +% fractions, exponents, absolutes and other operators or remarks in a way to make
1.1630 +% them pretty to read; our only posssiblilty were ASCII characters and a handfull
1.1631 +% greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
1.1632 +% \par
1.1633 +% With the upper collected knowledge it is possible to check if we were able to
1.1634 +% donate all required terms and expressions.
1.1635 +%
1.1636 +% \subsubsection{Definition and Usage of Rules}
1.1637 +%
1.1638 +% \paragraph{The core} of our implemented problem is the Z-Transformation, due
1.1639 +% the fact that the transformation itself would require higher math which isn't
1.1640 +% yet avaible in our system we decided to choose the way like it is applied in
1.1641 +% labratory and problem classes at our university - by applying transformation
1.1642 +% rules (collected in transformation tables).
1.1643 +% \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1.1644 +% use of axiomatizations like shown in Example~\ref{eg:ruledef}
1.1645 +%
1.1646 +% \begin{example}
1.1647 +% \label{eg:ruledef}
1.1648 +% \hfill\\
1.1649 +% \begin{verbatim}
1.1650 +% axiomatization where
1.1651 +% rule1: ``1 = $\delta$[n]'' and
1.1652 +% rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1.1653 +% rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1.1654 +% \end{verbatim}
1.1655 +% \end{example}
1.1656 +%
1.1657 +% This rules can be collected in a ruleset and applied to a given expression as
1.1658 +% follows in Example~\ref{eg:ruleapp}.
1.1659 +%
1.1660 +% \begin{example}
1.1661 +% \hfill\\
1.1662 +% \label{eg:ruleapp}
1.1663 +% \begin{enumerate}
1.1664 +% \item Store rules in ruleset:
1.1665 +% \begin{verbatim}
1.1666 +% val inverse_Z = append_rls "inverse_Z" e_rls
1.1667 +% [ Thm ("rule1",num_str @{thm rule1}),
1.1668 +% Thm ("rule2",num_str @{thm rule2}),
1.1669 +% Thm ("rule3",num_str @{thm rule3})
1.1670 +% ];\end{verbatim}
1.1671 +% \item Define exression:
1.1672 +% \begin{verbatim}
1.1673 +% val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1.1674 +% \item Apply ruleset:
1.1675 +% \begin{verbatim}
1.1676 +% val SOME (sample_term', asm) =
1.1677 +% rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1.1678 +% \end{enumerate}
1.1679 +% \end{example}
1.1680 +%
1.1681 +% The use of rulesets makes it much easier to develop our designated applications,
1.1682 +% but the programmer has to be careful and patient. When applying rulesets
1.1683 +% two important issues have to be mentionend:
1.1684 +% \subparagraph{How often} the rules have to be applied? In case of
1.1685 +% transformations it is quite clear that we use them once but other fields
1.1686 +% reuqire to apply rules until a special condition is reached (e.g.
1.1687 +% a simplification is finished when there is nothing to be done left).
1.1688 +% \subparagraph{The order} in which rules are applied often takes a big effect
1.1689 +% and has to be evaluated for each purpose once again.
1.1690 +% \par
1.1691 +% In our special case of Signal Processing and the rules defined in
1.1692 +% Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1.1693 +% constants. After this step has been done it no mather which rule fit's next.
1.1694 +%
1.1695 +% \subsubsection{Helping Functions}
1.1696 +%
1.1697 +% \paragraph{New Programms require,} often new ways to get through. This new ways
1.1698 +% means that we handle functions that have not been in use yet, they can be
1.1699 +% something special and unique for a programm or something famous but unneeded in
1.1700 +% the system yet. In our dedicated example it was for example neccessary to split
1.1701 +% a fraction into numerator and denominator; the creation of such function and
1.1702 +% even others is described in upper Sections~\ref{simp} and \ref{funs}.
1.1703 +%
1.1704 +% \subsubsection{Trials on equation solving}
1.1705 +% %simple eq and problem with double fractions/negative exponents
1.1706 +% \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
1.1707 +% equations degree one and two. Solving equations in the first degree is no
1.1708 +% problem, wether for a student nor for our machine; but even second degree
1.1709 +% equations can lead to big troubles. The origin of this troubles leads from
1.1710 +% the build up process of our equation solving functions; they have been
1.1711 +% implemented some time ago and of course they are not as good as we want them to
1.1712 +% be. Wether or not following we only want to show how cruel it is to build up new
1.1713 +% work on not well fundamentials.
1.1714 +% \subparagraph{A simple equation solving,} can be set up as shown in the next
1.1715 +% example:
1.1716 +%
1.1717 +% \begin{example}
1.1718 +% \begin{verbatim}
1.1719 +%
1.1720 +% val fmz =
1.1721 +% ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
1.1722 +% "solveFor z",
1.1723 +% "solutions L"];
1.1724 +%
1.1725 +% val (dI',pI',mI') =
1.1726 +% ("Isac",
1.1727 +% ["abcFormula","degree_2","polynomial","univariate","equation"],
1.1728 +% ["no_met"]);\end{verbatim}
1.1729 +% \end{example}
1.1730 +%
1.1731 +% Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
1.1732 +% a short overview on the commands; at first we set up the equation and tell the
1.1733 +% machine what's the bound variable and where to store the solution. Second step
1.1734 +% is to define the equation type and determine if we want to use a special method
1.1735 +% to solve this type.) Simple checks tell us that the we will get two results for
1.1736 +% this equation and this results will be real.
1.1737 +% So far it is easy for us and for our machine to solve, but
1.1738 +% mentioned that a unvariate equation second order can have three different types
1.1739 +% of solutions it is getting worth.
1.1740 +% \subparagraph{The solving of} all this types of solutions is not yet supported.
1.1741 +% Luckily it was needed for us; but something which has been needed in this
1.1742 +% context, would have been the solving of an euation looking like:
1.1743 +% $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
1.1744 +% before (remember that befor it was no problem to handle for the machine) but
1.1745 +% now, after a simple equivalent transformation, we are not able to solve
1.1746 +% it anymore.
1.1747 +% \subparagraph{Error messages} we get when we try to solve something like upside
1.1748 +% were very confusing and also leads us to no special hint about a problem.
1.1749 +% \par The fault behind is, that we have no well error handling on one side and
1.1750 +% no sufficient formed equation solving on the other side. This two facts are
1.1751 +% making the implemention of new material very difficult.
1.1752 +%
1.1753 +% \subsection{Formalization of missing knowledge in Isabelle}
1.1754 +%
1.1755 +% \paragraph{A problem} behind is the mechanization of mathematic
1.1756 +% theories in TP-bases languages. There is still a huge gap between
1.1757 +% these algorithms and this what we want as a solution - in Example
1.1758 +% Signal Processing.
1.1759 +%
1.1760 +% \vbox{
1.1761 +% \begin{example}
1.1762 +% \label{eg:gap}
1.1763 +% \[
1.1764 +% X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1.1765 +% \]
1.1766 +% {\small\textit{
1.1767 +% \noindent A very simple example on this what we call gap is the
1.1768 +% simplification above. It is needles to say that it is correct and also
1.1769 +% Isabelle for fills it correct - \emph{always}. But sometimes we don't
1.1770 +% want expand such terms, sometimes we want another structure of
1.1771 +% them. Think of a problem were we now would need only the coefficients
1.1772 +% of $X$ and $Y$. This is what we call the gap between mechanical
1.1773 +% simplification and the solution.
1.1774 +% }}
1.1775 +% \end{example}
1.1776 +% }
1.1777 +%
1.1778 +% \paragraph{We are not able to fill this gap,} until we have to live
1.1779 +% with it but first have a look on the meaning of this statement:
1.1780 +% Mechanized math starts from mathematical models and \emph{hopefully}
1.1781 +% proceeds to match physics. Academic engineering starts from physics
1.1782 +% (experimentation, measurement) and then proceeds to mathematical
1.1783 +% modeling and formalization. The process from a physical observance to
1.1784 +% a mathematical theory is unavoidable bound of setting up a big
1.1785 +% collection of standards, rules, definition but also exceptions. These
1.1786 +% are the things making mechanization that difficult.
1.1787 +%
1.1788 +% \vbox{
1.1789 +% \begin{example}
1.1790 +% \label{eg:units}
1.1791 +% \[
1.1792 +% m,\ kg,\ s,\ldots
1.1793 +% \]
1.1794 +% {\small\textit{
1.1795 +% \noindent Think about some units like that one's above. Behind
1.1796 +% each unit there is a discerning and very accurate definition: One
1.1797 +% Meter is the distance the light travels, in a vacuum, through the time
1.1798 +% of 1 / 299.792.458 second; one kilogram is the weight of a
1.1799 +% platinum-iridium cylinder in paris; and so on. But are these
1.1800 +% definitions usable in a computer mechanized world?!
1.1801 +% }}
1.1802 +% \end{example}
1.1803 +% }
1.1804 +%
1.1805 +% \paragraph{A computer} or a TP-System builds on programs with
1.1806 +% predefined logical rules and does not know any mathematical trick
1.1807 +% (follow up example \ref{eg:trick}) or recipe to walk around difficult
1.1808 +% expressions.
1.1809 +%
1.1810 +% \vbox{
1.1811 +% \begin{example}
1.1812 +% \label{eg:trick}
1.1813 +% \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1.1814 +% \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1.1815 +% \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1.1816 +% \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1.1817 +% {\small\textit{
1.1818 +% \noindent Sometimes it is also useful to be able to apply some
1.1819 +% \emph{tricks} to get a beautiful and particularly meaningful result,
1.1820 +% which we are able to interpret. But as seen in this example it can be
1.1821 +% hard to find out what operations have to be done to transform a result
1.1822 +% into a meaningful one.
1.1823 +% }}
1.1824 +% \end{example}
1.1825 +% }
1.1826 +%
1.1827 +% \paragraph{The only possibility,} for such a system, is to work
1.1828 +% through its known definitions and stops if none of these
1.1829 +% fits. Specified on Signal Processing or any other application it is
1.1830 +% often possible to walk through by doing simple creases. This creases
1.1831 +% are in general based on simple math operational but the challenge is
1.1832 +% to teach the machine \emph{all}\footnote{Its pride to call it
1.1833 +% \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
1.1834 +% reach a high level of \emph{all} but it in real it will still be a
1.1835 +% survey of knowledge which links to other knowledge and {{\sisac}{}} a
1.1836 +% trainer and helper but no human compensating calculator.
1.1837 +% \par
1.1838 +% {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
1.1839 +% specifications of problems out of topics from Signal Processing, etc.)
1.1840 +% and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
1.1841 +% physical knowledge. The result is a three-dimensional universe of
1.1842 +% mathematics seen in Figure~\ref{fig:mathuni}.
1.1843 +%
1.1844 +% \begin{figure}
1.1845 +% \begin{center}
1.1846 +% \includegraphics{fig/universe}
1.1847 +% \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
1.1848 +% combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
1.1849 +% leads to a three dimensional math universe.\label{fig:mathuni}}
1.1850 +% \end{center}
1.1851 +% \end{figure}
1.1852 +%
1.1853 +% %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
1.1854 +% %WN bitte folgende Bezeichnungen nehmen:
1.1855 +% %WN
1.1856 +% %WN axis 1: Algorithmic Knowledge (Programs)
1.1857 +% %WN axis 2: Application-oriented Knowledge (Specifications)
1.1858 +% %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
1.1859 +% %WN
1.1860 +% %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
1.1861 +% %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
1.1862 +% %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
1.1863 +%
1.1864 +% %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
1.1865 +% %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
1.1866 +% %JR gefordert werden WN2...
1.1867 +% %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
1.1868 +% %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
1.1869 +% %WN2 zusammenschneiden um die R"ander weg zu bekommen)
1.1870 +% %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
1.1871 +% %WN2 png + pdf figures mitzuschicken.
1.1872 +%
1.1873 +% \subsection{Notes on Problems with Traditional Notation}
1.1874 +%
1.1875 +% \paragraph{During research} on these topic severely problems on
1.1876 +% traditional notations have been discovered. Some of them have been
1.1877 +% known in computer science for many years now and are still unsolved,
1.1878 +% one of them aggregates with the so called \emph{Lambda Calculus},
1.1879 +% Example~\ref{eg:lamda} provides a look on the problem that embarrassed
1.1880 +% us.
1.1881 +%
1.1882 +% \vbox{
1.1883 +% \begin{example}
1.1884 +% \label{eg:lamda}
1.1885 +%
1.1886 +% \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1.1887 +%
1.1888 +%
1.1889 +% \[ f(p)=\ldots\; p \in \quad R \]
1.1890 +%
1.1891 +% {\small\textit{
1.1892 +% \noindent Above we see two equations. The first equation aims to
1.1893 +% be a mapping of an function from the reel range to the reel one, but
1.1894 +% when we change only one letter we get the second equation which
1.1895 +% usually aims to insert a reel point $p$ into the reel function. In
1.1896 +% computer science now we have the problem to tell the machine (TP) the
1.1897 +% difference between this two notations. This Problem is called
1.1898 +% \emph{Lambda Calculus}.
1.1899 +% }}
1.1900 +% \end{example}
1.1901 +% }
1.1902 +%
1.1903 +% \paragraph{An other problem} is that terms are not full simplified in
1.1904 +% traditional notations, in {{\sisac}} we have to simplify them complete
1.1905 +% to check weather results are compatible or not. in e.g. the solutions
1.1906 +% of an second order linear equation is an rational in {{\sisac}} but in
1.1907 +% tradition we keep fractions as long as possible and as long as they
1.1908 +% aim to be \textit{beautiful} (1/8, 5/16,...).
1.1909 +% \subparagraph{The math} which should be mechanized in Computer Theorem
1.1910 +% Provers (\emph{TP}) has (almost) a problem with traditional notations
1.1911 +% (predicate calculus) for axioms, definitions, lemmas, theorems as a
1.1912 +% computer program or script is not able to interpret every Greek or
1.1913 +% Latin letter and every Greek, Latin or whatever calculations
1.1914 +% symbol. Also if we would be able to handle these symbols we still have
1.1915 +% a problem to interpret them at all. (Follow up \hbox{Example
1.1916 +% \ref{eg:symbint1}})
1.1917 +%
1.1918 +% \vbox{
1.1919 +% \begin{example}
1.1920 +% \label{eg:symbint1}
1.1921 +% \[
1.1922 +% u\left[n\right] \ \ldots \ unitstep
1.1923 +% \]
1.1924 +% {\small\textit{
1.1925 +% \noindent The unitstep is something we need to solve Signal
1.1926 +% Processing problem classes. But in {{{\sisac}{}}} the rectangular
1.1927 +% brackets have a different meaning. So we abuse them for our
1.1928 +% requirements. We get something which is not defined, but usable. The
1.1929 +% Result is syntax only without semantic.
1.1930 +% }}
1.1931 +% \end{example}
1.1932 +% }
1.1933 +%
1.1934 +% In different problems, symbols and letters have different meanings and
1.1935 +% ask for different ways to get through. (Follow up \hbox{Example
1.1936 +% \ref{eg:symbint2}})
1.1937 +%
1.1938 +% \vbox{
1.1939 +% \begin{example}
1.1940 +% \label{eg:symbint2}
1.1941 +% \[
1.1942 +% \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
1.1943 +% \]
1.1944 +% {\small\textit{
1.1945 +% \noindent For using exponents the three \texttt{widehat} symbols
1.1946 +% are required. The reason for that is due the development of
1.1947 +% {{{\sisac}{}}} the single \texttt{widehat} and also the double were
1.1948 +% already in use for different operations.
1.1949 +% }}
1.1950 +% \end{example}
1.1951 +% }
1.1952 +%
1.1953 +% \paragraph{Also the output} can be a problem. We are familiar with a
1.1954 +% specified notations and style taught in university but a computer
1.1955 +% program has no knowledge of the form proved by a professor and the
1.1956 +% machines themselves also have not yet the possibilities to print every
1.1957 +% symbol (correct) Recent developments provide proofs in a human
1.1958 +% readable format but according to the fact that there is no money for
1.1959 +% good working formal editors yet, the style is one thing we have to
1.1960 +% live with.
1.1961 +%
1.1962 +% \section{Problems rising out of the Development Environment}
1.1963 +%
1.1964 +% fehlermeldungen! TODO
1.1965 +
1.1966 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
1.1967 +
1.1968 +\section{Summary and Conclusions}\label{conclusion}
1.1969 +
1.1970 +%JR obvious
1.1971 +
1.1972 +%This paper gives a first experience report about programming with a
1.1973 +%TP-based programming language.
1.1974 +
1.1975 +A brief re-introduction of the novel kind of programming
1.1976 +language by example of the {\sisac}-prototype makes the paper
1.1977 +self-contained. The main section describes all the main concepts
1.1978 +involved in TP-based programming and all the sub-tasks concerning
1.1979 +respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain
1.1980 +modeling, implementation of term rewriting systems for the
1.1981 +rewriting-engine, formal (implicit) specification of the problem to be
1.1982 +(explicitly) described by the program, implementation of the many components
1.1983 +required for Lucas-Interpretation and finally implementation of the
1.1984 +program itself.
1.1985 +
1.1986 +The many concepts and sub-tasks involved in programming require a
1.1987 +comprehensive work-flow; first experiences with the work-flow as
1.1988 +supported by the present prototype are described as well: Isabelle +
1.1989 +Isar + jEdit provide appropriate components for establishing an
1.1990 +efficient development environment integrating computation and
1.1991 +deduction. However, the present state of the prototype is far off a
1.1992 +state appropriate for wide-spread use: the prototype of the program
1.1993 +language lacks expressiveness and elegance, the prototype of the
1.1994 +development environment is hardly usable: error messages still address
1.1995 +the developer of the prototype's interpreter rather than the
1.1996 +application programmer, implementation of the many settings for the
1.1997 +Lucas-Interpreter is cumbersome.
1.1998 +
1.1999 +\subsection{Conclusions for Future Development}
1.2000 +From the above mentioned experiences a successful proof of concept can be concluded:
1.2001 +programming arbitrary problems from engineering sciences is possible,
1.2002 +in principle even in the prototype. Furthermore the experiences allow
1.2003 +to conclude detailed requirements for further development:
1.2004 +\begin{enumerate}
1.2005 +\item Clarify underlying logics such that programming is smoothly
1.2006 +integrated with verification of the program; the post-condition should
1.2007 +be proved more or less automatically, otherwise working engineers
1.2008 +would not encounter such programming.
1.2009 +\item Combine the prototype's programming language with Isabelle's
1.2010 +powerful function package and probably with more of SML's
1.2011 +pattern-matching features; include parallel execution on multi-core
1.2012 +machines into the language design.
1.2013 +\item Extend the prototype's Lucas-Interpreter such that it also
1.2014 +handles functions defined by use of Isabelle's functions package; and
1.2015 +generalize Isabelle's code generator such that efficient code for the
1.2016 +whole definition of the programming language can be generated (for
1.2017 +multi-core machines).
1.2018 +\item Develop an efficient development environment with
1.2019 +integration of programming and proving, with management not only of
1.2020 +Isabelle theories, but also of large collections of specifications and
1.2021 +of programs.
1.2022 +\item\label{CAS} Extend Isabelle's computational features in direction of
1.2023 +\textit{verfied} Computer Algebra: simplification extended by
1.2024 +algorithms beyond rewriting (cancellation of multivariate rationals,
1.2025 +factorisation, partial fraction decomposition, etc), equation solving
1.2026 +, integration, etc.
1.2027 +\end{enumerate}
1.2028 +Provided successful accomplishment, these points provide distinguished
1.2029 +components for virtual workbenches appealing to practitioners of
1.2030 +engineering in the near future.
1.2031 +
1.2032 +\subsection{Preview to Development of Course Material}
1.2033 +Interactive course material, as addressed by the title,
1.2034 +can comprise step-wise problem solving created as a side-effect of a
1.2035 +TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an
1.2036 +interactive programming environment, Lucas-Interpretation also can
1.2037 +provide TP-based services for a flexible dialogue component with
1.2038 +adaptive user guidance for independent and inquiry-based learning.
1.2039 +
1.2040 +However, the {\sisac} prototype is not ready for use in field-tests,
1.2041 +not only due to the above five requirements not sufficiently
1.2042 +accomplished, but also due to usability of the fron-end, in particular
1.2043 +the lack of an editor for formulas in 2-dimension representation.
1.2044 +
1.2045 +Nevertheless, the experiences from the case study described in this
1.2046 +paper, allow to give a preview to the development of course material,
1.2047 +if based on Lucas-Interpretation:
1.2048 +
1.2049 +\paragraph{Development of material from scratch} is too much effort
1.2050 +just for e-learning; this has become clear with the case study. For
1.2051 +getting support for stepwise problem solving just in {\em one} example
1.2052 +class, the one presented in this paper, involved the following tasks:
1.2053 +\begin{itemize}
1.2054 +\item Adapt the equation solver; since that was too laborous, the
1.2055 +program has been adapted in an unelegant way.
1.2056 +\item Implement an algorithms for partial fraction decomposition,
1.2057 +which is considered a standard normal form in Computer Algebra.
1.2058 +\item Implement a specification for partial fraction decomposition and
1.2059 +locate it appropriately in the hierarchy of specification.
1.2060 +\item Declare definitions and theorems within the theory of
1.2061 +${\cal Z}$-transform, and prove the theorems (which was not done in the
1.2062 +case study).
1.2063 +\end{itemize}
1.2064 +On the other hand, for the one the class of problems implemented,
1.2065 +adding an arbitrary number of examples within this class requires a
1.2066 +few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an
1.2067 +example is called from an HTML-file by an URL, which addresses an
1.2068 +XML-structure holding the respective data as shown on
1.2069 +p.\pageref{ml-check-program}.} and the support for individual stepwise
1.2070 +problem solving comes for free.
1.2071 +
1.2072 +\paragraph{E-learning benefits from Formal Domain Engineering} which can be
1.2073 +expected for various domains in the near future. In order to cope with
1.2074 +increasing complexity in domain of technology, specific domain
1.2075 +knowledge is beeing mechanised, not only for software technology
1.2076 +\footnote{For instance, the Archive of Formal Proofs
1.2077 +http://afp.sourceforge.net/} but also for other engineering domains
1.2078 +\cite{Dehbonei&94,Hansen94b,db:dom-eng}. This fairly new part of
1.2079 +engineering sciences is called ``domain engineering'' in
1.2080 +\cite{db:SW-engIII}.
1.2081 +
1.2082 +Given this kind of mechanised knowledge including mathematical
1.2083 +theories, domain specific definitions, specifications and algorithms,
1.2084 +theorems and proofs, then e-learning with support for individual
1.2085 +stepwise problem solving will not be much ado anymore; then e-learning
1.2086 +media in technology education can be derived from this knowledge with
1.2087 +reasonable effort.
1.2088 +
1.2089 +\paragraph{Development differentiates into tasks} more separated than
1.2090 +without Lucas-Interpretation and more challenginging in specific
1.2091 +expertise. These are the kinds of experts expected to cooperate in
1.2092 +development of
1.2093 +\begin{itemize}
1.2094 +\item ``Domain engineers'', who accomplish fairly novel tasks
1.2095 +described in this paper.
1.2096 +\item Course designers, who provide the instructional design according
1.2097 +to curricula, together with usability experts and media designers, are
1.2098 +indispensable in production of e-learning media at the state-of-the
1.2099 +art.
1.2100 +\item ``Dialog designers'', whose part of development is clearly
1.2101 +separated from the part of domain engineers as a consequence of
1.2102 +Lucas-Interpretation: TP-based programs are functional, as mentioned,
1.2103 +and are only concerned with describing mathematics --- and not at all
1.2104 +concerned with interaction, psychology, learning theory and the like,
1.2105 +because there are no in/output statements. Dialog designers can expect
1.2106 +a high-level rule-based language~\cite{gdaroczy-EP-13} for describing
1.2107 +their part.
1.2108 +\end{itemize}
1.2109 +
1.2110 +% response-to-referees:
1.2111 +% (2.1) details of novel technology in order to estimate the impact
1.2112 +% (2.2) which kinds of expertise are required for production of e-learning media (instructional design, math authoring, dialog authoring, media design)
1.2113 +% (2.3) what in particular is required for programming new exercises supported by next-step-guidance (expertise / efforts)
1.2114 +% (2.4) estimation of break-even points for development of next-step-guidance
1.2115 +% (2.5) usability of ISAC prototype at the present state
1.2116 +%
1.2117 +% The points (1.*) seem to be well covered in the paper, the points (2.*) are not. So I decided to address the points (2.*) in a separate section §5.1."".
1.2118 +
1.2119 +\bigskip\noindent For this decade there seems to be a window of opportunity opening from
1.2120 +one side inreasing demand for formal domain engineering and from the
1.2121 +other side from TP more and more gaining industrial relevance. Within
1.2122 +this window, development of TP-based educational software can take
1.2123 +benefit from the fact, that the TPs leading in Europe, Coq~\cite{coq-team-10} and
1.2124 +Isabelle are still open source together with the major part of
1.2125 +mechanised knowledge.%~\footnote{NICTA}.
1.2126 +
1.2127 +\bibliographystyle{alpha}
1.2128 +{\small\bibliography{references}}
1.2129 +
1.2130 +\end{document}
1.2131 +% LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
1.2132 +% LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised
1.2133 +% LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
1.2134 +% LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
1.2135 +% LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
1.2136 +% LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq
1.2137 +% LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
1.2138 +% LocalWords: mechanisation multi