
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: 
neuper@42464: % \paragraph{Didactics of mathematics} 
neuper@42464: %WN: wenn man in einem high-quality paper von 'didactics' spricht, 
neuper@42464: %WN muss man am state-of-the-art ankn"upfen -- siehe
neuper@42464: %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.
neuper@42464: %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell 
neuper@42464: %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: % 
neuper@42464: 
neuper@42464: 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: 
neuper@42464: \medskip 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: 
neuper@42464: 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.
neuper@42464: 
neuper@42464: \medskip 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@42464: \includegraphics[width=120mm]{fig/isac-Ztrans-math.png}
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}
neuper@42464: 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''.
neuper@42464: 
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.
neuper@42464: 
neuper@42464: \medskip 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.
neuper@42464: 
neuper@42464: \medskip 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} }
jan@42463: \noindent \textit{The running example's program uses some of these elements
jan@42463: (marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt
jan@42463: let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for
jan@42463: lists and {\tt o} for functional (forward) composition in line
jan@42463: $10$. In fact, the whole program is an Isabelle term with specific
jan@42463: function constants like {\sc program}, {\sc Substitute} and {\sc
jan@42463: Rewrite\_Set\_Inst} in lines $01$ and $10$ 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@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
jan@42463: term}\Rightarrow{\it term}$:
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}$:
jan@42463: this tactic allows to enter a phase of interactive specification
jan@42463: of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance,
jan@42463: a specific type of equation) and a method (for instance, solving an
jan@42463: equation symbolically or numerically).
jan@42463: 
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
jan@42463: break-points and control is handed over to the user. The user is free
jan@42463: to investigate underlying knowledge, applicable theorems, etc.  And
jan@42463: the user can proceed constructing a solution by input of a tactic to
jan@42463: be 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: 
jan@42463: \subsection{Tacticals for Control of Interpretation}
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
jan@42463: long as a tactic is applicable (for instance, {\it 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},
jan@42463: otherwise {\it term} is passed on unchanged.
jan@42463: 
jan@42463: \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
jan@42463: term}\Rightarrow{\it term}$:
jan@42463: 
jan@42463: 
jan@42463: \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
jan@42463: term}\Rightarrow{\it term}$:
jan@42463: 
jan@42463: \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
jan@42463: term}\Rightarrow{\it term}$:
jan@42463: 
jan@42463: \end{description}
jan@42463: 
jan@42463: no input / output --- Lucas-Interpretation
jan@42463: 
jan@42463: .\\.\\.\\TODO\\.\\.\\
jan@42463: 
neuper@42464: \section{Development of a Program on Trial}\label{trial} 
neuper@42464: As mentioned above, {\sisac} is an experimental system for a proof of
neuper@42464: concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}.  The
neuper@42464: latter interprets a specific kind of TP-based programming language,
neuper@42464: which is as experimental as the whole prototype --- so programming in
neuper@42464: this language can be only ``on trial'', presently.  However, as a
neuper@42464: prototype, the language addresses essentials described below.
neuper@42464: 
neuper@42464: \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
neuper@42464: 
neuper@42464: %WN was Fachleute unter obigem Titel interessiert findet
neuper@42464: %WN unterhalb des auskommentierten Textes.
neuper@42464: 
neuper@42464: %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
neuper@42464: %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: % 
neuper@42464: % \paragraph{Educational software in mathematics} is, if at all, based
neuper@42464: % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
neuper@42464: % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
neuper@42464: % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
neuper@42464: % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
neuper@42464: % base technologies are used to program math lessons and sometimes even
neuper@42464: % exercises. The latter are cumbersome: the steps towards a solution of
neuper@42464: % such an interactive exercise need to be provided with feedback, where
neuper@42464: % at each step a wide variety of possible input has to be foreseen by
neuper@42464: % the programmer - so such interactive exercises either require high
neuper@42464: % development efforts or the exercises constrain possible inputs.
neuper@42464: % 
neuper@42464: % \subparagraph{A new generation} of educational math assistants (EMAs)
neuper@42464: % is emerging presently, which is based on Theorem Proving (TP). TP, for
neuper@42464: % instance Isabelle and Coq, is a technology which requires each fact
neuper@42464: % and each action justified by formal logic. Pushed by demands for
neuper@42464: % \textit{proven} correctness of safety-critical software TP advances
neuper@42464: % into software engineering; from these advancements computer
neuper@42464: % mathematics benefits in general, and math education in particular. Two
neuper@42464: % features of TP are immediately beneficial for learning:
neuper@42464: % 
neuper@42464: % \paragraph{TP have knowledge in human readable format,} that is in
neuper@42464: % standard predicate calculus. TP following the LCF-tradition have that
neuper@42464: % knowledge down to the basic definitions of set, equality,
neuper@42464: % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
neuper@42464: % following the typical deductive development of math, natural numbers
neuper@42464: % are defined and their properties
neuper@42464: % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
neuper@42464: % etc. Present knowledge mechanized in TP exceeds high-school
neuper@42464: % mathematics by far, however by knowledge required in software
neuper@42464: % technology, and not in other engineering sciences.
neuper@42464: % 
neuper@42464: % \paragraph{TP can model the whole problem solving process} in
neuper@42464: % mathematical problem solving {\em within} a coherent logical
neuper@42464: % 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
neuper@42464: % Having the whole problem solving process within a logical coherent
neuper@42464: % system, such a design guarantees correctness of intermediate steps and
neuper@42464: % of the result (which seems essential for math software); and the
neuper@42464: % second advantage is that TP provides a wealth of theories which can be
neuper@42464: % 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: % 
neuper@42464: % One essential feature for educational software is feedback to user
neuper@42464: % input and assistance in coming to a solution.
neuper@42464: % 
neuper@42464: % \paragraph{Checking user input} by ATP during stepwise problem solving
neuper@42464: % is being accomplished by the three projects mentioned above
neuper@42464: % exclusively. They model the whole problem solving process as mentioned
neuper@42464: % above, so all what happens between formalized assumptions (or formal
neuper@42464: % specification) and goal (or fulfilled postcondition) can be
neuper@42464: % mechanized. Such mechanization promises to greatly extend the scope of
neuper@42464: % educational software in stepwise problem solving.
neuper@42464: % 
neuper@42464: % \paragraph{NSG (Next step guidance)} comprises the system's ability to
neuper@42464: % propose a next step; this is a challenge for TP: either a radical
neuper@42464: % restriction of the search space by restriction to very specific
neuper@42464: % problem classes is required, or much care and effort is required in
neuper@42464: % designing possible variants in the process of problem solving
neuper@42464: % \cite{proof-strategies-11}.
neuper@42464: % \par
neuper@42464: % Another approach is restricted to problem solving in engineering
neuper@42464: % domains, where a problem is specified by input, precondition, output
neuper@42464: % and postcondition, and where the postcondition is proven by ATP behind
neuper@42464: % the scenes: Here the possible variants in the process of problem
neuper@42464: % solving are provided with feedback {\em automatically}, if the problem
neuper@42464: % is described in a TP-based programing language: \cite{plmms10} the
neuper@42464: % programmer only describes the math algorithm without caring about
neuper@42464: % interaction (the respective program is functional and even has no
neuper@42464: % input or output statements!); interaction is generated as a
neuper@42464: % side-effect by the interpreter --- an efficient separation of concern
neuper@42464: % 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}}
neuper@42464: % Authoring new mathematics knowledge in {{\sisac}} can be compared with
neuper@42464: % ``application programing'' of engineering problems; most of such
neuper@42464: % programing uses CAS-based programing languages (CAS = Computer Algebra
neuper@42464: % Systems; e.g. Mathematica's or Maple's programing language).
neuper@42464: % 
neuper@42464: % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
neuper@42464: % \cite{plmms10} for describing how to construct a solution to an
neuper@42464: % engineering problem and for calling equation solvers, integration,
neuper@42464: % etc~\footnote{Implementation of CAS-like functionality in TP is not
neuper@42464: % primarily concerned with efficiency, but with a didactic question:
neuper@42464: % What to decide for: for high-brow algorithms at the state-of-the-art
neuper@42464: % or for elementary algorithms comprehensible for students?} within TP;
neuper@42464: % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
neuper@42464: % are impossible for CAS which have no logics underlying.
neuper@42464: % 
neuper@42464: % \subparagraph{Authoring is perfect} by writing such TP based programs;
neuper@42464: % the application programmer is not concerned with interaction or with
neuper@42464: % user guidance: this is concern of a novel kind of program interpreter
neuper@42464: % called Lucas-Interpreter. This interpreter hands over control to a
neuper@42464: % dialog component at each step of calculation (like a debugger at
neuper@42464: % breakpoints) and calls automated TP to check user input following
neuper@42464: % personalized strategies according to a feedback module.
neuper@42464: % \par
neuper@42464: % However ``application programing with TP'' is not done with writing a
neuper@42464: % program: according to the principles of TP, each step must be
neuper@42464: % justified. Such justifications are given by theorems. So all steps
neuper@42464: % must be related to some theorem, if there is no such theorem it must
neuper@42464: % be added to the existing knowledge, which is organized in so-called
neuper@42464: % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
neuper@42464: % Isabelle comprises a mechanism (called ``axiomatization''), which
neuper@42464: % allows to omit proofs. Such a theorem is shown in
neuper@42464: % Example~\ref{eg:neuper1}.
neuper@42464: 
neuper@42464: The running example, introduced by Fig.\ref{fig-interactive} on
neuper@42464: p.\pageref{fig-interactive}, requires to determine the inverse $\cal
neuper@42464: Z$-transform for a class of functions. The domain of Signal Processing
neuper@42464: is accustomed to specific notation for the resulting functions, which
neuper@42464: are absolutely summable and are called TODO: $u[n]$, where $u$ is the
neuper@42464: function, $n$ is the argument and the brackets indicate that the
neuper@42464: arguments are TODO. Surprisingly, Isabelle accepts the rules for
neuper@42464: ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
neuper@42464: experts might be particularly surprised, that the brackets do not
neuper@42464: 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\\
neuper@42464:   \>\>  rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
neuper@42464: %TODO
neuper@42464:   \>\>  rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
neuper@42464: %TODO
jan@42463:   \>\>  rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
jan@42463: %TODO
neuper@42464:   \>\>  rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
neuper@42464: %TODO
neuper@42464:   \end{tabbing}
neuper@42464:   }
neuper@42464: % \end{example}
neuper@42464: %}
neuper@42464: These 6 rules can be used as conditional rewrite rules, depending on
neuper@42464: the respective convergence radius. Satisfaction from notation
neuper@42464: contrasts with the word {\em axiomatization}: As TP-based, the
neuper@42464: programming language expects these rules as {\em proved} theorems, and
neuper@42464: not as axioms implemented in the above brute force manner; otherwise
neuper@42464: all the verification efforts envisaged (like proof of the
neuper@42464: post-condition, see below) would be meaningless.
neuper@42464: 
neuper@42464: Isabelle provides a large body of knowledge, rigorously proven from
neuper@42464: the basic axioms of mathematics~\footnote{This way of rigorously
neuper@42464: deriving all knowledge from first principles is called the
neuper@42464: LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
neuper@42464: knowledge can be found in the theoris on Multivariate
neuper@42464: Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
neuper@42464: building up knowledge such that a proof for the above rules would be
neuper@42464: reasonably short and easily comprehensible, still requires lots of
neuper@42464: work (and is definitely out of scope of our case study).
neuper@42464: 
neuper@42464: \medskip At the state-of-the-art in mechanization of knowledge in
neuper@42464: engineering, the process does not stop with the mechanization of
neuper@42464: mathematics. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
neuper@42464: proceed to formal description of physical items.  Signal Processing,
neuper@42464: for instance is concerned with physical devices for signal acquisition
neuper@42464: and reconstruction, which involve measuring a physical signal, storing
neuper@42464: it, and possibly later rebuilding the original signal or an
neuper@42464: approximation thereof. For digital systems, this typically includes
neuper@42464: sampling and quantization; devices for signal compression, including
neuper@42464: audio compression, image compression, and video compression, etc.
neuper@42464: ``Domain engineering''\cite{db-domain-engineering} is concerned with
neuper@42464: {\em specification} of these devices' components and features; this
neuper@42464: part in the process of mechanization is only at the beginning.
neuper@42464: 
neuper@42464: \medskip TP-based programming, concern of this paper, adds a third
neuper@42464: part of mechanisation, providing a third axis of ``algorithmic
neuper@42464: knowledge'' in Fig.\ref{fig:mathuni} on p.\pageref{fig:mathuni}.
neuper@42464: 
neuper@42464:   \begin{figure}
neuper@42464:     \hfill \\
neuper@42464:     \begin{center}
neuper@42464:       \includegraphics{fig/universe}
neuper@42464:       \caption{Didactic ``Math-Universe''\label{fig:mathuni}}
neuper@42464:     \end{center}
neuper@42464:   \end{figure}
neuper@42464: %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
neuper@42464: %WN bitte folgende Bezeichnungen nehmen:
neuper@42464: %WN 
neuper@42464: %WN axis 1: Algorithmic Knowledge (Programs)
neuper@42464: %WN axis 2: Application-oriented Knowledge (Specifications)
neuper@42464: %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
neuper@42464: 
neuper@42464: \subsection{Specification of the Problem}\label{spec}
neuper@42464: %WN <--> \chapter 7 der Thesis
neuper@42464: %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
neuper@42464: In order to provide TP with logical facts for checking user input, the
neuper@42464: Lucas-Interpreter requires a \textbf{specification}. Such a
neuper@42464: specification is shown in Example~\ref{eg:neuper2}.
neuper@42464: 
jan@42463: -------------------------------------------------------------------
jan@42463: 
jan@42463: Hier brauchen wir die Spezifikation des 'running example' ...
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:   \label{eg:neuper2}
jan@42463:   {\small\begin{tabbing}
jan@42463:   123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
jan@42463:   \hfill \\
jan@42463:   Specification no.1:\\
jan@42463:   %\>input\>: $\{\;r={\it arbitraryFix}\;\}$  \\
jan@42463:   \>input    \>: $\{\;r\;\}$  \\
jan@42463:   \>precond  \>: $0 < r$   \\
jan@42463:   \>output   \>: $\{\;A,\; u,v\;\}$ \\
jan@42463:   \>postcond \>:{\small  $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\
jan@42463:   \>     \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land
jan@42463:   (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\
jan@42463:   \>props\>: $\{\;A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\;\}$
neuper@42464:   \end{tabbing}
neuper@42464:   }
neuper@42464:   \end{example}
neuper@42464: }
neuper@42464: 
neuper@42464: ... und die Implementation in Isac (mit Kommentaren aus dem datatype)
neuper@42464: 
jan@42463: %WN das w"urde ich in \sec\label{}
jan@42463: Such a specification is checked before the execution of a program is
jan@42463: started, the same applies for sub-programs. In the following example
jan@42463: (Example~\ref{eg:subprob}) shows the call of such a subproblem:
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:   \label{eg:subprob}
jan@42463:   \hfill \\
jan@42463:   {\ttfamily \begin{tabbing}
jan@42463:   ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
jan@42463:   ``\>\>[linear,univariate,equation,test],'' \\
jan@42463:   ``\>\>[Test,solve\_linear])'' \\
neuper@42464:   ``\>[BOOL equ, REAL z])'' \\
neuper@42464:   \end{tabbing}
neuper@42464:   }
neuper@42464:   {\small\textit{
jan@42463:     \noindent If a program requires a result which has to be
jan@42463: calculated first we can use a subproblem to do so. In our specific
jan@42463: case we wanted to calculate the zeros of a fraction and used a
neuper@42464: subproblem to calculate the zeros of the denominator polynom.
neuper@42464:     }}
neuper@42464:   \end{example}
neuper@42464: }
neuper@42464: 
neuper@42464: \subsection{Implementation of the Method}\label{meth}
neuper@42464: %WN <--> \chapter 7 der Thesis
neuper@42464: TODO
neuper@42464: \subsection{Preparation of ML-Functions for the Program}\label{funs}
neuper@42464: %WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr}
neuper@42464: %WN brauchst
neuper@42464: TODO
jan@42463: \subsection{Implementation of the TP-based Program}\label{progr}
neuper@42464: %WN <--> \chapter 8 der Thesis
neuper@42464: TODO
neuper@42464: 
neuper@42464: \section{Workflow of Programming in the Prototype}\label{workflow}
neuper@42464: -------------------------------------------------------------------
neuper@42464: 
neuper@42464: ``workflow'' heisst: das mache ich zuerst, dann das ...
neuper@42464: 
neuper@42464: \subsection{Preparations and Trials}\label{flow-prep}
neuper@42464: TODO ... Build\_Inverse\_Z\_Transform.thy !!!
neuper@42464: 
neuper@42464: \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
neuper@42464: TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
neuper@42464: 
neuper@42464: \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
neuper@42464: TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
neuper@42464: 
neuper@42464: -------------------------------------------------------------------
neuper@42464: 
neuper@42464: Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are 
jan@42463: vermutlich auf andere sections aufzuteilen.
jan@42463: 
neuper@42464: -------------------------------------------------------------------
neuper@42464: 
neuper@42464: \subsection{Formalization of missing knowledge in Isabelle}
neuper@42464: 
jan@42463: \paragraph{A problem} behind is the mechanization of mathematic
jan@42463: theories in TP-bases languages. There is still a huge gap between
jan@42463: these algorithms and this what we want as a solution - in Example
jan@42463: Signal Processing. 
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:     \label{eg:gap}
neuper@42464:     \[
neuper@42464:       X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
neuper@42464:     \]
neuper@42464:     {\small\textit{
neuper@42464:       \noindent A very simple example on this what we call gap is the
neuper@42464: simplification above. It is needles to say that it is correct and also
neuper@42464: Isabelle for fills it correct - \emph{always}. But sometimes we don't
jan@42463: want expand such terms, sometimes we want another structure of
jan@42463: them. Think of a problem were we now would need only the coefficients
jan@42463: of $X$ and $Y$. This is what we call the gap between mechanical
jan@42463: simplification and the solution.
neuper@42464:     }}
neuper@42464:   \end{example}
neuper@42464: }
neuper@42464: 
neuper@42464: \paragraph{We are not able to fill this gap,} until we have to live
neuper@42464: with it but first have a look on the meaning of this statement:
neuper@42464: Mechanized math starts from mathematical models and \emph{hopefully}
neuper@42464: proceeds to match physics. Academic engineering starts from physics
neuper@42464: (experimentation, measurement) and then proceeds to mathematical
jan@42463: modeling and formalization. The process from a physical observance to
jan@42463: a mathematical theory is unavoidable bound of setting up a big
jan@42463: collection of standards, rules, definition but also exceptions. These
jan@42463: are the things making mechanization that difficult.
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:     \label{eg:units}
neuper@42464:     \[
neuper@42464:       m,\ kg,\ s,\ldots
neuper@42464:     \]
neuper@42464:     {\small\textit{
neuper@42464:       \noindent Think about some units like that one's above. Behind
neuper@42464: each unit there is a discerning and very accurate definition: One
jan@42463: Meter is the distance the light travels, in a vacuum, through the time
jan@42463: of 1 / 299.792.458 second; one kilogram is the weight of a
jan@42463: platinum-iridium cylinder in paris; and so on. But are these
jan@42463: definitions usable in a computer mechanized world?!
neuper@42464:     }}
neuper@42464:   \end{example}
neuper@42464: }
neuper@42464: 
jan@42463: \paragraph{A computer} or a TP-System builds on programs with
jan@42463: predefined logical rules and does not know any mathematical trick
jan@42463: (follow up example \ref{eg:trick}) or recipe to walk around difficult
jan@42463: expressions. 
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:     \label{eg:trick}
jan@42463:   \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
neuper@42464:   \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
neuper@42464:      \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
neuper@42464:   \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
neuper@42464:     {\small\textit{
neuper@42464:       \noindent Sometimes it is also useful to be able to apply some
jan@42463: \emph{tricks} to get a beautiful and particularly meaningful result,
jan@42463: which we are able to interpret. But as seen in this example it can be
jan@42463: hard to find out what operations have to be done to transform a result
jan@42463: into a meaningful one.
neuper@42464:     }}
neuper@42464:   \end{example}
neuper@42464: }
neuper@42464: 
neuper@42464: \paragraph{The only possibility,} for such a system, is to work
neuper@42464: through its known definitions and stops if none of these
neuper@42464: fits. Specified on Signal Processing or any other application it is
neuper@42464: often possible to walk through by doing simple creases. This creases
neuper@42464: are in general based on simple math operational but the challenge is
neuper@42464: to teach the machine \emph{all}\footnote{Its pride to call it
jan@42463: \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
neuper@42464: reach a high level of \emph{all} but it in real it will still be a
neuper@42464: survey of knowledge which links to other knowledge and {{\sisac}{}} a
neuper@42464: trainer and helper but no human compensating calculator. 
neuper@42464: \par
neuper@42464: {{{\sisac}{}}} itself aims to adds an \emph{application} axis (formal
jan@42463: specifications of problems out of topics from Signal Processing, etc.)
jan@42463: and an \emph{algorithmic} axis to the \emph{deductive} axis of
jan@42463: physical knowledge. The result is a three-dimensional universe of
jan@42463: mathematics seen in Figure~\ref{fig:mathuni}.
jan@42463: 
jan@42463:   \begin{figure}
jan@42463:     \hfill \\
jan@42463:     \begin{center}
jan@42463:       \includegraphics{fig/universe}
jan@42463:       \caption{Didactic ``Math-Universe''\label{fig:mathuni}}
jan@42463:     \end{center}
neuper@42464:   \end{figure}
neuper@42464: 
neuper@42464: \subsection{Notes on Problems with Traditional Notation}
neuper@42464: 
neuper@42464: \paragraph{During research} on these topic severely problems on
neuper@42464: traditional notations have been discovered. Some of them have been
jan@42463: known in computer science for many years now and are still unsolved,
jan@42463: one of them aggregates with the so called \emph{Lambda Calculus},
jan@42463: Example~\ref{eg:lamda} provides a look on the problem that embarrassed
jan@42463: us.
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:     \label{eg:lamda}
jan@42463: 
jan@42463:   \[ f(x)=\ldots\;  \quad R \rightarrow \quad R \]
jan@42463: 
neuper@42464: 
neuper@42464:   \[ f(p)=\ldots\;  p \in \quad R \]
neuper@42464: 
neuper@42464:     {\small\textit{
neuper@42464:       \noindent Above we see two equations. The first equation aims to
neuper@42464: be a mapping of an function from the reel range to the reel one, but
neuper@42464: when we change only one letter we get the second equation which
jan@42463: usually aims to insert a reel point $p$ into the reel function. In
jan@42463: computer science now we have the problem to tell the machine (TP) the
jan@42463: difference between this two notations. This Problem is called
jan@42463: \emph{Lambda Calculus}.
neuper@42464:     }}
neuper@42464:   \end{example}
neuper@42464: }
neuper@42464: 
neuper@42464: \paragraph{An other problem} is that terms are not full simplified in
neuper@42464: traditional notations, in {{\sisac}} we have to simplify them complete
neuper@42464: to check weather results are compatible or not. in e.g. the solutions
neuper@42464: of an second order linear equation is an rational in {{\sisac}} but in
neuper@42464: tradition we keep fractions as long as possible and as long as they
neuper@42464: aim to be \textit{beautiful} (1/8, 5/16,...).
neuper@42464: \subparagraph{The math} which should be mechanized in Computer Theorem
neuper@42464: Provers (\emph{TP}) has (almost) a problem with traditional notations
neuper@42464: (predicate calculus) for axioms, definitions, lemmas, theorems as a
neuper@42464: computer program or script is not able to interpret every Greek or
jan@42463: Latin letter and every Greek, Latin or whatever calculations
jan@42463: symbol. Also if we would be able to handle these symbols we still have
jan@42463: a problem to interpret them at all. (Follow up \hbox{Example
jan@42463: \ref{eg:symbint1}})
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:     \label{eg:symbint1}
neuper@42464:     \[
neuper@42464:       u\left[n\right] \ \ldots \ unitstep
neuper@42464:     \]
neuper@42464:     {\small\textit{
neuper@42464:       \noindent The unitstep is something we need to solve Signal
jan@42463: Processing problem classes. But in {{{\sisac}{}}} the rectangular
jan@42463: brackets have a different meaning. So we abuse them for our
jan@42463: requirements. We get something which is not defined, but usable. The
jan@42463: Result is syntax only without semantic.
neuper@42464:     }}
neuper@42464:   \end{example}
neuper@42464: }
jan@42463: 
jan@42463: In different problems, symbols and letters have different meanings and
jan@42463: ask for different ways to get through. (Follow up \hbox{Example
jan@42463: \ref{eg:symbint2}}) 
jan@42463: 
jan@42463: \vbox{
jan@42463:   \begin{example}
jan@42463:     \label{eg:symbint2}
neuper@42464:     \[
neuper@42464:       \widehat{\ }\ \widehat{\ }\ \widehat{\ } \  \ldots \  exponent
neuper@42464:     \]
neuper@42464:     {\small\textit{
jan@42463:     \noindent For using exponents the three \texttt{widehat} symbols
jan@42463: are required. The reason for that is due the development of
jan@42463: {{{\sisac}{}}} the single \texttt{widehat} and also the double were
jan@42463: already in use for different operations.
neuper@42464:     }}
neuper@42464:   \end{example}
neuper@42464: }
neuper@42464: 
neuper@42464: \paragraph{Also the output} can be a problem. We are familiar with a
neuper@42464: specified notations and style taught in university but a computer
neuper@42464: program has no knowledge of the form proved by a professor and the
neuper@42464: machines themselves also have not yet the possibilities to print every
jan@42463: symbol (correct) Recent developments provide proofs in a human
jan@42463: readable format but according to the fact that there is no money for
jan@42463: good working formal editors yet, the style is one thing we have to
jan@42463: live with.
jan@42463: 
neuper@42464: \section{Problems rising out of the Development Environment}
jan@42463: 
jan@42463: fehlermeldungen! TODO
jan@42463: 
jan@42463: \section{Conclusion}\label{conclusion}
jan@42463: 
jan@42463: TODO
jan@42463: 
neuper@42464: \bibliographystyle{alpha}
neuper@42464: \bibliography{references}
neuper@42464: 
neuper@42464: \end{document}



