
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-</delta>)+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-</delta>)+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}



