jan@42463
|
1 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
2 |
% Electronic Journal of Mathematics and Technology (eJMT) %
|
jan@42463
|
3 |
% style sheet for LaTeX. Please do not modify sections %
|
jan@42463
|
4 |
% or commands marked 'eJMT'. %
|
jan@42463
|
5 |
% %
|
jan@42463
|
6 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
7 |
% %
|
jan@42463
|
8 |
% eJMT commands %
|
jan@42463
|
9 |
% %
|
jan@42463
|
10 |
\documentclass[12pt,a4paper]{article}% %
|
jan@42463
|
11 |
\usepackage{times} %
|
jan@42463
|
12 |
\usepackage{amsfonts,amsmath,amssymb} %
|
jan@42463
|
13 |
\usepackage[a4paper]{geometry} %
|
jan@42463
|
14 |
\usepackage{fancyhdr} %
|
jan@42463
|
15 |
\usepackage{color} %
|
jan@42463
|
16 |
\usepackage[pdftex]{hyperref} % see note below %
|
jan@42463
|
17 |
\usepackage{graphicx}% %
|
jan@42463
|
18 |
\hypersetup{ %
|
jan@42463
|
19 |
a4paper, %
|
jan@42463
|
20 |
breaklinks %
|
jan@42463
|
21 |
} %
|
jan@42463
|
22 |
% %
|
jan@42463
|
23 |
\newtheorem{theorem}{Theorem} %
|
jan@42463
|
24 |
\newtheorem{acknowledgement}[theorem]{Acknowledgement} %
|
jan@42463
|
25 |
\newtheorem{algorithm}[theorem]{Algorithm} %
|
jan@42463
|
26 |
\newtheorem{axiom}[theorem]{Axiom} %
|
jan@42463
|
27 |
\newtheorem{case}[theorem]{Case} %
|
jan@42463
|
28 |
\newtheorem{claim}[theorem]{Claim} %
|
jan@42463
|
29 |
\newtheorem{conclusion}[theorem]{Conclusion} %
|
jan@42463
|
30 |
\newtheorem{condition}[theorem]{Condition} %
|
jan@42463
|
31 |
\newtheorem{conjecture}[theorem]{Conjecture} %
|
jan@42463
|
32 |
\newtheorem{corollary}[theorem]{Corollary} %
|
jan@42463
|
33 |
\newtheorem{criterion}[theorem]{Criterion} %
|
jan@42463
|
34 |
\newtheorem{definition}[theorem]{Definition} %
|
jan@42463
|
35 |
\newtheorem{example}[theorem]{Example} %
|
jan@42463
|
36 |
\newtheorem{exercise}[theorem]{Exercise} %
|
jan@42463
|
37 |
\newtheorem{lemma}[theorem]{Lemma} %
|
jan@42463
|
38 |
\newtheorem{notation}[theorem]{Notation} %
|
jan@42463
|
39 |
\newtheorem{problem}[theorem]{Problem} %
|
jan@42463
|
40 |
\newtheorem{proposition}[theorem]{Proposition} %
|
jan@42463
|
41 |
\newtheorem{remark}[theorem]{Remark} %
|
jan@42463
|
42 |
\newtheorem{solution}[theorem]{Solution} %
|
jan@42463
|
43 |
\newtheorem{summary}[theorem]{Summary} %
|
jan@42463
|
44 |
\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } %
|
jan@42463
|
45 |
{\ \rule{0.5em}{0.5em}} %
|
jan@42463
|
46 |
% %
|
jan@42463
|
47 |
% eJMT page dimensions %
|
jan@42463
|
48 |
% %
|
jan@42463
|
49 |
\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
|
jan@42463
|
50 |
% %
|
jan@42463
|
51 |
% eJMT header & footer %
|
jan@42463
|
52 |
% %
|
jan@42463
|
53 |
\newcounter{ejmtFirstpage} %
|
jan@42463
|
54 |
\setcounter{ejmtFirstpage}{1} %
|
jan@42463
|
55 |
\pagestyle{empty} %
|
jan@42463
|
56 |
\setlength{\headheight}{14pt} %
|
jan@42463
|
57 |
\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
|
jan@42463
|
58 |
\pagestyle{fancyplain} %
|
jan@42463
|
59 |
\fancyhf{} %
|
jan@42463
|
60 |
\fancyhead[c]{\small The Electronic Journal of Mathematics%
|
jan@42463
|
61 |
\ and Technology, Volume 1, Number 1, ISSN 1933-2823} %
|
jan@42463
|
62 |
\cfoot{% %
|
jan@42463
|
63 |
\ifnum\value{ejmtFirstpage}=0% %
|
jan@42463
|
64 |
{\vtop to\hsize{\hrule\vskip .2cm\thepage}}% %
|
jan@42463
|
65 |
\else\setcounter{ejmtFirstpage}{0}\fi% %
|
jan@42463
|
66 |
} %
|
jan@42463
|
67 |
% %
|
jan@42463
|
68 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
69 |
%
|
jan@42463
|
70 |
% Please place your own definitions here
|
jan@42463
|
71 |
%
|
jan@42463
|
72 |
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
|
jan@42463
|
73 |
\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
|
jan@42463
|
74 |
|
jan@42463
|
75 |
\usepackage{color}
|
jan@42463
|
76 |
\definecolor{lgray}{RGB}{238,238,238}
|
jan@42463
|
77 |
|
jan@42463
|
78 |
%
|
jan@42463
|
79 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
80 |
% %
|
jan@42463
|
81 |
% How to use hyperref %
|
jan@42463
|
82 |
% ------------------- %
|
jan@42463
|
83 |
% %
|
jan@42463
|
84 |
% Probably the only way you will need to use the hyperref %
|
jan@42463
|
85 |
% package is as follows. To make some text, say %
|
jan@42463
|
86 |
% "My Text Link", into a link to the URL %
|
jan@42463
|
87 |
% http://something.somewhere.com/mystuff, use %
|
jan@42463
|
88 |
% %
|
jan@42463
|
89 |
% \href{http://something.somewhere.com/mystuff}{My Text Link}
|
jan@42463
|
90 |
% %
|
jan@42463
|
91 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
92 |
%
|
jan@42463
|
93 |
\begin{document}
|
jan@42463
|
94 |
%
|
jan@42463
|
95 |
% document title
|
jan@42463
|
96 |
%
|
neuper@42464
|
97 |
\title{Trials with TP-based Programming
|
neuper@42464
|
98 |
\\
|
neuper@42464
|
99 |
for Interactive Course Material}%
|
jan@42463
|
100 |
%
|
jan@42463
|
101 |
% Single author. Please supply at least your name,
|
jan@42463
|
102 |
% email address, and affiliation here.
|
jan@42463
|
103 |
%
|
jan@42463
|
104 |
\author{\begin{tabular}{c}
|
jan@42463
|
105 |
\textit{Jan Ro\v{c}nik} \\
|
jan@42463
|
106 |
jan.rocnik@student.tugraz.at \\
|
jan@42463
|
107 |
IST, SPSC\\
|
neuper@42464
|
108 |
Graz University of Technologie\\
|
jan@42463
|
109 |
Austria\end{tabular}
|
jan@42463
|
110 |
}%
|
jan@42463
|
111 |
%
|
jan@42463
|
112 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
113 |
% %
|
jan@42463
|
114 |
% eJMT commands - do not change these %
|
jan@42463
|
115 |
% %
|
jan@42463
|
116 |
\date{} %
|
jan@42463
|
117 |
\maketitle %
|
jan@42463
|
118 |
% %
|
jan@42463
|
119 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
120 |
%
|
jan@42463
|
121 |
% abstract
|
jan@42463
|
122 |
%
|
jan@42463
|
123 |
\begin{abstract}
|
jan@42463
|
124 |
|
jan@42463
|
125 |
Traditional course material in engineering disciplines lacks an
|
jan@42463
|
126 |
important component, interactive support for step-wise problem
|
neuper@42464
|
127 |
solving. Theorem-Proving (TP) technology is appropriate for one part
|
jan@42463
|
128 |
of such support, in checking user-input. For the other part of such
|
jan@42463
|
129 |
support, guiding the learner towards a solution, another kind of
|
jan@42463
|
130 |
technology is required. %TODO ... connect to prototype ...
|
jan@42463
|
131 |
|
jan@42463
|
132 |
A prototype combines TP with a programming language, the latter
|
jan@42463
|
133 |
interpreted in a specific way: certain statements in a program, called
|
jan@42463
|
134 |
tactics, are treated as breakpoints where control is handed over to
|
jan@42463
|
135 |
the user. An input formula is checked by TP (using logical context
|
jan@42463
|
136 |
built up by the interpreter); and if a learner gets stuck, a program
|
jan@42463
|
137 |
describing the steps towards a solution of a problem ``knows the next
|
jan@42463
|
138 |
step''. This kind of interpretation is called Lucas-Interpretation for
|
jan@42463
|
139 |
\emph{TP-based programming languages}.
|
jan@42463
|
140 |
|
jan@42463
|
141 |
This paper describes the prototype's TP-based programming language
|
jan@42463
|
142 |
within a case study creating interactive material for an advanced
|
jan@42463
|
143 |
course in Signal Processing: implementation of definitions and
|
jan@42463
|
144 |
theorems in TP, formal specification of a problem and step-wise
|
jan@42463
|
145 |
development of the program solving the problem. Experiences with the
|
neuper@42464
|
146 |
ork flow in iterative development with testing and identifying errors
|
jan@42463
|
147 |
are described, too. The description clarifies the components missing
|
jan@42463
|
148 |
in the prototype's language as well as deficiencies experienced during
|
jan@42463
|
149 |
programming.
|
jan@42463
|
150 |
\par
|
jan@42463
|
151 |
These experiences are particularly notable, because the author is the
|
jan@42463
|
152 |
first programmer using the language beyond the core team which
|
jan@42463
|
153 |
developed the prototype's TP-based language interpreter.
|
jan@42463
|
154 |
%
|
jan@42463
|
155 |
\end{abstract}%
|
jan@42463
|
156 |
%
|
jan@42463
|
157 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
158 |
% %
|
jan@42463
|
159 |
% eJMT command %
|
jan@42463
|
160 |
% %
|
jan@42463
|
161 |
\thispagestyle{fancy} %
|
jan@42463
|
162 |
% %
|
jan@42463
|
163 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
164 |
%
|
jan@42463
|
165 |
% Please use the following to indicate sections, subsections,
|
jan@42463
|
166 |
% etc. Please also use \subsubsection{...}, \paragraph{...}
|
jan@42463
|
167 |
% and \subparagraph{...} as necessary.
|
jan@42463
|
168 |
%
|
jan@42463
|
169 |
|
neuper@42464
|
170 |
\section{Introduction}\label{intro}
|
jan@42463
|
171 |
|
neuper@42464
|
172 |
% \paragraph{Didactics of mathematics}
|
neuper@42464
|
173 |
%WN: wenn man in einem high-quality paper von 'didactics' spricht,
|
neuper@42464
|
174 |
%WN muss man am state-of-the-art ankn"upfen -- siehe
|
neuper@42464
|
175 |
%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
|
neuper@42464
|
176 |
% faces a specific issue, a gap
|
neuper@42464
|
177 |
% between (1) introduction of math concepts and skills and (2)
|
neuper@42464
|
178 |
% application of these concepts and skills, which usually are separated
|
neuper@42464
|
179 |
% into different units in curricula (for good reasons). For instance,
|
neuper@42464
|
180 |
% (1) teaching partial fraction decomposition is separated from (2)
|
neuper@42464
|
181 |
% application for inverse Z-transform in signal processing.
|
neuper@42464
|
182 |
%
|
neuper@42464
|
183 |
% \par This gap is an obstacle for applying math as an fundamental
|
neuper@42464
|
184 |
% thinking technology in engineering: In (1) motivation is lacking
|
neuper@42464
|
185 |
% because the question ``What is this stuff good for?'' cannot be
|
neuper@42464
|
186 |
% treated sufficiently, and in (2) the ``stuff'' is not available to
|
neuper@42464
|
187 |
% students in higher semesters as widespread experience shows.
|
neuper@42464
|
188 |
%
|
neuper@42464
|
189 |
% \paragraph{Motivation} taken by this didactic issue on the one hand,
|
neuper@42464
|
190 |
% and ongoing research and development on a novel kind of educational
|
neuper@42464
|
191 |
% mathematics assistant at Graz University of
|
neuper@42464
|
192 |
% Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
|
neuper@42464
|
193 |
% scope with this issue on the other hand, several institutes are
|
neuper@42464
|
194 |
% planning to join their expertise: the Institute for Information
|
neuper@42464
|
195 |
% Systems and Computer Media (IICM), the Institute for Software
|
neuper@42464
|
196 |
% Technology (IST), the Institutes for Mathematics, the Institute for
|
neuper@42464
|
197 |
% Signal Processing and Speech Communication (SPSC), the Institute for
|
neuper@42464
|
198 |
% Structural Analysis and the Institute of Electrical Measurement and
|
neuper@42464
|
199 |
% Measurement Signal Processing.
|
neuper@42464
|
200 |
%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
|
neuper@42464
|
201 |
%WN und damit zu verg"anglich.
|
neuper@42464
|
202 |
% \par This thesis is the first attempt to tackle the above mentioned
|
neuper@42464
|
203 |
% issue, it focuses on Telematics, because these specific studies focus
|
neuper@42464
|
204 |
% on mathematics in \emph{STEOP}, the introductory orientation phase in
|
neuper@42464
|
205 |
% Austria. \emph{STEOP} is considered an opportunity to investigate the
|
neuper@42464
|
206 |
% impact of {\sisac}'s prototype on the issue and others.
|
neuper@42464
|
207 |
%
|
neuper@42464
|
208 |
|
neuper@42464
|
209 |
Traditional course material in engineering disciplines lacks an
|
neuper@42464
|
210 |
important component, interactive support for step-wise problem
|
neuper@42464
|
211 |
solving. Theorem-Proving (TP) technology can provide such support by
|
neuper@42464
|
212 |
specific services. An important part of such services is called
|
neuper@42464
|
213 |
``next-step-guidance'', generated by a specific kind of ``TP-based
|
neuper@42464
|
214 |
programming language''. In the
|
neuper@42464
|
215 |
{\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
|
neuper@42464
|
216 |
a language is prototyped in line with~\cite{plmms10} and built upon
|
neuper@42464
|
217 |
the theorem prover
|
neuper@42464
|
218 |
Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
|
neuper@42464
|
219 |
The TP services are coordinated by a specific interpreter for the
|
neuper@42464
|
220 |
programming language, called
|
neuper@42464
|
221 |
Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
|
neuper@42464
|
222 |
interpreter will be briefly re-introduced in order to make the paper
|
neuper@42464
|
223 |
self-contained.
|
jan@42463
|
224 |
|
neuper@42464
|
225 |
\medskip The main part of the paper is an account of first experiences
|
neuper@42464
|
226 |
with programming in this TP-based language. The experience was gained
|
neuper@42464
|
227 |
in a case study by the author. The author was considered an ideal
|
neuper@42464
|
228 |
candidate for this study for the following reasons: as a student in
|
neuper@42464
|
229 |
Telematics (computer science with focus on Signal Processing) he had
|
neuper@42464
|
230 |
general knowledge in programming as well as specific domain knowledge
|
neuper@42464
|
231 |
in Signal Processing; and he was not involved in the development of
|
neuper@42464
|
232 |
{\sisac}'s programming language and interpeter, thus a novice to the
|
neuper@42464
|
233 |
language.
|
jan@42463
|
234 |
|
neuper@42464
|
235 |
The goal of the case study was (1) some TP-based programs for
|
neuper@42464
|
236 |
interactive course material for a specific ``Adavanced Signal
|
neuper@42464
|
237 |
Processing Lab'' in a higher semester, (2) respective program
|
neuper@42464
|
238 |
development with as little advice from the {\sisac}-team and (3) records
|
neuper@42464
|
239 |
and comments for the main steps of development in an Isabelle theory;
|
neuper@42464
|
240 |
this theory should provide guidelines for future programmers. An
|
neuper@42464
|
241 |
excerpt from this theory is the main part of this paper.
|
neuper@42464
|
242 |
|
neuper@42464
|
243 |
\medskip The paper will use the problem in Fig.\ref{fig-interactive} as a
|
jan@42463
|
244 |
running example:
|
jan@42463
|
245 |
\begin{figure} [htb]
|
jan@42463
|
246 |
\begin{center}
|
neuper@42464
|
247 |
\includegraphics[width=120mm]{fig/isac-Ztrans-math.png}
|
jan@42463
|
248 |
\caption{Step-wise problem solving guided by the TP-based program}
|
jan@42463
|
249 |
\label{fig-interactive}
|
jan@42463
|
250 |
\end{center}
|
jan@42463
|
251 |
\end{figure}
|
neuper@42464
|
252 |
The problem is from the domain of Signal Processing and requests to
|
neuper@42464
|
253 |
determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
|
neuper@42464
|
254 |
also shows the beginning of the interactive construction of a solution
|
neuper@42464
|
255 |
for the problem. This construction is done in the right window named
|
neuper@42464
|
256 |
``Worksheet''.
|
neuper@42464
|
257 |
|
neuper@42464
|
258 |
User-interaction on the Worksheet is {\em checked} and {\em guided} by
|
neuper@42464
|
259 |
TP services:
|
neuper@42464
|
260 |
\begin{enumerate}
|
neuper@42464
|
261 |
\item Formulas input by the user are {\em checked} by TP: such a
|
neuper@42464
|
262 |
formula establishes a proof situation --- the prover has to derive the
|
neuper@42464
|
263 |
formula from the logical context. The context is built up from the
|
neuper@42464
|
264 |
formal specification of the problem (here hidden from the user) by the
|
neuper@42464
|
265 |
Lucas-Interpreter.
|
neuper@42464
|
266 |
\item If the user gets stuck, the program developed below in this
|
neuper@42464
|
267 |
paper ``knows the next step'' from behind the scenes. How the latter
|
neuper@42464
|
268 |
TP-service is exploited by dialogue authoring is out of scope of this
|
neuper@42464
|
269 |
paper and can be studied in~\cite{gdaroczy-EP-13}.
|
neuper@42464
|
270 |
\end{enumerate} It should be noted that the programmer using the
|
neuper@42464
|
271 |
TP-based language is not concerned with interaction at all; we will
|
neuper@42464
|
272 |
see that the program contains neither input-statements nor
|
neuper@42464
|
273 |
output-statements. Rather, interaction is handled by services
|
neuper@42464
|
274 |
generated automatically.
|
neuper@42464
|
275 |
|
neuper@42464
|
276 |
\medskip So there is a clear separation of concerns: Dialogues are
|
neuper@42464
|
277 |
adapted by dialogue authors (in Java-based tools), using automatically
|
neuper@42464
|
278 |
generated TP services, while the TP-based program is written by
|
neuper@42464
|
279 |
mathematics experts (in Isabelle/ML). The latter is concern of this
|
neuper@42464
|
280 |
paper.
|
neuper@42464
|
281 |
|
neuper@42464
|
282 |
\medskip The paper is structed as follows: The introduction
|
neuper@42464
|
283 |
\S\ref{intro} is followed by a brief re-introduction of the TP-based
|
neuper@42464
|
284 |
programming language in \S\ref{PL}, which extends the executable
|
neuper@42464
|
285 |
fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
|
neuper@42464
|
286 |
play a specific role in Lucas-Interpretation and in providing the TP
|
neuper@42464
|
287 |
services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes
|
neuper@42464
|
288 |
the main steps in developing the program for the running example:
|
neuper@42464
|
289 |
prepare domain knowledge, implement the formal specification of the
|
neuper@42464
|
290 |
problem, prepare the environment for the program, implement the
|
neuper@42464
|
291 |
program. The workflow of programming, debugging and testing is
|
neuper@42464
|
292 |
described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
|
neuper@42464
|
293 |
give directions identified for future development.
|
neuper@42464
|
294 |
|
jan@42463
|
295 |
|
jan@42463
|
296 |
\section{\isac's Prototype for a Programming Language}\label{PL}
|
jan@42463
|
297 |
The prototype's language extends the executable fragment in the
|
jan@42463
|
298 |
language of the theorem prover
|
jan@42463
|
299 |
Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}
|
jan@42463
|
300 |
by tactics which have a specific role in Lucas-Interpretation.
|
jan@42463
|
301 |
|
jan@42463
|
302 |
\subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
|
jan@42463
|
303 |
The executable fragment consists of data-type and function
|
jan@42463
|
304 |
definitions. It's usability even suggests that fragment for
|
jan@42463
|
305 |
introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
|
jan@42463
|
306 |
whose type system resembles that of functional programming
|
jan@42463
|
307 |
languages. Thus there are
|
jan@42463
|
308 |
\begin{description}
|
jan@42463
|
309 |
\item[base types,] in particular \textit{bool}, the type of truth
|
jan@42463
|
310 |
values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
|
jan@42463
|
311 |
natural, integer and complex numbers respectively in mathematics.
|
jan@42463
|
312 |
\item[type constructors] allow to define arbitrary types, from
|
jan@42463
|
313 |
\textit{set}, \textit{list} to advanced data-structures like
|
jan@42463
|
314 |
\textit{trees}, red-black-trees etc.
|
jan@42463
|
315 |
\item[function types,] denoted by $\Rightarrow$.
|
jan@42463
|
316 |
\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
|
jan@42463
|
317 |
type polymorphism. Isabelle automatically computes the type of each
|
jan@42463
|
318 |
variable in a term by use of Hindley-Milner type inference
|
jan@42463
|
319 |
\cite{pl:hind97,Milner-78}.
|
jan@42463
|
320 |
\end{description}
|
jan@42463
|
321 |
|
jan@42463
|
322 |
\textbf{Terms} are formed as in functional programming by applying
|
jan@42463
|
323 |
functions to arguments. If $f$ is a function of type
|
jan@42463
|
324 |
$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
|
jan@42463
|
325 |
$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
|
jan@42463
|
326 |
has type $\tau$. There are many predefined infix symbols like $+$ and
|
jan@42463
|
327 |
$\leq$ most of which are overloaded for various types.
|
jan@42463
|
328 |
|
jan@42463
|
329 |
HOL also supports some basic constructs from functional programming:
|
jan@42463
|
330 |
{\it\label{isabelle-stmts}
|
jan@42463
|
331 |
\begin{tabbing} 123\=\kill
|
jan@42463
|
332 |
\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
|
jan@42463
|
333 |
\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
|
jan@42463
|
334 |
\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
|
jan@42463
|
335 |
\Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
|
jan@42463
|
336 |
\end{tabbing} }
|
jan@42463
|
337 |
\noindent \textit{The running example's program uses some of these elements
|
jan@42463
|
338 |
(marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt
|
jan@42463
|
339 |
let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for
|
jan@42463
|
340 |
lists and {\tt o} for functional (forward) composition in line
|
jan@42463
|
341 |
$10$. In fact, the whole program is an Isabelle term with specific
|
jan@42463
|
342 |
function constants like {\sc program}, {\sc Substitute} and {\sc
|
jan@42463
|
343 |
Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.}
|
jan@42463
|
344 |
|
jan@42463
|
345 |
% Terms may also contain $\lambda$-abstractions. For example, $\lambda
|
jan@42463
|
346 |
% x. \; x$ is the identity function.
|
jan@42463
|
347 |
|
neuper@42464
|
348 |
\textbf{Formulae} are terms of type \textit{bool}. There are the basic
|
jan@42463
|
349 |
constants \textit{True} and \textit{False} and the usual logical
|
jan@42463
|
350 |
connectives (in decreasing order of precedence): $\neg, \land, \lor,
|
jan@42463
|
351 |
\rightarrow$.
|
jan@42463
|
352 |
|
neuper@42464
|
353 |
\textbf{Equality} is available in the form of the infix function $=$
|
neuper@42464
|
354 |
of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
|
neuper@42464
|
355 |
formulas, where it means ``if and only if''.
|
jan@42463
|
356 |
|
jan@42463
|
357 |
\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
|
jan@42463
|
358 |
P$. Quantifiers lead to non-executable functions, so functions do not
|
jan@42463
|
359 |
always correspond to programs, for instance, if comprising \\$(
|
jan@42463
|
360 |
\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
|
jan@42463
|
361 |
\;)$.
|
jan@42463
|
362 |
|
jan@42463
|
363 |
\subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
|
jan@42463
|
364 |
The prototype extends Isabelle's language by specific statements
|
neuper@42464
|
365 |
called tactics~\footnote{{\sisac}'s tactics are different from
|
jan@42463
|
366 |
Isabelle's tactics: the former concern steps in a calculation, the
|
jan@42463
|
367 |
latter concern proof steps.} and tacticals. For the programmer these
|
jan@42463
|
368 |
statements are functions with the following signatures:
|
jan@42463
|
369 |
|
jan@42463
|
370 |
\begin{description}
|
jan@42463
|
371 |
\item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
|
jan@42463
|
372 |
term} * {\it term}\;{\it list}$:
|
jan@42463
|
373 |
this tactic appplies {\it theorem} to a {\it term} yielding a {\it
|
jan@42463
|
374 |
term} and a {\it term list}, the list are assumptions generated by
|
jan@42463
|
375 |
conditional rewriting. For instance, the {\it theorem}
|
jan@42463
|
376 |
$b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
|
jan@42463
|
377 |
applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
|
jan@42463
|
378 |
$(\frac{2}{3}, [x\not=0])$.
|
jan@42463
|
379 |
|
jan@42463
|
380 |
\item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
|
jan@42463
|
381 |
term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
|
jan@42463
|
382 |
this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
|
jan@42463
|
383 |
a confluent and terminating term rewrite system, in general. If
|
jan@42463
|
384 |
none of the rules ({\it theorem}s) is applicable on interpretation
|
jan@42463
|
385 |
of this tactic, an exception is thrown.
|
jan@42463
|
386 |
|
jan@42463
|
387 |
% \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
|
jan@42463
|
388 |
% theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
|
jan@42463
|
389 |
% list}$:
|
jan@42463
|
390 |
%
|
jan@42463
|
391 |
% \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
|
jan@42463
|
392 |
% ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
|
jan@42463
|
393 |
% list}$:
|
jan@42463
|
394 |
|
jan@42463
|
395 |
\item[Substitute:] ${\it substitution}\Rightarrow{\it
|
jan@42463
|
396 |
term}\Rightarrow{\it term}$:
|
jan@42463
|
397 |
|
jan@42463
|
398 |
\item[Take:] ${\it term}\Rightarrow{\it term}$:
|
jan@42463
|
399 |
this tactic has no effect in the program; but it creates a side-effect
|
jan@42463
|
400 |
by Lucas-Interpretation (see below) and writes {\it term} to the
|
jan@42463
|
401 |
Worksheet.
|
jan@42463
|
402 |
|
jan@42463
|
403 |
\item[Subproblem:] ${\it theory} * {\it specification} * {\it
|
jan@42463
|
404 |
method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
|
jan@42463
|
405 |
this tactic allows to enter a phase of interactive specification
|
jan@42463
|
406 |
of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance,
|
jan@42463
|
407 |
a specific type of equation) and a method (for instance, solving an
|
jan@42463
|
408 |
equation symbolically or numerically).
|
jan@42463
|
409 |
|
jan@42463
|
410 |
\end{description}
|
jan@42463
|
411 |
The tactics play a specific role in
|
jan@42463
|
412 |
Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
|
jan@42463
|
413 |
break-points and control is handed over to the user. The user is free
|
jan@42463
|
414 |
to investigate underlying knowledge, applicable theorems, etc. And
|
jan@42463
|
415 |
the user can proceed constructing a solution by input of a tactic to
|
jan@42463
|
416 |
be applied or by input of a formula; in the latter case the
|
jan@42463
|
417 |
Lucas-Interpreter has built up a logical context (initialised with the
|
jan@42463
|
418 |
precondition of the formal specification) such that Isabelle can
|
jan@42463
|
419 |
derive the formula from this context --- or give feedback, that no
|
jan@42463
|
420 |
derivation can be found.
|
jan@42463
|
421 |
|
jan@42463
|
422 |
\subsection{Tacticals for Control of Interpretation}
|
jan@42463
|
423 |
The flow of control in a program can be determined by {\tt if then else}
|
jan@42463
|
424 |
and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
|
jan@42463
|
425 |
by additional tacticals:
|
jan@42463
|
426 |
\begin{description}
|
jan@42463
|
427 |
\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
|
jan@42463
|
428 |
term}$: iterates over tactics which take a {\it term} as argument as
|
jan@42463
|
429 |
long as a tactic is applicable (for instance, {\it Rewrite\_Set} might
|
jan@42463
|
430 |
not be applicable).
|
jan@42463
|
431 |
|
jan@42463
|
432 |
\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
|
jan@42463
|
433 |
if {\it tactic} is applicable, then it is applied to {\it term},
|
jan@42463
|
434 |
otherwise {\it term} is passed on unchanged.
|
jan@42463
|
435 |
|
jan@42463
|
436 |
\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
jan@42463
|
437 |
term}\Rightarrow{\it term}$:
|
jan@42463
|
438 |
|
jan@42463
|
439 |
|
jan@42463
|
440 |
\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
jan@42463
|
441 |
term}\Rightarrow{\it term}$:
|
jan@42463
|
442 |
|
jan@42463
|
443 |
\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
|
jan@42463
|
444 |
term}\Rightarrow{\it term}$:
|
jan@42463
|
445 |
|
jan@42463
|
446 |
\end{description}
|
jan@42463
|
447 |
|
jan@42463
|
448 |
no input / output --- Lucas-Interpretation
|
jan@42463
|
449 |
|
jan@42463
|
450 |
.\\.\\.\\TODO\\.\\.\\
|
jan@42463
|
451 |
|
neuper@42464
|
452 |
\section{Development of a Program on Trial}\label{trial}
|
neuper@42464
|
453 |
As mentioned above, {\sisac} is an experimental system for a proof of
|
neuper@42464
|
454 |
concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
|
neuper@42464
|
455 |
latter interprets a specific kind of TP-based programming language,
|
neuper@42464
|
456 |
which is as experimental as the whole prototype --- so programming in
|
neuper@42464
|
457 |
this language can be only ``on trial'', presently. However, as a
|
neuper@42464
|
458 |
prototype, the language addresses essentials described below.
|
neuper@42464
|
459 |
|
neuper@42464
|
460 |
\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
|
neuper@42464
|
461 |
|
neuper@42464
|
462 |
%WN was Fachleute unter obigem Titel interessiert findet
|
neuper@42464
|
463 |
%WN unterhalb des auskommentierten Textes.
|
neuper@42464
|
464 |
|
neuper@42464
|
465 |
%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
|
neuper@42464
|
466 |
%WN auf Computer-Mathematiker fokussiert.
|
neuper@42464
|
467 |
% \paragraph{As mentioned in the introduction,} a prototype of an
|
neuper@42464
|
468 |
% educational math assistant called
|
neuper@42464
|
469 |
% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
|
neuper@42464
|
470 |
% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
|
neuper@42464
|
471 |
% the gap between (1) introducation and (2) application of mathematics:
|
neuper@42464
|
472 |
% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
|
neuper@42464
|
473 |
% requires each fact and each action justified by formal logic, so
|
neuper@42464
|
474 |
% {{{\sisac}{}}} makes justifications transparent to students in
|
neuper@42464
|
475 |
% interactive step-wise problem solving. By that way {{\sisac}} already
|
neuper@42464
|
476 |
% can serve both:
|
neuper@42464
|
477 |
% \begin{enumerate}
|
neuper@42464
|
478 |
% \item Introduction of math stuff (in e.g. partial fraction
|
neuper@42464
|
479 |
% decomposition) by stepwise explaining and exercising respective
|
neuper@42464
|
480 |
% symbolic calculations with ``next step guidance (NSG)'' and rigorously
|
neuper@42464
|
481 |
% checking steps freely input by students --- this also in context with
|
neuper@42464
|
482 |
% advanced applications (where the stuff to be taught in higher
|
neuper@42464
|
483 |
% semesters can be skimmed through by NSG), and
|
neuper@42464
|
484 |
% \item Application of math stuff in advanced engineering courses
|
neuper@42464
|
485 |
% (e.g. problems to be solved by inverse Z-transform in a Signal
|
neuper@42464
|
486 |
% Processing Lab) and now without much ado about basic math techniques
|
neuper@42464
|
487 |
% (like partial fraction decomposition): ``next step guidance'' supports
|
neuper@42464
|
488 |
% students in independently (re-)adopting such techniques.
|
neuper@42464
|
489 |
% \end{enumerate}
|
neuper@42464
|
490 |
% Before the question is answers, how {{\sisac}}
|
neuper@42464
|
491 |
% accomplishes this task from a technical point of view, some remarks on
|
neuper@42464
|
492 |
% the state-of-the-art is given, therefor follow up Section~\ref{emas}.
|
neuper@42464
|
493 |
%
|
neuper@42464
|
494 |
% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
|
neuper@42464
|
495 |
%
|
neuper@42464
|
496 |
% \paragraph{Educational software in mathematics} is, if at all, based
|
neuper@42464
|
497 |
% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
|
neuper@42464
|
498 |
% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
|
neuper@42464
|
499 |
% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
|
neuper@42464
|
500 |
% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
|
neuper@42464
|
501 |
% base technologies are used to program math lessons and sometimes even
|
neuper@42464
|
502 |
% exercises. The latter are cumbersome: the steps towards a solution of
|
neuper@42464
|
503 |
% such an interactive exercise need to be provided with feedback, where
|
neuper@42464
|
504 |
% at each step a wide variety of possible input has to be foreseen by
|
neuper@42464
|
505 |
% the programmer - so such interactive exercises either require high
|
neuper@42464
|
506 |
% development efforts or the exercises constrain possible inputs.
|
neuper@42464
|
507 |
%
|
neuper@42464
|
508 |
% \subparagraph{A new generation} of educational math assistants (EMAs)
|
neuper@42464
|
509 |
% is emerging presently, which is based on Theorem Proving (TP). TP, for
|
neuper@42464
|
510 |
% instance Isabelle and Coq, is a technology which requires each fact
|
neuper@42464
|
511 |
% and each action justified by formal logic. Pushed by demands for
|
neuper@42464
|
512 |
% \textit{proven} correctness of safety-critical software TP advances
|
neuper@42464
|
513 |
% into software engineering; from these advancements computer
|
neuper@42464
|
514 |
% mathematics benefits in general, and math education in particular. Two
|
neuper@42464
|
515 |
% features of TP are immediately beneficial for learning:
|
neuper@42464
|
516 |
%
|
neuper@42464
|
517 |
% \paragraph{TP have knowledge in human readable format,} that is in
|
neuper@42464
|
518 |
% standard predicate calculus. TP following the LCF-tradition have that
|
neuper@42464
|
519 |
% knowledge down to the basic definitions of set, equality,
|
neuper@42464
|
520 |
% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
|
neuper@42464
|
521 |
% following the typical deductive development of math, natural numbers
|
neuper@42464
|
522 |
% are defined and their properties
|
neuper@42464
|
523 |
% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
|
neuper@42464
|
524 |
% etc. Present knowledge mechanized in TP exceeds high-school
|
neuper@42464
|
525 |
% mathematics by far, however by knowledge required in software
|
neuper@42464
|
526 |
% technology, and not in other engineering sciences.
|
neuper@42464
|
527 |
%
|
neuper@42464
|
528 |
% \paragraph{TP can model the whole problem solving process} in
|
neuper@42464
|
529 |
% mathematical problem solving {\em within} a coherent logical
|
neuper@42464
|
530 |
% framework. This is already being done by three projects, by
|
neuper@42464
|
531 |
% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
|
neuper@42464
|
532 |
% \par
|
neuper@42464
|
533 |
% Having the whole problem solving process within a logical coherent
|
neuper@42464
|
534 |
% system, such a design guarantees correctness of intermediate steps and
|
neuper@42464
|
535 |
% of the result (which seems essential for math software); and the
|
neuper@42464
|
536 |
% second advantage is that TP provides a wealth of theories which can be
|
neuper@42464
|
537 |
% exploited for mechanizing other features essential for educational
|
neuper@42464
|
538 |
% software.
|
neuper@42464
|
539 |
%
|
neuper@42464
|
540 |
% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
|
neuper@42464
|
541 |
%
|
neuper@42464
|
542 |
% One essential feature for educational software is feedback to user
|
neuper@42464
|
543 |
% input and assistance in coming to a solution.
|
neuper@42464
|
544 |
%
|
neuper@42464
|
545 |
% \paragraph{Checking user input} by ATP during stepwise problem solving
|
neuper@42464
|
546 |
% is being accomplished by the three projects mentioned above
|
neuper@42464
|
547 |
% exclusively. They model the whole problem solving process as mentioned
|
neuper@42464
|
548 |
% above, so all what happens between formalized assumptions (or formal
|
neuper@42464
|
549 |
% specification) and goal (or fulfilled postcondition) can be
|
neuper@42464
|
550 |
% mechanized. Such mechanization promises to greatly extend the scope of
|
neuper@42464
|
551 |
% educational software in stepwise problem solving.
|
neuper@42464
|
552 |
%
|
neuper@42464
|
553 |
% \paragraph{NSG (Next step guidance)} comprises the system's ability to
|
neuper@42464
|
554 |
% propose a next step; this is a challenge for TP: either a radical
|
neuper@42464
|
555 |
% restriction of the search space by restriction to very specific
|
neuper@42464
|
556 |
% problem classes is required, or much care and effort is required in
|
neuper@42464
|
557 |
% designing possible variants in the process of problem solving
|
neuper@42464
|
558 |
% \cite{proof-strategies-11}.
|
neuper@42464
|
559 |
% \par
|
neuper@42464
|
560 |
% Another approach is restricted to problem solving in engineering
|
neuper@42464
|
561 |
% domains, where a problem is specified by input, precondition, output
|
neuper@42464
|
562 |
% and postcondition, and where the postcondition is proven by ATP behind
|
neuper@42464
|
563 |
% the scenes: Here the possible variants in the process of problem
|
neuper@42464
|
564 |
% solving are provided with feedback {\em automatically}, if the problem
|
neuper@42464
|
565 |
% is described in a TP-based programing language: \cite{plmms10} the
|
neuper@42464
|
566 |
% programmer only describes the math algorithm without caring about
|
neuper@42464
|
567 |
% interaction (the respective program is functional and even has no
|
neuper@42464
|
568 |
% input or output statements!); interaction is generated as a
|
neuper@42464
|
569 |
% side-effect by the interpreter --- an efficient separation of concern
|
neuper@42464
|
570 |
% between math programmers and dialog designers promising application
|
neuper@42464
|
571 |
% all over engineering disciplines.
|
neuper@42464
|
572 |
%
|
neuper@42464
|
573 |
%
|
neuper@42464
|
574 |
% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
|
neuper@42464
|
575 |
% Authoring new mathematics knowledge in {{\sisac}} can be compared with
|
neuper@42464
|
576 |
% ``application programing'' of engineering problems; most of such
|
neuper@42464
|
577 |
% programing uses CAS-based programing languages (CAS = Computer Algebra
|
neuper@42464
|
578 |
% Systems; e.g. Mathematica's or Maple's programing language).
|
neuper@42464
|
579 |
%
|
neuper@42464
|
580 |
% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
|
neuper@42464
|
581 |
% \cite{plmms10} for describing how to construct a solution to an
|
neuper@42464
|
582 |
% engineering problem and for calling equation solvers, integration,
|
neuper@42464
|
583 |
% etc~\footnote{Implementation of CAS-like functionality in TP is not
|
neuper@42464
|
584 |
% primarily concerned with efficiency, but with a didactic question:
|
neuper@42464
|
585 |
% What to decide for: for high-brow algorithms at the state-of-the-art
|
neuper@42464
|
586 |
% or for elementary algorithms comprehensible for students?} within TP;
|
neuper@42464
|
587 |
% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
|
neuper@42464
|
588 |
% are impossible for CAS which have no logics underlying.
|
neuper@42464
|
589 |
%
|
neuper@42464
|
590 |
% \subparagraph{Authoring is perfect} by writing such TP based programs;
|
neuper@42464
|
591 |
% the application programmer is not concerned with interaction or with
|
neuper@42464
|
592 |
% user guidance: this is concern of a novel kind of program interpreter
|
neuper@42464
|
593 |
% called Lucas-Interpreter. This interpreter hands over control to a
|
neuper@42464
|
594 |
% dialog component at each step of calculation (like a debugger at
|
neuper@42464
|
595 |
% breakpoints) and calls automated TP to check user input following
|
neuper@42464
|
596 |
% personalized strategies according to a feedback module.
|
neuper@42464
|
597 |
% \par
|
neuper@42464
|
598 |
% However ``application programing with TP'' is not done with writing a
|
neuper@42464
|
599 |
% program: according to the principles of TP, each step must be
|
neuper@42464
|
600 |
% justified. Such justifications are given by theorems. So all steps
|
neuper@42464
|
601 |
% must be related to some theorem, if there is no such theorem it must
|
neuper@42464
|
602 |
% be added to the existing knowledge, which is organized in so-called
|
neuper@42464
|
603 |
% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
|
neuper@42464
|
604 |
% Isabelle comprises a mechanism (called ``axiomatization''), which
|
neuper@42464
|
605 |
% allows to omit proofs. Such a theorem is shown in
|
neuper@42464
|
606 |
% Example~\ref{eg:neuper1}.
|
neuper@42464
|
607 |
|
neuper@42464
|
608 |
The running example, introduced by Fig.\ref{fig-interactive} on
|
neuper@42464
|
609 |
p.\pageref{fig-interactive}, requires to determine the inverse $\cal
|
neuper@42464
|
610 |
Z$-transform for a class of functions. The domain of Signal Processing
|
neuper@42464
|
611 |
is accustomed to specific notation for the resulting functions, which
|
neuper@42464
|
612 |
are absolutely summable and are called TODO: $u[n]$, where $u$ is the
|
neuper@42464
|
613 |
function, $n$ is the argument and the brackets indicate that the
|
neuper@42464
|
614 |
arguments are TODO. Surprisingly, Isabelle accepts the rules for
|
neuper@42464
|
615 |
${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
|
neuper@42464
|
616 |
experts might be particularly surprised, that the brackets do not
|
neuper@42464
|
617 |
cause errors in typing (as lists).}:
|
neuper@42464
|
618 |
%\vbox{
|
neuper@42464
|
619 |
% \begin{example}
|
jan@42463
|
620 |
\label{eg:neuper1}
|
jan@42463
|
621 |
{\small\begin{tabbing}
|
jan@42463
|
622 |
123\=123\=123\=123\=\kill
|
jan@42463
|
623 |
\hfill \\
|
jan@42463
|
624 |
\>axiomatization where \\
|
neuper@42464
|
625 |
\>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
|
neuper@42464
|
626 |
\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
|
neuper@42464
|
627 |
\>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
|
neuper@42464
|
628 |
%TODO
|
neuper@42464
|
629 |
\>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
|
neuper@42464
|
630 |
%TODO
|
jan@42463
|
631 |
\>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
|
jan@42463
|
632 |
%TODO
|
neuper@42464
|
633 |
\>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
|
neuper@42464
|
634 |
%TODO
|
neuper@42464
|
635 |
\end{tabbing}
|
neuper@42464
|
636 |
}
|
neuper@42464
|
637 |
% \end{example}
|
neuper@42464
|
638 |
%}
|
neuper@42464
|
639 |
These 6 rules can be used as conditional rewrite rules, depending on
|
neuper@42464
|
640 |
the respective convergence radius. Satisfaction from notation
|
neuper@42464
|
641 |
contrasts with the word {\em axiomatization}: As TP-based, the
|
neuper@42464
|
642 |
programming language expects these rules as {\em proved} theorems, and
|
neuper@42464
|
643 |
not as axioms implemented in the above brute force manner; otherwise
|
neuper@42464
|
644 |
all the verification efforts envisaged (like proof of the
|
neuper@42464
|
645 |
post-condition, see below) would be meaningless.
|
neuper@42464
|
646 |
|
neuper@42464
|
647 |
Isabelle provides a large body of knowledge, rigorously proven from
|
neuper@42464
|
648 |
the basic axioms of mathematics~\footnote{This way of rigorously
|
neuper@42464
|
649 |
deriving all knowledge from first principles is called the
|
neuper@42464
|
650 |
LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
|
neuper@42464
|
651 |
knowledge can be found in the theoris on Multivariate
|
neuper@42464
|
652 |
Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
|
neuper@42464
|
653 |
building up knowledge such that a proof for the above rules would be
|
neuper@42464
|
654 |
reasonably short and easily comprehensible, still requires lots of
|
neuper@42464
|
655 |
work (and is definitely out of scope of our case study).
|
neuper@42464
|
656 |
|
neuper@42464
|
657 |
\medskip At the state-of-the-art in mechanization of knowledge in
|
neuper@42464
|
658 |
engineering, the process does not stop with the mechanization of
|
neuper@42464
|
659 |
mathematics. Rather, ``Formal Methods''~\cite{TODO-formal-methods}
|
neuper@42464
|
660 |
proceed to formal description of physical items. Signal Processing,
|
neuper@42464
|
661 |
for instance is concerned with physical devices for signal acquisition
|
neuper@42464
|
662 |
and reconstruction, which involve measuring a physical signal, storing
|
neuper@42464
|
663 |
it, and possibly later rebuilding the original signal or an
|
neuper@42464
|
664 |
approximation thereof. For digital systems, this typically includes
|
neuper@42464
|
665 |
sampling and quantization; devices for signal compression, including
|
neuper@42464
|
666 |
audio compression, image compression, and video compression, etc.
|
neuper@42464
|
667 |
``Domain engineering''\cite{db-domain-engineering} is concerned with
|
neuper@42464
|
668 |
{\em specification} of these devices' components and features; this
|
neuper@42464
|
669 |
part in the process of mechanization is only at the beginning.
|
neuper@42464
|
670 |
|
neuper@42464
|
671 |
\medskip TP-based programming, concern of this paper, adds a third
|
neuper@42464
|
672 |
part of mechanisation, providing a third axis of ``algorithmic
|
neuper@42464
|
673 |
knowledge'' in Fig.\ref{fig:mathuni} on p.\pageref{fig:mathuni}.
|
neuper@42464
|
674 |
|
neuper@42464
|
675 |
\begin{figure}
|
neuper@42464
|
676 |
\hfill \\
|
neuper@42464
|
677 |
\begin{center}
|
neuper@42464
|
678 |
\includegraphics{fig/universe}
|
neuper@42464
|
679 |
\caption{Didactic ``Math-Universe''\label{fig:mathuni}}
|
neuper@42464
|
680 |
\end{center}
|
neuper@42464
|
681 |
\end{figure}
|
neuper@42464
|
682 |
%WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
|
neuper@42464
|
683 |
%WN bitte folgende Bezeichnungen nehmen:
|
neuper@42464
|
684 |
%WN
|
neuper@42464
|
685 |
%WN axis 1: Algorithmic Knowledge (Programs)
|
neuper@42464
|
686 |
%WN axis 2: Application-oriented Knowledge (Specifications)
|
neuper@42464
|
687 |
%WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
|
neuper@42464
|
688 |
|
neuper@42464
|
689 |
\subsection{Specification of the Problem}\label{spec}
|
neuper@42464
|
690 |
%WN <--> \chapter 7 der Thesis
|
neuper@42464
|
691 |
%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
|
neuper@42464
|
692 |
In order to provide TP with logical facts for checking user input, the
|
neuper@42464
|
693 |
Lucas-Interpreter requires a \textbf{specification}. Such a
|
neuper@42464
|
694 |
specification is shown in Example~\ref{eg:neuper2}.
|
neuper@42464
|
695 |
|
jan@42463
|
696 |
-------------------------------------------------------------------
|
jan@42463
|
697 |
|
jan@42463
|
698 |
Hier brauchen wir die Spezifikation des 'running example' ...
|
jan@42463
|
699 |
|
jan@42463
|
700 |
\vbox{
|
jan@42463
|
701 |
\begin{example}
|
jan@42463
|
702 |
\label{eg:neuper2}
|
jan@42463
|
703 |
{\small\begin{tabbing}
|
jan@42463
|
704 |
123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
|
jan@42463
|
705 |
\hfill \\
|
jan@42463
|
706 |
Specification no.1:\\
|
jan@42463
|
707 |
%\>input\>: $\{\;r={\it arbitraryFix}\;\}$ \\
|
jan@42463
|
708 |
\>input \>: $\{\;r\;\}$ \\
|
jan@42463
|
709 |
\>precond \>: $0 < r$ \\
|
jan@42463
|
710 |
\>output \>: $\{\;A,\; u,v\;\}$ \\
|
jan@42463
|
711 |
\>postcond \>:{\small $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\
|
jan@42463
|
712 |
\> \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land
|
jan@42463
|
713 |
(\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\
|
jan@42463
|
714 |
\>props\>: $\{\;A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\;\}$
|
neuper@42464
|
715 |
\end{tabbing}
|
neuper@42464
|
716 |
}
|
neuper@42464
|
717 |
\end{example}
|
neuper@42464
|
718 |
}
|
neuper@42464
|
719 |
|
neuper@42464
|
720 |
... und die Implementation in Isac (mit Kommentaren aus dem datatype)
|
neuper@42464
|
721 |
|
jan@42463
|
722 |
%WN das w"urde ich in \sec\label{}
|
jan@42463
|
723 |
Such a specification is checked before the execution of a program is
|
jan@42463
|
724 |
started, the same applies for sub-programs. In the following example
|
jan@42463
|
725 |
(Example~\ref{eg:subprob}) shows the call of such a subproblem:
|
jan@42463
|
726 |
|
jan@42463
|
727 |
\vbox{
|
jan@42463
|
728 |
\begin{example}
|
jan@42463
|
729 |
\label{eg:subprob}
|
jan@42463
|
730 |
\hfill \\
|
jan@42463
|
731 |
{\ttfamily \begin{tabbing}
|
jan@42463
|
732 |
``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
|
jan@42463
|
733 |
``\>\>[linear,univariate,equation,test],'' \\
|
jan@42463
|
734 |
``\>\>[Test,solve\_linear])'' \\
|
neuper@42464
|
735 |
``\>[BOOL equ, REAL z])'' \\
|
neuper@42464
|
736 |
\end{tabbing}
|
neuper@42464
|
737 |
}
|
neuper@42464
|
738 |
{\small\textit{
|
jan@42463
|
739 |
\noindent If a program requires a result which has to be
|
jan@42463
|
740 |
calculated first we can use a subproblem to do so. In our specific
|
jan@42463
|
741 |
case we wanted to calculate the zeros of a fraction and used a
|
neuper@42464
|
742 |
subproblem to calculate the zeros of the denominator polynom.
|
neuper@42464
|
743 |
}}
|
neuper@42464
|
744 |
\end{example}
|
neuper@42464
|
745 |
}
|
neuper@42464
|
746 |
|
neuper@42464
|
747 |
\subsection{Implementation of the Method}\label{meth}
|
neuper@42464
|
748 |
%WN <--> \chapter 7 der Thesis
|
neuper@42464
|
749 |
TODO
|
neuper@42464
|
750 |
\subsection{Preparation of ML-Functions for the Program}\label{funs}
|
neuper@42464
|
751 |
%WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr}
|
neuper@42464
|
752 |
%WN brauchst
|
neuper@42464
|
753 |
TODO
|
jan@42463
|
754 |
\subsection{Implementation of the TP-based Program}\label{progr}
|
neuper@42464
|
755 |
%WN <--> \chapter 8 der Thesis
|
neuper@42464
|
756 |
TODO
|
neuper@42464
|
757 |
|
neuper@42464
|
758 |
\section{Workflow of Programming in the Prototype}\label{workflow}
|
neuper@42464
|
759 |
-------------------------------------------------------------------
|
neuper@42464
|
760 |
|
neuper@42464
|
761 |
``workflow'' heisst: das mache ich zuerst, dann das ...
|
neuper@42464
|
762 |
|
neuper@42464
|
763 |
\subsection{Preparations and Trials}\label{flow-prep}
|
neuper@42464
|
764 |
TODO ... Build\_Inverse\_Z\_Transform.thy !!!
|
neuper@42464
|
765 |
|
neuper@42464
|
766 |
\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
|
neuper@42464
|
767 |
TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
|
neuper@42464
|
768 |
|
neuper@42464
|
769 |
\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
|
neuper@42464
|
770 |
TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
|
neuper@42464
|
771 |
|
neuper@42464
|
772 |
-------------------------------------------------------------------
|
neuper@42464
|
773 |
|
neuper@42464
|
774 |
Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are
|
jan@42463
|
775 |
vermutlich auf andere sections aufzuteilen.
|
jan@42463
|
776 |
|
neuper@42464
|
777 |
-------------------------------------------------------------------
|
neuper@42464
|
778 |
|
neuper@42464
|
779 |
\subsection{Formalization of missing knowledge in Isabelle}
|
neuper@42464
|
780 |
|
jan@42463
|
781 |
\paragraph{A problem} behind is the mechanization of mathematic
|
jan@42463
|
782 |
theories in TP-bases languages. There is still a huge gap between
|
jan@42463
|
783 |
these algorithms and this what we want as a solution - in Example
|
jan@42463
|
784 |
Signal Processing.
|
jan@42463
|
785 |
|
jan@42463
|
786 |
\vbox{
|
jan@42463
|
787 |
\begin{example}
|
jan@42463
|
788 |
\label{eg:gap}
|
neuper@42464
|
789 |
\[
|
neuper@42464
|
790 |
X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
|
neuper@42464
|
791 |
\]
|
neuper@42464
|
792 |
{\small\textit{
|
neuper@42464
|
793 |
\noindent A very simple example on this what we call gap is the
|
neuper@42464
|
794 |
simplification above. It is needles to say that it is correct and also
|
neuper@42464
|
795 |
Isabelle for fills it correct - \emph{always}. But sometimes we don't
|
jan@42463
|
796 |
want expand such terms, sometimes we want another structure of
|
jan@42463
|
797 |
them. Think of a problem were we now would need only the coefficients
|
jan@42463
|
798 |
of $X$ and $Y$. This is what we call the gap between mechanical
|
jan@42463
|
799 |
simplification and the solution.
|
neuper@42464
|
800 |
}}
|
neuper@42464
|
801 |
\end{example}
|
neuper@42464
|
802 |
}
|
neuper@42464
|
803 |
|
neuper@42464
|
804 |
\paragraph{We are not able to fill this gap,} until we have to live
|
neuper@42464
|
805 |
with it but first have a look on the meaning of this statement:
|
neuper@42464
|
806 |
Mechanized math starts from mathematical models and \emph{hopefully}
|
neuper@42464
|
807 |
proceeds to match physics. Academic engineering starts from physics
|
neuper@42464
|
808 |
(experimentation, measurement) and then proceeds to mathematical
|
jan@42463
|
809 |
modeling and formalization. The process from a physical observance to
|
jan@42463
|
810 |
a mathematical theory is unavoidable bound of setting up a big
|
jan@42463
|
811 |
collection of standards, rules, definition but also exceptions. These
|
jan@42463
|
812 |
are the things making mechanization that difficult.
|
jan@42463
|
813 |
|
jan@42463
|
814 |
\vbox{
|
jan@42463
|
815 |
\begin{example}
|
jan@42463
|
816 |
\label{eg:units}
|
neuper@42464
|
817 |
\[
|
neuper@42464
|
818 |
m,\ kg,\ s,\ldots
|
neuper@42464
|
819 |
\]
|
neuper@42464
|
820 |
{\small\textit{
|
neuper@42464
|
821 |
\noindent Think about some units like that one's above. Behind
|
neuper@42464
|
822 |
each unit there is a discerning and very accurate definition: One
|
jan@42463
|
823 |
Meter is the distance the light travels, in a vacuum, through the time
|
jan@42463
|
824 |
of 1 / 299.792.458 second; one kilogram is the weight of a
|
jan@42463
|
825 |
platinum-iridium cylinder in paris; and so on. But are these
|
jan@42463
|
826 |
definitions usable in a computer mechanized world?!
|
neuper@42464
|
827 |
}}
|
neuper@42464
|
828 |
\end{example}
|
neuper@42464
|
829 |
}
|
neuper@42464
|
830 |
|
jan@42463
|
831 |
\paragraph{A computer} or a TP-System builds on programs with
|
jan@42463
|
832 |
predefined logical rules and does not know any mathematical trick
|
jan@42463
|
833 |
(follow up example \ref{eg:trick}) or recipe to walk around difficult
|
jan@42463
|
834 |
expressions.
|
jan@42463
|
835 |
|
jan@42463
|
836 |
\vbox{
|
jan@42463
|
837 |
\begin{example}
|
jan@42463
|
838 |
\label{eg:trick}
|
jan@42463
|
839 |
\[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
|
neuper@42464
|
840 |
\[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
|
neuper@42464
|
841 |
\frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
|
neuper@42464
|
842 |
\[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
|
neuper@42464
|
843 |
{\small\textit{
|
neuper@42464
|
844 |
\noindent Sometimes it is also useful to be able to apply some
|
jan@42463
|
845 |
\emph{tricks} to get a beautiful and particularly meaningful result,
|
jan@42463
|
846 |
which we are able to interpret. But as seen in this example it can be
|
jan@42463
|
847 |
hard to find out what operations have to be done to transform a result
|
jan@42463
|
848 |
into a meaningful one.
|
neuper@42464
|
849 |
}}
|
neuper@42464
|
850 |
\end{example}
|
neuper@42464
|
851 |
}
|
neuper@42464
|
852 |
|
neuper@42464
|
853 |
\paragraph{The only possibility,} for such a system, is to work
|
neuper@42464
|
854 |
through its known definitions and stops if none of these
|
neuper@42464
|
855 |
fits. Specified on Signal Processing or any other application it is
|
neuper@42464
|
856 |
often possible to walk through by doing simple creases. This creases
|
neuper@42464
|
857 |
are in general based on simple math operational but the challenge is
|
neuper@42464
|
858 |
to teach the machine \emph{all}\footnote{Its pride to call it
|
jan@42463
|
859 |
\emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
|
neuper@42464
|
860 |
reach a high level of \emph{all} but it in real it will still be a
|
neuper@42464
|
861 |
survey of knowledge which links to other knowledge and {{\sisac}{}} a
|
neuper@42464
|
862 |
trainer and helper but no human compensating calculator.
|
neuper@42464
|
863 |
\par
|
neuper@42464
|
864 |
{{{\sisac}{}}} itself aims to adds an \emph{application} axis (formal
|
jan@42463
|
865 |
specifications of problems out of topics from Signal Processing, etc.)
|
jan@42463
|
866 |
and an \emph{algorithmic} axis to the \emph{deductive} axis of
|
jan@42463
|
867 |
physical knowledge. The result is a three-dimensional universe of
|
jan@42463
|
868 |
mathematics seen in Figure~\ref{fig:mathuni}.
|
jan@42463
|
869 |
|
jan@42463
|
870 |
\begin{figure}
|
jan@42463
|
871 |
\hfill \\
|
jan@42463
|
872 |
\begin{center}
|
jan@42463
|
873 |
\includegraphics{fig/universe}
|
jan@42463
|
874 |
\caption{Didactic ``Math-Universe''\label{fig:mathuni}}
|
jan@42463
|
875 |
\end{center}
|
neuper@42464
|
876 |
\end{figure}
|
neuper@42464
|
877 |
|
neuper@42464
|
878 |
\subsection{Notes on Problems with Traditional Notation}
|
neuper@42464
|
879 |
|
neuper@42464
|
880 |
\paragraph{During research} on these topic severely problems on
|
neuper@42464
|
881 |
traditional notations have been discovered. Some of them have been
|
jan@42463
|
882 |
known in computer science for many years now and are still unsolved,
|
jan@42463
|
883 |
one of them aggregates with the so called \emph{Lambda Calculus},
|
jan@42463
|
884 |
Example~\ref{eg:lamda} provides a look on the problem that embarrassed
|
jan@42463
|
885 |
us.
|
jan@42463
|
886 |
|
jan@42463
|
887 |
\vbox{
|
jan@42463
|
888 |
\begin{example}
|
jan@42463
|
889 |
\label{eg:lamda}
|
jan@42463
|
890 |
|
jan@42463
|
891 |
\[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
|
jan@42463
|
892 |
|
neuper@42464
|
893 |
|
neuper@42464
|
894 |
\[ f(p)=\ldots\; p \in \quad R \]
|
neuper@42464
|
895 |
|
neuper@42464
|
896 |
{\small\textit{
|
neuper@42464
|
897 |
\noindent Above we see two equations. The first equation aims to
|
neuper@42464
|
898 |
be a mapping of an function from the reel range to the reel one, but
|
neuper@42464
|
899 |
when we change only one letter we get the second equation which
|
jan@42463
|
900 |
usually aims to insert a reel point $p$ into the reel function. In
|
jan@42463
|
901 |
computer science now we have the problem to tell the machine (TP) the
|
jan@42463
|
902 |
difference between this two notations. This Problem is called
|
jan@42463
|
903 |
\emph{Lambda Calculus}.
|
neuper@42464
|
904 |
}}
|
neuper@42464
|
905 |
\end{example}
|
neuper@42464
|
906 |
}
|
neuper@42464
|
907 |
|
neuper@42464
|
908 |
\paragraph{An other problem} is that terms are not full simplified in
|
neuper@42464
|
909 |
traditional notations, in {{\sisac}} we have to simplify them complete
|
neuper@42464
|
910 |
to check weather results are compatible or not. in e.g. the solutions
|
neuper@42464
|
911 |
of an second order linear equation is an rational in {{\sisac}} but in
|
neuper@42464
|
912 |
tradition we keep fractions as long as possible and as long as they
|
neuper@42464
|
913 |
aim to be \textit{beautiful} (1/8, 5/16,...).
|
neuper@42464
|
914 |
\subparagraph{The math} which should be mechanized in Computer Theorem
|
neuper@42464
|
915 |
Provers (\emph{TP}) has (almost) a problem with traditional notations
|
neuper@42464
|
916 |
(predicate calculus) for axioms, definitions, lemmas, theorems as a
|
neuper@42464
|
917 |
computer program or script is not able to interpret every Greek or
|
jan@42463
|
918 |
Latin letter and every Greek, Latin or whatever calculations
|
jan@42463
|
919 |
symbol. Also if we would be able to handle these symbols we still have
|
jan@42463
|
920 |
a problem to interpret them at all. (Follow up \hbox{Example
|
jan@42463
|
921 |
\ref{eg:symbint1}})
|
jan@42463
|
922 |
|
jan@42463
|
923 |
\vbox{
|
jan@42463
|
924 |
\begin{example}
|
jan@42463
|
925 |
\label{eg:symbint1}
|
neuper@42464
|
926 |
\[
|
neuper@42464
|
927 |
u\left[n\right] \ \ldots \ unitstep
|
neuper@42464
|
928 |
\]
|
neuper@42464
|
929 |
{\small\textit{
|
neuper@42464
|
930 |
\noindent The unitstep is something we need to solve Signal
|
jan@42463
|
931 |
Processing problem classes. But in {{{\sisac}{}}} the rectangular
|
jan@42463
|
932 |
brackets have a different meaning. So we abuse them for our
|
jan@42463
|
933 |
requirements. We get something which is not defined, but usable. The
|
jan@42463
|
934 |
Result is syntax only without semantic.
|
neuper@42464
|
935 |
}}
|
neuper@42464
|
936 |
\end{example}
|
neuper@42464
|
937 |
}
|
jan@42463
|
938 |
|
jan@42463
|
939 |
In different problems, symbols and letters have different meanings and
|
jan@42463
|
940 |
ask for different ways to get through. (Follow up \hbox{Example
|
jan@42463
|
941 |
\ref{eg:symbint2}})
|
jan@42463
|
942 |
|
jan@42463
|
943 |
\vbox{
|
jan@42463
|
944 |
\begin{example}
|
jan@42463
|
945 |
\label{eg:symbint2}
|
neuper@42464
|
946 |
\[
|
neuper@42464
|
947 |
\widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
|
neuper@42464
|
948 |
\]
|
neuper@42464
|
949 |
{\small\textit{
|
jan@42463
|
950 |
\noindent For using exponents the three \texttt{widehat} symbols
|
jan@42463
|
951 |
are required. The reason for that is due the development of
|
jan@42463
|
952 |
{{{\sisac}{}}} the single \texttt{widehat} and also the double were
|
jan@42463
|
953 |
already in use for different operations.
|
neuper@42464
|
954 |
}}
|
neuper@42464
|
955 |
\end{example}
|
neuper@42464
|
956 |
}
|
neuper@42464
|
957 |
|
neuper@42464
|
958 |
\paragraph{Also the output} can be a problem. We are familiar with a
|
neuper@42464
|
959 |
specified notations and style taught in university but a computer
|
neuper@42464
|
960 |
program has no knowledge of the form proved by a professor and the
|
neuper@42464
|
961 |
machines themselves also have not yet the possibilities to print every
|
jan@42463
|
962 |
symbol (correct) Recent developments provide proofs in a human
|
jan@42463
|
963 |
readable format but according to the fact that there is no money for
|
jan@42463
|
964 |
good working formal editors yet, the style is one thing we have to
|
jan@42463
|
965 |
live with.
|
jan@42463
|
966 |
|
neuper@42464
|
967 |
\section{Problems rising out of the Development Environment}
|
jan@42463
|
968 |
|
jan@42463
|
969 |
fehlermeldungen! TODO
|
jan@42463
|
970 |
|
jan@42463
|
971 |
\section{Conclusion}\label{conclusion}
|
jan@42463
|
972 |
|
jan@42463
|
973 |
TODO
|
jan@42463
|
974 |
|
neuper@42464
|
975 |
\bibliographystyle{alpha}
|
neuper@42464
|
976 |
\bibliography{references}
|
neuper@42464
|
977 |
|
neuper@42464
|
978 |
\end{document} |