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: neuper@42487: At the state-of-the-art in mechanization of knowledge in engineering neuper@42487: sciences, the process does not stop with the mechanization of neuper@42487: mathematics traditionally used in these sciences. Rather, ``Formal neuper@42487: Methods''~\cite{ fm-03} are expected to proceed to formal and explicit neuper@42487: description of physical items. Signal Processing, for instance is neuper@42487: concerned with physical devices for signal acquisition and neuper@42487: reconstruction, which involve measuring a physical signal, storing it, neuper@42487: and possibly later rebuilding the original signal or an approximation neuper@42487: thereof. For digital systems, this typically includes sampling and neuper@42487: quantization; devices for signal compression, including audio neuper@42487: compression, image compression, and video compression, etc. ``Domain neuper@42487: engineering''\cite{db:dom-eng} is concerned with {\em specification} neuper@42487: of these devices' components and features; this part in the process of neuper@42487: mechanization is only at the beginning in domains like Signal neuper@42487: Processing. jan@42466: neuper@42487: TP-based programming, concern of this paper, is determined to jan@42466: add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on jan@42466: p.\pageref{fig:mathuni}. As we shall see below, TP-based programming jan@42466: starts with a formal {\em specification} of the problem to be solved. neuper@42478: \begin{figure} neuper@42478: \begin{center} neuper@42483: \includegraphics[width=110mm]{fig/math-universe-small} neuper@42487: \caption{The three-dimensional universe of mathematics knowledge} neuper@42478: \label{fig:mathuni} neuper@42478: \end{center} neuper@42478: \end{figure} neuper@42487: The language for both axes is defined in the axis at the bottom, deductive neuper@42487: knowledge, in {\sisac} represented by Isabelle's theories. jan@42466: jan@42489: \subsection{Preparation of Simplifiers for the Program}\label{simp} jan@42489: jan@42489: \paragraph{If it is clear} how the later calculation should look like and when jan@42489: which mathematic rule should be applied, it can be started to find ways of jan@42489: simplifications. This includes in e.g. the simplification of reational jan@42489: expressions or also rewrites of an expession. jan@42489: \subparagraph{Obligate is the use} of the function \texttt{drop\_questionmarks} jan@42489: which excludes irrelevant symbols out of the expression. (Irrelevant symbols may jan@42489: be result out of the system during the calculation. The function has to be jan@42489: applied for two reasons. First two make every placeholder in a expression jan@42489: useable as a constant and second to provide a better view at the frontend.) jan@42489: \subparagraph{Most rewrites are represented} through rulesets this jan@42489: rulesets tell the machine which terms have to be rewritten into which jan@42489: representation. In the upcoming programm a rewrite can be applied only in using jan@42489: such rulesets on existing terms. jan@42489: \paragraph{The core} of our implemented problem is the Z-Transformation jan@42489: (remember the description of the running example, introduced by jan@42489: Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the jan@42489: transformation itself would require higher math which isn't yet avaible in our system we decided to choose the way like it is applied in labratory and problem classes at our university - by applying transformation rules (collected in jan@42489: transformation tables). jan@42489: \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the jan@42489: use of axiomatizations like shown in Example~\ref{eg:ruledef}. This rules can be jan@42489: collected in a ruleset (collection of rules) and applied to a given expression jan@42489: as follows in Example~\ref{eg:ruleapp}. jan@42489: jan@42489: \begin{example} jan@42489: \label{eg:ruledef} jan@42489: \hfill\\ jan@42489: \begin{verbatim} jan@42489: axiomatization where jan@42489: rule1: ``1 = $\delta$[n]'' and jan@42489: rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and jan@42489: rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]'' jan@42489: \end{verbatim} jan@42489: \end{example} jan@42489: jan@42489: \begin{example} jan@42489: \hfill\\ jan@42489: \label{eg:ruleapp} jan@42489: \begin{enumerate} jan@42489: \item Store rules in ruleset: jan@42489: \begin{verbatim} jan@42489: val inverse_Z = append_rls "inverse_Z" e_rls jan@42489: [ Thm ("rule1",num_str @{thm rule1}), jan@42489: Thm ("rule2",num_str @{thm rule2}), jan@42489: Thm ("rule3",num_str @{thm rule3}) jan@42489: ];\end{verbatim} jan@42489: \item Define exression: jan@42489: \begin{verbatim} jan@42489: val sample_term = str2term "z/(z-1)+z/(z-)+1";\end{verbatim} jan@42489: \item Apply ruleset: jan@42489: \begin{verbatim} jan@42489: val SOME (sample_term', asm) = jan@42489: rewrite_set_ thy true inverse_Z sample_term;\end{verbatim} jan@42489: \end{enumerate} jan@42489: \end{example} jan@42489: jan@42489: The use of rulesets makes it much easier to develop our designated applications, jan@42489: but the programmer has to be careful and patient. When applying rulesets jan@42489: two important issues have to be mentionend: jan@42489: \subparagraph{How often} the rules have to be applied? In case of jan@42489: transformations it is quite clear that we use them once but other fields jan@42489: reuqire to apply rules until a special condition is reached (e.g. jan@42489: a simplification is finished when there is nothing to be done left). jan@42489: \subparagraph{The order} in which rules are applied often takes a big effect jan@42489: and has to be evaluated for each purpose once again. jan@42489: \par jan@42489: In our special case of Signal Processing and the rules defined in jan@42489: Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all jan@42489: constants. After this step has been done it no mather which rule fit's next. 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: jan@42491: \subsection{Specification of the Problem}\label{spec} jan@42491: %WN <--> \chapter 7 der Thesis jan@42491: %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. jan@42491: jan@42491: The problem of the running example is textually described in jan@42491: Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em jan@42491: formal} specification of this problem, in traditional mathematical jan@42491: notation, could look like is this: jan@42491: jan@42491: %WN Hier brauchen wir die Spezifikation des 'running example' ... jan@42491: %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei jan@42491: %JR der post condition - die existiert für uns ja eigentlich nicht aka jan@42491: %JR haben sie bis jetzt nicht beachtet WN... jan@42491: %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren. jan@42491: %JR2 done jan@42491: jan@42491: \label{eg:neuper2} jan@42491: {\small\begin{tabbing} jan@42491: 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill jan@42491: \hfill \\ jan@42491: Specification:\\ jan@42491: \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\ jan@42491: \>precond \>: filterExpression continius on $\mathbb{R}$ \\ jan@42491: \>output \>: stepResponse $x[n]$ \\ jan@42491: \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}} jan@42491: jan@42491: \begin{remark} jan@42491: Defining the postcondition requires a high amount mathematical jan@42491: knowledge, the difficult part in our case is not to set up this condition jan@42491: nor it is more to define it in a way the interpreter is able to handle it. jan@42491: Due the fact that implementing that mechanisms is quite the same amount as jan@42491: creating the programm itself, it is not avaible in our prototype. jan@42491: \label{rm:postcond} jan@42491: \end{remark} jan@42491: jan@42491: \paragraph{The implementation} of the formal specification in the present jan@42491: prototype, still bar-bones without support for authoring: jan@42491: %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert: jan@42491: {\footnotesize\label{exp-spec} jan@42491: \begin{verbatim} jan@42491: 01 store_specification jan@42491: 02 (prepare_specification jan@42491: 03 ["Jan Rocnik"] jan@42491: 04 "pbl_SP_Ztrans_inv" jan@42491: 05 thy jan@42491: 06 ( ["Inverse", "Z_Transform", "SignalProcessing"], jan@42491: 07 [ ("#Given", ["filterExpression X_eq"]), jan@42491: 08 ("#Pre" , ["X_eq is_continuous"]), jan@42491: 19 ("#Find" , ["stepResponse n_eq"]), jan@42491: 10 ("#Post" , [" TODO "])], jan@42491: 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)], jan@42491: 12 NONE, jan@42491: 13 [["SignalProcessing","Z_Transform","Inverse"]])); jan@42491: \end{verbatim}} jan@42491: Although the above details are partly very technical, we explain them jan@42491: in order to document some intricacies of TP-based programming in the jan@42491: present state of the {\sisac} prototype: jan@42491: \begin{description} jan@42491: \item[01..02]\textit{store\_specification:} stores the result of the jan@42491: function \textit{prep\_specification} in a global reference jan@42491: \textit{Unsynchronized.ref}, which causes principal conflicts with jan@42491: Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and jan@42491: parallel execution~\cite{Makarius-09:parall-proof} and is under jan@42491: reconstruction already. jan@42491: jan@42491: \textit{prep\_pbt:} translates the specification to an internal format jan@42491: which allows efficient processing; see for instance line {\rm 07} jan@42491: below. jan@42491: \item[03..04] are the ``mathematics author'' holding the copy-rights jan@42491: and a unique identifier for the specification within {\sisac}, jan@42491: complare line {\rm 06}. jan@42491: \item[05] is the Isabelle \textit{theory} required to parse the jan@42491: specification in lines {\rm 07..10}. jan@42491: \item[06] is a key into the tree of all specifications as presented to jan@42491: the user (where some branches might be hidden by the dialog jan@42491: component). jan@42491: \item[07..10] are the specification with input, pre-condition, output jan@42491: and post-condition respectively; the post-condition is not handled in jan@42491: the prototype presently. (Follow up Remark~\ref{rm:postcond}) jan@42491: \item[11] creates a term rewriting system (abbreviated \textit{rls} in jan@42491: {\sisac}) which evaluates the pre-condition for the actual input data. jan@42491: Only if the evaluation yields \textit{True}, a program con be started. jan@42491: \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a jan@42491: problem associated to a function from Computer Algebra (like an jan@42491: equation solver) which is not the case here. jan@42491: \item[13] is the specific key into the tree of programs addressing a jan@42491: method which is able to find a solution which satiesfies the jan@42491: post-condition of the specification. jan@42491: \end{description} jan@42491: jan@42491: jan@42491: %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *" jan@42491: %WN ... jan@42491: % type pbt = jan@42491: % {guh : guh, (*unique within this isac-knowledge*) jan@42491: % mathauthors: string list, (*copyright*) jan@42491: % init : pblID, (*to start refinement with*) jan@42491: % thy : theory, (* which allows to compile that pbt jan@42491: % TODO: search generalized for subthy (ref.p.69*) jan@42491: % (*^^^ WN050912 NOT used during application of the problem, jan@42491: % because applied terms may be from 'subthy' as well as from super; jan@42491: % thus we take 'maxthy'; see match_ags !*) jan@42491: % cas : term option,(*'CAS-command'*) jan@42491: % prls : rls, (* for preds in where_*) jan@42491: % where_: term list, (* where - predicates*) jan@42491: % ppc : pat list, jan@42491: % (*this is the model-pattern; jan@42491: % it contains "#Given","#Where","#Find","#Relate"-patterns jan@42491: % for constraints on identifiers see "fun cpy_nam"*) jan@42491: % met : metID list}; (* methods solving the pbt*) jan@42491: % jan@42491: %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen jan@42491: %WN oben selbst geschrieben. jan@42491: jan@42491: jan@42491: jan@42491: jan@42491: %WN das w"urde ich in \sec\label{progr} verschieben und jan@42491: %WN das SubProblem partial fractions zum Erkl"aren verwenden. jan@42491: % Such a specification is checked before the execution of a program is jan@42491: % started, the same applies for sub-programs. In the following example jan@42491: % (Example~\ref{eg:subprob}) shows the call of such a subproblem: jan@42491: % jan@42491: % \vbox{ jan@42491: % \begin{example} jan@42491: % \label{eg:subprob} jan@42491: % \hfill \\ jan@42491: % {\ttfamily \begin{tabbing} jan@42491: % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\ jan@42491: % ``\>\>[linear,univariate,equation,test],'' \\ jan@42491: % ``\>\>[Test,solve\_linear])'' \\ jan@42491: % ``\>[BOOL equ, REAL z])'' \\ jan@42491: % \end{tabbing} jan@42491: % } jan@42491: % {\small\textit{ jan@42491: % \noindent If a program requires a result which has to be jan@42491: % calculated first we can use a subproblem to do so. In our specific jan@42491: % case we wanted to calculate the zeros of a fraction and used a jan@42491: % subproblem to calculate the zeros of the denominator polynom. jan@42491: % }} jan@42491: % \end{example} jan@42491: % } jan@42491: jan@42491: \subsection{Implementation of the Method}\label{meth} jan@42491: jan@42491: \paragraph{todo} jan@42491: jan@42491: \begin{example} jan@42491: \begin{verbatim} jan@42491: jan@42491: 01 store_met jan@42491: 02 (prep_met thy "met_SP_Ztrans_inv" [] e_metID jan@42491: 03 (["SignalProcessing", "Z_Transform", "Inverse"], jan@42491: 04 [("#Given" ,["filterExpression (X_eq::bool)"]), jan@42491: 05 ("#Find" ,["stepResponse (n_eq::bool)"])], jan@42491: 06 {rew_ord'="tless_true", jan@42491: 07 rls'= e_rls, jan@42491: 08 calc = [], jan@42491: 09 srls = e_rls, jan@42491: 10 prls = e_rls, jan@42491: 11 crls = e_rls, jan@42491: 12 errpats = [], jan@42491: 13 nrls = e_rls}, jan@42491: 14 "empty_script" jan@42491: 15 )); jan@42491: \end{verbatim} jan@42491: \end{example} jan@42491: neuper@42478: \subsection{Implementation of the TP-based Program}\label{progr} neuper@42480: So finally all the prerequisites are described and the very topic can neuper@42480: be addressed. The program below comes back to the running example: it neuper@42480: computes a solution for the problem from Fig.\ref{fig-interactive} on neuper@42480: p.\pageref{fig-interactive}. The reader is reminded of neuper@42480: \S\ref{PL-isab}, the introduction of the programming language: 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 - \) + 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-)+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}