diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex --- a/src/Doc/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Sep 16 12:27:20 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2135 +0,0 @@ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% 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