%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Electronic Journal of Mathematics and Technology (eJMT) %

% style sheet for LaTeX.  Please do not modify sections   %

% or commands marked 'eJMT'.                              %

%                                                         %

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%                                                         %

% eJMT commands                                           %

%                                                         %

\documentclass[12pt,a4paper]{article}%                    %

\usepackage{times}                                        %

\usepackage{amsfonts,amsmath,amssymb}                     %

\usepackage[a4paper]{geometry}                            %

\usepackage{fancyhdr}                                     %

\usepackage{color}                                        %

\usepackage[pdftex]{hyperref} % see note below            %

\usepackage{graphicx}%                                    %

\hypersetup{                                              %

    a4paper,                                              %

    breaklinks                                            %

}                                                         %

%                                                         %

\newtheorem{theorem}{Theorem}                             %

\newtheorem{acknowledgement}[theorem]{Acknowledgement}    %

\newtheorem{algorithm}[theorem]{Algorithm}                %

\newtheorem{axiom}[theorem]{Axiom}                        %

\newtheorem{case}[theorem]{Case}                          %

\newtheorem{claim}[theorem]{Claim}                        %

\newtheorem{conclusion}[theorem]{Conclusion}              %

\newtheorem{condition}[theorem]{Condition}                %

\newtheorem{conjecture}[theorem]{Conjecture}              %

\newtheorem{corollary}[theorem]{Corollary}                %

\newtheorem{criterion}[theorem]{Criterion}                %

\newtheorem{definition}[theorem]{Definition}              %

\newtheorem{example}[theorem]{Example}                    %

\newtheorem{exercise}[theorem]{Exercise}                  %

\newtheorem{lemma}[theorem]{Lemma}                        %

\newtheorem{notation}[theorem]{Notation}                  %

\newtheorem{problem}[theorem]{Problem}                    %

\newtheorem{proposition}[theorem]{Proposition}            %

\newtheorem{remark}[theorem]{Remark}                      %

\newtheorem{solution}[theorem]{Solution}                  %

\newtheorem{summary}[theorem]{Summary}                    %

\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }  %

{\ \rule{0.5em}{0.5em}}                                   %

%                                                         %

% eJMT page dimensions                                    %

%                                                         %

\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm}        %

%                                                         %

% eJMT header & footer                                    %

%                                                         %

\newcounter{ejmtFirstpage}                                %

\setcounter{ejmtFirstpage}{1}                             %

\pagestyle{empty}                                         %

\setlength{\headheight}{14pt}                             %

\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm}        %

\pagestyle{fancyplain}                                    %

\fancyhf{}                                                %

\fancyhead[c]{\small The Electronic Journal of Mathematics%

\ and Technology, Volume 1, Number 1, ISSN 1933-2823}     %

\cfoot{%                                                  %

  \ifnum\value{ejmtFirstpage}=0%                          %

    {\vtop to\hsize{\hrule\vskip .2cm\thepage}}%          %

  \else\setcounter{ejmtFirstpage}{0}\fi%                  %

}                                                         %

%                                                         %

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%

% Please place your own definitions here

%

\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

\usepackage{color}

\definecolor{lgray}{RGB}{238,238,238}

%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%                                                         %

% How to use hyperref                                     %

% -------------------                                     %

%                                                         %

% Probably the only way you will need to use the hyperref %

% package is as follows.  To make some text, say          %

% "My Text Link", into a link to the URL                  %

% http://something.somewhere.com/mystuff, use             %

%                                                         %

