jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % Electronic Journal of Mathematics and Technology (eJMT) % jan@42463: % style sheet for LaTeX. Please do not modify sections % jan@42463: % or commands marked 'eJMT'. % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % eJMT commands % jan@42463: % % jan@42463: \documentclass[12pt,a4paper]{article}% % jan@42463: \usepackage{times} % jan@42463: \usepackage{amsfonts,amsmath,amssymb} % jan@42463: \usepackage[a4paper]{geometry} % jan@42463: \usepackage{fancyhdr} % jan@42463: \usepackage{color} % jan@42463: \usepackage[pdftex]{hyperref} % see note below % jan@42463: \usepackage{graphicx}% % jan@42463: \hypersetup{ % jan@42463: a4paper, % jan@42463: breaklinks % jan@42463: } % jan@42463: % % jan@42463: \newtheorem{theorem}{Theorem} % jan@42463: \newtheorem{acknowledgement}[theorem]{Acknowledgement} % jan@42463: \newtheorem{algorithm}[theorem]{Algorithm} % jan@42463: \newtheorem{axiom}[theorem]{Axiom} % jan@42463: \newtheorem{case}[theorem]{Case} % jan@42463: \newtheorem{claim}[theorem]{Claim} % jan@42463: \newtheorem{conclusion}[theorem]{Conclusion} % jan@42463: \newtheorem{condition}[theorem]{Condition} % jan@42463: \newtheorem{conjecture}[theorem]{Conjecture} % jan@42463: \newtheorem{corollary}[theorem]{Corollary} % jan@42463: \newtheorem{criterion}[theorem]{Criterion} % jan@42463: \newtheorem{definition}[theorem]{Definition} % jan@42463: \newtheorem{example}[theorem]{Example} % jan@42463: \newtheorem{exercise}[theorem]{Exercise} % jan@42463: \newtheorem{lemma}[theorem]{Lemma} % jan@42463: \newtheorem{notation}[theorem]{Notation} % jan@42463: \newtheorem{problem}[theorem]{Problem} % jan@42463: \newtheorem{proposition}[theorem]{Proposition} % jan@42463: \newtheorem{remark}[theorem]{Remark} % jan@42463: \newtheorem{solution}[theorem]{Solution} % jan@42463: \newtheorem{summary}[theorem]{Summary} % jan@42463: \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } % jan@42463: {\ \rule{0.5em}{0.5em}} % jan@42463: % % jan@42463: % eJMT page dimensions % jan@42463: % % jan@42463: \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} % jan@42463: % % jan@42463: % eJMT header & footer % jan@42463: % % jan@42463: \newcounter{ejmtFirstpage} % jan@42463: \setcounter{ejmtFirstpage}{1} % jan@42463: \pagestyle{empty} % jan@42463: \setlength{\headheight}{14pt} % jan@42463: \geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} % jan@42463: \pagestyle{fancyplain} % jan@42463: \fancyhf{} % jan@42463: \fancyhead[c]{\small The Electronic Journal of Mathematics% jan@42463: \ and Technology, Volume 1, Number 1, ISSN 1933-2823} % jan@42463: \cfoot{% % jan@42463: \ifnum\value{ejmtFirstpage}=0% % jan@42463: {\vtop to\hsize{\hrule\vskip .2cm\thepage}}% % jan@42463: \else\setcounter{ejmtFirstpage}{0}\fi% % jan@42463: } % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: % Please place your own definitions here jan@42463: % jan@42463: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} jan@42463: \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} jan@42463: jan@42463: \usepackage{color} jan@42463: \definecolor{lgray}{RGB}{238,238,238} jan@42463: jan@42463: % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % How to use hyperref % jan@42463: % ------------------- % jan@42463: % % jan@42463: % Probably the only way you will need to use the hyperref % jan@42463: % package is as follows. To make some text, say % jan@42463: % "My Text Link", into a link to the URL % jan@42463: % http://something.somewhere.com/mystuff, use % jan@42463: % % jan@42463: % \href{http://something.somewhere.com/mystuff}{My Text Link} jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: \begin{document} jan@42463: % jan@42463: % document title jan@42463: % neuper@42464: \title{Trials with TP-based Programming neuper@42464: \\ neuper@42464: for Interactive Course Material}% jan@42463: % jan@42463: % Single author. Please supply at least your name, jan@42463: % email address, and affiliation here. jan@42463: % jan@42463: \author{\begin{tabular}{c} jan@42463: \textit{Jan Ro\v{c}nik} \\ jan@42463: jan.rocnik@student.tugraz.at \\ jan@42463: IST, SPSC\\ neuper@42464: Graz University of Technologie\\ jan@42463: Austria\end{tabular} jan@42463: }% jan@42463: % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % eJMT commands - do not change these % jan@42463: % % jan@42463: \date{} % jan@42463: \maketitle % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: % abstract jan@42463: % jan@42463: \begin{abstract} jan@42463: jan@42463: Traditional course material in engineering disciplines lacks an jan@42463: important component, interactive support for step-wise problem neuper@42464: solving. Theorem-Proving (TP) technology is appropriate for one part jan@42463: of such support, in checking user-input. For the other part of such jan@42463: support, guiding the learner towards a solution, another kind of jan@42463: technology is required. %TODO ... connect to prototype ... jan@42463: jan@42463: A prototype combines TP with a programming language, the latter jan@42463: interpreted in a specific way: certain statements in a program, called jan@42463: tactics, are treated as breakpoints where control is handed over to jan@42463: the user. An input formula is checked by TP (using logical context jan@42463: built up by the interpreter); and if a learner gets stuck, a program jan@42463: describing the steps towards a solution of a problem ``knows the next jan@42463: step''. This kind of interpretation is called Lucas-Interpretation for jan@42463: \emph{TP-based programming languages}. jan@42463: jan@42463: This paper describes the prototype's TP-based programming language jan@42463: within a case study creating interactive material for an advanced jan@42463: course in Signal Processing: implementation of definitions and jan@42463: theorems in TP, formal specification of a problem and step-wise jan@42463: development of the program solving the problem. Experiences with the neuper@42464: ork flow in iterative development with testing and identifying errors jan@42463: are described, too. The description clarifies the components missing jan@42463: in the prototype's language as well as deficiencies experienced during jan@42463: programming. jan@42463: \par jan@42463: These experiences are particularly notable, because the author is the jan@42463: first programmer using the language beyond the core team which jan@42463: developed the prototype's TP-based language interpreter. jan@42463: % jan@42463: \end{abstract}% jan@42463: % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % % jan@42463: % eJMT command % jan@42463: % % jan@42463: \thispagestyle{fancy} % jan@42463: % % jan@42463: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42463: % jan@42463: % Please use the following to indicate sections, subsections, jan@42463: % etc. Please also use \subsubsection{...}, \paragraph{...} jan@42463: % and \subparagraph{...} as necessary. jan@42463: % jan@42463: neuper@42464: \section{Introduction}\label{intro} jan@42463: neuper@42464: % \paragraph{Didactics of mathematics} neuper@42464: %WN: wenn man in einem high-quality paper von 'didactics' spricht, neuper@42464: %WN muss man am state-of-the-art ankn"upfen -- siehe neuper@42464: %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants neuper@42464: % faces a specific issue, a gap neuper@42464: % between (1) introduction of math concepts and skills and (2) neuper@42464: % application of these concepts and skills, which usually are separated neuper@42464: % into different units in curricula (for good reasons). For instance, neuper@42464: % (1) teaching partial fraction decomposition is separated from (2) neuper@42464: % application for inverse Z-transform in signal processing. neuper@42464: % neuper@42464: % \par This gap is an obstacle for applying math as an fundamental neuper@42464: % thinking technology in engineering: In (1) motivation is lacking neuper@42464: % because the question ``What is this stuff good for?'' cannot be neuper@42464: % treated sufficiently, and in (2) the ``stuff'' is not available to neuper@42464: % students in higher semesters as widespread experience shows. neuper@42464: % neuper@42464: % \paragraph{Motivation} taken by this didactic issue on the one hand, neuper@42464: % and ongoing research and development on a novel kind of educational neuper@42464: % mathematics assistant at Graz University of neuper@42464: % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to neuper@42464: % scope with this issue on the other hand, several institutes are neuper@42464: % planning to join their expertise: the Institute for Information neuper@42464: % Systems and Computer Media (IICM), the Institute for Software neuper@42464: % Technology (IST), the Institutes for Mathematics, the Institute for neuper@42464: % Signal Processing and Speech Communication (SPSC), the Institute for neuper@42464: % Structural Analysis and the Institute of Electrical Measurement and neuper@42464: % Measurement Signal Processing. neuper@42464: %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell neuper@42464: %WN und damit zu verg"anglich. neuper@42464: % \par This thesis is the first attempt to tackle the above mentioned neuper@42464: % issue, it focuses on Telematics, because these specific studies focus neuper@42464: % on mathematics in \emph{STEOP}, the introductory orientation phase in neuper@42464: % Austria. \emph{STEOP} is considered an opportunity to investigate the neuper@42464: % impact of {\sisac}'s prototype on the issue and others. neuper@42464: % neuper@42464: neuper@42464: Traditional course material in engineering disciplines lacks an neuper@42464: important component, interactive support for step-wise problem neuper@42464: solving. Theorem-Proving (TP) technology can provide such support by neuper@42464: specific services. An important part of such services is called neuper@42464: ``next-step-guidance'', generated by a specific kind of ``TP-based neuper@42464: programming language''. In the neuper@42464: {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such neuper@42464: a language is prototyped in line with~\cite{plmms10} and built upon neuper@42464: the theorem prover neuper@42464: Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}. neuper@42464: The TP services are coordinated by a specific interpreter for the neuper@42464: programming language, called neuper@42464: Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the neuper@42464: interpreter will be briefly re-introduced in order to make the paper neuper@42464: self-contained. jan@42463: neuper@42464: \medskip The main part of the paper is an account of first experiences neuper@42464: with programming in this TP-based language. The experience was gained neuper@42464: in a case study by the author. The author was considered an ideal neuper@42464: candidate for this study for the following reasons: as a student in neuper@42464: Telematics (computer science with focus on Signal Processing) he had neuper@42464: general knowledge in programming as well as specific domain knowledge neuper@42464: in Signal Processing; and he was not involved in the development of neuper@42464: {\sisac}'s programming language and interpeter, thus a novice to the neuper@42464: language. jan@42463: neuper@42464: The goal of the case study was (1) some TP-based programs for neuper@42464: interactive course material for a specific ``Adavanced Signal neuper@42464: Processing Lab'' in a higher semester, (2) respective program neuper@42464: development with as little advice from the {\sisac}-team and (3) records neuper@42464: and comments for the main steps of development in an Isabelle theory; neuper@42464: this theory should provide guidelines for future programmers. An neuper@42464: excerpt from this theory is the main part of this paper. neuper@42464: neuper@42464: \medskip The paper will use the problem in Fig.\ref{fig-interactive} as a jan@42463: running example: jan@42463: \begin{figure} [htb] jan@42463: \begin{center} neuper@42464: \includegraphics[width=120mm]{fig/isac-Ztrans-math.png} jan@42463: \caption{Step-wise problem solving guided by the TP-based program} jan@42463: \label{fig-interactive} jan@42463: \end{center} jan@42463: \end{figure} neuper@42464: The problem is from the domain of Signal Processing and requests to neuper@42464: determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive} neuper@42464: also shows the beginning of the interactive construction of a solution neuper@42464: for the problem. This construction is done in the right window named neuper@42464: ``Worksheet''. neuper@42464: neuper@42464: User-interaction on the Worksheet is {\em checked} and {\em guided} by neuper@42464: TP services: neuper@42464: \begin{enumerate} neuper@42464: \item Formulas input by the user are {\em checked} by TP: such a neuper@42464: formula establishes a proof situation --- the prover has to derive the neuper@42464: formula from the logical context. The context is built up from the neuper@42464: formal specification of the problem (here hidden from the user) by the neuper@42464: Lucas-Interpreter. neuper@42464: \item If the user gets stuck, the program developed below in this neuper@42464: paper ``knows the next step'' from behind the scenes. How the latter neuper@42464: TP-service is exploited by dialogue authoring is out of scope of this neuper@42464: paper and can be studied in~\cite{gdaroczy-EP-13}. neuper@42464: \end{enumerate} It should be noted that the programmer using the neuper@42464: TP-based language is not concerned with interaction at all; we will neuper@42464: see that the program contains neither input-statements nor neuper@42464: output-statements. Rather, interaction is handled by services neuper@42464: generated automatically. neuper@42464: neuper@42464: \medskip So there is a clear separation of concerns: Dialogues are neuper@42464: adapted by dialogue authors (in Java-based tools), using automatically neuper@42464: generated TP services, while the TP-based program is written by neuper@42464: mathematics experts (in Isabelle/ML). The latter is concern of this neuper@42464: paper. neuper@42464: neuper@42464: \medskip The paper is structed as follows: The introduction neuper@42464: \S\ref{intro} is followed by a brief re-introduction of the TP-based neuper@42464: programming language in \S\ref{PL}, which extends the executable neuper@42464: fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which neuper@42464: play a specific role in Lucas-Interpretation and in providing the TP neuper@42464: services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes neuper@42464: the main steps in developing the program for the running example: neuper@42464: prepare domain knowledge, implement the formal specification of the neuper@42464: problem, prepare the environment for the program, implement the neuper@42464: program. The workflow of programming, debugging and testing is neuper@42464: described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will neuper@42464: give directions identified for future development. neuper@42464: jan@42463: jan@42463: \section{\isac's Prototype for a Programming Language}\label{PL} jan@42463: The prototype's language extends the executable fragment in the jan@42463: language of the theorem prover jan@42463: Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/} jan@42463: by tactics which have a specific role in Lucas-Interpretation. jan@42463: jan@42463: \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab} jan@42463: The executable fragment consists of data-type and function jan@42463: definitions. It's usability even suggests that fragment for jan@42463: introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic jan@42463: whose type system resembles that of functional programming jan@42463: languages. Thus there are jan@42463: \begin{description} jan@42463: \item[base types,] in particular \textit{bool}, the type of truth jan@42463: values, \textit{nat}, \textit{int}, \textit{complex}, and the types of jan@42463: natural, integer and complex numbers respectively in mathematics. jan@42463: \item[type constructors] allow to define arbitrary types, from jan@42463: \textit{set}, \textit{list} to advanced data-structures like jan@42463: \textit{trees}, red-black-trees etc. jan@42463: \item[function types,] denoted by $\Rightarrow$. jan@42463: \item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide jan@42463: type polymorphism. Isabelle automatically computes the type of each jan@42463: variable in a term by use of Hindley-Milner type inference jan@42463: \cite{pl:hind97,Milner-78}. jan@42463: \end{description} jan@42463: jan@42463: \textbf{Terms} are formed as in functional programming by applying jan@42463: functions to arguments. If $f$ is a function of type jan@42463: $\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then jan@42463: $f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$ jan@42463: has type $\tau$. There are many predefined infix symbols like $+$ and jan@42463: $\leq$ most of which are overloaded for various types. jan@42463: jan@42463: HOL also supports some basic constructs from functional programming: jan@42463: {\it\label{isabelle-stmts} jan@42463: \begin{tabbing} 123\=\kill jan@42463: \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\ jan@42463: \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\ jan@42463: \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1 jan@42463: \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$ jan@42463: \end{tabbing} } jan@42463: \noindent \textit{The running example's program uses some of these elements jan@42463: (marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt jan@42463: let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for jan@42463: lists and {\tt o} for functional (forward) composition in line jan@42463: $10$. In fact, the whole program is an Isabelle term with specific jan@42463: function constants like {\sc program}, {\sc Substitute} and {\sc jan@42463: Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.} jan@42463: jan@42463: % Terms may also contain $\lambda$-abstractions. For example, $\lambda jan@42463: % x. \; x$ is the identity function. jan@42463: neuper@42464: \textbf{Formulae} are terms of type \textit{bool}. There are the basic jan@42463: constants \textit{True} and \textit{False} and the usual logical jan@42463: connectives (in decreasing order of precedence): $\neg, \land, \lor, jan@42463: \rightarrow$. jan@42463: neuper@42464: \textbf{Equality} is available in the form of the infix function $=$ neuper@42464: of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for neuper@42464: formulas, where it means ``if and only if''. jan@42463: jan@42463: \textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \; jan@42463: P$. Quantifiers lead to non-executable functions, so functions do not jan@42463: always correspond to programs, for instance, if comprising \\$( jan@42463: \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2 jan@42463: \;)$. jan@42463: jan@42463: \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs} jan@42463: The prototype extends Isabelle's language by specific statements neuper@42464: called tactics~\footnote{{\sisac}'s tactics are different from jan@42463: Isabelle's tactics: the former concern steps in a calculation, the jan@42463: latter concern proof steps.} and tacticals. For the programmer these jan@42463: statements are functions with the following signatures: jan@42463: jan@42463: \begin{description} jan@42463: \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it jan@42463: term} * {\it term}\;{\it list}$: jan@42463: this tactic appplies {\it theorem} to a {\it term} yielding a {\it jan@42463: term} and a {\it term list}, the list are assumptions generated by jan@42463: conditional rewriting. For instance, the {\it theorem} jan@42463: $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$ jan@42463: applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields jan@42463: $(\frac{2}{3}, [x\not=0])$. jan@42463: jan@42463: \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term} * {\it term}\;{\it list}$: jan@42463: this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is jan@42463: a confluent and terminating term rewrite system, in general. If jan@42463: none of the rules ({\it theorem}s) is applicable on interpretation jan@42463: of this tactic, an exception is thrown. jan@42463: jan@42463: % \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it jan@42463: % theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it jan@42463: % list}$: jan@42463: % jan@42463: % \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it jan@42463: % ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it jan@42463: % list}$: jan@42463: jan@42463: \item[Substitute:] ${\it substitution}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: \item[Take:] ${\it term}\Rightarrow{\it term}$: jan@42463: this tactic has no effect in the program; but it creates a side-effect jan@42463: by Lucas-Interpretation (see below) and writes {\it term} to the jan@42463: Worksheet. jan@42463: jan@42463: \item[Subproblem:] ${\it theory} * {\it specification} * {\it jan@42463: method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$: jan@42463: this tactic allows to enter a phase of interactive specification jan@42463: of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance, jan@42463: a specific type of equation) and a method (for instance, solving an jan@42463: equation symbolically or numerically). jan@42463: jan@42463: \end{description} jan@42463: The tactics play a specific role in jan@42463: Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as jan@42463: break-points and control is handed over to the user. The user is free jan@42463: to investigate underlying knowledge, applicable theorems, etc. And jan@42463: the user can proceed constructing a solution by input of a tactic to jan@42463: be applied or by input of a formula; in the latter case the jan@42463: Lucas-Interpreter has built up a logical context (initialised with the jan@42463: precondition of the formal specification) such that Isabelle can jan@42463: derive the formula from this context --- or give feedback, that no jan@42463: derivation can be found. jan@42463: jan@42463: \subsection{Tacticals for Control of Interpretation} jan@42463: The flow of control in a program can be determined by {\tt if then else} jan@42463: and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also jan@42463: by additional tacticals: jan@42463: \begin{description} jan@42463: \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it jan@42463: term}$: iterates over tactics which take a {\it term} as argument as jan@42463: long as a tactic is applicable (for instance, {\it Rewrite\_Set} might jan@42463: not be applicable). jan@42463: jan@42463: \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$: jan@42463: if {\it tactic} is applicable, then it is applied to {\it term}, jan@42463: otherwise {\it term} is passed on unchanged. jan@42463: jan@42463: \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: jan@42463: \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it jan@42463: term}\Rightarrow{\it term}$: jan@42463: jan@42463: \end{description} jan@42463: jan@42463: no input / output --- Lucas-Interpretation jan@42463: jan@42463: .\\.\\.\\TODO\\.\\.\\ jan@42463: neuper@42464: \section{Development of a Program on Trial}\label{trial} neuper@42464: As mentioned above, {\sisac} is an experimental system for a proof of neuper@42464: concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The neuper@42464: latter interprets a specific kind of TP-based programming language, neuper@42464: which is as experimental as the whole prototype --- so programming in neuper@42464: this language can be only ``on trial'', presently. However, as a neuper@42464: prototype, the language addresses essentials described below. neuper@42464: neuper@42464: \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac} neuper@42464: neuper@42464: %WN was Fachleute unter obigem Titel interessiert findet neuper@42464: %WN unterhalb des auskommentierten Textes. neuper@42464: neuper@42464: %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell neuper@42464: %WN auf Computer-Mathematiker fokussiert. neuper@42464: % \paragraph{As mentioned in the introduction,} a prototype of an neuper@42464: % educational math assistant called neuper@42464: % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for neuper@42464: % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges neuper@42464: % the gap between (1) introducation and (2) application of mathematics: neuper@42464: % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which neuper@42464: % requires each fact and each action justified by formal logic, so neuper@42464: % {{{\sisac}{}}} makes justifications transparent to students in neuper@42464: % interactive step-wise problem solving. By that way {{\sisac}} already neuper@42464: % can serve both: neuper@42464: % \begin{enumerate} neuper@42464: % \item Introduction of math stuff (in e.g. partial fraction neuper@42464: % decomposition) by stepwise explaining and exercising respective neuper@42464: % symbolic calculations with ``next step guidance (NSG)'' and rigorously neuper@42464: % checking steps freely input by students --- this also in context with neuper@42464: % advanced applications (where the stuff to be taught in higher neuper@42464: % semesters can be skimmed through by NSG), and neuper@42464: % \item Application of math stuff in advanced engineering courses neuper@42464: % (e.g. problems to be solved by inverse Z-transform in a Signal neuper@42464: % Processing Lab) and now without much ado about basic math techniques neuper@42464: % (like partial fraction decomposition): ``next step guidance'' supports neuper@42464: % students in independently (re-)adopting such techniques. neuper@42464: % \end{enumerate} neuper@42464: % Before the question is answers, how {{\sisac}} neuper@42464: % accomplishes this task from a technical point of view, some remarks on neuper@42464: % the state-of-the-art is given, therefor follow up Section~\ref{emas}. neuper@42464: % neuper@42464: % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} neuper@42464: % neuper@42464: % \paragraph{Educational software in mathematics} is, if at all, based neuper@42464: % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry neuper@42464: % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org} neuper@42464: % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC neuper@42464: % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These neuper@42464: % base technologies are used to program math lessons and sometimes even neuper@42464: % exercises. The latter are cumbersome: the steps towards a solution of neuper@42464: % such an interactive exercise need to be provided with feedback, where neuper@42464: % at each step a wide variety of possible input has to be foreseen by neuper@42464: % the programmer - so such interactive exercises either require high neuper@42464: % development efforts or the exercises constrain possible inputs. neuper@42464: % neuper@42464: % \subparagraph{A new generation} of educational math assistants (EMAs) neuper@42464: % is emerging presently, which is based on Theorem Proving (TP). TP, for neuper@42464: % instance Isabelle and Coq, is a technology which requires each fact neuper@42464: % and each action justified by formal logic. Pushed by demands for neuper@42464: % \textit{proven} correctness of safety-critical software TP advances neuper@42464: % into software engineering; from these advancements computer neuper@42464: % mathematics benefits in general, and math education in particular. Two neuper@42464: % features of TP are immediately beneficial for learning: neuper@42464: % neuper@42464: % \paragraph{TP have knowledge in human readable format,} that is in neuper@42464: % standard predicate calculus. TP following the LCF-tradition have that neuper@42464: % knowledge down to the basic definitions of set, equality, neuper@42464: % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; neuper@42464: % following the typical deductive development of math, natural numbers neuper@42464: % are defined and their properties neuper@42464: % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, neuper@42464: % etc. Present knowledge mechanized in TP exceeds high-school neuper@42464: % mathematics by far, however by knowledge required in software neuper@42464: % technology, and not in other engineering sciences. neuper@42464: % neuper@42464: % \paragraph{TP can model the whole problem solving process} in neuper@42464: % mathematical problem solving {\em within} a coherent logical neuper@42464: % framework. This is already being done by three projects, by neuper@42464: % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor. neuper@42464: % \par neuper@42464: % Having the whole problem solving process within a logical coherent neuper@42464: % system, such a design guarantees correctness of intermediate steps and neuper@42464: % of the result (which seems essential for math software); and the neuper@42464: % second advantage is that TP provides a wealth of theories which can be neuper@42464: % exploited for mechanizing other features essential for educational neuper@42464: % software. neuper@42464: % neuper@42464: % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid} neuper@42464: % neuper@42464: % One essential feature for educational software is feedback to user neuper@42464: % input and assistance in coming to a solution. neuper@42464: % neuper@42464: % \paragraph{Checking user input} by ATP during stepwise problem solving neuper@42464: % is being accomplished by the three projects mentioned above neuper@42464: % exclusively. They model the whole problem solving process as mentioned neuper@42464: % above, so all what happens between formalized assumptions (or formal neuper@42464: % specification) and goal (or fulfilled postcondition) can be neuper@42464: % mechanized. Such mechanization promises to greatly extend the scope of neuper@42464: % educational software in stepwise problem solving. neuper@42464: % neuper@42464: % \paragraph{NSG (Next step guidance)} comprises the system's ability to neuper@42464: % propose a next step; this is a challenge for TP: either a radical neuper@42464: % restriction of the search space by restriction to very specific neuper@42464: % problem classes is required, or much care and effort is required in neuper@42464: % designing possible variants in the process of problem solving neuper@42464: % \cite{proof-strategies-11}. neuper@42464: % \par neuper@42464: % Another approach is restricted to problem solving in engineering neuper@42464: % domains, where a problem is specified by input, precondition, output neuper@42464: % and postcondition, and where the postcondition is proven by ATP behind neuper@42464: % the scenes: Here the possible variants in the process of problem neuper@42464: % solving are provided with feedback {\em automatically}, if the problem neuper@42464: % is described in a TP-based programing language: \cite{plmms10} the neuper@42464: % programmer only describes the math algorithm without caring about neuper@42464: % interaction (the respective program is functional and even has no neuper@42464: % input or output statements!); interaction is generated as a neuper@42464: % side-effect by the interpreter --- an efficient separation of concern neuper@42464: % between math programmers and dialog designers promising application neuper@42464: % all over engineering disciplines. neuper@42464: % neuper@42464: % neuper@42464: % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}} neuper@42464: % Authoring new mathematics knowledge in {{\sisac}} can be compared with neuper@42464: % ``application programing'' of engineering problems; most of such neuper@42464: % programing uses CAS-based programing languages (CAS = Computer Algebra neuper@42464: % Systems; e.g. Mathematica's or Maple's programing language). neuper@42464: % neuper@42464: % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}} neuper@42464: % \cite{plmms10} for describing how to construct a solution to an neuper@42464: % engineering problem and for calling equation solvers, integration, neuper@42464: % etc~\footnote{Implementation of CAS-like functionality in TP is not neuper@42464: % primarily concerned with efficiency, but with a didactic question: neuper@42464: % What to decide for: for high-brow algorithms at the state-of-the-art neuper@42464: % or for elementary algorithms comprehensible for students?} within TP; neuper@42464: % TP can ensure ``systems that never make a mistake'' \cite{casproto} - neuper@42464: % are impossible for CAS which have no logics underlying. neuper@42464: % neuper@42464: % \subparagraph{Authoring is perfect} by writing such TP based programs; neuper@42464: % the application programmer is not concerned with interaction or with neuper@42464: % user guidance: this is concern of a novel kind of program interpreter neuper@42464: % called Lucas-Interpreter. This interpreter hands over control to a neuper@42464: % dialog component at each step of calculation (like a debugger at neuper@42464: % breakpoints) and calls automated TP to check user input following neuper@42464: % personalized strategies according to a feedback module. neuper@42464: % \par neuper@42464: % However ``application programing with TP'' is not done with writing a neuper@42464: % program: according to the principles of TP, each step must be neuper@42464: % justified. Such justifications are given by theorems. So all steps neuper@42464: % must be related to some theorem, if there is no such theorem it must neuper@42464: % be added to the existing knowledge, which is organized in so-called neuper@42464: % \textbf{theories} in Isabelle. A theorem must be proven; fortunately neuper@42464: % Isabelle comprises a mechanism (called ``axiomatization''), which neuper@42464: % allows to omit proofs. Such a theorem is shown in neuper@42464: % Example~\ref{eg:neuper1}. neuper@42464: neuper@42464: The running example, introduced by Fig.\ref{fig-interactive} on neuper@42464: p.\pageref{fig-interactive}, requires to determine the inverse $\cal neuper@42464: Z$-transform for a class of functions. The domain of Signal Processing neuper@42464: is accustomed to specific notation for the resulting functions, which neuper@42464: are absolutely summable and are called TODO: $u[n]$, where $u$ is the neuper@42464: function, $n$ is the argument and the brackets indicate that the neuper@42464: arguments are TODO. Surprisingly, Isabelle accepts the rules for neuper@42464: ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle neuper@42464: experts might be particularly surprised, that the brackets do not neuper@42464: cause errors in typing (as lists).}: neuper@42464: %\vbox{ neuper@42464: % \begin{example} jan@42463: \label{eg:neuper1} jan@42463: {\small\begin{tabbing} jan@42463: 123\=123\=123\=123\=\kill jan@42463: \hfill \\ jan@42463: \>axiomatization where \\ neuper@42464: \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\ neuper@42464: \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\ neuper@42464: \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\ neuper@42464: %TODO neuper@42464: \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\ neuper@42464: %TODO jan@42463: \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\ jan@42463: %TODO neuper@42464: \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\ neuper@42464: %TODO neuper@42464: \end{tabbing} neuper@42464: } neuper@42464: % \end{example} neuper@42464: %} neuper@42464: These 6 rules can be used as conditional rewrite rules, depending on neuper@42464: the respective convergence radius. Satisfaction from notation neuper@42464: contrasts with the word {\em axiomatization}: As TP-based, the neuper@42464: programming language expects these rules as {\em proved} theorems, and neuper@42464: not as axioms implemented in the above brute force manner; otherwise neuper@42464: all the verification efforts envisaged (like proof of the neuper@42464: post-condition, see below) would be meaningless. neuper@42464: neuper@42464: Isabelle provides a large body of knowledge, rigorously proven from neuper@42464: the basic axioms of mathematics~\footnote{This way of rigorously neuper@42464: deriving all knowledge from first principles is called the neuper@42464: LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced neuper@42464: knowledge can be found in the theoris on Multivariate neuper@42464: Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However, neuper@42464: building up knowledge such that a proof for the above rules would be neuper@42464: reasonably short and easily comprehensible, still requires lots of neuper@42464: work (and is definitely out of scope of our case study). neuper@42464: neuper@42464: \medskip At the state-of-the-art in mechanization of knowledge in neuper@42464: engineering, the process does not stop with the mechanization of neuper@42464: mathematics. Rather, ``Formal Methods''~\cite{TODO-formal-methods} neuper@42464: proceed to formal description of physical items. Signal Processing, neuper@42464: for instance is concerned with physical devices for signal acquisition neuper@42464: and reconstruction, which involve measuring a physical signal, storing neuper@42464: it, and possibly later rebuilding the original signal or an neuper@42464: approximation thereof. For digital systems, this typically includes neuper@42464: sampling and quantization; devices for signal compression, including neuper@42464: audio compression, image compression, and video compression, etc. neuper@42464: ``Domain engineering''\cite{db-domain-engineering} is concerned with neuper@42464: {\em specification} of these devices' components and features; this neuper@42464: part in the process of mechanization is only at the beginning. neuper@42464: neuper@42464: \medskip TP-based programming, concern of this paper, adds a third neuper@42464: part of mechanisation, providing a third axis of ``algorithmic neuper@42464: knowledge'' in Fig.\ref{fig:mathuni} on p.\pageref{fig:mathuni}. neuper@42464: neuper@42464: \begin{figure} neuper@42464: \hfill \\ neuper@42464: \begin{center} neuper@42464: \includegraphics{fig/universe} neuper@42464: \caption{Didactic ``Math-Universe''\label{fig:mathuni}} neuper@42464: \end{center} neuper@42464: \end{figure} neuper@42464: %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen; neuper@42464: %WN bitte folgende Bezeichnungen nehmen: neuper@42464: %WN neuper@42464: %WN axis 1: Algorithmic Knowledge (Programs) neuper@42464: %WN axis 2: Application-oriented Knowledge (Specifications) neuper@42464: %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems) neuper@42464: neuper@42464: \subsection{Specification of the Problem}\label{spec} neuper@42464: %WN <--> \chapter 7 der Thesis neuper@42464: %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. neuper@42464: In order to provide TP with logical facts for checking user input, the neuper@42464: Lucas-Interpreter requires a \textbf{specification}. Such a neuper@42464: specification is shown in Example~\ref{eg:neuper2}. neuper@42464: jan@42463: ------------------------------------------------------------------- jan@42463: jan@42463: Hier brauchen wir die Spezifikation des 'running example' ... jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:neuper2} jan@42463: {\small\begin{tabbing} jan@42463: 123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill jan@42463: \hfill \\ jan@42463: Specification no.1:\\ jan@42463: %\>input\>: $\{\;r={\it arbitraryFix}\;\}$ \\ jan@42463: \>input \>: $\{\;r\;\}$ \\ jan@42463: \>precond \>: $0 < r$ \\ jan@42463: \>output \>: $\{\;A,\; u,v\;\}$ \\ jan@42463: \>postcond \>:{\small $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\ jan@42463: \> \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land jan@42463: (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\ jan@42463: \>props\>: $\{\;A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\;\}$ neuper@42464: \end{tabbing} neuper@42464: } neuper@42464: \end{example} neuper@42464: } neuper@42464: neuper@42464: ... und die Implementation in Isac (mit Kommentaren aus dem datatype) neuper@42464: jan@42463: %WN das w"urde ich in \sec\label{} jan@42463: Such a specification is checked before the execution of a program is jan@42463: started, the same applies for sub-programs. In the following example jan@42463: (Example~\ref{eg:subprob}) shows the call of such a subproblem: jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:subprob} jan@42463: \hfill \\ jan@42463: {\ttfamily \begin{tabbing} jan@42463: ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\ jan@42463: ``\>\>[linear,univariate,equation,test],'' \\ jan@42463: ``\>\>[Test,solve\_linear])'' \\ neuper@42464: ``\>[BOOL equ, REAL z])'' \\ neuper@42464: \end{tabbing} neuper@42464: } neuper@42464: {\small\textit{ jan@42463: \noindent If a program requires a result which has to be jan@42463: calculated first we can use a subproblem to do so. In our specific jan@42463: case we wanted to calculate the zeros of a fraction and used a neuper@42464: subproblem to calculate the zeros of the denominator polynom. neuper@42464: }} neuper@42464: \end{example} neuper@42464: } neuper@42464: neuper@42464: \subsection{Implementation of the Method}\label{meth} neuper@42464: %WN <--> \chapter 7 der Thesis neuper@42464: TODO neuper@42464: \subsection{Preparation of ML-Functions for the Program}\label{funs} neuper@42464: %WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr} neuper@42464: %WN brauchst neuper@42464: TODO jan@42463: \subsection{Implementation of the TP-based Program}\label{progr} neuper@42464: %WN <--> \chapter 8 der Thesis neuper@42464: TODO neuper@42464: neuper@42464: \section{Workflow of Programming in the Prototype}\label{workflow} neuper@42464: ------------------------------------------------------------------- neuper@42464: neuper@42464: ``workflow'' heisst: das mache ich zuerst, dann das ... neuper@42464: neuper@42464: \subsection{Preparations and Trials}\label{flow-prep} neuper@42464: TODO ... Build\_Inverse\_Z\_Transform.thy !!! neuper@42464: neuper@42464: \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} neuper@42464: TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac'' neuper@42464: neuper@42464: \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans} neuper@42464: TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ? neuper@42464: neuper@42464: ------------------------------------------------------------------- neuper@42464: neuper@42464: Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are jan@42463: vermutlich auf andere sections aufzuteilen. jan@42463: neuper@42464: ------------------------------------------------------------------- neuper@42464: neuper@42464: \subsection{Formalization of missing knowledge in Isabelle} neuper@42464: jan@42463: \paragraph{A problem} behind is the mechanization of mathematic jan@42463: theories in TP-bases languages. There is still a huge gap between jan@42463: these algorithms and this what we want as a solution - in Example jan@42463: Signal Processing. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:gap} neuper@42464: \[ neuper@42464: X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY neuper@42464: \] neuper@42464: {\small\textit{ neuper@42464: \noindent A very simple example on this what we call gap is the neuper@42464: simplification above. It is needles to say that it is correct and also neuper@42464: Isabelle for fills it correct - \emph{always}. But sometimes we don't jan@42463: want expand such terms, sometimes we want another structure of jan@42463: them. Think of a problem were we now would need only the coefficients jan@42463: of $X$ and $Y$. This is what we call the gap between mechanical jan@42463: simplification and the solution. neuper@42464: }} neuper@42464: \end{example} neuper@42464: } neuper@42464: neuper@42464: \paragraph{We are not able to fill this gap,} until we have to live neuper@42464: with it but first have a look on the meaning of this statement: neuper@42464: Mechanized math starts from mathematical models and \emph{hopefully} neuper@42464: proceeds to match physics. Academic engineering starts from physics neuper@42464: (experimentation, measurement) and then proceeds to mathematical jan@42463: modeling and formalization. The process from a physical observance to jan@42463: a mathematical theory is unavoidable bound of setting up a big jan@42463: collection of standards, rules, definition but also exceptions. These jan@42463: are the things making mechanization that difficult. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:units} neuper@42464: \[ neuper@42464: m,\ kg,\ s,\ldots neuper@42464: \] neuper@42464: {\small\textit{ neuper@42464: \noindent Think about some units like that one's above. Behind neuper@42464: each unit there is a discerning and very accurate definition: One jan@42463: Meter is the distance the light travels, in a vacuum, through the time jan@42463: of 1 / 299.792.458 second; one kilogram is the weight of a jan@42463: platinum-iridium cylinder in paris; and so on. But are these jan@42463: definitions usable in a computer mechanized world?! neuper@42464: }} neuper@42464: \end{example} neuper@42464: } neuper@42464: jan@42463: \paragraph{A computer} or a TP-System builds on programs with jan@42463: predefined logical rules and does not know any mathematical trick jan@42463: (follow up example \ref{eg:trick}) or recipe to walk around difficult jan@42463: expressions. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:trick} jan@42463: \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] neuper@42464: \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= neuper@42464: \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] neuper@42464: \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] neuper@42464: {\small\textit{ neuper@42464: \noindent Sometimes it is also useful to be able to apply some jan@42463: \emph{tricks} to get a beautiful and particularly meaningful result, jan@42463: which we are able to interpret. But as seen in this example it can be jan@42463: hard to find out what operations have to be done to transform a result jan@42463: into a meaningful one. neuper@42464: }} neuper@42464: \end{example} neuper@42464: } neuper@42464: neuper@42464: \paragraph{The only possibility,} for such a system, is to work neuper@42464: through its known definitions and stops if none of these neuper@42464: fits. Specified on Signal Processing or any other application it is neuper@42464: often possible to walk through by doing simple creases. This creases neuper@42464: are in general based on simple math operational but the challenge is neuper@42464: to teach the machine \emph{all}\footnote{Its pride to call it jan@42463: \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to neuper@42464: reach a high level of \emph{all} but it in real it will still be a neuper@42464: survey of knowledge which links to other knowledge and {{\sisac}{}} a neuper@42464: trainer and helper but no human compensating calculator. neuper@42464: \par neuper@42464: {{{\sisac}{}}} itself aims to adds an \emph{application} axis (formal jan@42463: specifications of problems out of topics from Signal Processing, etc.) jan@42463: and an \emph{algorithmic} axis to the \emph{deductive} axis of jan@42463: physical knowledge. The result is a three-dimensional universe of jan@42463: mathematics seen in Figure~\ref{fig:mathuni}. jan@42463: jan@42463: \begin{figure} jan@42463: \hfill \\ jan@42463: \begin{center} jan@42463: \includegraphics{fig/universe} jan@42463: \caption{Didactic ``Math-Universe''\label{fig:mathuni}} jan@42463: \end{center} neuper@42464: \end{figure} neuper@42464: neuper@42464: \subsection{Notes on Problems with Traditional Notation} neuper@42464: neuper@42464: \paragraph{During research} on these topic severely problems on neuper@42464: traditional notations have been discovered. Some of them have been jan@42463: known in computer science for many years now and are still unsolved, jan@42463: one of them aggregates with the so called \emph{Lambda Calculus}, jan@42463: Example~\ref{eg:lamda} provides a look on the problem that embarrassed jan@42463: us. jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:lamda} jan@42463: jan@42463: \[ f(x)=\ldots\; \quad R \rightarrow \quad R \] jan@42463: neuper@42464: neuper@42464: \[ f(p)=\ldots\; p \in \quad R \] neuper@42464: neuper@42464: {\small\textit{ neuper@42464: \noindent Above we see two equations. The first equation aims to neuper@42464: be a mapping of an function from the reel range to the reel one, but neuper@42464: when we change only one letter we get the second equation which jan@42463: usually aims to insert a reel point $p$ into the reel function. In jan@42463: computer science now we have the problem to tell the machine (TP) the jan@42463: difference between this two notations. This Problem is called jan@42463: \emph{Lambda Calculus}. neuper@42464: }} neuper@42464: \end{example} neuper@42464: } neuper@42464: neuper@42464: \paragraph{An other problem} is that terms are not full simplified in neuper@42464: traditional notations, in {{\sisac}} we have to simplify them complete neuper@42464: to check weather results are compatible or not. in e.g. the solutions neuper@42464: of an second order linear equation is an rational in {{\sisac}} but in neuper@42464: tradition we keep fractions as long as possible and as long as they neuper@42464: aim to be \textit{beautiful} (1/8, 5/16,...). neuper@42464: \subparagraph{The math} which should be mechanized in Computer Theorem neuper@42464: Provers (\emph{TP}) has (almost) a problem with traditional notations neuper@42464: (predicate calculus) for axioms, definitions, lemmas, theorems as a neuper@42464: computer program or script is not able to interpret every Greek or jan@42463: Latin letter and every Greek, Latin or whatever calculations jan@42463: symbol. Also if we would be able to handle these symbols we still have jan@42463: a problem to interpret them at all. (Follow up \hbox{Example jan@42463: \ref{eg:symbint1}}) jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:symbint1} neuper@42464: \[ neuper@42464: u\left[n\right] \ \ldots \ unitstep neuper@42464: \] neuper@42464: {\small\textit{ neuper@42464: \noindent The unitstep is something we need to solve Signal jan@42463: Processing problem classes. But in {{{\sisac}{}}} the rectangular jan@42463: brackets have a different meaning. So we abuse them for our jan@42463: requirements. We get something which is not defined, but usable. The jan@42463: Result is syntax only without semantic. neuper@42464: }} neuper@42464: \end{example} neuper@42464: } jan@42463: jan@42463: In different problems, symbols and letters have different meanings and jan@42463: ask for different ways to get through. (Follow up \hbox{Example jan@42463: \ref{eg:symbint2}}) jan@42463: jan@42463: \vbox{ jan@42463: \begin{example} jan@42463: \label{eg:symbint2} neuper@42464: \[ neuper@42464: \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent neuper@42464: \] neuper@42464: {\small\textit{ jan@42463: \noindent For using exponents the three \texttt{widehat} symbols jan@42463: are required. The reason for that is due the development of jan@42463: {{{\sisac}{}}} the single \texttt{widehat} and also the double were jan@42463: already in use for different operations. neuper@42464: }} neuper@42464: \end{example} neuper@42464: } neuper@42464: neuper@42464: \paragraph{Also the output} can be a problem. We are familiar with a neuper@42464: specified notations and style taught in university but a computer neuper@42464: program has no knowledge of the form proved by a professor and the neuper@42464: machines themselves also have not yet the possibilities to print every jan@42463: symbol (correct) Recent developments provide proofs in a human jan@42463: readable format but according to the fact that there is no money for jan@42463: good working formal editors yet, the style is one thing we have to jan@42463: live with. jan@42463: neuper@42464: \section{Problems rising out of the Development Environment} jan@42463: jan@42463: fehlermeldungen! TODO jan@42463: jan@42463: \section{Conclusion}\label{conclusion} jan@42463: jan@42463: TODO jan@42463: neuper@42464: \bibliographystyle{alpha} neuper@42464: \bibliography{references} neuper@42464: neuper@42464: \end{document}