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: jan@42463: % isac logos 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: % jan@42463: \title{Interactive Course Material by TP-based Programming}% 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\\ jan@42463: University of Technologie Graz\\ 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 jan@42463: solving. \textbf{TP} (Theorem-Proving) 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 jan@42463: work 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: jan@42463: \section{Introduction} jan@42463: jan@42463: \paragraph{Didactics of mathematics} faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which usually are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing. jan@42463: \par jan@42463: This gap is an obstacle for applying math as an fundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows. jan@42463: jan@42463: \paragraph{Motivation} taken by this didactic issue on the one hand, and ongoing research and development on a novel kind of educational mathematics assistant at Graz University of Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to scope with this issue on the other hand, several institutes are planning to join their expertise: the Institute for Information Systems and Computer Media (IICM), the Institute for Software Technology (IST), the Institutes for Mathematics, the Institute for Signal Processing and Speech Communication (SPSC), the Institute for Structural Analysis and the Institute of Electrical Measurement and Measurement Signal Processing. jan@42463: \par This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in \emph{STEOP}, the introductory orientation phase in Austria. \emph{STEOP} is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. jan@42463: jan@42463: The paper will use the problem in Fig.\ref{fig-gclc} as a jan@42463: running example: jan@42463: \begin{figure} [htb] jan@42463: \begin{center} jan@42463: %\includegraphics[width=120mm]{fig/newgen/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: \label{fig-gclc} jan@42463: \end{figure} 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: jan@42463: \textbf{Formula} 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: jan@42463: \textbf{Equality} is available in the form of the infix function $=$ of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for 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 jan@42463: 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@42463: \section{Development of a Program on Trial}\label{trial} jan@42463: jan@42463: \subsection{Mechanization of Math in Isabelle/ISAC\label{isabisac}} jan@42463: jan@42463: \paragraph{As mentioned in the introduction,} a prototype of an educational math assistant called {\sisac}\footnote{{\sisac}=\textbf{Isa}belle for \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges the gap between (1) introducation and (2) application of mathematics: {\sisac} is based on Computer Theorem Proving (TP), a technology which requires each fact and each action justified by formal logic, so {{\sisac{}}} makes justifications transparent to students in interactive step-wise problem solving. By that way {\sisac} already can serve both: jan@42463: \begin{enumerate} jan@42463: \item Introduction of math stuff (in e.g. partial fraction decomposition) by stepwise explaining and exercising respective symbolic calculations with ``next step guidance (NSG)'' and rigorously checking steps freely input by students --- this also in context with advanced applications (where the stuff to be taught in higher semesters can be skimmed through by NSG), and jan@42463: \item Application of math stuff in advanced engineering courses (e.g. problems to be solved by inverse Z-transform in a Signal Processing Lab) and now without much ado about basic math techniques (like partial fraction decomposition): ``next step guidance'' supports students in independently (re-)adopting such techniques. jan@42463: \end{enumerate} jan@42463: Before the question is answers, how {\sisac} accomplishes this task from a technical point of view, some remarks on the state-of-the-art is given, therefor follow up Section~\ref{emas}. jan@42463: jan@42463: \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} jan@42463: jan@42463: \paragraph{Educational software in mathematics} is, if at all, based on Computer Algebra Systems (CAS, for instance), Dynamic Geometry Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org} \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These base technologies are used to program math lessons and sometimes even exercises. The latter are cumbersome: the steps towards a solution of such an interactive exercise need to be provided with feedback, where at each step a wide variety of possible input has to be foreseen by the programmer - so such interactive exercises either require high development efforts or the exercises constrain possible inputs. jan@42463: jan@42463: \subparagraph{A new generation} of educational math assistants (EMAs) is emerging presently, which is based on Theorem Proving (TP). TP, for instance Isabelle and Coq, is a technology which requires each fact and each action justified by formal logic. Pushed by demands for \textit{proven} correctness of safety-critical software TP advances into software engineering; from these advancements computer mathematics benefits in general, and math education in particular. Two features of TP are immediately beneficial for learning: jan@42463: jan@42463: \paragraph{TP have knowledge in human readable format,} that is in standard predicate calculus. TP following the LCF-tradition have that knowledge down to the basic definitions of set, equality, etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; following the typical deductive development of math, natural numbers are defined and their properties proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, etc. Present knowledge mechanized in TP exceeds high-school mathematics by far, however by knowledge required in software technology, and not in other engineering sciences. jan@42463: jan@42463: \paragraph{TP can model the whole problem solving process} in mathematical problem solving {\em within} a coherent logical framework. This is already being done by three projects, by Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor. jan@42463: \par jan@42463: Having the whole problem solving process within a logical coherent system, such a design guarantees correctness of intermediate steps and of the result (which seems essential for math software); and the second advantage is that TP provides a wealth of theories which can be exploited for mechanizing other features essential for educational software. jan@42463: jan@42463: \subsubsection{Generation of User Guidance in EMAs}\label{user-guid} jan@42463: jan@42463: One essential feature for educational software is feedback to user input and assistance in coming to a solution. jan@42463: jan@42463: \paragraph{Checking user input} by ATP during stepwise problem solving is being accomplished by the three projects mentioned above exclusively. They model the whole problem solving process as mentioned above, so all what happens between formalized assumptions (or formal specification) and goal (or fulfilled postcondition) can be mechanized. Such mechanization promises to greatly extend the scope of educational software in stepwise problem solving. jan@42463: jan@42463: \paragraph{NSG (Next step guidance)} comprises the system's ability to propose a next step; this is a challenge for TP: either a radical restriction of the search space by restriction to very specific problem classes is required, or much care and effort is required in designing possible variants in the process of problem solving \cite{proof-strategies-11}. jan@42463: \par jan@42463: Another approach is restricted to problem solving in engineering domains, where a problem is specified by input, precondition, output and postcondition, and where the postcondition is proven by ATP behind the scenes: Here the possible variants in the process of problem solving are provided with feedback {\em automatically}, if the problem is described in a TP-based programing language: jan@42463: \cite{plmms10} the programmer only describes the math algorithm without caring about interaction (the respective program is functional and even has no input or output statements!); interaction is generated as a side-effect by the interpreter --- an efficient separation of concern between math programmers and dialog designers promising application all over engineering disciplines. jan@42463: jan@42463: jan@42463: \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}} jan@42463: Authoring new mathematics knowledge in {\sisac} can be compared with ``application programing'' of engineering problems; most of such programing uses CAS-based programing languages (CAS = Computer Algebra Systems; e.g. Mathematica's or Maple's programing language). jan@42463: jan@42463: \paragraph{A novel type of TP-based language} is used by {\sisac{}} \cite{plmms10} for describing how to construct a solution to an engineering problem and for calling equation solvers, integration, etc~\footnote{Implementation of CAS-like functionality in TP is not primarily concerned with efficiency, but with a didactic question: What to decide for: for high-brow algorithms at the state-of-the-art or for elementary algorithms comprehensible for students?} within TP; TP can ensure ``systems that never make a mistake'' \cite{casproto} - are impossible for CAS which have no logics underlying. jan@42463: jan@42463: \subparagraph{Authoring is perfect} by writing such TP based programs; the application programmer is not concerned with interaction or with user guidance: this is concern of a novel kind of program interpreter called Lucas-Interpreter. This interpreter hands over control to a dialog component at each step of calculation (like a debugger at breakpoints) and calls automated TP to check user input following personalized strategies according to a feedback module. jan@42463: \par jan@42463: However ``application programing with TP'' is not done with writing a program: according to the principles of TP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is shown in Example~\ref{eg:neuper1}. jan@42463: jan@42463: \vbox{ jan@42463: \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 \\ jan@42463: \>\> rule1: ``1 = $\delta$ [n]'' and\\ jan@42463: \>\> rule2: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z / (z - 1) = u [n]'' and\\ jan@42463: \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\ jan@42463: \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\ 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: \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]'' jan@42463: \end{tabbing} jan@42463: } jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: In order to provide TP with logical facts for checking user input, the Lucas-Interpreter requires a \textbf{specification}. Such a specification is shown in Example~\ref{eg:neuper2}. 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\;\}$ jan@42463: \end{tabbing} jan@42463: } jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: Such a specification is checked before the execution of a program is started, the same applies for sub-programs. In the following example (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])'' \\ jan@42463: ``\>[BOOL equ, REAL z])'' \\ jan@42463: \end{tabbing} jan@42463: } jan@42463: {\small\textit{ jan@42463: \noindent If a program requires a result which has to be calculated first we can use a subproblem to do so. In our specific case we wanted to calculate the zeros of a fraction and used a subproblem to calculate the zeros of the denominator polynom. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: \section{Workflow of Programming in the Prototype}\label{workflow} jan@42463: jan@42463: \subsection{Formalization of missing knowledge in Isabelle} jan@42463: jan@42463: \paragraph{A problem} behind is the mechanization of mathematic theories in TP-bases languages. There is still a huge gap between these algorithms and this what we want as a solution - in Example 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@42463: \noindent A very simple example on this what we call gap is the simplification above. It is needles to say that it is correct and also Isabelle for fills it correct - \emph{always}. But sometimes we don't want expand such terms, sometimes we want another structure of them. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between mechanical simplification and the solution. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: \paragraph{We are not able to fill this gap,} until we have to live with it but first have a look on the meaning of this statement: Mechanized math starts from mathematical models and \emph{hopefully} proceeds to match physics. Academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modeling and formalization. The process from a physical observance to a mathematical theory is unavoidable bound of setting up a big collection of standards, rules, definition but also exceptions. These 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@42463: \noindent Think about some units like that one's above. Behind each unit there is a discerning and very accurate definition: One Meter is the distance the light travels, in a vacuum, through the time of 1 / 299.792.458 second; one kilogram is the weight of a platinum-iridium cylinder in paris; and so on. But are these definitions usable in a computer mechanized world?! jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: \paragraph{A computer} or a TP-System builds on programs with predefined logical rules and does not know any mathematical trick (follow up example \ref{eg:trick}) or recipe to walk around difficult 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@42463: \noindent Sometimes it is also useful to be able to apply some \emph{tricks} to get a beautiful and particularly meaningful result, which we are able to interpret. But as seen in this example it can be hard to find out what operations have to be done to transform a result into a meaningful one. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: \paragraph{The only possibility,} for such a system, is to work through its known definitions and stops if none of these fits. Specified on Signal Processing or any other application it is often possible to walk through by doing simple creases. This creases are in general based on simple math operational but the challenge is to teach the machine \emph{all}\footnote{Its pride to call it \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to reach a high level of \emph{all} but it in real it will still be a survey of knowledge which links to other knowledge and {\sisac{}} a trainer and helper but no human compensating calculator. jan@42463: \par jan@42463: {{\sisac{}}} itself aims to adds an \emph{application} axis (formal specifications of problems out of topics from Signal Processing, etc.) and an \emph{algorithmic} axis to the \emph{deductive} axis of physical knowledge. The result is a three-dimensional universe of 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} jan@42463: \end{figure} jan@42463: jan@42463: \subsection{Notes on Problems with Traditional Notation} jan@42463: jan@42463: \paragraph{During research} on these topic severely problems on traditional notations have been discovered. Some of them have been known in computer science for many years now and are still unsolved, one of them aggregates with the so called \emph{Lambda Calculus}, Example~\ref{eg:lamda} provides a look on the problem that embarrassed 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@42463: \noindent Above we see two equations. The first equation aims to be a mapping of an function from the reel range to the reel one, but when we change only one letter we get the second equation which usually aims to insert a reel point $p$ into the reel function. In computer science now we have the problem to tell the machine (TP) the difference between this two notations. This Problem is called \emph{Lambda Calculus}. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: \paragraph{An other problem} is that terms are not full simplified in traditional notations, in {\sisac} we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in {\sisac} but in tradition we keep fractions as long as possible and as long as they aim to be \textit{beautiful} (1/8, 5/16,...). jan@42463: \subparagraph{The math} which should be mechanized in Computer Theorem Provers (\emph{TP}) has (almost) a problem with traditional notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer program or script is not able to interpret every Greek or Latin letter and every Greek, Latin or whatever calculations symbol. Also if we would be able to handle these symbols we still have a problem to interpret them at all. (Follow up \hbox{Example \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@42463: \noindent The unitstep is something we need to solve Signal Processing problem classes. But in {{\sisac{}}} the rectangular brackets have a different meaning. So we abuse them for our requirements. We get something which is not defined, but usable. The Result is syntax only without semantic. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: In different problems, symbols and letters have different meanings and ask for different ways to get through. (Follow up \hbox{Example \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@42463: \noindent For using exponents the three \texttt{widehat} symbols are required. The reason for that is due the development of {{\sisac{}}} the single \texttt{widehat} and also the double were already in use for different operations. jan@42463: }} jan@42463: \end{example} jan@42463: } jan@42463: jan@42463: \paragraph{Also the output} can be a problem. We are familiar with a specified notations and style taught in university but a computer program has no knowledge of the form proved by a professor and the machines themselves also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a human readable format but according to the fact that there is no money for good working formal editors yet, the style is one thing we have to live with. jan@42463: jan@42463: \section{Problems rising out of the Development Environment} jan@42463: jan@42463: fehlermeldungen! TODO jan@42463: jan@42463: \section{Conclusion} jan@42463: jan@42463: TODO jan@42463: jan@42463: \bibliographystyle{alpha} jan@42463: \bibliography{references} jan@42463: jan@42463: \end{document}