% \href{http://something.somewhere.com/mystuff}{My Text Link}

%                                                         %

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%

\begin{document}

%

% document title

%

\title{Trials with TP-based Programming

\\

for Interactive Course Material}%

%

% Single author.  Please supply at least your name,

% email address, and affiliation here.

%

\author{\begin{tabular}{c}

\textit{Jan Ro\v{c}nik} \\

jan.rocnik@student.tugraz.at \\

IST, SPSC\\

Graz University of Technologie\\

Austria\end{tabular}

}%

%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%                                                         %

% eJMT commands - do not change these                     %

%                                                         %

\date{}                                                   %

\maketitle                                                %

%                                                         %

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%

% abstract

%

\begin{abstract}

Traditional course material in engineering disciplines lacks an

important component, interactive support for step-wise problem

solving. Theorem-Proving (TP) technology is appropriate for one part

of such support, in checking user-input. For the other part of such

support, guiding the learner towards a solution, another kind of

technology is required. %TODO ... connect to prototype ...

Both kinds of support can be acchieved by so-called

Lucas-Interpretation which combines deduction and computation and, for

the latter, uses a novel kind of programming language. This language

is based on (Computer) Theorem Proving (TP), thus called a ``TP-based

programming language''.

This paper is the experience report of the first ``application

programmer'' using this language for creating exercises in step-wise

problem solving for an advanced lab in Signal Processing. The tasks

involved in TP-based programming are described together with the

experience gained from a prototype of the programming language and of

it's interpreter.

The report concludes with a positive proof of concept, states

insuggicient usability of the prototype and captures the requirements

for further development of both, the programming language and the

interpreter.

%

\end{abstract}%

%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%                                                         %

% eJMT command                                            %

%                                                         %

\thispagestyle{fancy}                                     %

%                                                         %

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%

% Please use the following to indicate sections, subsections,

% etc.  Please also use \subsubsection{...}, \paragraph{...}

% and \subparagraph{...} as necessary.

%

\section{Introduction}\label{intro}

% \paragraph{Didactics of mathematics} 

%WN: wenn man in einem high-quality paper von 'didactics' spricht, 

%WN muss man am state-of-the-art ankn"upfen -- siehe

%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants

% faces a specific issue, a gap

% between (1) introduction of math concepts and skills and (2)

% application of these concepts and skills, which usually are separated

% into different units in curricula (for good reasons). For instance,

% (1) teaching partial fraction decomposition is separated from (2)

% application for inverse Z-transform in signal processing.

% 

% \par This gap is an obstacle for applying math as an fundamental

% thinking technology in engineering: In (1) motivation is lacking

% because the question ``What is this stuff good for?'' cannot be

% treated sufficiently, and in (2) the ``stuff'' is not available to

% students in higher semesters as widespread experience shows.

% 

% \paragraph{Motivation} taken by this didactic issue on the one hand,

% and ongoing research and development on a novel kind of educational

% mathematics assistant at Graz University of

% Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to

% scope with this issue on the other hand, several institutes are

% planning to join their expertise: the Institute for Information

% Systems and Computer Media (IICM), the Institute for Software

% Technology (IST), the Institutes for Mathematics, the Institute for

% Signal Processing and Speech Communication (SPSC), the Institute for

% Structural Analysis and the Institute of Electrical Measurement and

% Measurement Signal Processing.

%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell 

%WN und damit zu verg"anglich.

% \par This thesis is the first attempt to tackle the above mentioned

% issue, it focuses on Telematics, because these specific studies focus

% on mathematics in \emph{STEOP}, the introductory orientation phase in

% Austria. \emph{STEOP} is considered an opportunity to investigate the

% impact of {\sisac}'s prototype on the issue and others.

% 

Traditional course material in engineering disciplines lacks an

important component, interactive support for step-wise problem

solving. Theorem-Proving (TP) technology can provide such support by

specific services. An important part of such services is called

``next-step-guidance'', generated by a specific kind of ``TP-based

programming language''. In the

{\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such

a language is prototyped in line with~\cite{plmms10} and built upon

the theorem prover

Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.

The TP services are coordinated by a specific interpreter for the

programming language, called

Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the

interpreter will be briefly re-introduced in order to make the paper

self-contained.

The main part of the paper is an account of first experiences

with programming in this TP-based language. The experience was gained

in a case study by the author. The author was considered an ideal

candidate for this study for the following reasons: as a student in

Telematics (computer science with focus on Signal Processing) he had

general knowledge in programming as well as specific domain knowledge

in Signal Processing; and he was {\em not} involved in the development of

{\sisac}'s programming language and interpeter, thus a novice to the

language.

The goal of the case study was (1) some TP-based programs for

interactive course material for a specific ``Adavanced Signal

Processing Lab'' in a higher semester, (2) respective program

development with as little advice from the {\sisac}-team and (3) records

and comments for the main steps of development in an Isabelle theory;

this theory should provide guidelines for future programmers. An

excerpt from this theory is the main part of this paper.

\par

The paper will use the problem in Fig.\ref{fig-interactive} as a

running example:

\begin{figure} [htb]

\begin{center}

\includegraphics[width=140mm]{fig/isac-Ztrans-math-3}

%\includegraphics[width=140mm]{fig/isac-Ztrans-math}

\caption{Step-wise problem solving guided by the TP-based program}

\label{fig-interactive}

\end{center}

\end{figure}

The problem is from the domain of Signal Processing and requests to

determine the inverse ${\cal Z}$-transform for a given term. Fig.\ref{fig-interactive}

also shows the beginning of the interactive construction of a solution

for the problem. This construction is done in the right window named

``Worksheet''.

\par

User-interaction on the Worksheet is {\em checked} and {\em guided} by

TP services:

\begin{enumerate}

\item Formulas input by the user are {\em checked} by TP: such a

formula establishes a proof situation --- the prover has to derive the

formula from the logical context. The context is built up from the

formal specification of the problem (here hidden from the user) by the

Lucas-Interpreter.

\item If the user gets stuck, the program developed below in this

paper ``knows the next step'' and Lucas-Interpretation provides services

featuring so-called ``next-step-guidance''; this is out of scope of this

paper and can be studied in~\cite{gdaroczy-EP-13}.

\end{enumerate} It should be noted that the programmer using the

TP-based language is not concerned with interaction at all; we will

see that the program contains neither input-statements nor

output-statements. Rather, interaction is handled by the interpreter

pf the language.

So there is a clear separation of concerns: Dialogues are adapted by

dialogue authors (in Java-based tools), using TP services provided by

Lucas-Interpretation. The latter acts on programs developed by

mathematics-authors (in Isabelle/ML); their task is concern of this

paper.

\paragraph{The paper is structed} as follows: The introduction

\S\ref{intro} is followed by a brief re-introduction of the TP-based

programming language in \S\ref{PL}, which extends the executable

fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which

play a specific role in Lucas-Interpretation and in providing the TP

services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes

the main steps in developing the program for the running example:

prepare domain knowledge, implement the formal specification of the

problem, prepare the environment for the interpreter, implement the

program in \S\ref{isabisac} to \S\ref{progr} respectively. 

The workflow of programming, debugging and testing is

described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will

give directions identified for future development. 

\section{\isac's Prototype for a Programming Language}\label{PL} 

The prototype of the language and of the Lucas-Interpreter are briefly

described from the point of view of a programmer. The language extends

the executable fragment in the language of the theorem prover

Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.

\subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}

The executable fragment consists of data-type and function

definitions.  It's usability even suggests that fragment for

introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic

whose type system resembles that of functional programming

languages. Thus there are

\begin{description}

\item[base types,] in particular \textit{bool}, the type of truth

values, \textit{nat}, \textit{int}, \textit{complex}, and the types of

natural, integer and complex numbers respectively in mathematics.

\item[type constructors] allow to define arbitrary types, from

\textit{set}, \textit{list} to advanced data-structures like

\textit{trees}, red-black-trees etc.

\item[function types,] denoted by $\Rightarrow$.

\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide

type polymorphism. Isabelle automatically computes the type of each

variable in a term by use of Hindley-Milner type inference

\cite{pl:hind97,Milner-78}.

\end{description}

\textbf{Terms} are formed as in functional programming by applying

functions to arguments. If $f$ is a function of type

$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then

$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$

has type $\tau$. There are many predefined infix symbols like $+$ and

$\leq$ most of which are overloaded for various types.

HOL also supports some basic constructs from functional programming:

{\it\label{isabelle-stmts}

\begin{tabbing} 123\=\kill

\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\

\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\

\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1

  \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$

\end{tabbing} }

\noindent The running example's program uses some of these elements

(marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt

let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program

is an Isabelle term with specific function constants like {\tt

program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt

Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}

respectively.

% Terms may also contain $\lambda$-abstractions. For example, $\lambda

% x. \; x$ is the identity function.

%JR warum auskommentiert? WN2...

%WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb

%WN2 des Papers auftauchen m"usste; nachdem ich einen solchen

%WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht

%WN2 gel"oscht.

%WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen

%WN2 Platz f"ur Anderes weg.

\textbf{Formulae} are terms of type \textit{bool}. There are the basic

constants \textit{True} and \textit{False} and the usual logical

connectives (in decreasing order of precedence): $\neg, \land, \lor,

\rightarrow$.

\textbf{Equality} is available in the form of the infix function $=$

of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for

formulas, where it means ``if and only if''.

\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;

P$.  Quantifiers lead to non-executable functions, so functions do not

always correspond to programs, for instance, if comprising \\$(

\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2

\;)$.

\subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}

The prototype extends Isabelle's language by specific statements

called tactics~\footnote{{\sisac}'s tactics are different from

Isabelle's tactics: the former concern steps in a calculation, the

latter concern proofs.}  and tacticals. For the programmer these

statements are functions with the following signatures:

\begin{description}

\item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it

term} * {\it term}\;{\it list}$:

this tactic appplies {\it theorem} to a {\it term} yielding a {\it

term} and a {\it term list}, the list are assumptions generated by

conditional rewriting. For instance, the {\it theorem}

$b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$

applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields

$(\frac{2}{3}, [x\not=0])$.

\item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it

term}\Rightarrow{\it term} * {\it term}\;{\it list}$:

