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@48778
|
78 |
\usepackage{hyperref}
|
jan@48778
|
79 |
|
jan@42463
|
80 |
%
|
jan@42463
|
81 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
82 |
% %
|
jan@42463
|
83 |
% How to use hyperref %
|
jan@42463
|
84 |
% ------------------- %
|
jan@42463
|
85 |
% %
|
jan@42463
|
86 |
% Probably the only way you will need to use the hyperref %
|
jan@42463
|
87 |
% package is as follows. To make some text, say %
|
jan@42463
|
88 |
% "My Text Link", into a link to the URL %
|
jan@42463
|
89 |
% http://something.somewhere.com/mystuff, use %
|
jan@42463
|
90 |
% %
|
jan@42463
|
91 |
% \href{http://something.somewhere.com/mystuff}{My Text Link}
|
jan@42463
|
92 |
% %
|
jan@42463
|
93 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
94 |
%
|
jan@42463
|
95 |
\begin{document}
|
jan@42463
|
96 |
%
|
jan@42463
|
97 |
% document title
|
jan@42463
|
98 |
%
|
neuper@42464
|
99 |
\title{Trials with TP-based Programming
|
neuper@42464
|
100 |
\\
|
neuper@42464
|
101 |
for Interactive Course Material}%
|
jan@42463
|
102 |
%
|
jan@42463
|
103 |
% Single author. Please supply at least your name,
|
jan@42463
|
104 |
% email address, and affiliation here.
|
jan@42463
|
105 |
%
|
jan@42463
|
106 |
\author{\begin{tabular}{c}
|
jan@42463
|
107 |
\textit{Jan Ro\v{c}nik} \\
|
jan@42463
|
108 |
jan.rocnik@student.tugraz.at \\
|
jan@42463
|
109 |
IST, SPSC\\
|
neuper@42514
|
110 |
Graz University of Technology\\
|
jan@42463
|
111 |
Austria\end{tabular}
|
jan@42463
|
112 |
}%
|
jan@42463
|
113 |
%
|
jan@42463
|
114 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
115 |
% %
|
jan@42463
|
116 |
% eJMT commands - do not change these %
|
jan@42463
|
117 |
% %
|
jan@42463
|
118 |
\date{} %
|
jan@42463
|
119 |
\maketitle %
|
jan@42463
|
120 |
% %
|
jan@42463
|
121 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
122 |
%
|
jan@42463
|
123 |
% abstract
|
jan@42463
|
124 |
%
|
jan@42463
|
125 |
\begin{abstract}
|
jan@42463
|
126 |
|
jan@42463
|
127 |
Traditional course material in engineering disciplines lacks an
|
jan@42463
|
128 |
important component, interactive support for step-wise problem
|
neuper@42464
|
129 |
solving. Theorem-Proving (TP) technology is appropriate for one part
|
jan@42463
|
130 |
of such support, in checking user-input. For the other part of such
|
jan@42463
|
131 |
support, guiding the learner towards a solution, another kind of
|
neuper@42516
|
132 |
technology is required.
|
jan@42463
|
133 |
|
jan@42511
|
134 |
Both kinds of support can be achieved by so-called
|
neuper@42504
|
135 |
Lucas-Interpretation which combines deduction and computation and, for
|
neuper@42504
|
136 |
the latter, uses a novel kind of programming language. This language
|
neuper@42504
|
137 |
is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
|
neuper@42504
|
138 |
programming language''.
|
jan@42463
|
139 |
|
neuper@42504
|
140 |
This paper is the experience report of the first ``application
|
neuper@42507
|
141 |
programmer'' using this language for creating exercises in step-wise
|
neuper@42507
|
142 |
problem solving for an advanced lab in Signal Processing. The tasks
|
neuper@42507
|
143 |
involved in TP-based programming are described together with the
|
neuper@42507
|
144 |
experience gained from a prototype of the programming language and of
|
neuper@42507
|
145 |
it's interpreter.
|
neuper@42504
|
146 |
|
neuper@42504
|
147 |
The report concludes with a positive proof of concept, states
|
jan@42512
|
148 |
insufficiency usability of the prototype and captures the requirements
|
neuper@42504
|
149 |
for further development of both, the programming language and the
|
neuper@42504
|
150 |
interpreter.
|
jan@42463
|
151 |
%
|
jan@42463
|
152 |
\end{abstract}%
|
jan@42463
|
153 |
%
|
jan@42463
|
154 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
155 |
% %
|
jan@42463
|
156 |
% eJMT command %
|
jan@42463
|
157 |
% %
|
jan@42463
|
158 |
\thispagestyle{fancy} %
|
jan@42463
|
159 |
% %
|
jan@42463
|
160 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
161 |
%
|
jan@42463
|
162 |
% Please use the following to indicate sections, subsections,
|
jan@42463
|
163 |
% etc. Please also use \subsubsection{...}, \paragraph{...}
|
jan@42463
|
164 |
% and \subparagraph{...} as necessary.
|
jan@42463
|
165 |
%
|
jan@42463
|
166 |
|
neuper@42464
|
167 |
\section{Introduction}\label{intro}
|
jan@42463
|
168 |
|
jan@42466
|
169 |
% \paragraph{Didactics of mathematics}
|
jan@42466
|
170 |
%WN: wenn man in einem high-quality paper von 'didactics' spricht,
|
jan@42466
|
171 |
%WN muss man am state-of-the-art ankn"upfen -- siehe
|
jan@42466
|
172 |
%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
|
neuper@42464
|
173 |
% faces a specific issue, a gap
|
neuper@42464
|
174 |
% between (1) introduction of math concepts and skills and (2)
|
neuper@42464
|
175 |
% application of these concepts and skills, which usually are separated
|
neuper@42464
|
176 |
% into different units in curricula (for good reasons). For instance,
|
neuper@42464
|
177 |
% (1) teaching partial fraction decomposition is separated from (2)
|
neuper@42464
|
178 |
% application for inverse Z-transform in signal processing.
|
neuper@42464
|
179 |
%
|
neuper@42464
|
180 |
% \par This gap is an obstacle for applying math as an fundamental
|
neuper@42464
|
181 |
% thinking technology in engineering: In (1) motivation is lacking
|
neuper@42464
|
182 |
% because the question ``What is this stuff good for?'' cannot be
|
neuper@42464
|
183 |
% treated sufficiently, and in (2) the ``stuff'' is not available to
|
neuper@42464
|
184 |
% students in higher semesters as widespread experience shows.
|
neuper@42464
|
185 |
%
|
neuper@42464
|
186 |
% \paragraph{Motivation} taken by this didactic issue on the one hand,
|
neuper@42464
|
187 |
% and ongoing research and development on a novel kind of educational
|
neuper@42464
|
188 |
% mathematics assistant at Graz University of
|
neuper@42464
|
189 |
% Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
|
neuper@42464
|
190 |
% scope with this issue on the other hand, several institutes are
|
neuper@42464
|
191 |
% planning to join their expertise: the Institute for Information
|
neuper@42464
|
192 |
% Systems and Computer Media (IICM), the Institute for Software
|
neuper@42464
|
193 |
% Technology (IST), the Institutes for Mathematics, the Institute for
|
neuper@42464
|
194 |
% Signal Processing and Speech Communication (SPSC), the Institute for
|
neuper@42464
|
195 |
% Structural Analysis and the Institute of Electrical Measurement and
|
neuper@42464
|
196 |
% Measurement Signal Processing.
|
jan@42466
|
197 |
%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
|
jan@42466
|
198 |
%WN und damit zu verg"anglich.
|
neuper@42464
|
199 |
% \par This thesis is the first attempt to tackle the above mentioned
|
neuper@42464
|
200 |
% issue, it focuses on Telematics, because these specific studies focus
|
neuper@42464
|
201 |
% on mathematics in \emph{STEOP}, the introductory orientation phase in
|
neuper@42464
|
202 |
% Austria. \emph{STEOP} is considered an opportunity to investigate the
|
neuper@42464
|
203 |
% impact of {\sisac}'s prototype on the issue and others.
|
neuper@42464
|
204 |
%
|
jan@42466
|
205 |
|
jan@42502
|
206 |
Traditional course material in engineering disciplines lacks an
|
neuper@42464
|
207 |
important component, interactive support for step-wise problem
|
neuper@48772
|
208 |
solving. The lack becomes evident by comparing existing course
|
neuper@48772
|
209 |
material with the sheets collected from written exams (in case solving
|
neuper@48772
|
210 |
engineering problems is {\em not} deteriorated to multiple choice
|
neuper@48772
|
211 |
tests) on the topics addressed by the materials.
|
neuper@48772
|
212 |
Theorem-Proving (TP) technology can provide such support by
|
neuper@42464
|
213 |
specific services. An important part of such services is called
|
neuper@42464
|
214 |
``next-step-guidance'', generated by a specific kind of ``TP-based
|
neuper@42464
|
215 |
programming language''. In the
|
neuper@42464
|
216 |
{\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
|
neuper@42464
|
217 |
a language is prototyped in line with~\cite{plmms10} and built upon
|
jan@48766
|
218 |
the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}
|
jan@48766
|
219 |
\footnote{http://isabelle.in.tum.de/}.
|
neuper@42464
|
220 |
The TP services are coordinated by a specific interpreter for the
|
neuper@42464
|
221 |
programming language, called
|
neuper@48772
|
222 |
Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language
|
neuper@48772
|
223 |
will be briefly re-introduced in order to make the paper
|
neuper@42464
|
224 |
self-contained.
|
jan@42463
|
225 |
|
neuper@42504
|
226 |
The main part of the paper is an account of first experiences
|
neuper@42464
|
227 |
with programming in this TP-based language. The experience was gained
|
neuper@42464
|
228 |
in a case study by the author. The author was considered an ideal
|
neuper@42464
|
229 |
candidate for this study for the following reasons: as a student in
|
neuper@42464
|
230 |
Telematics (computer science with focus on Signal Processing) he had
|
neuper@42464
|
231 |
general knowledge in programming as well as specific domain knowledge
|
neuper@42504
|
232 |
in Signal Processing; and he was {\em not} involved in the development of
|
jan@48766
|
233 |
{\sisac}'s programming language and interpreter, thus being a novice to the
|
neuper@42464
|
234 |
language.
|
jan@42463
|
235 |
|
jan@48766
|
236 |
The goals of the case study were: (1) to identify some TP-based programs for
|
jan@42511
|
237 |
interactive course material for a specific ``Advanced Signal
|
neuper@42464
|
238 |
Processing Lab'' in a higher semester, (2) respective program
|
jan@48766
|
239 |
development with as little advice as possible from the {\sisac}-team and (3)
|
jan@48766
|
240 |
to document records and comments for the main steps of development in an
|
jan@48766
|
241 |
Isabelle theory; this theory should provide guidelines for future programmers.
|
jan@48766
|
242 |
An excerpt from this theory is the main part of this paper.
|
jan@42466
|
243 |
\par
|
neuper@48771
|
244 |
|
neuper@48771
|
245 |
\medskip The major example resulting from the case study will be used
|
neuper@48771
|
246 |
as running example throughout this paper. This example requires a
|
neuper@48771
|
247 |
program resembling the size of real-world applications in engineering;
|
neuper@48771
|
248 |
such a size was considered essential for the case study, since there
|
neuper@48771
|
249 |
are many small programs for a long time (mainly concerned with
|
neuper@48771
|
250 |
elementary Computer Algebra like simplification, equation solving,
|
neuper@48771
|
251 |
calculus, etc.~\footnote{The programs existing in the {\sisac}
|
neuper@48771
|
252 |
prototype are found at
|
neuper@48771
|
253 |
http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})
|
neuper@48771
|
254 |
|
neuper@48771
|
255 |
\paragraph{The mathematical background of the running example} is the
|
jan@48774
|
256 |
following: In Signal Processing, ``the ${\cal Z}$-transform for
|
neuper@48771
|
257 |
discrete-time signals is the counterpart of the Laplace transform for
|
neuper@48771
|
258 |
continuous-time signals, and they each have a similar relationship to
|
neuper@48771
|
259 |
the corresponding Fourier transform. One motivation for introducing
|
neuper@48771
|
260 |
this generalization is that the Fourier transform does not converge
|
neuper@48771
|
261 |
for all sequences, and it is useful to have a generalization of the
|
neuper@48771
|
262 |
Fourier transform that encompasses a broader class of signals. A
|
jan@48774
|
263 |
second advantage is that in analytic problems, the ${\cal Z}$-transform
|
neuper@48771
|
264 |
notation is often more convenient than the Fourier transform
|
jan@48774
|
265 |
notation.'' ~\cite[p. 128]{oppenheim2010discrete}. The ${\cal Z}$-transform
|
neuper@48771
|
266 |
is defined as
|
neuper@48771
|
267 |
\begin{equation*}
|
neuper@48771
|
268 |
X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}
|
neuper@48771
|
269 |
\end{equation*}
|
neuper@48771
|
270 |
where a discrete time sequence $x[n]$ is transformed into the function
|
neuper@48771
|
271 |
$X(z)$ where $z$ is a continuous complex variable. The inverse
|
neuper@48771
|
272 |
function is addressed in the running example and can be determined by
|
neuper@48771
|
273 |
the integral
|
neuper@48771
|
274 |
\begin{equation*}
|
neuper@48771
|
275 |
x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz
|
neuper@48771
|
276 |
\end{equation*}
|
neuper@48771
|
277 |
where the letter $C$ represents a contour within the range of
|
jan@48774
|
278 |
convergence of the ${\cal Z}$-transform. The unit circle can be a special
|
neuper@48771
|
279 |
case of this contour. Remember that $j$ is the complex number in the
|
jan@48774
|
280 |
domain of engineering. As this transform requires high effort to
|
neuper@48771
|
281 |
be solved, tables of commonly used transform pairs are used in
|
neuper@48771
|
282 |
education as well as in engineering practice; such tables can be found
|
neuper@48771
|
283 |
at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.
|
neuper@48771
|
284 |
A completely solved and more detailed example can be found at
|
neuper@48771
|
285 |
~\cite[p. 149f]{oppenheim2010discrete}.
|
neuper@48771
|
286 |
|
neuper@48771
|
287 |
Following conventions in engineering education and in practice, the
|
neuper@48771
|
288 |
running example solves the problem by use of a table.
|
neuper@48771
|
289 |
|
neuper@48771
|
290 |
\paragraph{Support for interactive stepwise problem solving} in the
|
neuper@48771
|
291 |
{\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,
|
neuper@48771
|
292 |
the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:
|
neuper@48771
|
293 |
A student inputs formulas line by line on the \textit{``Worksheet''},
|
neuper@48771
|
294 |
and each step (i.e. each formula on completion) is immediately checked
|
neuper@48775
|
295 |
by the system, such that at most {\em one inconsistent} formula can reside on
|
neuper@48771
|
296 |
the Worksheet (on the input line, marked by the red $\otimes$).
|
jan@42463
|
297 |
\begin{figure} [htb]
|
jan@42463
|
298 |
\begin{center}
|
neuper@42468
|
299 |
\includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
|
neuper@42468
|
300 |
%\includegraphics[width=140mm]{fig/isac-Ztrans-math}
|
jan@42512
|
301 |
\caption{Step-wise problem solving guided by the TP-based program
|
jan@42512
|
302 |
\label{fig-interactive}}
|
jan@42463
|
303 |
\end{center}
|
jan@42463
|
304 |
\end{figure}
|
neuper@48772
|
305 |
If the student gets stuck and does not know the formula to proceed
|
neuper@48772
|
306 |
with, there is the button \framebox{NEXT} presenting the next formula
|
neuper@48777
|
307 |
on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the
|
neuper@48772
|
308 |
final result in case the student is not interested in intermediate
|
neuper@48772
|
309 |
steps.
|
jan@42466
|
310 |
|
neuper@48771
|
311 |
Adaptive dialogue guidance is already under
|
neuper@48771
|
312 |
construction~\cite{gdaroczy-EP-13} and the two buttons will disappear,
|
neuper@48771
|
313 |
since their presence is not wanted in many learning scenarios (in
|
neuper@48771
|
314 |
particular, {\em not} in written exams).
|
jan@48767
|
315 |
|
neuper@48771
|
316 |
The buttons \framebox{Theories}, \framebox{Problems} and
|
neuper@48771
|
317 |
\framebox{Methods} are the entry points for interactive lookup of the
|
neuper@48771
|
318 |
underlying knowledge. For instance, pushing \framebox{Theories} in
|
neuper@48771
|
319 |
the configuration shown in Fig.\ref{fig-interactive}, pops up a
|
neuper@48771
|
320 |
``Theory browser'' displaying the theorem(s) justifying the current
|
neuper@48772
|
321 |
step. The browser allows to lookup all other theories, thus
|
neuper@48771
|
322 |
supporting indepentend investigation of underlying definitions,
|
neuper@48771
|
323 |
theorems, proofs --- where the HTML representation of the browsers is
|
neuper@48772
|
324 |
ready for arbitrary multimedia add-ons. Likewise, the browsers for
|
neuper@48772
|
325 |
\framebox{Problems} and \framebox{Methods} support context sensitive
|
neuper@48772
|
326 |
as well as interactive access to specifications and programs
|
neuper@48772
|
327 |
respectively.
|
neuper@48772
|
328 |
|
neuper@48772
|
329 |
There is also a simple web-based representation of knowledge items;
|
neuper@48772
|
330 |
the items under consideration in this paper can be looked up as
|
jan@48778
|
331 |
well
|
jan@48778
|
332 |
~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Inverse\_Z\_Transform.thy}}}
|
jan@48778
|
333 |
~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Partial\_Fractions.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Partial\_Fractions.thy}}}
|
jan@48778
|
334 |
~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Build\_Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Build\_Inverse\_Z\_Transform.thy}}}.
|
jan@48767
|
335 |
|
neuper@48771
|
336 |
% can be explained by having a look at
|
neuper@48771
|
337 |
% Fig.\ref{fig-interactive} which shows the beginning of the interactive
|
neuper@48771
|
338 |
% construction of a solution for the problem. This construction is done in the
|
neuper@48771
|
339 |
% right window named ``Worksheet''.
|
neuper@48771
|
340 |
% \par
|
neuper@48771
|
341 |
% User-interaction on the Worksheet is {\em checked} and {\em guided} by
|
neuper@48771
|
342 |
% TP services:
|
neuper@48771
|
343 |
% \begin{enumerate}
|
neuper@48771
|
344 |
% \item Formulas input by the user are {\em checked} by TP: such a
|
neuper@48771
|
345 |
% formula establishes a proof situation --- the prover has to derive the
|
neuper@48771
|
346 |
% formula from the logical context. The context is built up from the
|
neuper@48771
|
347 |
% formal specification of the problem (here hidden from the user) by the
|
neuper@48771
|
348 |
% Lucas-Interpreter.
|
neuper@48771
|
349 |
% \item If the user gets stuck, the program developed below in this
|
neuper@48771
|
350 |
% paper ``knows the next step'' and Lucas-Interpretation provides services
|
neuper@48771
|
351 |
% featuring so-called ``next-step-guidance''; this is out of scope of this
|
neuper@48771
|
352 |
% paper and can be studied in~\cite{gdaroczy-EP-13}.
|
neuper@48771
|
353 |
% \end{enumerate} It should be noted that the programmer using the
|
neuper@48771
|
354 |
% TP-based language is not concerned with interaction at all; we will
|
neuper@48771
|
355 |
% see that the program contains neither input-statements nor
|
neuper@48771
|
356 |
% output-statements. Rather, interaction is handled by the interpreter
|
neuper@48771
|
357 |
% of the language.
|
neuper@48771
|
358 |
%
|
neuper@48771
|
359 |
% So there is a clear separation of concerns: Dialogues are adapted by
|
neuper@48771
|
360 |
% dialogue authors (in Java-based tools), using TP services provided by
|
neuper@48771
|
361 |
% Lucas-Interpretation. The latter acts on programs developed by
|
neuper@48771
|
362 |
% mathematics-authors (in Isabelle/ML); their task is concern of this
|
neuper@48771
|
363 |
% paper.
|
jan@48767
|
364 |
|
neuper@48771
|
365 |
\bigskip The paper is structured as follows: The introduction
|
neuper@42464
|
366 |
\S\ref{intro} is followed by a brief re-introduction of the TP-based
|
neuper@42464
|
367 |
programming language in \S\ref{PL}, which extends the executable
|
neuper@42464
|
368 |
fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
|
neuper@42464
|
369 |
play a specific role in Lucas-Interpretation and in providing the TP
|
neuper@42504
|
370 |
services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
|
neuper@42464
|
371 |
the main steps in developing the program for the running example:
|
neuper@42464
|
372 |
prepare domain knowledge, implement the formal specification of the
|
neuper@42504
|
373 |
problem, prepare the environment for the interpreter, implement the
|
neuper@42504
|
374 |
program in \S\ref{isabisac} to \S\ref{progr} respectively.
|
jan@42511
|
375 |
The work-flow of programming, debugging and testing is
|
neuper@42464
|
376 |
described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
|
neuper@42464
|
377 |
give directions identified for future development.
|
neuper@42464
|
378 |
|
jan@42463
|
379 |
|
jan@42463
|
380 |
\section{\isac's Prototype for a Programming Language}\label{PL}
|
jan@48768
|
381 |
The prototype of the language and of the Lucas-Interpreter is briefly
|
neuper@42504
|
382 |
described from the point of view of a programmer. The language extends
|
neuper@48771
|
383 |
the executable fragment of Higher-Order Logic (HOL) in the theorem prover
|
neuper@42504
|
384 |
Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
|
jan@42463
|
385 |
|
jan@42463
|
386 |
\subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
|
jan@42463
|
387 |
The executable fragment consists of data-type and function
|
jan@42463
|
388 |
definitions. It's usability even suggests that fragment for
|
neuper@48771
|
389 |
introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming
|
jan@42463
|
390 |
languages. Thus there are
|
jan@42463
|
391 |
\begin{description}
|
jan@42463
|
392 |
\item[base types,] in particular \textit{bool}, the type of truth
|
jan@42463
|
393 |
values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
|
jan@42463
|
394 |
natural, integer and complex numbers respectively in mathematics.
|
jan@42463
|
395 |
\item[type constructors] allow to define arbitrary types, from
|
jan@42463
|
396 |
\textit{set}, \textit{list} to advanced data-structures like
|
jan@42463
|
397 |
\textit{trees}, red-black-trees etc.
|
jan@42463
|
398 |
\item[function types,] denoted by $\Rightarrow$.
|
jan@42463
|
399 |
\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
|
jan@42463
|
400 |
type polymorphism. Isabelle automatically computes the type of each
|
jan@42463
|
401 |
variable in a term by use of Hindley-Milner type inference
|
jan@42463
|
402 |
\cite{pl:hind97,Milner-78}.
|
jan@42463
|
403 |
\end{description}
|
jan@42463
|
404 |
|
jan@42463
|
405 |
\textbf{Terms} are formed as in functional programming by applying
|
jan@42463
|
406 |
functions to arguments. If $f$ is a function of type
|
jan@42463
|
407 |
$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
|
jan@42463
|
408 |
$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
|
jan@42463
|
409 |
has type $\tau$. There are many predefined infix symbols like $+$ and
|
jan@42463
|
410 |
$\leq$ most of which are overloaded for various types.
|
jan@42463
|
411 |
|
jan@42463
|
412 |
HOL also supports some basic constructs from functional programming:
|
jan@42512
|
413 |
{\footnotesize\it\label{isabelle-stmts}
|
jan@42463
|
414 |
\begin{tabbing} 123\=\kill
|
jan@42513
|
415 |
01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
|
jan@42513
|
416 |
02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
|
jan@42513
|
417 |
03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
|
jan@42463
|
418 |
\Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
|
jan@42512
|
419 |
\end{tabbing}}
|
neuper@42482
|
420 |
\noindent The running example's program uses some of these elements
|
neuper@42482
|
421 |
(marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
|
neuper@42482
|
422 |
let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
|
neuper@42482
|
423 |
is an Isabelle term with specific function constants like {\tt
|
neuper@42482
|
424 |
program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
|
neuper@42482
|
425 |
Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
|
neuper@42482
|
426 |
respectively.
|
jan@42463
|
427 |
|
jan@42463
|
428 |
% Terms may also contain $\lambda$-abstractions. For example, $\lambda
|
jan@42463
|
429 |
% x. \; x$ is the identity function.
|
jan@42463
|
430 |
|
neuper@42467
|
431 |
%JR warum auskommentiert? WN2...
|
neuper@42467
|
432 |
%WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
|
neuper@42467
|
433 |
%WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
|
neuper@42467
|
434 |
%WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
|
neuper@42467
|
435 |
%WN2 gel"oscht.
|
neuper@42467
|
436 |
%WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
|
neuper@42467
|
437 |
%WN2 Platz f"ur Anderes weg.
|
jan@42466
|
438 |
|
neuper@42464
|
439 |
\textbf{Formulae} are terms of type \textit{bool}. There are the basic
|
jan@42463
|
440 |
constants \textit{True} and \textit{False} and the usual logical
|
jan@42463
|
441 |
connectives (in decreasing order of precedence): $\neg, \land, \lor,
|
jan@42463
|
442 |
\rightarrow$.
|
jan@42463
|
443 |
|
neuper@42464
|
444 |
\textbf{Equality} is available in the form of the infix function $=$
|
neuper@42464
|
445 |
of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
|
neuper@42464
|
446 |
formulas, where it means ``if and only if''.
|
jan@42463
|
447 |
|
jan@42463
|
448 |
\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
|
jan@42463
|
449 |
P$. Quantifiers lead to non-executable functions, so functions do not
|
jan@42463
|
450 |
always correspond to programs, for instance, if comprising \\$(
|
jan@42463
|
451 |
\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
|
jan@42463
|
452 |
\;)$.
|
jan@42463
|
453 |
|
jan@42463
|
454 |
\subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
|
jan@42463
|
455 |
The prototype extends Isabelle's language by specific statements
|
neuper@48775
|
456 |
called tactics~\footnote{{\sisac}'s. These tactics are different from
|
jan@42463
|
457 |
Isabelle's tactics: the former concern steps in a calculation, the
|
neuper@48775
|
458 |
latter concern proofs.}. For the programmer these
|
jan@42463
|
459 |
statements are functions with the following signatures:
|
jan@42463
|
460 |
|
jan@42463
|
461 |
\begin{description}
|
jan@42463
|
462 |
\item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
|
jan@42463
|
463 |
term} * {\it term}\;{\it list}$:
|
jan@42511
|
464 |
this tactic applies {\it theorem} to a {\it term} yielding a {\it
|
jan@42463
|
465 |
term} and a {\it term list}, the list are assumptions generated by
|
jan@42463
|
466 |
conditional rewriting. For instance, the {\it theorem}
|
jan@42463
|
467 |
$b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
|
jan@42463
|
468 |
applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
|
jan@42463
|
469 |
$(\frac{2}{3}, [x\not=0])$.
|
jan@42463
|
470 |
|
jan@42463
|
471 |
\item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
|
jan@42463
|
472 |
term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
|
jan@42511
|
473 |
this tactic applies {\it ruleset} to a {\it term}; {\it ruleset} is
|
jan@42463
|
474 |
a confluent and terminating term rewrite system, in general. If
|
jan@42463
|
475 |
none of the rules ({\it theorem}s) is applicable on interpretation
|
jan@42463
|
476 |
of this tactic, an exception is thrown.
|
jan@42463
|
477 |
|
jan@42463
|
478 |
% \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
|
jan@42463
|
479 |
% theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
|
jan@42463
|
480 |
% list}$:
|
jan@42463
|
481 |
%
|
jan@42463
|
482 |
% \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
|
jan@42463
|
483 |
% ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
|
jan@42463
|
484 |
% list}$:
|
jan@42463
|
485 |
|
neuper@42504
|
486 |
%SPACEvvv
|
jan@42463
|
487 |
\item[Substitute:] ${\it substitution}\Rightarrow{\it
|
neuper@42482
|
488 |
term}\Rightarrow{\it term}$: allows to access sub-terms.
|
neuper@42504
|
489 |
%SPACE^^^
|
jan@42463
|
490 |
|
jan@42463
|
491 |
\item[Take:] ${\it term}\Rightarrow{\it term}$:
|
jan@42463
|
492 |
this tactic has no effect in the program; but it creates a side-effect
|
jan@42463
|
493 |
by Lucas-Interpretation (see below) and writes {\it term} to the
|
jan@42463
|
494 |
Worksheet.
|
jan@42463
|
495 |
|
jan@42463
|
496 |
\item[Subproblem:] ${\it theory} * {\it specification} * {\it
|
jan@42463
|
497 |
method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
|
neuper@42482
|
498 |
this tactic is a generalisation of a function call: it takes an
|
neuper@42482
|
499 |
\textit{argument list} as usual, and additionally a triple consisting
|
neuper@42482
|
500 |
of an Isabelle \textit{theory}, an implicit \textit{specification} of the
|
neuper@42482
|
501 |
program and a \textit{method} containing data for Lucas-Interpretation,
|
neuper@42482
|
502 |
last not least a program (as an explicit specification)~\footnote{In
|
neuper@42482
|
503 |
interactive tutoring these three items can be determined explicitly
|
neuper@42482
|
504 |
by the user.}.
|
jan@42463
|
505 |
\end{description}
|
jan@42463
|
506 |
The tactics play a specific role in
|
jan@42463
|
507 |
Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
|
neuper@42482
|
508 |
break-points where, as a side-effect, a line is added to a calculation
|
neuper@42483
|
509 |
as a protocol for proceeding towards a solution in step-wise problem
|
neuper@42483
|
510 |
solving. At the same points Lucas-Interpretation serves interactive
|
neuper@42504
|
511 |
tutoring and hands over control to the user. The user is free to
|
neuper@42483
|
512 |
investigate underlying knowledge, applicable theorems, etc. And the
|
neuper@42483
|
513 |
user can proceed constructing a solution by input of a tactic to be
|
neuper@42483
|
514 |
applied or by input of a formula; in the latter case the
|
jan@42463
|
515 |
Lucas-Interpreter has built up a logical context (initialised with the
|
jan@42463
|
516 |
precondition of the formal specification) such that Isabelle can
|
jan@42463
|
517 |
derive the formula from this context --- or give feedback, that no
|
jan@42463
|
518 |
derivation can be found.
|
jan@42463
|
519 |
|
jan@42511
|
520 |
\subsection{Tactics as Control Flow Statements}
|
jan@42463
|
521 |
The flow of control in a program can be determined by {\tt if then else}
|
jan@42463
|
522 |
and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
|
jan@42511
|
523 |
by additional tactics:
|
jan@42463
|
524 |
\begin{description}
|
jan@42463
|
525 |
\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
|
jan@42463
|
526 |
term}$: iterates over tactics which take a {\it term} as argument as
|
neuper@42482
|
527 |
long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
|
jan@42463
|
528 |
not be applicable).
|
jan@42463
|
529 |
|
jan@42463
|
530 |
\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
|
jan@42463
|
531 |
if {\it tactic} is applicable, then it is applied to {\it term},
|
neuper@42483
|
532 |
otherwise {\it term} is passed on without changes.
|
jan@42463
|
533 |
|
jan@42463
|
534 |
\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
neuper@42483
|
535 |
term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
|
neuper@42483
|
536 |
it is applied to the first {\it term} yielding another {\it term},
|
neuper@42483
|
537 |
otherwise the second {\it tactic} is applied; if none is applicable an
|
neuper@42483
|
538 |
exception is raised.
|
jan@42463
|
539 |
|
jan@42463
|
540 |
\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
neuper@42483
|
541 |
term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
|
neuper@42483
|
542 |
first {\it term} yielding an intermediate term (not appearing in the
|
neuper@42483
|
543 |
signature) to which the second {\it tactic} is applied.
|
jan@42463
|
544 |
|
jan@42463
|
545 |
\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
|
neuper@42483
|
546 |
term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
|
neuper@42483
|
547 |
{\it tactic} is applied to the first {\it term} yielding an
|
neuper@42483
|
548 |
intermediate term (not appearing in the signature); the intermediate
|
neuper@42483
|
549 |
term is added to the environment the first {\it term} is evaluated in
|
jan@42511
|
550 |
etc. as long as the first {\it term} is true.
|
jan@42463
|
551 |
\end{description}
|
jan@42511
|
552 |
The tactics are not treated as break-points by Lucas-Interpretation
|
neuper@42504
|
553 |
and thus do neither contribute to the calculation nor to interaction.
|
jan@42463
|
554 |
|
neuper@42498
|
555 |
\section{Concepts and Tasks in TP-based Programming}\label{trial}
|
neuper@42498
|
556 |
%\section{Development of a Program on Trial}
|
neuper@42498
|
557 |
|
neuper@42498
|
558 |
This section presents all the concepts involved in TP-based
|
neuper@42498
|
559 |
programming and all the tasks to be accomplished by programmers. The
|
neuper@42504
|
560 |
presentation uses the running example from
|
neuper@42498
|
561 |
Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
|
jan@42466
|
562 |
|
jan@42466
|
563 |
\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
|
jan@42466
|
564 |
|
neuper@42467
|
565 |
%WN was Fachleute unter obigem Titel interessiert findet sich
|
jan@42466
|
566 |
%WN unterhalb des auskommentierten Textes.
|
jan@42466
|
567 |
|
jan@42466
|
568 |
%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
|
jan@42466
|
569 |
%WN auf Computer-Mathematiker fokussiert.
|
neuper@42464
|
570 |
% \paragraph{As mentioned in the introduction,} a prototype of an
|
neuper@42464
|
571 |
% educational math assistant called
|
neuper@42464
|
572 |
% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
|
neuper@42464
|
573 |
% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
|
neuper@42464
|
574 |
% the gap between (1) introducation and (2) application of mathematics:
|
neuper@42464
|
575 |
% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
|
neuper@42464
|
576 |
% requires each fact and each action justified by formal logic, so
|
neuper@42464
|
577 |
% {{{\sisac}{}}} makes justifications transparent to students in
|
neuper@42464
|
578 |
% interactive step-wise problem solving. By that way {{\sisac}} already
|
neuper@42464
|
579 |
% can serve both:
|
neuper@42464
|
580 |
% \begin{enumerate}
|
neuper@42464
|
581 |
% \item Introduction of math stuff (in e.g. partial fraction
|
neuper@42464
|
582 |
% decomposition) by stepwise explaining and exercising respective
|
neuper@42464
|
583 |
% symbolic calculations with ``next step guidance (NSG)'' and rigorously
|
neuper@42464
|
584 |
% checking steps freely input by students --- this also in context with
|
neuper@42464
|
585 |
% advanced applications (where the stuff to be taught in higher
|
neuper@42464
|
586 |
% semesters can be skimmed through by NSG), and
|
neuper@42464
|
587 |
% \item Application of math stuff in advanced engineering courses
|
neuper@42464
|
588 |
% (e.g. problems to be solved by inverse Z-transform in a Signal
|
neuper@42464
|
589 |
% Processing Lab) and now without much ado about basic math techniques
|
neuper@42464
|
590 |
% (like partial fraction decomposition): ``next step guidance'' supports
|
neuper@42464
|
591 |
% students in independently (re-)adopting such techniques.
|
neuper@42464
|
592 |
% \end{enumerate}
|
neuper@42464
|
593 |
% Before the question is answers, how {{\sisac}}
|
neuper@42464
|
594 |
% accomplishes this task from a technical point of view, some remarks on
|
neuper@42464
|
595 |
% the state-of-the-art is given, therefor follow up Section~\ref{emas}.
|
neuper@42464
|
596 |
%
|
neuper@42464
|
597 |
% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
|
neuper@42464
|
598 |
%
|
jan@42466
|
599 |
% \paragraph{Educational software in mathematics} is, if at all, based
|
jan@42466
|
600 |
% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
|
jan@42466
|
601 |
% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
|
jan@42466
|
602 |
% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
|
jan@42466
|
603 |
% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
|
jan@42466
|
604 |
% base technologies are used to program math lessons and sometimes even
|
jan@42466
|
605 |
% exercises. The latter are cumbersome: the steps towards a solution of
|
jan@42466
|
606 |
% such an interactive exercise need to be provided with feedback, where
|
jan@42466
|
607 |
% at each step a wide variety of possible input has to be foreseen by
|
jan@42466
|
608 |
% the programmer - so such interactive exercises either require high
|
neuper@42464
|
609 |
% development efforts or the exercises constrain possible inputs.
|
neuper@42464
|
610 |
%
|
jan@42466
|
611 |
% \subparagraph{A new generation} of educational math assistants (EMAs)
|
jan@42466
|
612 |
% is emerging presently, which is based on Theorem Proving (TP). TP, for
|
jan@42466
|
613 |
% instance Isabelle and Coq, is a technology which requires each fact
|
jan@42466
|
614 |
% and each action justified by formal logic. Pushed by demands for
|
jan@42466
|
615 |
% \textit{proven} correctness of safety-critical software TP advances
|
jan@42466
|
616 |
% into software engineering; from these advancements computer
|
jan@42466
|
617 |
% mathematics benefits in general, and math education in particular. Two
|
neuper@42464
|
618 |
% features of TP are immediately beneficial for learning:
|
neuper@42464
|
619 |
%
|
jan@42466
|
620 |
% \paragraph{TP have knowledge in human readable format,} that is in
|
jan@42466
|
621 |
% standard predicate calculus. TP following the LCF-tradition have that
|
jan@42466
|
622 |
% knowledge down to the basic definitions of set, equality,
|
jan@42466
|
623 |
% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
|
jan@42466
|
624 |
% following the typical deductive development of math, natural numbers
|
jan@42466
|
625 |
% are defined and their properties
|
jan@42466
|
626 |
% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
|
jan@42466
|
627 |
% etc. Present knowledge mechanized in TP exceeds high-school
|
jan@42466
|
628 |
% mathematics by far, however by knowledge required in software
|
neuper@42464
|
629 |
% technology, and not in other engineering sciences.
|
neuper@42464
|
630 |
%
|
jan@42466
|
631 |
% \paragraph{TP can model the whole problem solving process} in
|
jan@42466
|
632 |
% mathematical problem solving {\em within} a coherent logical
|
jan@42466
|
633 |
% framework. This is already being done by three projects, by
|
neuper@42464
|
634 |
% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
|
neuper@42464
|
635 |
% \par
|
jan@42466
|
636 |
% Having the whole problem solving process within a logical coherent
|
jan@42466
|
637 |
% system, such a design guarantees correctness of intermediate steps and
|
jan@42466
|
638 |
% of the result (which seems essential for math software); and the
|
jan@42466
|
639 |
% second advantage is that TP provides a wealth of theories which can be
|
jan@42466
|
640 |
% exploited for mechanizing other features essential for educational
|
neuper@42464
|
641 |
% software.
|
neuper@42464
|
642 |
%
|
neuper@42464
|
643 |
% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
|
neuper@42464
|
644 |
%
|
jan@42466
|
645 |
% One essential feature for educational software is feedback to user
|
neuper@42464
|
646 |
% input and assistance in coming to a solution.
|
neuper@42464
|
647 |
%
|
jan@42466
|
648 |
% \paragraph{Checking user input} by ATP during stepwise problem solving
|
jan@42466
|
649 |
% is being accomplished by the three projects mentioned above
|
jan@42466
|
650 |
% exclusively. They model the whole problem solving process as mentioned
|
jan@42466
|
651 |
% above, so all what happens between formalized assumptions (or formal
|
jan@42466
|
652 |
% specification) and goal (or fulfilled postcondition) can be
|
jan@42466
|
653 |
% mechanized. Such mechanization promises to greatly extend the scope of
|
neuper@42464
|
654 |
% educational software in stepwise problem solving.
|
neuper@42464
|
655 |
%
|
jan@42466
|
656 |
% \paragraph{NSG (Next step guidance)} comprises the system's ability to
|
jan@42466
|
657 |
% propose a next step; this is a challenge for TP: either a radical
|
jan@42466
|
658 |
% restriction of the search space by restriction to very specific
|
jan@42466
|
659 |
% problem classes is required, or much care and effort is required in
|
jan@42466
|
660 |
% designing possible variants in the process of problem solving
|
neuper@42464
|
661 |
% \cite{proof-strategies-11}.
|
neuper@42464
|
662 |
% \par
|
jan@42466
|
663 |
% Another approach is restricted to problem solving in engineering
|
jan@42466
|
664 |
% domains, where a problem is specified by input, precondition, output
|
jan@42466
|
665 |
% and postcondition, and where the postcondition is proven by ATP behind
|
jan@42466
|
666 |
% the scenes: Here the possible variants in the process of problem
|
jan@42466
|
667 |
% solving are provided with feedback {\em automatically}, if the problem
|
jan@42466
|
668 |
% is described in a TP-based programing language: \cite{plmms10} the
|
jan@42466
|
669 |
% programmer only describes the math algorithm without caring about
|
jan@42466
|
670 |
% interaction (the respective program is functional and even has no
|
jan@42466
|
671 |
% input or output statements!); interaction is generated as a
|
jan@42466
|
672 |
% side-effect by the interpreter --- an efficient separation of concern
|
jan@42466
|
673 |
% between math programmers and dialog designers promising application
|
neuper@42464
|
674 |
% all over engineering disciplines.
|
neuper@42464
|
675 |
%
|
neuper@42464
|
676 |
%
|
neuper@42464
|
677 |
% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
|
jan@42466
|
678 |
% Authoring new mathematics knowledge in {{\sisac}} can be compared with
|
jan@42466
|
679 |
% ``application programing'' of engineering problems; most of such
|
jan@42466
|
680 |
% programing uses CAS-based programing languages (CAS = Computer Algebra
|
neuper@42464
|
681 |
% Systems; e.g. Mathematica's or Maple's programing language).
|
neuper@42464
|
682 |
%
|
jan@42466
|
683 |
% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
|
jan@42466
|
684 |
% \cite{plmms10} for describing how to construct a solution to an
|
jan@42466
|
685 |
% engineering problem and for calling equation solvers, integration,
|
jan@42466
|
686 |
% etc~\footnote{Implementation of CAS-like functionality in TP is not
|
jan@42466
|
687 |
% primarily concerned with efficiency, but with a didactic question:
|
jan@42466
|
688 |
% What to decide for: for high-brow algorithms at the state-of-the-art
|
jan@42466
|
689 |
% or for elementary algorithms comprehensible for students?} within TP;
|
jan@42466
|
690 |
% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
|
neuper@42464
|
691 |
% are impossible for CAS which have no logics underlying.
|
neuper@42464
|
692 |
%
|
jan@42466
|
693 |
% \subparagraph{Authoring is perfect} by writing such TP based programs;
|
jan@42466
|
694 |
% the application programmer is not concerned with interaction or with
|
jan@42466
|
695 |
% user guidance: this is concern of a novel kind of program interpreter
|
jan@42466
|
696 |
% called Lucas-Interpreter. This interpreter hands over control to a
|
jan@42466
|
697 |
% dialog component at each step of calculation (like a debugger at
|
jan@42466
|
698 |
% breakpoints) and calls automated TP to check user input following
|
neuper@42464
|
699 |
% personalized strategies according to a feedback module.
|
neuper@42464
|
700 |
% \par
|
jan@42466
|
701 |
% However ``application programing with TP'' is not done with writing a
|
jan@42466
|
702 |
% program: according to the principles of TP, each step must be
|
jan@42466
|
703 |
% justified. Such justifications are given by theorems. So all steps
|
jan@42466
|
704 |
% must be related to some theorem, if there is no such theorem it must
|
jan@42466
|
705 |
% be added to the existing knowledge, which is organized in so-called
|
jan@42466
|
706 |
% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
|
jan@42466
|
707 |
% Isabelle comprises a mechanism (called ``axiomatization''), which
|
jan@42466
|
708 |
% allows to omit proofs. Such a theorem is shown in
|
neuper@42464
|
709 |
% Example~\ref{eg:neuper1}.
|
jan@42466
|
710 |
|
jan@48774
|
711 |
The running example requires to determine the inverse ${\cal Z}$-transform
|
jan@48774
|
712 |
for a class of functions. The domain of Signal Processing
|
jan@42466
|
713 |
is accustomed to specific notation for the resulting functions, which
|
jan@42511
|
714 |
are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
|
jan@42466
|
715 |
function, $n$ is the argument and the brackets indicate that the
|
neuper@42504
|
716 |
arguments are discrete. Surprisingly, Isabelle accepts the rules for
|
jan@42513
|
717 |
$z^{-1}$ in this traditional notation~\footnote{Isabelle
|
jan@42466
|
718 |
experts might be particularly surprised, that the brackets do not
|
jan@42466
|
719 |
cause errors in typing (as lists).}:
|
neuper@42464
|
720 |
%\vbox{
|
neuper@42464
|
721 |
% \begin{example}
|
jan@42463
|
722 |
\label{eg:neuper1}
|
jan@42509
|
723 |
{\footnotesize\begin{tabbing}
|
jan@42463
|
724 |
123\=123\=123\=123\=\kill
|
jan@42509
|
725 |
|
jan@42513
|
726 |
01\>axiomatization where \\
|
jan@42513
|
727 |
02\>\> rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\
|
jan@42513
|
728 |
03\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\
|
jan@42513
|
729 |
04\>\> rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\
|
jan@42513
|
730 |
05\>\> rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\
|
jan@42513
|
731 |
06\>\> rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\
|
jan@42513
|
732 |
07\>\> rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''
|
jan@42509
|
733 |
\end{tabbing}}
|
neuper@42464
|
734 |
% \end{example}
|
jan@42466
|
735 |
%}
|
jan@42466
|
736 |
These 6 rules can be used as conditional rewrite rules, depending on
|
jan@48774
|
737 |
the respective convergence radius. Satisfaction from accordance with traditional
|
jan@48774
|
738 |
notation contrasts with the above word {\em axiomatization}: As TP-based, the
|
jan@42466
|
739 |
programming language expects these rules as {\em proved} theorems, and
|
jan@42466
|
740 |
not as axioms implemented in the above brute force manner; otherwise
|
jan@42466
|
741 |
all the verification efforts envisaged (like proof of the
|
jan@42466
|
742 |
post-condition, see below) would be meaningless.
|
jan@42466
|
743 |
|
neuper@42514
|
744 |
Isabelle provides a large body of knowledge, rigorously proved from
|
jan@42466
|
745 |
the basic axioms of mathematics~\footnote{This way of rigorously
|
jan@42466
|
746 |
deriving all knowledge from first principles is called the
|
jan@48774
|
747 |
LCF-paradigm in TP.}. In the case of the ${\cal Z}$-transform the most advanced
|
jan@42511
|
748 |
knowledge can be found in the theories on Multivariate
|
jan@42466
|
749 |
Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
|
jan@42466
|
750 |
building up knowledge such that a proof for the above rules would be
|
jan@42466
|
751 |
reasonably short and easily comprehensible, still requires lots of
|
jan@42466
|
752 |
work (and is definitely out of scope of our case study).
|
jan@42466
|
753 |
|
neuper@42508
|
754 |
%REMOVED DUE TO SPACE CONSTRAINTS
|
neuper@42508
|
755 |
%At the state-of-the-art in mechanization of knowledge in engineering
|
neuper@42508
|
756 |
%sciences, the process does not stop with the mechanization of
|
neuper@42508
|
757 |
%mathematics traditionally used in these sciences. Rather, ``Formal
|
neuper@42508
|
758 |
%Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
|
neuper@42508
|
759 |
%description of physical items. Signal Processing, for instance is
|
neuper@42508
|
760 |
%concerned with physical devices for signal acquisition and
|
neuper@42508
|
761 |
%reconstruction, which involve measuring a physical signal, storing it,
|
neuper@42508
|
762 |
%and possibly later rebuilding the original signal or an approximation
|
neuper@42508
|
763 |
%thereof. For digital systems, this typically includes sampling and
|
neuper@42508
|
764 |
%quantization; devices for signal compression, including audio
|
neuper@42508
|
765 |
%compression, image compression, and video compression, etc. ``Domain
|
neuper@42508
|
766 |
%engineering''\cite{db:dom-eng} is concerned with {\em specification}
|
neuper@42508
|
767 |
%of these devices' components and features; this part in the process of
|
neuper@42508
|
768 |
%mechanization is only at the beginning in domains like Signal
|
neuper@42508
|
769 |
%Processing.
|
neuper@42508
|
770 |
%
|
neuper@42508
|
771 |
%TP-based programming, concern of this paper, is determined to
|
neuper@42508
|
772 |
%add ``algorithmic knowledge'' to the mechanised body of knowledge.
|
neuper@42508
|
773 |
%% in Fig.\ref{fig:mathuni} on
|
neuper@42508
|
774 |
%% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
|
neuper@42508
|
775 |
%% starts with a formal {\em specification} of the problem to be solved.
|
neuper@42508
|
776 |
%% \begin{figure}
|
neuper@42508
|
777 |
%% \begin{center}
|
neuper@42508
|
778 |
%% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
|
neuper@42508
|
779 |
%% \caption{The three-dimensional universe of mathematics knowledge}
|
neuper@42508
|
780 |
%% \label{fig:mathuni}
|
neuper@42508
|
781 |
%% \end{center}
|
neuper@42508
|
782 |
%% \end{figure}
|
neuper@42508
|
783 |
%% The language for both axes is defined in the axis at the bottom, deductive
|
neuper@42508
|
784 |
%% knowledge, in {\sisac} represented by Isabelle's theories.
|
jan@42466
|
785 |
|
jan@42466
|
786 |
\subsection{Preparation of Simplifiers for the Program}\label{simp}
|
jan@42469
|
787 |
|
jan@42511
|
788 |
All evaluation in the prototype's Lucas-Interpreter is done by term rewriting on
|
neuper@42507
|
789 |
Isabelle's terms, see \S\ref{meth} below; in this section some of respective
|
jan@42505
|
790 |
preparations are described. In order to work reliably with term rewriting, the
|
jan@42505
|
791 |
respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
|
jan@42505
|
792 |
then they are called (canonical) simplifiers. These properties do not go without
|
jan@42505
|
793 |
saying, their establishment is a difficult task for the programmer; this task is
|
neuper@42508
|
794 |
not yet supported in the prototype.
|
jan@42505
|
795 |
|
jan@42505
|
796 |
The prototype rewrites using theorems only. Axioms which are theorems as well
|
jan@42505
|
797 |
have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
|
jan@42512
|
798 |
assemble them in a rule-set and apply them in ML as follows:
|
jan@42505
|
799 |
|
neuper@42508
|
800 |
{\footnotesize
|
neuper@42508
|
801 |
\begin{verbatim}
|
jan@42512
|
802 |
01 val inverse_z = Rls
|
jan@42512
|
803 |
02 {id = "inverse_z",
|
jan@42512
|
804 |
03 rew_ord = dummy_ord,
|
jan@42512
|
805 |
04 erls = Erls,
|
jan@42512
|
806 |
05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
|
jan@42512
|
807 |
06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
|
jan@42512
|
808 |
07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
|
jan@42512
|
809 |
08 errpatts = [],
|
jan@42512
|
810 |
09 scr = ""}
|
neuper@42508
|
811 |
\end{verbatim}}
|
jan@42505
|
812 |
|
neuper@42508
|
813 |
\noindent The items, line by line, in the above record have the following purpose:
|
neuper@42508
|
814 |
\begin{description}
|
jan@42512
|
815 |
\item[01..02] the ML-value \textit{inverse\_z} stores it's identifier
|
neuper@42508
|
816 |
as a string for ``reflection'' when switching between the language
|
neuper@42508
|
817 |
layers of Isabelle/ML (like in the Lucas-Interpreter) and
|
neuper@42508
|
818 |
Isabelle/Isar (like in the example program on p.\pageref{s:impl} on
|
neuper@42508
|
819 |
line {\rm 12}).
|
jan@42475
|
820 |
|
jan@42512
|
821 |
\item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
|
neuper@42508
|
822 |
\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
|
neuper@42508
|
823 |
(a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
|
neuper@42508
|
824 |
and (b) the assumptions of the \textit{rules} need not be evaluated
|
neuper@42508
|
825 |
(they just go into the context during rewriting).
|
jan@42505
|
826 |
|
jan@42512
|
827 |
\item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
|
neuper@42508
|
828 |
also ML-functions (\S\ref{funs}) can come into this list as shown in
|
neuper@42508
|
829 |
\S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm}
|
neuper@42508
|
830 |
and \textit{Calc} respectively; for the purpose of reflection both
|
neuper@42508
|
831 |
contain their identifiers.
|
jan@42502
|
832 |
|
jan@42512
|
833 |
\item[08..09] are error-patterns not discussed here and \textit{scr}
|
neuper@42508
|
834 |
is prepared to get a program, automatically generated by {\sisac} for
|
neuper@42508
|
835 |
producing intermediate rewrites when requested by the user.
|
jan@42502
|
836 |
|
neuper@42508
|
837 |
\end{description}
|
jan@42505
|
838 |
|
neuper@42514
|
839 |
%OUTCOMMENTED DUE TO SPACE RESTRICTIONS
|
neuper@42514
|
840 |
% \noindent It is advisable to immediately test rule-sets; for that
|
neuper@42514
|
841 |
% purpose an appropriate term has to be created; \textit{parse} takes a
|
neuper@42514
|
842 |
% context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
|
neuper@42514
|
843 |
% Z}^{-1}$) and creates a term:
|
neuper@42514
|
844 |
%
|
neuper@42514
|
845 |
% {\footnotesize
|
neuper@42514
|
846 |
% \begin{verbatim}
|
neuper@42514
|
847 |
% 01 ML {*
|
neuper@42514
|
848 |
% 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
|
neuper@42514
|
849 |
% 03 *}
|
neuper@42514
|
850 |
% 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1",
|
neuper@42514
|
851 |
% 05 "RealDef.real => RealDef.real => RealDef.real") $
|
neuper@42514
|
852 |
% 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...)
|
neuper@42514
|
853 |
% \end{verbatim}}
|
neuper@42514
|
854 |
%
|
neuper@42514
|
855 |
% \noindent The internal representation of the term, as required for
|
neuper@42514
|
856 |
% rewriting, consists of \textit{Const}ants, a pair of a string
|
neuper@42514
|
857 |
% \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
|
neuper@42514
|
858 |
% \textit{Free} and the respective constructor \textit{\$}. Now the
|
neuper@42514
|
859 |
% term can be rewritten by the rule-set \textit{inverse\_z}:
|
neuper@42514
|
860 |
%
|
neuper@42514
|
861 |
% {\footnotesize
|
neuper@42514
|
862 |
% \begin{verbatim}
|
neuper@42514
|
863 |
% 01 ML {*
|
neuper@42514
|
864 |
% 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
|
neuper@42514
|
865 |
% 03 term2str t';
|
neuper@42514
|
866 |
% 04 terms2str asm;
|
neuper@42514
|
867 |
% 05 *}
|
neuper@42514
|
868 |
% 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
|
neuper@42514
|
869 |
% 07 val it = "|| z || > 1 & || z || > </alpha>" : string
|
neuper@42514
|
870 |
% \end{verbatim}}
|
neuper@42514
|
871 |
%
|
neuper@42514
|
872 |
% \noindent The resulting term \textit{t} and the assumptions
|
neuper@42514
|
873 |
% \textit{asm} are converted to readable strings by \textit{term2str}
|
neuper@42514
|
874 |
% and \textit{terms2str}.
|
jan@42505
|
875 |
|
jan@42466
|
876 |
\subsection{Preparation of ML-Functions}\label{funs}
|
neuper@42504
|
877 |
Some functionality required in programming, cannot be accomplished by
|
neuper@42504
|
878 |
rewriting. So the prototype has a mechanism to call functions within
|
neuper@42514
|
879 |
the rewrite-engine: certain redexes in Isabelle terms call these
|
neuper@42504
|
880 |
functions written in SML~\cite{pl:milner97}, the implementation {\em
|
neuper@42504
|
881 |
and} meta-language of Isabelle. The programmer has to use this
|
neuper@42504
|
882 |
mechanism.
|
jan@42469
|
883 |
|
neuper@42498
|
884 |
In the running example's program on p.\pageref{s:impl} the lines {\rm
|
neuper@42498
|
885 |
05} and {\rm 06} contain such functions; we go into the details with
|
neuper@42498
|
886 |
\textit{argument\_in X\_z;}. This function fetches the argument from a
|
neuper@42498
|
887 |
function application: Line {\rm 03} in the example calculation on
|
neuper@42498
|
888 |
p.\pageref{exp-calc} is created by line {\rm 06} of the example
|
neuper@42498
|
889 |
program on p.\pageref{s:impl} where the program's environment assigns
|
neuper@42498
|
890 |
the value \textit{X z} to the variable \textit{X\_z}; so the function
|
neuper@42498
|
891 |
shall extract the argument \textit{z}.
|
jan@42469
|
892 |
|
neuper@42498
|
893 |
\medskip In order to be recognised as a function constant in the
|
neuper@42499
|
894 |
program source the constant needs to be declared in a theory, here in
|
neuper@42498
|
895 |
\textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
|
neuper@42498
|
896 |
the context \textit{ctxt} of that theory:
|
neuper@42504
|
897 |
|
neuper@42498
|
898 |
{\footnotesize
|
neuper@42498
|
899 |
\begin{verbatim}
|
jan@42513
|
900 |
01 consts
|
jan@42513
|
901 |
02 argument'_in :: "real => real" ("argument'_in _" 10)
|
neuper@42507
|
902 |
\end{verbatim}}
|
neuper@42498
|
903 |
|
neuper@42507
|
904 |
%^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
|
neuper@42507
|
905 |
%^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real โ RealDef.real")
|
neuper@42507
|
906 |
%^3.2^ $ (Free ("X", "RealDef.real โ RealDef.real") $ Free ("z", "RealDef.real")): term
|
neuper@42507
|
907 |
%^3.2^ \end{verbatim}}
|
neuper@42507
|
908 |
%^3.2^
|
neuper@42507
|
909 |
%^3.2^ \noindent Parsing produces a term \texttt{t} in internal
|
neuper@42507
|
910 |
%^3.2^ representation~\footnote{The attentive reader realizes the
|
neuper@42507
|
911 |
%^3.2^ differences between interal and extermal representation even in the
|
neuper@42507
|
912 |
%^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
|
neuper@42507
|
913 |
%^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
|
neuper@42507
|
914 |
%^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
|
neuper@42507
|
915 |
%^3.2^ constructor.
|
neuper@42507
|
916 |
The function body below is implemented directly in SML,
|
neuper@42499
|
917 |
i.e in an \texttt{ML \{* *\}} block; the function definition provides
|
neuper@42499
|
918 |
a unique prefix \texttt{eval\_} to the function name:
|
jan@42473
|
919 |
|
neuper@42498
|
920 |
{\footnotesize
|
jan@42470
|
921 |
\begin{verbatim}
|
jan@42513
|
922 |
01 ML {*
|
jan@42513
|
923 |
02 fun eval_argument_in _
|
jan@42513
|
924 |
03 "Build_Inverse_Z_Transform.argument'_in"
|
jan@42513
|
925 |
04 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
|
jan@42513
|
926 |
05 if is_Free arg (*could be something to be simplified before*)
|
jan@42513
|
927 |
06 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
|
jan@42513
|
928 |
07 else NONE
|
jan@42513
|
929 |
08 | eval_argument_in _ _ _ _ = NONE;
|
jan@42513
|
930 |
09 *}
|
neuper@42498
|
931 |
\end{verbatim}}
|
jan@42469
|
932 |
|
jan@48766
|
933 |
\noindent The function body creates either \texttt{NONE}
|
neuper@42514
|
934 |
telling the rewrite-engine to search for the next redex, or creates an
|
neuper@42498
|
935 |
ad-hoc theorem for rewriting, thus the programmer needs to adopt many
|
neuper@42498
|
936 |
technicalities of Isabelle, for instance, the \textit{Trueprop}
|
neuper@42498
|
937 |
constant.
|
jan@42469
|
938 |
|
neuper@42498
|
939 |
\bigskip This sub-task particularly sheds light on basic issues in the
|
jan@42511
|
940 |
design of a programming language, the integration of differential language
|
neuper@42498
|
941 |
layers, the layer of Isabelle/Isar and Isabelle/ML.
|
jan@42469
|
942 |
|
neuper@42498
|
943 |
Another point of improvement for the prototype is the rewrite-engine: The
|
neuper@42498
|
944 |
program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
|
neuper@42498
|
945 |
and {\rm 06} to
|
jan@42469
|
946 |
|
neuper@42498
|
947 |
{\small\it\label{s:impl}
|
neuper@42498
|
948 |
\begin{tabbing}
|
neuper@42498
|
949 |
123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
|
jan@42512
|
950 |
\>{\rm 05/06}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
|
neuper@42498
|
951 |
\end{tabbing}}
|
jan@42469
|
952 |
|
neuper@42498
|
953 |
\noindent because nested function calls would require creating redexes
|
neuper@42498
|
954 |
inside-out; however, the prototype's rewrite-engine only works top down
|
neuper@42498
|
955 |
from the root of a term down to the leaves.
|
jan@42469
|
956 |
|
neuper@42504
|
957 |
How all these technicalities are to be checked in the prototype is
|
neuper@42498
|
958 |
shown in \S\ref{flow-prep} below.
|
jan@42473
|
959 |
|
neuper@42498
|
960 |
% \paragraph{Explicit Problems} require explicit methods to solve them, and within
|
neuper@42498
|
961 |
% this methods we have some explicit steps to do. This steps can be unique for
|
neuper@42498
|
962 |
% a special problem or refindable in other problems. No mather what case, such
|
neuper@42498
|
963 |
% steps often require some technical functions behind. For the solving process
|
neuper@42498
|
964 |
% of the Inverse Z Transformation and the corresponding partial fraction it was
|
neuper@42498
|
965 |
% neccessary to build helping functions like \texttt{get\_denominator},
|
neuper@42498
|
966 |
% \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
|
neuper@42498
|
967 |
% to filter the denominator or numerator out of a fraction, last one helps us to
|
neuper@42498
|
968 |
% get to know the bound variable in a equation.
|
neuper@42498
|
969 |
% \par
|
neuper@42498
|
970 |
% By taking \texttt{get\_denominator} as an example, we want to explain how to
|
neuper@42498
|
971 |
% implement new functions into the existing system and how we can later use them
|
neuper@42498
|
972 |
% in our program.
|
neuper@42498
|
973 |
%
|
neuper@42498
|
974 |
% \subsubsection{Find a place to Store the Function}
|
neuper@42498
|
975 |
%
|
neuper@42498
|
976 |
% The whole system builds up on a well defined structure of Knowledge. This
|
neuper@42498
|
977 |
% Knowledge sets up at the Path:
|
neuper@42498
|
978 |
% \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
|
neuper@42498
|
979 |
% For implementing the Function \texttt{get\_denominator} (which let us extract
|
neuper@42498
|
980 |
% the denominator out of a fraction) we have choosen the Theory (file)
|
neuper@42498
|
981 |
% \texttt{Rational.thy}.
|
neuper@42498
|
982 |
%
|
neuper@42498
|
983 |
% \subsubsection{Write down the new Function}
|
neuper@42498
|
984 |
%
|
neuper@42498
|
985 |
% In upper Theory we now define the new function and its purpose:
|
neuper@42498
|
986 |
% \begin{verbatim}
|
neuper@42498
|
987 |
% get_denominator :: "real => real"
|
neuper@42498
|
988 |
% \end{verbatim}
|
neuper@42498
|
989 |
% This command tells the machine that a function with the name
|
neuper@42498
|
990 |
% \texttt{get\_denominator} exists which gets a real expression as argument and
|
neuper@42498
|
991 |
% returns once again a real expression. Now we are able to implement the function
|
neuper@42498
|
992 |
% itself, upcoming example now shows the implementation of
|
neuper@42498
|
993 |
% \texttt{get\_denominator}.
|
neuper@42498
|
994 |
%
|
neuper@42498
|
995 |
% %\begin{example}
|
neuper@42498
|
996 |
% \label{eg:getdenom}
|
neuper@42498
|
997 |
% \begin{verbatim}
|
neuper@42498
|
998 |
%
|
neuper@42498
|
999 |
% 01 (*
|
neuper@42498
|
1000 |
% 02 *("get_denominator",
|
neuper@42498
|
1001 |
% 03 * ("Rational.get_denominator", eval_get_denominator ""))
|
neuper@42498
|
1002 |
% 04 *)
|
neuper@42498
|
1003 |
% 05 fun eval_get_denominator (thmid:string) _
|
neuper@42498
|
1004 |
% 06 (t as Const ("Rational.get_denominator", _) $
|
neuper@42498
|
1005 |
% 07 (Const ("Rings.inverse_class.divide", _) $num
|
neuper@42498
|
1006 |
% 08 $denom)) thy =
|
neuper@42498
|
1007 |
% 09 SOME (mk_thmid thmid ""
|
neuper@42498
|
1008 |
% 10 (Print_Mode.setmp []
|
neuper@42498
|
1009 |
% 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
|
neuper@42498
|
1010 |
% 12 Trueprop $ (mk_equality (t, denom)))
|
neuper@42498
|
1011 |
% 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
|
neuper@42498
|
1012 |
% %\end{example}
|
neuper@42498
|
1013 |
%
|
neuper@42498
|
1014 |
% Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
|
neuper@42498
|
1015 |
% there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
|
neuper@42498
|
1016 |
% splittet
|
neuper@42498
|
1017 |
% into its two parts (\texttt{\$num \$denom}). The lines before are additionals
|
neuper@42498
|
1018 |
% commands for declaring the function and the lines after are modeling and
|
neuper@42498
|
1019 |
% returning a real variable out of \texttt{\$denom}.
|
neuper@42498
|
1020 |
%
|
neuper@42498
|
1021 |
% \subsubsection{Add a test for the new Function}
|
neuper@42498
|
1022 |
%
|
neuper@42498
|
1023 |
% \paragraph{Everytime when adding} a new function it is essential also to add
|
neuper@42498
|
1024 |
% a test for it. Tests for all functions are sorted in the same structure as the
|
neuper@42498
|
1025 |
% knowledge it self and can be found up from the path:
|
neuper@42498
|
1026 |
% \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
|
neuper@42498
|
1027 |
% This tests are nothing very special, as a first prototype the functionallity
|
neuper@42498
|
1028 |
% of a function can be checked by evaluating the result of a simple expression
|
neuper@42498
|
1029 |
% passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
|
neuper@42498
|
1030 |
% \textit{just} created function \texttt{get\_denominator}.
|
neuper@42498
|
1031 |
%
|
neuper@42498
|
1032 |
% %\begin{example}
|
neuper@42498
|
1033 |
% \label{eg:getdenomtest}
|
neuper@42498
|
1034 |
% \begin{verbatim}
|
neuper@42498
|
1035 |
%
|
neuper@42498
|
1036 |
% 01 val thy = @{theory Isac};
|
neuper@42498
|
1037 |
% 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
|
neuper@42498
|
1038 |
% 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
|
neuper@42498
|
1039 |
% 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
|
neuper@42498
|
1040 |
% 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
|
neuper@42498
|
1041 |
% %\end{example}
|
neuper@42498
|
1042 |
%
|
neuper@42498
|
1043 |
% \begin{description}
|
neuper@42498
|
1044 |
% \item[01] checks if the proofer set up on our {\sisac{}} System.
|
neuper@42498
|
1045 |
% \item[02] passes a simple expression (fraction) to our suddenly created
|
neuper@42498
|
1046 |
% function.
|
neuper@42498
|
1047 |
% \item[04] checks if the resulting variable is the correct one (in this case
|
neuper@42498
|
1048 |
% ``b'' the denominator) and returns.
|
neuper@42498
|
1049 |
% \item[05] handels the error case and reports that the function is not able to
|
neuper@42498
|
1050 |
% solve the given problem.
|
neuper@42498
|
1051 |
% \end{description}
|
jan@42469
|
1052 |
|
jan@42491
|
1053 |
\subsection{Specification of the Problem}\label{spec}
|
jan@42491
|
1054 |
%WN <--> \chapter 7 der Thesis
|
jan@42491
|
1055 |
%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
|
jan@42491
|
1056 |
|
neuper@42504
|
1057 |
Mechanical treatment requires to translate a textual problem
|
neuper@42504
|
1058 |
description like in Fig.\ref{fig-interactive} on
|
neuper@42504
|
1059 |
p.\pageref{fig-interactive} into a {\em formal} specification. The
|
neuper@48777
|
1060 |
formal specification of the running example could look like is this
|
neuper@48777
|
1061 |
~\footnote{The ``TODO'' in the postcondition indicates, that postconditions
|
neuper@48777
|
1062 |
are not yet handled in the prototype; in particular, the postcondition, i.e.
|
neuper@48777
|
1063 |
the correctness of the result is not yet automatically proved.}:
|
jan@42491
|
1064 |
|
jan@42491
|
1065 |
%WN Hier brauchen wir die Spezifikation des 'running example' ...
|
jan@42491
|
1066 |
%JR Habe input, output und precond vom Beispiel eingefรผgt brauche aber Hilfe bei
|
jan@42491
|
1067 |
%JR der post condition - die existiert fรผr uns ja eigentlich nicht aka
|
jan@42491
|
1068 |
%JR haben sie bis jetzt nicht beachtet WN...
|
jan@42491
|
1069 |
%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
|
jan@42491
|
1070 |
%JR2 done
|
jan@42491
|
1071 |
|
neuper@42504
|
1072 |
\label{eg:neuper2}
|
neuper@42504
|
1073 |
{\small\begin{tabbing}
|
neuper@42504
|
1074 |
123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
|
neuper@42504
|
1075 |
%\hfill \\
|
neuper@42504
|
1076 |
\>Specification:\\
|
neuper@42507
|
1077 |
\> \>input \>: ${\it filterExpression} \;\;X\;z=\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}, \;{\it domain}\;\mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$\\
|
neuper@42504
|
1078 |
\>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
|
neuper@42504
|
1079 |
\>\>output \>: stepResponse $x[n]$ \\
|
neuper@42504
|
1080 |
\>\>postcond \>: TODO
|
neuper@42504
|
1081 |
\end{tabbing}}
|
jan@42491
|
1082 |
|
jan@42500
|
1083 |
%JR wie besprochen, kein remark, keine begrรผndung, nur simples "nicht behandelt"
|
jan@42500
|
1084 |
|
jan@42500
|
1085 |
% \begin{remark}
|
jan@42500
|
1086 |
% Defining the postcondition requires a high amount mathematical
|
jan@42500
|
1087 |
% knowledge, the difficult part in our case is not to set up this condition
|
jan@42500
|
1088 |
% nor it is more to define it in a way the interpreter is able to handle it.
|
jan@42500
|
1089 |
% Due the fact that implementing that mechanisms is quite the same amount as
|
jan@42500
|
1090 |
% creating the programm itself, it is not avaible in our prototype.
|
jan@42500
|
1091 |
% \label{rm:postcond}
|
jan@42500
|
1092 |
% \end{remark}
|
jan@42491
|
1093 |
|
neuper@42504
|
1094 |
The implementation of the formal specification in the present
|
neuper@42504
|
1095 |
prototype, still bar-bones without support for authoring, is done
|
neuper@42504
|
1096 |
like that:
|
jan@42491
|
1097 |
%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
|
neuper@42504
|
1098 |
|
jan@42491
|
1099 |
{\footnotesize\label{exp-spec}
|
jan@42491
|
1100 |
\begin{verbatim}
|
neuper@42504
|
1101 |
00 ML {*
|
jan@42491
|
1102 |
01 store_specification
|
jan@42491
|
1103 |
02 (prepare_specification
|
neuper@42504
|
1104 |
03 "pbl_SP_Ztrans_inv"
|
neuper@42504
|
1105 |
04 ["Jan Rocnik"]
|
jan@42491
|
1106 |
05 thy
|
jan@42491
|
1107 |
06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
|
neuper@42507
|
1108 |
07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
|
neuper@42507
|
1109 |
08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
|
jan@42494
|
1110 |
09 ("#Find" , ["stepResponse n_eq"]),
|
neuper@42507
|
1111 |
10 ("#Post" , [" TODO "])])
|
neuper@42507
|
1112 |
11 prls
|
neuper@42507
|
1113 |
12 NONE
|
neuper@42507
|
1114 |
13 [["SignalProcessing","Z_Transform","Inverse"]]);
|
neuper@42504
|
1115 |
14 *}
|
jan@42491
|
1116 |
\end{verbatim}}
|
neuper@42504
|
1117 |
|
jan@42491
|
1118 |
Although the above details are partly very technical, we explain them
|
jan@42491
|
1119 |
in order to document some intricacies of TP-based programming in the
|
jan@42491
|
1120 |
present state of the {\sisac} prototype:
|
jan@42491
|
1121 |
\begin{description}
|
jan@42491
|
1122 |
\item[01..02]\textit{store\_specification:} stores the result of the
|
jan@42491
|
1123 |
function \textit{prep\_specification} in a global reference
|
jan@42491
|
1124 |
\textit{Unsynchronized.ref}, which causes principal conflicts with
|
jan@42511
|
1125 |
Isabelle's asynchronous document model~\cite{Wenzel-11:doc-orient} and
|
jan@42491
|
1126 |
parallel execution~\cite{Makarius-09:parall-proof} and is under
|
jan@42491
|
1127 |
reconstruction already.
|
jan@42491
|
1128 |
|
neuper@42504
|
1129 |
\textit{prep\_specification:} translates the specification to an internal format
|
jan@42491
|
1130 |
which allows efficient processing; see for instance line {\rm 07}
|
jan@42491
|
1131 |
below.
|
neuper@42504
|
1132 |
\item[03..04] are a unique identifier for the specification within {\sisac}
|
neuper@42504
|
1133 |
and the ``mathematics author'' holding the copy-rights.
|
jan@42491
|
1134 |
\item[05] is the Isabelle \textit{theory} required to parse the
|
jan@42491
|
1135 |
specification in lines {\rm 07..10}.
|
jan@42491
|
1136 |
\item[06] is a key into the tree of all specifications as presented to
|
jan@42511
|
1137 |
the user (where some branches might be hidden by the dialogue
|
jan@42491
|
1138 |
component).
|
jan@42491
|
1139 |
\item[07..10] are the specification with input, pre-condition, output
|
neuper@42507
|
1140 |
and post-condition respectively; note that the specification contains
|
neuper@42507
|
1141 |
variables to be instantiated with concrete values for a concrete problem ---
|
neuper@42507
|
1142 |
thus the specification actually captures a class of problems. The post-condition is not handled in
|
neuper@42504
|
1143 |
the prototype presently.
|
neuper@42507
|
1144 |
\item[11] is a rule-set (defined elsewhere) for evaluation of the pre-condition: \textit{(rhs X\_eq) is\_continuous\_in D}, instantiated with the values of a concrete problem, evaluates to true or false --- and all evaluation is done by
|
neuper@42507
|
1145 |
rewriting determined by rule-sets.
|
jan@42491
|
1146 |
\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
|
jan@42491
|
1147 |
problem associated to a function from Computer Algebra (like an
|
jan@42491
|
1148 |
equation solver) which is not the case here.
|
neuper@42504
|
1149 |
\item[13] is a list of methods solving the specified problem (here
|
neuper@42504
|
1150 |
only one list item) represented analogously to {\rm 06}.
|
jan@42491
|
1151 |
\end{description}
|
jan@42491
|
1152 |
|
jan@42491
|
1153 |
|
jan@42491
|
1154 |
%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
|
jan@42491
|
1155 |
%WN ...
|
jan@42491
|
1156 |
% type pbt =
|
jan@42491
|
1157 |
% {guh : guh, (*unique within this isac-knowledge*)
|
jan@42491
|
1158 |
% mathauthors: string list, (*copyright*)
|
jan@42491
|
1159 |
% init : pblID, (*to start refinement with*)
|
jan@42491
|
1160 |
% thy : theory, (* which allows to compile that pbt
|
jan@42491
|
1161 |
% TODO: search generalized for subthy (ref.p.69*)
|
jan@42491
|
1162 |
% (*^^^ WN050912 NOT used during application of the problem,
|
jan@42491
|
1163 |
% because applied terms may be from 'subthy' as well as from super;
|
jan@42491
|
1164 |
% thus we take 'maxthy'; see match_ags !*)
|
jan@42491
|
1165 |
% cas : term option,(*'CAS-command'*)
|
jan@42491
|
1166 |
% prls : rls, (* for preds in where_*)
|
jan@42491
|
1167 |
% where_: term list, (* where - predicates*)
|
jan@42491
|
1168 |
% ppc : pat list,
|
jan@42491
|
1169 |
% (*this is the model-pattern;
|
jan@42491
|
1170 |
% it contains "#Given","#Where","#Find","#Relate"-patterns
|
Walther@60469
|
1171 |
% for constraints on identifiers see "fun copy_name"*)
|
jan@42491
|
1172 |
% met : metID list}; (* methods solving the pbt*)
|
jan@42491
|
1173 |
%
|
jan@42491
|
1174 |
%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
|
jan@42491
|
1175 |
%WN oben selbst geschrieben.
|
jan@42491
|
1176 |
|
jan@42491
|
1177 |
|
jan@42491
|
1178 |
|
jan@42491
|
1179 |
|
jan@42491
|
1180 |
%WN das w"urde ich in \sec\label{progr} verschieben und
|
jan@42491
|
1181 |
%WN das SubProblem partial fractions zum Erkl"aren verwenden.
|
jan@42491
|
1182 |
% Such a specification is checked before the execution of a program is
|
jan@42491
|
1183 |
% started, the same applies for sub-programs. In the following example
|
jan@42491
|
1184 |
% (Example~\ref{eg:subprob}) shows the call of such a subproblem:
|
jan@42491
|
1185 |
%
|
jan@42491
|
1186 |
% \vbox{
|
jan@42491
|
1187 |
% \begin{example}
|
jan@42491
|
1188 |
% \label{eg:subprob}
|
jan@42491
|
1189 |
% \hfill \\
|
jan@42491
|
1190 |
% {\ttfamily \begin{tabbing}
|
jan@42491
|
1191 |
% ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
|
jan@42491
|
1192 |
% ``\>\>[linear,univariate,equation,test],'' \\
|
jan@42491
|
1193 |
% ``\>\>[Test,solve\_linear])'' \\
|
jan@42491
|
1194 |
% ``\>[BOOL equ, REAL z])'' \\
|
jan@42491
|
1195 |
% \end{tabbing}
|
jan@42491
|
1196 |
% }
|
jan@42491
|
1197 |
% {\small\textit{
|
jan@42491
|
1198 |
% \noindent If a program requires a result which has to be
|
jan@42491
|
1199 |
% calculated first we can use a subproblem to do so. In our specific
|
jan@42491
|
1200 |
% case we wanted to calculate the zeros of a fraction and used a
|
jan@42491
|
1201 |
% subproblem to calculate the zeros of the denominator polynom.
|
jan@42491
|
1202 |
% }}
|
jan@42491
|
1203 |
% \end{example}
|
jan@42491
|
1204 |
% }
|
jan@42491
|
1205 |
|
jan@42491
|
1206 |
\subsection{Implementation of the Method}\label{meth}
|
neuper@42504
|
1207 |
A method collects all data required to interpret a certain program by
|
neuper@42504
|
1208 |
Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
|
neuper@42507
|
1209 |
the running example is embedded on the last line in the following method:
|
neuper@42504
|
1210 |
%The methods represent the different ways a problem can be solved. This can
|
neuper@42504
|
1211 |
%include mathematical tactics as well as tactics taught in different courses.
|
neuper@42504
|
1212 |
%Declaring the Method itself gives us the possibilities to describe the way of
|
neuper@42504
|
1213 |
%calculation in deep, as well we get the oppertunities to build in different
|
neuper@42504
|
1214 |
%rulesets.
|
jan@42491
|
1215 |
|
jan@42502
|
1216 |
{\footnotesize
|
jan@42491
|
1217 |
\begin{verbatim}
|
neuper@42504
|
1218 |
00 ML {*
|
neuper@42504
|
1219 |
01 store_method
|
neuper@42504
|
1220 |
02 (prep_method
|
neuper@42504
|
1221 |
03 "SP_InverseZTransformation_classic"
|
neuper@42504
|
1222 |
04 ["Jan Rocnik"]
|
neuper@42504
|
1223 |
05 thy
|
neuper@42507
|
1224 |
06 ( ["SignalProcessing", "Z_Transform", "Inverse"],
|
neuper@42507
|
1225 |
07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
|
neuper@42507
|
1226 |
08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
|
neuper@42507
|
1227 |
09 ("#Find" , ["stepResponse n_eq"]),
|
neuper@42507
|
1228 |
10 rew_ord erls
|
neuper@42507
|
1229 |
11 srls prls nrls
|
neuper@42507
|
1230 |
12 errpats
|
neuper@42507
|
1231 |
13 program);
|
neuper@42507
|
1232 |
14 *}
|
neuper@42504
|
1233 |
\end{verbatim}}
|
jan@42494
|
1234 |
|
neuper@42504
|
1235 |
\noindent The above code stores the whole structure analogously to a
|
neuper@42507
|
1236 |
specification as described above:
|
neuper@42504
|
1237 |
\begin{description}
|
neuper@42504
|
1238 |
\item[01..06] are identical to those for the example specification on
|
neuper@42504
|
1239 |
p.\pageref{exp-spec}.
|
jan@42494
|
1240 |
|
neuper@42504
|
1241 |
\item[07..09] show something looking like the specification; this is a
|
neuper@42507
|
1242 |
{\em guard}: as long as not all \textit{Given} items are present and
|
neuper@42507
|
1243 |
the \textit{Pre}-conditions is not true, interpretation of the program
|
neuper@42504
|
1244 |
is not started.
|
neuper@42504
|
1245 |
|
neuper@42507
|
1246 |
\item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case
|
neuper@42507
|
1247 |
\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets
|
neuper@42507
|
1248 |
\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
|
jan@42511
|
1249 |
\textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec}
|
neuper@42507
|
1250 |
and (c) is required for the derivation-machinery checking user-input formulas.
|
neuper@42504
|
1251 |
|
neuper@42507
|
1252 |
\item[12..13] \textit{errpats} are error-patterns~\cite{gdaroczy-EP-13} for this method and \textit{program} is the variable holding the example from p.\pageref {s:impl}.
|
jan@42494
|
1253 |
\end{description}
|
neuper@42507
|
1254 |
The many rule-sets above cause considerable efforts for the
|
neuper@42507
|
1255 |
programmers, in particular, because there are no tools for checking
|
neuper@42507
|
1256 |
essential features of rule-sets.
|
neuper@42504
|
1257 |
|
neuper@42504
|
1258 |
% is again very technical and goes hard in detail. Unfortunataly
|
neuper@42504
|
1259 |
% most declerations are not essential for a basic programm but leads us to a huge
|
neuper@42504
|
1260 |
% range of powerful possibilities.
|
neuper@42504
|
1261 |
%
|
neuper@42504
|
1262 |
% \begin{description}
|
neuper@42504
|
1263 |
% \item[01..02] stores the method with the given name into the system under a global
|
neuper@42504
|
1264 |
% reference.
|
neuper@42504
|
1265 |
% \item[03] specifies the topic within which context the method can be found.
|
neuper@42504
|
1266 |
% \item[04..05] as the requirements for different methods can be deviant we
|
neuper@42504
|
1267 |
% declare what is \emph{given} and and what to \emph{find} for this specific method.
|
neuper@42504
|
1268 |
% The code again helds on the topic of the case studie, where the inverse
|
neuper@42504
|
1269 |
% z-transformation does a switch between a term describing a electrical filter into
|
neuper@42504
|
1270 |
% its step response. Also the datatype has to be declared (bool - due the fact that
|
neuper@42504
|
1271 |
% we handle equations).
|
neuper@42504
|
1272 |
% \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
|
neuper@42504
|
1273 |
% theorem of it is used for rewriting one single step.
|
neuper@42504
|
1274 |
% \item[07] \texttt{rls} is the currently used ruleset for this method. This set
|
neuper@42504
|
1275 |
% has already been defined before.
|
neuper@42504
|
1276 |
% \item[08] we would have the possiblitiy to add this method to a predefined tree of
|
neuper@42504
|
1277 |
% calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
|
neuper@42504
|
1278 |
% independend.
|
neuper@42504
|
1279 |
% \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
|
neuper@42504
|
1280 |
% the source.
|
neuper@42504
|
1281 |
% \item[10] \emph{predicates ruleset} can be used to indicates predicates within
|
neuper@42504
|
1282 |
% model patterns.
|
neuper@42504
|
1283 |
% \item[11] The \emph{check ruleset} summarizes rules for checking formulas
|
neuper@42504
|
1284 |
% elementwise.
|
neuper@42504
|
1285 |
% \item[12] \emph{error patterns} which are expected in this kind of method can be
|
neuper@42504
|
1286 |
% pre-specified to recognize them during the method.
|
neuper@42504
|
1287 |
% \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
|
neuper@42504
|
1288 |
% of the specific method.
|
neuper@42504
|
1289 |
% \item[14] for this code snipset we don't specify the programm itself and keep it
|
neuper@42504
|
1290 |
% empty. Follow up \S\ref{progr} for informations on how to implement this
|
neuper@42504
|
1291 |
% \textit{main} part.
|
neuper@42504
|
1292 |
% \end{description}
|
neuper@42504
|
1293 |
|
neuper@42478
|
1294 |
\subsection{Implementation of the TP-based Program}\label{progr}
|
neuper@42507
|
1295 |
So finally all the prerequisites are described and the final task can
|
neuper@42480
|
1296 |
be addressed. The program below comes back to the running example: it
|
neuper@42480
|
1297 |
computes a solution for the problem from Fig.\ref{fig-interactive} on
|
neuper@42480
|
1298 |
p.\pageref{fig-interactive}. The reader is reminded of
|
neuper@42480
|
1299 |
\S\ref{PL-isab}, the introduction of the programming language:
|
jan@42502
|
1300 |
|
jan@42502
|
1301 |
{\footnotesize\it\label{s:impl}
|
neuper@42482
|
1302 |
\begin{tabbing}
|
neuper@42478
|
1303 |
123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
|
neuper@42507
|
1304 |
\>{\rm 00}\>ML \{*\\
|
neuper@42480
|
1305 |
\>{\rm 00}\>val program =\\
|
neuper@42480
|
1306 |
\>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
|
neuper@42482
|
1307 |
\>{\rm 02}\>\> {\tt let} \\
|
neuper@42468
|
1308 |
\>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
|
neuper@42507
|
1309 |
\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
|
neuper@42468
|
1310 |
\>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
|
neuper@42468
|
1311 |
\>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
|
neuper@42468
|
1312 |
\>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
|
neuper@42478
|
1313 |
\>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
|
neuper@42478
|
1314 |
%\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
|
neuper@42478
|
1315 |
\>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
|
neuper@42478
|
1316 |
\>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
|
neuper@42507
|
1317 |
\>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@ \\
|
neuper@42478
|
1318 |
\>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
|
neuper@42482
|
1319 |
\>{\rm 13}\>\> {\tt in } \\
|
neuper@42504
|
1320 |
\>{\rm 14}\>\>\> X'\_eq"\\
|
neuper@42507
|
1321 |
\>{\rm 15}\>*\}
|
neuper@42478
|
1322 |
\end{tabbing}}
|
neuper@42468
|
1323 |
% ORIGINAL FROM Inverse_Z_Transform.thy
|
neuper@42468
|
1324 |
% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
neuper@42468
|
1325 |
% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
neuper@42468
|
1326 |
% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1327 |
% " (X'_z::real) = lhs X'; "^(* ?X' z*)
|
neuper@42468
|
1328 |
% " (zzz::real) = argument_in X'_z; "^(* z *)
|
neuper@42468
|
1329 |
% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1330 |
%
|
neuper@42468
|
1331 |
% " (pbz::real) = (SubProblem (Isac', "^(**)
|
neuper@42468
|
1332 |
% " [partial_fraction,rational,simplification], "^
|
neuper@42468
|
1333 |
% " [simplification,of_rationals,to_partial_fraction]) "^
|
neuper@42468
|
1334 |
% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1335 |
%
|
neuper@42468
|
1336 |
% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1337 |
% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
neuper@42468
|
1338 |
% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1339 |
% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1340 |
% " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
|
neuper@42468
|
1341 |
% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1342 |
% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42480
|
1343 |
The program is represented as a string and part of the method in
|
neuper@42480
|
1344 |
\S\ref{meth}. As mentioned in \S\ref{PL} the program is purely
|
neuper@42480
|
1345 |
functional and lacks any input statements and output statements. So
|
neuper@42480
|
1346 |
the steps of calculation towards a solution (and interactive tutoring
|
neuper@42480
|
1347 |
in step-wise problem solving) are created as a side-effect by
|
neuper@42480
|
1348 |
Lucas-Interpretation. The side-effects are triggered by the tactics
|
neuper@42482
|
1349 |
\texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
|
neuper@42482
|
1350 |
\texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
|
neuper@42507
|
1351 |
{\rm 12} respectively. These tactics produce the respective lines in the
|
neuper@42480
|
1352 |
calculation on p.\pageref{flow-impl}.
|
neuper@42478
|
1353 |
|
neuper@42480
|
1354 |
The above lines {\rm 05, 06} do not contain a tactics, so they do not
|
neuper@42480
|
1355 |
immediately contribute to the calculation on p.\pageref{flow-impl};
|
neuper@42482
|
1356 |
rather, they compute actual arguments for the \texttt{SubProblem} in
|
neuper@42480
|
1357 |
line {\rm 09}~\footnote{The tactics also are break-points for the
|
neuper@42480
|
1358 |
interpreter, where control is handed over to the user in interactive
|
neuper@42482
|
1359 |
tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
|
neuper@42480
|
1360 |
|
neuper@42480
|
1361 |
\medskip The above program also indicates the dominant role of interactive
|
neuper@42478
|
1362 |
selection of knowledge in the three-dimensional universe of
|
jan@48766
|
1363 |
mathematics. The \texttt{SubProblem} in the above lines
|
neuper@42478
|
1364 |
{\rm 07..09} is more than a function call with the actual arguments
|
neuper@42478
|
1365 |
\textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
|
neuper@42478
|
1366 |
three items:
|
neuper@42480
|
1367 |
|
neuper@42478
|
1368 |
\begin{enumerate}
|
neuper@42478
|
1369 |
\item the theory, in the example \textit{Isac} because different
|
neuper@42478
|
1370 |
methods can be selected in Pt.3 below, which are defined in different
|
neuper@42478
|
1371 |
theories with \textit{Isac} collecting them.
|
neuper@42480
|
1372 |
\item the specification identified by \textit{[partial\_fraction,
|
neuper@42480
|
1373 |
rational, simplification]} in the tree of specifications; this
|
neuper@42480
|
1374 |
specification is analogous to the specification of the main program
|
neuper@42480
|
1375 |
described in \S\ref{spec}; the problem is to find a ``partial fraction
|
neuper@42480
|
1376 |
decomposition'' for a univariate rational polynomial.
|
neuper@42480
|
1377 |
\item the method in the above example is \textit{[ ]}, i.e. empty,
|
neuper@42480
|
1378 |
which supposes the interpreter to select one of the methods predefined
|
neuper@42480
|
1379 |
in the specification, for instance in line {\rm 13} in the running
|
neuper@42480
|
1380 |
example's specification on p.\pageref{exp-spec}~\footnote{The freedom
|
neuper@42480
|
1381 |
(or obligation) for selection carries over to the student in
|
neuper@42480
|
1382 |
interactive tutoring.}.
|
neuper@42478
|
1383 |
\end{enumerate}
|
neuper@42478
|
1384 |
|
neuper@42480
|
1385 |
The program code, above presented as a string, is parsed by Isabelle's
|
neuper@42480
|
1386 |
parser --- the program is an Isabelle term. This fact is expected to
|
neuper@42480
|
1387 |
simplify verification tasks in the future; on the other hand, this
|
jan@42511
|
1388 |
fact causes troubles in error detection which are discussed as part
|
neuper@42514
|
1389 |
of the work-flow in the subsequent section.
|
neuper@42467
|
1390 |
|
neuper@42514
|
1391 |
\section{Work-flow of Programming in the Prototype}\label{workflow}
|
neuper@42498
|
1392 |
The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
|
neuper@42498
|
1393 |
step forward for interactive theory and proof development. The
|
neuper@42498
|
1394 |
{\sisac}-prototype re-uses this IDE as a programming environment. The
|
neuper@42498
|
1395 |
experiences from this re-use show, that the essential components are
|
neuper@42498
|
1396 |
available from Isabelle/jEdit. However, additional tools and features
|
jan@42511
|
1397 |
are required to achieve acceptable usability.
|
neuper@42498
|
1398 |
|
neuper@42498
|
1399 |
So notable experiences are reported here, also as a requirement
|
neuper@42498
|
1400 |
capture for further development of TP-based languages and respective
|
neuper@42498
|
1401 |
IDEs.
|
neuper@42468
|
1402 |
|
jan@42466
|
1403 |
\subsection{Preparations and Trials}\label{flow-prep}
|
neuper@42499
|
1404 |
The many sub-tasks to be accomplished {\em before} the first line of
|
neuper@42499
|
1405 |
program code can be written and tested suggest an approach which
|
neuper@42499
|
1406 |
step-wise establishes the prerequisites. The case study underlying
|
neuper@42499
|
1407 |
this paper~\cite{jrocnik-bakk} documents the approach in a separate
|
neuper@42499
|
1408 |
Isabelle theory,
|
neuper@42499
|
1409 |
\textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
|
neuper@42499
|
1410 |
II in the study comprises this theory, \LaTeX ed from the theory by
|
neuper@42499
|
1411 |
use of Isabelle's document preparation system. This paper resembles
|
neuper@42499
|
1412 |
the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
|
neuper@42499
|
1413 |
implementation work involves several iterations.
|
neuper@42498
|
1414 |
|
neuper@42499
|
1415 |
\bigskip For instance, only the last step, implementing the program
|
neuper@42499
|
1416 |
described in \S\ref{meth}, reveals details required. Let us assume,
|
neuper@42499
|
1417 |
this is the ML-function \textit{argument\_in} required in line {\rm 06}
|
neuper@42499
|
1418 |
of the example program on p.\pageref{s:impl}; how this function needs
|
neuper@42499
|
1419 |
to be implemented in the prototype has been discussed in \S\ref{funs}
|
neuper@42499
|
1420 |
already.
|
neuper@42498
|
1421 |
|
neuper@42499
|
1422 |
Now let us assume, that calling this function from the program code
|
neuper@42499
|
1423 |
does not work; so testing this function is required in order to find out
|
neuper@42499
|
1424 |
the reason: type errors, a missing entry of the function somewhere or
|
neuper@42499
|
1425 |
even more nasty technicalities \dots
|
neuper@42498
|
1426 |
|
neuper@42499
|
1427 |
{\footnotesize
|
neuper@42482
|
1428 |
\begin{verbatim}
|
jan@42513
|
1429 |
01 ML {*
|
jan@42513
|
1430 |
02 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
|
jan@42513
|
1431 |
03 val SOME (str, t') = eval_argument_in ""
|
jan@42513
|
1432 |
04 "Build_Inverse_Z_Transform.argument'_in" t 0;
|
jan@42513
|
1433 |
05 term2str t';
|
jan@42513
|
1434 |
06 *}
|
jan@42513
|
1435 |
07 val it = "(argument_in X z) = z": string\end{verbatim}}
|
neuper@42499
|
1436 |
|
neuper@42499
|
1437 |
\noindent So, this works: we get an ad-hoc theorem, which used in
|
neuper@42499
|
1438 |
rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
|
neuper@42499
|
1439 |
reduction and create a rule-set \texttt{rls} for that purpose:
|
neuper@42499
|
1440 |
|
neuper@42499
|
1441 |
{\footnotesize
|
neuper@42482
|
1442 |
\begin{verbatim}
|
jan@42513
|
1443 |
01 ML {*
|
jan@42513
|
1444 |
02 val rls = append_rls "test" e_rls
|
jan@42513
|
1445 |
03 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
|
jan@42513
|
1446 |
04 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
|
jan@42513
|
1447 |
05 *}
|
jan@42513
|
1448 |
06 val t' = Free ("z", "RealDef.real"): term
|
jan@42513
|
1449 |
07 val asm = []: term list\end{verbatim}}
|
neuper@42499
|
1450 |
|
neuper@42499
|
1451 |
\noindent The resulting term \texttt{t'} is \texttt{Free ("z",
|
neuper@42499
|
1452 |
"RealDef.real")}, i.e the variable \texttt{z}, so all is
|
neuper@42499
|
1453 |
perfect. Probably we have forgotten to store this function correctly~?
|
neuper@42499
|
1454 |
We review the respective \texttt{calclist} (again an
|
neuper@42499
|
1455 |
\textit{Unsynchronized.ref} to be removed in order to adjust to
|
neuper@42514
|
1456 |
Isabelle/Isar's asynchronous document model):
|
neuper@42499
|
1457 |
|
neuper@42499
|
1458 |
{\footnotesize
|
neuper@42499
|
1459 |
\begin{verbatim}
|
jan@42513
|
1460 |
01 calclist:= overwritel (! calclist,
|
jan@42513
|
1461 |
02 [("argument_in",
|
jan@42513
|
1462 |
03 ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
|
jan@42513
|
1463 |
04 ...
|
jan@42513
|
1464 |
05 ]);\end{verbatim}}
|
neuper@42499
|
1465 |
|
neuper@42499
|
1466 |
\noindent The entry is perfect. So what is the reason~? Ah, probably there
|
neuper@42499
|
1467 |
is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
|
neuper@42499
|
1468 |
right, the function \texttt{argument\_in} is not contained in the respective
|
neuper@42499
|
1469 |
rule-set \textit{srls} \dots this just as an example of the intricacies in
|
neuper@42499
|
1470 |
debugging a program in the present state of the prototype.
|
neuper@42499
|
1471 |
|
neuper@42499
|
1472 |
\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
|
neuper@42499
|
1473 |
Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
|
neuper@42499
|
1474 |
usually developed within several iterations, the program can be
|
neuper@42499
|
1475 |
assembled; on p.\pageref{s:impl} there is the complete program of the
|
neuper@42499
|
1476 |
running example.
|
neuper@42499
|
1477 |
|
neuper@42499
|
1478 |
The completion of this program required efforts for several weeks
|
neuper@42499
|
1479 |
(after some months of familiarisation with {\sisac}), caused by the
|
neuper@42499
|
1480 |
abundance of intricacies indicated above. Also writing the program is
|
neuper@42499
|
1481 |
not pleasant, given Isabelle/Isar/ without add-ons for
|
neuper@42499
|
1482 |
programming. Already writing and parsing a few lines of program code
|
neuper@42499
|
1483 |
is a challenge: the program is an Isabelle term; Isabelle's parser,
|
neuper@42499
|
1484 |
however, is not meant for huge terms like the program of the running
|
neuper@42499
|
1485 |
example. So reading out the specific error (usually type errors) from
|
neuper@42499
|
1486 |
Isabelle's message is difficult.
|
neuper@42499
|
1487 |
|
neuper@42499
|
1488 |
\medskip Testing the evaluation of the program has to rely on very
|
neuper@42514
|
1489 |
simple tools. Step-wise execution is modeled by a function
|
neuper@42499
|
1490 |
\texttt{me}, short for mathematics-engine~\footnote{The interface used
|
neuper@42514
|
1491 |
by the front-end which created the calculation on
|
neuper@42499
|
1492 |
p.\pageref{fig-interactive} is different from this function}:
|
neuper@42499
|
1493 |
%the following is a simplification of the actual function
|
neuper@42499
|
1494 |
|
neuper@42499
|
1495 |
{\footnotesize
|
neuper@42499
|
1496 |
\begin{verbatim}
|
jan@42513
|
1497 |
01 ML {* me; *}
|
jan@42513
|
1498 |
02 val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}}
|
neuper@42499
|
1499 |
|
neuper@42499
|
1500 |
\noindent This function takes as arguments a tactic \texttt{tac} which
|
neuper@42499
|
1501 |
determines the next step, the step applied to the interpreter-state
|
neuper@42499
|
1502 |
\texttt{ctree * pos} as last argument taken. The interpreter-state is
|
neuper@42499
|
1503 |
a pair of a tree \texttt{ctree} representing the calculation created
|
neuper@42499
|
1504 |
(see the example below) and a position \texttt{pos} in the
|
jan@42511
|
1505 |
calculation. The function delivers a quadruple, beginning with the new
|
neuper@42499
|
1506 |
formula \texttt{mout} and the next tactic followed by the new
|
neuper@42499
|
1507 |
interpreter-state.
|
neuper@42499
|
1508 |
|
neuper@42499
|
1509 |
This function allows to stepwise check the program:
|
neuper@42499
|
1510 |
|
neuper@48771
|
1511 |
{\footnotesize\label{ml-check-program}
|
neuper@42482
|
1512 |
\begin{verbatim}
|
jan@42513
|
1513 |
01 ML {*
|
jan@42513
|
1514 |
02 val fmz =
|
jan@42513
|
1515 |
03 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
|
jan@42513
|
1516 |
04 "stepResponse (x[n::real]::bool)"];
|
jan@42513
|
1517 |
05 val (dI,pI,mI) =
|
jan@42513
|
1518 |
06 ("Isac",
|
jan@42513
|
1519 |
07 ["Inverse", "Z_Transform", "SignalProcessing"],
|
jan@42513
|
1520 |
08 ["SignalProcessing","Z_Transform","Inverse"]);
|
jan@42513
|
1521 |
09 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
|
jan@42513
|
1522 |
10 val (mout, tac, ctree, pos) = me tac (ctree, pos);
|
jan@42513
|
1523 |
11 val (mout, tac, ctree, pos) = me tac (ctree, pos);
|
jan@42513
|
1524 |
12 val (mout, tac, ctree, pos) = me tac (ctree, pos);
|
neuper@48771
|
1525 |
13 ...
|
neuper@48771
|
1526 |
\end{verbatim}}
|
neuper@42481
|
1527 |
|
jan@42511
|
1528 |
\noindent Several dozens of calls for \texttt{me} are required to
|
neuper@42499
|
1529 |
create the lines in the calculation below (including the sub-problems
|
neuper@42499
|
1530 |
not shown). When an error occurs, the reason might be located
|
neuper@42499
|
1531 |
many steps before: if evaluation by rewriting, as done by the prototype,
|
neuper@42499
|
1532 |
fails, then first nothing happens --- the effects come later and
|
neuper@42499
|
1533 |
cause unpleasant checks.
|
neuper@42481
|
1534 |
|
neuper@42499
|
1535 |
The checks comprise watching the rewrite-engine for many different
|
neuper@42499
|
1536 |
kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
|
neuper@42499
|
1537 |
particular the environment and the context at the states position ---
|
neuper@42499
|
1538 |
all checks have to rely on simple functions accessing the
|
neuper@42499
|
1539 |
\texttt{ctree}. So getting the calculation below (which resembles the
|
neuper@42499
|
1540 |
calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
|
neuper@42507
|
1541 |
is the result of several weeks of development:
|
jan@42469
|
1542 |
|
neuper@42498
|
1543 |
{\small\it\label{exp-calc}
|
neuper@42468
|
1544 |
\begin{tabbing}
|
neuper@42468
|
1545 |
123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
|
neuper@42468
|
1546 |
\>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
|
neuper@42468
|
1547 |
\>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
|
neuper@42507
|
1548 |
\>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} prep\_for\_part\_frac X\_eq}\\
|
neuper@42468
|
1549 |
\>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
|
neuper@42468
|
1550 |
\>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
|
neuper@42468
|
1551 |
\>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
|
neuper@42468
|
1552 |
\>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
|
neuper@42468
|
1553 |
\>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
|
neuper@42468
|
1554 |
\>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
|
neuper@42468
|
1555 |
\>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
|
neuper@42468
|
1556 |
\> \>\>\>\> \_\_\_ \`- - -\\
|
neuper@42468
|
1557 |
\>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
|
jan@42512
|
1558 |
\>{\rm 12}\>\> $X^\prime z = {\cal z}^{-1} (\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}})$ \`{\footnotesize {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac)}\\
|
jan@42512
|
1559 |
\>{\rm 13}\>\> $X^\prime z = {\cal z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} prep\_for\_inverse\_z X'\_eq }\\
|
neuper@42468
|
1560 |
\>{\rm 14}\>\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Rewrite\_Set} inverse\_z X'\_eq}\\
|
neuper@42468
|
1561 |
\>{\rm 15}\> \dots\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Check\_Postcond}}
|
neuper@42468
|
1562 |
\end{tabbing}}
|
neuper@42507
|
1563 |
The tactics on the right margin of the above calculation are those in
|
neuper@42507
|
1564 |
the program on p.\pageref{s:impl} which create the respective formulas
|
neuper@42507
|
1565 |
on the left.
|
neuper@42468
|
1566 |
% ORIGINAL FROM Inverse_Z_Transform.thy
|
neuper@42468
|
1567 |
% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
neuper@42468
|
1568 |
% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
neuper@42468
|
1569 |
% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1570 |
% " (X'_z::real) = lhs X'; "^(* ?X' z*)
|
neuper@42468
|
1571 |
% " (zzz::real) = argument_in X'_z; "^(* z *)
|
neuper@42468
|
1572 |
% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1573 |
%
|
neuper@42468
|
1574 |
% " (pbz::real) = (SubProblem (Isac', "^(**)
|
neuper@42468
|
1575 |
% " [partial_fraction,rational,simplification], "^
|
neuper@42468
|
1576 |
% " [simplification,of_rationals,to_partial_fraction]) "^
|
neuper@42468
|
1577 |
% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1578 |
%
|
neuper@42468
|
1579 |
% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1580 |
% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
neuper@42468
|
1581 |
% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1582 |
% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1583 |
% " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
|
neuper@42468
|
1584 |
% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1585 |
% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1586 |
|
neuper@42499
|
1587 |
\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
|
neuper@42499
|
1588 |
Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
|
neuper@42499
|
1589 |
and the knowledge accumulated in it can be distributed to appropriate
|
neuper@42499
|
1590 |
theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
|
neuper@42499
|
1591 |
sub-problem accomplishing the partial fraction decomposition to
|
neuper@42499
|
1592 |
\textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
|
neuper@42499
|
1593 |
internals, this kind of distribution is not trivial. For instance, the
|
neuper@42499
|
1594 |
function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
|
neuper@42499
|
1595 |
string with the theory it has been defined in, so this string needs to
|
neuper@42499
|
1596 |
be updated from \texttt{Build\_Inverse\_Z\_Transform} to
|
neuper@42499
|
1597 |
\texttt{Atools} if that function is transferred to theory
|
neuper@42499
|
1598 |
\textit{Atools.thy}.
|
neuper@42468
|
1599 |
|
neuper@42499
|
1600 |
In order to obtain the functionality presented in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive} data must be exported from SML-structures to XML.
|
neuper@42499
|
1601 |
This process is also rather bare-bones without authoring tools and is
|
neuper@42499
|
1602 |
described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
|
neuper@42468
|
1603 |
|
neuper@42478
|
1604 |
% \newpage
|
neuper@42478
|
1605 |
% -------------------------------------------------------------------
|
neuper@42478
|
1606 |
%
|
neuper@42478
|
1607 |
% Material, falls noch Platz bleibt ...
|
neuper@42478
|
1608 |
%
|
neuper@42478
|
1609 |
% -------------------------------------------------------------------
|
neuper@42478
|
1610 |
%
|
neuper@42478
|
1611 |
%
|
neuper@42478
|
1612 |
% \subsubsection{Trials on Notation and Termination}
|
neuper@42478
|
1613 |
%
|
neuper@42478
|
1614 |
% \paragraph{Technical notations} are a big problem for our piece of software,
|
neuper@42478
|
1615 |
% but the reason for that isn't a fault of the software itself, one of the
|
neuper@42478
|
1616 |
% troubles comes out of the fact that different technical subtopics use different
|
neuper@42478
|
1617 |
% symbols and notations for a different purpose. The most famous example for such
|
neuper@42478
|
1618 |
% a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
|
neuper@42478
|
1619 |
% math). In the specific part of signal processing one of this notation issues is
|
neuper@42478
|
1620 |
% the use of brackets --- we use round brackets for analoge signals and squared
|
neuper@42478
|
1621 |
% brackets for digital samples. Also if there is no problem for us to handle this
|
neuper@42478
|
1622 |
% fact, we have to tell the machine what notation leads to wich meaning and that
|
neuper@42478
|
1623 |
% this purpose seperation is only valid for this special topic - signal
|
neuper@42478
|
1624 |
% processing.
|
neuper@42478
|
1625 |
% \subparagraph{In the programming language} itself it is not possible to declare
|
neuper@42478
|
1626 |
% fractions, exponents, absolutes and other operators or remarks in a way to make
|
neuper@42478
|
1627 |
% them pretty to read; our only posssiblilty were ASCII characters and a handfull
|
neuper@42478
|
1628 |
% greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
|
neuper@42478
|
1629 |
% \par
|
neuper@42478
|
1630 |
% With the upper collected knowledge it is possible to check if we were able to
|
neuper@42478
|
1631 |
% donate all required terms and expressions.
|
neuper@42478
|
1632 |
%
|
neuper@42478
|
1633 |
% \subsubsection{Definition and Usage of Rules}
|
neuper@42478
|
1634 |
%
|
neuper@42478
|
1635 |
% \paragraph{The core} of our implemented problem is the Z-Transformation, due
|
neuper@42478
|
1636 |
% the fact that the transformation itself would require higher math which isn't
|
neuper@42478
|
1637 |
% yet avaible in our system we decided to choose the way like it is applied in
|
neuper@42478
|
1638 |
% labratory and problem classes at our university - by applying transformation
|
neuper@42478
|
1639 |
% rules (collected in transformation tables).
|
neuper@42478
|
1640 |
% \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
|
neuper@42478
|
1641 |
% use of axiomatizations like shown in Example~\ref{eg:ruledef}
|
neuper@42478
|
1642 |
%
|
neuper@42478
|
1643 |
% \begin{example}
|
neuper@42478
|
1644 |
% \label{eg:ruledef}
|
neuper@42478
|
1645 |
% \hfill\\
|
neuper@42478
|
1646 |
% \begin{verbatim}
|
neuper@42478
|
1647 |
% axiomatization where
|
neuper@42478
|
1648 |
% rule1: ``1 = $\delta$[n]'' and
|
neuper@42478
|
1649 |
% rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
|
neuper@42478
|
1650 |
% rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
|
neuper@42478
|
1651 |
% \end{verbatim}
|
neuper@42478
|
1652 |
% \end{example}
|
neuper@42478
|
1653 |
%
|
neuper@42478
|
1654 |
% This rules can be collected in a ruleset and applied to a given expression as
|
neuper@42478
|
1655 |
% follows in Example~\ref{eg:ruleapp}.
|
neuper@42478
|
1656 |
%
|
neuper@42478
|
1657 |
% \begin{example}
|
neuper@42478
|
1658 |
% \hfill\\
|
neuper@42478
|
1659 |
% \label{eg:ruleapp}
|
neuper@42478
|
1660 |
% \begin{enumerate}
|
neuper@42478
|
1661 |
% \item Store rules in ruleset:
|
neuper@42478
|
1662 |
% \begin{verbatim}
|
neuper@42478
|
1663 |
% val inverse_Z = append_rls "inverse_Z" e_rls
|
neuper@42478
|
1664 |
% [ Thm ("rule1",num_str @{thm rule1}),
|
neuper@42478
|
1665 |
% Thm ("rule2",num_str @{thm rule2}),
|
neuper@42478
|
1666 |
% Thm ("rule3",num_str @{thm rule3})
|
neuper@42478
|
1667 |
% ];\end{verbatim}
|
neuper@42478
|
1668 |
% \item Define exression:
|
neuper@42478
|
1669 |
% \begin{verbatim}
|
neuper@42478
|
1670 |
% val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
|
neuper@42478
|
1671 |
% \item Apply ruleset:
|
neuper@42478
|
1672 |
% \begin{verbatim}
|
neuper@42478
|
1673 |
% val SOME (sample_term', asm) =
|
neuper@42478
|
1674 |
% rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
|
neuper@42478
|
1675 |
% \end{enumerate}
|
neuper@42478
|
1676 |
% \end{example}
|
neuper@42478
|
1677 |
%
|
neuper@42478
|
1678 |
% The use of rulesets makes it much easier to develop our designated applications,
|
neuper@42478
|
1679 |
% but the programmer has to be careful and patient. When applying rulesets
|
neuper@42478
|
1680 |
% two important issues have to be mentionend:
|
neuper@42478
|
1681 |
% \subparagraph{How often} the rules have to be applied? In case of
|
neuper@42478
|
1682 |
% transformations it is quite clear that we use them once but other fields
|
neuper@42478
|
1683 |
% reuqire to apply rules until a special condition is reached (e.g.
|
neuper@42478
|
1684 |
% a simplification is finished when there is nothing to be done left).
|
neuper@42478
|
1685 |
% \subparagraph{The order} in which rules are applied often takes a big effect
|
neuper@42478
|
1686 |
% and has to be evaluated for each purpose once again.
|
neuper@42478
|
1687 |
% \par
|
neuper@42478
|
1688 |
% In our special case of Signal Processing and the rules defined in
|
neuper@42478
|
1689 |
% Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
|
neuper@42478
|
1690 |
% constants. After this step has been done it no mather which rule fit's next.
|
neuper@42478
|
1691 |
%
|
neuper@42478
|
1692 |
% \subsubsection{Helping Functions}
|
neuper@42478
|
1693 |
%
|
neuper@42478
|
1694 |
% \paragraph{New Programms require,} often new ways to get through. This new ways
|
neuper@42478
|
1695 |
% means that we handle functions that have not been in use yet, they can be
|
neuper@42478
|
1696 |
% something special and unique for a programm or something famous but unneeded in
|
neuper@42478
|
1697 |
% the system yet. In our dedicated example it was for example neccessary to split
|
neuper@42478
|
1698 |
% a fraction into numerator and denominator; the creation of such function and
|
neuper@42478
|
1699 |
% even others is described in upper Sections~\ref{simp} and \ref{funs}.
|
neuper@42478
|
1700 |
%
|
neuper@42478
|
1701 |
% \subsubsection{Trials on equation solving}
|
neuper@42478
|
1702 |
% %simple eq and problem with double fractions/negative exponents
|
neuper@42478
|
1703 |
% \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
|
neuper@42478
|
1704 |
% equations degree one and two. Solving equations in the first degree is no
|
neuper@42478
|
1705 |
% problem, wether for a student nor for our machine; but even second degree
|
neuper@42478
|
1706 |
% equations can lead to big troubles. The origin of this troubles leads from
|
neuper@42478
|
1707 |
% the build up process of our equation solving functions; they have been
|
neuper@42478
|
1708 |
% implemented some time ago and of course they are not as good as we want them to
|
neuper@42478
|
1709 |
% be. Wether or not following we only want to show how cruel it is to build up new
|
neuper@42478
|
1710 |
% work on not well fundamentials.
|
neuper@42478
|
1711 |
% \subparagraph{A simple equation solving,} can be set up as shown in the next
|
neuper@42478
|
1712 |
% example:
|
neuper@42478
|
1713 |
%
|
neuper@42478
|
1714 |
% \begin{example}
|
neuper@42478
|
1715 |
% \begin{verbatim}
|
neuper@42478
|
1716 |
%
|
neuper@42478
|
1717 |
% val fmz =
|
neuper@42478
|
1718 |
% ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
|
neuper@42478
|
1719 |
% "solveFor z",
|
neuper@42478
|
1720 |
% "solutions L"];
|
neuper@42478
|
1721 |
%
|
neuper@42478
|
1722 |
% val (dI',pI',mI') =
|
neuper@42478
|
1723 |
% ("Isac",
|
neuper@42478
|
1724 |
% ["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@42478
|
1725 |
% ["no_met"]);\end{verbatim}
|
neuper@42478
|
1726 |
% \end{example}
|
neuper@42478
|
1727 |
%
|
neuper@42478
|
1728 |
% Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
|
neuper@42478
|
1729 |
% a short overview on the commands; at first we set up the equation and tell the
|
neuper@42478
|
1730 |
% machine what's the bound variable and where to store the solution. Second step
|
neuper@42478
|
1731 |
% is to define the equation type and determine if we want to use a special method
|
neuper@42478
|
1732 |
% to solve this type.) Simple checks tell us that the we will get two results for
|
neuper@42478
|
1733 |
% this equation and this results will be real.
|
neuper@42478
|
1734 |
% So far it is easy for us and for our machine to solve, but
|
neuper@42478
|
1735 |
% mentioned that a unvariate equation second order can have three different types
|
neuper@42478
|
1736 |
% of solutions it is getting worth.
|
neuper@42478
|
1737 |
% \subparagraph{The solving of} all this types of solutions is not yet supported.
|
neuper@42478
|
1738 |
% Luckily it was needed for us; but something which has been needed in this
|
neuper@42478
|
1739 |
% context, would have been the solving of an euation looking like:
|
neuper@42478
|
1740 |
% $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
|
neuper@42478
|
1741 |
% before (remember that befor it was no problem to handle for the machine) but
|
neuper@42478
|
1742 |
% now, after a simple equivalent transformation, we are not able to solve
|
neuper@42478
|
1743 |
% it anymore.
|
neuper@42478
|
1744 |
% \subparagraph{Error messages} we get when we try to solve something like upside
|
neuper@42478
|
1745 |
% were very confusing and also leads us to no special hint about a problem.
|
neuper@42478
|
1746 |
% \par The fault behind is, that we have no well error handling on one side and
|
neuper@42478
|
1747 |
% no sufficient formed equation solving on the other side. This two facts are
|
neuper@42478
|
1748 |
% making the implemention of new material very difficult.
|
neuper@42478
|
1749 |
%
|
neuper@42478
|
1750 |
% \subsection{Formalization of missing knowledge in Isabelle}
|
neuper@42478
|
1751 |
%
|
neuper@42478
|
1752 |
% \paragraph{A problem} behind is the mechanization of mathematic
|
neuper@42478
|
1753 |
% theories in TP-bases languages. There is still a huge gap between
|
neuper@42478
|
1754 |
% these algorithms and this what we want as a solution - in Example
|
neuper@42478
|
1755 |
% Signal Processing.
|
neuper@42478
|
1756 |
%
|
neuper@42478
|
1757 |
% \vbox{
|
neuper@42478
|
1758 |
% \begin{example}
|
neuper@42478
|
1759 |
% \label{eg:gap}
|
neuper@42478
|
1760 |
% \[
|
neuper@42478
|
1761 |
% X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
|
neuper@42478
|
1762 |
% \]
|
neuper@42478
|
1763 |
% {\small\textit{
|
neuper@42478
|
1764 |
% \noindent A very simple example on this what we call gap is the
|
neuper@42478
|
1765 |
% simplification above. It is needles to say that it is correct and also
|
neuper@42478
|
1766 |
% Isabelle for fills it correct - \emph{always}. But sometimes we don't
|
neuper@42478
|
1767 |
% want expand such terms, sometimes we want another structure of
|
neuper@42478
|
1768 |
% them. Think of a problem were we now would need only the coefficients
|
neuper@42478
|
1769 |
% of $X$ and $Y$. This is what we call the gap between mechanical
|
neuper@42478
|
1770 |
% simplification and the solution.
|
neuper@42478
|
1771 |
% }}
|
neuper@42478
|
1772 |
% \end{example}
|
neuper@42478
|
1773 |
% }
|
neuper@42478
|
1774 |
%
|
neuper@42478
|
1775 |
% \paragraph{We are not able to fill this gap,} until we have to live
|
neuper@42478
|
1776 |
% with it but first have a look on the meaning of this statement:
|
neuper@42478
|
1777 |
% Mechanized math starts from mathematical models and \emph{hopefully}
|
neuper@42478
|
1778 |
% proceeds to match physics. Academic engineering starts from physics
|
neuper@42478
|
1779 |
% (experimentation, measurement) and then proceeds to mathematical
|
neuper@42478
|
1780 |
% modeling and formalization. The process from a physical observance to
|
neuper@42478
|
1781 |
% a mathematical theory is unavoidable bound of setting up a big
|
neuper@42478
|
1782 |
% collection of standards, rules, definition but also exceptions. These
|
neuper@42478
|
1783 |
% are the things making mechanization that difficult.
|
neuper@42478
|
1784 |
%
|
neuper@42478
|
1785 |
% \vbox{
|
neuper@42478
|
1786 |
% \begin{example}
|
neuper@42478
|
1787 |
% \label{eg:units}
|
neuper@42478
|
1788 |
% \[
|
neuper@42478
|
1789 |
% m,\ kg,\ s,\ldots
|
neuper@42478
|
1790 |
% \]
|
neuper@42478
|
1791 |
% {\small\textit{
|
neuper@42478
|
1792 |
% \noindent Think about some units like that one's above. Behind
|
neuper@42478
|
1793 |
% each unit there is a discerning and very accurate definition: One
|
neuper@42478
|
1794 |
% Meter is the distance the light travels, in a vacuum, through the time
|
neuper@42478
|
1795 |
% of 1 / 299.792.458 second; one kilogram is the weight of a
|
neuper@42478
|
1796 |
% platinum-iridium cylinder in paris; and so on. But are these
|
neuper@42478
|
1797 |
% definitions usable in a computer mechanized world?!
|
neuper@42478
|
1798 |
% }}
|
neuper@42478
|
1799 |
% \end{example}
|
neuper@42478
|
1800 |
% }
|
neuper@42478
|
1801 |
%
|
neuper@42478
|
1802 |
% \paragraph{A computer} or a TP-System builds on programs with
|
neuper@42478
|
1803 |
% predefined logical rules and does not know any mathematical trick
|
neuper@42478
|
1804 |
% (follow up example \ref{eg:trick}) or recipe to walk around difficult
|
neuper@42478
|
1805 |
% expressions.
|
neuper@42478
|
1806 |
%
|
neuper@42478
|
1807 |
% \vbox{
|
neuper@42478
|
1808 |
% \begin{example}
|
neuper@42478
|
1809 |
% \label{eg:trick}
|
neuper@42478
|
1810 |
% \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
|
neuper@42478
|
1811 |
% \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
|
neuper@42478
|
1812 |
% \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
|
neuper@42478
|
1813 |
% \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
|
neuper@42478
|
1814 |
% {\small\textit{
|
neuper@42478
|
1815 |
% \noindent Sometimes it is also useful to be able to apply some
|
neuper@42478
|
1816 |
% \emph{tricks} to get a beautiful and particularly meaningful result,
|
neuper@42478
|
1817 |
% which we are able to interpret. But as seen in this example it can be
|
neuper@42478
|
1818 |
% hard to find out what operations have to be done to transform a result
|
neuper@42478
|
1819 |
% into a meaningful one.
|
neuper@42478
|
1820 |
% }}
|
neuper@42478
|
1821 |
% \end{example}
|
neuper@42478
|
1822 |
% }
|
neuper@42478
|
1823 |
%
|
neuper@42478
|
1824 |
% \paragraph{The only possibility,} for such a system, is to work
|
neuper@42478
|
1825 |
% through its known definitions and stops if none of these
|
neuper@42478
|
1826 |
% fits. Specified on Signal Processing or any other application it is
|
neuper@42478
|
1827 |
% often possible to walk through by doing simple creases. This creases
|
neuper@42478
|
1828 |
% are in general based on simple math operational but the challenge is
|
neuper@42478
|
1829 |
% to teach the machine \emph{all}\footnote{Its pride to call it
|
neuper@42478
|
1830 |
% \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
|
neuper@42478
|
1831 |
% reach a high level of \emph{all} but it in real it will still be a
|
neuper@42478
|
1832 |
% survey of knowledge which links to other knowledge and {{\sisac}{}} a
|
neuper@42478
|
1833 |
% trainer and helper but no human compensating calculator.
|
neuper@42478
|
1834 |
% \par
|
neuper@42478
|
1835 |
% {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
|
neuper@42478
|
1836 |
% specifications of problems out of topics from Signal Processing, etc.)
|
neuper@42478
|
1837 |
% and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
|
neuper@42478
|
1838 |
% physical knowledge. The result is a three-dimensional universe of
|
neuper@42478
|
1839 |
% mathematics seen in Figure~\ref{fig:mathuni}.
|
neuper@42478
|
1840 |
%
|
neuper@42478
|
1841 |
% \begin{figure}
|
neuper@42478
|
1842 |
% \begin{center}
|
neuper@42478
|
1843 |
% \includegraphics{fig/universe}
|
neuper@42478
|
1844 |
% \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
|
neuper@42478
|
1845 |
% combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
|
neuper@42478
|
1846 |
% leads to a three dimensional math universe.\label{fig:mathuni}}
|
neuper@42478
|
1847 |
% \end{center}
|
neuper@42478
|
1848 |
% \end{figure}
|
neuper@42478
|
1849 |
%
|
neuper@42478
|
1850 |
% %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
|
neuper@42478
|
1851 |
% %WN bitte folgende Bezeichnungen nehmen:
|
neuper@42478
|
1852 |
% %WN
|
neuper@42478
|
1853 |
% %WN axis 1: Algorithmic Knowledge (Programs)
|
neuper@42478
|
1854 |
% %WN axis 2: Application-oriented Knowledge (Specifications)
|
neuper@42478
|
1855 |
% %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
|
neuper@42478
|
1856 |
% %WN
|
neuper@42478
|
1857 |
% %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
|
neuper@42478
|
1858 |
% %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
|
neuper@42478
|
1859 |
% %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
|
neuper@42478
|
1860 |
%
|
neuper@42478
|
1861 |
% %JR Rรคnder und beschriftung geรคndert. Keine Ahnung warum eJMT sich pdf's
|
neuper@42478
|
1862 |
% %JR wรผnschen, wรผrde ebenfalls png oder รคhnliches verwenden, aber wenn pdf's
|
neuper@42478
|
1863 |
% %JR gefordert werden WN2...
|
neuper@42478
|
1864 |
% %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
|
neuper@42478
|
1865 |
% %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
|
neuper@42478
|
1866 |
% %WN2 zusammenschneiden um die R"ander weg zu bekommen)
|
neuper@42478
|
1867 |
% %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
|
neuper@42478
|
1868 |
% %WN2 png + pdf figures mitzuschicken.
|
neuper@42478
|
1869 |
%
|
neuper@42478
|
1870 |
% \subsection{Notes on Problems with Traditional Notation}
|
neuper@42478
|
1871 |
%
|
neuper@42478
|
1872 |
% \paragraph{During research} on these topic severely problems on
|
neuper@42478
|
1873 |
% traditional notations have been discovered. Some of them have been
|
neuper@42478
|
1874 |
% known in computer science for many years now and are still unsolved,
|
neuper@42478
|
1875 |
% one of them aggregates with the so called \emph{Lambda Calculus},
|
neuper@42478
|
1876 |
% Example~\ref{eg:lamda} provides a look on the problem that embarrassed
|
neuper@42478
|
1877 |
% us.
|
neuper@42478
|
1878 |
%
|
neuper@42478
|
1879 |
% \vbox{
|
neuper@42478
|
1880 |
% \begin{example}
|
neuper@42478
|
1881 |
% \label{eg:lamda}
|
neuper@42478
|
1882 |
%
|
neuper@42478
|
1883 |
% \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
|
neuper@42478
|
1884 |
%
|
neuper@42478
|
1885 |
%
|
neuper@42478
|
1886 |
% \[ f(p)=\ldots\; p \in \quad R \]
|
neuper@42478
|
1887 |
%
|
neuper@42478
|
1888 |
% {\small\textit{
|
neuper@42478
|
1889 |
% \noindent Above we see two equations. The first equation aims to
|
neuper@42478
|
1890 |
% be a mapping of an function from the reel range to the reel one, but
|
neuper@42478
|
1891 |
% when we change only one letter we get the second equation which
|
neuper@42478
|
1892 |
% usually aims to insert a reel point $p$ into the reel function. In
|
neuper@42478
|
1893 |
% computer science now we have the problem to tell the machine (TP) the
|
neuper@42478
|
1894 |
% difference between this two notations. This Problem is called
|
neuper@42478
|
1895 |
% \emph{Lambda Calculus}.
|
neuper@42478
|
1896 |
% }}
|
neuper@42478
|
1897 |
% \end{example}
|
neuper@42478
|
1898 |
% }
|
neuper@42478
|
1899 |
%
|
neuper@42478
|
1900 |
% \paragraph{An other problem} is that terms are not full simplified in
|
neuper@42478
|
1901 |
% traditional notations, in {{\sisac}} we have to simplify them complete
|
neuper@42478
|
1902 |
% to check weather results are compatible or not. in e.g. the solutions
|
neuper@42478
|
1903 |
% of an second order linear equation is an rational in {{\sisac}} but in
|
neuper@42478
|
1904 |
% tradition we keep fractions as long as possible and as long as they
|
neuper@42478
|
1905 |
% aim to be \textit{beautiful} (1/8, 5/16,...).
|
neuper@42478
|
1906 |
% \subparagraph{The math} which should be mechanized in Computer Theorem
|
neuper@42478
|
1907 |
% Provers (\emph{TP}) has (almost) a problem with traditional notations
|
neuper@42478
|
1908 |
% (predicate calculus) for axioms, definitions, lemmas, theorems as a
|
neuper@42478
|
1909 |
% computer program or script is not able to interpret every Greek or
|
neuper@42478
|
1910 |
% Latin letter and every Greek, Latin or whatever calculations
|
neuper@42478
|
1911 |
% symbol. Also if we would be able to handle these symbols we still have
|
neuper@42478
|
1912 |
% a problem to interpret them at all. (Follow up \hbox{Example
|
neuper@42478
|
1913 |
% \ref{eg:symbint1}})
|
neuper@42478
|
1914 |
%
|
neuper@42478
|
1915 |
% \vbox{
|
neuper@42478
|
1916 |
% \begin{example}
|
neuper@42478
|
1917 |
% \label{eg:symbint1}
|
neuper@42478
|
1918 |
% \[
|
neuper@42478
|
1919 |
% u\left[n\right] \ \ldots \ unitstep
|
neuper@42478
|
1920 |
% \]
|
neuper@42478
|
1921 |
% {\small\textit{
|
neuper@42478
|
1922 |
% \noindent The unitstep is something we need to solve Signal
|
neuper@42478
|
1923 |
% Processing problem classes. But in {{{\sisac}{}}} the rectangular
|
neuper@42478
|
1924 |
% brackets have a different meaning. So we abuse them for our
|
neuper@42478
|
1925 |
% requirements. We get something which is not defined, but usable. The
|
neuper@42478
|
1926 |
% Result is syntax only without semantic.
|
neuper@42478
|
1927 |
% }}
|
neuper@42478
|
1928 |
% \end{example}
|
neuper@42478
|
1929 |
% }
|
neuper@42478
|
1930 |
%
|
neuper@42478
|
1931 |
% In different problems, symbols and letters have different meanings and
|
neuper@42478
|
1932 |
% ask for different ways to get through. (Follow up \hbox{Example
|
neuper@42478
|
1933 |
% \ref{eg:symbint2}})
|
neuper@42478
|
1934 |
%
|
neuper@42478
|
1935 |
% \vbox{
|
neuper@42478
|
1936 |
% \begin{example}
|
neuper@42478
|
1937 |
% \label{eg:symbint2}
|
neuper@42478
|
1938 |
% \[
|
neuper@42478
|
1939 |
% \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
|
neuper@42478
|
1940 |
% \]
|
neuper@42478
|
1941 |
% {\small\textit{
|
neuper@42478
|
1942 |
% \noindent For using exponents the three \texttt{widehat} symbols
|
neuper@42478
|
1943 |
% are required. The reason for that is due the development of
|
neuper@42478
|
1944 |
% {{{\sisac}{}}} the single \texttt{widehat} and also the double were
|
neuper@42478
|
1945 |
% already in use for different operations.
|
neuper@42478
|
1946 |
% }}
|
neuper@42478
|
1947 |
% \end{example}
|
neuper@42478
|
1948 |
% }
|
neuper@42478
|
1949 |
%
|
neuper@42478
|
1950 |
% \paragraph{Also the output} can be a problem. We are familiar with a
|
neuper@42478
|
1951 |
% specified notations and style taught in university but a computer
|
neuper@42478
|
1952 |
% program has no knowledge of the form proved by a professor and the
|
neuper@42478
|
1953 |
% machines themselves also have not yet the possibilities to print every
|
neuper@42478
|
1954 |
% symbol (correct) Recent developments provide proofs in a human
|
neuper@42478
|
1955 |
% readable format but according to the fact that there is no money for
|
neuper@42478
|
1956 |
% good working formal editors yet, the style is one thing we have to
|
neuper@42478
|
1957 |
% live with.
|
neuper@42478
|
1958 |
%
|
neuper@42478
|
1959 |
% \section{Problems rising out of the Development Environment}
|
neuper@42478
|
1960 |
%
|
neuper@42478
|
1961 |
% fehlermeldungen! TODO
|
jan@42463
|
1962 |
|
neuper@42492
|
1963 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
|
neuper@42492
|
1964 |
|
neuper@48771
|
1965 |
\section{Summary and Conclusions}\label{conclusion}
|
jan@42463
|
1966 |
|
jan@42512
|
1967 |
%JR obvious
|
jan@42512
|
1968 |
|
jan@42512
|
1969 |
%This paper gives a first experience report about programming with a
|
jan@42512
|
1970 |
%TP-based programming language.
|
jan@42512
|
1971 |
|
jan@42512
|
1972 |
A brief re-introduction of the novel kind of programming
|
neuper@42492
|
1973 |
language by example of the {\sisac}-prototype makes the paper
|
neuper@42492
|
1974 |
self-contained. The main section describes all the main concepts
|
neuper@42492
|
1975 |
involved in TP-based programming and all the sub-tasks concerning
|
neuper@48771
|
1976 |
respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain
|
neuper@42514
|
1977 |
modeling, implementation of term rewriting systems for the
|
neuper@42492
|
1978 |
rewriting-engine, formal (implicit) specification of the problem to be
|
neuper@42507
|
1979 |
(explicitly) described by the program, implementation of the many components
|
neuper@42492
|
1980 |
required for Lucas-Interpretation and finally implementation of the
|
neuper@42492
|
1981 |
program itself.
|
neuper@42492
|
1982 |
|
neuper@42492
|
1983 |
The many concepts and sub-tasks involved in programming require a
|
neuper@42514
|
1984 |
comprehensive work-flow; first experiences with the work-flow as
|
neuper@42492
|
1985 |
supported by the present prototype are described as well: Isabelle +
|
neuper@42492
|
1986 |
Isar + jEdit provide appropriate components for establishing an
|
neuper@42492
|
1987 |
efficient development environment integrating computation and
|
neuper@42492
|
1988 |
deduction. However, the present state of the prototype is far off a
|
neuper@42492
|
1989 |
state appropriate for wide-spread use: the prototype of the program
|
neuper@42492
|
1990 |
language lacks expressiveness and elegance, the prototype of the
|
neuper@42492
|
1991 |
development environment is hardly usable: error messages still address
|
neuper@42492
|
1992 |
the developer of the prototype's interpreter rather than the
|
neuper@42492
|
1993 |
application programmer, implementation of the many settings for the
|
neuper@48771
|
1994 |
Lucas-Interpreter is cumbersome.
|
neuper@42492
|
1995 |
|
neuper@48773
|
1996 |
\subsection{Conclusions for Future Development}
|
neuper@48771
|
1997 |
From the above mentioned experiences a successful proof of concept can be concluded:
|
neuper@42492
|
1998 |
programming arbitrary problems from engineering sciences is possible,
|
neuper@42492
|
1999 |
in principle even in the prototype. Furthermore the experiences allow
|
neuper@42492
|
2000 |
to conclude detailed requirements for further development:
|
neuper@48771
|
2001 |
\begin{enumerate}
|
neuper@42492
|
2002 |
\item Clarify underlying logics such that programming is smoothly
|
neuper@42492
|
2003 |
integrated with verification of the program; the post-condition should
|
neuper@42492
|
2004 |
be proved more or less automatically, otherwise working engineers
|
neuper@42492
|
2005 |
would not encounter such programming.
|
neuper@42492
|
2006 |
\item Combine the prototype's programming language with Isabelle's
|
neuper@42492
|
2007 |
powerful function package and probably with more of SML's
|
neuper@42492
|
2008 |
pattern-matching features; include parallel execution on multi-core
|
jan@42511
|
2009 |
machines into the language design.
|
neuper@42492
|
2010 |
\item Extend the prototype's Lucas-Interpreter such that it also
|
neuper@42492
|
2011 |
handles functions defined by use of Isabelle's functions package; and
|
neuper@42492
|
2012 |
generalize Isabelle's code generator such that efficient code for the
|
neuper@42507
|
2013 |
whole definition of the programming language can be generated (for
|
neuper@42492
|
2014 |
multi-core machines).
|
neuper@42492
|
2015 |
\item Develop an efficient development environment with
|
neuper@42492
|
2016 |
integration of programming and proving, with management not only of
|
neuper@42492
|
2017 |
Isabelle theories, but also of large collections of specifications and
|
neuper@42492
|
2018 |
of programs.
|
neuper@48771
|
2019 |
\item\label{CAS} Extend Isabelle's computational features in direction of
|
neuper@48771
|
2020 |
\textit{verfied} Computer Algebra: simplification extended by
|
neuper@48771
|
2021 |
algorithms beyond rewriting (cancellation of multivariate rationals,
|
neuper@48771
|
2022 |
factorisation, partial fraction decomposition, etc), equation solving
|
neuper@48771
|
2023 |
, integration, etc.
|
neuper@48771
|
2024 |
\end{enumerate}
|
neuper@42492
|
2025 |
Provided successful accomplishment, these points provide distinguished
|
neuper@48771
|
2026 |
components for virtual workbenches appealing to practitioners of
|
neuper@42492
|
2027 |
engineering in the near future.
|
neuper@42492
|
2028 |
|
neuper@48771
|
2029 |
\subsection{Preview to Development of Course Material}
|
neuper@48771
|
2030 |
Interactive course material, as addressed by the title,
|
neuper@42507
|
2031 |
can comprise step-wise problem solving created as a side-effect of a
|
neuper@48771
|
2032 |
TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an
|
neuper@42507
|
2033 |
interactive programming environment, Lucas-Interpretation also can
|
jan@42511
|
2034 |
provide TP-based services for a flexible dialogue component with
|
neuper@42507
|
2035 |
adaptive user guidance for independent and inquiry-based learning.
|
neuper@42492
|
2036 |
|
neuper@48771
|
2037 |
However, the {\sisac} prototype is not ready for use in field-tests,
|
neuper@48771
|
2038 |
not only due to the above five requirements not sufficiently
|
neuper@48771
|
2039 |
accomplished, but also due to usability of the fron-end, in particular
|
neuper@48771
|
2040 |
the lack of an editor for formulas in 2-dimension representation.
|
neuper@48771
|
2041 |
|
neuper@48771
|
2042 |
Nevertheless, the experiences from the case study described in this
|
neuper@48771
|
2043 |
paper, allow to give a preview to the development of course material,
|
neuper@48771
|
2044 |
if based on Lucas-Interpretation:
|
neuper@48771
|
2045 |
|
neuper@48771
|
2046 |
\paragraph{Development of material from scratch} is too much effort
|
neuper@48771
|
2047 |
just for e-learning; this has become clear with the case study. For
|
neuper@48771
|
2048 |
getting support for stepwise problem solving just in {\em one} example
|
neuper@48771
|
2049 |
class, the one presented in this paper, involved the following tasks:
|
neuper@48771
|
2050 |
\begin{itemize}
|
neuper@48771
|
2051 |
\item Adapt the equation solver; since that was too laborous, the
|
neuper@48771
|
2052 |
program has been adapted in an unelegant way.
|
neuper@48771
|
2053 |
\item Implement an algorithms for partial fraction decomposition,
|
neuper@48771
|
2054 |
which is considered a standard normal form in Computer Algebra.
|
neuper@48771
|
2055 |
\item Implement a specification for partial fraction decomposition and
|
neuper@48771
|
2056 |
locate it appropriately in the hierarchy of specification.
|
jan@48774
|
2057 |
\item Declare definitions and theorems within the theory of
|
jan@48774
|
2058 |
${\cal Z}$-transform, and prove the theorems (which was not done in the
|
neuper@48771
|
2059 |
case study).
|
neuper@48771
|
2060 |
\end{itemize}
|
neuper@48771
|
2061 |
On the other hand, for the one the class of problems implemented,
|
neuper@48771
|
2062 |
adding an arbitrary number of examples within this class requires a
|
neuper@48771
|
2063 |
few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an
|
neuper@48771
|
2064 |
example is called from an HTML-file by an URL, which addresses an
|
neuper@48771
|
2065 |
XML-structure holding the respective data as shown on
|
neuper@48771
|
2066 |
p.\pageref{ml-check-program}.} and the support for individual stepwise
|
neuper@48771
|
2067 |
problem solving comes for free.
|
neuper@48771
|
2068 |
|
neuper@48771
|
2069 |
\paragraph{E-learning benefits from Formal Domain Engineering} which can be
|
neuper@48771
|
2070 |
expected for various domains in the near future. In order to cope with
|
neuper@48771
|
2071 |
increasing complexity in domain of technology, specific domain
|
neuper@48771
|
2072 |
knowledge is beeing mechanised, not only for software technology
|
neuper@48771
|
2073 |
\footnote{For instance, the Archive of Formal Proofs
|
neuper@48771
|
2074 |
http://afp.sourceforge.net/} but also for other engineering domains
|
neuper@48771
|
2075 |
\cite{Dehbonei&94,Hansen94b,db:dom-eng}. This fairly new part of
|
neuper@48771
|
2076 |
engineering sciences is called ``domain engineering'' in
|
neuper@48771
|
2077 |
\cite{db:SW-engIII}.
|
neuper@48771
|
2078 |
|
neuper@48771
|
2079 |
Given this kind of mechanised knowledge including mathematical
|
neuper@48771
|
2080 |
theories, domain specific definitions, specifications and algorithms,
|
neuper@48771
|
2081 |
theorems and proofs, then e-learning with support for individual
|
neuper@48771
|
2082 |
stepwise problem solving will not be much ado anymore; then e-learning
|
neuper@48771
|
2083 |
media in technology education can be derived from this knowledge with
|
neuper@48771
|
2084 |
reasonable effort.
|
neuper@48771
|
2085 |
|
neuper@48771
|
2086 |
\paragraph{Development differentiates into tasks} more separated than
|
neuper@48771
|
2087 |
without Lucas-Interpretation and more challenginging in specific
|
neuper@48771
|
2088 |
expertise. These are the kinds of experts expected to cooperate in
|
neuper@48771
|
2089 |
development of
|
neuper@48771
|
2090 |
\begin{itemize}
|
neuper@48773
|
2091 |
\item ``Domain engineers'', who accomplish fairly novel tasks
|
neuper@48773
|
2092 |
described in this paper.
|
neuper@48771
|
2093 |
\item Course designers, who provide the instructional design according
|
neuper@48771
|
2094 |
to curricula, together with usability experts and media designers, are
|
neuper@48771
|
2095 |
indispensable in production of e-learning media at the state-of-the
|
neuper@48771
|
2096 |
art.
|
neuper@48771
|
2097 |
\item ``Dialog designers'', whose part of development is clearly
|
neuper@48773
|
2098 |
separated from the part of domain engineers as a consequence of
|
neuper@48773
|
2099 |
Lucas-Interpretation: TP-based programs are functional, as mentioned,
|
neuper@48773
|
2100 |
and are only concerned with describing mathematics --- and not at all
|
neuper@48773
|
2101 |
concerned with interaction, psychology, learning theory and the like,
|
neuper@48773
|
2102 |
because there are no in/output statements. Dialog designers can expect
|
neuper@48773
|
2103 |
a high-level rule-based language~\cite{gdaroczy-EP-13} for describing
|
neuper@48773
|
2104 |
their part.
|
neuper@48771
|
2105 |
\end{itemize}
|
neuper@48771
|
2106 |
|
neuper@48771
|
2107 |
% response-to-referees:
|
neuper@48771
|
2108 |
% (2.1) details of novel technology in order to estimate the impact
|
neuper@48771
|
2109 |
% (2.2) which kinds of expertise are required for production of e-learning media (instructional design, math authoring, dialog authoring, media design)
|
neuper@48771
|
2110 |
% (2.3) what in particular is required for programming new exercises supported by next-step-guidance (expertise / efforts)
|
neuper@48771
|
2111 |
% (2.4) estimation of break-even points for development of next-step-guidance
|
neuper@48771
|
2112 |
% (2.5) usability of ISAC prototype at the present state
|
neuper@48771
|
2113 |
%
|
neuper@48771
|
2114 |
% The points (1.*) seem to be well covered in the paper, the points (2.*) are not. So I decided to address the points (2.*) in a separate section ยง5.1."".
|
neuper@48771
|
2115 |
|
neuper@48773
|
2116 |
\bigskip\noindent For this decade there seems to be a window of opportunity opening from
|
neuper@48771
|
2117 |
one side inreasing demand for formal domain engineering and from the
|
neuper@48771
|
2118 |
other side from TP more and more gaining industrial relevance. Within
|
neuper@48771
|
2119 |
this window, development of TP-based educational software can take
|
neuper@48775
|
2120 |
benefit from the fact, that the TPs leading in Europe, Coq~\cite{coq-team-10} and
|
neuper@48771
|
2121 |
Isabelle are still open source together with the major part of
|
neuper@48771
|
2122 |
mechanised knowledge.%~\footnote{NICTA}.
|
jan@42463
|
2123 |
|
jan@42463
|
2124 |
\bibliographystyle{alpha}
|
neuper@42507
|
2125 |
{\small\bibliography{references}}
|
jan@42463
|
2126 |
|
neuper@42514
|
2127 |
\end{document}
|
neuper@42514
|
2128 |
% LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
|
neuper@42514
|
2129 |
% LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised
|
neuper@42514
|
2130 |
% LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
|
neuper@42514
|
2131 |
% LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
|
neuper@42514
|
2132 |
% LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
|
neuper@42514
|
2133 |
% LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq
|
neuper@42514
|
2134 |
% LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
|
neuper@42514
|
2135 |
% LocalWords: mechanisation multi
|