jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % Electronic Journal of Mathematics and Technology (eJMT) % jan@42463: % style sheet for LaTeX. Please do not modify sections % jan@42463: % or commands marked 'eJMT'. % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % eJMT commands % jan@42463: % % jan@42463: \documentclass[12pt,a4paper]{article}% % jan@42463: \usepackage{times} % jan@42463: \usepackage{amsfonts,amsmath,amssymb} % jan@42463: \usepackage[a4paper]{geometry} % jan@42463: \usepackage{fancyhdr} % jan@42463: \usepackage{color} % jan@42463: \usepackage[pdftex]{hyperref} % see note below % jan@42463: \usepackage{graphicx}% % jan@42463: \hypersetup{ % jan@42463: a4paper, % jan@42463: breaklinks % jan@42463: } % jan@42463: % % jan@42463: \newtheorem{theorem}{Theorem} % jan@42463: \newtheorem{acknowledgement}[theorem]{Acknowledgement} % jan@42463: \newtheorem{algorithm}[theorem]{Algorithm} % jan@42463: \newtheorem{axiom}[theorem]{Axiom} % jan@42463: \newtheorem{case}[theorem]{Case} % jan@42463: \newtheorem{claim}[theorem]{Claim} % jan@42463: \newtheorem{conclusion}[theorem]{Conclusion} % jan@42463: \newtheorem{condition}[theorem]{Condition} % jan@42463: \newtheorem{conjecture}[theorem]{Conjecture} % jan@42463: \newtheorem{corollary}[theorem]{Corollary} % jan@42463: \newtheorem{criterion}[theorem]{Criterion} % jan@42463: \newtheorem{definition}[theorem]{Definition} % jan@42463: \newtheorem{example}[theorem]{Example} % jan@42463: \newtheorem{exercise}[theorem]{Exercise} % jan@42463: \newtheorem{lemma}[theorem]{Lemma} % jan@42463: \newtheorem{notation}[theorem]{Notation} % jan@42463: \newtheorem{problem}[theorem]{Problem} % jan@42463: \newtheorem{proposition}[theorem]{Proposition} % jan@42463: \newtheorem{remark}[theorem]{Remark} % jan@42463: \newtheorem{solution}[theorem]{Solution} % jan@42463: \newtheorem{summary}[theorem]{Summary} % jan@42463: \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } % jan@42463: {\ \rule{0.5em}{0.5em}} % jan@42463: % % jan@42463: % eJMT page dimensions % jan@42463: % % jan@42463: \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} % jan@42463: % % jan@42463: % eJMT header & footer % jan@42463: % % jan@42463: \newcounter{ejmtFirstpage} % jan@42463: \setcounter{ejmtFirstpage}{1} % jan@42463: \pagestyle{empty} % jan@42463: \setlength{\headheight}{14pt} % jan@42463: \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} % jan@42463: \pagestyle{fancyplain} % jan@42463: \fancyhf{} % jan@42463: \fancyhead[c]{\small The Electronic Journal of Mathematics% jan@42463: \ and Technology, Volume 1, Number 1, ISSN 1933-2823} % jan@42463: \cfoot{% % jan@42463: \ifnum\value{ejmtFirstpage}=0% % jan@42463: {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% % jan@42463: \else\setcounter{ejmtFirstpage}{0}\fi% % jan@42463: } % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: % Please place your own definitions here jan@42463: % jan@42463: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} jan@42463: \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} jan@42463: jan@42463: \usepackage{color} jan@42463: \definecolor{lgray}{RGB}{238,238,238} jan@42463: jan@42463: % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % How to use hyperref % jan@42463: % ------------------- % jan@42463: % % jan@42463: % Probably the only way you will need to use the hyperref % jan@42463: % package is as follows. To make some text, say % jan@42463: % "My Text Link", into a link to the URL % jan@42463: % http://something.somewhere.com/mystuff, use % jan@42463: % % jan@42463: % \href{http://something.somewhere.com/mystuff}{My Text Link} jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: \begin{document} jan@42463: % jan@42463: % document title jan@42463: % neuper@42464: \title{Trials with TP-based Programming neuper@42464: \\ neuper@42464: for Interactive Course Material}% jan@42463: % jan@42463: % Single author. Please supply at least your name, jan@42463: % email address, and affiliation here. jan@42463: % jan@42463: \author{\begin{tabular}{c} jan@42463: \textit{Jan Ro\v{c}nik} \\ jan@42463: jan.rocnik@student.tugraz.at \\ jan@42463: IST, SPSC\\ neuper@42464: Graz University of Technologie\\ jan@42463: Austria\end{tabular} jan@42463: }% jan@42463: % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % eJMT commands - do not change these % jan@42463: % % jan@42463: \date{} % jan@42463: \maketitle % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: % abstract jan@42463: % jan@42463: \begin{abstract} jan@42463: jan@42463: Traditional course material in engineering disciplines lacks an jan@42463: important component, interactive support for step-wise problem neuper@42464: solving. Theorem-Proving (TP) technology is appropriate for one part jan@42463: of such support, in checking user-input. For the other part of such jan@42463: support, guiding the learner towards a solution, another kind of jan@42463: technology is required. %TODO ... connect to prototype ... jan@42463: jan@42463: A prototype combines TP with a programming language, the latter jan@42463: interpreted in a specific way: certain statements in a program, called jan@42463: tactics, are treated as breakpoints where control is handed over to jan@42463: the user. An input formula is checked by TP (using logical context jan@42463: built up by the interpreter); and if a learner gets stuck, a program jan@42463: describing the steps towards a solution of a problem ``knows the next jan@42463: step''. This kind of interpretation is called Lucas-Interpretation for jan@42463: \emph{TP-based programming languages}. jan@42463: jan@42463: This paper describes the prototype's TP-based programming language jan@42463: within a case study creating interactive material for an advanced jan@42463: course in Signal Processing: implementation of definitions and jan@42463: theorems in TP, formal specification of a problem and step-wise jan@42463: development of the program solving the problem. Experiences with the neuper@42464: ork flow in iterative development with testing and identifying errors jan@42463: are described, too. The description clarifies the components missing jan@42463: in the prototype's language as well as deficiencies experienced during jan@42463: programming. jan@42463: \par jan@42463: These experiences are particularly notable, because the author is the jan@42463: first programmer using the language beyond the core team which jan@42463: developed the prototype's TP-based language interpreter. jan@42463: % jan@42463: \end{abstract}% jan@42463: % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % eJMT command % jan@42463: % % jan@42463: \thispagestyle{fancy} % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: % Please use the following to indicate sections, subsections, jan@42463: % etc. Please also use \subsubsection{...}, \paragraph{...} jan@42463: % and \subparagraph{...} as necessary. jan@42463: % jan@42463: neuper@42464: \section{Introduction}\label{intro} jan@42463: jan@42466: % \paragraph{Didactics of mathematics} jan@42466: %WN: wenn man in einem high-quality paper von 'didactics' spricht, jan@42466: %WN muss man am state-of-the-art ankn"upfen -- siehe jan@42466: %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants neuper@42464: % faces a specific issue, a gap neuper@42464: % between (1) introduction of math concepts and skills and (2) neuper@42464: % application of these concepts and skills, which usually are separated neuper@42464: % into different units in curricula (for good reasons). For instance, neuper@42464: % (1) teaching partial fraction decomposition is separated from (2) neuper@42464: % application for inverse Z-transform in signal processing. neuper@42464: % neuper@42464: % \par This gap is an obstacle for applying math as an fundamental neuper@42464: % thinking technology in engineering: In (1) motivation is lacking neuper@42464: % because the question ``What is this stuff good for?'' cannot be neuper@42464: % treated sufficiently, and in (2) the ``stuff'' is not available to neuper@42464: % students in higher semesters as widespread experience shows. neuper@42464: % neuper@42464: % \paragraph{Motivation} taken by this didactic issue on the one hand, neuper@42464: % and ongoing research and development on a novel kind of educational neuper@42464: % mathematics assistant at Graz University of neuper@42464: % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to neuper@42464: % scope with this issue on the other hand, several institutes are neuper@42464: % planning to join their expertise: the Institute for Information neuper@42464: % Systems and Computer Media (IICM), the Institute for Software neuper@42464: % Technology (IST), the Institutes for Mathematics, the Institute for neuper@42464: % Signal Processing and Speech Communication (SPSC), the Institute for neuper@42464: % Structural Analysis and the Institute of Electrical Measurement and neuper@42464: % Measurement Signal Processing. jan@42466: %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell jan@42466: %WN und damit zu verg"anglich. neuper@42464: % \par This thesis is the first attempt to tackle the above mentioned neuper@42464: % issue, it focuses on Telematics, because these specific studies focus neuper@42464: % on mathematics in \emph{STEOP}, the introductory orientation phase in neuper@42464: % Austria. \emph{STEOP} is considered an opportunity to investigate the neuper@42464: % impact of {\sisac}'s prototype on the issue and others. neuper@42464: % jan@42466: jan@42502: Traditional course material in engineering disciplines lacks an neuper@42464: important component, interactive support for step-wise problem neuper@42464: solving. Theorem-Proving (TP) technology can provide such support by neuper@42464: specific services. An important part of such services is called neuper@42464: ``next-step-guidance'', generated by a specific kind of ``TP-based neuper@42464: programming language''. In the neuper@42464: {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such neuper@42464: a language is prototyped in line with~\cite{plmms10} and built upon neuper@42464: the theorem prover neuper@42464: Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}. neuper@42464: The TP services are coordinated by a specific interpreter for the neuper@42464: programming language, called neuper@42464: Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the neuper@42464: interpreter will be briefly re-introduced in order to make the paper neuper@42464: self-contained. jan@42463: jan@42502: \paragraph{The main part} of the paper is an account of first experiences neuper@42464: with programming in this TP-based language. The experience was gained neuper@42464: in a case study by the author. The author was considered an ideal neuper@42464: candidate for this study for the following reasons: as a student in neuper@42464: Telematics (computer science with focus on Signal Processing) he had neuper@42464: general knowledge in programming as well as specific domain knowledge neuper@42464: in Signal Processing; and he was not involved in the development of neuper@42464: {\sisac}'s programming language and interpeter, thus a novice to the neuper@42464: language. jan@42463: jan@42502: \paragraph{The goal} of the case study was (1) some TP-based programs for neuper@42464: interactive course material for a specific ``Adavanced Signal neuper@42464: Processing Lab'' in a higher semester, (2) respective program neuper@42464: development with as little advice from the {\sisac}-team and (3) records neuper@42464: and comments for the main steps of development in an Isabelle theory; neuper@42464: this theory should provide guidelines for future programmers. An neuper@42464: excerpt from this theory is the main part of this paper. jan@42466: \par jan@42466: The paper will use the problem in Fig.\ref{fig-interactive} as a jan@42463: running example: jan@42463: \begin{figure} [htb] jan@42463: \begin{center} neuper@42468: \includegraphics[width=140mm]{fig/isac-Ztrans-math-3} neuper@42468: %\includegraphics[width=140mm]{fig/isac-Ztrans-math} jan@42463: \caption{Step-wise problem solving guided by the TP-based program} jan@42463: \label{fig-interactive} jan@42463: \end{center} jan@42463: \end{figure} jan@42466: jan@42502: The problem is from the domain of Signal Processing and requests to neuper@42464: determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive} neuper@42464: also shows the beginning of the interactive construction of a solution neuper@42464: for the problem. This construction is done in the right window named neuper@42464: ``Worksheet''. jan@42466: \par neuper@42464: User-interaction on the Worksheet is {\em checked} and {\em guided} by neuper@42464: TP services: neuper@42464: \begin{enumerate} neuper@42464: \item Formulas input by the user are {\em checked} by TP: such a neuper@42464: formula establishes a proof situation --- the prover has to derive the neuper@42464: formula from the logical context. The context is built up from the neuper@42464: formal specification of the problem (here hidden from the user) by the neuper@42464: Lucas-Interpreter. neuper@42464: \item If the user gets stuck, the program developed below in this neuper@42464: paper ``knows the next step'' from behind the scenes. How the latter neuper@42464: TP-service is exploited by dialogue authoring is out of scope of this neuper@42464: paper and can be studied in~\cite{gdaroczy-EP-13}. neuper@42464: \end{enumerate} It should be noted that the programmer using the neuper@42464: TP-based language is not concerned with interaction at all; we will neuper@42464: see that the program contains neither input-statements nor neuper@42464: output-statements. Rather, interaction is handled by services neuper@42464: generated automatically. jan@42466: \par jan@42466: So there is a clear separation of concerns: Dialogues are neuper@42464: adapted by dialogue authors (in Java-based tools), using automatically neuper@42464: generated TP services, while the TP-based program is written by neuper@42464: mathematics experts (in Isabelle/ML). The latter is concern of this neuper@42464: paper. jan@42466: jan@42466: \paragraph{The paper is structed} as follows: The introduction neuper@42464: \S\ref{intro} is followed by a brief re-introduction of the TP-based neuper@42464: programming language in \S\ref{PL}, which extends the executable neuper@42464: fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which neuper@42464: play a specific role in Lucas-Interpretation and in providing the TP neuper@42464: services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes neuper@42464: the main steps in developing the program for the running example: neuper@42464: prepare domain knowledge, implement the formal specification of the neuper@42464: problem, prepare the environment for the program, implement the neuper@42464: program. The workflow of programming, debugging and testing is neuper@42464: described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will neuper@42464: give directions identified for future development. neuper@42464: jan@42463: jan@42463: \section{\isac's Prototype for a Programming Language}\label{PL} jan@42463: The prototype's language extends the executable fragment in the jan@42463: language of the theorem prover jan@42463: Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/} jan@42463: by tactics which have a specific role in Lucas-Interpretation. jan@42463: jan@42463: \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab} jan@42463: The executable fragment consists of data-type and function jan@42463: definitions. It's usability even suggests that fragment for jan@42463: introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic jan@42463: whose type system resembles that of functional programming jan@42463: languages. Thus there are jan@42463: \begin{description} jan@42463: \item[base types,] in particular \textit{bool}, the type of truth jan@42463: values, \textit{nat}, \textit{int}, \textit{complex}, and the types of jan@42463: natural, integer and complex numbers respectively in mathematics. jan@42463: \item[type constructors] allow to define arbitrary types, from jan@42463: \textit{set}, \textit{list} to advanced data-structures like jan@42463: \textit{trees}, red-black-trees etc. jan@42463: \item[function types,] denoted by $\Rightarrow$. jan@42463: \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide jan@42463: type polymorphism. Isabelle automatically computes the type of each jan@42463: variable in a term by use of Hindley-Milner type inference jan@42463: \cite{pl:hind97,Milner-78}. jan@42463: \end{description} jan@42463: jan@42463: \textbf{Terms} are formed as in functional programming by applying jan@42463: functions to arguments. If $f$ is a function of type jan@42463: $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then jan@42463: $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$ jan@42463: has type $\tau$. There are many predefined infix symbols like $+$ and jan@42463: $\leq$ most of which are overloaded for various types. jan@42463: jan@42463: HOL also supports some basic constructs from functional programming: jan@42463: {\it\label{isabelle-stmts} jan@42463: \begin{tabbing} 123\=\kill jan@42463: \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\ jan@42463: \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\ jan@42463: \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1 jan@42463: \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$ jan@42463: \end{tabbing} } neuper@42482: \noindent The running example's program uses some of these elements neuper@42482: (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt neuper@42482: let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program neuper@42482: is an Isabelle term with specific function constants like {\tt neuper@42482: program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt neuper@42482: Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12} neuper@42482: respectively. jan@42463: jan@42463: % Terms may also contain $\lambda$-abstractions. For example, $\lambda jan@42463: % x. \; x$ is the identity function. jan@42463: neuper@42467: %JR warum auskommentiert? WN2... neuper@42467: %WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb neuper@42467: %WN2 des Papers auftauchen m"usste; nachdem ich einen solchen neuper@42467: %WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht neuper@42467: %WN2 gel"oscht. neuper@42467: %WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen neuper@42467: %WN2 Platz f"ur Anderes weg. jan@42466: neuper@42464: \textbf{Formulae} are terms of type \textit{bool}. There are the basic jan@42463: constants \textit{True} and \textit{False} and the usual logical jan@42463: connectives (in decreasing order of precedence): $\neg, \land, \lor, jan@42463: \rightarrow$. jan@42463: neuper@42464: \textbf{Equality} is available in the form of the infix function $=$ neuper@42464: of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for neuper@42464: formulas, where it means ``if and only if''. jan@42463: jan@42463: \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \; jan@42463: P$. Quantifiers lead to non-executable functions, so functions do not jan@42463: always correspond to programs, for instance, if comprising \\$( jan@42463: \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2 jan@42463: \;)$. jan@42463: jan@42463: \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs} jan@42463: The prototype extends Isabelle's language by specific statements neuper@42464: called tactics~\footnote{{\sisac}'s tactics are different from jan@42463: Isabelle's tactics: the former concern steps in a calculation, the jan@42463: latter concern proof steps.} and tacticals. For the programmer these jan@42463: statements are functions with the following signatures: jan@42463: jan@42463: \begin{description} jan@42463: \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it jan@42463: term} * {\it term}\;{\it list}$: jan@42463: this tactic appplies {\it theorem} to a {\it term} yielding a {\it jan@42463: term} and a {\it term list}, the list are assumptions generated by jan@42463: conditional rewriting. For instance, the {\it theorem} jan@42463: $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$ jan@42463: applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields jan@42463: $(\frac{2}{3}, [x\not=0])$. jan@42463: jan@42463: \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term} * {\it term}\;{\it list}$: jan@42463: this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is jan@42463: a confluent and terminating term rewrite system, in general. If jan@42463: none of the rules ({\it theorem}s) is applicable on interpretation jan@42463: of this tactic, an exception is thrown. jan@42463: jan@42463: % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it jan@42463: % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it jan@42463: % list}$: jan@42463: % jan@42463: % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it jan@42463: % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it jan@42463: % list}$: jan@42463: jan@42463: \item[Substitute:] ${\it substitution}\Rightarrow{\it neuper@42482: term}\Rightarrow{\it term}$: allows to access sub-terms. jan@42463: jan@42463: \item[Take:] ${\it term}\Rightarrow{\it term}$: jan@42463: this tactic has no effect in the program; but it creates a side-effect jan@42463: by Lucas-Interpretation (see below) and writes {\it term} to the jan@42463: Worksheet. jan@42463: jan@42463: \item[Subproblem:] ${\it theory} * {\it specification} * {\it jan@42463: method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$: neuper@42482: this tactic is a generalisation of a function call: it takes an neuper@42482: \textit{argument list} as usual, and additionally a triple consisting neuper@42482: of an Isabelle \textit{theory}, an implicit \textit{specification} of the neuper@42482: program and a \textit{method} containing data for Lucas-Interpretation, neuper@42482: last not least a program (as an explicit specification)~\footnote{In neuper@42482: interactive tutoring these three items can be determined explicitly neuper@42482: by the user.}. jan@42463: \end{description} jan@42463: The tactics play a specific role in jan@42463: Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as neuper@42482: break-points where, as a side-effect, a line is added to a calculation neuper@42483: as a protocol for proceeding towards a solution in step-wise problem neuper@42483: solving. At the same points Lucas-Interpretation serves interactive neuper@42483: tutoring and control is handed over to the user. The user is free to neuper@42483: investigate underlying knowledge, applicable theorems, etc. And the neuper@42483: user can proceed constructing a solution by input of a tactic to be neuper@42483: applied or by input of a formula; in the latter case the jan@42463: Lucas-Interpreter has built up a logical context (initialised with the jan@42463: precondition of the formal specification) such that Isabelle can jan@42463: derive the formula from this context --- or give feedback, that no jan@42463: derivation can be found. jan@42463: neuper@42496: \subsection{Tacticals as Control Flow Statements} jan@42463: The flow of control in a program can be determined by {\tt if then else} jan@42463: and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also jan@42463: by additional tacticals: jan@42463: \begin{description} jan@42463: \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it jan@42463: term}$: iterates over tactics which take a {\it term} as argument as neuper@42482: long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might jan@42463: not be applicable). jan@42463: jan@42463: \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$: jan@42463: if {\it tactic} is applicable, then it is applied to {\it term}, neuper@42483: otherwise {\it term} is passed on without changes. jan@42463: jan@42463: \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it neuper@42483: term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable, neuper@42483: it is applied to the first {\it term} yielding another {\it term}, neuper@42483: otherwise the second {\it tactic} is applied; if none is applicable an neuper@42483: exception is raised. jan@42463: jan@42463: \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it neuper@42483: term}\Rightarrow{\it term}$: applies the first {\it tactic} to the neuper@42483: first {\it term} yielding an intermediate term (not appearing in the neuper@42483: signature) to which the second {\it tactic} is applied. jan@42463: jan@42463: \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it neuper@42483: term}\Rightarrow{\it term}$: if the first {\it term} is true, then the neuper@42483: {\it tactic} is applied to the first {\it term} yielding an neuper@42483: intermediate term (not appearing in the signature); the intermediate neuper@42483: term is added to the environment the first {\it term} is evaluated in neuper@42483: etc as long as the first {\it term} is true. jan@42463: \end{description} neuper@42483: The tacticals are not treated as break-points by Lucas-Interpretation neuper@42483: and thus do not contribute to the calculation nor to interaction. jan@42463: neuper@42498: \section{Concepts and Tasks in TP-based Programming}\label{trial} neuper@42498: %\section{Development of a Program on Trial} neuper@42498: neuper@42498: This section presents all the concepts involved in TP-based neuper@42498: programming and all the tasks to be accomplished by programmers. The neuper@42498: presentation uses the running example which has been introduced in neuper@42498: Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. jan@42466: jan@42466: \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac} jan@42466: neuper@42467: %WN was Fachleute unter obigem Titel interessiert findet sich jan@42466: %WN unterhalb des auskommentierten Textes. jan@42466: jan@42466: %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell jan@42466: %WN auf Computer-Mathematiker fokussiert. neuper@42464: % \paragraph{As mentioned in the introduction,} a prototype of an neuper@42464: % educational math assistant called neuper@42464: % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for neuper@42464: % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges neuper@42464: % the gap between (1) introducation and (2) application of mathematics: neuper@42464: % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which neuper@42464: % requires each fact and each action justified by formal logic, so neuper@42464: % {{{\sisac}{}}} makes justifications transparent to students in neuper@42464: % interactive step-wise problem solving. By that way {{\sisac}} already neuper@42464: % can serve both: neuper@42464: % \begin{enumerate} neuper@42464: % \item Introduction of math stuff (in e.g. partial fraction neuper@42464: % decomposition) by stepwise explaining and exercising respective neuper@42464: % symbolic calculations with ``next step guidance (NSG)'' and rigorously neuper@42464: % checking steps freely input by students --- this also in context with neuper@42464: % advanced applications (where the stuff to be taught in higher neuper@42464: % semesters can be skimmed through by NSG), and neuper@42464: % \item Application of math stuff in advanced engineering courses neuper@42464: % (e.g. problems to be solved by inverse Z-transform in a Signal neuper@42464: % Processing Lab) and now without much ado about basic math techniques neuper@42464: % (like partial fraction decomposition): ``next step guidance'' supports neuper@42464: % students in independently (re-)adopting such techniques. neuper@42464: % \end{enumerate} neuper@42464: % Before the question is answers, how {{\sisac}} neuper@42464: % accomplishes this task from a technical point of view, some remarks on neuper@42464: % the state-of-the-art is given, therefor follow up Section~\ref{emas}. neuper@42464: % neuper@42464: % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} neuper@42464: % jan@42466: % \paragraph{Educational software in mathematics} is, if at all, based jan@42466: % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry jan@42466: % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org} jan@42466: % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC jan@42466: % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These jan@42466: % base technologies are used to program math lessons and sometimes even jan@42466: % exercises. The latter are cumbersome: the steps towards a solution of jan@42466: % such an interactive exercise need to be provided with feedback, where jan@42466: % at each step a wide variety of possible input has to be foreseen by jan@42466: % the programmer - so such interactive exercises either require high neuper@42464: % development efforts or the exercises constrain possible inputs. neuper@42464: % jan@42466: % \subparagraph{A new generation} of educational math assistants (EMAs) jan@42466: % is emerging presently, which is based on Theorem Proving (TP). TP, for jan@42466: % instance Isabelle and Coq, is a technology which requires each fact jan@42466: % and each action justified by formal logic. Pushed by demands for jan@42466: % \textit{proven} correctness of safety-critical software TP advances jan@42466: % into software engineering; from these advancements computer jan@42466: % mathematics benefits in general, and math education in particular. Two neuper@42464: % features of TP are immediately beneficial for learning: neuper@42464: % jan@42466: % \paragraph{TP have knowledge in human readable format,} that is in jan@42466: % standard predicate calculus. TP following the LCF-tradition have that jan@42466: % knowledge down to the basic definitions of set, equality, jan@42466: % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; jan@42466: % following the typical deductive development of math, natural numbers jan@42466: % are defined and their properties jan@42466: % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, jan@42466: % etc. Present knowledge mechanized in TP exceeds high-school jan@42466: % mathematics by far, however by knowledge required in software neuper@42464: % technology, and not in other engineering sciences. neuper@42464: % jan@42466: % \paragraph{TP can model the whole problem solving process} in jan@42466: % mathematical problem solving {\em within} a coherent logical jan@42466: % framework. This is already being done by three projects, by neuper@42464: % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor. neuper@42464: % \par jan@42466: % Having the whole problem solving process within a logical coherent jan@42466: % system, such a design guarantees correctness of intermediate steps and jan@42466: % of the result (which seems essential for math software); and the jan@42466: % second advantage is that TP provides a wealth of theories which can be jan@42466: % exploited for mechanizing other features essential for educational neuper@42464: % software. neuper@42464: % neuper@42464: % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid} neuper@42464: % jan@42466: % One essential feature for educational software is feedback to user neuper@42464: % input and assistance in coming to a solution. neuper@42464: % jan@42466: % \paragraph{Checking user input} by ATP during stepwise problem solving jan@42466: % is being accomplished by the three projects mentioned above jan@42466: % exclusively. They model the whole problem solving process as mentioned jan@42466: % above, so all what happens between formalized assumptions (or formal jan@42466: % specification) and goal (or fulfilled postcondition) can be jan@42466: % mechanized. Such mechanization promises to greatly extend the scope of neuper@42464: % educational software in stepwise problem solving. neuper@42464: % jan@42466: % \paragraph{NSG (Next step guidance)} comprises the system's ability to jan@42466: % propose a next step; this is a challenge for TP: either a radical jan@42466: % restriction of the search space by restriction to very specific jan@42466: % problem classes is required, or much care and effort is required in jan@42466: % designing possible variants in the process of problem solving neuper@42464: % \cite{proof-strategies-11}. neuper@42464: % \par jan@42466: % Another approach is restricted to problem solving in engineering jan@42466: % domains, where a problem is specified by input, precondition, output jan@42466: % and postcondition, and where the postcondition is proven by ATP behind jan@42466: % the scenes: Here the possible variants in the process of problem jan@42466: % solving are provided with feedback {\em automatically}, if the problem jan@42466: % is described in a TP-based programing language: \cite{plmms10} the jan@42466: % programmer only describes the math algorithm without caring about jan@42466: % interaction (the respective program is functional and even has no jan@42466: % input or output statements!); interaction is generated as a jan@42466: % side-effect by the interpreter --- an efficient separation of concern jan@42466: % between math programmers and dialog designers promising application neuper@42464: % all over engineering disciplines. neuper@42464: % neuper@42464: % neuper@42464: % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}} jan@42466: % Authoring new mathematics knowledge in {{\sisac}} can be compared with jan@42466: % ``application programing'' of engineering problems; most of such jan@42466: % programing uses CAS-based programing languages (CAS = Computer Algebra neuper@42464: % Systems; e.g. Mathematica's or Maple's programing language). neuper@42464: % jan@42466: % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}} jan@42466: % \cite{plmms10} for describing how to construct a solution to an jan@42466: % engineering problem and for calling equation solvers, integration, jan@42466: % etc~\footnote{Implementation of CAS-like functionality in TP is not jan@42466: % primarily concerned with efficiency, but with a didactic question: jan@42466: % What to decide for: for high-brow algorithms at the state-of-the-art jan@42466: % or for elementary algorithms comprehensible for students?} within TP; jan@42466: % TP can ensure ``systems that never make a mistake'' \cite{casproto} - neuper@42464: % are impossible for CAS which have no logics underlying. neuper@42464: % jan@42466: % \subparagraph{Authoring is perfect} by writing such TP based programs; jan@42466: % the application programmer is not concerned with interaction or with jan@42466: % user guidance: this is concern of a novel kind of program interpreter jan@42466: % called Lucas-Interpreter. This interpreter hands over control to a jan@42466: % dialog component at each step of calculation (like a debugger at jan@42466: % breakpoints) and calls automated TP to check user input following neuper@42464: % personalized strategies according to a feedback module. neuper@42464: % \par jan@42466: % However ``application programing with TP'' is not done with writing a jan@42466: % program: according to the principles of TP, each step must be jan@42466: % justified. Such justifications are given by theorems. So all steps jan@42466: % must be related to some theorem, if there is no such theorem it must jan@42466: % be added to the existing knowledge, which is organized in so-called jan@42466: % \textbf{theories} in Isabelle. A theorem must be proven; fortunately jan@42466: % Isabelle comprises a mechanism (called ``axiomatization''), which jan@42466: % allows to omit proofs. Such a theorem is shown in neuper@42464: % Example~\ref{eg:neuper1}. jan@42466: neuper@42498: The running example requires to determine the inverse $\cal jan@42466: Z$-transform for a class of functions. The domain of Signal Processing jan@42466: is accustomed to specific notation for the resulting functions, which jan@42466: are absolutely summable and are called TODO: $u[n]$, where $u$ is the jan@42466: function, $n$ is the argument and the brackets indicate that the jan@42466: arguments are TODO. Surprisingly, Isabelle accepts the rules for jan@42466: ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle jan@42466: experts might be particularly surprised, that the brackets do not jan@42466: cause errors in typing (as lists).}: neuper@42464: %\vbox{ neuper@42464: % \begin{example} jan@42463: \label{eg:neuper1} jan@42463: {\small\begin{tabbing} jan@42463: 123\=123\=123\=123\=\kill jan@42463: \hfill \\ jan@42463: \>axiomatization where \\ neuper@42464: \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\ neuper@42464: \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\ jan@42466: \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\ jan@42466: %TODO jan@42466: \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\ jan@42466: %TODO jan@42466: \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\ jan@42466: %TODO jan@42466: \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\ jan@42466: %TODO jan@42463: \end{tabbing} jan@42463: } neuper@42464: % \end{example} jan@42466: %} jan@42466: These 6 rules can be used as conditional rewrite rules, depending on jan@42466: the respective convergence radius. Satisfaction from accordance with traditional notation jan@42466: contrasts with the above word {\em axiomatization}: As TP-based, the jan@42466: programming language expects these rules as {\em proved} theorems, and jan@42466: not as axioms implemented in the above brute force manner; otherwise jan@42466: all the verification efforts envisaged (like proof of the jan@42466: post-condition, see below) would be meaningless. jan@42466: jan@42466: Isabelle provides a large body of knowledge, rigorously proven from jan@42466: the basic axioms of mathematics~\footnote{This way of rigorously jan@42466: deriving all knowledge from first principles is called the jan@42466: LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced jan@42466: knowledge can be found in the theoris on Multivariate jan@42466: Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However, jan@42466: building up knowledge such that a proof for the above rules would be jan@42466: reasonably short and easily comprehensible, still requires lots of jan@42466: work (and is definitely out of scope of our case study). jan@42466: neuper@42487: At the state-of-the-art in mechanization of knowledge in engineering neuper@42487: sciences, the process does not stop with the mechanization of neuper@42487: mathematics traditionally used in these sciences. Rather, ``Formal neuper@42487: Methods''~\cite{ fm-03} are expected to proceed to formal and explicit neuper@42487: description of physical items. Signal Processing, for instance is neuper@42487: concerned with physical devices for signal acquisition and neuper@42487: reconstruction, which involve measuring a physical signal, storing it, neuper@42487: and possibly later rebuilding the original signal or an approximation neuper@42487: thereof. For digital systems, this typically includes sampling and neuper@42487: quantization; devices for signal compression, including audio neuper@42487: compression, image compression, and video compression, etc. ``Domain neuper@42487: engineering''\cite{db:dom-eng} is concerned with {\em specification} neuper@42487: of these devices' components and features; this part in the process of neuper@42487: mechanization is only at the beginning in domains like Signal neuper@42487: Processing. jan@42466: neuper@42487: TP-based programming, concern of this paper, is determined to jan@42466: add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on jan@42466: p.\pageref{fig:mathuni}. As we shall see below, TP-based programming jan@42466: starts with a formal {\em specification} of the problem to be solved. neuper@42478: \begin{figure} neuper@42478: \begin{center} jan@42500: \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small} neuper@42487: \caption{The three-dimensional universe of mathematics knowledge} neuper@42478: \label{fig:mathuni} neuper@42478: \end{center} neuper@42478: \end{figure} neuper@42487: The language for both axes is defined in the axis at the bottom, deductive neuper@42487: knowledge, in {\sisac} represented by Isabelle's theories. jan@42466: jan@42466: \subsection{Preparation of Simplifiers for the Program}\label{simp} jan@42469: jan@42505: All evaluation in the prototyp's Lucas-Interpreter is done by term rewriting on jan@42505: Isabelle's terms, see \S\ref{math} below; in this section some of respective jan@42505: preparations are described. In order to work reliably with term rewriting, the jan@42505: respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that}, jan@42505: then they are called (canonical) simplifiers. These properties do not go without jan@42505: saying, their establishment is a difficult task for the programmer; this task is jan@42505: not yet supported in the prototype.\par jan@42502: jan@42505: % If it is clear how the later calculation should look like jan@42505: % %WN3 ... Allgem.<-->Konkret ist gut: aber hier ist 'calculation' jan@42505: % %WN3 zu weit weg: der Satz geh"ort bestenfalls gleich an den jan@42505: % %WN3 Anfang von \sect.3 jan@42505: % %WN3 jan@42505: % %WN3 Im Folgenden sind einige Ungenauigkeiten: jan@42505: % and when jan@42505: % which mathematic rule jan@42505: % %WN3 rewrite-rule oder theorem ! Ein Paper enth"alt viele Begriffe jan@42505: % %WN3 und man versucht, die Anzahl so gering wie m"oglich zu halten jan@42505: % %WN3 und die verbleibenden so pr"azise zu definieren wie m"oglich; jan@42505: % %WN3 das Vermeiden von Wiederholungen muss mit anderen Mitteln erfolgen, jan@42505: % %WN3 als dieselbe Sache mit verschiedenen Namen zu benennen; jan@42505: % %WN3 das gilt insbesonders f"ur technische Begriffe wie oben jan@42505: % should be applied, it can be started to find ways of jan@42505: % simplifications. jan@42505: % %WN3 ... zu allgemein. Das Folgende w"urde durch einen Verweis in jan@42505: % %WN3 das Programm auf S.12 gewinnen. jan@42505: % This includes in e.g. the simplification of reational jan@42505: % expressions or also rewrites of an expession. jan@42505: % \par jan@42505: % %WN3 das Folgende habe ich aus dem Beispielprogramm auf S.12 jan@42505: % %WN3 gestrichen, weil es aus prinzipiellen Gr"unden unsch"on ist. jan@42505: % %WN3 Und es ist so kompliziert dass es mehr Platz zum Erkl"aren jan@42505: % %WN3 braucht, als es wert ist ... jan@42505: % Obligate is the use of the function \texttt{drop\_questionmarks} jan@42505: % which excludes irrelevant symbols out of the expression. (Irrelevant symbols may jan@42505: % be result out of the system during the calculation. The function has to be jan@42505: % applied for two reasons. First two make every placeholder in a expression jan@42505: % useable as a constant and second to provide a better view at the frontend.) jan@42505: % \par jan@42505: % %WN3 Da kommt eine ganze Reihe von Ungenauigkeiten: jan@42505: % Most rewrites are represented through rulesets jan@42505: % %WN3 ... das ist schlicht falsch: jan@42505: % %WN3 _alle_ rewrites werden durch rule-sets erzeugt (per definition jan@42505: % %WN3 dieser W"orter). jan@42505: % this jan@42505: % rulesets tell the machine which terms have to be rewritten into which jan@42505: % representation. jan@42505: % %WN3 ... ist ein besonders "uberzeugendes Beispiel von Allgem.<-->Konkret: jan@42505: % %WN3 so allgemein, wie es hier steht, ist es jan@42505: % %WN3 # f"ur einen Fachmann klar und nicht ganz fachgem"ass formuliert jan@42505: % %WN3 (a rule-set rewrites a certain term into another with certain properties) jan@42505: % %WN3 # f"ur einen Nicht-Fachmann trotz allem unverst"andlich. jan@42505: % %WN3 jan@42505: % %WN3 Wenn schon allgemeine S"atze, dann unmittelbar auf das Beispiel jan@42505: % %WN3 unten verweisen, jan@42505: % %WN3 oder besser: den Satz dorthin schreiben, wo er unmittelbar vom jan@42505: % %WN3 Beispiel gefolgt wird. jan@42505: % In the upcoming programm a rewrite can be applied only in using jan@42505: % such rulesets on existing terms. jan@42505: % %WN3 Du willst wohl soetwas sagen wie ... jan@42505: % %WN3 rewriting is the main concept to step-wise create and transform jan@42505: % %WN3 formulas in order to proceed towards a solution of a problem jan@42505: % %WN3 ...? jan@42505: % \paragraph{The core} of our implemented problem is the Z-Transformation jan@42505: % %WN3 ^^^^^ ist nicht gut: was soll THE CORE vermitteln, wenn man die jan@42505: % %WN3 Seite "uberfliegt ? Dass hier das Zentrum Deiner Arbeit liegt ? jan@42505: % %WN3 jan@42505: % %WN3 Das Folgende ist eine allgemeine Design-"Uberlegung, die entweder jan@42505: % %WN3 vorne zur Einf"uhrung des Beispiels geh"ort, jan@42505: % %WN3 oder zur konkreten L"osung durch die Rechnung auf S.15/16. jan@42505: % (remember the description of the running example, introduced by jan@42505: % Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the jan@42505: % 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 jan@42505: % transformation tables). jan@42505: % \par jan@42505: % %WN3 Zum Folgenden: 'axiomatization' ist schon in 3.1. angesprochen: jan@42505: % %WN3 entweder dort erg"anzen, wenn's wichtig ist, oder weglassen. jan@42505: % Rules, in {\sisac{}}'s programming language can be designed by the use of jan@42505: % axiomatization. In this axiomatization we declare how a term has to look like jan@42505: % (left side) to be rewritten into another form (right side). Every line of this jan@42505: % axiomatizations starts with the name of the rule. jan@42505: jan@42505: The prototype rewrites using theorems only. Axioms which are theorems as well jan@42505: have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we jan@42505: assemble them in a rule-set and apply them as follows: jan@42505: jan@42505: % %WN3 Die folgenden Zeilen nehmen Platz weg: von hier auf S.6 verweisen jan@42505: % %\begin{example} jan@42505: % {\footnotesize jan@42505: % \label{eg:ruledef} jan@42505: % % \hfill\\ jan@42505: % \begin{verbatim} jan@42505: % axiomatization where jan@42505: % rule1: ``1 = $\delta$[n]'' and jan@42505: % rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and jan@42505: % rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]'' jan@42505: % \end{verbatim} jan@42505: % %\end{example} jan@42505: % } jan@42505: jan@42505: % Rules can be summarized in a ruleset (collection of rules) and afterwards tried % to be applied to a given expression as puttet over in following code. neuper@42503: %WN3 ... ist schon mehrmals gesagt worden. 1-mal pr"azise sagen gen"ugt. neuper@42503: %WN3 neuper@42503: %WN3 mit dem append_rls unten verbirgst Du die ganze Komplexit"at von neuper@42503: %WN3 rule-sets --- ich w"urde diese hier ausbreiten, damit man die neuper@42503: %WN3 Schwierigkeit von TP-based programming ermessen kann. neuper@42503: %WN3 Eine Erkl"arung wie in 3.4 und 3.5 braucht viel Platz, der sich neuper@42503: %WN3 meines Erachtens mehr auszahlt als die allgemeinen S"atze neuper@42503: %WN3 am Ende von 3.2 auf S.8. neuper@42503: %WN3 neuper@42503: %WN3 mache ein 'grep -r "and rls"; neuper@42503: %WN3 auch in Build_Inverse_Z_Transform.thy hast Du 'Rls' jan@42475: jan@42494: %\begin{example} jan@42502: % \hfill\\ jan@42505: jan@42489: \label{eg:ruleapp} jan@42489: \begin{enumerate} jan@42502: jan@42489: \item Store rules in ruleset: jan@42502: {\footnotesize\begin{verbatim} jan@42505: 01 val inverse_Z = append_rls "inverse_Z" e_rls jan@42505: 02 [ Thm ("rule1",num_str @{thm rule1}), jan@42505: 03 Thm ("rule2",num_str @{thm rule2}), jan@42505: 04 Thm ("rule3",num_str @{thm rule3}) jan@42505: 05 ];\end{verbatim}} jan@42502: jan@42489: \item Define exression: jan@42502: {\footnotesize\begin{verbatim} jan@42505: 06 val sample_term = str2term "z/(z-1)+z/(z-)+1";\end{verbatim}} jan@42505: jan@42505: neuper@42503: %WN3 vergleiche bitte obige Zeile mit den letzten 3 Zeilen aus S.8, neuper@42503: %WN3 diese entsprechen dem g"angigen functional-programming Stil. jan@42505: jan@42505: jan@42505: jan@42505: neuper@42503: %WN3 Super w"ar's, wenn Du hier schon die interne Darstellung von neuper@42503: %WN3 Isabelle Termen zeigen k"onntest, dann w"urde ich den entsprechenden Teil neuper@42503: %WN3 am Ende von S.8 und Anfang S.9 (erste 2.1 Zeilen) l"oschen. jan@42502: jan@42505: %JR ich habe einige male über seite acht gelesen, finde aber dass der teil über jan@42505: %JR die interne representation dorthin besser passt da diese in unserem jan@42505: %JR gezeigten beispiel ja in direkter verbindung zur gezeigtem funktion besteht jan@42505: %JR und so der übergang exzellent ist. jan@42505: jan@42489: \item Apply ruleset: jan@42502: {\footnotesize\begin{verbatim} jan@42505: 07 val SOME (sample_term', asm) = jan@42505: 08 rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}} jan@42502: jan@42489: \end{enumerate} jan@42494: %\end{example} jan@42489: neuper@42503: %WN3 Wie oben gesagt, die folgenden allgemeinen S"atze scheinen neuper@42503: %WN3 weniger wert als eine konkrete Beschreibung der rls-Struktur. neuper@42503: %WN3 neuper@42503: %WN3 Ich nehme an, wir l"oschen das Folgende neuper@42503: %WN3 und ich spare mir Kommentare (ausser Du hast noch Zeit/Energie neuper@42503: %WN3 daf"ur und fragst extra nach). jan@42505: jan@42505: % The use of rulesets makes it much easier to develop our designated applications, jan@42505: % but the programmer has to be careful and patient. When applying rulesets jan@42505: % two important issues have to be mentionend: jan@42505: % \begin{enumerate} jan@42505: % \item How often the rules have to be applied? In case of jan@42505: % transformations it is quite clear that we use them once but other fields jan@42505: % reuqire to apply rules until a special condition is reached (e.g. jan@42505: % a simplification is finished when there is nothing to be done left). jan@42505: % \item The order in which rules are applied often takes a big effect jan@42505: % and has to be evaluated for each purpose once again. jan@42505: % \end{enumerate} jan@42505: % In the special case of Signal Processing the rules defined in the jan@42505: % Example upwards have to be applied in a dedicated order to transform all jan@42505: % constants first of all. After this first transformation step has been done it no jan@42505: % mather which rule fit's next. jan@42505: neuper@42503: %WN3 Beim Paper-Schreiben ist mir aufgefallen, dass eine Konstante ZZ_1 neuper@42503: %WN3 (f"ur ${\cal Z}^{-1}$) die eben beschriebenen Probleme gel"ost neuper@42503: %WN3 h"atte: auf S.6 in rule1, auf S.12 in line 10 und in der Rechnung S.16 neuper@42503: %WN3 hab' ich die Konstante schon eingef"uhrt. neuper@42503: %WN3 neuper@42503: %WN3 Bite bei der rewrite_set_ demo oben bitte schummeln ! jan@42469: jan@42505: %JR TODO es is klein z bitte auf S.6 in rule1, auf S.12 in line 10 ausbessern jan@42505: %JR ${\cal z}^{-1}$ jan@42505: jan@42505: jan@42505: In the first step of upper code we extend the method's own ruleset with jan@42505: the predefined rules.\par jan@42505: When adding rules to this set we already have to take care on the order the jan@42505: rules we be applied in later context, this can be an important point when it jan@42505: comes to a case where one rule has to be applied explicite before an other. jan@42505: \par Rules are added to the ruleset with an unique name and a reference to their jan@42505: defined theorem. After summerizing this rules we still have the posibility to jan@42505: pick out a single one. jan@42505: \par In upper example we define an expression, as it comes up in our running jan@42505: example, it can be useful to take a look at \S\ref{funs} on p.\pageref{funs} to jan@42505: get to know {\sisac}'s' internal representation of variables. jan@42505: \par Upper step three is the final use of a ruleset for rewriting expression. jan@42505: The inline declared \ttfamily sample\_term' \normalfont is the result of applying the upper jan@42505: rule set one time to the before defined \texttt{sample\_term'}. jan@42505: jan@42505: jan@42466: \subsection{Preparation of ML-Functions}\label{funs} neuper@42498: The prototype's Lucas-Interpreter uses the {\sisac}-rewrite-engine for neuper@42498: all kinds of evaluation. Some functionality required in programming, neuper@42498: however, cannot be accomplished by rewriting. So the prototype has a neuper@42498: mechanism to call ML-functions during rewriting, and the programmer has neuper@42498: to use this mechanism. jan@42469: neuper@42498: In the running example's program on p.\pageref{s:impl} the lines {\rm neuper@42498: 05} and {\rm 06} contain such functions; we go into the details with neuper@42498: \textit{argument\_in X\_z;}. This function fetches the argument from a neuper@42498: function application: Line {\rm 03} in the example calculation on neuper@42498: p.\pageref{exp-calc} is created by line {\rm 06} of the example neuper@42498: program on p.\pageref{s:impl} where the program's environment assigns neuper@42498: the value \textit{X z} to the variable \textit{X\_z}; so the function neuper@42498: shall extract the argument \textit{z}. jan@42469: neuper@42498: \medskip In order to be recognised as a function constant in the neuper@42499: program source the constant needs to be declared in a theory, here in neuper@42498: \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in neuper@42498: the context \textit{ctxt} of that theory: neuper@42498: {\footnotesize neuper@42498: \begin{verbatim} neuper@42498: consts neuper@42498: argument'_in :: "real => real" ("argument'_in _" 10) neuper@42498: neuper@42498: ML {* val SOME t = parse ctxt "argument_in (X z)"; *} jan@42473: neuper@42498: val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real") neuper@42498: $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term neuper@42498: \end{verbatim}} jan@42469: neuper@42498: \noindent Parsing produces a term \texttt{t} in internal neuper@42499: representation~\footnote{The attentive reader realizes the delicate neuper@42499: differences between interal and extermal representation even in the neuper@42499: strings, i.e \texttt{'\_}}, consisting of \texttt{Const neuper@42499: ("argument'\_in", type)} and the two variables \texttt{Free ("X", neuper@42499: type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term neuper@42499: constructor. The function body below is implemented directly in ML, neuper@42499: i.e in an \texttt{ML \{* *\}} block; the function definition provides neuper@42499: a unique prefix \texttt{eval\_} to the function name: jan@42473: neuper@42498: {\footnotesize jan@42470: \begin{verbatim} neuper@42498: ML {* neuper@42498: fun eval_argument_in _ neuper@42498: "Build_Inverse_Z_Transform.argument'_in" neuper@42498: (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ = neuper@42498: if is_Free arg (*could be something to be simplified before*) neuper@42498: then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg))) neuper@42498: else NONE neuper@42498: | eval_argument_in _ _ _ _ = NONE; neuper@42498: *} neuper@42498: \end{verbatim}} jan@42469: neuper@42498: \noindent The function body creates either creates \texttt{NONE} neuper@42498: telling the rewrite-engine to search for the next redex, or creates an neuper@42498: ad-hoc theorem for rewriting, thus the programmer needs to adopt many neuper@42498: technicalities of Isabelle, for instance, the \textit{Trueprop} neuper@42498: constant. jan@42469: neuper@42498: \bigskip This sub-task particularly sheds light on basic issues in the neuper@42498: design of a programming language, the integration of diffent language neuper@42498: layers, the layer of Isabelle/Isar and Isabelle/ML. jan@42469: neuper@42498: Another point of improvement for the prototype is the rewrite-engine: The neuper@42498: program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05} neuper@42498: and {\rm 06} to jan@42469: neuper@42498: {\small\it\label{s:impl} neuper@42498: \begin{tabbing} neuper@42498: 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill neuper@42498: \>{\rm 05/6}\>\>\> (z::real) = argument\_in (lhs X\_eq) ; neuper@42498: \end{tabbing}} jan@42469: neuper@42498: \noindent because nested function calls would require creating redexes neuper@42498: inside-out; however, the prototype's rewrite-engine only works top down neuper@42498: from the root of a term down to the leaves. jan@42469: neuper@42498: How all these ugly technicalities are to be checked in the prototype is neuper@42498: shown in \S\ref{flow-prep} below. jan@42473: neuper@42498: % \paragraph{Explicit Problems} require explicit methods to solve them, and within neuper@42498: % this methods we have some explicit steps to do. This steps can be unique for neuper@42498: % a special problem or refindable in other problems. No mather what case, such neuper@42498: % steps often require some technical functions behind. For the solving process neuper@42498: % of the Inverse Z Transformation and the corresponding partial fraction it was neuper@42498: % neccessary to build helping functions like \texttt{get\_denominator}, neuper@42498: % \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us neuper@42498: % to filter the denominator or numerator out of a fraction, last one helps us to neuper@42498: % get to know the bound variable in a equation. neuper@42498: % \par neuper@42498: % By taking \texttt{get\_denominator} as an example, we want to explain how to neuper@42498: % implement new functions into the existing system and how we can later use them neuper@42498: % in our program. neuper@42498: % neuper@42498: % \subsubsection{Find a place to Store the Function} neuper@42498: % neuper@42498: % The whole system builds up on a well defined structure of Knowledge. This neuper@42498: % Knowledge sets up at the Path: neuper@42498: % \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center} neuper@42498: % For implementing the Function \texttt{get\_denominator} (which let us extract neuper@42498: % the denominator out of a fraction) we have choosen the Theory (file) neuper@42498: % \texttt{Rational.thy}. neuper@42498: % neuper@42498: % \subsubsection{Write down the new Function} neuper@42498: % neuper@42498: % In upper Theory we now define the new function and its purpose: neuper@42498: % \begin{verbatim} neuper@42498: % get_denominator :: "real => real" neuper@42498: % \end{verbatim} neuper@42498: % This command tells the machine that a function with the name neuper@42498: % \texttt{get\_denominator} exists which gets a real expression as argument and neuper@42498: % returns once again a real expression. Now we are able to implement the function neuper@42498: % itself, upcoming example now shows the implementation of neuper@42498: % \texttt{get\_denominator}. neuper@42498: % neuper@42498: % %\begin{example} neuper@42498: % \label{eg:getdenom} neuper@42498: % \begin{verbatim} neuper@42498: % neuper@42498: % 01 (* neuper@42498: % 02 *("get_denominator", neuper@42498: % 03 * ("Rational.get_denominator", eval_get_denominator "")) neuper@42498: % 04 *) neuper@42498: % 05 fun eval_get_denominator (thmid:string) _ neuper@42498: % 06 (t as Const ("Rational.get_denominator", _) $ neuper@42498: % 07 (Const ("Rings.inverse_class.divide", _) $num neuper@42498: % 08 $denom)) thy = neuper@42498: % 09 SOME (mk_thmid thmid "" neuper@42498: % 10 (Print_Mode.setmp [] neuper@42498: % 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "", neuper@42498: % 12 Trueprop $ (mk_equality (t, denom))) neuper@42498: % 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim} neuper@42498: % %\end{example} neuper@42498: % neuper@42498: % Line \texttt{07} and \texttt{08} are describing the mode of operation the best - neuper@42498: % there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont) neuper@42498: % splittet neuper@42498: % into its two parts (\texttt{\$num \$denom}). The lines before are additionals neuper@42498: % commands for declaring the function and the lines after are modeling and neuper@42498: % returning a real variable out of \texttt{\$denom}. neuper@42498: % neuper@42498: % \subsubsection{Add a test for the new Function} neuper@42498: % neuper@42498: % \paragraph{Everytime when adding} a new function it is essential also to add neuper@42498: % a test for it. Tests for all functions are sorted in the same structure as the neuper@42498: % knowledge it self and can be found up from the path: neuper@42498: % \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center} neuper@42498: % This tests are nothing very special, as a first prototype the functionallity neuper@42498: % of a function can be checked by evaluating the result of a simple expression neuper@42498: % passed to the function. Example~\ref{eg:getdenomtest} shows the test for our neuper@42498: % \textit{just} created function \texttt{get\_denominator}. neuper@42498: % neuper@42498: % %\begin{example} neuper@42498: % \label{eg:getdenomtest} neuper@42498: % \begin{verbatim} neuper@42498: % neuper@42498: % 01 val thy = @{theory Isac}; neuper@42498: % 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)")); neuper@42498: % 03 val SOME (_, t') = eval_get_denominator "" 0 t thy; neuper@42498: % 04 if term2str t' = "get_denominator ((a + x) / b) = b" then () neuper@42498: % 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim} neuper@42498: % %\end{example} neuper@42498: % neuper@42498: % \begin{description} neuper@42498: % \item[01] checks if the proofer set up on our {\sisac{}} System. neuper@42498: % \item[02] passes a simple expression (fraction) to our suddenly created neuper@42498: % function. neuper@42498: % \item[04] checks if the resulting variable is the correct one (in this case neuper@42498: % ``b'' the denominator) and returns. neuper@42498: % \item[05] handels the error case and reports that the function is not able to neuper@42498: % solve the given problem. neuper@42498: % \end{description} jan@42469: jan@42491: \subsection{Specification of the Problem}\label{spec} jan@42491: %WN <--> \chapter 7 der Thesis jan@42491: %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. jan@42491: jan@42491: The problem of the running example is textually described in jan@42491: Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em jan@42491: formal} specification of this problem, in traditional mathematical jan@42491: notation, could look like is this: jan@42491: jan@42491: %WN Hier brauchen wir die Spezifikation des 'running example' ... jan@42491: %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei jan@42491: %JR der post condition - die existiert für uns ja eigentlich nicht aka jan@42491: %JR haben sie bis jetzt nicht beachtet WN... jan@42491: %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren. jan@42491: %JR2 done jan@42491: jan@42491: \label{eg:neuper2} jan@42491: {\small\begin{tabbing} jan@42491: 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill jan@42491: \hfill \\ jan@42491: Specification:\\ jan@42491: \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\ jan@42491: \>precond \>: filterExpression continius on $\mathbb{R}$ \\ jan@42491: \>output \>: stepResponse $x[n]$ \\ jan@42500: \>postcond \>: TODO\\ \end{tabbing}} jan@42491: jan@42500: %JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt" jan@42500: jan@42500: % \begin{remark} jan@42500: % Defining the postcondition requires a high amount mathematical jan@42500: % knowledge, the difficult part in our case is not to set up this condition jan@42500: % nor it is more to define it in a way the interpreter is able to handle it. jan@42500: % Due the fact that implementing that mechanisms is quite the same amount as jan@42500: % creating the programm itself, it is not avaible in our prototype. jan@42500: % \label{rm:postcond} jan@42500: % \end{remark} jan@42491: jan@42491: \paragraph{The implementation} of the formal specification in the present jan@42491: prototype, still bar-bones without support for authoring: jan@42491: %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert: jan@42491: {\footnotesize\label{exp-spec} jan@42491: \begin{verbatim} jan@42491: 01 store_specification jan@42491: 02 (prepare_specification jan@42491: 03 ["Jan Rocnik"] jan@42491: 04 "pbl_SP_Ztrans_inv" jan@42491: 05 thy jan@42491: 06 ( ["Inverse", "Z_Transform", "SignalProcessing"], jan@42491: 07 [ ("#Given", ["filterExpression X_eq"]), jan@42491: 08 ("#Pre" , ["X_eq is_continuous"]), jan@42494: 09 ("#Find" , ["stepResponse n_eq"]), jan@42491: 10 ("#Post" , [" TODO "])], jan@42491: 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)], jan@42491: 12 NONE, jan@42491: 13 [["SignalProcessing","Z_Transform","Inverse"]])); jan@42491: \end{verbatim}} jan@42491: Although the above details are partly very technical, we explain them jan@42491: in order to document some intricacies of TP-based programming in the jan@42491: present state of the {\sisac} prototype: jan@42491: \begin{description} jan@42491: \item[01..02]\textit{store\_specification:} stores the result of the jan@42491: function \textit{prep\_specification} in a global reference jan@42491: \textit{Unsynchronized.ref}, which causes principal conflicts with jan@42491: Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and jan@42491: parallel execution~\cite{Makarius-09:parall-proof} and is under jan@42491: reconstruction already. jan@42491: jan@42491: \textit{prep\_pbt:} translates the specification to an internal format jan@42491: which allows efficient processing; see for instance line {\rm 07} jan@42491: below. jan@42491: \item[03..04] are the ``mathematics author'' holding the copy-rights jan@42491: and a unique identifier for the specification within {\sisac}, jan@42491: complare line {\rm 06}. jan@42491: \item[05] is the Isabelle \textit{theory} required to parse the jan@42491: specification in lines {\rm 07..10}. jan@42491: \item[06] is a key into the tree of all specifications as presented to jan@42491: the user (where some branches might be hidden by the dialog jan@42491: component). jan@42491: \item[07..10] are the specification with input, pre-condition, output jan@42491: and post-condition respectively; the post-condition is not handled in jan@42491: the prototype presently. (Follow up Remark~\ref{rm:postcond}) jan@42491: \item[11] creates a term rewriting system (abbreviated \textit{rls} in jan@42491: {\sisac}) which evaluates the pre-condition for the actual input data. jan@42491: Only if the evaluation yields \textit{True}, a program con be started. jan@42491: \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a jan@42491: problem associated to a function from Computer Algebra (like an jan@42491: equation solver) which is not the case here. jan@42491: \item[13] is the specific key into the tree of programs addressing a jan@42491: method which is able to find a solution which satiesfies the jan@42491: post-condition of the specification. jan@42491: \end{description} jan@42491: jan@42491: jan@42491: %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *" jan@42491: %WN ... jan@42491: % type pbt = jan@42491: % {guh : guh, (*unique within this isac-knowledge*) jan@42491: % mathauthors: string list, (*copyright*) jan@42491: % init : pblID, (*to start refinement with*) jan@42491: % thy : theory, (* which allows to compile that pbt jan@42491: % TODO: search generalized for subthy (ref.p.69*) jan@42491: % (*^^^ WN050912 NOT used during application of the problem, jan@42491: % because applied terms may be from 'subthy' as well as from super; jan@42491: % thus we take 'maxthy'; see match_ags !*) jan@42491: % cas : term option,(*'CAS-command'*) jan@42491: % prls : rls, (* for preds in where_*) jan@42491: % where_: term list, (* where - predicates*) jan@42491: % ppc : pat list, jan@42491: % (*this is the model-pattern; jan@42491: % it contains "#Given","#Where","#Find","#Relate"-patterns jan@42491: % for constraints on identifiers see "fun cpy_nam"*) jan@42491: % met : metID list}; (* methods solving the pbt*) jan@42491: % jan@42491: %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen jan@42491: %WN oben selbst geschrieben. jan@42491: jan@42491: jan@42491: jan@42491: jan@42491: %WN das w"urde ich in \sec\label{progr} verschieben und jan@42491: %WN das SubProblem partial fractions zum Erkl"aren verwenden. jan@42491: % Such a specification is checked before the execution of a program is jan@42491: % started, the same applies for sub-programs. In the following example jan@42491: % (Example~\ref{eg:subprob}) shows the call of such a subproblem: jan@42491: % jan@42491: % \vbox{ jan@42491: % \begin{example} jan@42491: % \label{eg:subprob} jan@42491: % \hfill \\ jan@42491: % {\ttfamily \begin{tabbing} jan@42491: % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\ jan@42491: % ``\>\>[linear,univariate,equation,test],'' \\ jan@42491: % ``\>\>[Test,solve\_linear])'' \\ jan@42491: % ``\>[BOOL equ, REAL z])'' \\ jan@42491: % \end{tabbing} jan@42491: % } jan@42491: % {\small\textit{ jan@42491: % \noindent If a program requires a result which has to be jan@42491: % calculated first we can use a subproblem to do so. In our specific jan@42491: % case we wanted to calculate the zeros of a fraction and used a jan@42491: % subproblem to calculate the zeros of the denominator polynom. jan@42491: % }} jan@42491: % \end{example} jan@42491: % } jan@42491: jan@42491: \subsection{Implementation of the Method}\label{meth} jan@42491: jan@42500: The methods represent the different ways a problem can be solved. This can jan@42500: include mathematical tactics as well as tactics taught in different courses. jan@42500: Declaring the Method itself gives us the possibilities to describe the way of jan@42500: calculation in deep, as well we get the oppertunities to build in different jan@42500: rulesets. jan@42491: jan@42502: {\footnotesize jan@42491: \begin{verbatim} jan@42491: 01 store_met jan@42494: 02 (prep_met thy "SP_InverseZTransformation_classic" [] e_metID jan@42491: 03 (["SignalProcessing", "Z_Transform", "Inverse"], jan@42491: 04 [("#Given" ,["filterExpression (X_eq::bool)"]), jan@42491: 05 ("#Find" ,["stepResponse (n_eq::bool)"])], jan@42491: 06 {rew_ord'="tless_true", jan@42500: 07 rls = rls, jan@42491: 08 calc = [], jan@42491: 09 srls = e_rls, jan@42491: 10 prls = e_rls, jan@42491: 11 crls = e_rls, jan@42491: 12 errpats = [], jan@42491: 13 nrls = e_rls}, jan@42500: 14 "empty_program" jan@42491: 15 )); jan@42491: \end{verbatim} jan@42500: } jan@42494: jan@42500: The above code is again very technical and goes hard in detail. Unfortunataly jan@42500: most declerations are not essential for a basic programm but leads us to a huge jan@42500: range of powerful possibilities. jan@42494: jan@42494: \begin{description} jan@42500: \item[01..02] stores the method with the given name into the system under a global jan@42500: reference. jan@42502: \item[03] specifies the topic within which context the method can be found. jan@42502: \item[04..05] as the requirements for different methods can be deviant we jan@42500: declare what is \emph{given} and and what to \emph{find} for this specific method. jan@42502: The code again helds on the topic of the case studie, where the inverse jan@42502: z-transformation does a switch between a term describing a electrical filter into jan@42502: its step response. Also the datatype has to be declared (bool - due the fact that jan@42502: we handle equations). jan@42502: \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one jan@42502: theorem of it is used for rewriting one single step. jan@42502: \item[07] \texttt{rls} is the currently used ruleset for this method. This set jan@42502: has already been defined before. jan@42502: \item[08] we would have the possiblitiy to add this method to a predefined tree of jan@42502: calculations, i.eg. if it would be a sub of a bigger problem, here we leave it jan@42502: independend. jan@42502: \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in jan@42502: the source. jan@42502: \item[10] \emph{predicates ruleset} can be used to indicates predicates within jan@42502: model patterns. jan@42502: \item[11] The \emph{check ruleset} summarizes rules for checking formulas jan@42502: elementwise. jan@42500: \item[12] \emph{error patterns} which are expected in this kind of method can be jan@42502: pre-specified to recognize them during the method. jan@42502: \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier jan@42502: of the specific method. jan@42502: \item[14] for this code snipset we don't specify the programm itself and keep it jan@42502: empty. Follow up \S\ref{progr} for informations on how to implement this jan@42502: \textit{main} part. jan@42494: \end{description} jan@42491: neuper@42478: \subsection{Implementation of the TP-based Program}\label{progr} neuper@42480: So finally all the prerequisites are described and the very topic can neuper@42480: be addressed. The program below comes back to the running example: it neuper@42480: computes a solution for the problem from Fig.\ref{fig-interactive} on neuper@42480: p.\pageref{fig-interactive}. The reader is reminded of neuper@42480: \S\ref{PL-isab}, the introduction of the programming language: jan@42502: jan@42502: {\footnotesize\it\label{s:impl} neuper@42482: \begin{tabbing} neuper@42478: 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill neuper@42480: \>{\rm 00}\>val program =\\ neuper@42480: \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\ neuper@42482: \>{\rm 02}\>\> {\tt let} \\ neuper@42468: \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\ neuper@42468: \>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\ neuper@42468: \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation neuper@42468: \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\ neuper@42468: \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\ neuper@42478: \>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\ neuper@42478: %\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\ neuper@42478: \>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\ neuper@42478: \>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\ neuper@42478: \>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@ \\ neuper@42478: \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\ neuper@42482: \>{\rm 13}\>\> {\tt in } \\ neuper@42480: \>{\rm 14}\>\>\> X'\_eq" neuper@42478: \end{tabbing}} neuper@42468: % ORIGINAL FROM Inverse_Z_Transform.thy neuper@42468: % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) neuper@42468: % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) neuper@42468: % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) neuper@42468: % " (X'_z::real) = lhs X'; "^(* ?X' z*) neuper@42468: % " (zzz::real) = argument_in X'_z; "^(* z *) neuper@42468: % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) neuper@42468: % neuper@42468: % " (pbz::real) = (SubProblem (Isac', "^(**) neuper@42468: % " [partial_fraction,rational,simplification], "^ neuper@42468: % " [simplification,of_rationals,to_partial_fraction]) "^ neuper@42468: % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) neuper@42468: % neuper@42468: % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) neuper@42468: % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) neuper@42468: % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) neuper@42468: % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) neuper@42468: % " 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]*) neuper@42468: % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) neuper@42468: % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) neuper@42480: The program is represented as a string and part of the method in neuper@42480: \S\ref{meth}. As mentioned in \S\ref{PL} the program is purely neuper@42480: functional and lacks any input statements and output statements. So neuper@42480: the steps of calculation towards a solution (and interactive tutoring neuper@42480: in step-wise problem solving) are created as a side-effect by neuper@42480: Lucas-Interpretation. The side-effects are triggered by the tactics neuper@42482: \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and neuper@42482: \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and neuper@42480: {\rm 12} respectively. These tactics produce the lines in the neuper@42480: calculation on p.\pageref{flow-impl}. neuper@42478: neuper@42480: The above lines {\rm 05, 06} do not contain a tactics, so they do not neuper@42480: immediately contribute to the calculation on p.\pageref{flow-impl}; neuper@42482: rather, they compute actual arguments for the \texttt{SubProblem} in neuper@42480: line {\rm 09}~\footnote{The tactics also are break-points for the neuper@42480: interpreter, where control is handed over to the user in interactive neuper@42482: tutoring.}. Line {\rm 11} contains tactical \textit{@@}. neuper@42480: neuper@42480: \medskip The above program also indicates the dominant role of interactive neuper@42478: selection of knowledge in the three-dimensional universe of neuper@42478: mathematics as depicted in Fig.\ref{fig:mathuni} on neuper@42482: p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines neuper@42478: {\rm 07..09} is more than a function call with the actual arguments neuper@42478: \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine neuper@42478: three items: neuper@42480: neuper@42478: \begin{enumerate} neuper@42478: \item the theory, in the example \textit{Isac} because different neuper@42478: methods can be selected in Pt.3 below, which are defined in different neuper@42478: theories with \textit{Isac} collecting them. neuper@42480: \item the specification identified by \textit{[partial\_fraction, neuper@42480: rational, simplification]} in the tree of specifications; this neuper@42480: specification is analogous to the specification of the main program neuper@42480: described in \S\ref{spec}; the problem is to find a ``partial fraction neuper@42480: decomposition'' for a univariate rational polynomial. neuper@42480: \item the method in the above example is \textit{[ ]}, i.e. empty, neuper@42480: which supposes the interpreter to select one of the methods predefined neuper@42480: in the specification, for instance in line {\rm 13} in the running neuper@42480: example's specification on p.\pageref{exp-spec}~\footnote{The freedom neuper@42480: (or obligation) for selection carries over to the student in neuper@42480: interactive tutoring.}. neuper@42478: \end{enumerate} neuper@42478: neuper@42480: The program code, above presented as a string, is parsed by Isabelle's neuper@42480: parser --- the program is an Isabelle term. This fact is expected to neuper@42480: simplify verification tasks in the future; on the other hand, this neuper@42480: fact causes troubles in error detectetion which are discussed as part neuper@42480: of the workflow in the subsequent section. neuper@42467: jan@42463: \section{Workflow of Programming in the Prototype}\label{workflow} neuper@42498: The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great neuper@42498: step forward for interactive theory and proof development. The neuper@42498: {\sisac}-prototype re-uses this IDE as a programming environment. The neuper@42498: experiences from this re-use show, that the essential components are neuper@42498: available from Isabelle/jEdit. However, additional tools and features neuper@42498: are required to acchieve acceptable usability. neuper@42498: neuper@42498: So notable experiences are reported here, also as a requirement neuper@42498: capture for further development of TP-based languages and respective neuper@42498: IDEs. neuper@42468: jan@42466: \subsection{Preparations and Trials}\label{flow-prep} neuper@42499: The many sub-tasks to be accomplished {\em before} the first line of neuper@42499: program code can be written and tested suggest an approach which neuper@42499: step-wise establishes the prerequisites. The case study underlying neuper@42499: this paper~\cite{jrocnik-bakk} documents the approach in a separate neuper@42499: Isabelle theory, neuper@42499: \textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part neuper@42499: II in the study comprises this theory, \LaTeX ed from the theory by neuper@42499: use of Isabelle's document preparation system. This paper resembles neuper@42499: the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual neuper@42499: implementation work involves several iterations. neuper@42498: neuper@42499: \bigskip For instance, only the last step, implementing the program neuper@42499: described in \S\ref{meth}, reveals details required. Let us assume, neuper@42499: this is the ML-function \textit{argument\_in} required in line {\rm 06} neuper@42499: of the example program on p.\pageref{s:impl}; how this function needs neuper@42499: to be implemented in the prototype has been discussed in \S\ref{funs} neuper@42499: already. neuper@42498: neuper@42499: Now let us assume, that calling this function from the program code neuper@42499: does not work; so testing this function is required in order to find out neuper@42499: the reason: type errors, a missing entry of the function somewhere or neuper@42499: even more nasty technicalities \dots neuper@42498: neuper@42499: {\footnotesize neuper@42482: \begin{verbatim} neuper@42482: ML {* neuper@42499: val SOME t = parseNEW ctxt "argument_in (X (z::real))"; neuper@42499: val SOME (str, t') = eval_argument_in "" neuper@42499: "Build_Inverse_Z_Transform.argument'_in" t 0; neuper@42482: *} neuper@42499: ML {* neuper@42499: term2str t'; neuper@42499: *} neuper@42499: val it = "(argument_in X z) = z": string neuper@42482: \end{verbatim}} neuper@42499: neuper@42499: \noindent So, this works: we get an ad-hoc theorem, which used in neuper@42499: rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this neuper@42499: reduction and create a rule-set \texttt{rls} for that purpose: neuper@42499: neuper@42499: {\footnotesize neuper@42482: \begin{verbatim} neuper@42482: ML {* neuper@42499: val rls = append_rls "test" e_rls neuper@42499: [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")] neuper@42482: *} neuper@42499: ML {* neuper@42499: val SOME (t', asm) = rewrite_set_ @{theory} rls t; neuper@42499: *} neuper@42499: val t' = Free ("z", "RealDef.real"): term neuper@42499: val asm = []: term list neuper@42482: \end{verbatim}} neuper@42499: neuper@42499: \noindent The resulting term \texttt{t'} is \texttt{Free ("z", neuper@42499: "RealDef.real")}, i.e the variable \texttt{z}, so all is neuper@42499: perfect. Probably we have forgotten to store this function correctly~? neuper@42499: We review the respective \texttt{calclist} (again an neuper@42499: \textit{Unsynchronized.ref} to be removed in order to adjust to neuper@42499: IsabelleIsar's asyncronous document model): neuper@42499: neuper@42499: {\footnotesize neuper@42499: \begin{verbatim} neuper@42499: calclist:= overwritel (! calclist, neuper@42499: [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")), neuper@42499: ... neuper@42499: ]); neuper@42499: \end{verbatim}} neuper@42499: neuper@42499: \noindent The entry is perfect. So what is the reason~? Ah, probably there neuper@42499: is something messed up with the many rule-sets in the method, see \S\ref{meth} --- neuper@42499: right, the function \texttt{argument\_in} is not contained in the respective neuper@42499: rule-set \textit{srls} \dots this just as an example of the intricacies in neuper@42499: debugging a program in the present state of the prototype. neuper@42499: neuper@42499: \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} neuper@42499: Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth}, neuper@42499: usually developed within several iterations, the program can be neuper@42499: assembled; on p.\pageref{s:impl} there is the complete program of the neuper@42499: running example. neuper@42499: neuper@42499: The completion of this program required efforts for several weeks neuper@42499: (after some months of familiarisation with {\sisac}), caused by the neuper@42499: abundance of intricacies indicated above. Also writing the program is neuper@42499: not pleasant, given Isabelle/Isar/ without add-ons for neuper@42499: programming. Already writing and parsing a few lines of program code neuper@42499: is a challenge: the program is an Isabelle term; Isabelle's parser, neuper@42499: however, is not meant for huge terms like the program of the running neuper@42499: example. So reading out the specific error (usually type errors) from neuper@42499: Isabelle's message is difficult. neuper@42499: neuper@42499: \medskip Testing the evaluation of the program has to rely on very neuper@42499: simple tools. Step-wise execution is modelled by a function neuper@42499: \texttt{me}, short for mathematics-engine~\footnote{The interface used neuper@42499: by the fron-end which created the calculation on neuper@42499: p.\pageref{fig-interactive} is different from this function}: neuper@42499: %the following is a simplification of the actual function neuper@42499: neuper@42499: {\footnotesize neuper@42499: \begin{verbatim} neuper@42499: ML {* me; *} neuper@42499: val it = tac -> ctree * pos -> mout * tac * ctree * pos neuper@42499: \end{verbatim}} neuper@42499: neuper@42499: \noindent This function takes as arguments a tactic \texttt{tac} which neuper@42499: determines the next step, the step applied to the interpreter-state neuper@42499: \texttt{ctree * pos} as last argument taken. The interpreter-state is neuper@42499: a pair of a tree \texttt{ctree} representing the calculation created neuper@42499: (see the example below) and a position \texttt{pos} in the neuper@42499: calculation. The function delivers a quadrupel, beginning with the new neuper@42499: formula \texttt{mout} and the next tactic followed by the new neuper@42499: interpreter-state. neuper@42499: neuper@42499: This function allows to stepwise check the program: neuper@42499: neuper@42499: {\footnotesize neuper@42482: \begin{verbatim} neuper@42482: ML {* neuper@42499: val fmz = neuper@42499: ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))", neuper@42499: "stepResponse (x[n::real]::bool)"]; neuper@42499: val (dI,pI,mI) = neuper@42499: ("Isac", neuper@42499: ["Inverse", "Z_Transform", "SignalProcessing"], neuper@42499: ["SignalProcessing","Z_Transform","Inverse"]); neuper@42499: neuper@42499: val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))]; neuper@42499: val (mout, tac, ctree, pos) = me tac (ctree, pos); neuper@42499: val (mout, tac, ctree, pos) = me tac (ctree, pos); neuper@42499: val (mout, tac, ctree, pos) = me tac (ctree, pos); neuper@42499: ... neuper@42499: \end{verbatim}} neuper@42481: neuper@42499: \noindent Several douzens of calls for \texttt{me} are required to neuper@42499: create the lines in the calculation below (including the sub-problems neuper@42499: not shown). When an error occurs, the reason might be located neuper@42499: many steps before: if evaluation by rewriting, as done by the prototype, neuper@42499: fails, then first nothing happens --- the effects come later and neuper@42499: cause unpleasant checks. neuper@42481: neuper@42499: The checks comprise watching the rewrite-engine for many different neuper@42499: kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in neuper@42499: particular the environment and the context at the states position --- neuper@42499: all checks have to rely on simple functions accessing the neuper@42499: \texttt{ctree}. So getting the calculation below (which resembles the neuper@42499: calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) neuper@42499: finished successfully is a relief: jan@42469: neuper@42498: {\small\it\label{exp-calc} neuper@42468: \begin{tabbing} neuper@42468: 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill neuper@42468: \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\ neuper@42468: \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\ neuper@42468: \>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\ neuper@42468: \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\ neuper@42468: \>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\ neuper@42468: \>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\ neuper@42468: \>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\ neuper@42468: \>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\ neuper@42468: \>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\ neuper@42468: \>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\ neuper@42468: \> \>\>\>\> \_\_\_ \`- - -\\ neuper@42468: \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\ neuper@42468: \>{\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)}\\ neuper@42468: \>{\rm 13}\>\> $X^\prime z = {\cal Z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} ruleYZ X'\_eq }\\ neuper@42468: \>{\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}\\ neuper@42468: \>{\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}} neuper@42468: \end{tabbing}} neuper@42468: % ORIGINAL FROM Inverse_Z_Transform.thy neuper@42468: % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) neuper@42468: % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) neuper@42468: % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) neuper@42468: % " (X'_z::real) = lhs X'; "^(* ?X' z*) neuper@42468: % " (zzz::real) = argument_in X'_z; "^(* z *) neuper@42468: % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) neuper@42468: % neuper@42468: % " (pbz::real) = (SubProblem (Isac', "^(**) neuper@42468: % " [partial_fraction,rational,simplification], "^ neuper@42468: % " [simplification,of_rationals,to_partial_fraction]) "^ neuper@42468: % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) neuper@42468: % neuper@42468: % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) neuper@42468: % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) neuper@42468: % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) neuper@42468: % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) neuper@42468: % " 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]*) neuper@42468: % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) neuper@42468: % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) neuper@42468: neuper@42499: \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans} neuper@42499: Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done neuper@42499: and the knowledge accumulated in it can be distributed to appropriate neuper@42499: theories: the program to \textit{Inverse\_Z\_Transform.thy}, the neuper@42499: sub-problem accomplishing the partial fraction decomposition to neuper@42499: \textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's neuper@42499: internals, this kind of distribution is not trivial. For instance, the neuper@42499: function \texttt{argument\_in} in \S\ref{funs} explicitly contains a neuper@42499: string with the theory it has been defined in, so this string needs to neuper@42499: be updated from \texttt{Build\_Inverse\_Z\_Transform} to neuper@42499: \texttt{Atools} if that function is transferred to theory neuper@42499: \textit{Atools.thy}. neuper@42468: neuper@42499: 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. neuper@42499: This process is also rather bare-bones without authoring tools and is neuper@42499: described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}. neuper@42468: neuper@42478: % \newpage neuper@42478: % ------------------------------------------------------------------- neuper@42478: % neuper@42478: % Material, falls noch Platz bleibt ... neuper@42478: % neuper@42478: % ------------------------------------------------------------------- neuper@42478: % neuper@42478: % neuper@42478: % \subsubsection{Trials on Notation and Termination} neuper@42478: % neuper@42478: % \paragraph{Technical notations} are a big problem for our piece of software, neuper@42478: % but the reason for that isn't a fault of the software itself, one of the neuper@42478: % troubles comes out of the fact that different technical subtopics use different neuper@42478: % symbols and notations for a different purpose. The most famous example for such neuper@42478: % a symbol is the complex number $i$ (in cassique math) or $j$ (in technical neuper@42478: % math). In the specific part of signal processing one of this notation issues is neuper@42478: % the use of brackets --- we use round brackets for analoge signals and squared neuper@42478: % brackets for digital samples. Also if there is no problem for us to handle this neuper@42478: % fact, we have to tell the machine what notation leads to wich meaning and that neuper@42478: % this purpose seperation is only valid for this special topic - signal neuper@42478: % processing. neuper@42478: % \subparagraph{In the programming language} itself it is not possible to declare neuper@42478: % fractions, exponents, absolutes and other operators or remarks in a way to make neuper@42478: % them pretty to read; our only posssiblilty were ASCII characters and a handfull neuper@42478: % greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$. neuper@42478: % \par neuper@42478: % With the upper collected knowledge it is possible to check if we were able to neuper@42478: % donate all required terms and expressions. neuper@42478: % neuper@42478: % \subsubsection{Definition and Usage of Rules} neuper@42478: % neuper@42478: % \paragraph{The core} of our implemented problem is the Z-Transformation, due neuper@42478: % the fact that the transformation itself would require higher math which isn't neuper@42478: % yet avaible in our system we decided to choose the way like it is applied in neuper@42478: % labratory and problem classes at our university - by applying transformation neuper@42478: % rules (collected in transformation tables). neuper@42478: % \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the neuper@42478: % use of axiomatizations like shown in Example~\ref{eg:ruledef} neuper@42478: % neuper@42478: % \begin{example} neuper@42478: % \label{eg:ruledef} neuper@42478: % \hfill\\ neuper@42478: % \begin{verbatim} neuper@42478: % axiomatization where neuper@42478: % rule1: ``1 = $\delta$[n]'' and neuper@42478: % rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and neuper@42478: % rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]'' neuper@42478: % \end{verbatim} neuper@42478: % \end{example} neuper@42478: % neuper@42478: % This rules can be collected in a ruleset and applied to a given expression as neuper@42478: % follows in Example~\ref{eg:ruleapp}. neuper@42478: % neuper@42478: % \begin{example} neuper@42478: % \hfill\\ neuper@42478: % \label{eg:ruleapp} neuper@42478: % \begin{enumerate} neuper@42478: % \item Store rules in ruleset: neuper@42478: % \begin{verbatim} neuper@42478: % val inverse_Z = append_rls "inverse_Z" e_rls neuper@42478: % [ Thm ("rule1",num_str @{thm rule1}), neuper@42478: % Thm ("rule2",num_str @{thm rule2}), neuper@42478: % Thm ("rule3",num_str @{thm rule3}) neuper@42478: % ];\end{verbatim} neuper@42478: % \item Define exression: neuper@42478: % \begin{verbatim} neuper@42478: % val sample_term = str2term "z/(z-1)+z/(z-)+1";\end{verbatim} neuper@42478: % \item Apply ruleset: neuper@42478: % \begin{verbatim} neuper@42478: % val SOME (sample_term', asm) = neuper@42478: % rewrite_set_ thy true inverse_Z sample_term;\end{verbatim} neuper@42478: % \end{enumerate} neuper@42478: % \end{example} neuper@42478: % neuper@42478: % The use of rulesets makes it much easier to develop our designated applications, neuper@42478: % but the programmer has to be careful and patient. When applying rulesets neuper@42478: % two important issues have to be mentionend: neuper@42478: % \subparagraph{How often} the rules have to be applied? In case of neuper@42478: % transformations it is quite clear that we use them once but other fields neuper@42478: % reuqire to apply rules until a special condition is reached (e.g. neuper@42478: % a simplification is finished when there is nothing to be done left). neuper@42478: % \subparagraph{The order} in which rules are applied often takes a big effect neuper@42478: % and has to be evaluated for each purpose once again. neuper@42478: % \par neuper@42478: % In our special case of Signal Processing and the rules defined in neuper@42478: % Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all neuper@42478: % constants. After this step has been done it no mather which rule fit's next. neuper@42478: % neuper@42478: % \subsubsection{Helping Functions} neuper@42478: % neuper@42478: % \paragraph{New Programms require,} often new ways to get through. This new ways neuper@42478: % means that we handle functions that have not been in use yet, they can be neuper@42478: % something special and unique for a programm or something famous but unneeded in neuper@42478: % the system yet. In our dedicated example it was for example neccessary to split neuper@42478: % a fraction into numerator and denominator; the creation of such function and neuper@42478: % even others is described in upper Sections~\ref{simp} and \ref{funs}. neuper@42478: % neuper@42478: % \subsubsection{Trials on equation solving} neuper@42478: % %simple eq and problem with double fractions/negative exponents neuper@42478: % \paragraph{The Inverse Z-Transformation} makes it neccessary to solve neuper@42478: % equations degree one and two. Solving equations in the first degree is no neuper@42478: % problem, wether for a student nor for our machine; but even second degree neuper@42478: % equations can lead to big troubles. The origin of this troubles leads from neuper@42478: % the build up process of our equation solving functions; they have been neuper@42478: % implemented some time ago and of course they are not as good as we want them to neuper@42478: % be. Wether or not following we only want to show how cruel it is to build up new neuper@42478: % work on not well fundamentials. neuper@42478: % \subparagraph{A simple equation solving,} can be set up as shown in the next neuper@42478: % example: neuper@42478: % neuper@42478: % \begin{example} neuper@42478: % \begin{verbatim} neuper@42478: % neuper@42478: % val fmz = neuper@42478: % ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))", neuper@42478: % "solveFor z", neuper@42478: % "solutions L"]; neuper@42478: % neuper@42478: % val (dI',pI',mI') = neuper@42478: % ("Isac", neuper@42478: % ["abcFormula","degree_2","polynomial","univariate","equation"], neuper@42478: % ["no_met"]);\end{verbatim} neuper@42478: % \end{example} neuper@42478: % neuper@42478: % Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give neuper@42478: % a short overview on the commands; at first we set up the equation and tell the neuper@42478: % machine what's the bound variable and where to store the solution. Second step neuper@42478: % is to define the equation type and determine if we want to use a special method neuper@42478: % to solve this type.) Simple checks tell us that the we will get two results for neuper@42478: % this equation and this results will be real. neuper@42478: % So far it is easy for us and for our machine to solve, but neuper@42478: % mentioned that a unvariate equation second order can have three different types neuper@42478: % of solutions it is getting worth. neuper@42478: % \subparagraph{The solving of} all this types of solutions is not yet supported. neuper@42478: % Luckily it was needed for us; but something which has been needed in this neuper@42478: % context, would have been the solving of an euation looking like: neuper@42478: % $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned neuper@42478: % before (remember that befor it was no problem to handle for the machine) but neuper@42478: % now, after a simple equivalent transformation, we are not able to solve neuper@42478: % it anymore. neuper@42478: % \subparagraph{Error messages} we get when we try to solve something like upside neuper@42478: % were very confusing and also leads us to no special hint about a problem. neuper@42478: % \par The fault behind is, that we have no well error handling on one side and neuper@42478: % no sufficient formed equation solving on the other side. This two facts are neuper@42478: % making the implemention of new material very difficult. neuper@42478: % neuper@42478: % \subsection{Formalization of missing knowledge in Isabelle} neuper@42478: % neuper@42478: % \paragraph{A problem} behind is the mechanization of mathematic neuper@42478: % theories in TP-bases languages. There is still a huge gap between neuper@42478: % these algorithms and this what we want as a solution - in Example neuper@42478: % Signal Processing. neuper@42478: % neuper@42478: % \vbox{ neuper@42478: % \begin{example} neuper@42478: % \label{eg:gap} neuper@42478: % \[ neuper@42478: % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY neuper@42478: % \] neuper@42478: % {\small\textit{ neuper@42478: % \noindent A very simple example on this what we call gap is the neuper@42478: % simplification above. It is needles to say that it is correct and also neuper@42478: % Isabelle for fills it correct - \emph{always}. But sometimes we don't neuper@42478: % want expand such terms, sometimes we want another structure of neuper@42478: % them. Think of a problem were we now would need only the coefficients neuper@42478: % of $X$ and $Y$. This is what we call the gap between mechanical neuper@42478: % simplification and the solution. neuper@42478: % }} neuper@42478: % \end{example} neuper@42478: % } neuper@42478: % neuper@42478: % \paragraph{We are not able to fill this gap,} until we have to live neuper@42478: % with it but first have a look on the meaning of this statement: neuper@42478: % Mechanized math starts from mathematical models and \emph{hopefully} neuper@42478: % proceeds to match physics. Academic engineering starts from physics neuper@42478: % (experimentation, measurement) and then proceeds to mathematical neuper@42478: % modeling and formalization. The process from a physical observance to neuper@42478: % a mathematical theory is unavoidable bound of setting up a big neuper@42478: % collection of standards, rules, definition but also exceptions. These neuper@42478: % are the things making mechanization that difficult. neuper@42478: % neuper@42478: % \vbox{ neuper@42478: % \begin{example} neuper@42478: % \label{eg:units} neuper@42478: % \[ neuper@42478: % m,\ kg,\ s,\ldots neuper@42478: % \] neuper@42478: % {\small\textit{ neuper@42478: % \noindent Think about some units like that one's above. Behind neuper@42478: % each unit there is a discerning and very accurate definition: One neuper@42478: % Meter is the distance the light travels, in a vacuum, through the time neuper@42478: % of 1 / 299.792.458 second; one kilogram is the weight of a neuper@42478: % platinum-iridium cylinder in paris; and so on. But are these neuper@42478: % definitions usable in a computer mechanized world?! neuper@42478: % }} neuper@42478: % \end{example} neuper@42478: % } neuper@42478: % neuper@42478: % \paragraph{A computer} or a TP-System builds on programs with neuper@42478: % predefined logical rules and does not know any mathematical trick neuper@42478: % (follow up example \ref{eg:trick}) or recipe to walk around difficult neuper@42478: % expressions. neuper@42478: % neuper@42478: % \vbox{ neuper@42478: % \begin{example} neuper@42478: % \label{eg:trick} neuper@42478: % \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] neuper@42478: % \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= neuper@42478: % \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] neuper@42478: % \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] neuper@42478: % {\small\textit{ neuper@42478: % \noindent Sometimes it is also useful to be able to apply some neuper@42478: % \emph{tricks} to get a beautiful and particularly meaningful result, neuper@42478: % which we are able to interpret. But as seen in this example it can be neuper@42478: % hard to find out what operations have to be done to transform a result neuper@42478: % into a meaningful one. neuper@42478: % }} neuper@42478: % \end{example} neuper@42478: % } neuper@42478: % neuper@42478: % \paragraph{The only possibility,} for such a system, is to work neuper@42478: % through its known definitions and stops if none of these neuper@42478: % fits. Specified on Signal Processing or any other application it is neuper@42478: % often possible to walk through by doing simple creases. This creases neuper@42478: % are in general based on simple math operational but the challenge is neuper@42478: % to teach the machine \emph{all}\footnote{Its pride to call it neuper@42478: % \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to neuper@42478: % reach a high level of \emph{all} but it in real it will still be a neuper@42478: % survey of knowledge which links to other knowledge and {{\sisac}{}} a neuper@42478: % trainer and helper but no human compensating calculator. neuper@42478: % \par neuper@42478: % {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal neuper@42478: % specifications of problems out of topics from Signal Processing, etc.) neuper@42478: % and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of neuper@42478: % physical knowledge. The result is a three-dimensional universe of neuper@42478: % mathematics seen in Figure~\ref{fig:mathuni}. neuper@42478: % neuper@42478: % \begin{figure} neuper@42478: % \begin{center} neuper@42478: % \includegraphics{fig/universe} neuper@42478: % \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is neuper@42478: % combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result neuper@42478: % leads to a three dimensional math universe.\label{fig:mathuni}} neuper@42478: % \end{center} neuper@42478: % \end{figure} neuper@42478: % neuper@42478: % %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen; neuper@42478: % %WN bitte folgende Bezeichnungen nehmen: neuper@42478: % %WN neuper@42478: % %WN axis 1: Algorithmic Knowledge (Programs) neuper@42478: % %WN axis 2: Application-oriented Knowledge (Specifications) neuper@42478: % %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems) neuper@42478: % %WN neuper@42478: % %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf neuper@42478: % %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz neuper@42478: % %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken) neuper@42478: % neuper@42478: % %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's neuper@42478: % %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's neuper@42478: % %JR gefordert werden WN2... neuper@42478: % %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann neuper@42478: % %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse neuper@42478: % %WN2 zusammenschneiden um die R"ander weg zu bekommen) neuper@42478: % %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und neuper@42478: % %WN2 png + pdf figures mitzuschicken. neuper@42478: % neuper@42478: % \subsection{Notes on Problems with Traditional Notation} neuper@42478: % neuper@42478: % \paragraph{During research} on these topic severely problems on neuper@42478: % traditional notations have been discovered. Some of them have been neuper@42478: % known in computer science for many years now and are still unsolved, neuper@42478: % one of them aggregates with the so called \emph{Lambda Calculus}, neuper@42478: % Example~\ref{eg:lamda} provides a look on the problem that embarrassed neuper@42478: % us. neuper@42478: % neuper@42478: % \vbox{ neuper@42478: % \begin{example} neuper@42478: % \label{eg:lamda} neuper@42478: % neuper@42478: % \[ f(x)=\ldots\; \quad R \rightarrow \quad R \] neuper@42478: % neuper@42478: % neuper@42478: % \[ f(p)=\ldots\; p \in \quad R \] neuper@42478: % neuper@42478: % {\small\textit{ neuper@42478: % \noindent Above we see two equations. The first equation aims to neuper@42478: % be a mapping of an function from the reel range to the reel one, but neuper@42478: % when we change only one letter we get the second equation which neuper@42478: % usually aims to insert a reel point $p$ into the reel function. In neuper@42478: % computer science now we have the problem to tell the machine (TP) the neuper@42478: % difference between this two notations. This Problem is called neuper@42478: % \emph{Lambda Calculus}. neuper@42478: % }} neuper@42478: % \end{example} neuper@42478: % } neuper@42478: % neuper@42478: % \paragraph{An other problem} is that terms are not full simplified in neuper@42478: % traditional notations, in {{\sisac}} we have to simplify them complete neuper@42478: % to check weather results are compatible or not. in e.g. the solutions neuper@42478: % of an second order linear equation is an rational in {{\sisac}} but in neuper@42478: % tradition we keep fractions as long as possible and as long as they neuper@42478: % aim to be \textit{beautiful} (1/8, 5/16,...). neuper@42478: % \subparagraph{The math} which should be mechanized in Computer Theorem neuper@42478: % Provers (\emph{TP}) has (almost) a problem with traditional notations neuper@42478: % (predicate calculus) for axioms, definitions, lemmas, theorems as a neuper@42478: % computer program or script is not able to interpret every Greek or neuper@42478: % Latin letter and every Greek, Latin or whatever calculations neuper@42478: % symbol. Also if we would be able to handle these symbols we still have neuper@42478: % a problem to interpret them at all. (Follow up \hbox{Example neuper@42478: % \ref{eg:symbint1}}) neuper@42478: % neuper@42478: % \vbox{ neuper@42478: % \begin{example} neuper@42478: % \label{eg:symbint1} neuper@42478: % \[ neuper@42478: % u\left[n\right] \ \ldots \ unitstep neuper@42478: % \] neuper@42478: % {\small\textit{ neuper@42478: % \noindent The unitstep is something we need to solve Signal neuper@42478: % Processing problem classes. But in {{{\sisac}{}}} the rectangular neuper@42478: % brackets have a different meaning. So we abuse them for our neuper@42478: % requirements. We get something which is not defined, but usable. The neuper@42478: % Result is syntax only without semantic. neuper@42478: % }} neuper@42478: % \end{example} neuper@42478: % } neuper@42478: % neuper@42478: % In different problems, symbols and letters have different meanings and neuper@42478: % ask for different ways to get through. (Follow up \hbox{Example neuper@42478: % \ref{eg:symbint2}}) neuper@42478: % neuper@42478: % \vbox{ neuper@42478: % \begin{example} neuper@42478: % \label{eg:symbint2} neuper@42478: % \[ neuper@42478: % \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent neuper@42478: % \] neuper@42478: % {\small\textit{ neuper@42478: % \noindent For using exponents the three \texttt{widehat} symbols neuper@42478: % are required. The reason for that is due the development of neuper@42478: % {{{\sisac}{}}} the single \texttt{widehat} and also the double were neuper@42478: % already in use for different operations. neuper@42478: % }} neuper@42478: % \end{example} neuper@42478: % } neuper@42478: % neuper@42478: % \paragraph{Also the output} can be a problem. We are familiar with a neuper@42478: % specified notations and style taught in university but a computer neuper@42478: % program has no knowledge of the form proved by a professor and the neuper@42478: % machines themselves also have not yet the possibilities to print every neuper@42478: % symbol (correct) Recent developments provide proofs in a human neuper@42478: % readable format but according to the fact that there is no money for neuper@42478: % good working formal editors yet, the style is one thing we have to neuper@42478: % live with. neuper@42478: % neuper@42478: % \section{Problems rising out of the Development Environment} neuper@42478: % neuper@42478: % fehlermeldungen! TODO jan@42463: neuper@42492: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim} neuper@42492: neuper@42464: \section{Conclusion}\label{conclusion} neuper@42492: This paper gives a first experience report about programming with a neuper@42492: TP-based programming language. jan@42463: neuper@42492: \medskip A brief re-introduction of the novel kind of programming neuper@42492: language by example of the {\sisac}-prototype makes the paper neuper@42492: self-contained. The main section describes all the main concepts neuper@42492: involved in TP-based programming and all the sub-tasks concerning neuper@42492: respective implementation: mechanisation of mathematics and domain neuper@42492: modelling, implementation of term rewriting systems for the neuper@42492: rewriting-engine, formal (implicit) specification of the problem to be neuper@42492: (explicitly) described by the program, implement the many components neuper@42492: required for Lucas-Interpretation and finally implementation of the neuper@42492: program itself. neuper@42492: neuper@42492: The many concepts and sub-tasks involved in programming require a neuper@42492: comprehensive workflow; first experiences with the workflow as neuper@42492: supported by the present prototype are described as well: Isabelle + neuper@42492: Isar + jEdit provide appropriate components for establishing an neuper@42492: efficient development environment integrating computation and neuper@42492: deduction. However, the present state of the prototype is far off a neuper@42492: state appropriate for wide-spread use: the prototype of the program neuper@42492: language lacks expressiveness and elegance, the prototype of the neuper@42492: development environment is hardly usable: error messages still address neuper@42492: the developer of the prototype's interpreter rather than the neuper@42492: application programmer, implementation of the many settings for the neuper@42492: Lucas-Interpreter is cumbersome. neuper@42492: neuper@42492: From these experiences a successful proof of concept can be concluded: neuper@42492: programming arbitrary problems from engineering sciences is possible, neuper@42492: in principle even in the prototype. Furthermore the experiences allow neuper@42492: to conclude detailed requirements for further development: neuper@42492: \begin{itemize} neuper@42492: \item Clarify underlying logics such that programming is smoothly neuper@42492: integrated with verification of the program; the post-condition should neuper@42492: be proved more or less automatically, otherwise working engineers neuper@42492: would not encounter such programming. neuper@42492: \item Combine the prototype's programming language with Isabelle's neuper@42492: powerful function package and probably with more of SML's neuper@42492: pattern-matching features; include parallel execution on multi-core neuper@42492: machines into the language desing. neuper@42492: \item Extend the prototype's Lucas-Interpreter such that it also neuper@42492: handles functions defined by use of Isabelle's functions package; and neuper@42492: generalize Isabelle's code generator such that efficient code for the neuper@42492: whole of the defined programming language can be generated (for neuper@42492: multi-core machines). neuper@42492: \item Develop an efficient development environment with neuper@42492: integration of programming and proving, with management not only of neuper@42492: Isabelle theories, but also of large collections of specifications and neuper@42492: of programs. neuper@42492: \end{itemize} neuper@42492: Provided successful accomplishment, these points provide distinguished neuper@42492: components for virtual workbenches appealing to practictioner of neuper@42492: engineering in the near future. neuper@42492: neuper@42492: \medskip And all programming with a TP-based language will neuper@42492: subsequently create interactive tutoring as a side-effect: neuper@42492: Lucas-Interpretation not only provides an interactive programming neuper@42492: environment, Lucas-Interpretation also can provide TP-based services neuper@42492: for a flexible dialog component with adaptive user guidance for neuper@42492: independent and inquiry-based learning. neuper@42492: jan@42463: jan@42463: \bibliographystyle{alpha} jan@42463: \bibliography{references} jan@42463: jan@42463: \end{document}