this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is

a confluent and terminating term rewrite system, in general. If

none of the rules ({\it theorem}s) is applicable on interpretation

of this tactic, an exception is thrown.

% \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it

% theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it

% list}$:

% 

% \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it

% ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it

% list}$:

%SPACEvvv

\item[Substitute:] ${\it substitution}\Rightarrow{\it

term}\Rightarrow{\it term}$: allows to access sub-terms.

%SPACE^^^

\item[Take:] ${\it term}\Rightarrow{\it term}$:

this tactic has no effect in the program; but it creates a side-effect

by Lucas-Interpretation (see below) and writes {\it term} to the

Worksheet.

\item[Subproblem:] ${\it theory} * {\it specification} * {\it

method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:

this tactic is a generalisation of a function call: it takes an

\textit{argument list} as usual, and additionally a triple consisting

of an Isabelle \textit{theory}, an implicit \textit{specification} of the

program and a \textit{method} containing data for Lucas-Interpretation,

last not least a program (as an explicit specification)~\footnote{In

interactive tutoring these three items can be determined explicitly

by the user.}.

\end{description}

The tactics play a specific role in

Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as

break-points where, as a side-effect, a line is added to a calculation

as a protocol for proceeding towards a solution in step-wise problem

solving. At the same points Lucas-Interpretation serves interactive

tutoring and hands over control to the user. The user is free to

investigate underlying knowledge, applicable theorems, etc.  And the

user can proceed constructing a solution by input of a tactic to be

applied or by input of a formula; in the latter case the

Lucas-Interpreter has built up a logical context (initialised with the

precondition of the formal specification) such that Isabelle can

derive the formula from this context --- or give feedback, that no

derivation can be found.

\subsection{Tacticals as Control Flow Statements}

The flow of control in a program can be determined by {\tt if then else}

and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also

by additional tacticals:

\begin{description}

\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it

term}$: iterates over tactics which take a {\it term} as argument as

