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} } jan@42463: \noindent \textit{The running example's program uses some of these elements jan@42463: (marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt jan@42463: let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for jan@42463: lists and {\tt o} for functional (forward) composition in line jan@42463: $10$. In fact, the whole program is an Isabelle term with specific jan@42463: function constants like {\sc program}, {\sc Substitute} and {\sc jan@42463: Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.} jan@42463: jan@42463: % Terms may also contain $\lambda$-abstractions. For example, $\lambda jan@42463: % x. \; x$ is the identity function. jan@42463: neuper@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 jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: \item[Take:] ${\it term}\Rightarrow{\it term}$: jan@42463: this tactic has no effect in the program; but it creates a side-effect jan@42463: by Lucas-Interpretation (see below) and writes {\it term} to the jan@42463: Worksheet. jan@42463: jan@42463: \item[Subproblem:] ${\it theory} * {\it specification} * {\it jan@42463: method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$: jan@42463: this tactic allows to enter a phase of interactive specification jan@42463: of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance, jan@42463: a specific type of equation) and a method (for instance, solving an jan@42463: equation symbolically or numerically). jan@42463: jan@42463: \end{description} jan@42463: The tactics play a specific role in jan@42463: Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as jan@42463: break-points and control is handed over to the user. The user is free jan@42463: to investigate underlying knowledge, applicable theorems, etc. And jan@42463: the user can proceed constructing a solution by input of a tactic to jan@42463: be applied or by input of a formula; in the latter case the jan@42463: Lucas-Interpreter has built up a logical context (initialised with the jan@42463: precondition of the formal specification) such that Isabelle can jan@42463: derive the formula from this context --- or give feedback, that no jan@42463: derivation can be found. jan@42463: jan@42463: \subsection{Tacticals for Control of Interpretation} jan@42463: The flow of control in a program can be determined by {\tt if then else} jan@42463: and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also jan@42463: by additional tacticals: jan@42463: \begin{description} jan@42463: \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it jan@42463: term}$: iterates over tactics which take a {\it term} as argument as jan@42463: long as a tactic is applicable (for instance, {\it Rewrite\_Set} might jan@42463: not be applicable). jan@42463: jan@42463: \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$: jan@42463: if {\it tactic} is applicable, then it is applied to {\it term}, jan@42463: otherwise {\it term} is passed on unchanged. jan@42463: jan@42463: \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: jan@42463: \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: \end{description} jan@42463: jan@42463: no input / output --- Lucas-Interpretation jan@42463: jan@42463: .\\.\\.\\TODO\\.\\.\\ jan@42463: jan@42466: \section{Development of a Program on Trial}\label{trial} jan@42466: As mentioned above, {\sisac} is an experimental system for a proof of jan@42466: concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The jan@42466: latter interprets a specific kind of TP-based programming language, jan@42466: which is as experimental as the whole prototype --- so programming in jan@42466: this language can be only ``on trial'', presently. However, as a jan@42466: prototype, the language addresses essentials described below. jan@42466: jan@42466: \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac} jan@42466: neuper@42467: %WN was Fachleute unter obigem Titel interessiert findet sich jan@42466: %WN unterhalb des auskommentierten Textes. jan@42466: jan@42466: %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell jan@42466: %WN auf Computer-Mathematiker fokussiert. neuper@42464: % \paragraph{As mentioned in the introduction,} a prototype of an neuper@42464: % educational math assistant called neuper@42464: % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for neuper@42464: % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges neuper@42464: % the gap between (1) introducation and (2) application of mathematics: neuper@42464: % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which neuper@42464: % requires each fact and each action justified by formal logic, so neuper@42464: % {{{\sisac}{}}} makes justifications transparent to students in neuper@42464: % interactive step-wise problem solving. By that way {{\sisac}} already neuper@42464: % can serve both: neuper@42464: % \begin{enumerate} neuper@42464: % \item Introduction of math stuff (in e.g. partial fraction neuper@42464: % decomposition) by stepwise explaining and exercising respective neuper@42464: % symbolic calculations with ``next step guidance (NSG)'' and rigorously neuper@42464: % checking steps freely input by students --- this also in context with neuper@42464: % advanced applications (where the stuff to be taught in higher neuper@42464: % semesters can be skimmed through by NSG), and neuper@42464: % \item Application of math stuff in advanced engineering courses neuper@42464: % (e.g. problems to be solved by inverse Z-transform in a Signal neuper@42464: % Processing Lab) and now without much ado about basic math techniques neuper@42464: % (like partial fraction decomposition): ``next step guidance'' supports neuper@42464: % students in independently (re-)adopting such techniques. neuper@42464: % \end{enumerate} neuper@42464: % Before the question is answers, how {{\sisac}} neuper@42464: % accomplishes this task from a technical point of view, some remarks on neuper@42464: % the state-of-the-art is given, therefor follow up Section~\ref{emas}. neuper@42464: % neuper@42464: % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} neuper@42464: % jan@42466: % \paragraph{Educational software in mathematics} is, if at all, based jan@42466: % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry jan@42466: % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org} jan@42466: % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC jan@42466: % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These jan@42466: % base technologies are used to program math lessons and sometimes even jan@42466: % exercises. The latter are cumbersome: the steps towards a solution of jan@42466: % such an interactive exercise need to be provided with feedback, where jan@42466: % at each step a wide variety of possible input has to be foreseen by jan@42466: % the programmer - so such interactive exercises either require high neuper@42464: % development efforts or the exercises constrain possible inputs. neuper@42464: % jan@42466: % \subparagraph{A new generation} of educational math assistants (EMAs) jan@42466: % is emerging presently, which is based on Theorem Proving (TP). TP, for jan@42466: % instance Isabelle and Coq, is a technology which requires each fact jan@42466: % and each action justified by formal logic. Pushed by demands for jan@42466: % \textit{proven} correctness of safety-critical software TP advances jan@42466: % into software engineering; from these advancements computer jan@42466: % mathematics benefits in general, and math education in particular. Two neuper@42464: % features of TP are immediately beneficial for learning: neuper@42464: % jan@42466: % \paragraph{TP have knowledge in human readable format,} that is in jan@42466: % standard predicate calculus. TP following the LCF-tradition have that jan@42466: % knowledge down to the basic definitions of set, equality, jan@42466: % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; jan@42466: % following the typical deductive development of math, natural numbers jan@42466: % are defined and their properties jan@42466: % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, jan@42466: % etc. Present knowledge mechanized in TP exceeds high-school jan@42466: % mathematics by far, however by knowledge required in software neuper@42464: % technology, and not in other engineering sciences. neuper@42464: % jan@42466: % \paragraph{TP can model the whole problem solving process} in jan@42466: % mathematical problem solving {\em within} a coherent logical jan@42466: % framework. This is already being done by three projects, by neuper@42464: % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor. neuper@42464: % \par jan@42466: % Having the whole problem solving process within a logical coherent jan@42466: % system, such a design guarantees correctness of intermediate steps and jan@42466: % of the result (which seems essential for math software); and the jan@42466: % second advantage is that TP provides a wealth of theories which can be jan@42466: % exploited for mechanizing other features essential for educational neuper@42464: % software. neuper@42464: % neuper@42464: % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid} neuper@42464: % jan@42466: % One essential feature for educational software is feedback to user neuper@42464: % input and assistance in coming to a solution. neuper@42464: % jan@42466: % \paragraph{Checking user input} by ATP during stepwise problem solving jan@42466: % is being accomplished by the three projects mentioned above jan@42466: % exclusively. They model the whole problem solving process as mentioned jan@42466: % above, so all what happens between formalized assumptions (or formal jan@42466: % specification) and goal (or fulfilled postcondition) can be jan@42466: % mechanized. Such mechanization promises to greatly extend the scope of neuper@42464: % educational software in stepwise problem solving. neuper@42464: % jan@42466: % \paragraph{NSG (Next step guidance)} comprises the system's ability to jan@42466: % propose a next step; this is a challenge for TP: either a radical jan@42466: % restriction of the search space by restriction to very specific jan@42466: % problem classes is required, or much care and effort is required in jan@42466: % designing possible variants in the process of problem solving neuper@42464: % \cite{proof-strategies-11}. neuper@42464: % \par jan@42466: % Another approach is restricted to problem solving in engineering jan@42466: % domains, where a problem is specified by input, precondition, output jan@42466: % and postcondition, and where the postcondition is proven by ATP behind jan@42466: % the scenes: Here the possible variants in the process of problem jan@42466: % solving are provided with feedback {\em automatically}, if the problem jan@42466: % is described in a TP-based programing language: \cite{plmms10} the jan@42466: % programmer only describes the math algorithm without caring about jan@42466: % interaction (the respective program is functional and even has no jan@42466: % input or output statements!); interaction is generated as a jan@42466: % side-effect by the interpreter --- an efficient separation of concern jan@42466: % between math programmers and dialog designers promising application neuper@42464: % all over engineering disciplines. neuper@42464: % neuper@42464: % neuper@42464: % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}} jan@42466: % Authoring new mathematics knowledge in {{\sisac}} can be compared with jan@42466: % ``application programing'' of engineering problems; most of such jan@42466: % programing uses CAS-based programing languages (CAS = Computer Algebra neuper@42464: % Systems; e.g. Mathematica's or Maple's programing language). neuper@42464: % jan@42466: % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}} jan@42466: % \cite{plmms10} for describing how to construct a solution to an jan@42466: % engineering problem and for calling equation solvers, integration, jan@42466: % etc~\footnote{Implementation of CAS-like functionality in TP is not jan@42466: % primarily concerned with efficiency, but with a didactic question: jan@42466: % What to decide for: for high-brow algorithms at the state-of-the-art jan@42466: % or for elementary algorithms comprehensible for students?} within TP; jan@42466: % TP can ensure ``systems that never make a mistake'' \cite{casproto} - neuper@42464: % are impossible for CAS which have no logics underlying. neuper@42464: % jan@42466: % \subparagraph{Authoring is perfect} by writing such TP based programs; jan@42466: % the application programmer is not concerned with interaction or with jan@42466: % user guidance: this is concern of a novel kind of program interpreter jan@42466: % called Lucas-Interpreter. This interpreter hands over control to a jan@42466: % dialog component at each step of calculation (like a debugger at jan@42466: % breakpoints) and calls automated TP to check user input following neuper@42464: % personalized strategies according to a feedback module. neuper@42464: % \par jan@42466: % However ``application programing with TP'' is not done with writing a jan@42466: % program: according to the principles of TP, each step must be jan@42466: % justified. Such justifications are given by theorems. So all steps jan@42466: % must be related to some theorem, if there is no such theorem it must jan@42466: % be added to the existing knowledge, which is organized in so-called jan@42466: % \textbf{theories} in Isabelle. A theorem must be proven; fortunately jan@42466: % Isabelle comprises a mechanism (called ``axiomatization''), which jan@42466: % allows to omit proofs. Such a theorem is shown in neuper@42464: % Example~\ref{eg:neuper1}. jan@42466: jan@42466: The running example, introduced by Fig.\ref{fig-interactive} on jan@42466: p.\pageref{fig-interactive}, requires to determine the inverse $\cal jan@42466: Z$-transform for a class of functions. The domain of Signal Processing jan@42466: is accustomed to specific notation for the resulting functions, which jan@42466: are absolutely summable and are called TODO: $u[n]$, where $u$ is the jan@42466: function, $n$ is the argument and the brackets indicate that the jan@42466: arguments are TODO. Surprisingly, Isabelle accepts the rules for jan@42466: ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle jan@42466: experts might be particularly surprised, that the brackets do not jan@42466: cause errors in typing (as lists).}: neuper@42464: %\vbox{ neuper@42464: % \begin{example} jan@42463: \label{eg:neuper1} jan@42463: {\small\begin{tabbing} jan@42463: 123\=123\=123\=123\=\kill jan@42463: \hfill \\ jan@42463: \>axiomatization where \\ neuper@42464: \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\ neuper@42464: \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\ jan@42466: \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\ jan@42466: %TODO jan@42466: \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\ jan@42466: %TODO jan@42466: \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\ jan@42466: %TODO jan@42466: \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\ jan@42466: %TODO jan@42463: \end{tabbing} jan@42463: } neuper@42464: % \end{example} jan@42466: %} jan@42466: These 6 rules can be used as conditional rewrite rules, depending on jan@42466: the respective convergence radius. Satisfaction from accordance with traditional notation jan@42466: contrasts with the above word {\em axiomatization}: As TP-based, the jan@42466: programming language expects these rules as {\em proved} theorems, and jan@42466: not as axioms implemented in the above brute force manner; otherwise jan@42466: all the verification efforts envisaged (like proof of the jan@42466: post-condition, see below) would be meaningless. jan@42466: jan@42466: Isabelle provides a large body of knowledge, rigorously proven from jan@42466: the basic axioms of mathematics~\footnote{This way of rigorously jan@42466: deriving all knowledge from first principles is called the jan@42466: LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced jan@42466: knowledge can be found in the theoris on Multivariate jan@42466: Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However, jan@42466: building up knowledge such that a proof for the above rules would be jan@42466: reasonably short and easily comprehensible, still requires lots of jan@42466: work (and is definitely out of scope of our case study). jan@42466: jan@42466: \paragraph{At the state-of-the-art in mechanization of knowledge} in jan@42466: engineering sciences, the process does not stop with the mechanization of jan@42466: mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods} jan@42466: are expected to proceed to formal and explicit description of physical items. Signal Processing, jan@42466: for instance is concerned with physical devices for signal acquisition jan@42466: and reconstruction, which involve measuring a physical signal, storing jan@42466: it, and possibly later rebuilding the original signal or an jan@42466: approximation thereof. For digital systems, this typically includes jan@42466: sampling and quantization; devices for signal compression, including jan@42466: audio compression, image compression, and video compression, etc. jan@42466: ``Domain engineering''\cite{db-domain-engineering} is concerned with jan@42466: {\em specification} of these devices' components and features; this jan@42466: part in the process of mechanization is only at the beginning in domains jan@42466: like Signal Processing. jan@42466: jan@42466: \subparagraph{TP-based programming, concern of this paper,} is determined to jan@42466: add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on jan@42466: p.\pageref{fig:mathuni}. As we shall see below, TP-based programming jan@42466: starts with a formal {\em specification} of the problem to be solved. jan@42466: jan@42466: jan@42466: \subsection{Specification of the Problem}\label{spec} jan@42466: %WN <--> \chapter 7 der Thesis jan@42466: %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. jan@42466: jan@42466: The problem of the running example is textually described in jan@42466: Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em jan@42466: formal} specification of this problem, in traditional mathematical jan@42469: notation, could look like is this: jan@42466: jan@42466: %WN Hier brauchen wir die Spezifikation des 'running example' ... jan@42466: jan@42466: %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei jan@42466: %JR der post condition - die existiert für uns ja eigentlich nicht aka neuper@42467: %JR haben sie bis jetzt nicht beachtet WN... neuper@42467: %WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren. jan@42466: jan@42463: \label{eg:neuper2} jan@42463: {\small\begin{tabbing} jan@42463: 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill jan@42463: \hfill \\ neuper@42465: Specification:\\ jan@42466: \>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\ jan@42466: \>precond \>: filterExpression continius on $\mathbb{R}$ \\ jan@42466: \>output \>: stepResponse $x[n]$ \\ jan@42469: \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}} jan@42466: jan@42469: \paragraph{Remark on post-conditions:} Defining the postcondition requires a jan@42469: high amount mathematical knowledge, the difficult part in our case is not to jan@42469: set up this condition nor it is more to define it in a way the interpreter is jan@42469: able to handle it. Due the fact that implementing that mechanisms is quite jan@42469: the same amount as creating the programm itself, it is not avaible in our jan@42469: prototype.\label{rm:postcond} jan@42469: jan@42469: \paragraph{The implementation} of the formal specification in the present jan@42466: prototype, still bar-bones without support for authoring: jan@42466: %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert: jan@42466: {\footnotesize jan@42466: \begin{verbatim} jan@42466: 01 store_specification jan@42466: 02 (prepare_specification jan@42466: 03 ["Jan Rocnik"] jan@42466: 04 "pbl_SP_Ztrans_inv" jan@42466: 05 thy jan@42466: 06 ( ["Inverse", "Z_Transform", "SignalProcessing"], jan@42466: 07 [ ("#Given", ["filterExpression X_eq"]), jan@42466: 08 ("#Pre" , ["X_eq is_continuous"]), jan@42466: 19 ("#Find" , ["stepResponse n_eq"]), jan@42466: 10 ("#Post" , [" TODO "])], jan@42466: 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)], jan@42466: 12 NONE, jan@42466: 13 [["SignalProcessing","Z_Transform","Inverse"]])); jan@42466: \end{verbatim}} jan@42466: Although the above details are partly very technical, we explain them jan@42466: in order to document some intricacies of TP-based programming in the jan@42466: present state of the {\sisac} prototype: jan@42466: \begin{description} jan@42466: \item[01..02]\textit{store\_specification:} stores the result of the jan@42466: function \textit{prep\_specification} in a global reference jan@42466: \textit{Unsynchronized.ref}, which causes principal conflicts with jan@42466: Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and jan@42466: parallel execution~\cite{Makarius-09:parall-proof} and is under jan@42466: reconstruction already. jan@42466: jan@42466: \textit{prep\_pbt:} translates the specification to an internal format jan@42466: which allows efficient processing; see for instance line {\rm 07} jan@42466: below. jan@42466: \item[03..04] are the ``mathematics author'' holding the copy-rights jan@42466: and a unique identifier for the specification within {\sisac}, jan@42466: complare line {\rm 06}. jan@42466: \item[05] is the Isabelle \textit{theory} required to parse the jan@42466: specification in lines {\rm 07..10}. jan@42466: \item[06] is a key into the tree of all specifications as presented to jan@42466: the user (where some branches might be hidden by the dialog jan@42466: component). jan@42466: \item[07..10] are the specification with input, pre-condition, output jan@42466: and post-condition respectively; the post-condition is not handled in jan@42469: the prototype presently. (Follow up Remark in Section~\ref{rm:postcond}) jan@42466: \item[11] creates a term rewriting system (abbreviated \textit{rls} in jan@42466: {\sisac}) which evaluates the pre-condition for the actual input data. jan@42466: Only if the evaluation yields \textit{True}, a program con be started. jan@42466: \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a jan@42466: problem associated to a function from Computer Algebra (like an jan@42466: equation solver) which is not the case here. jan@42466: \item[13] is the specific key into the tree of programs addressing a jan@42466: method which is able to find a solution which satiesfies the jan@42466: post-condition of the specification. jan@42466: \end{description} jan@42466: jan@42466: jan@42466: %WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *" jan@42466: %WN ... jan@42466: % type pbt = jan@42466: % {guh : guh, (*unique within this isac-knowledge*) jan@42466: % mathauthors: string list, (*copyright*) jan@42466: % init : pblID, (*to start refinement with*) jan@42466: % thy : theory, (* which allows to compile that pbt jan@42466: % TODO: search generalized for subthy (ref.p.69*) jan@42466: % (*^^^ WN050912 NOT used during application of the problem, jan@42466: % because applied terms may be from 'subthy' as well as from super; jan@42466: % thus we take 'maxthy'; see match_ags !*) jan@42466: % cas : term option,(*'CAS-command'*) jan@42466: % prls : rls, (* for preds in where_*) jan@42466: % where_: term list, (* where - predicates*) jan@42466: % ppc : pat list, jan@42466: % (*this is the model-pattern; jan@42466: % it contains "#Given","#Where","#Find","#Relate"-patterns jan@42466: % for constraints on identifiers see "fun cpy_nam"*) jan@42466: % met : metID list}; (* methods solving the pbt*) jan@42466: % jan@42466: %WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen jan@42466: %WN oben selbst geschrieben. jan@42466: jan@42466: jan@42466: jan@42466: jan@42466: %WN das w"urde ich in \sec\label{progr} verschieben und jan@42466: %WN das SubProblem partial fractions zum Erkl"aren verwenden. jan@42466: % Such a specification is checked before the execution of a program is jan@42466: % started, the same applies for sub-programs. In the following example neuper@42465: % (Example~\ref{eg:subprob}) shows the call of such a subproblem: neuper@42465: % neuper@42465: % \vbox{ neuper@42465: % \begin{example} neuper@42465: % \label{eg:subprob} neuper@42465: % \hfill \\ neuper@42465: % {\ttfamily \begin{tabbing} neuper@42465: % ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\ neuper@42465: % ``\>\>[linear,univariate,equation,test],'' \\ neuper@42465: % ``\>\>[Test,solve\_linear])'' \\ neuper@42465: % ``\>[BOOL equ, REAL z])'' \\ neuper@42465: % \end{tabbing} neuper@42465: % } neuper@42465: % {\small\textit{ jan@42466: % \noindent If a program requires a result which has to be jan@42466: % calculated first we can use a subproblem to do so. In our specific jan@42466: % case we wanted to calculate the zeros of a fraction and used a neuper@42465: % subproblem to calculate the zeros of the denominator polynom. neuper@42465: % }} neuper@42465: % \end{example} neuper@42465: % } jan@42466: jan@42466: \subsection{Implementation of the Method}\label{meth} jan@42466: %WN <--> \chapter 7 der Thesis jan@42466: TODO jan@42466: \subsection{Preparation of Simplifiers for the Program}\label{simp} jan@42469: jan@42469: %JR: ich denke wir können diesen punkt weglassen, methoden wie jan@42469: %JR: drop_questionmarks und ähnliche sind im arical nicht ersichtlich und im jan@42469: %JR: grunde nicht relevant (ihre erstellung gleich wie functionen im nächsten jan@42469: %JR: Punkt) 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@42469: to filter the deonimonator 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@42469: By taking \texttt{get\_denominator} we want to explain how to implement new jan@42469: functions into the existing system and how we can later use them in our program. jan@42469: jan@42469: \subsubsection{Find a place to Store the Function} jan@42469: The whole system builds up on a well defined structure of Knowledge. This jan@42469: Knowledge sets up at\ttfamily src/Tools/isac/Knowledge\normalfont. For the jan@42469: implementation of the Function \texttt{get\_denominator}, which let us now jan@42469: the denominator 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@42469: jan@42469: \begin{example} jan@42469: \begin{verbatim} jan@42469: jan@42469: ML {* jan@42469: (* jan@42469: *("get_denominator", jan@42469: * ("Rational.get_denominator", eval_get_denominator "")) jan@42469: *) jan@42469: fun eval_get_denominator (thmid:string) _ jan@42469: (t as Const ("Rational.get_denominator", _) $ jan@42469: (Const ("Rings.inverse_class.divide", _) $num jan@42469: $denom)) thy = jan@42469: SOME (mk_thmid thmid "" jan@42469: (Print_Mode.setmp [] jan@42469: (Syntax.string_of_term (thy2ctxt thy)) denom) "", jan@42469: Trueprop $ (mk_equality (t, denom))) jan@42469: | eval_get_denominator _ _ _ _ = NONE; jan@42469: *}\end{verbatim} jan@42469: \end{example} jan@42469: jan@42469: jan@42469: \subsubsection{Add a test for the new Function} jan@42469: \subsubsection{Use the new Function} jan@42469: jan@42469: jan@42469: jan@42466: \subsection{Implementation of the TP-based Program}\label{progr} jan@42466: %WN <--> \chapter 8 der Thesis neuper@42467: .\\.\\.\\ neuper@42467: neuper@42467: {\small\it\begin{tabbing} neuper@42467: 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill neuper@42467: \>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\ neuper@42467: \>{\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@42468: \>{\rm 08}\>\>\>\>\>\>\>\> ( \> Isac, \\ neuper@42468: \>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction, rational, simplification]\\ neuper@42467: \>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\ neuper@42468: \>{\rm 10}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\ neuper@42468: \>{\rm 12}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\ neuper@42467: neuper@42468: \>{\rm 12}\>\>\> X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ; \\ neuper@42468: \>{\rm 15}\>\>\> X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\ neuper@42467: \>{\rm 16}\>\> {\tt IN } \\ neuper@42468: \>{\rm 15}\>\>\> X'\_eq neuper@42467: \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@42467: neuper@42467: neuper@42467: .\\.\\.\\ jan@42466: jan@42463: \section{Workflow of Programming in the Prototype}\label{workflow} neuper@42468: jan@42466: \subsection{Preparations and Trials}\label{flow-prep} neuper@42468: TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions'' 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@42468: neuper@42468: neuper@42468: \newpage neuper@42468: ------------------------------------------------------------------- neuper@42468: neuper@42468: Material, falls noch Platz bleibt ... neuper@42468: neuper@42468: ------------------------------------------------------------------- neuper@42468: neuper@42468: jan@42466: \subsubsection{Trials on Notation and Termination} jan@42466: jan@42466: \paragraph{Technical notations} are a big problem for our piece of software, jan@42466: but the reason for that isn't a fault of the software itself, one of the jan@42466: troubles comes out of the fact that different technical subtopics use different jan@42466: symbols and notations for a different purpose. The most famous example for such jan@42466: a symbol is the complex number $i$ (in cassique math) or $j$ (in technical jan@42466: math). In the specific part of signal processing one of this notation issues is jan@42466: the use of brackets --- we use round brackets for analoge signals and squared jan@42466: brackets for digital samples. Also if there is no problem for us to handle this jan@42466: fact, we have to tell the machine what notation leads to wich meaning and that jan@42466: this purpose seperation is only valid for this special topic - signal jan@42466: processing. jan@42466: \subparagraph{In the programming language} itself it is not possible to declare jan@42466: fractions, exponents, absolutes and other operators or remarks in a way to make jan@42466: them pretty to read; our only posssiblilty were ASCII characters and a handfull jan@42466: greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$. jan@42466: \par jan@42466: With the upper collected knowledge it is possible to check if we were able to jan@42466: donate all required terms and expressions. jan@42466: jan@42466: \subsubsection{Definition and Usage of Rules} jan@42466: jan@42466: \paragraph{The core} of our implemented problem is the Z-Transformation, due jan@42466: the fact that the transformation itself would require higher math which isn't jan@42466: yet avaible in our system we decided to choose the way like it is applied in jan@42466: labratory and problem classes at our university - by applying transformation jan@42466: rules (collected in transformation tables). jan@42466: \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the jan@42466: use of axiomatizations like shown in Example~\ref{eg:ruledef} jan@42466: jan@42466: \begin{example} jan@42466: \label{eg:ruledef} jan@42466: \hfill\\ jan@42466: \begin{verbatim} jan@42466: axiomatization where jan@42466: rule1: ``1 = $\delta$[n]'' and jan@42466: rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and jan@42466: rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]'' jan@42466: \end{verbatim} jan@42466: \end{example} jan@42466: jan@42466: This rules can be collected in a ruleset and applied to a given expression as jan@42466: follows in Example~\ref{eg:ruleapp}. jan@42466: jan@42466: \begin{example} jan@42466: \hfill\\ jan@42466: \label{eg:ruleapp} jan@42466: \begin{enumerate} jan@42466: \item Store rules in ruleset: jan@42466: \begin{verbatim} jan@42466: val inverse_Z = append_rls "inverse_Z" e_rls jan@42466: [ Thm ("rule1",num_str @{thm rule1}), jan@42466: Thm ("rule2",num_str @{thm rule2}), jan@42466: Thm ("rule3",num_str @{thm rule3}) jan@42466: ];\end{verbatim} jan@42466: \item Define exression: jan@42466: \begin{verbatim} jan@42466: val sample_term = str2term "z/(z-1)+z/(z-)+1";\end{verbatim} jan@42466: \item Apply ruleset: jan@42466: \begin{verbatim} jan@42466: val SOME (sample_term', asm) = jan@42466: rewrite_set_ thy true inverse_Z sample_term;\end{verbatim} jan@42466: \end{enumerate} jan@42466: \end{example} jan@42466: jan@42466: The use of rulesets makes it much easier to develop our designated applications, jan@42466: but the programmer has to be careful and patient. When applying rulesets jan@42466: two important issues have to be mentionend: jan@42466: \subparagraph{How often} the rules have to be applied? In case of jan@42466: transformations it is quite clear that we use them once but other fields jan@42466: reuqire to apply rules until a special condition is reached (e.g. jan@42466: a simplification is finished when there is nothing to be done left). jan@42466: \subparagraph{The order} in which rules are applied often takes a big effect jan@42466: and has to be evaluated for each purpose once again. jan@42466: \par jan@42466: In our special case of Signal Processing and the rules defined in jan@42466: Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all jan@42466: constants. After this step has been done it no mather which rule fit's next. jan@42466: jan@42466: \subsubsection{Helping Functions} jan@42469: jan@42469: \paragraph{New Programms require,} often new ways to get through. This new ways jan@42469: means that we handle functions that have not been in use yet, they can be jan@42469: something special and unique for a programm or something famous but unneeded in jan@42469: the system yet. In our dedicated example it was for example neccessary to split jan@42469: a fraction into numerator and denominator; the creation of such function and jan@42469: even others is described in upper Sections~\ref{simp} and \ref{funs}. jan@42469: jan@42466: \subsubsection{Trials on equation solving} jan@42466: %simple eq and problem with double fractions/negative exponents jan@42469: \paragraph{The Inverse Z-Transformation} makes it neccessary to solve jan@42469: equations degree one and two. Solving equations in the first degree is no jan@42469: problem, wether for a student nor for our machine; but even second degree jan@42469: equations can lead to big troubles. The origin of this troubles leads from jan@42469: the build up process of our equation solving functions; they have been jan@42469: implemented some time ago and of course they are not as good as we want them to jan@42469: be. Wether or not following we only want to show how cruel it is to build up new jan@42469: work on not well fundamentials. jan@42469: \subparagraph{A simple equation solving,} can be set up as shown in the next jan@42469: example: jan@42466: jan@42469: \begin{example} jan@42469: \begin{verbatim} jan@42469: jan@42469: val fmz = jan@42469: ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))", jan@42469: "solveFor z", jan@42469: "solutions L"]; jan@42466: jan@42469: val (dI',pI',mI') = jan@42469: ("Isac", jan@42469: ["abcFormula","degree_2","polynomial","univariate","equation"], jan@42469: ["no_met"]);\end{verbatim} jan@42469: \end{example} jan@42469: jan@42469: Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give jan@42469: a short overview on the commands; at first we set up the equation and tell the jan@42469: machine what's the bound variable and where to store the solution. Second step jan@42469: is to define the equation type and determine if we want to use a special method jan@42469: to solve this type.) Simple checks tell us that the we will get two results for jan@42469: this equation and this results will be real. jan@42469: So far it is easy for us and for our machine to solve, but jan@42469: mentioned that a unvariate equation second order can have three different types jan@42469: of solutions it is getting worth. jan@42469: \subparagraph{The solving of} all this types of solutions is not yet supported. jan@42469: Luckily it was needed for us; but something which has been needed in this jan@42469: context, would have been the solving of an euation looking like: jan@42469: $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned jan@42469: before (remember that befor it was no problem to handle for the machine) but jan@42469: now, after a simple equivalent transformation, we are not able to solve jan@42469: it anymore. jan@42469: \subparagraph{Error messages} we get when we try to solve something like upside jan@42469: were very confusing and also leads us to no special hint about a problem. jan@42469: \par The fault behind is, that we have no well error handling on one side and jan@42469: no sufficient formed equation solving on the other side. This two facts are jan@42469: making the implemention of new material very difficult. jan@42466: jan@42463: \subsection{Formalization of missing knowledge in Isabelle} jan@42463: jan@42466: \paragraph{A problem} behind is the mechanization of mathematic jan@42466: theories in TP-bases languages. There is still a huge gap between jan@42466: these algorithms and this what we want as a solution - in Example neuper@42464: Signal Processing. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:gap} jan@42463: \[ jan@42463: X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY jan@42463: \] jan@42463: {\small\textit{ jan@42466: \noindent A very simple example on this what we call gap is the jan@42466: simplification above. It is needles to say that it is correct and also jan@42466: Isabelle for fills it correct - \emph{always}. But sometimes we don't jan@42466: want expand such terms, sometimes we want another structure of jan@42466: them. Think of a problem were we now would need only the coefficients jan@42466: of $X$ and $Y$. This is what we call the gap between mechanical neuper@42464: simplification and the solution. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42466: \paragraph{We are not able to fill this gap,} until we have to live jan@42466: with it but first have a look on the meaning of this statement: jan@42466: Mechanized math starts from mathematical models and \emph{hopefully} jan@42466: proceeds to match physics. Academic engineering starts from physics jan@42466: (experimentation, measurement) and then proceeds to mathematical jan@42466: modeling and formalization. The process from a physical observance to jan@42466: a mathematical theory is unavoidable bound of setting up a big jan@42466: collection of standards, rules, definition but also exceptions. These neuper@42464: are the things making mechanization that difficult. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:units} jan@42463: \[ jan@42463: m,\ kg,\ s,\ldots jan@42463: \] jan@42463: {\small\textit{ jan@42466: \noindent Think about some units like that one's above. Behind jan@42466: each unit there is a discerning and very accurate definition: One jan@42466: Meter is the distance the light travels, in a vacuum, through the time jan@42466: of 1 / 299.792.458 second; one kilogram is the weight of a jan@42466: platinum-iridium cylinder in paris; and so on. But are these neuper@42464: definitions usable in a computer mechanized world?! jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42466: \paragraph{A computer} or a TP-System builds on programs with jan@42466: predefined logical rules and does not know any mathematical trick jan@42466: (follow up example \ref{eg:trick}) or recipe to walk around difficult neuper@42464: expressions. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:trick} jan@42463: \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] jan@42463: \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= jan@42463: \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] jan@42463: \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] jan@42463: {\small\textit{ jan@42466: \noindent Sometimes it is also useful to be able to apply some jan@42466: \emph{tricks} to get a beautiful and particularly meaningful result, jan@42466: which we are able to interpret. But as seen in this example it can be jan@42466: hard to find out what operations have to be done to transform a result neuper@42464: into a meaningful one. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42466: \paragraph{The only possibility,} for such a system, is to work jan@42466: through its known definitions and stops if none of these jan@42466: fits. Specified on Signal Processing or any other application it is jan@42466: often possible to walk through by doing simple creases. This creases jan@42466: are in general based on simple math operational but the challenge is jan@42466: to teach the machine \emph{all}\footnote{Its pride to call it jan@42466: \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to jan@42466: reach a high level of \emph{all} but it in real it will still be a jan@42466: survey of knowledge which links to other knowledge and {{\sisac}{}} a neuper@42464: trainer and helper but no human compensating calculator. jan@42463: \par jan@42466: {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal jan@42466: specifications of problems out of topics from Signal Processing, etc.) jan@42466: and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of jan@42466: physical knowledge. The result is a three-dimensional universe of neuper@42464: mathematics seen in Figure~\ref{fig:mathuni}. jan@42463: jan@42466: \begin{figure} jan@42466: \begin{center} jan@42466: \includegraphics{fig/universe} jan@42466: \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is jan@42466: combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result jan@42466: leads to a three dimensional math universe.\label{fig:mathuni}} jan@42466: \end{center} jan@42466: \end{figure} jan@42466: jan@42466: %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen; jan@42466: %WN bitte folgende Bezeichnungen nehmen: jan@42466: %WN jan@42466: %WN axis 1: Algorithmic Knowledge (Programs) jan@42466: %WN axis 2: Application-oriented Knowledge (Specifications) jan@42466: %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems) jan@42466: %WN jan@42466: %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf jan@42466: %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz jan@42466: %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken) jan@42466: jan@42466: %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's jan@42466: %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's neuper@42467: %JR gefordert werden WN2... neuper@42467: %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann neuper@42467: %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse neuper@42467: %WN2 zusammenschneiden um die R"ander weg zu bekommen) neuper@42467: %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und neuper@42467: %WN2 png + pdf figures mitzuschicken. jan@42463: jan@42463: \subsection{Notes on Problems with Traditional Notation} jan@42463: jan@42466: \paragraph{During research} on these topic severely problems on jan@42466: traditional notations have been discovered. Some of them have been jan@42466: known in computer science for many years now and are still unsolved, jan@42466: one of them aggregates with the so called \emph{Lambda Calculus}, jan@42466: Example~\ref{eg:lamda} provides a look on the problem that embarrassed neuper@42464: us. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:lamda} jan@42463: jan@42463: \[ f(x)=\ldots\; \quad R \rightarrow \quad R \] jan@42463: jan@42463: jan@42463: \[ f(p)=\ldots\; p \in \quad R \] jan@42463: jan@42463: {\small\textit{ jan@42466: \noindent Above we see two equations. The first equation aims to jan@42466: be a mapping of an function from the reel range to the reel one, but jan@42466: when we change only one letter we get the second equation which jan@42466: usually aims to insert a reel point $p$ into the reel function. In jan@42466: computer science now we have the problem to tell the machine (TP) the jan@42466: difference between this two notations. This Problem is called neuper@42464: \emph{Lambda Calculus}. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42466: \paragraph{An other problem} is that terms are not full simplified in jan@42466: traditional notations, in {{\sisac}} we have to simplify them complete jan@42466: to check weather results are compatible or not. in e.g. the solutions jan@42466: of an second order linear equation is an rational in {{\sisac}} but in jan@42466: tradition we keep fractions as long as possible and as long as they neuper@42464: aim to be \textit{beautiful} (1/8, 5/16,...). jan@42466: \subparagraph{The math} which should be mechanized in Computer Theorem jan@42466: Provers (\emph{TP}) has (almost) a problem with traditional notations jan@42466: (predicate calculus) for axioms, definitions, lemmas, theorems as a jan@42466: computer program or script is not able to interpret every Greek or jan@42466: Latin letter and every Greek, Latin or whatever calculations jan@42466: symbol. Also if we would be able to handle these symbols we still have jan@42466: a problem to interpret them at all. (Follow up \hbox{Example neuper@42464: \ref{eg:symbint1}}) jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:symbint1} jan@42463: \[ jan@42463: u\left[n\right] \ \ldots \ unitstep jan@42463: \] jan@42463: {\small\textit{ jan@42466: \noindent The unitstep is something we need to solve Signal jan@42466: Processing problem classes. But in {{{\sisac}{}}} the rectangular jan@42466: brackets have a different meaning. So we abuse them for our jan@42466: requirements. We get something which is not defined, but usable. The neuper@42464: Result is syntax only without semantic. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42466: In different problems, symbols and letters have different meanings and jan@42466: ask for different ways to get through. (Follow up \hbox{Example neuper@42464: \ref{eg:symbint2}}) jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:symbint2} jan@42463: \[ jan@42463: \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent jan@42463: \] jan@42463: {\small\textit{ jan@42466: \noindent For using exponents the three \texttt{widehat} symbols jan@42466: are required. The reason for that is due the development of jan@42466: {{{\sisac}{}}} the single \texttt{widehat} and also the double were neuper@42464: already in use for different operations. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42466: \paragraph{Also the output} can be a problem. We are familiar with a jan@42466: specified notations and style taught in university but a computer jan@42466: program has no knowledge of the form proved by a professor and the jan@42466: machines themselves also have not yet the possibilities to print every jan@42466: symbol (correct) Recent developments provide proofs in a human jan@42466: readable format but according to the fact that there is no money for jan@42466: good working formal editors yet, the style is one thing we have to neuper@42464: live with. jan@42463: jan@42463: \section{Problems rising out of the Development Environment} jan@42463: jan@42463: 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}