
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: % Electronic Journal of Mathematics and Technology (eJMT) %
jan@42463: % style sheet for LaTeX.  Please do not modify sections   %
jan@42463: % or commands marked 'eJMT'.                              %
jan@42463: %                                                         %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %                                                         %
jan@42463: % eJMT commands                                           %
jan@42463: %                                                         %
jan@42463: \documentclass[12pt,a4paper]{article}%                    %
jan@42463: \usepackage{times}                                        %
jan@42463: \usepackage{amsfonts,amsmath,amssymb}                     %
jan@42463: \usepackage[a4paper]{geometry}                            %
jan@42463: \usepackage{fancyhdr}                                     %
jan@42463: \usepackage{color}                                        %
jan@42463: \usepackage[pdftex]{hyperref} % see note below            %
jan@42463: \usepackage{graphicx}%                                    %
jan@42463: \hypersetup{                                              %
jan@42463:     a4paper,                                              %
jan@42463:     breaklinks                                            %
jan@42463: }                                                         %
jan@42463: %                                                         %
jan@42463: \newtheorem{theorem}{Theorem}                             %
jan@42463: \newtheorem{acknowledgement}[theorem]{Acknowledgement}    %
jan@42463: \newtheorem{algorithm}[theorem]{Algorithm}                %
jan@42463: \newtheorem{axiom}[theorem]{Axiom}                        %
jan@42463: \newtheorem{case}[theorem]{Case}                          %
jan@42463: \newtheorem{claim}[theorem]{Claim}                        %
jan@42463: \newtheorem{conclusion}[theorem]{Conclusion}              %
jan@42463: \newtheorem{condition}[theorem]{Condition}                %
jan@42463: \newtheorem{conjecture}[theorem]{Conjecture}              %
jan@42463: \newtheorem{corollary}[theorem]{Corollary}                %
jan@42463: \newtheorem{criterion}[theorem]{Criterion}                %
jan@42463: \newtheorem{definition}[theorem]{Definition}              %
jan@42463: \newtheorem{example}[theorem]{Example}                    %
jan@42463: \newtheorem{exercise}[theorem]{Exercise}                  %
jan@42463: \newtheorem{lemma}[theorem]{Lemma}                        %
jan@42463: \newtheorem{notation}[theorem]{Notation}                  %
jan@42463: \newtheorem{problem}[theorem]{Problem}                    %
jan@42463: \newtheorem{proposition}[theorem]{Proposition}            %
jan@42463: \newtheorem{remark}[theorem]{Remark}                      %
jan@42463: \newtheorem{solution}[theorem]{Solution}                  %
jan@42463: \newtheorem{summary}[theorem]{Summary}                    %
jan@42463: \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }  %
jan@42463: {\ \rule{0.5em}{0.5em}}                                   %
jan@42463: %                                                         %
jan@42463: % eJMT page dimensions                                    %
jan@42463: %                                                         %
jan@42463: \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm}        %
jan@42463: %                                                         %
jan@42463: % eJMT header & footer                                    %
jan@42463: %                                                         %
jan@42463: \newcounter{ejmtFirstpage}                                %
jan@42463: \setcounter{ejmtFirstpage}{1}                             %
jan@42463: \pagestyle{empty}                                         %
jan@42463: \setlength{\headheight}{14pt}                             %
jan@42463: \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm}        %
jan@42463: \pagestyle{fancyplain}                                    %
jan@42463: \fancyhf{}                                                %
jan@42463: \fancyhead[c]{\small The Electronic Journal of Mathematics%
jan@42463: \ and Technology, Volume 1, Number 1, ISSN 1933-2823}     %
jan@42463: \cfoot{%                                                  %
jan@42463:   \ifnum\value{ejmtFirstpage}=0%                          %
jan@42463:     {\vtop to\hsize{\hrule\vskip .2cm\thepage}}%          %
jan@42463:   \else\setcounter{ejmtFirstpage}{0}\fi%                  %
jan@42463: }                                                         %
jan@42463: %                                                         %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %
jan@42463: % Please place your own definitions here
jan@42463: %
jan@42463: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
jan@42463: \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
jan@42463: 
jan@42463: \usepackage{color}
jan@42463: \definecolor{lgray}{RGB}{238,238,238}
jan@42463: 
jan@42463: %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %                                                         %
jan@42463: % How to use hyperref                                     %
jan@42463: % -------------------                                     %
jan@42463: %                                                         %
jan@42463: % Probably the only way you will need to use the hyperref %
jan@42463: % package is as follows.  To make some text, say          %
jan@42463: % "My Text Link", into a link to the URL                  %
jan@42463: % http://something.somewhere.com/mystuff, use             %
jan@42463: %                                                         %
jan@42463: % \href{http://something.somewhere.com/mystuff}{My Text Link}
jan@42463: %                                                         %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %
jan@42463: \begin{document}
jan@42463: %
jan@42463: % document title
jan@42463: %
neuper@42464: \title{Trials with TP-based Programming
neuper@42464: \\
neuper@42464: for Interactive Course Material}%
jan@42463: %
jan@42463: % Single author.  Please supply at least your name,
jan@42463: % email address, and affiliation here.
jan@42463: %
jan@42463: \author{\begin{tabular}{c}
jan@42463: \textit{Jan Ro\v{c}nik} \\
jan@42463: jan.rocnik@student.tugraz.at \\
jan@42463: IST, SPSC\\
neuper@42464: Graz University of Technologie\\
jan@42463: Austria\end{tabular}
jan@42463: }%
jan@42463: %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %                                                         %
jan@42463: % eJMT commands - do not change these                     %
jan@42463: %                                                         %
jan@42463: \date{}                                                   %
jan@42463: \maketitle                                                %
jan@42463: %                                                         %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %
jan@42463: % abstract
jan@42463: %
jan@42463: \begin{abstract}
jan@42463: 
jan@42463: Traditional course material in engineering disciplines lacks an
jan@42463: important component, interactive support for step-wise problem
neuper@42464: solving. Theorem-Proving (TP) technology is appropriate for one part
jan@42463: of such support, in checking user-input. For the other part of such
jan@42463: support, guiding the learner towards a solution, another kind of
jan@42463: technology is required. %TODO ... connect to prototype ...
jan@42463: 
jan@42463: A prototype combines TP with a programming language, the latter
jan@42463: interpreted in a specific way: certain statements in a program, called
jan@42463: tactics, are treated as breakpoints where control is handed over to
jan@42463: the user. An input formula is checked by TP (using logical context
jan@42463: built up by the interpreter); and if a learner gets stuck, a program
jan@42463: describing the steps towards a solution of a problem ``knows the next
jan@42463: step''. This kind of interpretation is called Lucas-Interpretation for
jan@42463: \emph{TP-based programming languages}.
jan@42463: 
jan@42463: This paper describes the prototype's TP-based programming language
jan@42463: within a case study creating interactive material for an advanced
jan@42463: course in Signal Processing: implementation of definitions and
jan@42463: theorems in TP, formal specification of a problem and step-wise
jan@42463: development of the program solving the problem. Experiences with the
neuper@42464: ork flow in iterative development with testing and identifying errors
jan@42463: are described, too. The description clarifies the components missing
jan@42463: in the prototype's language as well as deficiencies experienced during
jan@42463: programming.
jan@42463: \par
jan@42463: These experiences are particularly notable, because the author is the
jan@42463: first programmer using the language beyond the core team which
jan@42463: developed the prototype's TP-based language interpreter.
jan@42463: %
jan@42463: \end{abstract}%
jan@42463: %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %                                                         %
jan@42463: % eJMT command                                            %
jan@42463: %                                                         %
jan@42463: \thispagestyle{fancy}                                     %
jan@42463: %                                                         %
jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42463: %
jan@42463: % Please use the following to indicate sections, subsections,
jan@42463: % etc.  Please also use \subsubsection{...}, \paragraph{...}
jan@42463: % and \subparagraph{...} as necessary.
jan@42463: %
jan@42463: 
neuper@42464: \section{Introduction}\label{intro}
jan@42463: 
jan@42466: % \paragraph{Didactics of mathematics} 
jan@42466: %WN: wenn man in einem high-quality paper von 'didactics' spricht, 
jan@42466: %WN muss man am state-of-the-art ankn"upfen -- siehe
jan@42466: %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
neuper@42464: % faces a specific issue, a gap
neuper@42464: % between (1) introduction of math concepts and skills and (2)
neuper@42464: % application of these concepts and skills, which usually are separated
neuper@42464: % into different units in curricula (for good reasons). For instance,
neuper@42464: % (1) teaching partial fraction decomposition is separated from (2)
neuper@42464: % application for inverse Z-transform in signal processing.
neuper@42464: % 
neuper@42464: % \par This gap is an obstacle for applying math as an fundamental
neuper@42464: % thinking technology in engineering: In (1) motivation is lacking
neuper@42464: % because the question ``What is this stuff good for?'' cannot be
neuper@42464: % treated sufficiently, and in (2) the ``stuff'' is not available to
neuper@42464: % students in higher semesters as widespread experience shows.
neuper@42464: % 
neuper@42464: % \paragraph{Motivation} taken by this didactic issue on the one hand,
neuper@42464: % and ongoing research and development on a novel kind of educational
neuper@42464: % mathematics assistant at Graz University of
neuper@42464: % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
neuper@42464: % scope with this issue on the other hand, several institutes are
neuper@42464: % planning to join their expertise: the Institute for Information
neuper@42464: % Systems and Computer Media (IICM), the Institute for Software
neuper@42464: % Technology (IST), the Institutes for Mathematics, the Institute for
neuper@42464: % Signal Processing and Speech Communication (SPSC), the Institute for
neuper@42464: % Structural Analysis and the Institute of Electrical Measurement and
neuper@42464: % Measurement Signal Processing.
jan@42466: %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell 
jan@42466: %WN und damit zu verg"anglich.
neuper@42464: % \par This thesis is the first attempt to tackle the above mentioned
neuper@42464: % issue, it focuses on Telematics, because these specific studies focus
neuper@42464: % on mathematics in \emph{STEOP}, the introductory orientation phase in
neuper@42464: % Austria. \emph{STEOP} is considered an opportunity to investigate the
neuper@42464: % impact of {\sisac}'s prototype on the issue and others.
neuper@42464: % 
jan@42466: 
jan@42466: \paragraph{Traditional course material} in engineering disciplines lacks an
neuper@42464: important component, interactive support for step-wise problem
neuper@42464: solving. Theorem-Proving (TP) technology can provide such support by
neuper@42464: specific services. An important part of such services is called
neuper@42464: ``next-step-guidance'', generated by a specific kind of ``TP-based
neuper@42464: programming language''. In the
neuper@42464: {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
neuper@42464: a language is prototyped in line with~\cite{plmms10} and built upon
neuper@42464: the theorem prover
neuper@42464: Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
neuper@42464: The TP services are coordinated by a specific interpreter for the
neuper@42464: programming language, called
neuper@42464: Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
neuper@42464: interpreter will be briefly re-introduced in order to make the paper
neuper@42464: self-contained.
jan@42463: 
jan@42466: \subparagraph{The main part} of the paper is an account of first experiences
neuper@42464: with programming in this TP-based language. The experience was gained
neuper@42464: in a case study by the author. The author was considered an ideal
neuper@42464: candidate for this study for the following reasons: as a student in
neuper@42464: Telematics (computer science with focus on Signal Processing) he had
neuper@42464: general knowledge in programming as well as specific domain knowledge
neuper@42464: in Signal Processing; and he was not involved in the development of
neuper@42464: {\sisac}'s programming language and interpeter, thus a novice to the
neuper@42464: language.
jan@42463: 
jan@42466: \subparagraph{The goal} of the case study was (1) some TP-based programs for
neuper@42464: interactive course material for a specific ``Adavanced Signal
neuper@42464: Processing Lab'' in a higher semester, (2) respective program
neuper@42464: development with as little advice from the {\sisac}-team and (3) records
neuper@42464: and comments for the main steps of development in an Isabelle theory;
neuper@42464: this theory should provide guidelines for future programmers. An
neuper@42464: excerpt from this theory is the main part of this paper.
jan@42466: \par
jan@42466: The paper will use the problem in Fig.\ref{fig-interactive} as a
jan@42463: running example:
jan@42463: \begin{figure} [htb]
jan@42463: \begin{center}
neuper@42468: \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
neuper@42468: %\includegraphics[width=140mm]{fig/isac-Ztrans-math}
jan@42463: \caption{Step-wise problem solving guided by the TP-based program}
jan@42463: \label{fig-interactive}
jan@42463: \end{center}
jan@42463: \end{figure}
jan@42466: 
jan@42466: \paragraph{The problem is} from the domain of Signal Processing and requests to
neuper@42464: determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
neuper@42464: also shows the beginning of the interactive construction of a solution
neuper@42464: for the problem. This construction is done in the right window named
neuper@42464: ``Worksheet''.
jan@42466: \par
neuper@42464: User-interaction on the Worksheet is {\em checked} and {\em guided} by
neuper@42464: TP services:
neuper@42464: \begin{enumerate}
neuper@42464: \item Formulas input by the user are {\em checked} by TP: such a
neuper@42464: formula establishes a proof situation --- the prover has to derive the
neuper@42464: formula from the logical context. The context is built up from the
neuper@42464: formal specification of the problem (here hidden from the user) by the
neuper@42464: Lucas-Interpreter.
neuper@42464: \item If the user gets stuck, the program developed below in this
neuper@42464: paper ``knows the next step'' from behind the scenes. How the latter
neuper@42464: TP-service is exploited by dialogue authoring is out of scope of this
neuper@42464: paper and can be studied in~\cite{gdaroczy-EP-13}.
neuper@42464: \end{enumerate} It should be noted that the programmer using the
neuper@42464: TP-based language is not concerned with interaction at all; we will
neuper@42464: see that the program contains neither input-statements nor
neuper@42464: output-statements. Rather, interaction is handled by services
neuper@42464: generated automatically.
jan@42466: \par
jan@42466: So there is a clear separation of concerns: Dialogues are
neuper@42464: adapted by dialogue authors (in Java-based tools), using automatically
neuper@42464: generated TP services, while the TP-based program is written by
neuper@42464: mathematics experts (in Isabelle/ML). The latter is concern of this
neuper@42464: paper.
jan@42466: 
jan@42466: \paragraph{The paper is structed} as follows: The introduction
neuper@42464: \S\ref{intro} is followed by a brief re-introduction of the TP-based
neuper@42464: programming language in \S\ref{PL}, which extends the executable
neuper@42464: fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
neuper@42464: play a specific role in Lucas-Interpretation and in providing the TP
neuper@42464: services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes
neuper@42464: the main steps in developing the program for the running example:
neuper@42464: prepare domain knowledge, implement the formal specification of the
neuper@42464: problem, prepare the environment for the program, implement the
neuper@42464: program. The workflow of programming, debugging and testing is
neuper@42464: described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
neuper@42464: give directions identified for future development. 
neuper@42464: 
jan@42463: 
jan@42463: \section{\isac's Prototype for a Programming Language}\label{PL} 
jan@42463: The prototype's language extends the executable fragment in the
jan@42463: language of the theorem prover
jan@42463: Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}
jan@42463: by tactics which have a specific role in Lucas-Interpretation.
jan@42463: 
jan@42463: \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
jan@42463: The executable fragment consists of data-type and function
jan@42463: definitions.  It's usability even suggests that fragment for
jan@42463: introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
jan@42463: whose type system resembles that of functional programming
jan@42463: languages. Thus there are
jan@42463: \begin{description}
jan@42463: \item[base types,] in particular \textit{bool}, the type of truth
jan@42463: values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
jan@42463: natural, integer and complex numbers respectively in mathematics.
jan@42463: \item[type constructors] allow to define arbitrary types, from
jan@42463: \textit{set}, \textit{list} to advanced data-structures like
jan@42463: \textit{trees}, red-black-trees etc.
jan@42463: \item[function types,] denoted by $\Rightarrow$.
jan@42463: \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
jan@42463: type polymorphism. Isabelle automatically computes the type of each
jan@42463: variable in a term by use of Hindley-Milner type inference
jan@42463: \cite{pl:hind97,Milner-78}.
jan@42463: \end{description}
jan@42463: 
jan@42463: \textbf{Terms} are formed as in functional programming by applying
jan@42463: functions to arguments. If $f$ is a function of type
jan@42463: $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
jan@42463: $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
jan@42463: has type $\tau$. There are many predefined infix symbols like $+$ and
jan@42463: $\leq$ most of which are overloaded for various types.
jan@42463: 
jan@42463: HOL also supports some basic constructs from functional programming:
jan@42463: {\it\label{isabelle-stmts}
jan@42463: \begin{tabbing} 123\=\kill
jan@42463: \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
jan@42463: \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
jan@42463: \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
jan@42463:   \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
jan@42463: \end{tabbing} }
neuper@42482: \noindent The running example's program uses some of these elements
neuper@42482: (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
neuper@42482: let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
neuper@42482: is an Isabelle term with specific function constants like {\tt
neuper@42482: program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
neuper@42482: Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
neuper@42482: respectively.
jan@42463: 
jan@42463: % Terms may also contain $\lambda$-abstractions. For example, $\lambda
jan@42463: % x. \; x$ is the identity function.
jan@42463: 
neuper@42467: %JR warum auskommentiert? WN2...
neuper@42467: %WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
neuper@42467: %WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
neuper@42467: %WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
neuper@42467: %WN2 gel"oscht.
neuper@42467: %WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
neuper@42467: %WN2 Platz f"ur Anderes weg.
jan@42466: 
neuper@42464: \textbf{Formulae} are terms of type \textit{bool}. There are the basic
jan@42463: constants \textit{True} and \textit{False} and the usual logical
jan@42463: connectives (in decreasing order of precedence): $\neg, \land, \lor,
jan@42463: \rightarrow$.
jan@42463: 
neuper@42464: \textbf{Equality} is available in the form of the infix function $=$
neuper@42464: of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
neuper@42464: formulas, where it means ``if and only if''.
jan@42463: 
jan@42463: \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
jan@42463: P$.  Quantifiers lead to non-executable functions, so functions do not
jan@42463: always correspond to programs, for instance, if comprising \\$(
jan@42463: \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
jan@42463: \;)$.
jan@42463: 
jan@42463: \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
jan@42463: The prototype extends Isabelle's language by specific statements
neuper@42464: called tactics~\footnote{{\sisac}'s tactics are different from
jan@42463: Isabelle's tactics: the former concern steps in a calculation, the
jan@42463: latter concern proof steps.}  and tacticals. For the programmer these
jan@42463: statements are functions with the following signatures:
jan@42463: 
jan@42463: \begin{description}
jan@42463: \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
jan@42463: term} * {\it term}\;{\it list}$:
jan@42463: this tactic appplies {\it theorem} to a {\it term} yielding a {\it
jan@42463: term} and a {\it term list}, the list are assumptions generated by
jan@42463: conditional rewriting. For instance, the {\it theorem}
jan@42463: $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
jan@42463: applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
jan@42463: $(\frac{2}{3}, [x\not=0])$.
jan@42463: 
jan@42463: \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
jan@42463: term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
jan@42463: this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
jan@42463: a confluent and terminating term rewrite system, in general. If
jan@42463: none of the rules ({\it theorem}s) is applicable on interpretation
jan@42463: of this tactic, an exception is thrown.
jan@42463: 
jan@42463: % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
jan@42463: % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
jan@42463: % list}$:
jan@42463: % 
jan@42463: % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
jan@42463: % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
jan@42463: % list}$:
jan@42463: 
jan@42463: \item[Substitute:] ${\it substitution}\Rightarrow{\it
neuper@42482: term}\Rightarrow{\it term}$: allows to access sub-terms.
jan@42463: 
jan@42463: \item[Take:] ${\it term}\Rightarrow{\it term}$:
jan@42463: this tactic has no effect in the program; but it creates a side-effect
jan@42463: by Lucas-Interpretation (see below) and writes {\it term} to the
jan@42463: Worksheet.
jan@42463: 
jan@42463: \item[Subproblem:] ${\it theory} * {\it specification} * {\it
jan@42463: method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
neuper@42482: this tactic is a generalisation of a function call: it takes an
neuper@42482: \textit{argument list} as usual, and additionally a triple consisting
neuper@42482: of an Isabelle \textit{theory}, an implicit \textit{specification} of the
neuper@42482: program and a \textit{method} containing data for Lucas-Interpretation,
neuper@42482: last not least a program (as an explicit specification)~\footnote{In
neuper@42482: interactive tutoring these three items can be determined explicitly
neuper@42482: by the user.}.
jan@42463: \end{description}
jan@42463: The tactics play a specific role in
jan@42463: Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
neuper@42482: break-points where, as a side-effect, a line is added to a calculation
neuper@42483: as a protocol for proceeding towards a solution in step-wise problem
neuper@42483: solving. At the same points Lucas-Interpretation serves interactive
neuper@42483: tutoring and control is handed over to the user. The user is free to
neuper@42483: investigate underlying knowledge, applicable theorems, etc.  And the
neuper@42483: user can proceed constructing a solution by input of a tactic to be
neuper@42483: applied or by input of a formula; in the latter case the
jan@42463: Lucas-Interpreter has built up a logical context (initialised with the
jan@42463: precondition of the formal specification) such that Isabelle can
jan@42463: derive the formula from this context --- or give feedback, that no
jan@42463: derivation can be found.
jan@42463: 
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
neuper@42482: long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
jan@42463: not be applicable).
jan@42463: 
jan@42463: \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
jan@42463: if {\it tactic} is applicable, then it is applied to {\it term},
neuper@42483: otherwise {\it term} is passed on without changes.
jan@42463: 
jan@42463: \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
neuper@42483: term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
neuper@42483: it is applied to the first {\it term} yielding another {\it term},
neuper@42483: otherwise the second {\it tactic} is applied; if none is applicable an
neuper@42483: exception is raised.
jan@42463: 
jan@42463: \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
neuper@42483: term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
neuper@42483: first {\it term} yielding an intermediate term (not appearing in the
neuper@42483: signature) to which the second {\it tactic} is applied.
jan@42463: 
jan@42463: \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
neuper@42483: term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
neuper@42483: {\it tactic} is applied to the first {\it term} yielding an
neuper@42483: intermediate term (not appearing in the signature); the intermediate
neuper@42483: term is added to the environment the first {\it term} is evaluated in
neuper@42483: etc as long as the first {\it term} is true.
jan@42463: \end{description}
neuper@42483: The tacticals are not treated as break-points by Lucas-Interpretation
neuper@42483: and thus do not contribute to the calculation nor to interaction.
jan@42463: 
jan@42466: \section{Development of a Program on Trial}\label{trial} 
jan@42466: As mentioned above, {\sisac} is an experimental system for a proof of
jan@42466: concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}.  The
jan@42466: latter interprets a specific kind of TP-based programming language,
jan@42466: which is as experimental as the whole prototype --- so programming in
jan@42466: this language can be only ``on trial'', presently.  However, as a
jan@42466: prototype, the language addresses essentials described below.
jan@42466: 
jan@42466: \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
jan@42466: 
neuper@42467: %WN was Fachleute unter obigem Titel interessiert findet sich
jan@42466: %WN unterhalb des auskommentierten Textes.
jan@42466: 
jan@42466: %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
jan@42466: %WN auf Computer-Mathematiker fokussiert.
neuper@42464: % \paragraph{As mentioned in the introduction,} a prototype of an
neuper@42464: % educational math assistant called
neuper@42464: % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
neuper@42464: % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
neuper@42464: % the gap between (1) introducation and (2) application of mathematics:
neuper@42464: % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
neuper@42464: % requires each fact and each action justified by formal logic, so
neuper@42464: % {{{\sisac}{}}} makes justifications transparent to students in
neuper@42464: % interactive step-wise problem solving. By that way {{\sisac}} already
neuper@42464: % can serve both:
neuper@42464: % \begin{enumerate}
neuper@42464: %   \item Introduction of math stuff (in e.g. partial fraction
neuper@42464: % decomposition) by stepwise explaining and exercising respective
neuper@42464: % symbolic calculations with ``next step guidance (NSG)'' and rigorously
neuper@42464: % checking steps freely input by students --- this also in context with
neuper@42464: % advanced applications (where the stuff to be taught in higher
neuper@42464: % semesters can be skimmed through by NSG), and
neuper@42464: %   \item Application of math stuff in advanced engineering courses
neuper@42464: % (e.g. problems to be solved by inverse Z-transform in a Signal
neuper@42464: % Processing Lab) and now without much ado about basic math techniques
neuper@42464: % (like partial fraction decomposition): ``next step guidance'' supports
neuper@42464: % students in independently (re-)adopting such techniques.
neuper@42464: % \end{enumerate} 
neuper@42464: % Before the question is answers, how {{\sisac}}
neuper@42464: % accomplishes this task from a technical point of view, some remarks on
neuper@42464: % the state-of-the-art is given, therefor follow up Section~\ref{emas}.
neuper@42464: % 
neuper@42464: % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
neuper@42464: % 
jan@42466: % \paragraph{Educational software in mathematics} is, if at all, based
jan@42466: % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
jan@42466: % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
jan@42466: % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
jan@42466: % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
jan@42466: % base technologies are used to program math lessons and sometimes even
jan@42466: % exercises. The latter are cumbersome: the steps towards a solution of
jan@42466: % such an interactive exercise need to be provided with feedback, where
jan@42466: % at each step a wide variety of possible input has to be foreseen by
jan@42466: % the programmer - so such interactive exercises either require high
neuper@42464: % development efforts or the exercises constrain possible inputs.
neuper@42464: % 
jan@42466: % \subparagraph{A new generation} of educational math assistants (EMAs)
jan@42466: % is emerging presently, which is based on Theorem Proving (TP). TP, for
jan@42466: % instance Isabelle and Coq, is a technology which requires each fact
jan@42466: % and each action justified by formal logic. Pushed by demands for
jan@42466: % \textit{proven} correctness of safety-critical software TP advances
jan@42466: % into software engineering; from these advancements computer
jan@42466: % mathematics benefits in general, and math education in particular. Two
neuper@42464: % features of TP are immediately beneficial for learning:
neuper@42464: % 
jan@42466: % \paragraph{TP have knowledge in human readable format,} that is in
jan@42466: % standard predicate calculus. TP following the LCF-tradition have that
jan@42466: % knowledge down to the basic definitions of set, equality,
jan@42466: % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
jan@42466: % following the typical deductive development of math, natural numbers
jan@42466: % are defined and their properties
jan@42466: % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
jan@42466: % etc. Present knowledge mechanized in TP exceeds high-school
jan@42466: % mathematics by far, however by knowledge required in software
neuper@42464: % technology, and not in other engineering sciences.
neuper@42464: % 
jan@42466: % \paragraph{TP can model the whole problem solving process} in
jan@42466: % mathematical problem solving {\em within} a coherent logical
jan@42466: % framework. This is already being done by three projects, by
neuper@42464: % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
neuper@42464: % \par
jan@42466: % Having the whole problem solving process within a logical coherent
jan@42466: % system, such a design guarantees correctness of intermediate steps and
jan@42466: % of the result (which seems essential for math software); and the
jan@42466: % second advantage is that TP provides a wealth of theories which can be
jan@42466: % exploited for mechanizing other features essential for educational
neuper@42464: % software.
neuper@42464: % 
neuper@42464: % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
neuper@42464: % 
jan@42466: % One essential feature for educational software is feedback to user
neuper@42464: % input and assistance in coming to a solution.
neuper@42464: % 
jan@42466: % \paragraph{Checking user input} by ATP during stepwise problem solving
jan@42466: % is being accomplished by the three projects mentioned above
jan@42466: % exclusively. They model the whole problem solving process as mentioned
jan@42466: % above, so all what happens between formalized assumptions (or formal
jan@42466: % specification) and goal (or fulfilled postcondition) can be
jan@42466: % mechanized. Such mechanization promises to greatly extend the scope of
neuper@42464: % educational software in stepwise problem solving.
neuper@42464: % 
jan@42466: % \paragraph{NSG (Next step guidance)} comprises the system's ability to
jan@42466: % propose a next step; this is a challenge for TP: either a radical
jan@42466: % restriction of the search space by restriction to very specific
jan@42466: % problem classes is required, or much care and effort is required in
jan@42466: % designing possible variants in the process of problem solving
neuper@42464: % \cite{proof-strategies-11}.
neuper@42464: % \par
jan@42466: % Another approach is restricted to problem solving in engineering
jan@42466: % domains, where a problem is specified by input, precondition, output
jan@42466: % and postcondition, and where the postcondition is proven by ATP behind
jan@42466: % the scenes: Here the possible variants in the process of problem
jan@42466: % solving are provided with feedback {\em automatically}, if the problem
jan@42466: % is described in a TP-based programing language: \cite{plmms10} the
jan@42466: % programmer only describes the math algorithm without caring about
jan@42466: % interaction (the respective program is functional and even has no
jan@42466: % input or output statements!); interaction is generated as a
jan@42466: % side-effect by the interpreter --- an efficient separation of concern
jan@42466: % between math programmers and dialog designers promising application
neuper@42464: % all over engineering disciplines.
neuper@42464: % 
neuper@42464: % 
neuper@42464: % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
jan@42466: % Authoring new mathematics knowledge in {{\sisac}} can be compared with
jan@42466: % ``application programing'' of engineering problems; most of such
jan@42466: % programing uses CAS-based programing languages (CAS = Computer Algebra
neuper@42464: % Systems; e.g. Mathematica's or Maple's programing language).
neuper@42464: % 
jan@42466: % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
jan@42466: % \cite{plmms10} for describing how to construct a solution to an
jan@42466: % engineering problem and for calling equation solvers, integration,
jan@42466: % etc~\footnote{Implementation of CAS-like functionality in TP is not
jan@42466: % primarily concerned with efficiency, but with a didactic question:
jan@42466: % What to decide for: for high-brow algorithms at the state-of-the-art
jan@42466: % or for elementary algorithms comprehensible for students?} within TP;
jan@42466: % TP can ensure ``systems that never make a mistake'' \cite{casproto} -
neuper@42464: % are impossible for CAS which have no logics underlying.
neuper@42464: % 
jan@42466: % \subparagraph{Authoring is perfect} by writing such TP based programs;
jan@42466: % the application programmer is not concerned with interaction or with
jan@42466: % user guidance: this is concern of a novel kind of program interpreter
jan@42466: % called Lucas-Interpreter. This interpreter hands over control to a
jan@42466: % dialog component at each step of calculation (like a debugger at
jan@42466: % breakpoints) and calls automated TP to check user input following
neuper@42464: % personalized strategies according to a feedback module.
neuper@42464: % \par
jan@42466: % However ``application programing with TP'' is not done with writing a
jan@42466: % program: according to the principles of TP, each step must be
jan@42466: % justified. Such justifications are given by theorems. So all steps
jan@42466: % must be related to some theorem, if there is no such theorem it must
jan@42466: % be added to the existing knowledge, which is organized in so-called
jan@42466: % \textbf{theories} in Isabelle. A theorem must be proven; fortunately
jan@42466: % Isabelle comprises a mechanism (called ``axiomatization''), which
jan@42466: % allows to omit proofs. Such a theorem is shown in
neuper@42464: % Example~\ref{eg:neuper1}.
jan@42466: 
jan@42466: The running example, introduced by Fig.\ref{fig-interactive} on
jan@42466: p.\pageref{fig-interactive}, requires to determine the inverse $\cal
jan@42466: Z$-transform for a class of functions. The domain of Signal Processing
jan@42466: is accustomed to specific notation for the resulting functions, which
jan@42466: are absolutely summable and are called TODO: $u[n]$, where $u$ is the
jan@42466: function, $n$ is the argument and the brackets indicate that the
jan@42466: arguments are TODO. Surprisingly, Isabelle accepts the rules for
jan@42466: ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
jan@42466: experts might be particularly surprised, that the brackets do not
jan@42466: cause errors in typing (as lists).}:
neuper@42464: %\vbox{
neuper@42464: % \begin{example}
jan@42463:   \label{eg:neuper1}
jan@42463:   {\small\begin{tabbing}
jan@42463:   123\=123\=123\=123\=\kill
jan@42463:   \hfill \\
jan@42463:   \>axiomatization where \\
neuper@42464:   \>\>  rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
neuper@42464:   \>\>  rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
jan@42466:   \>\>  rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
jan@42466: %TODO
jan@42466:   \>\>  rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
jan@42466: %TODO
jan@42466:   \>\>  rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
jan@42466: %TODO
jan@42466:   \>\>  rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
jan@42466: %TODO
jan@42463:   \end{tabbing}
jan@42463:   }
neuper@42464: % \end{example}
jan@42466: %}
jan@42466: These 6 rules can be used as conditional rewrite rules, depending on
jan@42466: the respective convergence radius. Satisfaction from accordance with traditional notation
jan@42466: contrasts with the above word {\em axiomatization}: As TP-based, the
jan@42466: programming language expects these rules as {\em proved} theorems, and
jan@42466: not as axioms implemented in the above brute force manner; otherwise
jan@42466: all the verification efforts envisaged (like proof of the
jan@42466: post-condition, see below) would be meaningless.
jan@42466: 
jan@42466: Isabelle provides a large body of knowledge, rigorously proven from
jan@42466: the basic axioms of mathematics~\footnote{This way of rigorously
jan@42466: deriving all knowledge from first principles is called the
jan@42466: LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
jan@42466: knowledge can be found in the theoris on Multivariate
jan@42466: Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
jan@42466: building up knowledge such that a proof for the above rules would be
jan@42466: reasonably short and easily comprehensible, still requires lots of
jan@42466: work (and is definitely out of scope of our case study).
jan@42466: 
jan@42466: \paragraph{At the state-of-the-art in mechanization of knowledge} in
jan@42466: engineering sciences, the process does not stop with the mechanization of
neuper@42478: mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{
neuper@42478: fm-03}
jan@42466: are expected to proceed to formal and explicit description of physical items.  Signal Processing,
jan@42466: for instance is concerned with physical devices for signal acquisition
jan@42466: and reconstruction, which involve measuring a physical signal, storing
jan@42466: it, and possibly later rebuilding the original signal or an
jan@42466: approximation thereof. For digital systems, this typically includes
jan@42466: sampling and quantization; devices for signal compression, including
jan@42466: audio compression, image compression, and video compression, etc.
neuper@42478: ``Domain engineering''\cite{db:dom-eng} is concerned with
jan@42466: {\em specification} of these devices' components and features; this
jan@42466: part in the process of mechanization is only at the beginning in domains
jan@42466: like Signal Processing.
jan@42466: 
jan@42466: \subparagraph{TP-based programming, concern of this paper,} is determined to
jan@42466: add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
jan@42466: p.\pageref{fig:mathuni}.  As we shall see below, TP-based programming
jan@42466: starts with a formal {\em specification} of the problem to be solved.
neuper@42478: \begin{figure}
neuper@42478:   \begin{center}
neuper@42483:     \includegraphics[width=110mm]{fig/math-universe-small}
neuper@42478:     \caption{Didactic ``Math-Universe'': Algorithmic Knowledge
neuper@42478: (Programs) is combined with Application-oriented Knowledge
neuper@42478: (Specifications) and Deductive Knowledge (Axioms, Definitions,
neuper@42478: Theorems). The Result leads to a three dimensional math
neuper@42478: universe.}
neuper@42478:     \label{fig:mathuni}
neuper@42478:   \end{center}
neuper@42478: \end{figure}
jan@42466: 
jan@42466: 
jan@42466: \subsection{Specification of the Problem}\label{spec}
jan@42466: %WN <--> \chapter 7 der Thesis
jan@42466: %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
jan@42466: 
jan@42466: The problem of the running example is textually described in
jan@42466: Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
jan@42466: formal} specification of this problem, in traditional mathematical
jan@42469: notation, could look like is this:
jan@42466: 
jan@42466: %WN Hier brauchen wir die Spezifikation des 'running example' ...
jan@42466: %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
jan@42466: %JR der post condition - die existiert für uns ja eigentlich nicht aka
neuper@42467: %JR haben sie bis jetzt nicht beachtet WN...
neuper@42467: %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
jan@42473: %JR2 done
jan@42466: 
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 \\
neuper@42465:   Specification:\\
jan@42466:     \>input    \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
jan@42470:   \>precond  \>: filterExpression continius on $\mathbb{R}$ \\
jan@42466:   \>output   \>: stepResponse $x[n]$ \\
jan@42469:   \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
jan@42466: 
jan@42473: \begin{remark}
jan@42473:    Defining the postcondition requires a high amount mathematical 
jan@42473:    knowledge, the difficult part in our case is not to set up this condition 
jan@42473:    nor it is more to define it in a way the interpreter is able to handle it. 
jan@42473:    Due the fact that implementing that mechanisms is quite the same amount as 
jan@42473:    creating the programm itself, it is not avaible in our prototype.
jan@42473:    \label{rm:postcond}
jan@42473: \end{remark}
jan@42469: 
jan@42469: \paragraph{The implementation} of the formal specification in the present
jan@42466: prototype, still bar-bones without support for authoring:
jan@42466: %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
neuper@42480: {\footnotesize\label{exp-spec}
jan@42466: \begin{verbatim}
jan@42466:    01  store_specification
jan@42466:    02    (prepare_specification
jan@42466:    03      ["Jan Rocnik"]
jan@42466:    04      "pbl_SP_Ztrans_inv"
jan@42466:    05      thy
jan@42466:    06      ( ["Inverse", "Z_Transform", "SignalProcessing"],
jan@42466:    07        [ ("#Given", ["filterExpression X_eq"]),
jan@42466:    08          ("#Pre"  , ["X_eq is_continuous"]),
jan@42466:    19          ("#Find" , ["stepResponse n_eq"]),
jan@42466:    10          ("#Post" , [" TODO "])],
jan@42466:    11        append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)], 
jan@42466:    12        NONE, 
jan@42466:    13        [["SignalProcessing","Z_Transform","Inverse"]]));
jan@42466: \end{verbatim}}
jan@42466: Although the above details are partly very technical, we explain them
jan@42466: in order to document some intricacies of TP-based programming in the
jan@42466: present state of the {\sisac} prototype:
jan@42466: \begin{description}
jan@42466: \item[01..02]\textit{store\_specification:} stores the result of the
jan@42466: function \textit{prep\_specification} in a global reference
jan@42466: \textit{Unsynchronized.ref}, which causes principal conflicts with
jan@42466: Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
jan@42466: parallel execution~\cite{Makarius-09:parall-proof} and is under
jan@42466: reconstruction already.
jan@42466: 
jan@42466: \textit{prep\_pbt:} translates the specification to an internal format
jan@42466: which allows efficient processing; see for instance line {\rm 07}
jan@42466: below.
jan@42466: \item[03..04] are the ``mathematics author'' holding the copy-rights
jan@42466: and a unique identifier for the specification within {\sisac},
jan@42466: complare line {\rm 06}.
jan@42466: \item[05] is the Isabelle \textit{theory} required to parse the
jan@42466: specification in lines {\rm 07..10}.
jan@42466: \item[06] is a key into the tree of all specifications as presented to
jan@42466: the user (where some branches might be hidden by the dialog
jan@42466: component).
jan@42466: \item[07..10] are the specification with input, pre-condition, output
jan@42466: and post-condition respectively; the post-condition is not handled in
jan@42473: the prototype presently. (Follow up Remark~\ref{rm:postcond})
jan@42466: \item[11] creates a term rewriting system (abbreviated \textit{rls} in
jan@42466: {\sisac}) which evaluates the pre-condition for the actual input data.
jan@42466: Only if the evaluation yields \textit{True}, a program con be started.
jan@42466: \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
jan@42466: problem associated to a function from Computer Algebra (like an
jan@42466: equation solver) which is not the case here.
jan@42466: \item[13] is the specific key into the tree of programs addressing a
jan@42466: method which is able to find a solution which satiesfies the
jan@42466: post-condition of the specification.
jan@42466: \end{description}
jan@42466: 
jan@42466: 
jan@42466: %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
jan@42466: %WN ...
jan@42466: %  type pbt = 
jan@42466: %     {guh  : guh,         (*unique within this isac-knowledge*)
jan@42466: %      mathauthors: string list, (*copyright*)
jan@42466: %      init  : pblID,      (*to start refinement with*)
jan@42466: %      thy   : theory,     (* which allows to compile that pbt
jan@42466: %			  TODO: search generalized for subthy (ref.p.69*)
jan@42466: %      (*^^^ WN050912 NOT used during application of the problem,
jan@42466: %       because applied terms may be from 'subthy' as well as from super;
jan@42466: %       thus we take 'maxthy'; see match_ags !*)
jan@42466: %      cas   : term option,(*'CAS-command'*)
jan@42466: %      prls  : rls,        (* for preds in where_*)
jan@42466: %      where_: term list,  (* where - predicates*)
jan@42466: %      ppc   : pat list,
jan@42466: %      (*this is the model-pattern; 
jan@42466: %       it contains "#Given","#Where","#Find","#Relate"-patterns
jan@42466: %       for constraints on identifiers see "fun cpy_nam"*)
jan@42466: %      met   : metID list}; (* methods solving the pbt*)
jan@42466: %
jan@42466: %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
jan@42466: %WN oben selbst geschrieben.
jan@42466: 
jan@42466: 
jan@42466: 
jan@42466: 
jan@42466: %WN das w"urde ich in \sec\label{progr} verschieben und
jan@42466: %WN das SubProblem partial fractions zum Erkl"aren verwenden.
jan@42466: % Such a specification is checked before the execution of a program is
jan@42466: % started, the same applies for sub-programs. In the following example
neuper@42465: % (Example~\ref{eg:subprob}) shows the call of such a subproblem:
neuper@42465: % 
neuper@42465: % \vbox{
neuper@42465: %   \begin{example}
neuper@42465: %   \label{eg:subprob}
neuper@42465: %   \hfill \\
neuper@42465: %   {\ttfamily \begin{tabbing}
neuper@42465: %   ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
neuper@42465: %   ``\>\>[linear,univariate,equation,test],'' \\
neuper@42465: %   ``\>\>[Test,solve\_linear])'' \\
neuper@42465: %   ``\>[BOOL equ, REAL z])'' \\
neuper@42465: %   \end{tabbing}
neuper@42465: %   }
neuper@42465: %   {\small\textit{
jan@42466: %     \noindent If a program requires a result which has to be
jan@42466: % calculated first we can use a subproblem to do so. In our specific
jan@42466: % case we wanted to calculate the zeros of a fraction and used a
neuper@42465: % subproblem to calculate the zeros of the denominator polynom.
neuper@42465: %     }}
neuper@42465: %   \end{example}
neuper@42465: % }
jan@42466: 
jan@42466: \subsection{Implementation of the Method}\label{meth}
jan@42466: %WN <--> \chapter 7 der Thesis
jan@42466: TODO
jan@42466: \subsection{Preparation of Simplifiers for the Program}\label{simp}
jan@42469: 
neuper@42480: \paragraph{After collecting} informations about the problem 
neuper@42480: %WN4 welche 'informations' ?
neuper@42480: %WN4 Wenn das welche sind, die oben NICHT vorgekommen sind, dann anf"uhren
neuper@42480: %WN4 Wenn das welche sind, die oben SCHON vorgekommen sind, dann weglassen
neuper@42480: %WN4                       und Platz sparen.
neuper@42480: %WN4 
neuper@42480: %WN4 Wenn wir diese Bemerkung hier weglassen (sie m"usste eigentlich an jedem
neuper@42480: %WN4 Beginn von 3.* stehen), dann kommt sie gleich an den Anfang
neuper@42480: %WN4 nach der "Uberschrift von 3.
neuper@42480: and reviewing the calculations, 
neuper@42480: %WN4 welche 'calculations', ist von solchen bisher schon die Rede gewesen ?
neuper@42480: the programm may be seem hard and heavy, therefor we can set up
jan@42475: some simplifications, for e.g. is the simplification of reational expressions
neuper@42480: already provided in the {\sisac{}} system. 
neuper@42480: %WN4 
neuper@42480: Also obligate is the use of the 
jan@42475: function \texttt{drop\_questionmarks} which excludes irrelevant symbols out of
jan@42475: the expression. (Irrelevant symbols may be result out of the system during the
jan@42475: calculation.)
jan@42475: 
jan@42475: \subparagraph{Simplifiers often are represented} through rulesets\footnote{More
jan@42475: information about rulesets can be found in \S\ref{sec:rules}}, this rulesets
jan@42475: tell the machine which terms should be simplified into which representation. In
jan@42475: the upcoming programm a simplification is applied only in using such rulesets
jan@42475: on existing terms.
jan@42475: \par
jan@42475: Following example line was taken out of a finished programm and shows how
jan@42475: an rational expression can be simplified.
jan@42475: 
jan@42475: \begin{example}
jan@42475: \begin{verbatim}
jan@42475: 
jan@42475:   "expression = (Rewrite_Set norm_Rational False) expression;"^\end{verbatim}
jan@42475: \end{example}
jan@42475: 
jan@42475: \subparagraph{If other} methods for use in term with simplification are needed
jan@42475: \S\ref{funs} gives informations about new ML-Functions can be prepared.
jan@42469: 
jan@42466: \subsection{Preparation of ML-Functions}\label{funs}
jan@42469: 
jan@42469: \paragraph{Explicit Problems} require explicit methods to solve them, and within
jan@42469: this methods we have some explicit steps to do. This steps can be unique for
jan@42469: a special problem or refindable in other problems. No mather what case, such
jan@42469: steps often require some technical functions behind. For the solving process
jan@42469: of the Inverse Z Transformation and the corresponding partial fraction it was
jan@42469: neccessary to build helping functions like \texttt{get\_denominator},
jan@42469: \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
jan@42473: to filter the denominator or numerator out of a fraction, last one helps us to
jan@42469: get to know the bound variable in a equation.
jan@42469: \par
jan@42473: By taking \texttt{get\_denominator} as an example, we want to explain how to 
jan@42473: implement new functions into the existing system and how we can later use them
jan@42473: in our program.
jan@42469: 
jan@42469: \subsubsection{Find a place to Store the Function}
jan@42473: 
jan@42469: The whole system builds up on a well defined structure of Knowledge. This
jan@42473: Knowledge sets up at the Path:
jan@42473: \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
jan@42470: For implementing the Function \texttt{get\_denominator} (which let us extract
jan@42470: the denominator out of a fraction) we have choosen the Theory (file)
jan@42469: \texttt{Rational.thy}.
jan@42469: 
jan@42469: \subsubsection{Write down the new Function}
jan@42473: 
jan@42470: In upper Theory we now define the new function and its purpose:
jan@42470: \begin{verbatim}
jan@42470:   get_denominator :: "real => real"
jan@42470: \end{verbatim}
jan@42470: This command tells the machine that a function with the name
jan@42470: \texttt{get\_denominator} exists which gets a real expression as argument and
jan@42473: returns once again a real expression. Now we are able to implement the function
jan@42473: itself, Example~\ref{eg:getdenom} now shows the implementation of
jan@42473: \texttt{get\_denominator}.
jan@42469: 
jan@42469: \begin{example}
jan@42470:   \label{eg:getdenom}
jan@42470:   \begin{verbatim}
jan@42469: 
jan@42470: 01  (*
jan@42470: 02   *("get_denominator",
jan@42470: 03   *  ("Rational.get_denominator", eval_get_denominator ""))
jan@42470: 04   *)
jan@42470: 05  fun eval_get_denominator (thmid:string) _ 
jan@42470: 06            (t as Const ("Rational.get_denominator", _) $
jan@42470: 07                (Const ("Rings.inverse_class.divide", _) $num 
jan@42470: 08                  $denom)) thy = 
jan@42470: 09          SOME (mk_thmid thmid "" 
jan@42470: 10              (Print_Mode.setmp [] 
jan@42470: 11                (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
jan@42470: 12              Trueprop $ (mk_equality (t, denom)))
jan@42470: 13    | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
jan@42469: \end{example}
jan@42469: 
jan@42470: Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
jan@42470: there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont) 
jan@42470: splittet
jan@42473: into its two parts (\texttt{\$num \$denom}). The lines before are additionals
jan@42470: commands for declaring the function and the lines after are modeling and 
jan@42470: returning a real variable out of \texttt{\$denom}.
jan@42469: 
jan@42469: \subsubsection{Add a test for the new Function}
jan@42469: 
jan@42473: \paragraph{Everytime when adding} a new function it is essential also to add
jan@42473: a test for it. Tests for all functions are sorted in the same structure as the
jan@42473: knowledge it self and can be found up from the path:
jan@42473: \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
jan@42473: This tests are nothing very special, as a first prototype the functionallity
jan@42473: of a function can be checked by evaluating the result of a simple expression
jan@42473: passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
jan@42473: \textit{just} created function \texttt{get\_denominator}.
jan@42469: 
jan@42473: \begin{example}
jan@42473: \label{eg:getdenomtest}
jan@42473: \begin{verbatim}
jan@42473: 
jan@42473: 01 val thy = @{theory Isac};
jan@42473: 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
jan@42473: 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
jan@42473: 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
jan@42473: 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
jan@42473: \end{example}
jan@42473: 
jan@42473: \begin{description}
jan@42473: \item[01] checks if the proofer set up on our {\sisac{}} System.
jan@42473: \item[02] passes a simple expression (fraction) to our suddenly created
jan@42473:           function.
jan@42473: \item[04] checks if the resulting variable is the correct one (in this case
jan@42473:           ``b'' the denominator) and returns.
jan@42473: \item[05] handels the error case and reports that the function is not able to
jan@42473:           solve the given problem.
jan@42473: \end{description}
jan@42469: 
neuper@42478: \subsection{Implementation of the TP-based Program}\label{progr} 
neuper@42480: So finally all the prerequisites are described and the very topic can
neuper@42480: be addressed. The program below comes back to the running example: it
neuper@42480: computes a solution for the problem from Fig.\ref{fig-interactive} on
neuper@42480: p.\pageref{fig-interactive}. The reader is reminded of
neuper@42480: \S\ref{PL-isab}, the introduction of the programming language:
neuper@42482: {\small\it\label{s:impl}
neuper@42482: \begin{tabbing}
neuper@42478: 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
neuper@42480: \>{\rm 00}\>val program =\\
neuper@42480: \>{\rm 01}\>  "{\tt Program} InverseZTransform (X\_eq::bool) =   \\
neuper@42482: \>{\rm 02}\>\>  {\tt let}                                       \\
neuper@42468: \>{\rm 03}\>\>\>  X\_eq = {\tt Take} X\_eq ;   \\
neuper@42468: \>{\rm 04}\>\>\>  X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
neuper@42468: \>{\rm 05}\>\>\>  (X\_z::real) = lhs X\_eq ;       \\ %no inside-out evaluation
neuper@42468: \>{\rm 06}\>\>\>  (z::real) = argument\_in X\_z; \\
neuper@42468: \>{\rm 07}\>\>\>  (part\_frac::real) = {\tt SubProblem} \\
neuper@42478: \>{\rm 08}\>\>\>\>\>\>\>\>  ( Isac, [partial\_fraction, rational, simplification], [] )\\
neuper@42478: %\>{\rm 10}\>\>\>\>\>\>\>\>\>  [simplification, of\_rationals, to\_partial\_fraction] ) \\
neuper@42478: \>{\rm 09}\>\>\>\>\>\>\>\>  [ (rhs X\_eq)::real, z::real ]; \\
neuper@42478: \>{\rm 10}\>\>\>  (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
neuper@42478: \>{\rm 11}\>\>\>  X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@   \\
neuper@42478: \>{\rm 12}\>\>\>\>\>  $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
neuper@42482: \>{\rm 13}\>\>  {\tt in } \\
neuper@42480: \>{\rm 14}\>\>\>  X'\_eq"
neuper@42478: \end{tabbing}}
neuper@42468: % ORIGINAL FROM Inverse_Z_Transform.thy
neuper@42468: % "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
neuper@42468: % "(let X = Take X_eq;                                "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
neuper@42468: % "  X' = Rewrite ruleZY False X;                     "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
neuper@42468: % "  (X'_z::real) = lhs X';                           "^(*            ?X' z*)
neuper@42468: % "  (zzz::real) = argument_in X'_z;                  "^(*            z *)
neuper@42468: % "  (funterm::real) = rhs X';                        "^(*            3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
neuper@42468: %
neuper@42468: % "  (pbz::real) = (SubProblem (Isac',                "^(**)
neuper@42468: % "    [partial_fraction,rational,simplification],    "^
neuper@42468: % "    [simplification,of_rationals,to_partial_fraction]) "^
neuper@42468: % "    [REAL funterm, REAL zzz]);                     "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
neuper@42468: %
neuper@42468: % "  (pbz_eq::bool) = Take (X'_z = pbz);              "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
neuper@42468: % "  pbz_eq = Rewrite ruleYZ False pbz_eq;            "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
neuper@42468: % "  pbz_eq = drop_questionmarks pbz_eq;              "^(*               4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
neuper@42468: % "  (X_zeq::bool) = Take (X_z = rhs pbz_eq);         "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
neuper@42468: % "  n_eq = (Rewrite_Set inverse_z False) X_zeq;      "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
neuper@42468: % "  n_eq = drop_questionmarks n_eq                   "^(*            X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
neuper@42468: % "in n_eq)"                                            (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
neuper@42480: The program is represented as a string and part of the method in
neuper@42480: \S\ref{meth}.  As mentioned in \S\ref{PL} the program is purely
neuper@42480: functional and lacks any input statements and output statements. So
neuper@42480: the steps of calculation towards a solution (and interactive tutoring
neuper@42480: in step-wise problem solving) are created as a side-effect by
neuper@42480: Lucas-Interpretation.  The side-effects are triggered by the tactics
neuper@42482: \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
neuper@42482: \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
neuper@42480: {\rm 12} respectively. These tactics produce the lines in the
neuper@42480: calculation on p.\pageref{flow-impl}.
neuper@42478: 
neuper@42480: The above lines {\rm 05, 06} do not contain a tactics, so they do not
neuper@42480: immediately contribute to the calculation on p.\pageref{flow-impl};
neuper@42482: rather, they compute actual arguments for the \texttt{SubProblem} in
neuper@42480: line {\rm 09}~\footnote{The tactics also are break-points for the
neuper@42480: interpreter, where control is handed over to the user in interactive
neuper@42482: tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
neuper@42480: 
neuper@42480: \medskip The above program also indicates the dominant role of interactive
neuper@42478: selection of knowledge in the three-dimensional universe of
neuper@42478: mathematics as depicted in Fig.\ref{fig:mathuni} on
neuper@42482: p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines
neuper@42478: {\rm 07..09} is more than a function call with the actual arguments
neuper@42478: \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
neuper@42478: three items:
neuper@42480: 
neuper@42478: \begin{enumerate}
neuper@42478: \item the theory, in the example \textit{Isac} because different
neuper@42478: methods can be selected in Pt.3 below, which are defined in different
neuper@42478: theories with \textit{Isac} collecting them.
neuper@42480: \item the specification identified by \textit{[partial\_fraction,
neuper@42480: rational, simplification]} in the tree of specifications; this
neuper@42480: specification is analogous to the specification of the main program
neuper@42480: described in \S\ref{spec}; the problem is to find a ``partial fraction
neuper@42480: decomposition'' for a univariate rational polynomial.
neuper@42480: \item the method in the above example is \textit{[ ]}, i.e. empty,
neuper@42480: which supposes the interpreter to select one of the methods predefined
neuper@42480: in the specification, for instance in line {\rm 13} in the running
neuper@42480: example's specification on p.\pageref{exp-spec}~\footnote{The freedom
neuper@42480: (or obligation) for selection carries over to the student in
neuper@42480: interactive tutoring.}.
neuper@42478: \end{enumerate}
neuper@42478: 
neuper@42480: The program code, above presented as a string, is parsed by Isabelle's
neuper@42480: parser --- the program is an Isabelle term. This fact is expected to
neuper@42480: simplify verification tasks in the future; on the other hand, this
neuper@42480: fact causes troubles in error detectetion which are discussed as part
neuper@42480: of the workflow in the subsequent section.
neuper@42467: 
jan@42463: \section{Workflow of Programming in the Prototype}\label{workflow}
neuper@42480: The previous section presented all the duties and tasks to be accomplished by
neuper@42481: programmers of TP-based languages. Some tasks are interrelated and comprehensive,
neuper@42481: so first experiences with the workflow in programming are noted below. The notes
neuper@42481: also capture requirements for future language development.
neuper@42468: 
jan@42466: \subsection{Preparations and Trials}\label{flow-prep}
neuper@42481: % Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''
neuper@42481: The new graphical user-interface of Isabelle~\cite{makar-jedit-12} is a great
neuper@42481: step forward for interactive theory and proof development --- and so it is for
neuper@42481: interactive program development; the specific requirements raised by interactive
neuper@42481: programming will be mentioned separately.
neuper@42481: 
neuper@42481: The development in the {\sisac}-prototype was done in a separate
neuper@42481: theory~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}.
neuper@42481: The workflow tackled the tasks more or less following the order of the
neuper@42482: above sections from \S\ref{isabisac} to \S\ref{funs}. At each stage
neuper@42482: the interactivity of Isabelle/jEdit is very supportive. For instance,
neuper@42482: as soon as the theorems for the Z-transform are established (see
neuper@42482: \S\ref{isabisac}) it is tempting to see them at work: First we need
neuper@42482: technical prerequisites not worth to mention and parse a string to a
neuper@42482: term using {\sisac}'s function \textit{str2term}:
neuper@42482: {\footnotesize\label{exp-spec}
neuper@42482: \begin{verbatim}
neuper@42482:    ML {*
neuper@42482:      val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
neuper@42482:      val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
neuper@42482:    *}
neuper@42482: \end{verbatim}}
neuper@42482: Then we call {\sisac}'s rewrite-engine directly by \textit{rewrite\_} (instead via Lucas-Interpreter by \textit{Rewrite}) and yield
neuper@42482: a rewritten term \textit{t'} together with assumptions:
neuper@42482: {\footnotesize\label{exp-spec}
neuper@42482: \begin{verbatim}
neuper@42482:    ML {*
neuper@42482:      val SOME (t', asm) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
neuper@42482:    *}
neuper@42482: \end{verbatim}}
neuper@42482: And any evaluation of an \texttt{ML} section immediately responds with the
neuper@42482: values computed, for instance with the result of the rewrites, which above
neuper@42482: have been returned in the internal term representation --- here are the more
neuper@42482: readable string representations:
neuper@42482: {\footnotesize\label{exp-spec}
neuper@42482: \begin{verbatim}
neuper@42482:    ML {*
neuper@42482:      term2str t';
neuper@42482:      terms2str (asm);
neuper@42482:    *}
neuper@42482:    val it = "- ?u [- ?n - 1] + z / (z - α) + 1": string
neuper@42482:    val it = "[|| z || < 1]": string
neuper@42482: \end{verbatim}}
neuper@42482: Looking at the last line shows how the system will reliably handle
neuper@42482: assumptions like the convergence radius.
neuper@42482: %WN gerne w"urde ich oben das Beispiel aus subsection {*Apply Rules*}
neuper@42482: %WN aus http://www.ist.tugraz.at/projects/isac/publ/Build_Inverse_Z_Transform.thy.
neuper@42482: %WN Leider bekomme ich einen Fehler --- siehst Du eine schnelle Korrektur ?
neuper@42481: 
neuper@42481: 
neuper@42482: .\\.\\.\\
neuper@42482: 
neuper@42482: TODO test the function \textit{argument\_of} which is embedded in the
neuper@42482: ruleset which is used to evaluate the program by the Lucas-Interpreter.
neuper@42481: 
neuper@42468: .\\.\\.\\
neuper@42468: 
jan@42469: %JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich
jan@42469: %JR: eingefügt; das war der beinn unserer Arbeit in
jan@42469: %JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei
jan@42469: %JR: jedem neuen Programm nötigen Schritte.
jan@42469: 
neuper@42468: \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
neuper@42468: 
jan@42469: \paragraph{At the beginning} of the implementation it is good to decide on one
jan@42469: way the problem should be solved. We also did this for our Z-Transformation
jan@42469: Problem and have choosen the way it is also thaugt in the Signal Processing
jan@42469: Problem classes.
jan@42469: \subparagraph{By writing down} each of this neccesarry steps we are describing
jan@42469: one line of our upcoming program. In the following example we show the 
jan@42469: Calculation on the left and on the right the tactics in the program which
jan@42469: created the respective formula on the left.
jan@42469: 
jan@42469: \begin{example}
jan@42469: \hfill\\
neuper@42468: {\small\it
neuper@42468: \begin{tabbing}
neuper@42468: 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
neuper@42468: \>{\rm 01}\> $\bullet$  \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing])       \`\\
neuper@42468: \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$       \`{\footnotesize {\tt Take} X\_eq}\\
neuper@42468: \>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$          \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\
neuper@42468: \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification]        \`{\footnotesize {\tt SubProblem} \dots}\\
neuper@42468: \>{\rm 05}\>\>\>  $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$    \`- - -\\
neuper@42468: \>{\rm 06}\>\>\>  $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$                                   \`- - -\\
neuper@42468: \>{\rm 07}\>\>\>  $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ )                      \`- - -\\
neuper@42468: \>{\rm 08}\>\>\>\>   $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
neuper@42468: \>{\rm 09}\>\>\>\>   $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$           \`- - -\\
neuper@42468: \>{\rm 10}\>\>\>\>   $z = \frac{1}{2}\;\lor\;z =$ \_\_\_                                           \`- - -\\
neuper@42468: \>        \>\>\>\>   \_\_\_                                                                        \`- - -\\
neuper@42468: \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$                   \`\\
neuper@42468: \>{\rm 12}\>\> $X^\prime z = {\cal Z}^{-1} (\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}})$ \`{\footnotesize {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac)}\\
neuper@42468: \>{\rm 13}\>\> $X^\prime z = {\cal Z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} ruleYZ X'\_eq }\\
neuper@42468: \>{\rm 14}\>\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$  \`{\footnotesize {\tt Rewrite\_Set} inverse\_z X'\_eq}\\
neuper@42468: \>{\rm 15}\> \dots\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Check\_Postcond}}
neuper@42468: \end{tabbing}}
jan@42469: 
jan@42469: \end{example}
jan@42469: 
neuper@42468: % ORIGINAL FROM Inverse_Z_Transform.thy
neuper@42468: %    "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
neuper@42468: %    "(let X = Take X_eq;                                "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
neuper@42468: %    "  X' = Rewrite ruleZY False X;                     "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
neuper@42468: %    "  (X'_z::real) = lhs X';                           "^(*            ?X' z*)
neuper@42468: %    "  (zzz::real) = argument_in X'_z;                  "^(*            z *)
neuper@42468: %    "  (funterm::real) = rhs X';                        "^(*            3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
neuper@42468: % 
neuper@42468: %    "  (pbz::real) = (SubProblem (Isac',                "^(**)
neuper@42468: %    "    [partial_fraction,rational,simplification],    "^
neuper@42468: %    "    [simplification,of_rationals,to_partial_fraction]) "^
neuper@42468: %    "    [REAL funterm, REAL zzz]);                     "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
neuper@42468: % 
neuper@42468: %    "  (pbz_eq::bool) = Take (X'_z = pbz);              "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
neuper@42468: %    "  pbz_eq = Rewrite ruleYZ False pbz_eq;            "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
neuper@42468: %    "  pbz_eq = drop_questionmarks pbz_eq;              "^(*               4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
neuper@42468: %    "  (X_zeq::bool) = Take (X_z = rhs pbz_eq);         "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
neuper@42468: %    "  n_eq = (Rewrite_Set inverse_z False) X_zeq;      "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
neuper@42468: %    "  n_eq = drop_questionmarks n_eq                   "^(*            X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
neuper@42468: %    "in n_eq)"                                            (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
neuper@42468: 
neuper@42468: .\\.\\.\\
neuper@42468: 
neuper@42468: \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
neuper@42468: TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
neuper@42468: 
neuper@42468: 
neuper@42481: http://www.ist.tugraz.at/projects/isac/publ/Inverse\_Z\_Transform.thy
neuper@42468: 
neuper@42478: % \newpage
neuper@42478: % -------------------------------------------------------------------
neuper@42478: % 
neuper@42478: % Material, falls noch Platz bleibt ...
neuper@42478: % 
neuper@42478: % -------------------------------------------------------------------
neuper@42478: % 
neuper@42478: % 
neuper@42478: % \subsubsection{Trials on Notation and Termination}
neuper@42478: % 
neuper@42478: % \paragraph{Technical notations} are a big problem for our piece of software,
neuper@42478: % but the reason for that isn't a fault of the software itself, one of the
neuper@42478: % troubles comes out of the fact that different technical subtopics use different
neuper@42478: % symbols and notations for a different purpose. The most famous example for such
neuper@42478: % a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
neuper@42478: % math). In the specific part of signal processing one of this notation issues is
neuper@42478: % the use of brackets --- we use round brackets for analoge signals and squared
neuper@42478: % brackets for digital samples. Also if there is no problem for us to handle this
neuper@42478: % fact, we have to tell the machine what notation leads to wich meaning and that
neuper@42478: % this purpose seperation is only valid for this special topic - signal
neuper@42478: % processing.
neuper@42478: % \subparagraph{In the programming language} itself it is not possible to declare
neuper@42478: % fractions, exponents, absolutes and other operators or remarks in a way to make
neuper@42478: % them pretty to read; our only posssiblilty were ASCII characters and a handfull
neuper@42478: % greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
neuper@42478: % \par
neuper@42478: % With the upper collected knowledge it is possible to check if we were able to
neuper@42478: % donate all required terms and expressions.
neuper@42478: % 
neuper@42478: % \subsubsection{Definition and Usage of Rules}
neuper@42478: % 
neuper@42478: % \paragraph{The core} of our implemented problem is the Z-Transformation, due
neuper@42478: % the fact that the transformation itself would require higher math which isn't
neuper@42478: % yet avaible in our system we decided to choose the way like it is applied in
neuper@42478: % labratory and problem classes at our university - by applying transformation
neuper@42478: % rules (collected in transformation tables).
neuper@42478: % \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
neuper@42478: % use of axiomatizations like shown in Example~\ref{eg:ruledef}
neuper@42478: % 
neuper@42478: % \begin{example}
neuper@42478: %   \label{eg:ruledef}
neuper@42478: %   \hfill\\
neuper@42478: %   \begin{verbatim}
neuper@42478: %   axiomatization where
neuper@42478: %     rule1: ``1 = $\delta$[n]'' and
neuper@42478: %     rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
neuper@42478: %     rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
neuper@42478: %   \end{verbatim}
neuper@42478: % \end{example}
neuper@42478: % 
neuper@42478: % This rules can be collected in a ruleset and applied to a given expression as
neuper@42478: % follows in Example~\ref{eg:ruleapp}.
neuper@42478: % 
neuper@42478: % \begin{example}
neuper@42478: %   \hfill\\
neuper@42478: %   \label{eg:ruleapp}
neuper@42478: %   \begin{enumerate}
neuper@42478: %   \item Store rules in ruleset:
neuper@42478: %   \begin{verbatim}
neuper@42478: %   val inverse_Z = append_rls "inverse_Z" e_rls
neuper@42478: %     [ Thm ("rule1",num_str @{thm rule1}),
neuper@42478: %       Thm ("rule2",num_str @{thm rule2}),
neuper@42478: %       Thm ("rule3",num_str @{thm rule3})
neuper@42478: %     ];\end{verbatim}
neuper@42478: %   \item Define exression:
neuper@42478: %   \begin{verbatim}
neuper@42478: %   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
neuper@42478: %   \item Apply ruleset:
neuper@42478: %   \begin{verbatim}
neuper@42478: %   val SOME (sample_term', asm) = 
neuper@42478: %     rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
neuper@42478: %   \end{enumerate}
neuper@42478: % \end{example}
neuper@42478: % 
neuper@42478: % The use of rulesets makes it much easier to develop our designated applications,
neuper@42478: % but the programmer has to be careful and patient. When applying rulesets
neuper@42478: % two important issues have to be mentionend:
neuper@42478: % \subparagraph{How often} the rules have to be applied? In case of
neuper@42478: % transformations it is quite clear that we use them once but other fields
neuper@42478: % reuqire to apply rules until a special condition is reached (e.g.
neuper@42478: % a simplification is finished when there is nothing to be done left).
neuper@42478: % \subparagraph{The order} in which rules are applied often takes a big effect
neuper@42478: % and has to be evaluated for each purpose once again.
neuper@42478: % \par
neuper@42478: % In our special case of Signal Processing and the rules defined in
neuper@42478: % Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
neuper@42478: % constants. After this step has been done it no mather which rule fit's next.
neuper@42478: % 
neuper@42478: % \subsubsection{Helping Functions}
neuper@42478: % 
neuper@42478: % \paragraph{New Programms require,} often new ways to get through. This new ways
neuper@42478: % means that we handle functions that have not been in use yet, they can be 
neuper@42478: % something special and unique for a programm or something famous but unneeded in
neuper@42478: % the system yet. In our dedicated example it was for example neccessary to split
neuper@42478: % a fraction into numerator and denominator; the creation of such function and
neuper@42478: % even others is described in upper Sections~\ref{simp} and \ref{funs}.
neuper@42478: % 
neuper@42478: % \subsubsection{Trials on equation solving}
neuper@42478: % %simple eq and problem with double fractions/negative exponents
neuper@42478: % \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
neuper@42478: % equations degree one and two. Solving equations in the first degree is no 
neuper@42478: % problem, wether for a student nor for our machine; but even second degree
neuper@42478: % equations can lead to big troubles. The origin of this troubles leads from
neuper@42478: % the build up process of our equation solving functions; they have been
neuper@42478: % implemented some time ago and of course they are not as good as we want them to
neuper@42478: % be. Wether or not following we only want to show how cruel it is to build up new
neuper@42478: % work on not well fundamentials.
neuper@42478: % \subparagraph{A simple equation solving,} can be set up as shown in the next
neuper@42478: % example:
neuper@42478: % 
neuper@42478: % \begin{example}
neuper@42478: % \begin{verbatim}
neuper@42478: %   
neuper@42478: %   val fmz =
neuper@42478: %     ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
neuper@42478: %      "solveFor z",
neuper@42478: %      "solutions L"];                                    
neuper@42478: % 
neuper@42478: %   val (dI',pI',mI') =
neuper@42478: %     ("Isac", 
neuper@42478: %       ["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@42478: %       ["no_met"]);\end{verbatim}
neuper@42478: % \end{example}
neuper@42478: % 
neuper@42478: % Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
neuper@42478: % a short overview on the commands; at first we set up the equation and tell the
neuper@42478: % machine what's the bound variable and where to store the solution. Second step 
neuper@42478: % is to define the equation type and determine if we want to use a special method
neuper@42478: % to solve this type.) Simple checks tell us that the we will get two results for
neuper@42478: % this equation and this results will be real.
neuper@42478: % So far it is easy for us and for our machine to solve, but
neuper@42478: % mentioned that a unvariate equation second order can have three different types
neuper@42478: % of solutions it is getting worth.
neuper@42478: % \subparagraph{The solving of} all this types of solutions is not yet supported.
neuper@42478: % Luckily it was needed for us; but something which has been needed in this 
neuper@42478: % context, would have been the solving of an euation looking like:
neuper@42478: % $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
neuper@42478: % before (remember that befor it was no problem to handle for the machine) but
neuper@42478: % now, after a simple equivalent transformation, we are not able to solve
neuper@42478: % it anymore.
neuper@42478: % \subparagraph{Error messages} we get when we try to solve something like upside
neuper@42478: % were very confusing and also leads us to no special hint about a problem.
neuper@42478: % \par The fault behind is, that we have no well error handling on one side and
neuper@42478: % no sufficient formed equation solving on the other side. This two facts are
neuper@42478: % making the implemention of new material very difficult.
neuper@42478: % 
neuper@42478: % \subsection{Formalization of missing knowledge in Isabelle}
neuper@42478: % 
neuper@42478: % \paragraph{A problem} behind is the mechanization of mathematic
neuper@42478: % theories in TP-bases languages. There is still a huge gap between
neuper@42478: % these algorithms and this what we want as a solution - in Example
neuper@42478: % Signal Processing. 
neuper@42478: % 
neuper@42478: % \vbox{
neuper@42478: %   \begin{example}
neuper@42478: %     \label{eg:gap}
neuper@42478: %     \[
neuper@42478: %       X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
neuper@42478: %     \]
neuper@42478: %     {\small\textit{
neuper@42478: %       \noindent A very simple example on this what we call gap is the
neuper@42478: % simplification above. It is needles to say that it is correct and also
neuper@42478: % Isabelle for fills it correct - \emph{always}. But sometimes we don't
neuper@42478: % want expand such terms, sometimes we want another structure of
neuper@42478: % them. Think of a problem were we now would need only the coefficients
neuper@42478: % of $X$ and $Y$. This is what we call the gap between mechanical
neuper@42478: % simplification and the solution.
neuper@42478: %     }}
neuper@42478: %   \end{example}
neuper@42478: % }
neuper@42478: % 
neuper@42478: % \paragraph{We are not able to fill this gap,} until we have to live
neuper@42478: % with it but first have a look on the meaning of this statement:
neuper@42478: % Mechanized math starts from mathematical models and \emph{hopefully}
neuper@42478: % proceeds to match physics. Academic engineering starts from physics
neuper@42478: % (experimentation, measurement) and then proceeds to mathematical
neuper@42478: % modeling and formalization. The process from a physical observance to
neuper@42478: % a mathematical theory is unavoidable bound of setting up a big
neuper@42478: % collection of standards, rules, definition but also exceptions. These
neuper@42478: % are the things making mechanization that difficult.
neuper@42478: % 
neuper@42478: % \vbox{
neuper@42478: %   \begin{example}
neuper@42478: %     \label{eg:units}
neuper@42478: %     \[
neuper@42478: %       m,\ kg,\ s,\ldots
neuper@42478: %     \]
neuper@42478: %     {\small\textit{
neuper@42478: %       \noindent Think about some units like that one's above. Behind
neuper@42478: % each unit there is a discerning and very accurate definition: One
neuper@42478: % Meter is the distance the light travels, in a vacuum, through the time
neuper@42478: % of 1 / 299.792.458 second; one kilogram is the weight of a
neuper@42478: % platinum-iridium cylinder in paris; and so on. But are these
neuper@42478: % definitions usable in a computer mechanized world?!
neuper@42478: %     }}
neuper@42478: %   \end{example}
neuper@42478: % }
neuper@42478: % 
neuper@42478: % \paragraph{A computer} or a TP-System builds on programs with
neuper@42478: % predefined logical rules and does not know any mathematical trick
neuper@42478: % (follow up example \ref{eg:trick}) or recipe to walk around difficult
neuper@42478: % expressions. 
neuper@42478: % 
neuper@42478: % \vbox{
neuper@42478: %   \begin{example}
neuper@42478: %     \label{eg:trick}
neuper@42478: %   \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
neuper@42478: %   \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
neuper@42478: %      \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
neuper@42478: %   \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
neuper@42478: %     {\small\textit{
neuper@42478: %       \noindent Sometimes it is also useful to be able to apply some
neuper@42478: % \emph{tricks} to get a beautiful and particularly meaningful result,
neuper@42478: % which we are able to interpret. But as seen in this example it can be
neuper@42478: % hard to find out what operations have to be done to transform a result
neuper@42478: % into a meaningful one.
neuper@42478: %     }}
neuper@42478: %   \end{example}
neuper@42478: % }
neuper@42478: % 
neuper@42478: % \paragraph{The only possibility,} for such a system, is to work
neuper@42478: % through its known definitions and stops if none of these
neuper@42478: % fits. Specified on Signal Processing or any other application it is
neuper@42478: % often possible to walk through by doing simple creases. This creases
neuper@42478: % are in general based on simple math operational but the challenge is
neuper@42478: % to teach the machine \emph{all}\footnote{Its pride to call it
neuper@42478: % \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
neuper@42478: % reach a high level of \emph{all} but it in real it will still be a
neuper@42478: % survey of knowledge which links to other knowledge and {{\sisac}{}} a
neuper@42478: % trainer and helper but no human compensating calculator. 
neuper@42478: % \par
neuper@42478: % {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
neuper@42478: % specifications of problems out of topics from Signal Processing, etc.)
neuper@42478: % and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
neuper@42478: % physical knowledge. The result is a three-dimensional universe of
neuper@42478: % mathematics seen in Figure~\ref{fig:mathuni}.
neuper@42478: % 
neuper@42478: % \begin{figure}
neuper@42478: %   \begin{center}
neuper@42478: %     \includegraphics{fig/universe}
neuper@42478: %     \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
neuper@42478: %              combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
neuper@42478: %              leads to a three dimensional math universe.\label{fig:mathuni}}
neuper@42478: %   \end{center}
neuper@42478: % \end{figure}
neuper@42478: % 
neuper@42478: % %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
neuper@42478: % %WN bitte folgende Bezeichnungen nehmen:
neuper@42478: % %WN 
neuper@42478: % %WN axis 1: Algorithmic Knowledge (Programs)
neuper@42478: % %WN axis 2: Application-oriented Knowledge (Specifications)
neuper@42478: % %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
neuper@42478: % %WN 
neuper@42478: % %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
neuper@42478: % %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
neuper@42478: % %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
neuper@42478: % 
neuper@42478: % %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
neuper@42478: % %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
neuper@42478: % %JR gefordert werden WN2...
neuper@42478: % %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
neuper@42478: % %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
neuper@42478: % %WN2 zusammenschneiden um die R"ander weg zu bekommen)
neuper@42478: % %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
neuper@42478: % %WN2 png + pdf figures mitzuschicken.
neuper@42478: % 
neuper@42478: % \subsection{Notes on Problems with Traditional Notation}
neuper@42478: % 
neuper@42478: % \paragraph{During research} on these topic severely problems on
neuper@42478: % traditional notations have been discovered. Some of them have been
neuper@42478: % known in computer science for many years now and are still unsolved,
neuper@42478: % one of them aggregates with the so called \emph{Lambda Calculus},
neuper@42478: % Example~\ref{eg:lamda} provides a look on the problem that embarrassed
neuper@42478: % us.
neuper@42478: % 
neuper@42478: % \vbox{
neuper@42478: %   \begin{example}
neuper@42478: %     \label{eg:lamda}
neuper@42478: % 
neuper@42478: %   \[ f(x)=\ldots\;  \quad R \rightarrow \quad R \]
neuper@42478: % 
neuper@42478: % 
neuper@42478: %   \[ f(p)=\ldots\;  p \in \quad R \]
neuper@42478: % 
neuper@42478: %     {\small\textit{
neuper@42478: %       \noindent Above we see two equations. The first equation aims to
neuper@42478: % be a mapping of an function from the reel range to the reel one, but
neuper@42478: % when we change only one letter we get the second equation which
neuper@42478: % usually aims to insert a reel point $p$ into the reel function. In
neuper@42478: % computer science now we have the problem to tell the machine (TP) the
neuper@42478: % difference between this two notations. This Problem is called
neuper@42478: % \emph{Lambda Calculus}.
neuper@42478: %     }}
neuper@42478: %   \end{example}
neuper@42478: % }
neuper@42478: % 
neuper@42478: % \paragraph{An other problem} is that terms are not full simplified in
neuper@42478: % traditional notations, in {{\sisac}} we have to simplify them complete
neuper@42478: % to check weather results are compatible or not. in e.g. the solutions
neuper@42478: % of an second order linear equation is an rational in {{\sisac}} but in
neuper@42478: % tradition we keep fractions as long as possible and as long as they
neuper@42478: % aim to be \textit{beautiful} (1/8, 5/16,...).
neuper@42478: % \subparagraph{The math} which should be mechanized in Computer Theorem
neuper@42478: % Provers (\emph{TP}) has (almost) a problem with traditional notations
neuper@42478: % (predicate calculus) for axioms, definitions, lemmas, theorems as a
neuper@42478: % computer program or script is not able to interpret every Greek or
neuper@42478: % Latin letter and every Greek, Latin or whatever calculations
neuper@42478: % symbol. Also if we would be able to handle these symbols we still have
neuper@42478: % a problem to interpret them at all. (Follow up \hbox{Example
neuper@42478: % \ref{eg:symbint1}})
neuper@42478: % 
neuper@42478: % \vbox{
neuper@42478: %   \begin{example}
neuper@42478: %     \label{eg:symbint1}
neuper@42478: %     \[
neuper@42478: %       u\left[n\right] \ \ldots \ unitstep
neuper@42478: %     \]
neuper@42478: %     {\small\textit{
neuper@42478: %       \noindent The unitstep is something we need to solve Signal
neuper@42478: % Processing problem classes. But in {{{\sisac}{}}} the rectangular
neuper@42478: % brackets have a different meaning. So we abuse them for our
neuper@42478: % requirements. We get something which is not defined, but usable. The
neuper@42478: % Result is syntax only without semantic.
neuper@42478: %     }}
neuper@42478: %   \end{example}
neuper@42478: % }
neuper@42478: % 
neuper@42478: % In different problems, symbols and letters have different meanings and
neuper@42478: % ask for different ways to get through. (Follow up \hbox{Example
neuper@42478: % \ref{eg:symbint2}}) 
neuper@42478: % 
neuper@42478: % \vbox{
neuper@42478: %   \begin{example}
neuper@42478: %     \label{eg:symbint2}
neuper@42478: %     \[
neuper@42478: %       \widehat{\ }\ \widehat{\ }\ \widehat{\ } \  \ldots \  exponent
neuper@42478: %     \]
neuper@42478: %     {\small\textit{
neuper@42478: %     \noindent For using exponents the three \texttt{widehat} symbols
neuper@42478: % are required. The reason for that is due the development of
neuper@42478: % {{{\sisac}{}}} the single \texttt{widehat} and also the double were
neuper@42478: % already in use for different operations.
neuper@42478: %     }}
neuper@42478: %   \end{example}
neuper@42478: % }
neuper@42478: % 
neuper@42478: % \paragraph{Also the output} can be a problem. We are familiar with a
neuper@42478: % specified notations and style taught in university but a computer
neuper@42478: % program has no knowledge of the form proved by a professor and the
neuper@42478: % machines themselves also have not yet the possibilities to print every
neuper@42478: % symbol (correct) Recent developments provide proofs in a human
neuper@42478: % readable format but according to the fact that there is no money for
neuper@42478: % good working formal editors yet, the style is one thing we have to
neuper@42478: % live with.
neuper@42478: % 
neuper@42478: % \section{Problems rising out of the Development Environment}
neuper@42478: % 
neuper@42478: % fehlermeldungen! TODO
jan@42463: 
neuper@42464: \section{Conclusion}\label{conclusion}
jan@42463: 
jan@42463: TODO
jan@42463: 
jan@42463: \bibliographystyle{alpha}
jan@42463: \bibliography{references}
jan@42463: 
jan@42463: \end{document}