long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might

not be applicable).

\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:

if {\it tactic} is applicable, then it is applied to {\it term},

otherwise {\it term} is passed on without changes.

\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it

term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,

it is applied to the first {\it term} yielding another {\it term},

otherwise the second {\it tactic} is applied; if none is applicable an

exception is raised.

\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it

term}\Rightarrow{\it term}$: applies the first {\it tactic} to the

first {\it term} yielding an intermediate term (not appearing in the

signature) to which the second {\it tactic} is applied.

\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it

term}\Rightarrow{\it term}$: if the first {\it term} is true, then the

{\it tactic} is applied to the first {\it term} yielding an

intermediate term (not appearing in the signature); the intermediate

term is added to the environment the first {\it term} is evaluated in

etc as long as the first {\it term} is true.

\end{description}

The tacticals are not treated as break-points by Lucas-Interpretation

and thus do neither contribute to the calculation nor to interaction.

\section{Concepts and Tasks in TP-based Programming}\label{trial}

%\section{Development of a Program on Trial}

This section presents all the concepts involved in TP-based

programming and all the tasks to be accomplished by programmers. The

presentation uses the running example from

Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.

\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}

%WN was Fachleute unter obigem Titel interessiert findet sich

%WN unterhalb des auskommentierten Textes.

%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell

%WN auf Computer-Mathematiker fokussiert.

% \paragraph{As mentioned in the introduction,} a prototype of an

% educational math assistant called

% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for

% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges

% the gap between (1) introducation and (2) application of mathematics:

% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which

% requires each fact and each action justified by formal logic, so

% {{{\sisac}{}}} makes justifications transparent to students in

% interactive step-wise problem solving. By that way {{\sisac}} already

% can serve both:

% \begin{enumerate}

%   \item Introduction of math stuff (in e.g. partial fraction

% decomposition) by stepwise explaining and exercising respective

% symbolic calculations with ``next step guidance (NSG)'' and rigorously

% checking steps freely input by students --- this also in context with

% advanced applications (where the stuff to be taught in higher

% semesters can be skimmed through by NSG), and

%   \item Application of math stuff in advanced engineering courses

% (e.g. problems to be solved by inverse Z-transform in a Signal

% Processing Lab) and now without much ado about basic math techniques

% (like partial fraction decomposition): ``next step guidance'' supports

% students in independently (re-)adopting such techniques.

% \end{enumerate} 

% Before the question is answers, how {{\sisac}}

% accomplishes this task from a technical point of view, some remarks on

% the state-of-the-art is given, therefor follow up Section~\ref{emas}.

% 

% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}

% 

% \paragraph{Educational software in mathematics} is, if at all, based

% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry

% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}

% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC

% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These

% base technologies are used to program math lessons and sometimes even

% exercises. The latter are cumbersome: the steps towards a solution of

% such an interactive exercise need to be provided with feedback, where

% at each step a wide variety of possible input has to be foreseen by

% the programmer - so such interactive exercises either require high

% development efforts or the exercises constrain possible inputs.

% 

% \subparagraph{A new generation} of educational math assistants (EMAs)

% is emerging presently, which is based on Theorem Proving (TP). TP, for

% instance Isabelle and Coq, is a technology which requires each fact

% and each action justified by formal logic. Pushed by demands for

% \textit{proven} correctness of safety-critical software TP advances

% into software engineering; from these advancements computer

% mathematics benefits in general, and math education in particular. Two

% features of TP are immediately beneficial for learning:

% 

% \paragraph{TP have knowledge in human readable format,} that is in

% standard predicate calculus. TP following the LCF-tradition have that

% knowledge down to the basic definitions of set, equality,

% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};

% following the typical deductive development of math, natural numbers

% are defined and their properties

% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},

% etc. Present knowledge mechanized in TP exceeds high-school

% mathematics by far, however by knowledge required in software

% technology, and not in other engineering sciences.

% 

% \paragraph{TP can model the whole problem solving process} in

% mathematical problem solving {\em within} a coherent logical

