diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 17 09:50:52 2013 +0200 @@ -0,0 +1,2135 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Electronic Journal of Mathematics and Technology (eJMT) % +% style sheet for LaTeX. Please do not modify sections % +% or commands marked 'eJMT'. % +% % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% eJMT commands % +% % +\documentclass[12pt,a4paper]{article}% % +\usepackage{times} % +\usepackage{amsfonts,amsmath,amssymb} % +\usepackage[a4paper]{geometry} % +\usepackage{fancyhdr} % +\usepackage{color} % +\usepackage[pdftex]{hyperref} % see note below % +\usepackage{graphicx}% % +\hypersetup{ % + a4paper, % + breaklinks % +} % +% % +\newtheorem{theorem}{Theorem} % +\newtheorem{acknowledgement}[theorem]{Acknowledgement} % +\newtheorem{algorithm}[theorem]{Algorithm} % +\newtheorem{axiom}[theorem]{Axiom} % +\newtheorem{case}[theorem]{Case} % +\newtheorem{claim}[theorem]{Claim} % +\newtheorem{conclusion}[theorem]{Conclusion} % +\newtheorem{condition}[theorem]{Condition} % +\newtheorem{conjecture}[theorem]{Conjecture} % +\newtheorem{corollary}[theorem]{Corollary} % +\newtheorem{criterion}[theorem]{Criterion} % +\newtheorem{definition}[theorem]{Definition} % +\newtheorem{example}[theorem]{Example} % +\newtheorem{exercise}[theorem]{Exercise} % +\newtheorem{lemma}[theorem]{Lemma} % +\newtheorem{notation}[theorem]{Notation} % +\newtheorem{problem}[theorem]{Problem} % +\newtheorem{proposition}[theorem]{Proposition} % +\newtheorem{remark}[theorem]{Remark} % +\newtheorem{solution}[theorem]{Solution} % +\newtheorem{summary}[theorem]{Summary} % +\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } % +{\ \rule{0.5em}{0.5em}} % +% % +% eJMT page dimensions % +% % +\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} % +% % +% eJMT header & footer % +% % +\newcounter{ejmtFirstpage} % +\setcounter{ejmtFirstpage}{1} % +\pagestyle{empty} % +\setlength{\headheight}{14pt} % +\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} % +\pagestyle{fancyplain} % +\fancyhf{} % +\fancyhead[c]{\small The Electronic Journal of Mathematics% +\ and Technology, Volume 1, Number 1, ISSN 1933-2823} % +\cfoot{% % + \ifnum\value{ejmtFirstpage}=0% % + {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% % + \else\setcounter{ejmtFirstpage}{0}\fi% % +} % +% % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Please place your own definitions here +% +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} +\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} + +\usepackage{color} +\definecolor{lgray}{RGB}{238,238,238} + +\usepackage{hyperref} + +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% How to use hyperref % +% ------------------- % +% % +% Probably the only way you will need to use the hyperref % +% package is as follows. To make some text, say % +% "My Text Link", into a link to the URL % +% http://something.somewhere.com/mystuff, use % +% % +% \href{http://something.somewhere.com/mystuff}{My Text Link} +% % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +\begin{document} +% +% document title +% +\title{Trials with TP-based Programming +\\ +for Interactive Course Material}% +% +% Single author. Please supply at least your name, +% email address, and affiliation here. +% +\author{\begin{tabular}{c} +\textit{Jan Ro\v{c}nik} \\ +jan.rocnik@student.tugraz.at \\ +IST, SPSC\\ +Graz University of Technology\\ +Austria\end{tabular} +}% +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% eJMT commands - do not change these % +% % +\date{} % +\maketitle % +% % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% abstract +% +\begin{abstract} + +Traditional course material in engineering disciplines lacks an +important component, interactive support for step-wise problem +solving. Theorem-Proving (TP) technology is appropriate for one part +of such support, in checking user-input. For the other part of such +support, guiding the learner towards a solution, another kind of +technology is required. + +Both kinds of support can be achieved by so-called +Lucas-Interpretation which combines deduction and computation and, for +the latter, uses a novel kind of programming language. This language +is based on (Computer) Theorem Proving (TP), thus called a ``TP-based +programming language''. + +This paper is the experience report of the first ``application +programmer'' using this language for creating exercises in step-wise +problem solving for an advanced lab in Signal Processing. The tasks +involved in TP-based programming are described together with the +experience gained from a prototype of the programming language and of +it's interpreter. + +The report concludes with a positive proof of concept, states +insufficiency usability of the prototype and captures the requirements +for further development of both, the programming language and the +interpreter. +% +\end{abstract}% +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% eJMT command % +% % +\thispagestyle{fancy} % +% % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Please use the following to indicate sections, subsections, +% etc. Please also use \subsubsection{...}, \paragraph{...} +% and \subparagraph{...} as necessary. +% + +\section{Introduction}\label{intro} + +% \paragraph{Didactics of mathematics} +%WN: wenn man in einem high-quality paper von 'didactics' spricht, +%WN muss man am state-of-the-art ankn"upfen -- siehe +%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants +% faces a specific issue, a gap +% between (1) introduction of math concepts and skills and (2) +% application of these concepts and skills, which usually are separated +% into different units in curricula (for good reasons). For instance, +% (1) teaching partial fraction decomposition is separated from (2) +% application for inverse Z-transform in signal processing. +% +% \par This gap is an obstacle for applying math as an fundamental +% thinking technology in engineering: In (1) motivation is lacking +% because the question ``What is this stuff good for?'' cannot be +% treated sufficiently, and in (2) the ``stuff'' is not available to +% students in higher semesters as widespread experience shows. +% +% \paragraph{Motivation} taken by this didactic issue on the one hand, +% and ongoing research and development on a novel kind of educational +% mathematics assistant at Graz University of +% Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to +% scope with this issue on the other hand, several institutes are +% planning to join their expertise: the Institute for Information +% Systems and Computer Media (IICM), the Institute for Software +% Technology (IST), the Institutes for Mathematics, the Institute for +% Signal Processing and Speech Communication (SPSC), the Institute for +% Structural Analysis and the Institute of Electrical Measurement and +% Measurement Signal Processing. +%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell +%WN und damit zu verg"anglich. +% \par This thesis is the first attempt to tackle the above mentioned +% issue, it focuses on Telematics, because these specific studies focus +% on mathematics in \emph{STEOP}, the introductory orientation phase in +% Austria. \emph{STEOP} is considered an opportunity to investigate the +% impact of {\sisac}'s prototype on the issue and others. +% + +Traditional course material in engineering disciplines lacks an +important component, interactive support for step-wise problem +solving. The lack becomes evident by comparing existing course +material with the sheets collected from written exams (in case solving +engineering problems is {\em not} deteriorated to multiple choice +tests) on the topics addressed by the materials. +Theorem-Proving (TP) technology can provide such support by +specific services. An important part of such services is called +``next-step-guidance'', generated by a specific kind of ``TP-based +programming language''. In the +{\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such +a language is prototyped in line with~\cite{plmms10} and built upon +the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002} +\footnote{http://isabelle.in.tum.de/}. +The TP services are coordinated by a specific interpreter for the +programming language, called +Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language + will be briefly re-introduced in order to make the paper +self-contained. + +The main part of the paper is an account of first experiences +with programming in this TP-based language. The experience was gained +in a case study by the author. The author was considered an ideal +candidate for this study for the following reasons: as a student in +Telematics (computer science with focus on Signal Processing) he had +general knowledge in programming as well as specific domain knowledge +in Signal Processing; and he was {\em not} involved in the development of +{\sisac}'s programming language and interpreter, thus being a novice to the +language. + +The goals of the case study were: (1) to identify some TP-based programs for +interactive course material for a specific ``Advanced Signal +Processing Lab'' in a higher semester, (2) respective program +development with as little advice as possible from the {\sisac}-team and (3) +to document records and comments for the main steps of development in an +Isabelle theory; this theory should provide guidelines for future programmers. +An excerpt from this theory is the main part of this paper. +\par + +\medskip The major example resulting from the case study will be used +as running example throughout this paper. This example requires a +program resembling the size of real-world applications in engineering; +such a size was considered essential for the case study, since there +are many small programs for a long time (mainly concerned with +elementary Computer Algebra like simplification, equation solving, +calculus, etc.~\footnote{The programs existing in the {\sisac} +prototype are found at +http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html}) + +\paragraph{The mathematical background of the running example} is the +following: In Signal Processing, ``the ${\cal Z}$-transform for +discrete-time signals is the counterpart of the Laplace transform for +continuous-time signals, and they each have a similar relationship to +the corresponding Fourier transform. One motivation for introducing +this generalization is that the Fourier transform does not converge +for all sequences, and it is useful to have a generalization of the +Fourier transform that encompasses a broader class of signals. A +second advantage is that in analytic problems, the ${\cal Z}$-transform +notation is often more convenient than the Fourier transform +notation.'' ~\cite[p. 128]{oppenheim2010discrete}. The ${\cal Z}$-transform +is defined as +\begin{equation*} +X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n} +\end{equation*} +where a discrete time sequence $x[n]$ is transformed into the function +$X(z)$ where $z$ is a continuous complex variable. The inverse +function is addressed in the running example and can be determined by +the integral +\begin{equation*} +x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz +\end{equation*} +where the letter $C$ represents a contour within the range of +convergence of the ${\cal Z}$-transform. The unit circle can be a special +case of this contour. Remember that $j$ is the complex number in the +domain of engineering. As this transform requires high effort to +be solved, tables of commonly used transform pairs are used in +education as well as in engineering practice; such tables can be found +at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well. +A completely solved and more detailed example can be found at +~\cite[p. 149f]{oppenheim2010discrete}. + +Following conventions in engineering education and in practice, the +running example solves the problem by use of a table. + +\paragraph{Support for interactive stepwise problem solving} in the +{\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance, +the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}: +A student inputs formulas line by line on the \textit{``Worksheet''}, +and each step (i.e. each formula on completion) is immediately checked +by the system, such that at most {\em one inconsistent} formula can reside on +the Worksheet (on the input line, marked by the red $\otimes$). +\begin{figure} [htb] +\begin{center} +\includegraphics[width=140mm]{fig/isac-Ztrans-math-3} +%\includegraphics[width=140mm]{fig/isac-Ztrans-math} +\caption{Step-wise problem solving guided by the TP-based program +\label{fig-interactive}} +\end{center} +\end{figure} +If the student gets stuck and does not know the formula to proceed +with, there is the button \framebox{NEXT} presenting the next formula +on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the +final result in case the student is not interested in intermediate +steps. + +Adaptive dialogue guidance is already under +construction~\cite{gdaroczy-EP-13} and the two buttons will disappear, +since their presence is not wanted in many learning scenarios (in +particular, {\em not} in written exams). + +The buttons \framebox{Theories}, \framebox{Problems} and +\framebox{Methods} are the entry points for interactive lookup of the +underlying knowledge. For instance, pushing \framebox{Theories} in +the configuration shown in Fig.\ref{fig-interactive}, pops up a +``Theory browser'' displaying the theorem(s) justifying the current +step. The browser allows to lookup all other theories, thus +supporting indepentend investigation of underlying definitions, +theorems, proofs --- where the HTML representation of the browsers is +ready for arbitrary multimedia add-ons. Likewise, the browsers for +\framebox{Problems} and \framebox{Methods} support context sensitive +as well as interactive access to specifications and programs +respectively. + +There is also a simple web-based representation of knowledge items; +the items under consideration in this paper can be looked up as +well +~\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}}} +~\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}}} +~\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}}}. + +% can be explained by having a look at +% Fig.\ref{fig-interactive} which shows the beginning of the interactive +% construction of a solution for the problem. This construction is done in the +% right window named ``Worksheet''. +% \par +% User-interaction on the Worksheet is {\em checked} and {\em guided} by +% TP services: +% \begin{enumerate} +% \item Formulas input by the user are {\em checked} by TP: such a +% formula establishes a proof situation --- the prover has to derive the +% formula from the logical context. The context is built up from the +% formal specification of the problem (here hidden from the user) by the +% Lucas-Interpreter. +% \item If the user gets stuck, the program developed below in this +% paper ``knows the next step'' and Lucas-Interpretation provides services +% featuring so-called ``next-step-guidance''; this is out of scope of this +% paper and can be studied in~\cite{gdaroczy-EP-13}. +% \end{enumerate} It should be noted that the programmer using the +% TP-based language is not concerned with interaction at all; we will +% see that the program contains neither input-statements nor +% output-statements. Rather, interaction is handled by the interpreter +% of the language. +% +% So there is a clear separation of concerns: Dialogues are adapted by +% dialogue authors (in Java-based tools), using TP services provided by +% Lucas-Interpretation. The latter acts on programs developed by +% mathematics-authors (in Isabelle/ML); their task is concern of this +% paper. + +\bigskip The paper is structured as follows: The introduction +\S\ref{intro} is followed by a brief re-introduction of the TP-based +programming language in \S\ref{PL}, which extends the executable +fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which +play a specific role in Lucas-Interpretation and in providing the TP +services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes +the main steps in developing the program for the running example: +prepare domain knowledge, implement the formal specification of the +problem, prepare the environment for the interpreter, implement the +program in \S\ref{isabisac} to \S\ref{progr} respectively. +The work-flow of programming, debugging and testing is +described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will +give directions identified for future development. + + +\section{\isac's Prototype for a Programming Language}\label{PL} +The prototype of the language and of the Lucas-Interpreter is briefly +described from the point of view of a programmer. The language extends +the executable fragment of Higher-Order Logic (HOL) in the theorem prover +Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}. + +\subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab} +The executable fragment consists of data-type and function +definitions. It's usability even suggests that fragment for +introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming +languages. Thus there are +\begin{description} +\item[base types,] in particular \textit{bool}, the type of truth +values, \textit{nat}, \textit{int}, \textit{complex}, and the types of +natural, integer and complex numbers respectively in mathematics. +\item[type constructors] allow to define arbitrary types, from +\textit{set}, \textit{list} to advanced data-structures like +\textit{trees}, red-black-trees etc. +\item[function types,] denoted by $\Rightarrow$. +\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide +type polymorphism. Isabelle automatically computes the type of each +variable in a term by use of Hindley-Milner type inference +\cite{pl:hind97,Milner-78}. +\end{description} + +\textbf{Terms} are formed as in functional programming by applying +functions to arguments. If $f$ is a function of type +$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then +$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$ +has type $\tau$. There are many predefined infix symbols like $+$ and +$\leq$ most of which are overloaded for various types. + +HOL also supports some basic constructs from functional programming: +{\footnotesize\it\label{isabelle-stmts} +\begin{tabbing} 123\=\kill +01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\ +02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\ +03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1 + \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$ +\end{tabbing}} +\noindent The running example's program uses some of these elements +(marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt +let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program +is an Isabelle term with specific function constants like {\tt +program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt +Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12} +respectively. + +% Terms may also contain $\lambda$-abstractions. For example, $\lambda +% x. \; x$ is the identity function. + +%JR warum auskommentiert? WN2... +%WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb +%WN2 des Papers auftauchen m"usste; nachdem ich einen solchen +%WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht +%WN2 gel"oscht. +%WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen +%WN2 Platz f"ur Anderes weg. + +\textbf{Formulae} are terms of type \textit{bool}. There are the basic +constants \textit{True} and \textit{False} and the usual logical +connectives (in decreasing order of precedence): $\neg, \land, \lor, +\rightarrow$. + +\textbf{Equality} is available in the form of the infix function $=$ +of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for +formulas, where it means ``if and only if''. + +\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \; +P$. Quantifiers lead to non-executable functions, so functions do not +always correspond to programs, for instance, if comprising \\$( +\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2 +\;)$. + +\subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs} +The prototype extends Isabelle's language by specific statements +called tactics~\footnote{{\sisac}'s. These tactics are different from +Isabelle's tactics: the former concern steps in a calculation, the +latter concern proofs.}. For the programmer these +statements are functions with the following signatures: + +\begin{description} +\item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it +term} * {\it term}\;{\it list}$: +this tactic applies {\it theorem} to a {\it term} yielding a {\it +term} and a {\it term list}, the list are assumptions generated by +conditional rewriting. For instance, the {\it theorem} +$b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$ +applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields +$(\frac{2}{3}, [x\not=0])$. + +\item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it +term}\Rightarrow{\it term} * {\it term}\;{\it list}$: +this tactic applies {\it ruleset} to a {\it term}; {\it ruleset} is +a confluent and terminating term rewrite system, in general. If +none of the rules ({\it theorem}s) is applicable on interpretation +of this tactic, an exception is thrown. + +% \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it +% theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it +% list}$: +% +% \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it +% ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it +% list}$: + +%SPACEvvv +\item[Substitute:] ${\it substitution}\Rightarrow{\it +term}\Rightarrow{\it term}$: allows to access sub-terms. +%SPACE^^^ + +\item[Take:] ${\it term}\Rightarrow{\it term}$: +this tactic has no effect in the program; but it creates a side-effect +by Lucas-Interpretation (see below) and writes {\it term} to the +Worksheet. + +\item[Subproblem:] ${\it theory} * {\it specification} * {\it +method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$: +this tactic is a generalisation of a function call: it takes an +\textit{argument list} as usual, and additionally a triple consisting +of an Isabelle \textit{theory}, an implicit \textit{specification} of the +program and a \textit{method} containing data for Lucas-Interpretation, +last not least a program (as an explicit specification)~\footnote{In +interactive tutoring these three items can be determined explicitly +by the user.}. +\end{description} +The tactics play a specific role in +Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as +break-points where, as a side-effect, a line is added to a calculation +as a protocol for proceeding towards a solution in step-wise problem +solving. At the same points Lucas-Interpretation serves interactive +tutoring and hands over control to the user. The user is free to +investigate underlying knowledge, applicable theorems, etc. And the +user can proceed constructing a solution by input of a tactic to be +applied or by input of a formula; in the latter case the +Lucas-Interpreter has built up a logical context (initialised with the +precondition of the formal specification) such that Isabelle can +derive the formula from this context --- or give feedback, that no +derivation can be found. + +\subsection{Tactics as Control Flow Statements} +The flow of control in a program can be determined by {\tt if then else} +and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also +by additional tactics: +\begin{description} +\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it +term}$: iterates over tactics which take a {\it term} as argument as +long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might +not be applicable). + +\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$: +if {\it tactic} is applicable, then it is applied to {\it term}, +otherwise {\it term} is passed on without changes. + +\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it +term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable, +it is applied to the first {\it term} yielding another {\it term}, +otherwise the second {\it tactic} is applied; if none is applicable an +exception is raised. + +\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it +term}\Rightarrow{\it term}$: applies the first {\it tactic} to the +first {\it term} yielding an intermediate term (not appearing in the +signature) to which the second {\it tactic} is applied. + +\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it +term}\Rightarrow{\it term}$: if the first {\it term} is true, then the +{\it tactic} is applied to the first {\it term} yielding an +intermediate term (not appearing in the signature); the intermediate +term is added to the environment the first {\it term} is evaluated in +etc. as long as the first {\it term} is true. +\end{description} +The tactics are not treated as break-points by Lucas-Interpretation +and thus do neither contribute to the calculation nor to interaction. + +\section{Concepts and Tasks in TP-based Programming}\label{trial} +%\section{Development of a Program on Trial} + +This section presents all the concepts involved in TP-based +programming and all the tasks to be accomplished by programmers. The +presentation uses the running example from +Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. + +\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac} + +%WN was Fachleute unter obigem Titel interessiert findet sich +%WN unterhalb des auskommentierten Textes. + +%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell +%WN auf Computer-Mathematiker fokussiert. +% \paragraph{As mentioned in the introduction,} a prototype of an +% educational math assistant called +% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for +% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges +% the gap between (1) introducation and (2) application of mathematics: +% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which +% requires each fact and each action justified by formal logic, so +% {{{\sisac}{}}} makes justifications transparent to students in +% interactive step-wise problem solving. By that way {{\sisac}} already +% can serve both: +% \begin{enumerate} +% \item Introduction of math stuff (in e.g. partial fraction +% decomposition) by stepwise explaining and exercising respective +% symbolic calculations with ``next step guidance (NSG)'' and rigorously +% checking steps freely input by students --- this also in context with +% advanced applications (where the stuff to be taught in higher +% semesters can be skimmed through by NSG), and +% \item Application of math stuff in advanced engineering courses +% (e.g. problems to be solved by inverse Z-transform in a Signal +% Processing Lab) and now without much ado about basic math techniques +% (like partial fraction decomposition): ``next step guidance'' supports +% students in independently (re-)adopting such techniques. +% \end{enumerate} +% Before the question is answers, how {{\sisac}} +% accomplishes this task from a technical point of view, some remarks on +% the state-of-the-art is given, therefor follow up Section~\ref{emas}. +% +% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} +% +% \paragraph{Educational software in mathematics} is, if at all, based +% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry +% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org} +% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC +% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These +% base technologies are used to program math lessons and sometimes even +% exercises. The latter are cumbersome: the steps towards a solution of +% such an interactive exercise need to be provided with feedback, where +% at each step a wide variety of possible input has to be foreseen by +% the programmer - so such interactive exercises either require high +% development efforts or the exercises constrain possible inputs. +% +% \subparagraph{A new generation} of educational math assistants (EMAs) +% is emerging presently, which is based on Theorem Proving (TP). TP, for +% instance Isabelle and Coq, is a technology which requires each fact +% and each action justified by formal logic. Pushed by demands for +% \textit{proven} correctness of safety-critical software TP advances +% into software engineering; from these advancements computer +% mathematics benefits in general, and math education in particular. Two +% features of TP are immediately beneficial for learning: +% +% \paragraph{TP have knowledge in human readable format,} that is in +% standard predicate calculus. TP following the LCF-tradition have that +% knowledge down to the basic definitions of set, equality, +% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; +% following the typical deductive development of math, natural numbers +% are defined and their properties +% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, +% etc. Present knowledge mechanized in TP exceeds high-school +% mathematics by far, however by knowledge required in software +% technology, and not in other engineering sciences. +% +% \paragraph{TP can model the whole problem solving process} in +% mathematical problem solving {\em within} a coherent logical +% framework. This is already being done by three projects, by +% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor. +% \par +% Having the whole problem solving process within a logical coherent +% system, such a design guarantees correctness of intermediate steps and +% of the result (which seems essential for math software); and the +% second advantage is that TP provides a wealth of theories which can be +% exploited for mechanizing other features essential for educational +% software. +% +% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid} +% +% One essential feature for educational software is feedback to user +% input and assistance in coming to a solution. +% +% \paragraph{Checking user input} by ATP during stepwise problem solving +% is being accomplished by the three projects mentioned above +% exclusively. They model the whole problem solving process as mentioned +% above, so all what happens between formalized assumptions (or formal +% specification) and goal (or fulfilled postcondition) can be +% mechanized. Such mechanization promises to greatly extend the scope of +% educational software in stepwise problem solving. +% +% \paragraph{NSG (Next step guidance)} comprises the system's ability to +% propose a next step; this is a challenge for TP: either a radical +% restriction of the search space by restriction to very specific +% problem classes is required, or much care and effort is required in +% designing possible variants in the process of problem solving +% \cite{proof-strategies-11}. +% \par +% Another approach is restricted to problem solving in engineering +% domains, where a problem is specified by input, precondition, output +% and postcondition, and where the postcondition is proven by ATP behind +% the scenes: Here the possible variants in the process of problem +% solving are provided with feedback {\em automatically}, if the problem +% is described in a TP-based programing language: \cite{plmms10} the +% programmer only describes the math algorithm without caring about +% interaction (the respective program is functional and even has no +% input or output statements!); interaction is generated as a +% side-effect by the interpreter --- an efficient separation of concern +% between math programmers and dialog designers promising application +% all over engineering disciplines. +% +% +% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}} +% Authoring new mathematics knowledge in {{\sisac}} can be compared with +% ``application programing'' of engineering problems; most of such +% programing uses CAS-based programing languages (CAS = Computer Algebra +% Systems; e.g. Mathematica's or Maple's programing language). +% +% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}} +% \cite{plmms10} for describing how to construct a solution to an +% engineering problem and for calling equation solvers, integration, +% etc~\footnote{Implementation of CAS-like functionality in TP is not +% primarily concerned with efficiency, but with a didactic question: +% What to decide for: for high-brow algorithms at the state-of-the-art +% or for elementary algorithms comprehensible for students?} within TP; +% TP can ensure ``systems that never make a mistake'' \cite{casproto} - +% are impossible for CAS which have no logics underlying. +% +% \subparagraph{Authoring is perfect} by writing such TP based programs; +% the application programmer is not concerned with interaction or with +% user guidance: this is concern of a novel kind of program interpreter +% called Lucas-Interpreter. This interpreter hands over control to a +% dialog component at each step of calculation (like a debugger at +% breakpoints) and calls automated TP to check user input following +% personalized strategies according to a feedback module. +% \par +% However ``application programing with TP'' is not done with writing a +% program: according to the principles of TP, each step must be +% justified. Such justifications are given by theorems. So all steps +% must be related to some theorem, if there is no such theorem it must +% be added to the existing knowledge, which is organized in so-called +% \textbf{theories} in Isabelle. A theorem must be proven; fortunately +% Isabelle comprises a mechanism (called ``axiomatization''), which +% allows to omit proofs. Such a theorem is shown in +% Example~\ref{eg:neuper1}. + +The running example requires to determine the inverse ${\cal Z}$-transform +for a class of functions. The domain of Signal Processing +is accustomed to specific notation for the resulting functions, which +are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the +function, $n$ is the argument and the brackets indicate that the +arguments are discrete. Surprisingly, Isabelle accepts the rules for +$z^{-1}$ in this traditional notation~\footnote{Isabelle +experts might be particularly surprised, that the brackets do not +cause errors in typing (as lists).}: +%\vbox{ +% \begin{example} + \label{eg:neuper1} + {\footnotesize\begin{tabbing} + 123\=123\=123\=123\=\kill + + 01\>axiomatization where \\ + 02\>\> rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\ + 03\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\ + 04\>\> rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\ + 05\>\> rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\ + 06\>\> rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\ + 07\>\> rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$'' + \end{tabbing}} +% \end{example} +%} +These 6 rules can be used as conditional rewrite rules, depending on +the respective convergence radius. Satisfaction from accordance with traditional +notation contrasts with the above word {\em axiomatization}: As TP-based, the +programming language expects these rules as {\em proved} theorems, and +not as axioms implemented in the above brute force manner; otherwise +all the verification efforts envisaged (like proof of the +post-condition, see below) would be meaningless. + +Isabelle provides a large body of knowledge, rigorously proved from +the basic axioms of mathematics~\footnote{This way of rigorously +deriving all knowledge from first principles is called the +LCF-paradigm in TP.}. In the case of the ${\cal Z}$-transform the most advanced +knowledge can be found in the theories on Multivariate +Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However, +building up knowledge such that a proof for the above rules would be +reasonably short and easily comprehensible, still requires lots of +work (and is definitely out of scope of our case study). + +%REMOVED DUE TO SPACE CONSTRAINTS +%At the state-of-the-art in mechanization of knowledge in engineering +%sciences, the process does not stop with the mechanization of +%mathematics traditionally used in these sciences. Rather, ``Formal +%Methods''~\cite{ fm-03} are expected to proceed to formal and explicit +%description of physical items. Signal Processing, for instance is +%concerned with physical devices for signal acquisition and +%reconstruction, which involve measuring a physical signal, storing it, +%and possibly later rebuilding the original signal or an approximation +%thereof. For digital systems, this typically includes sampling and +%quantization; devices for signal compression, including audio +%compression, image compression, and video compression, etc. ``Domain +%engineering''\cite{db:dom-eng} is concerned with {\em specification} +%of these devices' components and features; this part in the process of +%mechanization is only at the beginning in domains like Signal +%Processing. +% +%TP-based programming, concern of this paper, is determined to +%add ``algorithmic knowledge'' to the mechanised body of knowledge. +%% in Fig.\ref{fig:mathuni} on +%% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming +%% starts with a formal {\em specification} of the problem to be solved. +%% \begin{figure} +%% \begin{center} +%% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small} +%% \caption{The three-dimensional universe of mathematics knowledge} +%% \label{fig:mathuni} +%% \end{center} +%% \end{figure} +%% The language for both axes is defined in the axis at the bottom, deductive +%% knowledge, in {\sisac} represented by Isabelle's theories. + +\subsection{Preparation of Simplifiers for the Program}\label{simp} + +All evaluation in the prototype's Lucas-Interpreter is done by term rewriting on +Isabelle's terms, see \S\ref{meth} below; in this section some of respective +preparations are described. In order to work reliably with term rewriting, the +respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that}, +then they are called (canonical) simplifiers. These properties do not go without +saying, their establishment is a difficult task for the programmer; this task is +not yet supported in the prototype. + +The prototype rewrites using theorems only. Axioms which are theorems as well +have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we +assemble them in a rule-set and apply them in ML as follows: + +{\footnotesize +\begin{verbatim} + 01 val inverse_z = Rls + 02 {id = "inverse_z", + 03 rew_ord = dummy_ord, + 04 erls = Erls, + 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}), + 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}), + 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})], + 08 errpatts = [], + 09 scr = ""} +\end{verbatim}} + +\noindent The items, line by line, in the above record have the following purpose: +\begin{description} +\item[01..02] the ML-value \textit{inverse\_z} stores it's identifier +as a string for ``reflection'' when switching between the language +layers of Isabelle/ML (like in the Lucas-Interpreter) and +Isabelle/Isar (like in the example program on p.\pageref{s:impl} on +line {\rm 12}). + +\item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that} +\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here: +(a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting +and (b) the assumptions of the \textit{rules} need not be evaluated +(they just go into the context during rewriting). + +\item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1}; +also ML-functions (\S\ref{funs}) can come into this list as shown in +\S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm} +and \textit{Calc} respectively; for the purpose of reflection both +contain their identifiers. + +\item[08..09] are error-patterns not discussed here and \textit{scr} +is prepared to get a program, automatically generated by {\sisac} for +producing intermediate rewrites when requested by the user. + +\end{description} + +%OUTCOMMENTED DUE TO SPACE RESTRICTIONS +% \noindent It is advisable to immediately test rule-sets; for that +% purpose an appropriate term has to be created; \textit{parse} takes a +% context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal +% Z}^{-1}$) and creates a term: +% +% {\footnotesize +% \begin{verbatim} +% 01 ML {* +% 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - ) + 1)"; +% 03 *} +% 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1", +% 05 "RealDef.real => RealDef.real => RealDef.real") $ +% 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...) +% \end{verbatim}} +% +% \noindent The internal representation of the term, as required for +% rewriting, consists of \textit{Const}ants, a pair of a string +% \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables +% \textit{Free} and the respective constructor \textit{\$}. Now the +% term can be rewritten by the rule-set \textit{inverse\_z}: +% +% {\footnotesize +% \begin{verbatim} +% 01 ML {* +% 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t; +% 03 term2str t'; +% 04 terms2str asm; +% 05 *} +% 06 val it = "u[n] + ^ n * u[n] + [n]" : string +% 07 val it = "|| z || > 1 & || z || > " : string +% \end{verbatim}} +% +% \noindent The resulting term \textit{t} and the assumptions +% \textit{asm} are converted to readable strings by \textit{term2str} +% and \textit{terms2str}. + +\subsection{Preparation of ML-Functions}\label{funs} +Some functionality required in programming, cannot be accomplished by +rewriting. So the prototype has a mechanism to call functions within +the rewrite-engine: certain redexes in Isabelle terms call these +functions written in SML~\cite{pl:milner97}, the implementation {\em +and} meta-language of Isabelle. The programmer has to use this +mechanism. + +In the running example's program on p.\pageref{s:impl} the lines {\rm +05} and {\rm 06} contain such functions; we go into the details with +\textit{argument\_in X\_z;}. This function fetches the argument from a +function application: Line {\rm 03} in the example calculation on +p.\pageref{exp-calc} is created by line {\rm 06} of the example +program on p.\pageref{s:impl} where the program's environment assigns +the value \textit{X z} to the variable \textit{X\_z}; so the function +shall extract the argument \textit{z}. + +\medskip In order to be recognised as a function constant in the +program source the constant needs to be declared in a theory, here in +\textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in +the context \textit{ctxt} of that theory: + +{\footnotesize +\begin{verbatim} +01 consts +02 argument'_in :: "real => real" ("argument'_in _" 10) +\end{verbatim}} + +%^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *} +%^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real") +%^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term +%^3.2^ \end{verbatim}} +%^3.2^ +%^3.2^ \noindent Parsing produces a term \texttt{t} in internal +%^3.2^ representation~\footnote{The attentive reader realizes the +%^3.2^ differences between interal and extermal representation even in the +%^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const +%^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X", +%^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term +%^3.2^ constructor. +The function body below is implemented directly in SML, +i.e in an \texttt{ML \{* *\}} block; the function definition provides +a unique prefix \texttt{eval\_} to the function name: + +{\footnotesize +\begin{verbatim} +01 ML {* +02 fun eval_argument_in _ +03 "Build_Inverse_Z_Transform.argument'_in" +04 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ = +05 if is_Free arg (*could be something to be simplified before*) +06 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg))) +07 else NONE +08 | eval_argument_in _ _ _ _ = NONE; +09 *} +\end{verbatim}} + +\noindent The function body creates either \texttt{NONE} +telling the rewrite-engine to search for the next redex, or creates an +ad-hoc theorem for rewriting, thus the programmer needs to adopt many +technicalities of Isabelle, for instance, the \textit{Trueprop} +constant. + +\bigskip This sub-task particularly sheds light on basic issues in the +design of a programming language, the integration of differential language +layers, the layer of Isabelle/Isar and Isabelle/ML. + +Another point of improvement for the prototype is the rewrite-engine: The +program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05} +and {\rm 06} to + +{\small\it\label{s:impl} +\begin{tabbing} +123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill +\>{\rm 05/06}\>\>\> (z::real) = argument\_in (lhs X\_eq) ; +\end{tabbing}} + +\noindent because nested function calls would require creating redexes +inside-out; however, the prototype's rewrite-engine only works top down +from the root of a term down to the leaves. + +How all these technicalities are to be checked in the prototype is +shown in \S\ref{flow-prep} below. + +% \paragraph{Explicit Problems} require explicit methods to solve them, and within +% this methods we have some explicit steps to do. This steps can be unique for +% a special problem or refindable in other problems. No mather what case, such +% steps often require some technical functions behind. For the solving process +% of the Inverse Z Transformation and the corresponding partial fraction it was +% neccessary to build helping functions like \texttt{get\_denominator}, +% \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us +% to filter the denominator or numerator out of a fraction, last one helps us to +% get to know the bound variable in a equation. +% \par +% By taking \texttt{get\_denominator} as an example, we want to explain how to +% implement new functions into the existing system and how we can later use them +% in our program. +% +% \subsubsection{Find a place to Store the Function} +% +% The whole system builds up on a well defined structure of Knowledge. This +% Knowledge sets up at the Path: +% \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center} +% For implementing the Function \texttt{get\_denominator} (which let us extract +% the denominator out of a fraction) we have choosen the Theory (file) +% \texttt{Rational.thy}. +% +% \subsubsection{Write down the new Function} +% +% In upper Theory we now define the new function and its purpose: +% \begin{verbatim} +% get_denominator :: "real => real" +% \end{verbatim} +% This command tells the machine that a function with the name +% \texttt{get\_denominator} exists which gets a real expression as argument and +% returns once again a real expression. Now we are able to implement the function +% itself, upcoming example now shows the implementation of +% \texttt{get\_denominator}. +% +% %\begin{example} +% \label{eg:getdenom} +% \begin{verbatim} +% +% 01 (* +% 02 *("get_denominator", +% 03 * ("Rational.get_denominator", eval_get_denominator "")) +% 04 *) +% 05 fun eval_get_denominator (thmid:string) _ +% 06 (t as Const ("Rational.get_denominator", _) $ +% 07 (Const ("Rings.inverse_class.divide", _) $num +% 08 $denom)) thy = +% 09 SOME (mk_thmid thmid "" +% 10 (Print_Mode.setmp [] +% 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "", +% 12 Trueprop $ (mk_equality (t, denom))) +% 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim} +% %\end{example} +% +% Line \texttt{07} and \texttt{08} are describing the mode of operation the best - +% there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont) +% splittet +% into its two parts (\texttt{\$num \$denom}). The lines before are additionals +% commands for declaring the function and the lines after are modeling and +% returning a real variable out of \texttt{\$denom}. +% +% \subsubsection{Add a test for the new Function} +% +% \paragraph{Everytime when adding} a new function it is essential also to add +% a test for it. Tests for all functions are sorted in the same structure as the +% knowledge it self and can be found up from the path: +% \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center} +% This tests are nothing very special, as a first prototype the functionallity +% of a function can be checked by evaluating the result of a simple expression +% passed to the function. Example~\ref{eg:getdenomtest} shows the test for our +% \textit{just} created function \texttt{get\_denominator}. +% +% %\begin{example} +% \label{eg:getdenomtest} +% \begin{verbatim} +% +% 01 val thy = @{theory Isac}; +% 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)")); +% 03 val SOME (_, t') = eval_get_denominator "" 0 t thy; +% 04 if term2str t' = "get_denominator ((a + x) / b) = b" then () +% 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim} +% %\end{example} +% +% \begin{description} +% \item[01] checks if the proofer set up on our {\sisac{}} System. +% \item[02] passes a simple expression (fraction) to our suddenly created +% function. +% \item[04] checks if the resulting variable is the correct one (in this case +% ``b'' the denominator) and returns. +% \item[05] handels the error case and reports that the function is not able to +% solve the given problem. +% \end{description} + +\subsection{Specification of the Problem}\label{spec} +%WN <--> \chapter 7 der Thesis +%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. + +Mechanical treatment requires to translate a textual problem +description like in Fig.\ref{fig-interactive} on +p.\pageref{fig-interactive} into a {\em formal} specification. The +formal specification of the running example could look like is this +~\footnote{The ``TODO'' in the postcondition indicates, that postconditions +are not yet handled in the prototype; in particular, the postcondition, i.e. +the correctness of the result is not yet automatically proved.}: + +%WN Hier brauchen wir die Spezifikation des 'running example' ... +%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei +%JR der post condition - die existiert für uns ja eigentlich nicht aka +%JR haben sie bis jetzt nicht beachtet WN... +%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren. +%JR2 done + +\label{eg:neuper2} +{\small\begin{tabbing} + 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill + %\hfill \\ + \>Specification:\\ + \> \>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}\}$\\ + \>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\ + \>\>output \>: stepResponse $x[n]$ \\ + \>\>postcond \>: TODO +\end{tabbing}} + +%JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt" + +% \begin{remark} +% Defining the postcondition requires a high amount mathematical +% knowledge, the difficult part in our case is not to set up this condition +% nor it is more to define it in a way the interpreter is able to handle it. +% Due the fact that implementing that mechanisms is quite the same amount as +% creating the programm itself, it is not avaible in our prototype. +% \label{rm:postcond} +% \end{remark} + +The implementation of the formal specification in the present +prototype, still bar-bones without support for authoring, is done +like that: +%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert: + +{\footnotesize\label{exp-spec} +\begin{verbatim} + 00 ML {* + 01 store_specification + 02 (prepare_specification + 03 "pbl_SP_Ztrans_inv" + 04 ["Jan Rocnik"] + 05 thy + 06 ( ["Inverse", "Z_Transform", "SignalProcessing"], + 07 [ ("#Given", ["filterExpression X_eq", "domain D"]), + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), + 09 ("#Find" , ["stepResponse n_eq"]), + 10 ("#Post" , [" TODO "])]) + 11 prls + 12 NONE + 13 [["SignalProcessing","Z_Transform","Inverse"]]); + 14 *} +\end{verbatim}} + +Although the above details are partly very technical, we explain them +in order to document some intricacies of TP-based programming in the +present state of the {\sisac} prototype: +\begin{description} +\item[01..02]\textit{store\_specification:} stores the result of the +function \textit{prep\_specification} in a global reference +\textit{Unsynchronized.ref}, which causes principal conflicts with +Isabelle's asynchronous document model~\cite{Wenzel-11:doc-orient} and +parallel execution~\cite{Makarius-09:parall-proof} and is under +reconstruction already. + +\textit{prep\_specification:} translates the specification to an internal format +which allows efficient processing; see for instance line {\rm 07} +below. +\item[03..04] are a unique identifier for the specification within {\sisac} +and the ``mathematics author'' holding the copy-rights. +\item[05] is the Isabelle \textit{theory} required to parse the +specification in lines {\rm 07..10}. +\item[06] is a key into the tree of all specifications as presented to +the user (where some branches might be hidden by the dialogue +component). +\item[07..10] are the specification with input, pre-condition, output +and post-condition respectively; note that the specification contains +variables to be instantiated with concrete values for a concrete problem --- +thus the specification actually captures a class of problems. The post-condition is not handled in +the prototype presently. +\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 +rewriting determined by rule-sets. +\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a +problem associated to a function from Computer Algebra (like an +equation solver) which is not the case here. +\item[13] is a list of methods solving the specified problem (here +only one list item) represented analogously to {\rm 06}. +\end{description} + + +%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *" +%WN ... +% type pbt = +% {guh : guh, (*unique within this isac-knowledge*) +% mathauthors: string list, (*copyright*) +% init : pblID, (*to start refinement with*) +% thy : theory, (* which allows to compile that pbt +% TODO: search generalized for subthy (ref.p.69*) +% (*^^^ WN050912 NOT used during application of the problem, +% because applied terms may be from 'subthy' as well as from super; +% thus we take 'maxthy'; see match_ags !*) +% cas : term option,(*'CAS-command'*) +% prls : rls, (* for preds in where_*) +% where_: term list, (* where - predicates*) +% ppc : pat list, +% (*this is the model-pattern; +% it contains "#Given","#Where","#Find","#Relate"-patterns +% for constraints on identifiers see "fun cpy_nam"*) +% met : metID list}; (* methods solving the pbt*) +% +%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen +%WN oben selbst geschrieben. + + + + +%WN das w"urde ich in \sec\label{progr} verschieben und +%WN das SubProblem partial fractions zum Erkl"aren verwenden. +% Such a specification is checked before the execution of a program is +% started, the same applies for sub-programs. In the following example +% (Example~\ref{eg:subprob}) shows the call of such a subproblem: +% +% \vbox{ +% \begin{example} +% \label{eg:subprob} +% \hfill \\ +% {\ttfamily \begin{tabbing} +% ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\ +% ``\>\>[linear,univariate,equation,test],'' \\ +% ``\>\>[Test,solve\_linear])'' \\ +% ``\>[BOOL equ, REAL z])'' \\ +% \end{tabbing} +% } +% {\small\textit{ +% \noindent If a program requires a result which has to be +% calculated first we can use a subproblem to do so. In our specific +% case we wanted to calculate the zeros of a fraction and used a +% subproblem to calculate the zeros of the denominator polynom. +% }} +% \end{example} +% } + +\subsection{Implementation of the Method}\label{meth} +A method collects all data required to interpret a certain program by +Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of +the running example is embedded on the last line in the following method: +%The methods represent the different ways a problem can be solved. This can +%include mathematical tactics as well as tactics taught in different courses. +%Declaring the Method itself gives us the possibilities to describe the way of +%calculation in deep, as well we get the oppertunities to build in different +%rulesets. + +{\footnotesize +\begin{verbatim} + 00 ML {* + 01 store_method + 02 (prep_method + 03 "SP_InverseZTransformation_classic" + 04 ["Jan Rocnik"] + 05 thy + 06 ( ["SignalProcessing", "Z_Transform", "Inverse"], + 07 [ ("#Given", ["filterExpression X_eq", "domain D"]), + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), + 09 ("#Find" , ["stepResponse n_eq"]), + 10 rew_ord erls + 11 srls prls nrls + 12 errpats + 13 program); + 14 *} +\end{verbatim}} + +\noindent The above code stores the whole structure analogously to a +specification as described above: +\begin{description} +\item[01..06] are identical to those for the example specification on +p.\pageref{exp-spec}. + +\item[07..09] show something looking like the specification; this is a +{\em guard}: as long as not all \textit{Given} items are present and +the \textit{Pre}-conditions is not true, interpretation of the program +is not started. + +\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 +\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 +\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g. +\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} +and (c) is required for the derivation-machinery checking user-input formulas. + +\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}. +\end{description} +The many rule-sets above cause considerable efforts for the +programmers, in particular, because there are no tools for checking +essential features of rule-sets. + +% is again very technical and goes hard in detail. Unfortunataly +% most declerations are not essential for a basic programm but leads us to a huge +% range of powerful possibilities. +% +% \begin{description} +% \item[01..02] stores the method with the given name into the system under a global +% reference. +% \item[03] specifies the topic within which context the method can be found. +% \item[04..05] as the requirements for different methods can be deviant we +% declare what is \emph{given} and and what to \emph{find} for this specific method. +% The code again helds on the topic of the case studie, where the inverse +% z-transformation does a switch between a term describing a electrical filter into +% its step response. Also the datatype has to be declared (bool - due the fact that +% we handle equations). +% \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one +% theorem of it is used for rewriting one single step. +% \item[07] \texttt{rls} is the currently used ruleset for this method. This set +% has already been defined before. +% \item[08] we would have the possiblitiy to add this method to a predefined tree of +% calculations, i.eg. if it would be a sub of a bigger problem, here we leave it +% independend. +% \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in +% the source. +% \item[10] \emph{predicates ruleset} can be used to indicates predicates within +% model patterns. +% \item[11] The \emph{check ruleset} summarizes rules for checking formulas +% elementwise. +% \item[12] \emph{error patterns} which are expected in this kind of method can be +% pre-specified to recognize them during the method. +% \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier +% of the specific method. +% \item[14] for this code snipset we don't specify the programm itself and keep it +% empty. Follow up \S\ref{progr} for informations on how to implement this +% \textit{main} part. +% \end{description} + +\subsection{Implementation of the TP-based Program}\label{progr} +So finally all the prerequisites are described and the final task can +be addressed. The program below comes back to the running example: it +computes a solution for the problem from Fig.\ref{fig-interactive} on +p.\pageref{fig-interactive}. The reader is reminded of +\S\ref{PL-isab}, the introduction of the programming language: + +{\footnotesize\it\label{s:impl} +\begin{tabbing} +123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill +\>{\rm 00}\>ML \{*\\ +\>{\rm 00}\>val program =\\ +\>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\ +\>{\rm 02}\>\> {\tt let} \\ +\>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\ +\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\ +\>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation +\>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\ +\>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\ +\>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\ +%\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\ +\>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\ +\>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\ +\>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@ \\ +\>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\ +\>{\rm 13}\>\> {\tt in } \\ +\>{\rm 14}\>\>\> X'\_eq"\\ +\>{\rm 15}\>*\} +\end{tabbing}} +% ORIGINAL FROM Inverse_Z_Transform.thy +% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) +% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) +% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) +% " (X'_z::real) = lhs X'; "^(* ?X' z*) +% " (zzz::real) = argument_in X'_z; "^(* z *) +% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) +% +% " (pbz::real) = (SubProblem (Isac', "^(**) +% " [partial_fraction,rational,simplification], "^ +% " [simplification,of_rationals,to_partial_fraction]) "^ +% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) +% +% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) +% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) +% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) +% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) +% " 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]*) +% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) +% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) +The program is represented as a string and part of the method in +\S\ref{meth}. As mentioned in \S\ref{PL} the program is purely +functional and lacks any input statements and output statements. So +the steps of calculation towards a solution (and interactive tutoring +in step-wise problem solving) are created as a side-effect by +Lucas-Interpretation. The side-effects are triggered by the tactics +\texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and +\texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and +{\rm 12} respectively. These tactics produce the respective lines in the +calculation on p.\pageref{flow-impl}. + +The above lines {\rm 05, 06} do not contain a tactics, so they do not +immediately contribute to the calculation on p.\pageref{flow-impl}; +rather, they compute actual arguments for the \texttt{SubProblem} in +line {\rm 09}~\footnote{The tactics also are break-points for the +interpreter, where control is handed over to the user in interactive +tutoring.}. Line {\rm 11} contains tactical \textit{@@}. + +\medskip The above program also indicates the dominant role of interactive +selection of knowledge in the three-dimensional universe of +mathematics. The \texttt{SubProblem} in the above lines +{\rm 07..09} is more than a function call with the actual arguments +\textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine +three items: + +\begin{enumerate} +\item the theory, in the example \textit{Isac} because different +methods can be selected in Pt.3 below, which are defined in different +theories with \textit{Isac} collecting them. +\item the specification identified by \textit{[partial\_fraction, +rational, simplification]} in the tree of specifications; this +specification is analogous to the specification of the main program +described in \S\ref{spec}; the problem is to find a ``partial fraction +decomposition'' for a univariate rational polynomial. +\item the method in the above example is \textit{[ ]}, i.e. empty, +which supposes the interpreter to select one of the methods predefined +in the specification, for instance in line {\rm 13} in the running +example's specification on p.\pageref{exp-spec}~\footnote{The freedom +(or obligation) for selection carries over to the student in +interactive tutoring.}. +\end{enumerate} + +The program code, above presented as a string, is parsed by Isabelle's +parser --- the program is an Isabelle term. This fact is expected to +simplify verification tasks in the future; on the other hand, this +fact causes troubles in error detection which are discussed as part +of the work-flow in the subsequent section. + +\section{Work-flow of Programming in the Prototype}\label{workflow} +The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great +step forward for interactive theory and proof development. The +{\sisac}-prototype re-uses this IDE as a programming environment. The +experiences from this re-use show, that the essential components are +available from Isabelle/jEdit. However, additional tools and features +are required to achieve acceptable usability. + +So notable experiences are reported here, also as a requirement +capture for further development of TP-based languages and respective +IDEs. + +\subsection{Preparations and Trials}\label{flow-prep} +The many sub-tasks to be accomplished {\em before} the first line of +program code can be written and tested suggest an approach which +step-wise establishes the prerequisites. The case study underlying +this paper~\cite{jrocnik-bakk} documents the approach in a separate +Isabelle theory, +\textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part +II in the study comprises this theory, \LaTeX ed from the theory by +use of Isabelle's document preparation system. This paper resembles +the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual +implementation work involves several iterations. + +\bigskip For instance, only the last step, implementing the program +described in \S\ref{meth}, reveals details required. Let us assume, +this is the ML-function \textit{argument\_in} required in line {\rm 06} +of the example program on p.\pageref{s:impl}; how this function needs +to be implemented in the prototype has been discussed in \S\ref{funs} +already. + +Now let us assume, that calling this function from the program code +does not work; so testing this function is required in order to find out +the reason: type errors, a missing entry of the function somewhere or +even more nasty technicalities \dots + +{\footnotesize +\begin{verbatim} +01 ML {* +02 val SOME t = parseNEW ctxt "argument_in (X (z::real))"; +03 val SOME (str, t') = eval_argument_in "" +04 "Build_Inverse_Z_Transform.argument'_in" t 0; +05 term2str t'; +06 *} +07 val it = "(argument_in X z) = z": string\end{verbatim}} + +\noindent So, this works: we get an ad-hoc theorem, which used in +rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this +reduction and create a rule-set \texttt{rls} for that purpose: + +{\footnotesize +\begin{verbatim} +01 ML {* +02 val rls = append_rls "test" e_rls +03 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")] +04 val SOME (t', asm) = rewrite_set_ @{theory} rls t; +05 *} +06 val t' = Free ("z", "RealDef.real"): term +07 val asm = []: term list\end{verbatim}} + +\noindent The resulting term \texttt{t'} is \texttt{Free ("z", +"RealDef.real")}, i.e the variable \texttt{z}, so all is +perfect. Probably we have forgotten to store this function correctly~? +We review the respective \texttt{calclist} (again an +\textit{Unsynchronized.ref} to be removed in order to adjust to +Isabelle/Isar's asynchronous document model): + +{\footnotesize +\begin{verbatim} +01 calclist:= overwritel (! calclist, +02 [("argument_in", +03 ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")), +04 ... +05 ]);\end{verbatim}} + +\noindent The entry is perfect. So what is the reason~? Ah, probably there +is something messed up with the many rule-sets in the method, see \S\ref{meth} --- +right, the function \texttt{argument\_in} is not contained in the respective +rule-set \textit{srls} \dots this just as an example of the intricacies in +debugging a program in the present state of the prototype. + +\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} +Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth}, +usually developed within several iterations, the program can be +assembled; on p.\pageref{s:impl} there is the complete program of the +running example. + +The completion of this program required efforts for several weeks +(after some months of familiarisation with {\sisac}), caused by the +abundance of intricacies indicated above. Also writing the program is +not pleasant, given Isabelle/Isar/ without add-ons for +programming. Already writing and parsing a few lines of program code +is a challenge: the program is an Isabelle term; Isabelle's parser, +however, is not meant for huge terms like the program of the running +example. So reading out the specific error (usually type errors) from +Isabelle's message is difficult. + +\medskip Testing the evaluation of the program has to rely on very +simple tools. Step-wise execution is modeled by a function +\texttt{me}, short for mathematics-engine~\footnote{The interface used +by the front-end which created the calculation on +p.\pageref{fig-interactive} is different from this function}: +%the following is a simplification of the actual function + +{\footnotesize +\begin{verbatim} +01 ML {* me; *} +02 val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}} + +\noindent This function takes as arguments a tactic \texttt{tac} which +determines the next step, the step applied to the interpreter-state +\texttt{ctree * pos} as last argument taken. The interpreter-state is +a pair of a tree \texttt{ctree} representing the calculation created +(see the example below) and a position \texttt{pos} in the +calculation. The function delivers a quadruple, beginning with the new +formula \texttt{mout} and the next tactic followed by the new +interpreter-state. + +This function allows to stepwise check the program: + +{\footnotesize\label{ml-check-program} +\begin{verbatim} +01 ML {* +02 val fmz = +03 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))", +04 "stepResponse (x[n::real]::bool)"]; +05 val (dI,pI,mI) = +06 ("Isac", +07 ["Inverse", "Z_Transform", "SignalProcessing"], +08 ["SignalProcessing","Z_Transform","Inverse"]); +09 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))]; +10 val (mout, tac, ctree, pos) = me tac (ctree, pos); +11 val (mout, tac, ctree, pos) = me tac (ctree, pos); +12 val (mout, tac, ctree, pos) = me tac (ctree, pos); +13 ... +\end{verbatim}} + +\noindent Several dozens of calls for \texttt{me} are required to +create the lines in the calculation below (including the sub-problems +not shown). When an error occurs, the reason might be located +many steps before: if evaluation by rewriting, as done by the prototype, +fails, then first nothing happens --- the effects come later and +cause unpleasant checks. + +The checks comprise watching the rewrite-engine for many different +kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in +particular the environment and the context at the states position --- +all checks have to rely on simple functions accessing the +\texttt{ctree}. So getting the calculation below (which resembles the +calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) +is the result of several weeks of development: + +{\small\it\label{exp-calc} +\begin{tabbing} +123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill +\>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\ +\>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\ +\>{\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}\\ +\>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\ +\>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\ +\>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\ +\>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\ +\>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\ +\>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\ +\>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\ +\> \>\>\>\> \_\_\_ \`- - -\\ +\>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\ +\>{\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)}\\ +\>{\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 }\\ +\>{\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}\\ +\>{\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}} +\end{tabbing}} +The tactics on the right margin of the above calculation are those in +the program on p.\pageref{s:impl} which create the respective formulas +on the left. +% ORIGINAL FROM Inverse_Z_Transform.thy +% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) +% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) +% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) +% " (X'_z::real) = lhs X'; "^(* ?X' z*) +% " (zzz::real) = argument_in X'_z; "^(* z *) +% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) +% +% " (pbz::real) = (SubProblem (Isac', "^(**) +% " [partial_fraction,rational,simplification], "^ +% " [simplification,of_rationals,to_partial_fraction]) "^ +% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) +% +% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) +% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) +% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) +% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) +% " 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]*) +% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) +% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) + +\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans} +Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done +and the knowledge accumulated in it can be distributed to appropriate +theories: the program to \textit{Inverse\_Z\_Transform.thy}, the +sub-problem accomplishing the partial fraction decomposition to +\textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's +internals, this kind of distribution is not trivial. For instance, the +function \texttt{argument\_in} in \S\ref{funs} explicitly contains a +string with the theory it has been defined in, so this string needs to +be updated from \texttt{Build\_Inverse\_Z\_Transform} to +\texttt{Atools} if that function is transferred to theory +\textit{Atools.thy}. + +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. +This process is also rather bare-bones without authoring tools and is +described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}. + +% \newpage +% ------------------------------------------------------------------- +% +% Material, falls noch Platz bleibt ... +% +% ------------------------------------------------------------------- +% +% +% \subsubsection{Trials on Notation and Termination} +% +% \paragraph{Technical notations} are a big problem for our piece of software, +% but the reason for that isn't a fault of the software itself, one of the +% troubles comes out of the fact that different technical subtopics use different +% symbols and notations for a different purpose. The most famous example for such +% a symbol is the complex number $i$ (in cassique math) or $j$ (in technical +% math). In the specific part of signal processing one of this notation issues is +% the use of brackets --- we use round brackets for analoge signals and squared +% brackets for digital samples. Also if there is no problem for us to handle this +% fact, we have to tell the machine what notation leads to wich meaning and that +% this purpose seperation is only valid for this special topic - signal +% processing. +% \subparagraph{In the programming language} itself it is not possible to declare +% fractions, exponents, absolutes and other operators or remarks in a way to make +% them pretty to read; our only posssiblilty were ASCII characters and a handfull +% greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$. +% \par +% With the upper collected knowledge it is possible to check if we were able to +% donate all required terms and expressions. +% +% \subsubsection{Definition and Usage of Rules} +% +% \paragraph{The core} of our implemented problem is the Z-Transformation, due +% the fact that the transformation itself would require higher math which isn't +% yet avaible in our system we decided to choose the way like it is applied in +% labratory and problem classes at our university - by applying transformation +% rules (collected in transformation tables). +% \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the +% use of axiomatizations like shown in Example~\ref{eg:ruledef} +% +% \begin{example} +% \label{eg:ruledef} +% \hfill\\ +% \begin{verbatim} +% axiomatization where +% rule1: ``1 = $\delta$[n]'' and +% rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and +% rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]'' +% \end{verbatim} +% \end{example} +% +% This rules can be collected in a ruleset and applied to a given expression as +% follows in Example~\ref{eg:ruleapp}. +% +% \begin{example} +% \hfill\\ +% \label{eg:ruleapp} +% \begin{enumerate} +% \item Store rules in ruleset: +% \begin{verbatim} +% val inverse_Z = append_rls "inverse_Z" e_rls +% [ Thm ("rule1",num_str @{thm rule1}), +% Thm ("rule2",num_str @{thm rule2}), +% Thm ("rule3",num_str @{thm rule3}) +% ];\end{verbatim} +% \item Define exression: +% \begin{verbatim} +% val sample_term = str2term "z/(z-1)+z/(z-)+1";\end{verbatim} +% \item Apply ruleset: +% \begin{verbatim} +% val SOME (sample_term', asm) = +% rewrite_set_ thy true inverse_Z sample_term;\end{verbatim} +% \end{enumerate} +% \end{example} +% +% The use of rulesets makes it much easier to develop our designated applications, +% but the programmer has to be careful and patient. When applying rulesets +% two important issues have to be mentionend: +% \subparagraph{How often} the rules have to be applied? In case of +% transformations it is quite clear that we use them once but other fields +% reuqire to apply rules until a special condition is reached (e.g. +% a simplification is finished when there is nothing to be done left). +% \subparagraph{The order} in which rules are applied often takes a big effect +% and has to be evaluated for each purpose once again. +% \par +% In our special case of Signal Processing and the rules defined in +% Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all +% constants. After this step has been done it no mather which rule fit's next. +% +% \subsubsection{Helping Functions} +% +% \paragraph{New Programms require,} often new ways to get through. This new ways +% means that we handle functions that have not been in use yet, they can be +% something special and unique for a programm or something famous but unneeded in +% the system yet. In our dedicated example it was for example neccessary to split +% a fraction into numerator and denominator; the creation of such function and +% even others is described in upper Sections~\ref{simp} and \ref{funs}. +% +% \subsubsection{Trials on equation solving} +% %simple eq and problem with double fractions/negative exponents +% \paragraph{The Inverse Z-Transformation} makes it neccessary to solve +% equations degree one and two. Solving equations in the first degree is no +% problem, wether for a student nor for our machine; but even second degree +% equations can lead to big troubles. The origin of this troubles leads from +% the build up process of our equation solving functions; they have been +% implemented some time ago and of course they are not as good as we want them to +% be. Wether or not following we only want to show how cruel it is to build up new +% work on not well fundamentials. +% \subparagraph{A simple equation solving,} can be set up as shown in the next +% example: +% +% \begin{example} +% \begin{verbatim} +% +% val fmz = +% ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))", +% "solveFor z", +% "solutions L"]; +% +% val (dI',pI',mI') = +% ("Isac", +% ["abcFormula","degree_2","polynomial","univariate","equation"], +% ["no_met"]);\end{verbatim} +% \end{example} +% +% Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give +% a short overview on the commands; at first we set up the equation and tell the +% machine what's the bound variable and where to store the solution. Second step +% is to define the equation type and determine if we want to use a special method +% to solve this type.) Simple checks tell us that the we will get two results for +% this equation and this results will be real. +% So far it is easy for us and for our machine to solve, but +% mentioned that a unvariate equation second order can have three different types +% of solutions it is getting worth. +% \subparagraph{The solving of} all this types of solutions is not yet supported. +% Luckily it was needed for us; but something which has been needed in this +% context, would have been the solving of an euation looking like: +% $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned +% before (remember that befor it was no problem to handle for the machine) but +% now, after a simple equivalent transformation, we are not able to solve +% it anymore. +% \subparagraph{Error messages} we get when we try to solve something like upside +% were very confusing and also leads us to no special hint about a problem. +% \par The fault behind is, that we have no well error handling on one side and +% no sufficient formed equation solving on the other side. This two facts are +% making the implemention of new material very difficult. +% +% \subsection{Formalization of missing knowledge in Isabelle} +% +% \paragraph{A problem} behind is the mechanization of mathematic +% theories in TP-bases languages. There is still a huge gap between +% these algorithms and this what we want as a solution - in Example +% Signal Processing. +% +% \vbox{ +% \begin{example} +% \label{eg:gap} +% \[ +% X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY +% \] +% {\small\textit{ +% \noindent A very simple example on this what we call gap is the +% simplification above. It is needles to say that it is correct and also +% Isabelle for fills it correct - \emph{always}. But sometimes we don't +% want expand such terms, sometimes we want another structure of +% them. Think of a problem were we now would need only the coefficients +% of $X$ and $Y$. This is what we call the gap between mechanical +% simplification and the solution. +% }} +% \end{example} +% } +% +% \paragraph{We are not able to fill this gap,} until we have to live +% with it but first have a look on the meaning of this statement: +% Mechanized math starts from mathematical models and \emph{hopefully} +% proceeds to match physics. Academic engineering starts from physics +% (experimentation, measurement) and then proceeds to mathematical +% modeling and formalization. The process from a physical observance to +% a mathematical theory is unavoidable bound of setting up a big +% collection of standards, rules, definition but also exceptions. These +% are the things making mechanization that difficult. +% +% \vbox{ +% \begin{example} +% \label{eg:units} +% \[ +% m,\ kg,\ s,\ldots +% \] +% {\small\textit{ +% \noindent Think about some units like that one's above. Behind +% each unit there is a discerning and very accurate definition: One +% Meter is the distance the light travels, in a vacuum, through the time +% of 1 / 299.792.458 second; one kilogram is the weight of a +% platinum-iridium cylinder in paris; and so on. But are these +% definitions usable in a computer mechanized world?! +% }} +% \end{example} +% } +% +% \paragraph{A computer} or a TP-System builds on programs with +% predefined logical rules and does not know any mathematical trick +% (follow up example \ref{eg:trick}) or recipe to walk around difficult +% expressions. +% +% \vbox{ +% \begin{example} +% \label{eg:trick} +% \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] +% \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= +% \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] +% \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] +% {\small\textit{ +% \noindent Sometimes it is also useful to be able to apply some +% \emph{tricks} to get a beautiful and particularly meaningful result, +% which we are able to interpret. But as seen in this example it can be +% hard to find out what operations have to be done to transform a result +% into a meaningful one. +% }} +% \end{example} +% } +% +% \paragraph{The only possibility,} for such a system, is to work +% through its known definitions and stops if none of these +% fits. Specified on Signal Processing or any other application it is +% often possible to walk through by doing simple creases. This creases +% are in general based on simple math operational but the challenge is +% to teach the machine \emph{all}\footnote{Its pride to call it +% \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to +% reach a high level of \emph{all} but it in real it will still be a +% survey of knowledge which links to other knowledge and {{\sisac}{}} a +% trainer and helper but no human compensating calculator. +% \par +% {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal +% specifications of problems out of topics from Signal Processing, etc.) +% and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of +% physical knowledge. The result is a three-dimensional universe of +% mathematics seen in Figure~\ref{fig:mathuni}. +% +% \begin{figure} +% \begin{center} +% \includegraphics{fig/universe} +% \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is +% combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result +% leads to a three dimensional math universe.\label{fig:mathuni}} +% \end{center} +% \end{figure} +% +% %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen; +% %WN bitte folgende Bezeichnungen nehmen: +% %WN +% %WN axis 1: Algorithmic Knowledge (Programs) +% %WN axis 2: Application-oriented Knowledge (Specifications) +% %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems) +% %WN +% %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf +% %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz +% %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken) +% +% %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's +% %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's +% %JR gefordert werden WN2... +% %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann +% %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse +% %WN2 zusammenschneiden um die R"ander weg zu bekommen) +% %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und +% %WN2 png + pdf figures mitzuschicken. +% +% \subsection{Notes on Problems with Traditional Notation} +% +% \paragraph{During research} on these topic severely problems on +% traditional notations have been discovered. Some of them have been +% known in computer science for many years now and are still unsolved, +% one of them aggregates with the so called \emph{Lambda Calculus}, +% Example~\ref{eg:lamda} provides a look on the problem that embarrassed +% us. +% +% \vbox{ +% \begin{example} +% \label{eg:lamda} +% +% \[ f(x)=\ldots\; \quad R \rightarrow \quad R \] +% +% +% \[ f(p)=\ldots\; p \in \quad R \] +% +% {\small\textit{ +% \noindent Above we see two equations. The first equation aims to +% be a mapping of an function from the reel range to the reel one, but +% when we change only one letter we get the second equation which +% usually aims to insert a reel point $p$ into the reel function. In +% computer science now we have the problem to tell the machine (TP) the +% difference between this two notations. This Problem is called +% \emph{Lambda Calculus}. +% }} +% \end{example} +% } +% +% \paragraph{An other problem} is that terms are not full simplified in +% traditional notations, in {{\sisac}} we have to simplify them complete +% to check weather results are compatible or not. in e.g. the solutions +% of an second order linear equation is an rational in {{\sisac}} but in +% tradition we keep fractions as long as possible and as long as they +% aim to be \textit{beautiful} (1/8, 5/16,...). +% \subparagraph{The math} which should be mechanized in Computer Theorem +% Provers (\emph{TP}) has (almost) a problem with traditional notations +% (predicate calculus) for axioms, definitions, lemmas, theorems as a +% computer program or script is not able to interpret every Greek or +% Latin letter and every Greek, Latin or whatever calculations +% symbol. Also if we would be able to handle these symbols we still have +% a problem to interpret them at all. (Follow up \hbox{Example +% \ref{eg:symbint1}}) +% +% \vbox{ +% \begin{example} +% \label{eg:symbint1} +% \[ +% u\left[n\right] \ \ldots \ unitstep +% \] +% {\small\textit{ +% \noindent The unitstep is something we need to solve Signal +% Processing problem classes. But in {{{\sisac}{}}} the rectangular +% brackets have a different meaning. So we abuse them for our +% requirements. We get something which is not defined, but usable. The +% Result is syntax only without semantic. +% }} +% \end{example} +% } +% +% In different problems, symbols and letters have different meanings and +% ask for different ways to get through. (Follow up \hbox{Example +% \ref{eg:symbint2}}) +% +% \vbox{ +% \begin{example} +% \label{eg:symbint2} +% \[ +% \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent +% \] +% {\small\textit{ +% \noindent For using exponents the three \texttt{widehat} symbols +% are required. The reason for that is due the development of +% {{{\sisac}{}}} the single \texttt{widehat} and also the double were +% already in use for different operations. +% }} +% \end{example} +% } +% +% \paragraph{Also the output} can be a problem. We are familiar with a +% specified notations and style taught in university but a computer +% program has no knowledge of the form proved by a professor and the +% machines themselves also have not yet the possibilities to print every +% symbol (correct) Recent developments provide proofs in a human +% readable format but according to the fact that there is no money for +% good working formal editors yet, the style is one thing we have to +% live with. +% +% \section{Problems rising out of the Development Environment} +% +% fehlermeldungen! TODO + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim} + +\section{Summary and Conclusions}\label{conclusion} + +%JR obvious + +%This paper gives a first experience report about programming with a +%TP-based programming language. + +A brief re-introduction of the novel kind of programming +language by example of the {\sisac}-prototype makes the paper +self-contained. The main section describes all the main concepts +involved in TP-based programming and all the sub-tasks concerning +respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain +modeling, implementation of term rewriting systems for the +rewriting-engine, formal (implicit) specification of the problem to be +(explicitly) described by the program, implementation of the many components +required for Lucas-Interpretation and finally implementation of the +program itself. + +The many concepts and sub-tasks involved in programming require a +comprehensive work-flow; first experiences with the work-flow as +supported by the present prototype are described as well: Isabelle + +Isar + jEdit provide appropriate components for establishing an +efficient development environment integrating computation and +deduction. However, the present state of the prototype is far off a +state appropriate for wide-spread use: the prototype of the program +language lacks expressiveness and elegance, the prototype of the +development environment is hardly usable: error messages still address +the developer of the prototype's interpreter rather than the +application programmer, implementation of the many settings for the +Lucas-Interpreter is cumbersome. + +\subsection{Conclusions for Future Development} +From the above mentioned experiences a successful proof of concept can be concluded: +programming arbitrary problems from engineering sciences is possible, +in principle even in the prototype. Furthermore the experiences allow +to conclude detailed requirements for further development: +\begin{enumerate} +\item Clarify underlying logics such that programming is smoothly +integrated with verification of the program; the post-condition should +be proved more or less automatically, otherwise working engineers +would not encounter such programming. +\item Combine the prototype's programming language with Isabelle's +powerful function package and probably with more of SML's +pattern-matching features; include parallel execution on multi-core +machines into the language design. +\item Extend the prototype's Lucas-Interpreter such that it also +handles functions defined by use of Isabelle's functions package; and +generalize Isabelle's code generator such that efficient code for the +whole definition of the programming language can be generated (for +multi-core machines). +\item Develop an efficient development environment with +integration of programming and proving, with management not only of +Isabelle theories, but also of large collections of specifications and +of programs. +\item\label{CAS} Extend Isabelle's computational features in direction of +\textit{verfied} Computer Algebra: simplification extended by +algorithms beyond rewriting (cancellation of multivariate rationals, +factorisation, partial fraction decomposition, etc), equation solving +, integration, etc. +\end{enumerate} +Provided successful accomplishment, these points provide distinguished +components for virtual workbenches appealing to practitioners of +engineering in the near future. + +\subsection{Preview to Development of Course Material} +Interactive course material, as addressed by the title, +can comprise step-wise problem solving created as a side-effect of a +TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an +interactive programming environment, Lucas-Interpretation also can +provide TP-based services for a flexible dialogue component with +adaptive user guidance for independent and inquiry-based learning. + +However, the {\sisac} prototype is not ready for use in field-tests, +not only due to the above five requirements not sufficiently +accomplished, but also due to usability of the fron-end, in particular +the lack of an editor for formulas in 2-dimension representation. + +Nevertheless, the experiences from the case study described in this +paper, allow to give a preview to the development of course material, +if based on Lucas-Interpretation: + +\paragraph{Development of material from scratch} is too much effort +just for e-learning; this has become clear with the case study. For +getting support for stepwise problem solving just in {\em one} example +class, the one presented in this paper, involved the following tasks: +\begin{itemize} +\item Adapt the equation solver; since that was too laborous, the +program has been adapted in an unelegant way. +\item Implement an algorithms for partial fraction decomposition, +which is considered a standard normal form in Computer Algebra. +\item Implement a specification for partial fraction decomposition and +locate it appropriately in the hierarchy of specification. +\item Declare definitions and theorems within the theory of +${\cal Z}$-transform, and prove the theorems (which was not done in the +case study). +\end{itemize} +On the other hand, for the one the class of problems implemented, +adding an arbitrary number of examples within this class requires a +few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an +example is called from an HTML-file by an URL, which addresses an +XML-structure holding the respective data as shown on +p.\pageref{ml-check-program}.} and the support for individual stepwise +problem solving comes for free. + +\paragraph{E-learning benefits from Formal Domain Engineering} which can be +expected for various domains in the near future. In order to cope with +increasing complexity in domain of technology, specific domain +knowledge is beeing mechanised, not only for software technology +\footnote{For instance, the Archive of Formal Proofs +http://afp.sourceforge.net/} but also for other engineering domains +\cite{Dehbonei&94,Hansen94b,db:dom-eng}. This fairly new part of +engineering sciences is called ``domain engineering'' in +\cite{db:SW-engIII}. + +Given this kind of mechanised knowledge including mathematical +theories, domain specific definitions, specifications and algorithms, +theorems and proofs, then e-learning with support for individual +stepwise problem solving will not be much ado anymore; then e-learning +media in technology education can be derived from this knowledge with +reasonable effort. + +\paragraph{Development differentiates into tasks} more separated than +without Lucas-Interpretation and more challenginging in specific +expertise. These are the kinds of experts expected to cooperate in +development of +\begin{itemize} +\item ``Domain engineers'', who accomplish fairly novel tasks +described in this paper. +\item Course designers, who provide the instructional design according +to curricula, together with usability experts and media designers, are +indispensable in production of e-learning media at the state-of-the +art. +\item ``Dialog designers'', whose part of development is clearly +separated from the part of domain engineers as a consequence of +Lucas-Interpretation: TP-based programs are functional, as mentioned, +and are only concerned with describing mathematics --- and not at all +concerned with interaction, psychology, learning theory and the like, +because there are no in/output statements. Dialog designers can expect +a high-level rule-based language~\cite{gdaroczy-EP-13} for describing +their part. +\end{itemize} + +% response-to-referees: +% (2.1) details of novel technology in order to estimate the impact +% (2.2) which kinds of expertise are required for production of e-learning media (instructional design, math authoring, dialog authoring, media design) +% (2.3) what in particular is required for programming new exercises supported by next-step-guidance (expertise / efforts) +% (2.4) estimation of break-even points for development of next-step-guidance +% (2.5) usability of ISAC prototype at the present state +% +% 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."". + +\bigskip\noindent For this decade there seems to be a window of opportunity opening from +one side inreasing demand for formal domain engineering and from the +other side from TP more and more gaining industrial relevance. Within +this window, development of TP-based educational software can take +benefit from the fact, that the TPs leading in Europe, Coq~\cite{coq-team-10} and +Isabelle are still open source together with the major part of +mechanised knowledge.%~\footnote{NICTA}. + +\bibliographystyle{alpha} +{\small\bibliography{references}} + +\end{document} +% LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley +% LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised +% LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML +% LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls +% LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs +% LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq +% LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's +% LocalWords: mechanisation multi