jan@42463
|
1 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
2 |
% Electronic Journal of Mathematics and Technology (eJMT) %
|
jan@42463
|
3 |
% style sheet for LaTeX. Please do not modify sections %
|
jan@42463
|
4 |
% or commands marked 'eJMT'. %
|
jan@42463
|
5 |
% %
|
jan@42463
|
6 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
7 |
% %
|
jan@42463
|
8 |
% eJMT commands %
|
jan@42463
|
9 |
% %
|
jan@42463
|
10 |
\documentclass[12pt,a4paper]{article}% %
|
jan@42463
|
11 |
\usepackage{times} %
|
jan@42463
|
12 |
\usepackage{amsfonts,amsmath,amssymb} %
|
jan@42463
|
13 |
\usepackage[a4paper]{geometry} %
|
jan@42463
|
14 |
\usepackage{fancyhdr} %
|
jan@42463
|
15 |
\usepackage{color} %
|
jan@42463
|
16 |
\usepackage[pdftex]{hyperref} % see note below %
|
jan@42463
|
17 |
\usepackage{graphicx}% %
|
jan@42463
|
18 |
\hypersetup{ %
|
jan@42463
|
19 |
a4paper, %
|
jan@42463
|
20 |
breaklinks %
|
jan@42463
|
21 |
} %
|
jan@42463
|
22 |
% %
|
jan@42463
|
23 |
\newtheorem{theorem}{Theorem} %
|
jan@42463
|
24 |
\newtheorem{acknowledgement}[theorem]{Acknowledgement} %
|
jan@42463
|
25 |
\newtheorem{algorithm}[theorem]{Algorithm} %
|
jan@42463
|
26 |
\newtheorem{axiom}[theorem]{Axiom} %
|
jan@42463
|
27 |
\newtheorem{case}[theorem]{Case} %
|
jan@42463
|
28 |
\newtheorem{claim}[theorem]{Claim} %
|
jan@42463
|
29 |
\newtheorem{conclusion}[theorem]{Conclusion} %
|
jan@42463
|
30 |
\newtheorem{condition}[theorem]{Condition} %
|
jan@42463
|
31 |
\newtheorem{conjecture}[theorem]{Conjecture} %
|
jan@42463
|
32 |
\newtheorem{corollary}[theorem]{Corollary} %
|
jan@42463
|
33 |
\newtheorem{criterion}[theorem]{Criterion} %
|
jan@42463
|
34 |
\newtheorem{definition}[theorem]{Definition} %
|
jan@42463
|
35 |
\newtheorem{example}[theorem]{Example} %
|
jan@42463
|
36 |
\newtheorem{exercise}[theorem]{Exercise} %
|
jan@42463
|
37 |
\newtheorem{lemma}[theorem]{Lemma} %
|
jan@42463
|
38 |
\newtheorem{notation}[theorem]{Notation} %
|
jan@42463
|
39 |
\newtheorem{problem}[theorem]{Problem} %
|
jan@42463
|
40 |
\newtheorem{proposition}[theorem]{Proposition} %
|
jan@42463
|
41 |
\newtheorem{remark}[theorem]{Remark} %
|
jan@42463
|
42 |
\newtheorem{solution}[theorem]{Solution} %
|
jan@42463
|
43 |
\newtheorem{summary}[theorem]{Summary} %
|
jan@42463
|
44 |
\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} } %
|
jan@42463
|
45 |
{\ \rule{0.5em}{0.5em}} %
|
jan@42463
|
46 |
% %
|
jan@42463
|
47 |
% eJMT page dimensions %
|
jan@42463
|
48 |
% %
|
jan@42463
|
49 |
\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
|
jan@42463
|
50 |
% %
|
jan@42463
|
51 |
% eJMT header & footer %
|
jan@42463
|
52 |
% %
|
jan@42463
|
53 |
\newcounter{ejmtFirstpage} %
|
jan@42463
|
54 |
\setcounter{ejmtFirstpage}{1} %
|
jan@42463
|
55 |
\pagestyle{empty} %
|
jan@42463
|
56 |
\setlength{\headheight}{14pt} %
|
jan@42463
|
57 |
\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm} %
|
jan@42463
|
58 |
\pagestyle{fancyplain} %
|
jan@42463
|
59 |
\fancyhf{} %
|
jan@42463
|
60 |
\fancyhead[c]{\small The Electronic Journal of Mathematics%
|
jan@42463
|
61 |
\ and Technology, Volume 1, Number 1, ISSN 1933-2823} %
|
jan@42463
|
62 |
\cfoot{% %
|
jan@42463
|
63 |
\ifnum\value{ejmtFirstpage}=0% %
|
jan@42463
|
64 |
{\vtop to\hsize{\hrule\vskip .2cm\thepage}}% %
|
jan@42463
|
65 |
\else\setcounter{ejmtFirstpage}{0}\fi% %
|
jan@42463
|
66 |
} %
|
jan@42463
|
67 |
% %
|
jan@42463
|
68 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
69 |
%
|
jan@42463
|
70 |
% Please place your own definitions here
|
jan@42463
|
71 |
%
|
jan@42463
|
72 |
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
|
jan@42463
|
73 |
\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
|
jan@42463
|
74 |
|
jan@42463
|
75 |
\usepackage{color}
|
jan@42463
|
76 |
\definecolor{lgray}{RGB}{238,238,238}
|
jan@42463
|
77 |
|
jan@42463
|
78 |
%
|
jan@42463
|
79 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
80 |
% %
|
jan@42463
|
81 |
% How to use hyperref %
|
jan@42463
|
82 |
% ------------------- %
|
jan@42463
|
83 |
% %
|
jan@42463
|
84 |
% Probably the only way you will need to use the hyperref %
|
jan@42463
|
85 |
% package is as follows. To make some text, say %
|
jan@42463
|
86 |
% "My Text Link", into a link to the URL %
|
jan@42463
|
87 |
% http://something.somewhere.com/mystuff, use %
|
jan@42463
|
88 |
% %
|
jan@42463
|
89 |
% \href{http://something.somewhere.com/mystuff}{My Text Link}
|
jan@42463
|
90 |
% %
|
jan@42463
|
91 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
92 |
%
|
jan@42463
|
93 |
\begin{document}
|
jan@42463
|
94 |
%
|
jan@42463
|
95 |
% document title
|
jan@42463
|
96 |
%
|
neuper@42464
|
97 |
\title{Trials with TP-based Programming
|
neuper@42464
|
98 |
\\
|
neuper@42464
|
99 |
for Interactive Course Material}%
|
jan@42463
|
100 |
%
|
jan@42463
|
101 |
% Single author. Please supply at least your name,
|
jan@42463
|
102 |
% email address, and affiliation here.
|
jan@42463
|
103 |
%
|
jan@42463
|
104 |
\author{\begin{tabular}{c}
|
jan@42463
|
105 |
\textit{Jan Ro\v{c}nik} \\
|
jan@42463
|
106 |
jan.rocnik@student.tugraz.at \\
|
jan@42463
|
107 |
IST, SPSC\\
|
neuper@42464
|
108 |
Graz University of Technologie\\
|
jan@42463
|
109 |
Austria\end{tabular}
|
jan@42463
|
110 |
}%
|
jan@42463
|
111 |
%
|
jan@42463
|
112 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
113 |
% %
|
jan@42463
|
114 |
% eJMT commands - do not change these %
|
jan@42463
|
115 |
% %
|
jan@42463
|
116 |
\date{} %
|
jan@42463
|
117 |
\maketitle %
|
jan@42463
|
118 |
% %
|
jan@42463
|
119 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
120 |
%
|
jan@42463
|
121 |
% abstract
|
jan@42463
|
122 |
%
|
jan@42463
|
123 |
\begin{abstract}
|
jan@42463
|
124 |
|
jan@42463
|
125 |
Traditional course material in engineering disciplines lacks an
|
jan@42463
|
126 |
important component, interactive support for step-wise problem
|
neuper@42464
|
127 |
solving. Theorem-Proving (TP) technology is appropriate for one part
|
jan@42463
|
128 |
of such support, in checking user-input. For the other part of such
|
jan@42463
|
129 |
support, guiding the learner towards a solution, another kind of
|
jan@42463
|
130 |
technology is required. %TODO ... connect to prototype ...
|
jan@42463
|
131 |
|
jan@42463
|
132 |
A prototype combines TP with a programming language, the latter
|
jan@42463
|
133 |
interpreted in a specific way: certain statements in a program, called
|
jan@42463
|
134 |
tactics, are treated as breakpoints where control is handed over to
|
jan@42463
|
135 |
the user. An input formula is checked by TP (using logical context
|
jan@42463
|
136 |
built up by the interpreter); and if a learner gets stuck, a program
|
jan@42463
|
137 |
describing the steps towards a solution of a problem ``knows the next
|
jan@42463
|
138 |
step''. This kind of interpretation is called Lucas-Interpretation for
|
jan@42463
|
139 |
\emph{TP-based programming languages}.
|
jan@42463
|
140 |
|
jan@42463
|
141 |
This paper describes the prototype's TP-based programming language
|
jan@42463
|
142 |
within a case study creating interactive material for an advanced
|
jan@42463
|
143 |
course in Signal Processing: implementation of definitions and
|
jan@42463
|
144 |
theorems in TP, formal specification of a problem and step-wise
|
jan@42463
|
145 |
development of the program solving the problem. Experiences with the
|
neuper@42464
|
146 |
ork flow in iterative development with testing and identifying errors
|
jan@42463
|
147 |
are described, too. The description clarifies the components missing
|
jan@42463
|
148 |
in the prototype's language as well as deficiencies experienced during
|
jan@42463
|
149 |
programming.
|
jan@42463
|
150 |
\par
|
jan@42463
|
151 |
These experiences are particularly notable, because the author is the
|
jan@42463
|
152 |
first programmer using the language beyond the core team which
|
jan@42463
|
153 |
developed the prototype's TP-based language interpreter.
|
jan@42463
|
154 |
%
|
jan@42463
|
155 |
\end{abstract}%
|
jan@42463
|
156 |
%
|
jan@42463
|
157 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
158 |
% %
|
jan@42463
|
159 |
% eJMT command %
|
jan@42463
|
160 |
% %
|
jan@42463
|
161 |
\thispagestyle{fancy} %
|
jan@42463
|
162 |
% %
|
jan@42463
|
163 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
jan@42463
|
164 |
%
|
jan@42463
|
165 |
% Please use the following to indicate sections, subsections,
|
jan@42463
|
166 |
% etc. Please also use \subsubsection{...}, \paragraph{...}
|
jan@42463
|
167 |
% and \subparagraph{...} as necessary.
|
jan@42463
|
168 |
%
|
jan@42463
|
169 |
|
neuper@42464
|
170 |
\section{Introduction}\label{intro}
|
jan@42463
|
171 |
|
jan@42466
|
172 |
% \paragraph{Didactics of mathematics}
|
jan@42466
|
173 |
%WN: wenn man in einem high-quality paper von 'didactics' spricht,
|
jan@42466
|
174 |
%WN muss man am state-of-the-art ankn"upfen -- siehe
|
jan@42466
|
175 |
%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
|
neuper@42464
|
176 |
% faces a specific issue, a gap
|
neuper@42464
|
177 |
% between (1) introduction of math concepts and skills and (2)
|
neuper@42464
|
178 |
% application of these concepts and skills, which usually are separated
|
neuper@42464
|
179 |
% into different units in curricula (for good reasons). For instance,
|
neuper@42464
|
180 |
% (1) teaching partial fraction decomposition is separated from (2)
|
neuper@42464
|
181 |
% application for inverse Z-transform in signal processing.
|
neuper@42464
|
182 |
%
|
neuper@42464
|
183 |
% \par This gap is an obstacle for applying math as an fundamental
|
neuper@42464
|
184 |
% thinking technology in engineering: In (1) motivation is lacking
|
neuper@42464
|
185 |
% because the question ``What is this stuff good for?'' cannot be
|
neuper@42464
|
186 |
% treated sufficiently, and in (2) the ``stuff'' is not available to
|
neuper@42464
|
187 |
% students in higher semesters as widespread experience shows.
|
neuper@42464
|
188 |
%
|
neuper@42464
|
189 |
% \paragraph{Motivation} taken by this didactic issue on the one hand,
|
neuper@42464
|
190 |
% and ongoing research and development on a novel kind of educational
|
neuper@42464
|
191 |
% mathematics assistant at Graz University of
|
neuper@42464
|
192 |
% Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
|
neuper@42464
|
193 |
% scope with this issue on the other hand, several institutes are
|
neuper@42464
|
194 |
% planning to join their expertise: the Institute for Information
|
neuper@42464
|
195 |
% Systems and Computer Media (IICM), the Institute for Software
|
neuper@42464
|
196 |
% Technology (IST), the Institutes for Mathematics, the Institute for
|
neuper@42464
|
197 |
% Signal Processing and Speech Communication (SPSC), the Institute for
|
neuper@42464
|
198 |
% Structural Analysis and the Institute of Electrical Measurement and
|
neuper@42464
|
199 |
% Measurement Signal Processing.
|
jan@42466
|
200 |
%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell
|
jan@42466
|
201 |
%WN und damit zu verg"anglich.
|
neuper@42464
|
202 |
% \par This thesis is the first attempt to tackle the above mentioned
|
neuper@42464
|
203 |
% issue, it focuses on Telematics, because these specific studies focus
|
neuper@42464
|
204 |
% on mathematics in \emph{STEOP}, the introductory orientation phase in
|
neuper@42464
|
205 |
% Austria. \emph{STEOP} is considered an opportunity to investigate the
|
neuper@42464
|
206 |
% impact of {\sisac}'s prototype on the issue and others.
|
neuper@42464
|
207 |
%
|
jan@42466
|
208 |
|
jan@42466
|
209 |
\paragraph{Traditional course material} in engineering disciplines lacks an
|
neuper@42464
|
210 |
important component, interactive support for step-wise problem
|
neuper@42464
|
211 |
solving. Theorem-Proving (TP) technology can provide such support by
|
neuper@42464
|
212 |
specific services. An important part of such services is called
|
neuper@42464
|
213 |
``next-step-guidance'', generated by a specific kind of ``TP-based
|
neuper@42464
|
214 |
programming language''. In the
|
neuper@42464
|
215 |
{\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
|
neuper@42464
|
216 |
a language is prototyped in line with~\cite{plmms10} and built upon
|
neuper@42464
|
217 |
the theorem prover
|
neuper@42464
|
218 |
Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
|
neuper@42464
|
219 |
The TP services are coordinated by a specific interpreter for the
|
neuper@42464
|
220 |
programming language, called
|
neuper@42464
|
221 |
Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
|
neuper@42464
|
222 |
interpreter will be briefly re-introduced in order to make the paper
|
neuper@42464
|
223 |
self-contained.
|
jan@42463
|
224 |
|
jan@42466
|
225 |
\subparagraph{The main part} of the paper is an account of first experiences
|
neuper@42464
|
226 |
with programming in this TP-based language. The experience was gained
|
neuper@42464
|
227 |
in a case study by the author. The author was considered an ideal
|
neuper@42464
|
228 |
candidate for this study for the following reasons: as a student in
|
neuper@42464
|
229 |
Telematics (computer science with focus on Signal Processing) he had
|
neuper@42464
|
230 |
general knowledge in programming as well as specific domain knowledge
|
neuper@42464
|
231 |
in Signal Processing; and he was not involved in the development of
|
neuper@42464
|
232 |
{\sisac}'s programming language and interpeter, thus a novice to the
|
neuper@42464
|
233 |
language.
|
jan@42463
|
234 |
|
jan@42466
|
235 |
\subparagraph{The goal} of the case study was (1) some TP-based programs for
|
neuper@42464
|
236 |
interactive course material for a specific ``Adavanced Signal
|
neuper@42464
|
237 |
Processing Lab'' in a higher semester, (2) respective program
|
neuper@42464
|
238 |
development with as little advice from the {\sisac}-team and (3) records
|
neuper@42464
|
239 |
and comments for the main steps of development in an Isabelle theory;
|
neuper@42464
|
240 |
this theory should provide guidelines for future programmers. An
|
neuper@42464
|
241 |
excerpt from this theory is the main part of this paper.
|
jan@42466
|
242 |
\par
|
jan@42466
|
243 |
The paper will use the problem in Fig.\ref{fig-interactive} as a
|
jan@42463
|
244 |
running example:
|
jan@42463
|
245 |
\begin{figure} [htb]
|
jan@42463
|
246 |
\begin{center}
|
neuper@42468
|
247 |
\includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
|
neuper@42468
|
248 |
%\includegraphics[width=140mm]{fig/isac-Ztrans-math}
|
jan@42463
|
249 |
\caption{Step-wise problem solving guided by the TP-based program}
|
jan@42463
|
250 |
\label{fig-interactive}
|
jan@42463
|
251 |
\end{center}
|
jan@42463
|
252 |
\end{figure}
|
jan@42466
|
253 |
|
jan@42466
|
254 |
\paragraph{The problem is} from the domain of Signal Processing and requests to
|
neuper@42464
|
255 |
determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
|
neuper@42464
|
256 |
also shows the beginning of the interactive construction of a solution
|
neuper@42464
|
257 |
for the problem. This construction is done in the right window named
|
neuper@42464
|
258 |
``Worksheet''.
|
jan@42466
|
259 |
\par
|
neuper@42464
|
260 |
User-interaction on the Worksheet is {\em checked} and {\em guided} by
|
neuper@42464
|
261 |
TP services:
|
neuper@42464
|
262 |
\begin{enumerate}
|
neuper@42464
|
263 |
\item Formulas input by the user are {\em checked} by TP: such a
|
neuper@42464
|
264 |
formula establishes a proof situation --- the prover has to derive the
|
neuper@42464
|
265 |
formula from the logical context. The context is built up from the
|
neuper@42464
|
266 |
formal specification of the problem (here hidden from the user) by the
|
neuper@42464
|
267 |
Lucas-Interpreter.
|
neuper@42464
|
268 |
\item If the user gets stuck, the program developed below in this
|
neuper@42464
|
269 |
paper ``knows the next step'' from behind the scenes. How the latter
|
neuper@42464
|
270 |
TP-service is exploited by dialogue authoring is out of scope of this
|
neuper@42464
|
271 |
paper and can be studied in~\cite{gdaroczy-EP-13}.
|
neuper@42464
|
272 |
\end{enumerate} It should be noted that the programmer using the
|
neuper@42464
|
273 |
TP-based language is not concerned with interaction at all; we will
|
neuper@42464
|
274 |
see that the program contains neither input-statements nor
|
neuper@42464
|
275 |
output-statements. Rather, interaction is handled by services
|
neuper@42464
|
276 |
generated automatically.
|
jan@42466
|
277 |
\par
|
jan@42466
|
278 |
So there is a clear separation of concerns: Dialogues are
|
neuper@42464
|
279 |
adapted by dialogue authors (in Java-based tools), using automatically
|
neuper@42464
|
280 |
generated TP services, while the TP-based program is written by
|
neuper@42464
|
281 |
mathematics experts (in Isabelle/ML). The latter is concern of this
|
neuper@42464
|
282 |
paper.
|
jan@42466
|
283 |
|
jan@42466
|
284 |
\paragraph{The paper is structed} as follows: The introduction
|
neuper@42464
|
285 |
\S\ref{intro} is followed by a brief re-introduction of the TP-based
|
neuper@42464
|
286 |
programming language in \S\ref{PL}, which extends the executable
|
neuper@42464
|
287 |
fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
|
neuper@42464
|
288 |
play a specific role in Lucas-Interpretation and in providing the TP
|
neuper@42464
|
289 |
services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes
|
neuper@42464
|
290 |
the main steps in developing the program for the running example:
|
neuper@42464
|
291 |
prepare domain knowledge, implement the formal specification of the
|
neuper@42464
|
292 |
problem, prepare the environment for the program, implement the
|
neuper@42464
|
293 |
program. The workflow of programming, debugging and testing is
|
neuper@42464
|
294 |
described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
|
neuper@42464
|
295 |
give directions identified for future development.
|
neuper@42464
|
296 |
|
jan@42463
|
297 |
|
jan@42463
|
298 |
\section{\isac's Prototype for a Programming Language}\label{PL}
|
jan@42463
|
299 |
The prototype's language extends the executable fragment in the
|
jan@42463
|
300 |
language of the theorem prover
|
jan@42463
|
301 |
Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}
|
jan@42463
|
302 |
by tactics which have a specific role in Lucas-Interpretation.
|
jan@42463
|
303 |
|
jan@42463
|
304 |
\subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
|
jan@42463
|
305 |
The executable fragment consists of data-type and function
|
jan@42463
|
306 |
definitions. It's usability even suggests that fragment for
|
jan@42463
|
307 |
introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
|
jan@42463
|
308 |
whose type system resembles that of functional programming
|
jan@42463
|
309 |
languages. Thus there are
|
jan@42463
|
310 |
\begin{description}
|
jan@42463
|
311 |
\item[base types,] in particular \textit{bool}, the type of truth
|
jan@42463
|
312 |
values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
|
jan@42463
|
313 |
natural, integer and complex numbers respectively in mathematics.
|
jan@42463
|
314 |
\item[type constructors] allow to define arbitrary types, from
|
jan@42463
|
315 |
\textit{set}, \textit{list} to advanced data-structures like
|
jan@42463
|
316 |
\textit{trees}, red-black-trees etc.
|
jan@42463
|
317 |
\item[function types,] denoted by $\Rightarrow$.
|
jan@42463
|
318 |
\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
|
jan@42463
|
319 |
type polymorphism. Isabelle automatically computes the type of each
|
jan@42463
|
320 |
variable in a term by use of Hindley-Milner type inference
|
jan@42463
|
321 |
\cite{pl:hind97,Milner-78}.
|
jan@42463
|
322 |
\end{description}
|
jan@42463
|
323 |
|
jan@42463
|
324 |
\textbf{Terms} are formed as in functional programming by applying
|
jan@42463
|
325 |
functions to arguments. If $f$ is a function of type
|
jan@42463
|
326 |
$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
|
jan@42463
|
327 |
$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
|
jan@42463
|
328 |
has type $\tau$. There are many predefined infix symbols like $+$ and
|
jan@42463
|
329 |
$\leq$ most of which are overloaded for various types.
|
jan@42463
|
330 |
|
jan@42463
|
331 |
HOL also supports some basic constructs from functional programming:
|
jan@42463
|
332 |
{\it\label{isabelle-stmts}
|
jan@42463
|
333 |
\begin{tabbing} 123\=\kill
|
jan@42463
|
334 |
\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
|
jan@42463
|
335 |
\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
|
jan@42463
|
336 |
\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
|
jan@42463
|
337 |
\Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
|
jan@42463
|
338 |
\end{tabbing} }
|
neuper@42482
|
339 |
\noindent The running example's program uses some of these elements
|
neuper@42482
|
340 |
(marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
|
neuper@42482
|
341 |
let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
|
neuper@42482
|
342 |
is an Isabelle term with specific function constants like {\tt
|
neuper@42482
|
343 |
program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
|
neuper@42482
|
344 |
Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
|
neuper@42482
|
345 |
respectively.
|
jan@42463
|
346 |
|
jan@42463
|
347 |
% Terms may also contain $\lambda$-abstractions. For example, $\lambda
|
jan@42463
|
348 |
% x. \; x$ is the identity function.
|
jan@42463
|
349 |
|
neuper@42467
|
350 |
%JR warum auskommentiert? WN2...
|
neuper@42467
|
351 |
%WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
|
neuper@42467
|
352 |
%WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
|
neuper@42467
|
353 |
%WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
|
neuper@42467
|
354 |
%WN2 gel"oscht.
|
neuper@42467
|
355 |
%WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
|
neuper@42467
|
356 |
%WN2 Platz f"ur Anderes weg.
|
jan@42466
|
357 |
|
neuper@42464
|
358 |
\textbf{Formulae} are terms of type \textit{bool}. There are the basic
|
jan@42463
|
359 |
constants \textit{True} and \textit{False} and the usual logical
|
jan@42463
|
360 |
connectives (in decreasing order of precedence): $\neg, \land, \lor,
|
jan@42463
|
361 |
\rightarrow$.
|
jan@42463
|
362 |
|
neuper@42464
|
363 |
\textbf{Equality} is available in the form of the infix function $=$
|
neuper@42464
|
364 |
of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
|
neuper@42464
|
365 |
formulas, where it means ``if and only if''.
|
jan@42463
|
366 |
|
jan@42463
|
367 |
\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
|
jan@42463
|
368 |
P$. Quantifiers lead to non-executable functions, so functions do not
|
jan@42463
|
369 |
always correspond to programs, for instance, if comprising \\$(
|
jan@42463
|
370 |
\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
|
jan@42463
|
371 |
\;)$.
|
jan@42463
|
372 |
|
jan@42463
|
373 |
\subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
|
jan@42463
|
374 |
The prototype extends Isabelle's language by specific statements
|
neuper@42464
|
375 |
called tactics~\footnote{{\sisac}'s tactics are different from
|
jan@42463
|
376 |
Isabelle's tactics: the former concern steps in a calculation, the
|
jan@42463
|
377 |
latter concern proof steps.} and tacticals. For the programmer these
|
jan@42463
|
378 |
statements are functions with the following signatures:
|
jan@42463
|
379 |
|
jan@42463
|
380 |
\begin{description}
|
jan@42463
|
381 |
\item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
|
jan@42463
|
382 |
term} * {\it term}\;{\it list}$:
|
jan@42463
|
383 |
this tactic appplies {\it theorem} to a {\it term} yielding a {\it
|
jan@42463
|
384 |
term} and a {\it term list}, the list are assumptions generated by
|
jan@42463
|
385 |
conditional rewriting. For instance, the {\it theorem}
|
jan@42463
|
386 |
$b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
|
jan@42463
|
387 |
applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
|
jan@42463
|
388 |
$(\frac{2}{3}, [x\not=0])$.
|
jan@42463
|
389 |
|
jan@42463
|
390 |
\item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
|
jan@42463
|
391 |
term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
|
jan@42463
|
392 |
this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
|
jan@42463
|
393 |
a confluent and terminating term rewrite system, in general. If
|
jan@42463
|
394 |
none of the rules ({\it theorem}s) is applicable on interpretation
|
jan@42463
|
395 |
of this tactic, an exception is thrown.
|
jan@42463
|
396 |
|
jan@42463
|
397 |
% \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
|
jan@42463
|
398 |
% theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
|
jan@42463
|
399 |
% list}$:
|
jan@42463
|
400 |
%
|
jan@42463
|
401 |
% \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
|
jan@42463
|
402 |
% ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
|
jan@42463
|
403 |
% list}$:
|
jan@42463
|
404 |
|
jan@42463
|
405 |
\item[Substitute:] ${\it substitution}\Rightarrow{\it
|
neuper@42482
|
406 |
term}\Rightarrow{\it term}$: allows to access sub-terms.
|
jan@42463
|
407 |
|
jan@42463
|
408 |
\item[Take:] ${\it term}\Rightarrow{\it term}$:
|
jan@42463
|
409 |
this tactic has no effect in the program; but it creates a side-effect
|
jan@42463
|
410 |
by Lucas-Interpretation (see below) and writes {\it term} to the
|
jan@42463
|
411 |
Worksheet.
|
jan@42463
|
412 |
|
jan@42463
|
413 |
\item[Subproblem:] ${\it theory} * {\it specification} * {\it
|
jan@42463
|
414 |
method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
|
neuper@42482
|
415 |
this tactic is a generalisation of a function call: it takes an
|
neuper@42482
|
416 |
\textit{argument list} as usual, and additionally a triple consisting
|
neuper@42482
|
417 |
of an Isabelle \textit{theory}, an implicit \textit{specification} of the
|
neuper@42482
|
418 |
program and a \textit{method} containing data for Lucas-Interpretation,
|
neuper@42482
|
419 |
last not least a program (as an explicit specification)~\footnote{In
|
neuper@42482
|
420 |
interactive tutoring these three items can be determined explicitly
|
neuper@42482
|
421 |
by the user.}.
|
jan@42463
|
422 |
\end{description}
|
jan@42463
|
423 |
The tactics play a specific role in
|
jan@42463
|
424 |
Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
|
neuper@42482
|
425 |
break-points where, as a side-effect, a line is added to a calculation
|
neuper@42483
|
426 |
as a protocol for proceeding towards a solution in step-wise problem
|
neuper@42483
|
427 |
solving. At the same points Lucas-Interpretation serves interactive
|
neuper@42483
|
428 |
tutoring and control is handed over to the user. The user is free to
|
neuper@42483
|
429 |
investigate underlying knowledge, applicable theorems, etc. And the
|
neuper@42483
|
430 |
user can proceed constructing a solution by input of a tactic to be
|
neuper@42483
|
431 |
applied or by input of a formula; in the latter case the
|
jan@42463
|
432 |
Lucas-Interpreter has built up a logical context (initialised with the
|
jan@42463
|
433 |
precondition of the formal specification) such that Isabelle can
|
jan@42463
|
434 |
derive the formula from this context --- or give feedback, that no
|
jan@42463
|
435 |
derivation can be found.
|
jan@42463
|
436 |
|
jan@42463
|
437 |
\subsection{Tacticals for Control of Interpretation}
|
jan@42463
|
438 |
The flow of control in a program can be determined by {\tt if then else}
|
jan@42463
|
439 |
and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
|
jan@42463
|
440 |
by additional tacticals:
|
jan@42463
|
441 |
\begin{description}
|
jan@42463
|
442 |
\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
|
jan@42463
|
443 |
term}$: iterates over tactics which take a {\it term} as argument as
|
neuper@42482
|
444 |
long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
|
jan@42463
|
445 |
not be applicable).
|
jan@42463
|
446 |
|
jan@42463
|
447 |
\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
|
jan@42463
|
448 |
if {\it tactic} is applicable, then it is applied to {\it term},
|
neuper@42483
|
449 |
otherwise {\it term} is passed on without changes.
|
jan@42463
|
450 |
|
jan@42463
|
451 |
\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
neuper@42483
|
452 |
term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
|
neuper@42483
|
453 |
it is applied to the first {\it term} yielding another {\it term},
|
neuper@42483
|
454 |
otherwise the second {\it tactic} is applied; if none is applicable an
|
neuper@42483
|
455 |
exception is raised.
|
jan@42463
|
456 |
|
jan@42463
|
457 |
\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
neuper@42483
|
458 |
term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
|
neuper@42483
|
459 |
first {\it term} yielding an intermediate term (not appearing in the
|
neuper@42483
|
460 |
signature) to which the second {\it tactic} is applied.
|
jan@42463
|
461 |
|
jan@42463
|
462 |
\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
|
neuper@42483
|
463 |
term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
|
neuper@42483
|
464 |
{\it tactic} is applied to the first {\it term} yielding an
|
neuper@42483
|
465 |
intermediate term (not appearing in the signature); the intermediate
|
neuper@42483
|
466 |
term is added to the environment the first {\it term} is evaluated in
|
neuper@42483
|
467 |
etc as long as the first {\it term} is true.
|
jan@42463
|
468 |
\end{description}
|
neuper@42483
|
469 |
The tacticals are not treated as break-points by Lucas-Interpretation
|
neuper@42483
|
470 |
and thus do not contribute to the calculation nor to interaction.
|
jan@42463
|
471 |
|
jan@42466
|
472 |
\section{Development of a Program on Trial}\label{trial}
|
jan@42466
|
473 |
As mentioned above, {\sisac} is an experimental system for a proof of
|
jan@42466
|
474 |
concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
|
jan@42466
|
475 |
latter interprets a specific kind of TP-based programming language,
|
jan@42466
|
476 |
which is as experimental as the whole prototype --- so programming in
|
jan@42466
|
477 |
this language can be only ``on trial'', presently. However, as a
|
jan@42466
|
478 |
prototype, the language addresses essentials described below.
|
jan@42466
|
479 |
|
jan@42466
|
480 |
\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
|
jan@42466
|
481 |
|
neuper@42467
|
482 |
%WN was Fachleute unter obigem Titel interessiert findet sich
|
jan@42466
|
483 |
%WN unterhalb des auskommentierten Textes.
|
jan@42466
|
484 |
|
jan@42466
|
485 |
%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
|
jan@42466
|
486 |
%WN auf Computer-Mathematiker fokussiert.
|
neuper@42464
|
487 |
% \paragraph{As mentioned in the introduction,} a prototype of an
|
neuper@42464
|
488 |
% educational math assistant called
|
neuper@42464
|
489 |
% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
|
neuper@42464
|
490 |
% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
|
neuper@42464
|
491 |
% the gap between (1) introducation and (2) application of mathematics:
|
neuper@42464
|
492 |
% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
|
neuper@42464
|
493 |
% requires each fact and each action justified by formal logic, so
|
neuper@42464
|
494 |
% {{{\sisac}{}}} makes justifications transparent to students in
|
neuper@42464
|
495 |
% interactive step-wise problem solving. By that way {{\sisac}} already
|
neuper@42464
|
496 |
% can serve both:
|
neuper@42464
|
497 |
% \begin{enumerate}
|
neuper@42464
|
498 |
% \item Introduction of math stuff (in e.g. partial fraction
|
neuper@42464
|
499 |
% decomposition) by stepwise explaining and exercising respective
|
neuper@42464
|
500 |
% symbolic calculations with ``next step guidance (NSG)'' and rigorously
|
neuper@42464
|
501 |
% checking steps freely input by students --- this also in context with
|
neuper@42464
|
502 |
% advanced applications (where the stuff to be taught in higher
|
neuper@42464
|
503 |
% semesters can be skimmed through by NSG), and
|
neuper@42464
|
504 |
% \item Application of math stuff in advanced engineering courses
|
neuper@42464
|
505 |
% (e.g. problems to be solved by inverse Z-transform in a Signal
|
neuper@42464
|
506 |
% Processing Lab) and now without much ado about basic math techniques
|
neuper@42464
|
507 |
% (like partial fraction decomposition): ``next step guidance'' supports
|
neuper@42464
|
508 |
% students in independently (re-)adopting such techniques.
|
neuper@42464
|
509 |
% \end{enumerate}
|
neuper@42464
|
510 |
% Before the question is answers, how {{\sisac}}
|
neuper@42464
|
511 |
% accomplishes this task from a technical point of view, some remarks on
|
neuper@42464
|
512 |
% the state-of-the-art is given, therefor follow up Section~\ref{emas}.
|
neuper@42464
|
513 |
%
|
neuper@42464
|
514 |
% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
|
neuper@42464
|
515 |
%
|
jan@42466
|
516 |
% \paragraph{Educational software in mathematics} is, if at all, based
|
jan@42466
|
517 |
% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
|
jan@42466
|
518 |
% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
|
jan@42466
|
519 |
% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
|
jan@42466
|
520 |
% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
|
jan@42466
|
521 |
% base technologies are used to program math lessons and sometimes even
|
jan@42466
|
522 |
% exercises. The latter are cumbersome: the steps towards a solution of
|
jan@42466
|
523 |
% such an interactive exercise need to be provided with feedback, where
|
jan@42466
|
524 |
% at each step a wide variety of possible input has to be foreseen by
|
jan@42466
|
525 |
% the programmer - so such interactive exercises either require high
|
neuper@42464
|
526 |
% development efforts or the exercises constrain possible inputs.
|
neuper@42464
|
527 |
%
|
jan@42466
|
528 |
% \subparagraph{A new generation} of educational math assistants (EMAs)
|
jan@42466
|
529 |
% is emerging presently, which is based on Theorem Proving (TP). TP, for
|
jan@42466
|
530 |
% instance Isabelle and Coq, is a technology which requires each fact
|
jan@42466
|
531 |
% and each action justified by formal logic. Pushed by demands for
|
jan@42466
|
532 |
% \textit{proven} correctness of safety-critical software TP advances
|
jan@42466
|
533 |
% into software engineering; from these advancements computer
|
jan@42466
|
534 |
% mathematics benefits in general, and math education in particular. Two
|
neuper@42464
|
535 |
% features of TP are immediately beneficial for learning:
|
neuper@42464
|
536 |
%
|
jan@42466
|
537 |
% \paragraph{TP have knowledge in human readable format,} that is in
|
jan@42466
|
538 |
% standard predicate calculus. TP following the LCF-tradition have that
|
jan@42466
|
539 |
% knowledge down to the basic definitions of set, equality,
|
jan@42466
|
540 |
% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
|
jan@42466
|
541 |
% following the typical deductive development of math, natural numbers
|
jan@42466
|
542 |
% are defined and their properties
|
jan@42466
|
543 |
% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
|
jan@42466
|
544 |
% etc. Present knowledge mechanized in TP exceeds high-school
|
jan@42466
|
545 |
% mathematics by far, however by knowledge required in software
|
neuper@42464
|
546 |
% technology, and not in other engineering sciences.
|
neuper@42464
|
547 |
%
|
jan@42466
|
548 |
% \paragraph{TP can model the whole problem solving process} in
|
jan@42466
|
549 |
% mathematical problem solving {\em within} a coherent logical
|
jan@42466
|
550 |
% framework. This is already being done by three projects, by
|
neuper@42464
|
551 |
% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
|
neuper@42464
|
552 |
% \par
|
jan@42466
|
553 |
% Having the whole problem solving process within a logical coherent
|
jan@42466
|
554 |
% system, such a design guarantees correctness of intermediate steps and
|
jan@42466
|
555 |
% of the result (which seems essential for math software); and the
|
jan@42466
|
556 |
% second advantage is that TP provides a wealth of theories which can be
|
jan@42466
|
557 |
% exploited for mechanizing other features essential for educational
|
neuper@42464
|
558 |
% software.
|
neuper@42464
|
559 |
%
|
neuper@42464
|
560 |
% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
|
neuper@42464
|
561 |
%
|
jan@42466
|
562 |
% One essential feature for educational software is feedback to user
|
neuper@42464
|
563 |
% input and assistance in coming to a solution.
|
neuper@42464
|
564 |
%
|
jan@42466
|
565 |
% \paragraph{Checking user input} by ATP during stepwise problem solving
|
jan@42466
|
566 |
% is being accomplished by the three projects mentioned above
|
jan@42466
|
567 |
% exclusively. They model the whole problem solving process as mentioned
|
jan@42466
|
568 |
% above, so all what happens between formalized assumptions (or formal
|
jan@42466
|
569 |
% specification) and goal (or fulfilled postcondition) can be
|
jan@42466
|
570 |
% mechanized. Such mechanization promises to greatly extend the scope of
|
neuper@42464
|
571 |
% educational software in stepwise problem solving.
|
neuper@42464
|
572 |
%
|
jan@42466
|
573 |
% \paragraph{NSG (Next step guidance)} comprises the system's ability to
|
jan@42466
|
574 |
% propose a next step; this is a challenge for TP: either a radical
|
jan@42466
|
575 |
% restriction of the search space by restriction to very specific
|
jan@42466
|
576 |
% problem classes is required, or much care and effort is required in
|
jan@42466
|
577 |
% designing possible variants in the process of problem solving
|
neuper@42464
|
578 |
% \cite{proof-strategies-11}.
|
neuper@42464
|
579 |
% \par
|
jan@42466
|
580 |
% Another approach is restricted to problem solving in engineering
|
jan@42466
|
581 |
% domains, where a problem is specified by input, precondition, output
|
jan@42466
|
582 |
% and postcondition, and where the postcondition is proven by ATP behind
|
jan@42466
|
583 |
% the scenes: Here the possible variants in the process of problem
|
jan@42466
|
584 |
% solving are provided with feedback {\em automatically}, if the problem
|
jan@42466
|
585 |
% is described in a TP-based programing language: \cite{plmms10} the
|
jan@42466
|
586 |
% programmer only describes the math algorithm without caring about
|
jan@42466
|
587 |
% interaction (the respective program is functional and even has no
|
jan@42466
|
588 |
% input or output statements!); interaction is generated as a
|
jan@42466
|
589 |
% side-effect by the interpreter --- an efficient separation of concern
|
jan@42466
|
590 |
% between math programmers and dialog designers promising application
|
neuper@42464
|
591 |
% all over engineering disciplines.
|
neuper@42464
|
592 |
%
|
neuper@42464
|
593 |
%
|
neuper@42464
|
594 |
% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
|
jan@42466
|
595 |
% Authoring new mathematics knowledge in {{\sisac}} can be compared with
|
jan@42466
|
596 |
% ``application programing'' of engineering problems; most of such
|
jan@42466
|
597 |
% programing uses CAS-based programing languages (CAS = Computer Algebra
|
neuper@42464
|
598 |
% Systems; e.g. Mathematica's or Maple's programing language).
|
neuper@42464
|
599 |
%
|
jan@42466
|
600 |
% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
|
jan@42466
|
601 |
% \cite{plmms10} for describing how to construct a solution to an
|
jan@42466
|
602 |
% engineering problem and for calling equation solvers, integration,
|
jan@42466
|
603 |
% etc~\footnote{Implementation of CAS-like functionality in TP is not
|
jan@42466
|
604 |
% primarily concerned with efficiency, but with a didactic question:
|
jan@42466
|
605 |
% What to decide for: for high-brow algorithms at the state-of-the-art
|
jan@42466
|
606 |
% or for elementary algorithms comprehensible for students?} within TP;
|
jan@42466
|
607 |
% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
|
neuper@42464
|
608 |
% are impossible for CAS which have no logics underlying.
|
neuper@42464
|
609 |
%
|
jan@42466
|
610 |
% \subparagraph{Authoring is perfect} by writing such TP based programs;
|
jan@42466
|
611 |
% the application programmer is not concerned with interaction or with
|
jan@42466
|
612 |
% user guidance: this is concern of a novel kind of program interpreter
|
jan@42466
|
613 |
% called Lucas-Interpreter. This interpreter hands over control to a
|
jan@42466
|
614 |
% dialog component at each step of calculation (like a debugger at
|
jan@42466
|
615 |
% breakpoints) and calls automated TP to check user input following
|
neuper@42464
|
616 |
% personalized strategies according to a feedback module.
|
neuper@42464
|
617 |
% \par
|
jan@42466
|
618 |
% However ``application programing with TP'' is not done with writing a
|
jan@42466
|
619 |
% program: according to the principles of TP, each step must be
|
jan@42466
|
620 |
% justified. Such justifications are given by theorems. So all steps
|
jan@42466
|
621 |
% must be related to some theorem, if there is no such theorem it must
|
jan@42466
|
622 |
% be added to the existing knowledge, which is organized in so-called
|
jan@42466
|
623 |
% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
|
jan@42466
|
624 |
% Isabelle comprises a mechanism (called ``axiomatization''), which
|
jan@42466
|
625 |
% allows to omit proofs. Such a theorem is shown in
|
neuper@42464
|
626 |
% Example~\ref{eg:neuper1}.
|
jan@42466
|
627 |
|
jan@42466
|
628 |
The running example, introduced by Fig.\ref{fig-interactive} on
|
jan@42466
|
629 |
p.\pageref{fig-interactive}, requires to determine the inverse $\cal
|
jan@42466
|
630 |
Z$-transform for a class of functions. The domain of Signal Processing
|
jan@42466
|
631 |
is accustomed to specific notation for the resulting functions, which
|
jan@42466
|
632 |
are absolutely summable and are called TODO: $u[n]$, where $u$ is the
|
jan@42466
|
633 |
function, $n$ is the argument and the brackets indicate that the
|
jan@42466
|
634 |
arguments are TODO. Surprisingly, Isabelle accepts the rules for
|
jan@42466
|
635 |
${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
|
jan@42466
|
636 |
experts might be particularly surprised, that the brackets do not
|
jan@42466
|
637 |
cause errors in typing (as lists).}:
|
neuper@42464
|
638 |
%\vbox{
|
neuper@42464
|
639 |
% \begin{example}
|
jan@42463
|
640 |
\label{eg:neuper1}
|
jan@42463
|
641 |
{\small\begin{tabbing}
|
jan@42463
|
642 |
123\=123\=123\=123\=\kill
|
jan@42463
|
643 |
\hfill \\
|
jan@42463
|
644 |
\>axiomatization where \\
|
neuper@42464
|
645 |
\>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
|
neuper@42464
|
646 |
\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
|
jan@42466
|
647 |
\>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
|
jan@42466
|
648 |
%TODO
|
jan@42466
|
649 |
\>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
|
jan@42466
|
650 |
%TODO
|
jan@42466
|
651 |
\>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
|
jan@42466
|
652 |
%TODO
|
jan@42466
|
653 |
\>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
|
jan@42466
|
654 |
%TODO
|
jan@42463
|
655 |
\end{tabbing}
|
jan@42463
|
656 |
}
|
neuper@42464
|
657 |
% \end{example}
|
jan@42466
|
658 |
%}
|
jan@42466
|
659 |
These 6 rules can be used as conditional rewrite rules, depending on
|
jan@42466
|
660 |
the respective convergence radius. Satisfaction from accordance with traditional notation
|
jan@42466
|
661 |
contrasts with the above word {\em axiomatization}: As TP-based, the
|
jan@42466
|
662 |
programming language expects these rules as {\em proved} theorems, and
|
jan@42466
|
663 |
not as axioms implemented in the above brute force manner; otherwise
|
jan@42466
|
664 |
all the verification efforts envisaged (like proof of the
|
jan@42466
|
665 |
post-condition, see below) would be meaningless.
|
jan@42466
|
666 |
|
jan@42466
|
667 |
Isabelle provides a large body of knowledge, rigorously proven from
|
jan@42466
|
668 |
the basic axioms of mathematics~\footnote{This way of rigorously
|
jan@42466
|
669 |
deriving all knowledge from first principles is called the
|
jan@42466
|
670 |
LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
|
jan@42466
|
671 |
knowledge can be found in the theoris on Multivariate
|
jan@42466
|
672 |
Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
|
jan@42466
|
673 |
building up knowledge such that a proof for the above rules would be
|
jan@42466
|
674 |
reasonably short and easily comprehensible, still requires lots of
|
jan@42466
|
675 |
work (and is definitely out of scope of our case study).
|
jan@42466
|
676 |
|
neuper@42487
|
677 |
At the state-of-the-art in mechanization of knowledge in engineering
|
neuper@42487
|
678 |
sciences, the process does not stop with the mechanization of
|
neuper@42487
|
679 |
mathematics traditionally used in these sciences. Rather, ``Formal
|
neuper@42487
|
680 |
Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
|
neuper@42487
|
681 |
description of physical items. Signal Processing, for instance is
|
neuper@42487
|
682 |
concerned with physical devices for signal acquisition and
|
neuper@42487
|
683 |
reconstruction, which involve measuring a physical signal, storing it,
|
neuper@42487
|
684 |
and possibly later rebuilding the original signal or an approximation
|
neuper@42487
|
685 |
thereof. For digital systems, this typically includes sampling and
|
neuper@42487
|
686 |
quantization; devices for signal compression, including audio
|
neuper@42487
|
687 |
compression, image compression, and video compression, etc. ``Domain
|
neuper@42487
|
688 |
engineering''\cite{db:dom-eng} is concerned with {\em specification}
|
neuper@42487
|
689 |
of these devices' components and features; this part in the process of
|
neuper@42487
|
690 |
mechanization is only at the beginning in domains like Signal
|
neuper@42487
|
691 |
Processing.
|
jan@42466
|
692 |
|
neuper@42487
|
693 |
TP-based programming, concern of this paper, is determined to
|
jan@42466
|
694 |
add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
|
jan@42466
|
695 |
p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
|
jan@42466
|
696 |
starts with a formal {\em specification} of the problem to be solved.
|
neuper@42478
|
697 |
\begin{figure}
|
neuper@42478
|
698 |
\begin{center}
|
neuper@42483
|
699 |
\includegraphics[width=110mm]{fig/math-universe-small}
|
neuper@42487
|
700 |
\caption{The three-dimensional universe of mathematics knowledge}
|
neuper@42478
|
701 |
\label{fig:mathuni}
|
neuper@42478
|
702 |
\end{center}
|
neuper@42478
|
703 |
\end{figure}
|
neuper@42487
|
704 |
The language for both axes is defined in the axis at the bottom, deductive
|
neuper@42487
|
705 |
knowledge, in {\sisac} represented by Isabelle's theories.
|
jan@42466
|
706 |
|
jan@42466
|
707 |
\subsection{Specification of the Problem}\label{spec}
|
jan@42466
|
708 |
%WN <--> \chapter 7 der Thesis
|
jan@42466
|
709 |
%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
|
jan@42466
|
710 |
|
jan@42466
|
711 |
The problem of the running example is textually described in
|
jan@42466
|
712 |
Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
|
jan@42466
|
713 |
formal} specification of this problem, in traditional mathematical
|
jan@42469
|
714 |
notation, could look like is this:
|
jan@42466
|
715 |
|
jan@42466
|
716 |
%WN Hier brauchen wir die Spezifikation des 'running example' ...
|
jan@42466
|
717 |
%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
|
jan@42466
|
718 |
%JR der post condition - die existiert für uns ja eigentlich nicht aka
|
neuper@42467
|
719 |
%JR haben sie bis jetzt nicht beachtet WN...
|
neuper@42467
|
720 |
%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
|
jan@42473
|
721 |
%JR2 done
|
jan@42466
|
722 |
|
jan@42463
|
723 |
\label{eg:neuper2}
|
jan@42463
|
724 |
{\small\begin{tabbing}
|
jan@42463
|
725 |
123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
|
jan@42463
|
726 |
\hfill \\
|
neuper@42465
|
727 |
Specification:\\
|
jan@42466
|
728 |
\>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
|
jan@42470
|
729 |
\>precond \>: filterExpression continius on $\mathbb{R}$ \\
|
jan@42466
|
730 |
\>output \>: stepResponse $x[n]$ \\
|
jan@42469
|
731 |
\>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
|
jan@42466
|
732 |
|
jan@42473
|
733 |
\begin{remark}
|
jan@42473
|
734 |
Defining the postcondition requires a high amount mathematical
|
jan@42473
|
735 |
knowledge, the difficult part in our case is not to set up this condition
|
jan@42473
|
736 |
nor it is more to define it in a way the interpreter is able to handle it.
|
jan@42473
|
737 |
Due the fact that implementing that mechanisms is quite the same amount as
|
jan@42473
|
738 |
creating the programm itself, it is not avaible in our prototype.
|
jan@42473
|
739 |
\label{rm:postcond}
|
jan@42473
|
740 |
\end{remark}
|
jan@42469
|
741 |
|
jan@42469
|
742 |
\paragraph{The implementation} of the formal specification in the present
|
jan@42466
|
743 |
prototype, still bar-bones without support for authoring:
|
jan@42466
|
744 |
%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
|
neuper@42480
|
745 |
{\footnotesize\label{exp-spec}
|
jan@42466
|
746 |
\begin{verbatim}
|
jan@42466
|
747 |
01 store_specification
|
jan@42466
|
748 |
02 (prepare_specification
|
jan@42466
|
749 |
03 ["Jan Rocnik"]
|
jan@42466
|
750 |
04 "pbl_SP_Ztrans_inv"
|
jan@42466
|
751 |
05 thy
|
jan@42466
|
752 |
06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
|
jan@42466
|
753 |
07 [ ("#Given", ["filterExpression X_eq"]),
|
jan@42466
|
754 |
08 ("#Pre" , ["X_eq is_continuous"]),
|
jan@42466
|
755 |
19 ("#Find" , ["stepResponse n_eq"]),
|
jan@42466
|
756 |
10 ("#Post" , [" TODO "])],
|
jan@42466
|
757 |
11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
|
jan@42466
|
758 |
12 NONE,
|
jan@42466
|
759 |
13 [["SignalProcessing","Z_Transform","Inverse"]]));
|
jan@42466
|
760 |
\end{verbatim}}
|
jan@42466
|
761 |
Although the above details are partly very technical, we explain them
|
jan@42466
|
762 |
in order to document some intricacies of TP-based programming in the
|
jan@42466
|
763 |
present state of the {\sisac} prototype:
|
jan@42466
|
764 |
\begin{description}
|
jan@42466
|
765 |
\item[01..02]\textit{store\_specification:} stores the result of the
|
jan@42466
|
766 |
function \textit{prep\_specification} in a global reference
|
jan@42466
|
767 |
\textit{Unsynchronized.ref}, which causes principal conflicts with
|
jan@42466
|
768 |
Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
|
jan@42466
|
769 |
parallel execution~\cite{Makarius-09:parall-proof} and is under
|
jan@42466
|
770 |
reconstruction already.
|
jan@42466
|
771 |
|
jan@42466
|
772 |
\textit{prep\_pbt:} translates the specification to an internal format
|
jan@42466
|
773 |
which allows efficient processing; see for instance line {\rm 07}
|
jan@42466
|
774 |
below.
|
jan@42466
|
775 |
\item[03..04] are the ``mathematics author'' holding the copy-rights
|
jan@42466
|
776 |
and a unique identifier for the specification within {\sisac},
|
jan@42466
|
777 |
complare line {\rm 06}.
|
jan@42466
|
778 |
\item[05] is the Isabelle \textit{theory} required to parse the
|
jan@42466
|
779 |
specification in lines {\rm 07..10}.
|
jan@42466
|
780 |
\item[06] is a key into the tree of all specifications as presented to
|
jan@42466
|
781 |
the user (where some branches might be hidden by the dialog
|
jan@42466
|
782 |
component).
|
jan@42466
|
783 |
\item[07..10] are the specification with input, pre-condition, output
|
jan@42466
|
784 |
and post-condition respectively; the post-condition is not handled in
|
jan@42473
|
785 |
the prototype presently. (Follow up Remark~\ref{rm:postcond})
|
jan@42466
|
786 |
\item[11] creates a term rewriting system (abbreviated \textit{rls} in
|
jan@42466
|
787 |
{\sisac}) which evaluates the pre-condition for the actual input data.
|
jan@42466
|
788 |
Only if the evaluation yields \textit{True}, a program con be started.
|
jan@42466
|
789 |
\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
|
jan@42466
|
790 |
problem associated to a function from Computer Algebra (like an
|
jan@42466
|
791 |
equation solver) which is not the case here.
|
jan@42466
|
792 |
\item[13] is the specific key into the tree of programs addressing a
|
jan@42466
|
793 |
method which is able to find a solution which satiesfies the
|
jan@42466
|
794 |
post-condition of the specification.
|
jan@42466
|
795 |
\end{description}
|
jan@42466
|
796 |
|
jan@42466
|
797 |
|
jan@42466
|
798 |
%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
|
jan@42466
|
799 |
%WN ...
|
jan@42466
|
800 |
% type pbt =
|
jan@42466
|
801 |
% {guh : guh, (*unique within this isac-knowledge*)
|
jan@42466
|
802 |
% mathauthors: string list, (*copyright*)
|
jan@42466
|
803 |
% init : pblID, (*to start refinement with*)
|
jan@42466
|
804 |
% thy : theory, (* which allows to compile that pbt
|
jan@42466
|
805 |
% TODO: search generalized for subthy (ref.p.69*)
|
jan@42466
|
806 |
% (*^^^ WN050912 NOT used during application of the problem,
|
jan@42466
|
807 |
% because applied terms may be from 'subthy' as well as from super;
|
jan@42466
|
808 |
% thus we take 'maxthy'; see match_ags !*)
|
jan@42466
|
809 |
% cas : term option,(*'CAS-command'*)
|
jan@42466
|
810 |
% prls : rls, (* for preds in where_*)
|
jan@42466
|
811 |
% where_: term list, (* where - predicates*)
|
jan@42466
|
812 |
% ppc : pat list,
|
jan@42466
|
813 |
% (*this is the model-pattern;
|
jan@42466
|
814 |
% it contains "#Given","#Where","#Find","#Relate"-patterns
|
jan@42466
|
815 |
% for constraints on identifiers see "fun cpy_nam"*)
|
jan@42466
|
816 |
% met : metID list}; (* methods solving the pbt*)
|
jan@42466
|
817 |
%
|
jan@42466
|
818 |
%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
|
jan@42466
|
819 |
%WN oben selbst geschrieben.
|
jan@42466
|
820 |
|
jan@42466
|
821 |
|
jan@42466
|
822 |
|
jan@42466
|
823 |
|
jan@42466
|
824 |
%WN das w"urde ich in \sec\label{progr} verschieben und
|
jan@42466
|
825 |
%WN das SubProblem partial fractions zum Erkl"aren verwenden.
|
jan@42466
|
826 |
% Such a specification is checked before the execution of a program is
|
jan@42466
|
827 |
% started, the same applies for sub-programs. In the following example
|
neuper@42465
|
828 |
% (Example~\ref{eg:subprob}) shows the call of such a subproblem:
|
neuper@42465
|
829 |
%
|
neuper@42465
|
830 |
% \vbox{
|
neuper@42465
|
831 |
% \begin{example}
|
neuper@42465
|
832 |
% \label{eg:subprob}
|
neuper@42465
|
833 |
% \hfill \\
|
neuper@42465
|
834 |
% {\ttfamily \begin{tabbing}
|
neuper@42465
|
835 |
% ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
|
neuper@42465
|
836 |
% ``\>\>[linear,univariate,equation,test],'' \\
|
neuper@42465
|
837 |
% ``\>\>[Test,solve\_linear])'' \\
|
neuper@42465
|
838 |
% ``\>[BOOL equ, REAL z])'' \\
|
neuper@42465
|
839 |
% \end{tabbing}
|
neuper@42465
|
840 |
% }
|
neuper@42465
|
841 |
% {\small\textit{
|
jan@42466
|
842 |
% \noindent If a program requires a result which has to be
|
jan@42466
|
843 |
% calculated first we can use a subproblem to do so. In our specific
|
jan@42466
|
844 |
% case we wanted to calculate the zeros of a fraction and used a
|
neuper@42465
|
845 |
% subproblem to calculate the zeros of the denominator polynom.
|
neuper@42465
|
846 |
% }}
|
neuper@42465
|
847 |
% \end{example}
|
neuper@42465
|
848 |
% }
|
jan@42466
|
849 |
|
jan@42466
|
850 |
\subsection{Implementation of the Method}\label{meth}
|
jan@42466
|
851 |
%WN <--> \chapter 7 der Thesis
|
jan@42466
|
852 |
TODO
|
jan@42466
|
853 |
\subsection{Preparation of Simplifiers for the Program}\label{simp}
|
jan@42469
|
854 |
|
neuper@42480
|
855 |
\paragraph{After collecting} informations about the problem
|
neuper@42480
|
856 |
%WN4 welche 'informations' ?
|
neuper@42480
|
857 |
%WN4 Wenn das welche sind, die oben NICHT vorgekommen sind, dann anf"uhren
|
neuper@42480
|
858 |
%WN4 Wenn das welche sind, die oben SCHON vorgekommen sind, dann weglassen
|
neuper@42480
|
859 |
%WN4 und Platz sparen.
|
neuper@42480
|
860 |
%WN4
|
neuper@42480
|
861 |
%WN4 Wenn wir diese Bemerkung hier weglassen (sie m"usste eigentlich an jedem
|
neuper@42480
|
862 |
%WN4 Beginn von 3.* stehen), dann kommt sie gleich an den Anfang
|
neuper@42480
|
863 |
%WN4 nach der "Uberschrift von 3.
|
neuper@42480
|
864 |
and reviewing the calculations,
|
neuper@42480
|
865 |
%WN4 welche 'calculations', ist von solchen bisher schon die Rede gewesen ?
|
neuper@42480
|
866 |
the programm may be seem hard and heavy, therefor we can set up
|
jan@42475
|
867 |
some simplifications, for e.g. is the simplification of reational expressions
|
neuper@42480
|
868 |
already provided in the {\sisac{}} system.
|
neuper@42480
|
869 |
%WN4
|
neuper@42480
|
870 |
Also obligate is the use of the
|
jan@42475
|
871 |
function \texttt{drop\_questionmarks} which excludes irrelevant symbols out of
|
jan@42475
|
872 |
the expression. (Irrelevant symbols may be result out of the system during the
|
jan@42475
|
873 |
calculation.)
|
jan@42475
|
874 |
|
jan@42475
|
875 |
\subparagraph{Simplifiers often are represented} through rulesets\footnote{More
|
jan@42475
|
876 |
information about rulesets can be found in \S\ref{sec:rules}}, this rulesets
|
jan@42475
|
877 |
tell the machine which terms should be simplified into which representation. In
|
jan@42475
|
878 |
the upcoming programm a simplification is applied only in using such rulesets
|
jan@42475
|
879 |
on existing terms.
|
jan@42475
|
880 |
\par
|
jan@42475
|
881 |
Following example line was taken out of a finished programm and shows how
|
jan@42475
|
882 |
an rational expression can be simplified.
|
jan@42475
|
883 |
|
jan@42475
|
884 |
\begin{example}
|
jan@42475
|
885 |
\begin{verbatim}
|
jan@42475
|
886 |
|
jan@42475
|
887 |
"expression = (Rewrite_Set norm_Rational False) expression;"^\end{verbatim}
|
jan@42475
|
888 |
\end{example}
|
jan@42475
|
889 |
|
jan@42475
|
890 |
\subparagraph{If other} methods for use in term with simplification are needed
|
jan@42475
|
891 |
\S\ref{funs} gives informations about new ML-Functions can be prepared.
|
jan@42469
|
892 |
|
jan@42466
|
893 |
\subsection{Preparation of ML-Functions}\label{funs}
|
jan@42469
|
894 |
|
jan@42469
|
895 |
\paragraph{Explicit Problems} require explicit methods to solve them, and within
|
jan@42469
|
896 |
this methods we have some explicit steps to do. This steps can be unique for
|
jan@42469
|
897 |
a special problem or refindable in other problems. No mather what case, such
|
jan@42469
|
898 |
steps often require some technical functions behind. For the solving process
|
jan@42469
|
899 |
of the Inverse Z Transformation and the corresponding partial fraction it was
|
jan@42469
|
900 |
neccessary to build helping functions like \texttt{get\_denominator},
|
jan@42469
|
901 |
\texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
|
jan@42473
|
902 |
to filter the denominator or numerator out of a fraction, last one helps us to
|
jan@42469
|
903 |
get to know the bound variable in a equation.
|
jan@42469
|
904 |
\par
|
jan@42473
|
905 |
By taking \texttt{get\_denominator} as an example, we want to explain how to
|
jan@42473
|
906 |
implement new functions into the existing system and how we can later use them
|
jan@42473
|
907 |
in our program.
|
jan@42469
|
908 |
|
jan@42469
|
909 |
\subsubsection{Find a place to Store the Function}
|
jan@42473
|
910 |
|
jan@42469
|
911 |
The whole system builds up on a well defined structure of Knowledge. This
|
jan@42473
|
912 |
Knowledge sets up at the Path:
|
jan@42473
|
913 |
\begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
|
jan@42470
|
914 |
For implementing the Function \texttt{get\_denominator} (which let us extract
|
jan@42470
|
915 |
the denominator out of a fraction) we have choosen the Theory (file)
|
jan@42469
|
916 |
\texttt{Rational.thy}.
|
jan@42469
|
917 |
|
jan@42469
|
918 |
\subsubsection{Write down the new Function}
|
jan@42473
|
919 |
|
jan@42470
|
920 |
In upper Theory we now define the new function and its purpose:
|
jan@42470
|
921 |
\begin{verbatim}
|
jan@42470
|
922 |
get_denominator :: "real => real"
|
jan@42470
|
923 |
\end{verbatim}
|
jan@42470
|
924 |
This command tells the machine that a function with the name
|
jan@42470
|
925 |
\texttt{get\_denominator} exists which gets a real expression as argument and
|
jan@42473
|
926 |
returns once again a real expression. Now we are able to implement the function
|
jan@42473
|
927 |
itself, Example~\ref{eg:getdenom} now shows the implementation of
|
jan@42473
|
928 |
\texttt{get\_denominator}.
|
jan@42469
|
929 |
|
jan@42469
|
930 |
\begin{example}
|
jan@42470
|
931 |
\label{eg:getdenom}
|
jan@42470
|
932 |
\begin{verbatim}
|
jan@42469
|
933 |
|
jan@42470
|
934 |
01 (*
|
jan@42470
|
935 |
02 *("get_denominator",
|
jan@42470
|
936 |
03 * ("Rational.get_denominator", eval_get_denominator ""))
|
jan@42470
|
937 |
04 *)
|
jan@42470
|
938 |
05 fun eval_get_denominator (thmid:string) _
|
jan@42470
|
939 |
06 (t as Const ("Rational.get_denominator", _) $
|
jan@42470
|
940 |
07 (Const ("Rings.inverse_class.divide", _) $num
|
jan@42470
|
941 |
08 $denom)) thy =
|
jan@42470
|
942 |
09 SOME (mk_thmid thmid ""
|
jan@42470
|
943 |
10 (Print_Mode.setmp []
|
jan@42470
|
944 |
11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
|
jan@42470
|
945 |
12 Trueprop $ (mk_equality (t, denom)))
|
jan@42470
|
946 |
13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
|
jan@42469
|
947 |
\end{example}
|
jan@42469
|
948 |
|
jan@42470
|
949 |
Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
|
jan@42470
|
950 |
there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
|
jan@42470
|
951 |
splittet
|
jan@42473
|
952 |
into its two parts (\texttt{\$num \$denom}). The lines before are additionals
|
jan@42470
|
953 |
commands for declaring the function and the lines after are modeling and
|
jan@42470
|
954 |
returning a real variable out of \texttt{\$denom}.
|
jan@42469
|
955 |
|
jan@42469
|
956 |
\subsubsection{Add a test for the new Function}
|
jan@42469
|
957 |
|
jan@42473
|
958 |
\paragraph{Everytime when adding} a new function it is essential also to add
|
jan@42473
|
959 |
a test for it. Tests for all functions are sorted in the same structure as the
|
jan@42473
|
960 |
knowledge it self and can be found up from the path:
|
jan@42473
|
961 |
\begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
|
jan@42473
|
962 |
This tests are nothing very special, as a first prototype the functionallity
|
jan@42473
|
963 |
of a function can be checked by evaluating the result of a simple expression
|
jan@42473
|
964 |
passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
|
jan@42473
|
965 |
\textit{just} created function \texttt{get\_denominator}.
|
jan@42469
|
966 |
|
jan@42473
|
967 |
\begin{example}
|
jan@42473
|
968 |
\label{eg:getdenomtest}
|
jan@42473
|
969 |
\begin{verbatim}
|
jan@42473
|
970 |
|
jan@42473
|
971 |
01 val thy = @{theory Isac};
|
jan@42473
|
972 |
02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
|
jan@42473
|
973 |
03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
|
jan@42473
|
974 |
04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
|
jan@42473
|
975 |
05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
|
jan@42473
|
976 |
\end{example}
|
jan@42473
|
977 |
|
jan@42473
|
978 |
\begin{description}
|
jan@42473
|
979 |
\item[01] checks if the proofer set up on our {\sisac{}} System.
|
jan@42473
|
980 |
\item[02] passes a simple expression (fraction) to our suddenly created
|
jan@42473
|
981 |
function.
|
jan@42473
|
982 |
\item[04] checks if the resulting variable is the correct one (in this case
|
jan@42473
|
983 |
``b'' the denominator) and returns.
|
jan@42473
|
984 |
\item[05] handels the error case and reports that the function is not able to
|
jan@42473
|
985 |
solve the given problem.
|
jan@42473
|
986 |
\end{description}
|
jan@42469
|
987 |
|
neuper@42478
|
988 |
\subsection{Implementation of the TP-based Program}\label{progr}
|
neuper@42480
|
989 |
So finally all the prerequisites are described and the very topic can
|
neuper@42480
|
990 |
be addressed. The program below comes back to the running example: it
|
neuper@42480
|
991 |
computes a solution for the problem from Fig.\ref{fig-interactive} on
|
neuper@42480
|
992 |
p.\pageref{fig-interactive}. The reader is reminded of
|
neuper@42480
|
993 |
\S\ref{PL-isab}, the introduction of the programming language:
|
neuper@42482
|
994 |
{\small\it\label{s:impl}
|
neuper@42482
|
995 |
\begin{tabbing}
|
neuper@42478
|
996 |
123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
|
neuper@42480
|
997 |
\>{\rm 00}\>val program =\\
|
neuper@42480
|
998 |
\>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
|
neuper@42482
|
999 |
\>{\rm 02}\>\> {\tt let} \\
|
neuper@42468
|
1000 |
\>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
|
neuper@42468
|
1001 |
\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
|
neuper@42468
|
1002 |
\>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
|
neuper@42468
|
1003 |
\>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
|
neuper@42468
|
1004 |
\>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
|
neuper@42478
|
1005 |
\>{\rm 08}\>\>\>\>\>\>\>\> ( Isac, [partial\_fraction, rational, simplification], [] )\\
|
neuper@42478
|
1006 |
%\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
|
neuper@42478
|
1007 |
\>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
|
neuper@42478
|
1008 |
\>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
|
neuper@42478
|
1009 |
\>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@ \\
|
neuper@42478
|
1010 |
\>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
|
neuper@42482
|
1011 |
\>{\rm 13}\>\> {\tt in } \\
|
neuper@42480
|
1012 |
\>{\rm 14}\>\>\> X'\_eq"
|
neuper@42478
|
1013 |
\end{tabbing}}
|
neuper@42468
|
1014 |
% ORIGINAL FROM Inverse_Z_Transform.thy
|
neuper@42468
|
1015 |
% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
neuper@42468
|
1016 |
% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
neuper@42468
|
1017 |
% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1018 |
% " (X'_z::real) = lhs X'; "^(* ?X' z*)
|
neuper@42468
|
1019 |
% " (zzz::real) = argument_in X'_z; "^(* z *)
|
neuper@42468
|
1020 |
% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1021 |
%
|
neuper@42468
|
1022 |
% " (pbz::real) = (SubProblem (Isac', "^(**)
|
neuper@42468
|
1023 |
% " [partial_fraction,rational,simplification], "^
|
neuper@42468
|
1024 |
% " [simplification,of_rationals,to_partial_fraction]) "^
|
neuper@42468
|
1025 |
% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1026 |
%
|
neuper@42468
|
1027 |
% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1028 |
% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
neuper@42468
|
1029 |
% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1030 |
% " (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
|
1031 |
% " 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
|
1032 |
% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1033 |
% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42480
|
1034 |
The program is represented as a string and part of the method in
|
neuper@42480
|
1035 |
\S\ref{meth}. As mentioned in \S\ref{PL} the program is purely
|
neuper@42480
|
1036 |
functional and lacks any input statements and output statements. So
|
neuper@42480
|
1037 |
the steps of calculation towards a solution (and interactive tutoring
|
neuper@42480
|
1038 |
in step-wise problem solving) are created as a side-effect by
|
neuper@42480
|
1039 |
Lucas-Interpretation. The side-effects are triggered by the tactics
|
neuper@42482
|
1040 |
\texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
|
neuper@42482
|
1041 |
\texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
|
neuper@42480
|
1042 |
{\rm 12} respectively. These tactics produce the lines in the
|
neuper@42480
|
1043 |
calculation on p.\pageref{flow-impl}.
|
neuper@42478
|
1044 |
|
neuper@42480
|
1045 |
The above lines {\rm 05, 06} do not contain a tactics, so they do not
|
neuper@42480
|
1046 |
immediately contribute to the calculation on p.\pageref{flow-impl};
|
neuper@42482
|
1047 |
rather, they compute actual arguments for the \texttt{SubProblem} in
|
neuper@42480
|
1048 |
line {\rm 09}~\footnote{The tactics also are break-points for the
|
neuper@42480
|
1049 |
interpreter, where control is handed over to the user in interactive
|
neuper@42482
|
1050 |
tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
|
neuper@42480
|
1051 |
|
neuper@42480
|
1052 |
\medskip The above program also indicates the dominant role of interactive
|
neuper@42478
|
1053 |
selection of knowledge in the three-dimensional universe of
|
neuper@42478
|
1054 |
mathematics as depicted in Fig.\ref{fig:mathuni} on
|
neuper@42482
|
1055 |
p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines
|
neuper@42478
|
1056 |
{\rm 07..09} is more than a function call with the actual arguments
|
neuper@42478
|
1057 |
\textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
|
neuper@42478
|
1058 |
three items:
|
neuper@42480
|
1059 |
|
neuper@42478
|
1060 |
\begin{enumerate}
|
neuper@42478
|
1061 |
\item the theory, in the example \textit{Isac} because different
|
neuper@42478
|
1062 |
methods can be selected in Pt.3 below, which are defined in different
|
neuper@42478
|
1063 |
theories with \textit{Isac} collecting them.
|
neuper@42480
|
1064 |
\item the specification identified by \textit{[partial\_fraction,
|
neuper@42480
|
1065 |
rational, simplification]} in the tree of specifications; this
|
neuper@42480
|
1066 |
specification is analogous to the specification of the main program
|
neuper@42480
|
1067 |
described in \S\ref{spec}; the problem is to find a ``partial fraction
|
neuper@42480
|
1068 |
decomposition'' for a univariate rational polynomial.
|
neuper@42480
|
1069 |
\item the method in the above example is \textit{[ ]}, i.e. empty,
|
neuper@42480
|
1070 |
which supposes the interpreter to select one of the methods predefined
|
neuper@42480
|
1071 |
in the specification, for instance in line {\rm 13} in the running
|
neuper@42480
|
1072 |
example's specification on p.\pageref{exp-spec}~\footnote{The freedom
|
neuper@42480
|
1073 |
(or obligation) for selection carries over to the student in
|
neuper@42480
|
1074 |
interactive tutoring.}.
|
neuper@42478
|
1075 |
\end{enumerate}
|
neuper@42478
|
1076 |
|
neuper@42480
|
1077 |
The program code, above presented as a string, is parsed by Isabelle's
|
neuper@42480
|
1078 |
parser --- the program is an Isabelle term. This fact is expected to
|
neuper@42480
|
1079 |
simplify verification tasks in the future; on the other hand, this
|
neuper@42480
|
1080 |
fact causes troubles in error detectetion which are discussed as part
|
neuper@42480
|
1081 |
of the workflow in the subsequent section.
|
neuper@42467
|
1082 |
|
jan@42463
|
1083 |
\section{Workflow of Programming in the Prototype}\label{workflow}
|
neuper@42480
|
1084 |
The previous section presented all the duties and tasks to be accomplished by
|
neuper@42481
|
1085 |
programmers of TP-based languages. Some tasks are interrelated and comprehensive,
|
neuper@42481
|
1086 |
so first experiences with the workflow in programming are noted below. The notes
|
neuper@42481
|
1087 |
also capture requirements for future language development.
|
neuper@42468
|
1088 |
|
jan@42466
|
1089 |
\subsection{Preparations and Trials}\label{flow-prep}
|
neuper@42481
|
1090 |
% Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''
|
neuper@42481
|
1091 |
The new graphical user-interface of Isabelle~\cite{makar-jedit-12} is a great
|
neuper@42481
|
1092 |
step forward for interactive theory and proof development --- and so it is for
|
neuper@42481
|
1093 |
interactive program development; the specific requirements raised by interactive
|
neuper@42481
|
1094 |
programming will be mentioned separately.
|
neuper@42481
|
1095 |
|
neuper@42481
|
1096 |
The development in the {\sisac}-prototype was done in a separate
|
neuper@42481
|
1097 |
theory~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}.
|
neuper@42481
|
1098 |
The workflow tackled the tasks more or less following the order of the
|
neuper@42482
|
1099 |
above sections from \S\ref{isabisac} to \S\ref{funs}. At each stage
|
neuper@42482
|
1100 |
the interactivity of Isabelle/jEdit is very supportive. For instance,
|
neuper@42482
|
1101 |
as soon as the theorems for the Z-transform are established (see
|
neuper@42482
|
1102 |
\S\ref{isabisac}) it is tempting to see them at work: First we need
|
neuper@42482
|
1103 |
technical prerequisites not worth to mention and parse a string to a
|
neuper@42482
|
1104 |
term using {\sisac}'s function \textit{str2term}:
|
neuper@42482
|
1105 |
{\footnotesize\label{exp-spec}
|
neuper@42482
|
1106 |
\begin{verbatim}
|
neuper@42482
|
1107 |
ML {*
|
neuper@42482
|
1108 |
val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
|
neuper@42482
|
1109 |
val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
|
neuper@42482
|
1110 |
*}
|
neuper@42482
|
1111 |
\end{verbatim}}
|
neuper@42482
|
1112 |
Then we call {\sisac}'s rewrite-engine directly by \textit{rewrite\_} (instead via Lucas-Interpreter by \textit{Rewrite}) and yield
|
neuper@42482
|
1113 |
a rewritten term \textit{t'} together with assumptions:
|
neuper@42482
|
1114 |
{\footnotesize\label{exp-spec}
|
neuper@42482
|
1115 |
\begin{verbatim}
|
neuper@42482
|
1116 |
ML {*
|
neuper@42482
|
1117 |
val SOME (t', asm) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
|
neuper@42482
|
1118 |
*}
|
neuper@42482
|
1119 |
\end{verbatim}}
|
neuper@42482
|
1120 |
And any evaluation of an \texttt{ML} section immediately responds with the
|
neuper@42482
|
1121 |
values computed, for instance with the result of the rewrites, which above
|
neuper@42482
|
1122 |
have been returned in the internal term representation --- here are the more
|
neuper@42482
|
1123 |
readable string representations:
|
neuper@42482
|
1124 |
{\footnotesize\label{exp-spec}
|
neuper@42482
|
1125 |
\begin{verbatim}
|
neuper@42482
|
1126 |
ML {*
|
neuper@42482
|
1127 |
term2str t';
|
neuper@42482
|
1128 |
terms2str (asm);
|
neuper@42482
|
1129 |
*}
|
neuper@42482
|
1130 |
val it = "- ?u [- ?n - 1] + z / (z - α) + 1": string
|
neuper@42482
|
1131 |
val it = "[|| z || < 1]": string
|
neuper@42482
|
1132 |
\end{verbatim}}
|
neuper@42482
|
1133 |
Looking at the last line shows how the system will reliably handle
|
neuper@42482
|
1134 |
assumptions like the convergence radius.
|
neuper@42482
|
1135 |
%WN gerne w"urde ich oben das Beispiel aus subsection {*Apply Rules*}
|
neuper@42482
|
1136 |
%WN aus http://www.ist.tugraz.at/projects/isac/publ/Build_Inverse_Z_Transform.thy.
|
neuper@42482
|
1137 |
%WN Leider bekomme ich einen Fehler --- siehst Du eine schnelle Korrektur ?
|
neuper@42481
|
1138 |
|
neuper@42481
|
1139 |
|
neuper@42482
|
1140 |
.\\.\\.\\
|
neuper@42482
|
1141 |
|
neuper@42482
|
1142 |
TODO test the function \textit{argument\_of} which is embedded in the
|
neuper@42482
|
1143 |
ruleset which is used to evaluate the program by the Lucas-Interpreter.
|
neuper@42481
|
1144 |
|
neuper@42468
|
1145 |
.\\.\\.\\
|
neuper@42468
|
1146 |
|
jan@42469
|
1147 |
%JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich
|
jan@42469
|
1148 |
%JR: eingefügt; das war der beinn unserer Arbeit in
|
jan@42469
|
1149 |
%JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei
|
jan@42469
|
1150 |
%JR: jedem neuen Programm nötigen Schritte.
|
jan@42469
|
1151 |
|
neuper@42468
|
1152 |
\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
|
neuper@42468
|
1153 |
|
jan@42469
|
1154 |
\paragraph{At the beginning} of the implementation it is good to decide on one
|
jan@42469
|
1155 |
way the problem should be solved. We also did this for our Z-Transformation
|
jan@42469
|
1156 |
Problem and have choosen the way it is also thaugt in the Signal Processing
|
jan@42469
|
1157 |
Problem classes.
|
jan@42469
|
1158 |
\subparagraph{By writing down} each of this neccesarry steps we are describing
|
jan@42469
|
1159 |
one line of our upcoming program. In the following example we show the
|
jan@42469
|
1160 |
Calculation on the left and on the right the tactics in the program which
|
jan@42469
|
1161 |
created the respective formula on the left.
|
jan@42469
|
1162 |
|
jan@42469
|
1163 |
\begin{example}
|
jan@42469
|
1164 |
\hfill\\
|
neuper@42468
|
1165 |
{\small\it
|
neuper@42468
|
1166 |
\begin{tabbing}
|
neuper@42468
|
1167 |
123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
|
neuper@42468
|
1168 |
\>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
|
neuper@42468
|
1169 |
\>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
|
neuper@42468
|
1170 |
\>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\
|
neuper@42468
|
1171 |
\>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
|
neuper@42468
|
1172 |
\>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
|
neuper@42468
|
1173 |
\>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
|
neuper@42468
|
1174 |
\>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
|
neuper@42468
|
1175 |
\>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
|
neuper@42468
|
1176 |
\>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
|
neuper@42468
|
1177 |
\>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
|
neuper@42468
|
1178 |
\> \>\>\>\> \_\_\_ \`- - -\\
|
neuper@42468
|
1179 |
\>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
|
neuper@42468
|
1180 |
\>{\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@42468
|
1181 |
\>{\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} ruleYZ X'\_eq }\\
|
neuper@42468
|
1182 |
\>{\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
|
1183 |
\>{\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
|
1184 |
\end{tabbing}}
|
jan@42469
|
1185 |
|
jan@42469
|
1186 |
\end{example}
|
jan@42469
|
1187 |
|
neuper@42468
|
1188 |
% ORIGINAL FROM Inverse_Z_Transform.thy
|
neuper@42468
|
1189 |
% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
neuper@42468
|
1190 |
% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
neuper@42468
|
1191 |
% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1192 |
% " (X'_z::real) = lhs X'; "^(* ?X' z*)
|
neuper@42468
|
1193 |
% " (zzz::real) = argument_in X'_z; "^(* z *)
|
neuper@42468
|
1194 |
% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1195 |
%
|
neuper@42468
|
1196 |
% " (pbz::real) = (SubProblem (Isac', "^(**)
|
neuper@42468
|
1197 |
% " [partial_fraction,rational,simplification], "^
|
neuper@42468
|
1198 |
% " [simplification,of_rationals,to_partial_fraction]) "^
|
neuper@42468
|
1199 |
% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1200 |
%
|
neuper@42468
|
1201 |
% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1202 |
% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
neuper@42468
|
1203 |
% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1204 |
% " (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
|
1205 |
% " 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
|
1206 |
% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1207 |
% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1208 |
|
neuper@42468
|
1209 |
.\\.\\.\\
|
neuper@42468
|
1210 |
|
neuper@42468
|
1211 |
\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
|
neuper@42468
|
1212 |
TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
|
neuper@42468
|
1213 |
|
neuper@42468
|
1214 |
|
neuper@42481
|
1215 |
http://www.ist.tugraz.at/projects/isac/publ/Inverse\_Z\_Transform.thy
|
neuper@42468
|
1216 |
|
neuper@42478
|
1217 |
% \newpage
|
neuper@42478
|
1218 |
% -------------------------------------------------------------------
|
neuper@42478
|
1219 |
%
|
neuper@42478
|
1220 |
% Material, falls noch Platz bleibt ...
|
neuper@42478
|
1221 |
%
|
neuper@42478
|
1222 |
% -------------------------------------------------------------------
|
neuper@42478
|
1223 |
%
|
neuper@42478
|
1224 |
%
|
neuper@42478
|
1225 |
% \subsubsection{Trials on Notation and Termination}
|
neuper@42478
|
1226 |
%
|
neuper@42478
|
1227 |
% \paragraph{Technical notations} are a big problem for our piece of software,
|
neuper@42478
|
1228 |
% but the reason for that isn't a fault of the software itself, one of the
|
neuper@42478
|
1229 |
% troubles comes out of the fact that different technical subtopics use different
|
neuper@42478
|
1230 |
% symbols and notations for a different purpose. The most famous example for such
|
neuper@42478
|
1231 |
% a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
|
neuper@42478
|
1232 |
% math). In the specific part of signal processing one of this notation issues is
|
neuper@42478
|
1233 |
% the use of brackets --- we use round brackets for analoge signals and squared
|
neuper@42478
|
1234 |
% brackets for digital samples. Also if there is no problem for us to handle this
|
neuper@42478
|
1235 |
% fact, we have to tell the machine what notation leads to wich meaning and that
|
neuper@42478
|
1236 |
% this purpose seperation is only valid for this special topic - signal
|
neuper@42478
|
1237 |
% processing.
|
neuper@42478
|
1238 |
% \subparagraph{In the programming language} itself it is not possible to declare
|
neuper@42478
|
1239 |
% fractions, exponents, absolutes and other operators or remarks in a way to make
|
neuper@42478
|
1240 |
% them pretty to read; our only posssiblilty were ASCII characters and a handfull
|
neuper@42478
|
1241 |
% greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
|
neuper@42478
|
1242 |
% \par
|
neuper@42478
|
1243 |
% With the upper collected knowledge it is possible to check if we were able to
|
neuper@42478
|
1244 |
% donate all required terms and expressions.
|
neuper@42478
|
1245 |
%
|
neuper@42478
|
1246 |
% \subsubsection{Definition and Usage of Rules}
|
neuper@42478
|
1247 |
%
|
neuper@42478
|
1248 |
% \paragraph{The core} of our implemented problem is the Z-Transformation, due
|
neuper@42478
|
1249 |
% the fact that the transformation itself would require higher math which isn't
|
neuper@42478
|
1250 |
% yet avaible in our system we decided to choose the way like it is applied in
|
neuper@42478
|
1251 |
% labratory and problem classes at our university - by applying transformation
|
neuper@42478
|
1252 |
% rules (collected in transformation tables).
|
neuper@42478
|
1253 |
% \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
|
neuper@42478
|
1254 |
% use of axiomatizations like shown in Example~\ref{eg:ruledef}
|
neuper@42478
|
1255 |
%
|
neuper@42478
|
1256 |
% \begin{example}
|
neuper@42478
|
1257 |
% \label{eg:ruledef}
|
neuper@42478
|
1258 |
% \hfill\\
|
neuper@42478
|
1259 |
% \begin{verbatim}
|
neuper@42478
|
1260 |
% axiomatization where
|
neuper@42478
|
1261 |
% rule1: ``1 = $\delta$[n]'' and
|
neuper@42478
|
1262 |
% rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
|
neuper@42478
|
1263 |
% rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
|
neuper@42478
|
1264 |
% \end{verbatim}
|
neuper@42478
|
1265 |
% \end{example}
|
neuper@42478
|
1266 |
%
|
neuper@42478
|
1267 |
% This rules can be collected in a ruleset and applied to a given expression as
|
neuper@42478
|
1268 |
% follows in Example~\ref{eg:ruleapp}.
|
neuper@42478
|
1269 |
%
|
neuper@42478
|
1270 |
% \begin{example}
|
neuper@42478
|
1271 |
% \hfill\\
|
neuper@42478
|
1272 |
% \label{eg:ruleapp}
|
neuper@42478
|
1273 |
% \begin{enumerate}
|
neuper@42478
|
1274 |
% \item Store rules in ruleset:
|
neuper@42478
|
1275 |
% \begin{verbatim}
|
neuper@42478
|
1276 |
% val inverse_Z = append_rls "inverse_Z" e_rls
|
neuper@42478
|
1277 |
% [ Thm ("rule1",num_str @{thm rule1}),
|
neuper@42478
|
1278 |
% Thm ("rule2",num_str @{thm rule2}),
|
neuper@42478
|
1279 |
% Thm ("rule3",num_str @{thm rule3})
|
neuper@42478
|
1280 |
% ];\end{verbatim}
|
neuper@42478
|
1281 |
% \item Define exression:
|
neuper@42478
|
1282 |
% \begin{verbatim}
|
neuper@42478
|
1283 |
% val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
|
neuper@42478
|
1284 |
% \item Apply ruleset:
|
neuper@42478
|
1285 |
% \begin{verbatim}
|
neuper@42478
|
1286 |
% val SOME (sample_term', asm) =
|
neuper@42478
|
1287 |
% rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
|
neuper@42478
|
1288 |
% \end{enumerate}
|
neuper@42478
|
1289 |
% \end{example}
|
neuper@42478
|
1290 |
%
|
neuper@42478
|
1291 |
% The use of rulesets makes it much easier to develop our designated applications,
|
neuper@42478
|
1292 |
% but the programmer has to be careful and patient. When applying rulesets
|
neuper@42478
|
1293 |
% two important issues have to be mentionend:
|
neuper@42478
|
1294 |
% \subparagraph{How often} the rules have to be applied? In case of
|
neuper@42478
|
1295 |
% transformations it is quite clear that we use them once but other fields
|
neuper@42478
|
1296 |
% reuqire to apply rules until a special condition is reached (e.g.
|
neuper@42478
|
1297 |
% a simplification is finished when there is nothing to be done left).
|
neuper@42478
|
1298 |
% \subparagraph{The order} in which rules are applied often takes a big effect
|
neuper@42478
|
1299 |
% and has to be evaluated for each purpose once again.
|
neuper@42478
|
1300 |
% \par
|
neuper@42478
|
1301 |
% In our special case of Signal Processing and the rules defined in
|
neuper@42478
|
1302 |
% Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
|
neuper@42478
|
1303 |
% constants. After this step has been done it no mather which rule fit's next.
|
neuper@42478
|
1304 |
%
|
neuper@42478
|
1305 |
% \subsubsection{Helping Functions}
|
neuper@42478
|
1306 |
%
|
neuper@42478
|
1307 |
% \paragraph{New Programms require,} often new ways to get through. This new ways
|
neuper@42478
|
1308 |
% means that we handle functions that have not been in use yet, they can be
|
neuper@42478
|
1309 |
% something special and unique for a programm or something famous but unneeded in
|
neuper@42478
|
1310 |
% the system yet. In our dedicated example it was for example neccessary to split
|
neuper@42478
|
1311 |
% a fraction into numerator and denominator; the creation of such function and
|
neuper@42478
|
1312 |
% even others is described in upper Sections~\ref{simp} and \ref{funs}.
|
neuper@42478
|
1313 |
%
|
neuper@42478
|
1314 |
% \subsubsection{Trials on equation solving}
|
neuper@42478
|
1315 |
% %simple eq and problem with double fractions/negative exponents
|
neuper@42478
|
1316 |
% \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
|
neuper@42478
|
1317 |
% equations degree one and two. Solving equations in the first degree is no
|
neuper@42478
|
1318 |
% problem, wether for a student nor for our machine; but even second degree
|
neuper@42478
|
1319 |
% equations can lead to big troubles. The origin of this troubles leads from
|
neuper@42478
|
1320 |
% the build up process of our equation solving functions; they have been
|
neuper@42478
|
1321 |
% implemented some time ago and of course they are not as good as we want them to
|
neuper@42478
|
1322 |
% be. Wether or not following we only want to show how cruel it is to build up new
|
neuper@42478
|
1323 |
% work on not well fundamentials.
|
neuper@42478
|
1324 |
% \subparagraph{A simple equation solving,} can be set up as shown in the next
|
neuper@42478
|
1325 |
% example:
|
neuper@42478
|
1326 |
%
|
neuper@42478
|
1327 |
% \begin{example}
|
neuper@42478
|
1328 |
% \begin{verbatim}
|
neuper@42478
|
1329 |
%
|
neuper@42478
|
1330 |
% val fmz =
|
neuper@42478
|
1331 |
% ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
|
neuper@42478
|
1332 |
% "solveFor z",
|
neuper@42478
|
1333 |
% "solutions L"];
|
neuper@42478
|
1334 |
%
|
neuper@42478
|
1335 |
% val (dI',pI',mI') =
|
neuper@42478
|
1336 |
% ("Isac",
|
neuper@42478
|
1337 |
% ["abcFormula","degree_2","polynomial","univariate","equation"],
|
neuper@42478
|
1338 |
% ["no_met"]);\end{verbatim}
|
neuper@42478
|
1339 |
% \end{example}
|
neuper@42478
|
1340 |
%
|
neuper@42478
|
1341 |
% Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
|
neuper@42478
|
1342 |
% a short overview on the commands; at first we set up the equation and tell the
|
neuper@42478
|
1343 |
% machine what's the bound variable and where to store the solution. Second step
|
neuper@42478
|
1344 |
% is to define the equation type and determine if we want to use a special method
|
neuper@42478
|
1345 |
% to solve this type.) Simple checks tell us that the we will get two results for
|
neuper@42478
|
1346 |
% this equation and this results will be real.
|
neuper@42478
|
1347 |
% So far it is easy for us and for our machine to solve, but
|
neuper@42478
|
1348 |
% mentioned that a unvariate equation second order can have three different types
|
neuper@42478
|
1349 |
% of solutions it is getting worth.
|
neuper@42478
|
1350 |
% \subparagraph{The solving of} all this types of solutions is not yet supported.
|
neuper@42478
|
1351 |
% Luckily it was needed for us; but something which has been needed in this
|
neuper@42478
|
1352 |
% context, would have been the solving of an euation looking like:
|
neuper@42478
|
1353 |
% $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
|
neuper@42478
|
1354 |
% before (remember that befor it was no problem to handle for the machine) but
|
neuper@42478
|
1355 |
% now, after a simple equivalent transformation, we are not able to solve
|
neuper@42478
|
1356 |
% it anymore.
|
neuper@42478
|
1357 |
% \subparagraph{Error messages} we get when we try to solve something like upside
|
neuper@42478
|
1358 |
% were very confusing and also leads us to no special hint about a problem.
|
neuper@42478
|
1359 |
% \par The fault behind is, that we have no well error handling on one side and
|
neuper@42478
|
1360 |
% no sufficient formed equation solving on the other side. This two facts are
|
neuper@42478
|
1361 |
% making the implemention of new material very difficult.
|
neuper@42478
|
1362 |
%
|
neuper@42478
|
1363 |
% \subsection{Formalization of missing knowledge in Isabelle}
|
neuper@42478
|
1364 |
%
|
neuper@42478
|
1365 |
% \paragraph{A problem} behind is the mechanization of mathematic
|
neuper@42478
|
1366 |
% theories in TP-bases languages. There is still a huge gap between
|
neuper@42478
|
1367 |
% these algorithms and this what we want as a solution - in Example
|
neuper@42478
|
1368 |
% Signal Processing.
|
neuper@42478
|
1369 |
%
|
neuper@42478
|
1370 |
% \vbox{
|
neuper@42478
|
1371 |
% \begin{example}
|
neuper@42478
|
1372 |
% \label{eg:gap}
|
neuper@42478
|
1373 |
% \[
|
neuper@42478
|
1374 |
% X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
|
neuper@42478
|
1375 |
% \]
|
neuper@42478
|
1376 |
% {\small\textit{
|
neuper@42478
|
1377 |
% \noindent A very simple example on this what we call gap is the
|
neuper@42478
|
1378 |
% simplification above. It is needles to say that it is correct and also
|
neuper@42478
|
1379 |
% Isabelle for fills it correct - \emph{always}. But sometimes we don't
|
neuper@42478
|
1380 |
% want expand such terms, sometimes we want another structure of
|
neuper@42478
|
1381 |
% them. Think of a problem were we now would need only the coefficients
|
neuper@42478
|
1382 |
% of $X$ and $Y$. This is what we call the gap between mechanical
|
neuper@42478
|
1383 |
% simplification and the solution.
|
neuper@42478
|
1384 |
% }}
|
neuper@42478
|
1385 |
% \end{example}
|
neuper@42478
|
1386 |
% }
|
neuper@42478
|
1387 |
%
|
neuper@42478
|
1388 |
% \paragraph{We are not able to fill this gap,} until we have to live
|
neuper@42478
|
1389 |
% with it but first have a look on the meaning of this statement:
|
neuper@42478
|
1390 |
% Mechanized math starts from mathematical models and \emph{hopefully}
|
neuper@42478
|
1391 |
% proceeds to match physics. Academic engineering starts from physics
|
neuper@42478
|
1392 |
% (experimentation, measurement) and then proceeds to mathematical
|
neuper@42478
|
1393 |
% modeling and formalization. The process from a physical observance to
|
neuper@42478
|
1394 |
% a mathematical theory is unavoidable bound of setting up a big
|
neuper@42478
|
1395 |
% collection of standards, rules, definition but also exceptions. These
|
neuper@42478
|
1396 |
% are the things making mechanization that difficult.
|
neuper@42478
|
1397 |
%
|
neuper@42478
|
1398 |
% \vbox{
|
neuper@42478
|
1399 |
% \begin{example}
|
neuper@42478
|
1400 |
% \label{eg:units}
|
neuper@42478
|
1401 |
% \[
|
neuper@42478
|
1402 |
% m,\ kg,\ s,\ldots
|
neuper@42478
|
1403 |
% \]
|
neuper@42478
|
1404 |
% {\small\textit{
|
neuper@42478
|
1405 |
% \noindent Think about some units like that one's above. Behind
|
neuper@42478
|
1406 |
% each unit there is a discerning and very accurate definition: One
|
neuper@42478
|
1407 |
% Meter is the distance the light travels, in a vacuum, through the time
|
neuper@42478
|
1408 |
% of 1 / 299.792.458 second; one kilogram is the weight of a
|
neuper@42478
|
1409 |
% platinum-iridium cylinder in paris; and so on. But are these
|
neuper@42478
|
1410 |
% definitions usable in a computer mechanized world?!
|
neuper@42478
|
1411 |
% }}
|
neuper@42478
|
1412 |
% \end{example}
|
neuper@42478
|
1413 |
% }
|
neuper@42478
|
1414 |
%
|
neuper@42478
|
1415 |
% \paragraph{A computer} or a TP-System builds on programs with
|
neuper@42478
|
1416 |
% predefined logical rules and does not know any mathematical trick
|
neuper@42478
|
1417 |
% (follow up example \ref{eg:trick}) or recipe to walk around difficult
|
neuper@42478
|
1418 |
% expressions.
|
neuper@42478
|
1419 |
%
|
neuper@42478
|
1420 |
% \vbox{
|
neuper@42478
|
1421 |
% \begin{example}
|
neuper@42478
|
1422 |
% \label{eg:trick}
|
neuper@42478
|
1423 |
% \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
|
neuper@42478
|
1424 |
% \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
|
neuper@42478
|
1425 |
% \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
|
neuper@42478
|
1426 |
% \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
|
neuper@42478
|
1427 |
% {\small\textit{
|
neuper@42478
|
1428 |
% \noindent Sometimes it is also useful to be able to apply some
|
neuper@42478
|
1429 |
% \emph{tricks} to get a beautiful and particularly meaningful result,
|
neuper@42478
|
1430 |
% which we are able to interpret. But as seen in this example it can be
|
neuper@42478
|
1431 |
% hard to find out what operations have to be done to transform a result
|
neuper@42478
|
1432 |
% into a meaningful one.
|
neuper@42478
|
1433 |
% }}
|
neuper@42478
|
1434 |
% \end{example}
|
neuper@42478
|
1435 |
% }
|
neuper@42478
|
1436 |
%
|
neuper@42478
|
1437 |
% \paragraph{The only possibility,} for such a system, is to work
|
neuper@42478
|
1438 |
% through its known definitions and stops if none of these
|
neuper@42478
|
1439 |
% fits. Specified on Signal Processing or any other application it is
|
neuper@42478
|
1440 |
% often possible to walk through by doing simple creases. This creases
|
neuper@42478
|
1441 |
% are in general based on simple math operational but the challenge is
|
neuper@42478
|
1442 |
% to teach the machine \emph{all}\footnote{Its pride to call it
|
neuper@42478
|
1443 |
% \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
|
neuper@42478
|
1444 |
% reach a high level of \emph{all} but it in real it will still be a
|
neuper@42478
|
1445 |
% survey of knowledge which links to other knowledge and {{\sisac}{}} a
|
neuper@42478
|
1446 |
% trainer and helper but no human compensating calculator.
|
neuper@42478
|
1447 |
% \par
|
neuper@42478
|
1448 |
% {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
|
neuper@42478
|
1449 |
% specifications of problems out of topics from Signal Processing, etc.)
|
neuper@42478
|
1450 |
% and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
|
neuper@42478
|
1451 |
% physical knowledge. The result is a three-dimensional universe of
|
neuper@42478
|
1452 |
% mathematics seen in Figure~\ref{fig:mathuni}.
|
neuper@42478
|
1453 |
%
|
neuper@42478
|
1454 |
% \begin{figure}
|
neuper@42478
|
1455 |
% \begin{center}
|
neuper@42478
|
1456 |
% \includegraphics{fig/universe}
|
neuper@42478
|
1457 |
% \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
|
neuper@42478
|
1458 |
% combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
|
neuper@42478
|
1459 |
% leads to a three dimensional math universe.\label{fig:mathuni}}
|
neuper@42478
|
1460 |
% \end{center}
|
neuper@42478
|
1461 |
% \end{figure}
|
neuper@42478
|
1462 |
%
|
neuper@42478
|
1463 |
% %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
|
neuper@42478
|
1464 |
% %WN bitte folgende Bezeichnungen nehmen:
|
neuper@42478
|
1465 |
% %WN
|
neuper@42478
|
1466 |
% %WN axis 1: Algorithmic Knowledge (Programs)
|
neuper@42478
|
1467 |
% %WN axis 2: Application-oriented Knowledge (Specifications)
|
neuper@42478
|
1468 |
% %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
|
neuper@42478
|
1469 |
% %WN
|
neuper@42478
|
1470 |
% %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
|
neuper@42478
|
1471 |
% %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
|
neuper@42478
|
1472 |
% %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
|
neuper@42478
|
1473 |
%
|
neuper@42478
|
1474 |
% %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
|
neuper@42478
|
1475 |
% %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
|
neuper@42478
|
1476 |
% %JR gefordert werden WN2...
|
neuper@42478
|
1477 |
% %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
|
neuper@42478
|
1478 |
% %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
|
neuper@42478
|
1479 |
% %WN2 zusammenschneiden um die R"ander weg zu bekommen)
|
neuper@42478
|
1480 |
% %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
|
neuper@42478
|
1481 |
% %WN2 png + pdf figures mitzuschicken.
|
neuper@42478
|
1482 |
%
|
neuper@42478
|
1483 |
% \subsection{Notes on Problems with Traditional Notation}
|
neuper@42478
|
1484 |
%
|
neuper@42478
|
1485 |
% \paragraph{During research} on these topic severely problems on
|
neuper@42478
|
1486 |
% traditional notations have been discovered. Some of them have been
|
neuper@42478
|
1487 |
% known in computer science for many years now and are still unsolved,
|
neuper@42478
|
1488 |
% one of them aggregates with the so called \emph{Lambda Calculus},
|
neuper@42478
|
1489 |
% Example~\ref{eg:lamda} provides a look on the problem that embarrassed
|
neuper@42478
|
1490 |
% us.
|
neuper@42478
|
1491 |
%
|
neuper@42478
|
1492 |
% \vbox{
|
neuper@42478
|
1493 |
% \begin{example}
|
neuper@42478
|
1494 |
% \label{eg:lamda}
|
neuper@42478
|
1495 |
%
|
neuper@42478
|
1496 |
% \[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
|
neuper@42478
|
1497 |
%
|
neuper@42478
|
1498 |
%
|
neuper@42478
|
1499 |
% \[ f(p)=\ldots\; p \in \quad R \]
|
neuper@42478
|
1500 |
%
|
neuper@42478
|
1501 |
% {\small\textit{
|
neuper@42478
|
1502 |
% \noindent Above we see two equations. The first equation aims to
|
neuper@42478
|
1503 |
% be a mapping of an function from the reel range to the reel one, but
|
neuper@42478
|
1504 |
% when we change only one letter we get the second equation which
|
neuper@42478
|
1505 |
% usually aims to insert a reel point $p$ into the reel function. In
|
neuper@42478
|
1506 |
% computer science now we have the problem to tell the machine (TP) the
|
neuper@42478
|
1507 |
% difference between this two notations. This Problem is called
|
neuper@42478
|
1508 |
% \emph{Lambda Calculus}.
|
neuper@42478
|
1509 |
% }}
|
neuper@42478
|
1510 |
% \end{example}
|
neuper@42478
|
1511 |
% }
|
neuper@42478
|
1512 |
%
|
neuper@42478
|
1513 |
% \paragraph{An other problem} is that terms are not full simplified in
|
neuper@42478
|
1514 |
% traditional notations, in {{\sisac}} we have to simplify them complete
|
neuper@42478
|
1515 |
% to check weather results are compatible or not. in e.g. the solutions
|
neuper@42478
|
1516 |
% of an second order linear equation is an rational in {{\sisac}} but in
|
neuper@42478
|
1517 |
% tradition we keep fractions as long as possible and as long as they
|
neuper@42478
|
1518 |
% aim to be \textit{beautiful} (1/8, 5/16,...).
|
neuper@42478
|
1519 |
% \subparagraph{The math} which should be mechanized in Computer Theorem
|
neuper@42478
|
1520 |
% Provers (\emph{TP}) has (almost) a problem with traditional notations
|
neuper@42478
|
1521 |
% (predicate calculus) for axioms, definitions, lemmas, theorems as a
|
neuper@42478
|
1522 |
% computer program or script is not able to interpret every Greek or
|
neuper@42478
|
1523 |
% Latin letter and every Greek, Latin or whatever calculations
|
neuper@42478
|
1524 |
% symbol. Also if we would be able to handle these symbols we still have
|
neuper@42478
|
1525 |
% a problem to interpret them at all. (Follow up \hbox{Example
|
neuper@42478
|
1526 |
% \ref{eg:symbint1}})
|
neuper@42478
|
1527 |
%
|
neuper@42478
|
1528 |
% \vbox{
|
neuper@42478
|
1529 |
% \begin{example}
|
neuper@42478
|
1530 |
% \label{eg:symbint1}
|
neuper@42478
|
1531 |
% \[
|
neuper@42478
|
1532 |
% u\left[n\right] \ \ldots \ unitstep
|
neuper@42478
|
1533 |
% \]
|
neuper@42478
|
1534 |
% {\small\textit{
|
neuper@42478
|
1535 |
% \noindent The unitstep is something we need to solve Signal
|
neuper@42478
|
1536 |
% Processing problem classes. But in {{{\sisac}{}}} the rectangular
|
neuper@42478
|
1537 |
% brackets have a different meaning. So we abuse them for our
|
neuper@42478
|
1538 |
% requirements. We get something which is not defined, but usable. The
|
neuper@42478
|
1539 |
% Result is syntax only without semantic.
|
neuper@42478
|
1540 |
% }}
|
neuper@42478
|
1541 |
% \end{example}
|
neuper@42478
|
1542 |
% }
|
neuper@42478
|
1543 |
%
|
neuper@42478
|
1544 |
% In different problems, symbols and letters have different meanings and
|
neuper@42478
|
1545 |
% ask for different ways to get through. (Follow up \hbox{Example
|
neuper@42478
|
1546 |
% \ref{eg:symbint2}})
|
neuper@42478
|
1547 |
%
|
neuper@42478
|
1548 |
% \vbox{
|
neuper@42478
|
1549 |
% \begin{example}
|
neuper@42478
|
1550 |
% \label{eg:symbint2}
|
neuper@42478
|
1551 |
% \[
|
neuper@42478
|
1552 |
% \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
|
neuper@42478
|
1553 |
% \]
|
neuper@42478
|
1554 |
% {\small\textit{
|
neuper@42478
|
1555 |
% \noindent For using exponents the three \texttt{widehat} symbols
|
neuper@42478
|
1556 |
% are required. The reason for that is due the development of
|
neuper@42478
|
1557 |
% {{{\sisac}{}}} the single \texttt{widehat} and also the double were
|
neuper@42478
|
1558 |
% already in use for different operations.
|
neuper@42478
|
1559 |
% }}
|
neuper@42478
|
1560 |
% \end{example}
|
neuper@42478
|
1561 |
% }
|
neuper@42478
|
1562 |
%
|
neuper@42478
|
1563 |
% \paragraph{Also the output} can be a problem. We are familiar with a
|
neuper@42478
|
1564 |
% specified notations and style taught in university but a computer
|
neuper@42478
|
1565 |
% program has no knowledge of the form proved by a professor and the
|
neuper@42478
|
1566 |
% machines themselves also have not yet the possibilities to print every
|
neuper@42478
|
1567 |
% symbol (correct) Recent developments provide proofs in a human
|
neuper@42478
|
1568 |
% readable format but according to the fact that there is no money for
|
neuper@42478
|
1569 |
% good working formal editors yet, the style is one thing we have to
|
neuper@42478
|
1570 |
% live with.
|
neuper@42478
|
1571 |
%
|
neuper@42478
|
1572 |
% \section{Problems rising out of the Development Environment}
|
neuper@42478
|
1573 |
%
|
neuper@42478
|
1574 |
% fehlermeldungen! TODO
|
jan@42463
|
1575 |
|
neuper@42492
|
1576 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
|
neuper@42492
|
1577 |
|
neuper@42464
|
1578 |
\section{Conclusion}\label{conclusion}
|
neuper@42492
|
1579 |
This paper gives a first experience report about programming with a
|
neuper@42492
|
1580 |
TP-based programming language.
|
jan@42463
|
1581 |
|
neuper@42492
|
1582 |
\medskip A brief re-introduction of the novel kind of programming
|
neuper@42492
|
1583 |
language by example of the {\sisac}-prototype makes the paper
|
neuper@42492
|
1584 |
self-contained. The main section describes all the main concepts
|
neuper@42492
|
1585 |
involved in TP-based programming and all the sub-tasks concerning
|
neuper@42492
|
1586 |
respective implementation: mechanisation of mathematics and domain
|
neuper@42492
|
1587 |
modelling, implementation of term rewriting systems for the
|
neuper@42492
|
1588 |
rewriting-engine, formal (implicit) specification of the problem to be
|
neuper@42492
|
1589 |
(explicitly) described by the program, implement the many components
|
neuper@42492
|
1590 |
required for Lucas-Interpretation and finally implementation of the
|
neuper@42492
|
1591 |
program itself.
|
neuper@42492
|
1592 |
|
neuper@42492
|
1593 |
The many concepts and sub-tasks involved in programming require a
|
neuper@42492
|
1594 |
comprehensive workflow; first experiences with the workflow as
|
neuper@42492
|
1595 |
supported by the present prototype are described as well: Isabelle +
|
neuper@42492
|
1596 |
Isar + jEdit provide appropriate components for establishing an
|
neuper@42492
|
1597 |
efficient development environment integrating computation and
|
neuper@42492
|
1598 |
deduction. However, the present state of the prototype is far off a
|
neuper@42492
|
1599 |
state appropriate for wide-spread use: the prototype of the program
|
neuper@42492
|
1600 |
language lacks expressiveness and elegance, the prototype of the
|
neuper@42492
|
1601 |
development environment is hardly usable: error messages still address
|
neuper@42492
|
1602 |
the developer of the prototype's interpreter rather than the
|
neuper@42492
|
1603 |
application programmer, implementation of the many settings for the
|
neuper@42492
|
1604 |
Lucas-Interpreter is cumbersome.
|
neuper@42492
|
1605 |
|
neuper@42492
|
1606 |
From these experiences a successful proof of concept can be concluded:
|
neuper@42492
|
1607 |
programming arbitrary problems from engineering sciences is possible,
|
neuper@42492
|
1608 |
in principle even in the prototype. Furthermore the experiences allow
|
neuper@42492
|
1609 |
to conclude detailed requirements for further development:
|
neuper@42492
|
1610 |
\begin{itemize}
|
neuper@42492
|
1611 |
\item Clarify underlying logics such that programming is smoothly
|
neuper@42492
|
1612 |
integrated with verification of the program; the post-condition should
|
neuper@42492
|
1613 |
be proved more or less automatically, otherwise working engineers
|
neuper@42492
|
1614 |
would not encounter such programming.
|
neuper@42492
|
1615 |
\item Combine the prototype's programming language with Isabelle's
|
neuper@42492
|
1616 |
powerful function package and probably with more of SML's
|
neuper@42492
|
1617 |
pattern-matching features; include parallel execution on multi-core
|
neuper@42492
|
1618 |
machines into the language desing.
|
neuper@42492
|
1619 |
\item Extend the prototype's Lucas-Interpreter such that it also
|
neuper@42492
|
1620 |
handles functions defined by use of Isabelle's functions package; and
|
neuper@42492
|
1621 |
generalize Isabelle's code generator such that efficient code for the
|
neuper@42492
|
1622 |
whole of the defined programming language can be generated (for
|
neuper@42492
|
1623 |
multi-core machines).
|
neuper@42492
|
1624 |
\item Develop an efficient development environment with
|
neuper@42492
|
1625 |
integration of programming and proving, with management not only of
|
neuper@42492
|
1626 |
Isabelle theories, but also of large collections of specifications and
|
neuper@42492
|
1627 |
of programs.
|
neuper@42492
|
1628 |
\end{itemize}
|
neuper@42492
|
1629 |
Provided successful accomplishment, these points provide distinguished
|
neuper@42492
|
1630 |
components for virtual workbenches appealing to practictioner of
|
neuper@42492
|
1631 |
engineering in the near future.
|
neuper@42492
|
1632 |
|
neuper@42492
|
1633 |
\medskip And all programming with a TP-based language will
|
neuper@42492
|
1634 |
subsequently create interactive tutoring as a side-effect:
|
neuper@42492
|
1635 |
Lucas-Interpretation not only provides an interactive programming
|
neuper@42492
|
1636 |
environment, Lucas-Interpretation also can provide TP-based services
|
neuper@42492
|
1637 |
for a flexible dialog component with adaptive user guidance for
|
neuper@42492
|
1638 |
independent and inquiry-based learning.
|
neuper@42492
|
1639 |
|
jan@42463
|
1640 |
|
jan@42463
|
1641 |
\bibliographystyle{alpha}
|
jan@42463
|
1642 |
\bibliography{references}
|
jan@42463
|
1643 |
|
jan@42463
|
1644 |
\end{document} |