% framework. This is already being done by three projects, by

% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.

% \par

% Having the whole problem solving process within a logical coherent

% system, such a design guarantees correctness of intermediate steps and

% of the result (which seems essential for math software); and the

% second advantage is that TP provides a wealth of theories which can be

% exploited for mechanizing other features essential for educational

% software.

% 

% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}

% 

% One essential feature for educational software is feedback to user

% input and assistance in coming to a solution.

% 

% \paragraph{Checking user input} by ATP during stepwise problem solving

% is being accomplished by the three projects mentioned above

% exclusively. They model the whole problem solving process as mentioned

% above, so all what happens between formalized assumptions (or formal

% specification) and goal (or fulfilled postcondition) can be

% mechanized. Such mechanization promises to greatly extend the scope of

% educational software in stepwise problem solving.

% 

% \paragraph{NSG (Next step guidance)} comprises the system's ability to

% propose a next step; this is a challenge for TP: either a radical

% restriction of the search space by restriction to very specific

% problem classes is required, or much care and effort is required in

% designing possible variants in the process of problem solving

% \cite{proof-strategies-11}.

% \par

% Another approach is restricted to problem solving in engineering

% domains, where a problem is specified by input, precondition, output

% and postcondition, and where the postcondition is proven by ATP behind

% the scenes: Here the possible variants in the process of problem

% solving are provided with feedback {\em automatically}, if the problem

% is described in a TP-based programing language: \cite{plmms10} the

% programmer only describes the math algorithm without caring about

% interaction (the respective program is functional and even has no

% input or output statements!); interaction is generated as a

% side-effect by the interpreter --- an efficient separation of concern

% between math programmers and dialog designers promising application

% all over engineering disciplines.

% 

% 

% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}

% Authoring new mathematics knowledge in {{\sisac}} can be compared with

% ``application programing'' of engineering problems; most of such

% programing uses CAS-based programing languages (CAS = Computer Algebra

% Systems; e.g. Mathematica's or Maple's programing language).

% 

% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}

% \cite{plmms10} for describing how to construct a solution to an

% engineering problem and for calling equation solvers, integration,

% etc~\footnote{Implementation of CAS-like functionality in TP is not

% primarily concerned with efficiency, but with a didactic question:

% What to decide for: for high-brow algorithms at the state-of-the-art

% or for elementary algorithms comprehensible for students?} within TP;

% TP can ensure ``systems that never make a mistake'' \cite{casproto} -

% are impossible for CAS which have no logics underlying.

% 

% \subparagraph{Authoring is perfect} by writing such TP based programs;

% the application programmer is not concerned with interaction or with

% user guidance: this is concern of a novel kind of program interpreter

% called Lucas-Interpreter. This interpreter hands over control to a

% dialog component at each step of calculation (like a debugger at

% breakpoints) and calls automated TP to check user input following

% personalized strategies according to a feedback module.

% \par

% However ``application programing with TP'' is not done with writing a

% program: according to the principles of TP, each step must be

% justified. Such justifications are given by theorems. So all steps

% must be related to some theorem, if there is no such theorem it must

% be added to the existing knowledge, which is organized in so-called

% \textbf{theories} in Isabelle. A theorem must be proven; fortunately

% Isabelle comprises a mechanism (called ``axiomatization''), which

% allows to omit proofs. Such a theorem is shown in

% Example~\ref{eg:neuper1}.

The running example requires to determine the inverse $\cal

Z$-transform for a class of functions. The domain of Signal Processing

is accustomed to specific notation for the resulting functions, which

are absolutely summable and are called step-response: $u[n]$, where $u$ is the

function, $n$ is the argument and the brackets indicate that the

arguments are discrete. Surprisingly, Isabelle accepts the rules for

${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle

experts might be particularly surprised, that the brackets do not

cause errors in typing (as lists).}:

%\vbox{

% \begin{example}

  \label{eg:neuper1}

  {\small\begin{tabbing}

  123\=123\=123\=123\=\kill

  \hfill \\

  \>axiomatization where \\

  \>\>  rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\

  \>\>  rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\

  \>\>  rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\

%TODO

  \>\>  rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\

%TODO

  \>\>  rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\

%TODO

  \>\>  rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\

%TODO

  \end{tabbing}

  }

% \end{example}

%}

These 6 rules can be used as conditional rewrite rules, depending on

the respective convergence radius. Satisfaction from accordance with traditional notation

contrasts with the above word {\em axiomatization}: As TP-based, the

programming language expects these rules as {\em proved} theorems, and

not as axioms implemented in the above brute force manner; otherwise

all the verification efforts envisaged (like proof of the

post-condition, see below) would be meaningless.

Isabelle provides a large body of knowledge, rigorously proven from

the basic axioms of mathematics~\footnote{This way of rigorously

deriving all knowledge from first principles is called the

LCF-paradigm in TP.}. In the case of the ${\cal Z}$-Transform the most advanced

knowledge can be found in the theoris on Multivariate

Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,

