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