building up knowledge such that a proof for the above rules would be

reasonably short and easily comprehensible, still requires lots of

work (and is definitely out of scope of our case study).

At the state-of-the-art in mechanization of knowledge in engineering

sciences, the process does not stop with the mechanization of

mathematics traditionally used in these sciences. Rather, ``Formal

Methods''~\cite{ fm-03} are expected to proceed to formal and explicit

description of physical items.  Signal Processing, for instance is

concerned with physical devices for signal acquisition and

reconstruction, which involve measuring a physical signal, storing it,

and possibly later rebuilding the original signal or an approximation

thereof. For digital systems, this typically includes sampling and

quantization; devices for signal compression, including audio

compression, image compression, and video compression, etc.  ``Domain

engineering''\cite{db:dom-eng} is concerned with {\em specification}

of these devices' components and features; this part in the process of

mechanization is only at the beginning in domains like Signal

Processing.

TP-based programming, concern of this paper, is determined to

add ``algorithmic knowledge'' to the mechanised body of knowledge.

% in Fig.\ref{fig:mathuni} on

% p.\pageref{fig:mathuni}.  As we shall see below, TP-based programming

% starts with a formal {\em specification} of the problem to be solved.

% \begin{figure}

%   \begin{center}

%     \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}

%     \caption{The three-dimensional universe of mathematics knowledge}

%     \label{fig:mathuni}

%   \end{center}

% \end{figure}

% The language for both axes is defined in the axis at the bottom, deductive

% knowledge, in {\sisac} represented by Isabelle's theories.

\subsection{Preparation of Simplifiers for the Program}\label{simp}

All evaluation in the prototyp's Lucas-Interpreter is done by term rewriting on

Isabelle's terms, see \S\ref{meth} below; in this section some of respective

preparations are described. In order to work reliably with term rewriting, the

respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},

then they are called (canonical) simplifiers. These properties do not go without

saying, their establishment is a difficult task for the programmer; this task is

not yet supported in the prototype.\par

% If it is clear how the later calculation should look like

% %WN3 ... Allgem.<-->Konkret ist gut: aber hier ist 'calculation'

% %WN3 zu weit weg: der Satz geh"ort bestenfalls gleich an den

% %WN3 Anfang von \sect.3

% %WN3 

% %WN3 Im Folgenden sind einige Ungenauigkeiten:

%  and when

% which mathematic rule 

% %WN3 rewrite-rule oder theorem ! Ein Paper enth"alt viele Begriffe

% %WN3 und man versucht, die Anzahl so gering wie m"oglich zu halten

% %WN3 und die verbleibenden so pr"azise zu definieren wie m"oglich;

% %WN3 das Vermeiden von Wiederholungen muss mit anderen Mitteln erfolgen,

% %WN3 als dieselbe Sache mit verschiedenen Namen zu benennen;

% %WN3 das gilt insbesonders f"ur technische Begriffe wie oben

% should be applied, it can be started to find ways of

% simplifications. 

% %WN3 ... zu allgemein. Das Folgende w"urde durch einen Verweis in

% %WN3 das Programm auf S.12 gewinnen.

% This includes in e.g. the simplification of reational 

% expressions or also rewrites of an expession.

% \par

% %WN3 das Folgende habe ich aus dem Beispielprogramm auf S.12

% %WN3 gestrichen, weil es aus prinzipiellen Gr"unden unsch"on ist.

% %WN3 Und es ist so kompliziert dass es mehr Platz zum Erkl"aren

% %WN3 braucht, als es wert ist ...

% Obligate is the use of the function \texttt{drop\_questionmarks} 

% which excludes irrelevant symbols out of the expression. (Irrelevant symbols may 

% be result out of the system during the calculation. The function has to be

% applied for two reasons. First two make every placeholder in a expression 

% useable as a constant and second to provide a better view at the frontend.) 

% \par

% %WN3 Da kommt eine ganze Reihe von Ungenauigkeiten:

% Most rewrites are represented through rulesets

% %WN3 ... das ist schlicht falsch:

% %WN3 _alle_ rewrites werden durch rule-sets erzeugt (per definition

% %WN3 dieser W"orter).

%  this

% rulesets tell the machine which terms have to be rewritten into which

% representation. 

% %WN3 ... ist ein besonders "uberzeugendes Beispiel von Allgem.<-->Konkret:

% %WN3 so allgemein, wie es hier steht, ist es

% %WN3 # f"ur einen Fachmann klar und nicht ganz fachgem"ass formuliert

% %WN3   (a rule-set rewrites a certain term into another with certain properties)

% %WN3 # f"ur einen Nicht-Fachmann trotz allem unverst"andlich.

% %WN3 

% %WN3 Wenn schon allgemeine S"atze, dann unmittelbar auf das Beispiel

% %WN3 unten verweisen,

% %WN3 oder besser: den Satz dorthin schreiben, wo er unmittelbar vom

% %WN3 Beispiel gefolgt wird.

% In the upcoming programm a rewrite can be applied only in using

% such rulesets on existing terms.

% %WN3 Du willst wohl soetwas sagen wie ...

% %WN3 rewriting is the main concept to step-wise create and transform 

% %WN3 formulas in order to proceed towards a solution of a problem

% %WN3 ...?

% \paragraph{The core} of our implemented problem is the Z-Transformation

% %WN3 ^^^^^ ist nicht gut: was soll THE CORE vermitteln, wenn man die

% %WN3 Seite "uberfliegt ? Dass hier das Zentrum Deiner Arbeit liegt ?

% %WN3 

% %WN3 Das Folgende ist eine allgemeine Design-"Uberlegung, die entweder

% %WN3 vorne zur Einf"uhrung des Beispiels geh"ort,

% %WN3 oder zur konkreten L"osung durch die Rechnung auf S.15/16.

% (remember the description of the running example, introduced by

% Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the

% transformation itself would require higher math which isn't yet avaible in our system we decided to choose the way like it is applied in labratory and problem classes at our university - by applying transformation rules (collected in

% transformation tables).

% \par

% %WN3 Zum Folgenden: 'axiomatization' ist schon in 3.1. angesprochen:

% %WN3 entweder dort erg"anzen, wenn's wichtig ist, oder weglassen.

% Rules, in {\sisac{}}'s programming language can be designed by the use of

% axiomatization. In this axiomatization we declare how a term has to look like

% (left side) to be rewritten into another form (right side). Every line of this 

% axiomatizations starts with the name of the rule.

The prototype rewrites using theorems only. Axioms which are theorems as well 

have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we

assemble them in a rule-set and apply them as follows:

% %WN3 Die folgenden Zeilen nehmen Platz weg: von hier auf S.6 verweisen

% %\begin{example}

% {\footnotesize

%   \label{eg:ruledef}

% %  \hfill\\

%   \begin{verbatim}

%   axiomatization where

%     rule1: ``1 = $\delta$[n]'' and

%     rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and

%     rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''

% \end{verbatim}

% %\end{example}

% }

% 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.

%WN3 ... ist schon mehrmals gesagt worden. 1-mal pr"azise sagen gen"ugt.

%WN3 

%WN3 mit dem append_rls unten verbirgst Du die ganze Komplexit"at von

%WN3 rule-sets --- ich w"urde diese hier ausbreiten, damit man die

%WN3 Schwierigkeit von TP-based programming ermessen kann.

%WN3 Eine Erkl"arung wie in 3.4 und 3.5 braucht viel Platz, der sich

%WN3 meines Erachtens mehr auszahlt als die allgemeinen S"atze 

%WN3 am Ende von 3.2 auf S.8.

%WN3 

%WN3 mache ein 'grep -r "and rls";

%WN3 auch in Build_Inverse_Z_Transform.thy hast Du 'Rls'

%\begin{example}

%  \hfill\\

  \label{eg:ruleapp}

  \begin{enumerate}

  \item Store rules in ruleset:

  {\footnotesize\begin{verbatim}

01  val inverse_Z = append_rls "inverse_Z" e_rls

02    [ Thm ("rule1",num_str @{thm rule1}),

03      Thm ("rule2",num_str @{thm rule2}),

04      Thm ("rule3",num_str @{thm rule3})

05    ];\end{verbatim}}

  \item Define exression:

  {\footnotesize\begin{verbatim}

06  val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}}

%WN3 vergleiche bitte obige Zeile mit den letzten 3 Zeilen aus S.8,

%WN3 diese entsprechen dem g"angigen functional-programming Stil.

%WN3 Super w"ar's, wenn Du hier schon die interne Darstellung von

%WN3 Isabelle Termen zeigen k"onntest, dann w"urde ich den entsprechenden Teil

%WN3 am Ende von S.8 und Anfang S.9 (erste 2.1 Zeilen) l"oschen.

%JR ich habe einige male über seite acht gelesen, finde aber dass der teil über

%JR die interne representation dorthin besser passt da diese in unserem 

%JR gezeigten beispiel ja in direkter verbindung zur gezeigtem funktion besteht

%JR und so der übergang exzellent ist.

  \item Apply ruleset:

  {\footnotesize\begin{verbatim}

07  val SOME (sample_term', asm) = 

08    rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}}

  \end{enumerate}

%\end{example}

%WN3 Wie oben gesagt, die folgenden allgemeinen S"atze scheinen

%WN3 weniger wert als eine konkrete Beschreibung der rls-Struktur.

%WN3 

%WN3 Ich nehme an, wir l"oschen das Folgende

%WN3 und ich spare mir Kommentare (ausser Du hast noch Zeit/Energie

%WN3 daf"ur und fragst extra nach).

% The use of rulesets makes it much easier to develop our designated applications,

% but the programmer has to be careful and patient. When applying rulesets

% two important issues have to be mentionend:

% \begin{enumerate}

% \item How often the rules have to be applied? In case of

% transformations it is quite clear that we use them once but other fields

% reuqire to apply rules until a special condition is reached (e.g.

% a simplification is finished when there is nothing to be done left).

% \item The order in which rules are applied often takes a big effect

% and has to be evaluated for each purpose once again.

% \end{enumerate}

% In the special case of Signal Processing the rules defined in the

% Example upwards have to be applied in a dedicated order to transform all 

% constants first of all. After this first transformation step has been done it no 

% mather which rule fit's next.

%WN3 Beim Paper-Schreiben ist mir aufgefallen, dass eine Konstante ZZ_1

%WN3 (f"ur ${\cal Z}^{-1}$) die eben beschriebenen Probleme gel"ost

%WN3 h"atte: auf S.6 in rule1, auf S.12 in line 10 und in der Rechnung S.16

%WN3 hab' ich die Konstante schon eingef"uhrt.

%WN3 

%WN3 Bite bei der rewrite_set_ demo oben bitte schummeln !

%JR TODO es is klein z bitte auf S.6 in rule1, auf S.12 in line 10 ausbessern

%JR  ${\cal z}^{-1}$

In the first step of upper code we extend the method's own ruleset with

the predefined rules.\par

When adding rules to this set we already have to take care on the order the

rules we be applied in later context, this can be an important point when it

comes to a case where one rule has to be applied explicite before an other.

\par Rules are added to the ruleset with an unique name and a reference to their

defined theorem. After summerizing this rules we still have the posibility to

pick out a single one.

\par In upper example we define an expression, as it comes up in our running

example, it can be useful to take a look at \S\ref{funs} on p.\pageref{funs} to

get to know {\sisac}'s' internal representation of variables.

\par Upper step three is the final use of a ruleset for rewriting expression.

The inline declared \ttfamily sample\_term' \normalfont is the result of applying the upper

rule set one time to the before defined \texttt{sample\_term'}.

\subsection{Preparation of ML-Functions}\label{funs}

Some functionality required in programming, cannot be accomplished by

rewriting. So the prototype has a mechanism to call functions within

the rewrite-engine: certain redexes in Isabelle terms call these

functions written in SML~\cite{pl:milner97}, the implementation {\em

and} meta-language of Isabelle. The programmer has to use this

mechanism.

In the running example's program on p.\pageref{s:impl} the lines {\rm

05} and {\rm 06} contain such functions; we go into the details with

\textit{argument\_in X\_z;}. This function fetches the argument from a

function application: Line {\rm 03} in the example calculation on

p.\pageref{exp-calc} is created by line {\rm 06} of the example

program on p.\pageref{s:impl} where the program's environment assigns

the value \textit{X z} to the variable \textit{X\_z}; so the function

shall extract the argument \textit{z}.

\medskip In order to be recognised as a function constant in the

program source the constant needs to be declared in a theory, here in

\textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in

the context \textit{ctxt} of that theory:

{\footnotesize

\begin{verbatim}

   consts

     argument'_in :: "real => real" ("argument'_in _" 10)

\end{verbatim}}

%^3.2^    ML {* val SOME t = parse ctxt "argument_in (X z)"; *}

%^3.2^    val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real") 

%^3.2^              $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term

%^3.2^ \end{verbatim}}

%^3.2^ 

%^3.2^ \noindent Parsing produces a term \texttt{t} in internal

%^3.2^ representation~\footnote{The attentive reader realizes the 

%^3.2^ differences between interal and extermal representation even in the

%^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const

%^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",

%^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term

%^3.2^ constructor. 

The function body below is implemented directly in SML,

i.e in an \texttt{ML \{* *\}} block; the function definition provides

a unique prefix \texttt{eval\_} to the function name:

{\footnotesize

\begin{verbatim}

   ML {*

     fun eval_argument_in _ 

       "Build_Inverse_Z_Transform.argument'_in" 

       (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ =

         if is_Free arg (*could be something to be simplified before*)

         then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg)))

         else NONE

     | eval_argument_in _ _ _ _ = NONE;

   *}

\end{verbatim}}

\noindent The function body creates either creates \texttt{NONE}

telling the rewrite-engine to search for the next redex, or creates an

ad-hoc theorem for rewriting, thus the programmer needs to adopt many

technicalities of Isabelle, for instance, the \textit{Trueprop}

constant.

\bigskip This sub-task particularly sheds light on basic issues in the

design of a programming language, the integration of diffent language

layers, the layer of Isabelle/Isar and Isabelle/ML.

Another point of improvement for the prototype is the rewrite-engine: The

program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}

and {\rm 06} to

{\small\it\label{s:impl}

\begin{tabbing}

123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill

\>{\rm 05/6}\>\>\>  (z::real) = argument\_in (lhs X\_eq) ;

\end{tabbing}}

\noindent because nested function calls would require creating redexes

inside-out; however, the prototype's rewrite-engine only works top down

from the root of a term down to the leaves.