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} }
|
jan@42463
|
339 |
\noindent \textit{The running example's program uses some of these elements
|
jan@42463
|
340 |
(marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt
|
jan@42463
|
341 |
let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for
|
jan@42463
|
342 |
lists and {\tt o} for functional (forward) composition in line
|
jan@42463
|
343 |
$10$. In fact, the whole program is an Isabelle term with specific
|
jan@42463
|
344 |
function constants like {\sc program}, {\sc Substitute} and {\sc
|
jan@42463
|
345 |
Rewrite\_Set\_Inst} in lines $01$ and $10$ 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
|
jan@42463
|
406 |
term}\Rightarrow{\it term}$:
|
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}$:
|
jan@42463
|
415 |
this tactic allows to enter a phase of interactive specification
|
jan@42463
|
416 |
of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance,
|
jan@42463
|
417 |
a specific type of equation) and a method (for instance, solving an
|
jan@42463
|
418 |
equation symbolically or numerically).
|
jan@42463
|
419 |
|
jan@42463
|
420 |
\end{description}
|
jan@42463
|
421 |
The tactics play a specific role in
|
jan@42463
|
422 |
Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
|
jan@42463
|
423 |
break-points and control is handed over to the user. The user is free
|
jan@42463
|
424 |
to investigate underlying knowledge, applicable theorems, etc. And
|
jan@42463
|
425 |
the user can proceed constructing a solution by input of a tactic to
|
jan@42463
|
426 |
be applied or by input of a formula; in the latter case the
|
jan@42463
|
427 |
Lucas-Interpreter has built up a logical context (initialised with the
|
jan@42463
|
428 |
precondition of the formal specification) such that Isabelle can
|
jan@42463
|
429 |
derive the formula from this context --- or give feedback, that no
|
jan@42463
|
430 |
derivation can be found.
|
jan@42463
|
431 |
|
jan@42463
|
432 |
\subsection{Tacticals for Control of Interpretation}
|
jan@42463
|
433 |
The flow of control in a program can be determined by {\tt if then else}
|
jan@42463
|
434 |
and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
|
jan@42463
|
435 |
by additional tacticals:
|
jan@42463
|
436 |
\begin{description}
|
jan@42463
|
437 |
\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
|
jan@42463
|
438 |
term}$: iterates over tactics which take a {\it term} as argument as
|
jan@42463
|
439 |
long as a tactic is applicable (for instance, {\it Rewrite\_Set} might
|
jan@42463
|
440 |
not be applicable).
|
jan@42463
|
441 |
|
jan@42463
|
442 |
\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
|
jan@42463
|
443 |
if {\it tactic} is applicable, then it is applied to {\it term},
|
jan@42463
|
444 |
otherwise {\it term} is passed on unchanged.
|
jan@42463
|
445 |
|
jan@42463
|
446 |
\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
jan@42463
|
447 |
term}\Rightarrow{\it term}$:
|
jan@42463
|
448 |
|
jan@42463
|
449 |
|
jan@42463
|
450 |
\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
|
jan@42463
|
451 |
term}\Rightarrow{\it term}$:
|
jan@42463
|
452 |
|
jan@42463
|
453 |
\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
|
jan@42463
|
454 |
term}\Rightarrow{\it term}$:
|
jan@42463
|
455 |
|
jan@42463
|
456 |
\end{description}
|
jan@42463
|
457 |
|
jan@42463
|
458 |
no input / output --- Lucas-Interpretation
|
jan@42463
|
459 |
|
jan@42463
|
460 |
.\\.\\.\\TODO\\.\\.\\
|
jan@42463
|
461 |
|
jan@42466
|
462 |
\section{Development of a Program on Trial}\label{trial}
|
jan@42466
|
463 |
As mentioned above, {\sisac} is an experimental system for a proof of
|
jan@42466
|
464 |
concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
|
jan@42466
|
465 |
latter interprets a specific kind of TP-based programming language,
|
jan@42466
|
466 |
which is as experimental as the whole prototype --- so programming in
|
jan@42466
|
467 |
this language can be only ``on trial'', presently. However, as a
|
jan@42466
|
468 |
prototype, the language addresses essentials described below.
|
jan@42466
|
469 |
|
jan@42466
|
470 |
\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
|
jan@42466
|
471 |
|
neuper@42467
|
472 |
%WN was Fachleute unter obigem Titel interessiert findet sich
|
jan@42466
|
473 |
%WN unterhalb des auskommentierten Textes.
|
jan@42466
|
474 |
|
jan@42466
|
475 |
%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
|
jan@42466
|
476 |
%WN auf Computer-Mathematiker fokussiert.
|
neuper@42464
|
477 |
% \paragraph{As mentioned in the introduction,} a prototype of an
|
neuper@42464
|
478 |
% educational math assistant called
|
neuper@42464
|
479 |
% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
|
neuper@42464
|
480 |
% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
|
neuper@42464
|
481 |
% the gap between (1) introducation and (2) application of mathematics:
|
neuper@42464
|
482 |
% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
|
neuper@42464
|
483 |
% requires each fact and each action justified by formal logic, so
|
neuper@42464
|
484 |
% {{{\sisac}{}}} makes justifications transparent to students in
|
neuper@42464
|
485 |
% interactive step-wise problem solving. By that way {{\sisac}} already
|
neuper@42464
|
486 |
% can serve both:
|
neuper@42464
|
487 |
% \begin{enumerate}
|
neuper@42464
|
488 |
% \item Introduction of math stuff (in e.g. partial fraction
|
neuper@42464
|
489 |
% decomposition) by stepwise explaining and exercising respective
|
neuper@42464
|
490 |
% symbolic calculations with ``next step guidance (NSG)'' and rigorously
|
neuper@42464
|
491 |
% checking steps freely input by students --- this also in context with
|
neuper@42464
|
492 |
% advanced applications (where the stuff to be taught in higher
|
neuper@42464
|
493 |
% semesters can be skimmed through by NSG), and
|
neuper@42464
|
494 |
% \item Application of math stuff in advanced engineering courses
|
neuper@42464
|
495 |
% (e.g. problems to be solved by inverse Z-transform in a Signal
|
neuper@42464
|
496 |
% Processing Lab) and now without much ado about basic math techniques
|
neuper@42464
|
497 |
% (like partial fraction decomposition): ``next step guidance'' supports
|
neuper@42464
|
498 |
% students in independently (re-)adopting such techniques.
|
neuper@42464
|
499 |
% \end{enumerate}
|
neuper@42464
|
500 |
% Before the question is answers, how {{\sisac}}
|
neuper@42464
|
501 |
% accomplishes this task from a technical point of view, some remarks on
|
neuper@42464
|
502 |
% the state-of-the-art is given, therefor follow up Section~\ref{emas}.
|
neuper@42464
|
503 |
%
|
neuper@42464
|
504 |
% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
|
neuper@42464
|
505 |
%
|
jan@42466
|
506 |
% \paragraph{Educational software in mathematics} is, if at all, based
|
jan@42466
|
507 |
% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
|
jan@42466
|
508 |
% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
|
jan@42466
|
509 |
% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
|
jan@42466
|
510 |
% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
|
jan@42466
|
511 |
% base technologies are used to program math lessons and sometimes even
|
jan@42466
|
512 |
% exercises. The latter are cumbersome: the steps towards a solution of
|
jan@42466
|
513 |
% such an interactive exercise need to be provided with feedback, where
|
jan@42466
|
514 |
% at each step a wide variety of possible input has to be foreseen by
|
jan@42466
|
515 |
% the programmer - so such interactive exercises either require high
|
neuper@42464
|
516 |
% development efforts or the exercises constrain possible inputs.
|
neuper@42464
|
517 |
%
|
jan@42466
|
518 |
% \subparagraph{A new generation} of educational math assistants (EMAs)
|
jan@42466
|
519 |
% is emerging presently, which is based on Theorem Proving (TP). TP, for
|
jan@42466
|
520 |
% instance Isabelle and Coq, is a technology which requires each fact
|
jan@42466
|
521 |
% and each action justified by formal logic. Pushed by demands for
|
jan@42466
|
522 |
% \textit{proven} correctness of safety-critical software TP advances
|
jan@42466
|
523 |
% into software engineering; from these advancements computer
|
jan@42466
|
524 |
% mathematics benefits in general, and math education in particular. Two
|
neuper@42464
|
525 |
% features of TP are immediately beneficial for learning:
|
neuper@42464
|
526 |
%
|
jan@42466
|
527 |
% \paragraph{TP have knowledge in human readable format,} that is in
|
jan@42466
|
528 |
% standard predicate calculus. TP following the LCF-tradition have that
|
jan@42466
|
529 |
% knowledge down to the basic definitions of set, equality,
|
jan@42466
|
530 |
% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
|
jan@42466
|
531 |
% following the typical deductive development of math, natural numbers
|
jan@42466
|
532 |
% are defined and their properties
|
jan@42466
|
533 |
% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
|
jan@42466
|
534 |
% etc. Present knowledge mechanized in TP exceeds high-school
|
jan@42466
|
535 |
% mathematics by far, however by knowledge required in software
|
neuper@42464
|
536 |
% technology, and not in other engineering sciences.
|
neuper@42464
|
537 |
%
|
jan@42466
|
538 |
% \paragraph{TP can model the whole problem solving process} in
|
jan@42466
|
539 |
% mathematical problem solving {\em within} a coherent logical
|
jan@42466
|
540 |
% framework. This is already being done by three projects, by
|
neuper@42464
|
541 |
% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
|
neuper@42464
|
542 |
% \par
|
jan@42466
|
543 |
% Having the whole problem solving process within a logical coherent
|
jan@42466
|
544 |
% system, such a design guarantees correctness of intermediate steps and
|
jan@42466
|
545 |
% of the result (which seems essential for math software); and the
|
jan@42466
|
546 |
% second advantage is that TP provides a wealth of theories which can be
|
jan@42466
|
547 |
% exploited for mechanizing other features essential for educational
|
neuper@42464
|
548 |
% software.
|
neuper@42464
|
549 |
%
|
neuper@42464
|
550 |
% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
|
neuper@42464
|
551 |
%
|
jan@42466
|
552 |
% One essential feature for educational software is feedback to user
|
neuper@42464
|
553 |
% input and assistance in coming to a solution.
|
neuper@42464
|
554 |
%
|
jan@42466
|
555 |
% \paragraph{Checking user input} by ATP during stepwise problem solving
|
jan@42466
|
556 |
% is being accomplished by the three projects mentioned above
|
jan@42466
|
557 |
% exclusively. They model the whole problem solving process as mentioned
|
jan@42466
|
558 |
% above, so all what happens between formalized assumptions (or formal
|
jan@42466
|
559 |
% specification) and goal (or fulfilled postcondition) can be
|
jan@42466
|
560 |
% mechanized. Such mechanization promises to greatly extend the scope of
|
neuper@42464
|
561 |
% educational software in stepwise problem solving.
|
neuper@42464
|
562 |
%
|
jan@42466
|
563 |
% \paragraph{NSG (Next step guidance)} comprises the system's ability to
|
jan@42466
|
564 |
% propose a next step; this is a challenge for TP: either a radical
|
jan@42466
|
565 |
% restriction of the search space by restriction to very specific
|
jan@42466
|
566 |
% problem classes is required, or much care and effort is required in
|
jan@42466
|
567 |
% designing possible variants in the process of problem solving
|
neuper@42464
|
568 |
% \cite{proof-strategies-11}.
|
neuper@42464
|
569 |
% \par
|
jan@42466
|
570 |
% Another approach is restricted to problem solving in engineering
|
jan@42466
|
571 |
% domains, where a problem is specified by input, precondition, output
|
jan@42466
|
572 |
% and postcondition, and where the postcondition is proven by ATP behind
|
jan@42466
|
573 |
% the scenes: Here the possible variants in the process of problem
|
jan@42466
|
574 |
% solving are provided with feedback {\em automatically}, if the problem
|
jan@42466
|
575 |
% is described in a TP-based programing language: \cite{plmms10} the
|
jan@42466
|
576 |
% programmer only describes the math algorithm without caring about
|
jan@42466
|
577 |
% interaction (the respective program is functional and even has no
|
jan@42466
|
578 |
% input or output statements!); interaction is generated as a
|
jan@42466
|
579 |
% side-effect by the interpreter --- an efficient separation of concern
|
jan@42466
|
580 |
% between math programmers and dialog designers promising application
|
neuper@42464
|
581 |
% all over engineering disciplines.
|
neuper@42464
|
582 |
%
|
neuper@42464
|
583 |
%
|
neuper@42464
|
584 |
% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
|
jan@42466
|
585 |
% Authoring new mathematics knowledge in {{\sisac}} can be compared with
|
jan@42466
|
586 |
% ``application programing'' of engineering problems; most of such
|
jan@42466
|
587 |
% programing uses CAS-based programing languages (CAS = Computer Algebra
|
neuper@42464
|
588 |
% Systems; e.g. Mathematica's or Maple's programing language).
|
neuper@42464
|
589 |
%
|
jan@42466
|
590 |
% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
|
jan@42466
|
591 |
% \cite{plmms10} for describing how to construct a solution to an
|
jan@42466
|
592 |
% engineering problem and for calling equation solvers, integration,
|
jan@42466
|
593 |
% etc~\footnote{Implementation of CAS-like functionality in TP is not
|
jan@42466
|
594 |
% primarily concerned with efficiency, but with a didactic question:
|
jan@42466
|
595 |
% What to decide for: for high-brow algorithms at the state-of-the-art
|
jan@42466
|
596 |
% or for elementary algorithms comprehensible for students?} within TP;
|
jan@42466
|
597 |
% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
|
neuper@42464
|
598 |
% are impossible for CAS which have no logics underlying.
|
neuper@42464
|
599 |
%
|
jan@42466
|
600 |
% \subparagraph{Authoring is perfect} by writing such TP based programs;
|
jan@42466
|
601 |
% the application programmer is not concerned with interaction or with
|
jan@42466
|
602 |
% user guidance: this is concern of a novel kind of program interpreter
|
jan@42466
|
603 |
% called Lucas-Interpreter. This interpreter hands over control to a
|
jan@42466
|
604 |
% dialog component at each step of calculation (like a debugger at
|
jan@42466
|
605 |
% breakpoints) and calls automated TP to check user input following
|
neuper@42464
|
606 |
% personalized strategies according to a feedback module.
|
neuper@42464
|
607 |
% \par
|
jan@42466
|
608 |
% However ``application programing with TP'' is not done with writing a
|
jan@42466
|
609 |
% program: according to the principles of TP, each step must be
|
jan@42466
|
610 |
% justified. Such justifications are given by theorems. So all steps
|
jan@42466
|
611 |
% must be related to some theorem, if there is no such theorem it must
|
jan@42466
|
612 |
% be added to the existing knowledge, which is organized in so-called
|
jan@42466
|
613 |
% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
|
jan@42466
|
614 |
% Isabelle comprises a mechanism (called ``axiomatization''), which
|
jan@42466
|
615 |
% allows to omit proofs. Such a theorem is shown in
|
neuper@42464
|
616 |
% Example~\ref{eg:neuper1}.
|
jan@42466
|
617 |
|
jan@42466
|
618 |
The running example, introduced by Fig.\ref{fig-interactive} on
|
jan@42466
|
619 |
p.\pageref{fig-interactive}, requires to determine the inverse $\cal
|
jan@42466
|
620 |
Z$-transform for a class of functions. The domain of Signal Processing
|
jan@42466
|
621 |
is accustomed to specific notation for the resulting functions, which
|
jan@42466
|
622 |
are absolutely summable and are called TODO: $u[n]$, where $u$ is the
|
jan@42466
|
623 |
function, $n$ is the argument and the brackets indicate that the
|
jan@42466
|
624 |
arguments are TODO. Surprisingly, Isabelle accepts the rules for
|
jan@42466
|
625 |
${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
|
jan@42466
|
626 |
experts might be particularly surprised, that the brackets do not
|
jan@42466
|
627 |
cause errors in typing (as lists).}:
|
neuper@42464
|
628 |
%\vbox{
|
neuper@42464
|
629 |
% \begin{example}
|
jan@42463
|
630 |
\label{eg:neuper1}
|
jan@42463
|
631 |
{\small\begin{tabbing}
|
jan@42463
|
632 |
123\=123\=123\=123\=\kill
|
jan@42463
|
633 |
\hfill \\
|
jan@42463
|
634 |
\>axiomatization where \\
|
neuper@42464
|
635 |
\>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
|
neuper@42464
|
636 |
\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
|
jan@42466
|
637 |
\>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
|
jan@42466
|
638 |
%TODO
|
jan@42466
|
639 |
\>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
|
jan@42466
|
640 |
%TODO
|
jan@42466
|
641 |
\>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
|
jan@42466
|
642 |
%TODO
|
jan@42466
|
643 |
\>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\
|
jan@42466
|
644 |
%TODO
|
jan@42463
|
645 |
\end{tabbing}
|
jan@42463
|
646 |
}
|
neuper@42464
|
647 |
% \end{example}
|
jan@42466
|
648 |
%}
|
jan@42466
|
649 |
These 6 rules can be used as conditional rewrite rules, depending on
|
jan@42466
|
650 |
the respective convergence radius. Satisfaction from accordance with traditional notation
|
jan@42466
|
651 |
contrasts with the above word {\em axiomatization}: As TP-based, the
|
jan@42466
|
652 |
programming language expects these rules as {\em proved} theorems, and
|
jan@42466
|
653 |
not as axioms implemented in the above brute force manner; otherwise
|
jan@42466
|
654 |
all the verification efforts envisaged (like proof of the
|
jan@42466
|
655 |
post-condition, see below) would be meaningless.
|
jan@42466
|
656 |
|
jan@42466
|
657 |
Isabelle provides a large body of knowledge, rigorously proven from
|
jan@42466
|
658 |
the basic axioms of mathematics~\footnote{This way of rigorously
|
jan@42466
|
659 |
deriving all knowledge from first principles is called the
|
jan@42466
|
660 |
LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced
|
jan@42466
|
661 |
knowledge can be found in the theoris on Multivariate
|
jan@42466
|
662 |
Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
|
jan@42466
|
663 |
building up knowledge such that a proof for the above rules would be
|
jan@42466
|
664 |
reasonably short and easily comprehensible, still requires lots of
|
jan@42466
|
665 |
work (and is definitely out of scope of our case study).
|
jan@42466
|
666 |
|
jan@42466
|
667 |
\paragraph{At the state-of-the-art in mechanization of knowledge} in
|
jan@42466
|
668 |
engineering sciences, the process does not stop with the mechanization of
|
jan@42473
|
669 |
mathematics traditionally used in these sciences. Rather, ``Formal Methods''.
|
jan@42473
|
670 |
%% \cite{TODO-formal-methods}
|
jan@42466
|
671 |
are expected to proceed to formal and explicit description of physical items. Signal Processing,
|
jan@42466
|
672 |
for instance is concerned with physical devices for signal acquisition
|
jan@42466
|
673 |
and reconstruction, which involve measuring a physical signal, storing
|
jan@42466
|
674 |
it, and possibly later rebuilding the original signal or an
|
jan@42466
|
675 |
approximation thereof. For digital systems, this typically includes
|
jan@42466
|
676 |
sampling and quantization; devices for signal compression, including
|
jan@42466
|
677 |
audio compression, image compression, and video compression, etc.
|
jan@42473
|
678 |
``Domain engineering''
|
jan@42473
|
679 |
%% \cite{db-domain-engineering}
|
jan@42473
|
680 |
is concerned with
|
jan@42466
|
681 |
{\em specification} of these devices' components and features; this
|
jan@42466
|
682 |
part in the process of mechanization is only at the beginning in domains
|
jan@42466
|
683 |
like Signal Processing.
|
jan@42466
|
684 |
|
jan@42466
|
685 |
\subparagraph{TP-based programming, concern of this paper,} is determined to
|
jan@42466
|
686 |
add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on
|
jan@42466
|
687 |
p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
|
jan@42466
|
688 |
starts with a formal {\em specification} of the problem to be solved.
|
jan@42466
|
689 |
|
jan@42466
|
690 |
|
jan@42466
|
691 |
\subsection{Specification of the Problem}\label{spec}
|
jan@42466
|
692 |
%WN <--> \chapter 7 der Thesis
|
jan@42466
|
693 |
%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
|
jan@42466
|
694 |
|
jan@42466
|
695 |
The problem of the running example is textually described in
|
jan@42466
|
696 |
Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
|
jan@42466
|
697 |
formal} specification of this problem, in traditional mathematical
|
jan@42469
|
698 |
notation, could look like is this:
|
jan@42466
|
699 |
|
jan@42466
|
700 |
%WN Hier brauchen wir die Spezifikation des 'running example' ...
|
jan@42466
|
701 |
%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
|
jan@42466
|
702 |
%JR der post condition - die existiert für uns ja eigentlich nicht aka
|
neuper@42467
|
703 |
%JR haben sie bis jetzt nicht beachtet WN...
|
neuper@42467
|
704 |
%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
|
jan@42473
|
705 |
%JR2 done
|
jan@42466
|
706 |
|
jan@42463
|
707 |
\label{eg:neuper2}
|
jan@42463
|
708 |
{\small\begin{tabbing}
|
jan@42463
|
709 |
123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
|
jan@42463
|
710 |
\hfill \\
|
neuper@42465
|
711 |
Specification:\\
|
jan@42466
|
712 |
\>input \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
|
jan@42466
|
713 |
\>precond \>: filterExpression continius on $\mathbb{R}$ \\
|
jan@42466
|
714 |
\>output \>: stepResponse $x[n]$ \\
|
jan@42469
|
715 |
\>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
|
jan@42466
|
716 |
|
jan@42473
|
717 |
\begin{remark}
|
jan@42473
|
718 |
Defining the postcondition requires a high amount mathematical
|
jan@42473
|
719 |
knowledge, the difficult part in our case is not to set up this condition
|
jan@42473
|
720 |
nor it is more to define it in a way the interpreter is able to handle it.
|
jan@42473
|
721 |
Due the fact that implementing that mechanisms is quite the same amount as
|
jan@42473
|
722 |
creating the programm itself, it is not avaible in our prototype.
|
jan@42473
|
723 |
\label{rm:postcond}
|
jan@42473
|
724 |
\end{remark}
|
jan@42469
|
725 |
|
jan@42469
|
726 |
\paragraph{The implementation} of the formal specification in the present
|
jan@42466
|
727 |
prototype, still bar-bones without support for authoring:
|
jan@42466
|
728 |
%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
|
jan@42466
|
729 |
{\footnotesize
|
jan@42466
|
730 |
\begin{verbatim}
|
jan@42466
|
731 |
01 store_specification
|
jan@42466
|
732 |
02 (prepare_specification
|
jan@42466
|
733 |
03 ["Jan Rocnik"]
|
jan@42466
|
734 |
04 "pbl_SP_Ztrans_inv"
|
jan@42466
|
735 |
05 thy
|
jan@42466
|
736 |
06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
|
jan@42466
|
737 |
07 [ ("#Given", ["filterExpression X_eq"]),
|
jan@42466
|
738 |
08 ("#Pre" , ["X_eq is_continuous"]),
|
jan@42466
|
739 |
19 ("#Find" , ["stepResponse n_eq"]),
|
jan@42466
|
740 |
10 ("#Post" , [" TODO "])],
|
jan@42466
|
741 |
11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
|
jan@42466
|
742 |
12 NONE,
|
jan@42466
|
743 |
13 [["SignalProcessing","Z_Transform","Inverse"]]));
|
jan@42466
|
744 |
\end{verbatim}}
|
jan@42466
|
745 |
Although the above details are partly very technical, we explain them
|
jan@42466
|
746 |
in order to document some intricacies of TP-based programming in the
|
jan@42466
|
747 |
present state of the {\sisac} prototype:
|
jan@42466
|
748 |
\begin{description}
|
jan@42466
|
749 |
\item[01..02]\textit{store\_specification:} stores the result of the
|
jan@42466
|
750 |
function \textit{prep\_specification} in a global reference
|
jan@42466
|
751 |
\textit{Unsynchronized.ref}, which causes principal conflicts with
|
jan@42466
|
752 |
Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
|
jan@42466
|
753 |
parallel execution~\cite{Makarius-09:parall-proof} and is under
|
jan@42466
|
754 |
reconstruction already.
|
jan@42466
|
755 |
|
jan@42466
|
756 |
\textit{prep\_pbt:} translates the specification to an internal format
|
jan@42466
|
757 |
which allows efficient processing; see for instance line {\rm 07}
|
jan@42466
|
758 |
below.
|
jan@42466
|
759 |
\item[03..04] are the ``mathematics author'' holding the copy-rights
|
jan@42466
|
760 |
and a unique identifier for the specification within {\sisac},
|
jan@42466
|
761 |
complare line {\rm 06}.
|
jan@42466
|
762 |
\item[05] is the Isabelle \textit{theory} required to parse the
|
jan@42466
|
763 |
specification in lines {\rm 07..10}.
|
jan@42466
|
764 |
\item[06] is a key into the tree of all specifications as presented to
|
jan@42466
|
765 |
the user (where some branches might be hidden by the dialog
|
jan@42466
|
766 |
component).
|
jan@42466
|
767 |
\item[07..10] are the specification with input, pre-condition, output
|
jan@42466
|
768 |
and post-condition respectively; the post-condition is not handled in
|
jan@42473
|
769 |
the prototype presently. (Follow up Remark~\ref{rm:postcond})
|
jan@42466
|
770 |
\item[11] creates a term rewriting system (abbreviated \textit{rls} in
|
jan@42466
|
771 |
{\sisac}) which evaluates the pre-condition for the actual input data.
|
jan@42466
|
772 |
Only if the evaluation yields \textit{True}, a program con be started.
|
jan@42466
|
773 |
\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
|
jan@42466
|
774 |
problem associated to a function from Computer Algebra (like an
|
jan@42466
|
775 |
equation solver) which is not the case here.
|
jan@42466
|
776 |
\item[13] is the specific key into the tree of programs addressing a
|
jan@42466
|
777 |
method which is able to find a solution which satiesfies the
|
jan@42466
|
778 |
post-condition of the specification.
|
jan@42466
|
779 |
\end{description}
|
jan@42466
|
780 |
|
jan@42466
|
781 |
|
jan@42466
|
782 |
%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
|
jan@42466
|
783 |
%WN ...
|
jan@42466
|
784 |
% type pbt =
|
jan@42466
|
785 |
% {guh : guh, (*unique within this isac-knowledge*)
|
jan@42466
|
786 |
% mathauthors: string list, (*copyright*)
|
jan@42466
|
787 |
% init : pblID, (*to start refinement with*)
|
jan@42466
|
788 |
% thy : theory, (* which allows to compile that pbt
|
jan@42466
|
789 |
% TODO: search generalized for subthy (ref.p.69*)
|
jan@42466
|
790 |
% (*^^^ WN050912 NOT used during application of the problem,
|
jan@42466
|
791 |
% because applied terms may be from 'subthy' as well as from super;
|
jan@42466
|
792 |
% thus we take 'maxthy'; see match_ags !*)
|
jan@42466
|
793 |
% cas : term option,(*'CAS-command'*)
|
jan@42466
|
794 |
% prls : rls, (* for preds in where_*)
|
jan@42466
|
795 |
% where_: term list, (* where - predicates*)
|
jan@42466
|
796 |
% ppc : pat list,
|
jan@42466
|
797 |
% (*this is the model-pattern;
|
jan@42466
|
798 |
% it contains "#Given","#Where","#Find","#Relate"-patterns
|
jan@42466
|
799 |
% for constraints on identifiers see "fun cpy_nam"*)
|
jan@42466
|
800 |
% met : metID list}; (* methods solving the pbt*)
|
jan@42466
|
801 |
%
|
jan@42466
|
802 |
%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
|
jan@42466
|
803 |
%WN oben selbst geschrieben.
|
jan@42466
|
804 |
|
jan@42466
|
805 |
|
jan@42466
|
806 |
|
jan@42466
|
807 |
|
jan@42466
|
808 |
%WN das w"urde ich in \sec\label{progr} verschieben und
|
jan@42466
|
809 |
%WN das SubProblem partial fractions zum Erkl"aren verwenden.
|
jan@42466
|
810 |
% Such a specification is checked before the execution of a program is
|
jan@42466
|
811 |
% started, the same applies for sub-programs. In the following example
|
neuper@42465
|
812 |
% (Example~\ref{eg:subprob}) shows the call of such a subproblem:
|
neuper@42465
|
813 |
%
|
neuper@42465
|
814 |
% \vbox{
|
neuper@42465
|
815 |
% \begin{example}
|
neuper@42465
|
816 |
% \label{eg:subprob}
|
neuper@42465
|
817 |
% \hfill \\
|
neuper@42465
|
818 |
% {\ttfamily \begin{tabbing}
|
neuper@42465
|
819 |
% ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
|
neuper@42465
|
820 |
% ``\>\>[linear,univariate,equation,test],'' \\
|
neuper@42465
|
821 |
% ``\>\>[Test,solve\_linear])'' \\
|
neuper@42465
|
822 |
% ``\>[BOOL equ, REAL z])'' \\
|
neuper@42465
|
823 |
% \end{tabbing}
|
neuper@42465
|
824 |
% }
|
neuper@42465
|
825 |
% {\small\textit{
|
jan@42466
|
826 |
% \noindent If a program requires a result which has to be
|
jan@42466
|
827 |
% calculated first we can use a subproblem to do so. In our specific
|
jan@42466
|
828 |
% case we wanted to calculate the zeros of a fraction and used a
|
neuper@42465
|
829 |
% subproblem to calculate the zeros of the denominator polynom.
|
neuper@42465
|
830 |
% }}
|
neuper@42465
|
831 |
% \end{example}
|
neuper@42465
|
832 |
% }
|
jan@42466
|
833 |
|
jan@42466
|
834 |
\subsection{Implementation of the Method}\label{meth}
|
jan@42466
|
835 |
%WN <--> \chapter 7 der Thesis
|
jan@42466
|
836 |
TODO
|
jan@42466
|
837 |
\subsection{Preparation of Simplifiers for the Program}\label{simp}
|
jan@42469
|
838 |
|
jan@42475
|
839 |
\paragraph{After collecting} informations about the problem and reviewing the
|
jan@42475
|
840 |
calculations, the programm may be seem hard and heavy, therefor we can set up
|
jan@42475
|
841 |
some simplifications, for e.g. is the simplification of reational expressions
|
jan@42475
|
842 |
already provided in the {\sisac{}} system. Also obligate is the use of the
|
jan@42475
|
843 |
function \texttt{drop\_questionmarks} which excludes irrelevant symbols out of
|
jan@42475
|
844 |
the expression. (Irrelevant symbols may be result out of the system during the
|
jan@42475
|
845 |
calculation.)
|
jan@42475
|
846 |
|
jan@42475
|
847 |
\subparagraph{Simplifiers often are represented} through rulesets\footnote{More
|
jan@42475
|
848 |
information about rulesets can be found in \S\ref{sec:rules}}, this rulesets
|
jan@42475
|
849 |
tell the machine which terms should be simplified into which representation. In
|
jan@42475
|
850 |
the upcoming programm a simplification is applied only in using such rulesets
|
jan@42475
|
851 |
on existing terms.
|
jan@42475
|
852 |
\par
|
jan@42475
|
853 |
Following example line was taken out of a finished programm and shows how
|
jan@42475
|
854 |
an rational expression can be simplified.
|
jan@42475
|
855 |
|
jan@42475
|
856 |
\begin{example}
|
jan@42475
|
857 |
\begin{verbatim}
|
jan@42475
|
858 |
|
jan@42475
|
859 |
"expression = (Rewrite_Set norm_Rational False) expression;"^\end{verbatim}
|
jan@42475
|
860 |
\end{example}
|
jan@42475
|
861 |
|
jan@42475
|
862 |
\subparagraph{If other} methods for use in term with simplification are needed
|
jan@42475
|
863 |
\S\ref{funs} gives informations about new ML-Functions can be prepared.
|
jan@42469
|
864 |
|
jan@42466
|
865 |
\subsection{Preparation of ML-Functions}\label{funs}
|
jan@42469
|
866 |
|
jan@42469
|
867 |
\paragraph{Explicit Problems} require explicit methods to solve them, and within
|
jan@42469
|
868 |
this methods we have some explicit steps to do. This steps can be unique for
|
jan@42469
|
869 |
a special problem or refindable in other problems. No mather what case, such
|
jan@42469
|
870 |
steps often require some technical functions behind. For the solving process
|
jan@42469
|
871 |
of the Inverse Z Transformation and the corresponding partial fraction it was
|
jan@42469
|
872 |
neccessary to build helping functions like \texttt{get\_denominator},
|
jan@42469
|
873 |
\texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
|
jan@42473
|
874 |
to filter the denominator or numerator out of a fraction, last one helps us to
|
jan@42469
|
875 |
get to know the bound variable in a equation.
|
jan@42469
|
876 |
\par
|
jan@42473
|
877 |
By taking \texttt{get\_denominator} as an example, we want to explain how to
|
jan@42473
|
878 |
implement new functions into the existing system and how we can later use them
|
jan@42473
|
879 |
in our program.
|
jan@42469
|
880 |
|
jan@42469
|
881 |
\subsubsection{Find a place to Store the Function}
|
jan@42473
|
882 |
|
jan@42469
|
883 |
The whole system builds up on a well defined structure of Knowledge. This
|
jan@42473
|
884 |
Knowledge sets up at the Path:
|
jan@42473
|
885 |
\begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
|
jan@42470
|
886 |
For implementing the Function \texttt{get\_denominator} (which let us extract
|
jan@42470
|
887 |
the denominator out of a fraction) we have choosen the Theory (file)
|
jan@42469
|
888 |
\texttt{Rational.thy}.
|
jan@42469
|
889 |
|
jan@42469
|
890 |
\subsubsection{Write down the new Function}
|
jan@42473
|
891 |
|
jan@42470
|
892 |
In upper Theory we now define the new function and its purpose:
|
jan@42470
|
893 |
\begin{verbatim}
|
jan@42470
|
894 |
get_denominator :: "real => real"
|
jan@42470
|
895 |
\end{verbatim}
|
jan@42470
|
896 |
This command tells the machine that a function with the name
|
jan@42470
|
897 |
\texttt{get\_denominator} exists which gets a real expression as argument and
|
jan@42473
|
898 |
returns once again a real expression. Now we are able to implement the function
|
jan@42473
|
899 |
itself, Example~\ref{eg:getdenom} now shows the implementation of
|
jan@42473
|
900 |
\texttt{get\_denominator}.
|
jan@42469
|
901 |
|
jan@42469
|
902 |
\begin{example}
|
jan@42470
|
903 |
\label{eg:getdenom}
|
jan@42470
|
904 |
\begin{verbatim}
|
jan@42469
|
905 |
|
jan@42470
|
906 |
01 (*
|
jan@42470
|
907 |
02 *("get_denominator",
|
jan@42470
|
908 |
03 * ("Rational.get_denominator", eval_get_denominator ""))
|
jan@42470
|
909 |
04 *)
|
jan@42470
|
910 |
05 fun eval_get_denominator (thmid:string) _
|
jan@42470
|
911 |
06 (t as Const ("Rational.get_denominator", _) $
|
jan@42470
|
912 |
07 (Const ("Rings.inverse_class.divide", _) $num
|
jan@42470
|
913 |
08 $denom)) thy =
|
jan@42470
|
914 |
09 SOME (mk_thmid thmid ""
|
jan@42470
|
915 |
10 (Print_Mode.setmp []
|
jan@42470
|
916 |
11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
|
jan@42470
|
917 |
12 Trueprop $ (mk_equality (t, denom)))
|
jan@42470
|
918 |
13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
|
jan@42469
|
919 |
\end{example}
|
jan@42469
|
920 |
|
jan@42470
|
921 |
Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
|
jan@42470
|
922 |
there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
|
jan@42470
|
923 |
splittet
|
jan@42473
|
924 |
into its two parts (\texttt{\$num \$denom}). The lines before are additionals
|
jan@42470
|
925 |
commands for declaring the function and the lines after are modeling and
|
jan@42470
|
926 |
returning a real variable out of \texttt{\$denom}.
|
jan@42469
|
927 |
|
jan@42469
|
928 |
\subsubsection{Add a test for the new Function}
|
jan@42469
|
929 |
|
jan@42473
|
930 |
\paragraph{Everytime when adding} a new function it is essential also to add
|
jan@42473
|
931 |
a test for it. Tests for all functions are sorted in the same structure as the
|
jan@42473
|
932 |
knowledge it self and can be found up from the path:
|
jan@42473
|
933 |
\begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
|
jan@42473
|
934 |
This tests are nothing very special, as a first prototype the functionallity
|
jan@42473
|
935 |
of a function can be checked by evaluating the result of a simple expression
|
jan@42473
|
936 |
passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
|
jan@42473
|
937 |
\textit{just} created function \texttt{get\_denominator}.
|
jan@42469
|
938 |
|
jan@42473
|
939 |
\begin{example}
|
jan@42473
|
940 |
\label{eg:getdenomtest}
|
jan@42473
|
941 |
\begin{verbatim}
|
jan@42473
|
942 |
|
jan@42473
|
943 |
01 val thy = @{theory Isac};
|
jan@42473
|
944 |
02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
|
jan@42473
|
945 |
03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
|
jan@42473
|
946 |
04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
|
jan@42473
|
947 |
05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
|
jan@42473
|
948 |
\end{example}
|
jan@42473
|
949 |
|
jan@42473
|
950 |
\begin{description}
|
jan@42473
|
951 |
\item[01] checks if the proofer set up on our {\sisac{}} System.
|
jan@42473
|
952 |
\item[02] passes a simple expression (fraction) to our suddenly created
|
jan@42473
|
953 |
function.
|
jan@42473
|
954 |
\item[04] checks if the resulting variable is the correct one (in this case
|
jan@42473
|
955 |
``b'' the denominator) and returns.
|
jan@42473
|
956 |
\item[05] handels the error case and reports that the function is not able to
|
jan@42473
|
957 |
solve the given problem.
|
jan@42473
|
958 |
\end{description}
|
jan@42469
|
959 |
|
jan@42466
|
960 |
\subsection{Implementation of the TP-based Program}\label{progr}
|
neuper@42467
|
961 |
|
jan@42473
|
962 |
\paragraph{After introducing} neccesarry informations about the {\sisac{}}
|
jan@42473
|
963 |
System, the main part of a implementation in the TP-bases language can be shown.
|
jan@42473
|
964 |
\par
|
jan@42473
|
965 |
Solution~\ref{s:impl} shows us the implementation of the
|
jan@42473
|
966 |
Inverse-Z-Transformation, a description on the code is given afterwards.
|
jan@42473
|
967 |
|
jan@42473
|
968 |
\begin{solution}
|
jan@42473
|
969 |
\label{s:impl}
|
jan@42473
|
970 |
\begin{tabbing}
|
jan@42473
|
971 |
\small\it
|
neuper@42467
|
972 |
123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill
|
jan@42473
|
973 |
\> \\
|
jan@42473
|
974 |
\> \\
|
neuper@42467
|
975 |
\>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\
|
neuper@42467
|
976 |
\>{\rm 02}\>\> {\tt LET} \\
|
neuper@42468
|
977 |
\>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
|
neuper@42468
|
978 |
\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
|
neuper@42468
|
979 |
\>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
|
neuper@42468
|
980 |
\>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
|
neuper@42468
|
981 |
\>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
|
neuper@42468
|
982 |
\>{\rm 08}\>\>\>\>\>\>\>\> ( \> Isac, \\
|
neuper@42468
|
983 |
\>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction, rational, simplification]\\
|
neuper@42467
|
984 |
\>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\
|
neuper@42468
|
985 |
\>{\rm 10}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
|
neuper@42468
|
986 |
\>{\rm 12}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
|
neuper@42467
|
987 |
|
neuper@42468
|
988 |
\>{\rm 12}\>\>\> X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ; \\
|
neuper@42468
|
989 |
\>{\rm 15}\>\>\> X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\
|
neuper@42467
|
990 |
\>{\rm 16}\>\> {\tt IN } \\
|
neuper@42468
|
991 |
\>{\rm 15}\>\>\> X'\_eq
|
jan@42473
|
992 |
\end{tabbing}
|
jan@42473
|
993 |
\end{solution}
|
jan@42473
|
994 |
|
neuper@42468
|
995 |
% ORIGINAL FROM Inverse_Z_Transform.thy
|
neuper@42468
|
996 |
% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
neuper@42468
|
997 |
% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
neuper@42468
|
998 |
% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
999 |
% " (X'_z::real) = lhs X'; "^(* ?X' z*)
|
neuper@42468
|
1000 |
% " (zzz::real) = argument_in X'_z; "^(* z *)
|
neuper@42468
|
1001 |
% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1002 |
%
|
neuper@42468
|
1003 |
% " (pbz::real) = (SubProblem (Isac', "^(**)
|
neuper@42468
|
1004 |
% " [partial_fraction,rational,simplification], "^
|
neuper@42468
|
1005 |
% " [simplification,of_rationals,to_partial_fraction]) "^
|
neuper@42468
|
1006 |
% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1007 |
%
|
neuper@42468
|
1008 |
% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1009 |
% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
neuper@42468
|
1010 |
% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1011 |
% " (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
|
1012 |
% " 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
|
1013 |
% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1014 |
% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42467
|
1015 |
|
jan@42463
|
1016 |
\section{Workflow of Programming in the Prototype}\label{workflow}
|
neuper@42468
|
1017 |
|
jan@42466
|
1018 |
\subsection{Preparations and Trials}\label{flow-prep}
|
neuper@42468
|
1019 |
TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''
|
neuper@42468
|
1020 |
.\\.\\.\\
|
neuper@42468
|
1021 |
|
jan@42469
|
1022 |
%JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich
|
jan@42469
|
1023 |
%JR: eingefügt; das war der beinn unserer Arbeit in
|
jan@42469
|
1024 |
%JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei
|
jan@42469
|
1025 |
%JR: jedem neuen Programm nötigen Schritte.
|
jan@42469
|
1026 |
|
neuper@42468
|
1027 |
\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
|
neuper@42468
|
1028 |
|
jan@42469
|
1029 |
\paragraph{At the beginning} of the implementation it is good to decide on one
|
jan@42469
|
1030 |
way the problem should be solved. We also did this for our Z-Transformation
|
jan@42469
|
1031 |
Problem and have choosen the way it is also thaugt in the Signal Processing
|
jan@42469
|
1032 |
Problem classes.
|
jan@42469
|
1033 |
\subparagraph{By writing down} each of this neccesarry steps we are describing
|
jan@42469
|
1034 |
one line of our upcoming program. In the following example we show the
|
jan@42469
|
1035 |
Calculation on the left and on the right the tactics in the program which
|
jan@42469
|
1036 |
created the respective formula on the left.
|
jan@42469
|
1037 |
|
jan@42469
|
1038 |
\begin{example}
|
jan@42469
|
1039 |
\hfill\\
|
neuper@42468
|
1040 |
{\small\it
|
neuper@42468
|
1041 |
\begin{tabbing}
|
neuper@42468
|
1042 |
123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
|
neuper@42468
|
1043 |
\>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
|
neuper@42468
|
1044 |
\>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
|
neuper@42468
|
1045 |
\>{\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
|
1046 |
\>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
|
neuper@42468
|
1047 |
\>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
|
neuper@42468
|
1048 |
\>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
|
neuper@42468
|
1049 |
\>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
|
neuper@42468
|
1050 |
\>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
|
neuper@42468
|
1051 |
\>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
|
neuper@42468
|
1052 |
\>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
|
neuper@42468
|
1053 |
\> \>\>\>\> \_\_\_ \`- - -\\
|
neuper@42468
|
1054 |
\>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
|
neuper@42468
|
1055 |
\>{\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
|
1056 |
\>{\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
|
1057 |
\>{\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
|
1058 |
\>{\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
|
1059 |
\end{tabbing}}
|
jan@42469
|
1060 |
|
jan@42469
|
1061 |
\end{example}
|
jan@42469
|
1062 |
|
neuper@42468
|
1063 |
% ORIGINAL FROM Inverse_Z_Transform.thy
|
neuper@42468
|
1064 |
% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
neuper@42468
|
1065 |
% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
neuper@42468
|
1066 |
% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1067 |
% " (X'_z::real) = lhs X'; "^(* ?X' z*)
|
neuper@42468
|
1068 |
% " (zzz::real) = argument_in X'_z; "^(* z *)
|
neuper@42468
|
1069 |
% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42468
|
1070 |
%
|
neuper@42468
|
1071 |
% " (pbz::real) = (SubProblem (Isac', "^(**)
|
neuper@42468
|
1072 |
% " [partial_fraction,rational,simplification], "^
|
neuper@42468
|
1073 |
% " [simplification,of_rationals,to_partial_fraction]) "^
|
neuper@42468
|
1074 |
% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1075 |
%
|
neuper@42468
|
1076 |
% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42468
|
1077 |
% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
neuper@42468
|
1078 |
% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42468
|
1079 |
% " (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
|
1080 |
% " 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
|
1081 |
% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1082 |
% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42468
|
1083 |
|
neuper@42468
|
1084 |
.\\.\\.\\
|
neuper@42468
|
1085 |
|
neuper@42468
|
1086 |
\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
|
neuper@42468
|
1087 |
TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
|
neuper@42468
|
1088 |
|
neuper@42468
|
1089 |
|
neuper@42468
|
1090 |
|
neuper@42468
|
1091 |
|
neuper@42468
|
1092 |
\newpage
|
neuper@42468
|
1093 |
-------------------------------------------------------------------
|
neuper@42468
|
1094 |
|
neuper@42468
|
1095 |
Material, falls noch Platz bleibt ...
|
neuper@42468
|
1096 |
|
neuper@42468
|
1097 |
-------------------------------------------------------------------
|
neuper@42468
|
1098 |
|
neuper@42468
|
1099 |
|
jan@42466
|
1100 |
\subsubsection{Trials on Notation and Termination}
|
jan@42466
|
1101 |
|
jan@42466
|
1102 |
\paragraph{Technical notations} are a big problem for our piece of software,
|
jan@42466
|
1103 |
but the reason for that isn't a fault of the software itself, one of the
|
jan@42466
|
1104 |
troubles comes out of the fact that different technical subtopics use different
|
jan@42466
|
1105 |
symbols and notations for a different purpose. The most famous example for such
|
jan@42466
|
1106 |
a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
|
jan@42466
|
1107 |
math). In the specific part of signal processing one of this notation issues is
|
jan@42466
|
1108 |
the use of brackets --- we use round brackets for analoge signals and squared
|
jan@42466
|
1109 |
brackets for digital samples. Also if there is no problem for us to handle this
|
jan@42466
|
1110 |
fact, we have to tell the machine what notation leads to wich meaning and that
|
jan@42466
|
1111 |
this purpose seperation is only valid for this special topic - signal
|
jan@42466
|
1112 |
processing.
|
jan@42466
|
1113 |
\subparagraph{In the programming language} itself it is not possible to declare
|
jan@42466
|
1114 |
fractions, exponents, absolutes and other operators or remarks in a way to make
|
jan@42466
|
1115 |
them pretty to read; our only posssiblilty were ASCII characters and a handfull
|
jan@42466
|
1116 |
greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
|
jan@42466
|
1117 |
\par
|
jan@42466
|
1118 |
With the upper collected knowledge it is possible to check if we were able to
|
jan@42466
|
1119 |
donate all required terms and expressions.
|
jan@42466
|
1120 |
|
jan@42475
|
1121 |
\subsubsection{Definition and Usage of Rules\label{sec:rules}}
|
jan@42466
|
1122 |
|
jan@42466
|
1123 |
\paragraph{The core} of our implemented problem is the Z-Transformation, due
|
jan@42466
|
1124 |
the fact that the transformation itself would require higher math which isn't
|
jan@42466
|
1125 |
yet avaible in our system we decided to choose the way like it is applied in
|
jan@42466
|
1126 |
labratory and problem classes at our university - by applying transformation
|
jan@42466
|
1127 |
rules (collected in transformation tables).
|
jan@42466
|
1128 |
\paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
|
jan@42466
|
1129 |
use of axiomatizations like shown in Example~\ref{eg:ruledef}
|
jan@42466
|
1130 |
|
jan@42466
|
1131 |
\begin{example}
|
jan@42466
|
1132 |
\label{eg:ruledef}
|
jan@42466
|
1133 |
\hfill\\
|
jan@42466
|
1134 |
\begin{verbatim}
|
jan@42466
|
1135 |
axiomatization where
|
jan@42466
|
1136 |
rule1: ``1 = $\delta$[n]'' and
|
jan@42466
|
1137 |
rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
|
jan@42466
|
1138 |
rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
|
jan@42466
|
1139 |
\end{verbatim}
|
jan@42466
|
1140 |
\end{example}
|
jan@42466
|
1141 |
|
jan@42466
|
1142 |
This rules can be collected in a ruleset and applied to a given expression as
|
jan@42466
|
1143 |
follows in Example~\ref{eg:ruleapp}.
|
jan@42466
|
1144 |
|
jan@42466
|
1145 |
\begin{example}
|
jan@42466
|
1146 |
\hfill\\
|
jan@42466
|
1147 |
\label{eg:ruleapp}
|
jan@42466
|
1148 |
\begin{enumerate}
|
jan@42466
|
1149 |
\item Store rules in ruleset:
|
jan@42466
|
1150 |
\begin{verbatim}
|
jan@42466
|
1151 |
val inverse_Z = append_rls "inverse_Z" e_rls
|
jan@42466
|
1152 |
[ Thm ("rule1",num_str @{thm rule1}),
|
jan@42466
|
1153 |
Thm ("rule2",num_str @{thm rule2}),
|
jan@42466
|
1154 |
Thm ("rule3",num_str @{thm rule3})
|
jan@42466
|
1155 |
];\end{verbatim}
|
jan@42466
|
1156 |
\item Define exression:
|
jan@42466
|
1157 |
\begin{verbatim}
|
jan@42466
|
1158 |
val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
|
jan@42466
|
1159 |
\item Apply ruleset:
|
jan@42466
|
1160 |
\begin{verbatim}
|
jan@42466
|
1161 |
val SOME (sample_term', asm) =
|
jan@42466
|
1162 |
rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
|
jan@42466
|
1163 |
\end{enumerate}
|
jan@42466
|
1164 |
\end{example}
|
jan@42466
|
1165 |
|
jan@42466
|
1166 |
The use of rulesets makes it much easier to develop our designated applications,
|
jan@42466
|
1167 |
but the programmer has to be careful and patient. When applying rulesets
|
jan@42466
|
1168 |
two important issues have to be mentionend:
|
jan@42466
|
1169 |
\subparagraph{How often} the rules have to be applied? In case of
|
jan@42466
|
1170 |
transformations it is quite clear that we use them once but other fields
|
jan@42466
|
1171 |
reuqire to apply rules until a special condition is reached (e.g.
|
jan@42466
|
1172 |
a simplification is finished when there is nothing to be done left).
|
jan@42466
|
1173 |
\subparagraph{The order} in which rules are applied often takes a big effect
|
jan@42466
|
1174 |
and has to be evaluated for each purpose once again.
|
jan@42466
|
1175 |
\par
|
jan@42466
|
1176 |
In our special case of Signal Processing and the rules defined in
|
jan@42466
|
1177 |
Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
|
jan@42466
|
1178 |
constants. After this step has been done it no mather which rule fit's next.
|
jan@42466
|
1179 |
|
jan@42466
|
1180 |
\subsubsection{Helping Functions}
|
jan@42469
|
1181 |
|
jan@42469
|
1182 |
\paragraph{New Programms require,} often new ways to get through. This new ways
|
jan@42469
|
1183 |
means that we handle functions that have not been in use yet, they can be
|
jan@42469
|
1184 |
something special and unique for a programm or something famous but unneeded in
|
jan@42469
|
1185 |
the system yet. In our dedicated example it was for example neccessary to split
|
jan@42469
|
1186 |
a fraction into numerator and denominator; the creation of such function and
|
jan@42469
|
1187 |
even others is described in upper Sections~\ref{simp} and \ref{funs}.
|
jan@42469
|
1188 |
|
jan@42466
|
1189 |
\subsubsection{Trials on equation solving}
|
jan@42466
|
1190 |
%simple eq and problem with double fractions/negative exponents
|
jan@42469
|
1191 |
\paragraph{The Inverse Z-Transformation} makes it neccessary to solve
|
jan@42469
|
1192 |
equations degree one and two. Solving equations in the first degree is no
|
jan@42469
|
1193 |
problem, wether for a student nor for our machine; but even second degree
|
jan@42469
|
1194 |
equations can lead to big troubles. The origin of this troubles leads from
|
jan@42469
|
1195 |
the build up process of our equation solving functions; they have been
|
jan@42469
|
1196 |
implemented some time ago and of course they are not as good as we want them to
|
jan@42469
|
1197 |
be. Wether or not following we only want to show how cruel it is to build up new
|
jan@42469
|
1198 |
work on not well fundamentials.
|
jan@42469
|
1199 |
\subparagraph{A simple equation solving,} can be set up as shown in the next
|
jan@42469
|
1200 |
example:
|
jan@42466
|
1201 |
|
jan@42469
|
1202 |
\begin{example}
|
jan@42469
|
1203 |
\begin{verbatim}
|
jan@42469
|
1204 |
|
jan@42469
|
1205 |
val fmz =
|
jan@42469
|
1206 |
["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
|
jan@42469
|
1207 |
"solveFor z",
|
jan@42469
|
1208 |
"solutions L"];
|
jan@42466
|
1209 |
|
jan@42469
|
1210 |
val (dI',pI',mI') =
|
jan@42469
|
1211 |
("Isac",
|
jan@42469
|
1212 |
["abcFormula","degree_2","polynomial","univariate","equation"],
|
jan@42469
|
1213 |
["no_met"]);\end{verbatim}
|
jan@42469
|
1214 |
\end{example}
|
jan@42469
|
1215 |
|
jan@42469
|
1216 |
Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
|
jan@42469
|
1217 |
a short overview on the commands; at first we set up the equation and tell the
|
jan@42469
|
1218 |
machine what's the bound variable and where to store the solution. Second step
|
jan@42469
|
1219 |
is to define the equation type and determine if we want to use a special method
|
jan@42469
|
1220 |
to solve this type.) Simple checks tell us that the we will get two results for
|
jan@42469
|
1221 |
this equation and this results will be real.
|
jan@42469
|
1222 |
So far it is easy for us and for our machine to solve, but
|
jan@42469
|
1223 |
mentioned that a unvariate equation second order can have three different types
|
jan@42469
|
1224 |
of solutions it is getting worth.
|
jan@42469
|
1225 |
\subparagraph{The solving of} all this types of solutions is not yet supported.
|
jan@42469
|
1226 |
Luckily it was needed for us; but something which has been needed in this
|
jan@42469
|
1227 |
context, would have been the solving of an euation looking like:
|
jan@42469
|
1228 |
$-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
|
jan@42469
|
1229 |
before (remember that befor it was no problem to handle for the machine) but
|
jan@42469
|
1230 |
now, after a simple equivalent transformation, we are not able to solve
|
jan@42469
|
1231 |
it anymore.
|
jan@42469
|
1232 |
\subparagraph{Error messages} we get when we try to solve something like upside
|
jan@42469
|
1233 |
were very confusing and also leads us to no special hint about a problem.
|
jan@42469
|
1234 |
\par The fault behind is, that we have no well error handling on one side and
|
jan@42469
|
1235 |
no sufficient formed equation solving on the other side. This two facts are
|
jan@42469
|
1236 |
making the implemention of new material very difficult.
|
jan@42466
|
1237 |
|
jan@42463
|
1238 |
\subsection{Formalization of missing knowledge in Isabelle}
|
jan@42463
|
1239 |
|
jan@42466
|
1240 |
\paragraph{A problem} behind is the mechanization of mathematic
|
jan@42466
|
1241 |
theories in TP-bases languages. There is still a huge gap between
|
jan@42466
|
1242 |
these algorithms and this what we want as a solution - in Example
|
neuper@42464
|
1243 |
Signal Processing.
|
jan@42463
|
1244 |
|
jan@42463
|
1245 |
\vbox{
|
jan@42463
|
1246 |
\begin{example}
|
jan@42463
|
1247 |
\label{eg:gap}
|
jan@42463
|
1248 |
\[
|
jan@42463
|
1249 |
X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
|
jan@42463
|
1250 |
\]
|
jan@42463
|
1251 |
{\small\textit{
|
jan@42466
|
1252 |
\noindent A very simple example on this what we call gap is the
|
jan@42466
|
1253 |
simplification above. It is needles to say that it is correct and also
|
jan@42466
|
1254 |
Isabelle for fills it correct - \emph{always}. But sometimes we don't
|
jan@42466
|
1255 |
want expand such terms, sometimes we want another structure of
|
jan@42466
|
1256 |
them. Think of a problem were we now would need only the coefficients
|
jan@42466
|
1257 |
of $X$ and $Y$. This is what we call the gap between mechanical
|
neuper@42464
|
1258 |
simplification and the solution.
|
jan@42463
|
1259 |
}}
|
jan@42463
|
1260 |
\end{example}
|
jan@42463
|
1261 |
}
|
jan@42463
|
1262 |
|
jan@42466
|
1263 |
\paragraph{We are not able to fill this gap,} until we have to live
|
jan@42466
|
1264 |
with it but first have a look on the meaning of this statement:
|
jan@42466
|
1265 |
Mechanized math starts from mathematical models and \emph{hopefully}
|
jan@42466
|
1266 |
proceeds to match physics. Academic engineering starts from physics
|
jan@42466
|
1267 |
(experimentation, measurement) and then proceeds to mathematical
|
jan@42466
|
1268 |
modeling and formalization. The process from a physical observance to
|
jan@42466
|
1269 |
a mathematical theory is unavoidable bound of setting up a big
|
jan@42466
|
1270 |
collection of standards, rules, definition but also exceptions. These
|
neuper@42464
|
1271 |
are the things making mechanization that difficult.
|
jan@42463
|
1272 |
|
jan@42463
|
1273 |
\vbox{
|
jan@42463
|
1274 |
\begin{example}
|
jan@42463
|
1275 |
\label{eg:units}
|
jan@42463
|
1276 |
\[
|
jan@42463
|
1277 |
m,\ kg,\ s,\ldots
|
jan@42463
|
1278 |
\]
|
jan@42463
|
1279 |
{\small\textit{
|
jan@42466
|
1280 |
\noindent Think about some units like that one's above. Behind
|
jan@42466
|
1281 |
each unit there is a discerning and very accurate definition: One
|
jan@42466
|
1282 |
Meter is the distance the light travels, in a vacuum, through the time
|
jan@42466
|
1283 |
of 1 / 299.792.458 second; one kilogram is the weight of a
|
jan@42466
|
1284 |
platinum-iridium cylinder in paris; and so on. But are these
|
neuper@42464
|
1285 |
definitions usable in a computer mechanized world?!
|
jan@42463
|
1286 |
}}
|
jan@42463
|
1287 |
\end{example}
|
jan@42463
|
1288 |
}
|
jan@42463
|
1289 |
|
jan@42466
|
1290 |
\paragraph{A computer} or a TP-System builds on programs with
|
jan@42466
|
1291 |
predefined logical rules and does not know any mathematical trick
|
jan@42466
|
1292 |
(follow up example \ref{eg:trick}) or recipe to walk around difficult
|
neuper@42464
|
1293 |
expressions.
|
jan@42463
|
1294 |
|
jan@42463
|
1295 |
\vbox{
|
jan@42463
|
1296 |
\begin{example}
|
jan@42463
|
1297 |
\label{eg:trick}
|
jan@42463
|
1298 |
\[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
|
jan@42463
|
1299 |
\[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
|
jan@42463
|
1300 |
\frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
|
jan@42463
|
1301 |
\[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
|
jan@42463
|
1302 |
{\small\textit{
|
jan@42466
|
1303 |
\noindent Sometimes it is also useful to be able to apply some
|
jan@42466
|
1304 |
\emph{tricks} to get a beautiful and particularly meaningful result,
|
jan@42466
|
1305 |
which we are able to interpret. But as seen in this example it can be
|
jan@42466
|
1306 |
hard to find out what operations have to be done to transform a result
|
neuper@42464
|
1307 |
into a meaningful one.
|
jan@42463
|
1308 |
}}
|
jan@42463
|
1309 |
\end{example}
|
jan@42463
|
1310 |
}
|
jan@42463
|
1311 |
|
jan@42466
|
1312 |
\paragraph{The only possibility,} for such a system, is to work
|
jan@42466
|
1313 |
through its known definitions and stops if none of these
|
jan@42466
|
1314 |
fits. Specified on Signal Processing or any other application it is
|
jan@42466
|
1315 |
often possible to walk through by doing simple creases. This creases
|
jan@42466
|
1316 |
are in general based on simple math operational but the challenge is
|
jan@42466
|
1317 |
to teach the machine \emph{all}\footnote{Its pride to call it
|
jan@42466
|
1318 |
\emph{all}.} of them. Unfortunately the goal of TP Isabelle is to
|
jan@42466
|
1319 |
reach a high level of \emph{all} but it in real it will still be a
|
jan@42466
|
1320 |
survey of knowledge which links to other knowledge and {{\sisac}{}} a
|
neuper@42464
|
1321 |
trainer and helper but no human compensating calculator.
|
jan@42463
|
1322 |
\par
|
jan@42466
|
1323 |
{{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
|
jan@42466
|
1324 |
specifications of problems out of topics from Signal Processing, etc.)
|
jan@42466
|
1325 |
and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
|
jan@42466
|
1326 |
physical knowledge. The result is a three-dimensional universe of
|
neuper@42464
|
1327 |
mathematics seen in Figure~\ref{fig:mathuni}.
|
jan@42463
|
1328 |
|
jan@42466
|
1329 |
\begin{figure}
|
jan@42466
|
1330 |
\begin{center}
|
jan@42466
|
1331 |
\includegraphics{fig/universe}
|
jan@42466
|
1332 |
\caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
|
jan@42466
|
1333 |
combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
|
jan@42466
|
1334 |
leads to a three dimensional math universe.\label{fig:mathuni}}
|
jan@42466
|
1335 |
\end{center}
|
jan@42466
|
1336 |
\end{figure}
|
jan@42466
|
1337 |
|
jan@42466
|
1338 |
%WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
|
jan@42466
|
1339 |
%WN bitte folgende Bezeichnungen nehmen:
|
jan@42466
|
1340 |
%WN
|
jan@42466
|
1341 |
%WN axis 1: Algorithmic Knowledge (Programs)
|
jan@42466
|
1342 |
%WN axis 2: Application-oriented Knowledge (Specifications)
|
jan@42466
|
1343 |
%WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
|
jan@42466
|
1344 |
%WN
|
jan@42466
|
1345 |
%WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
|
jan@42466
|
1346 |
%WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
|
jan@42466
|
1347 |
%WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
|
jan@42466
|
1348 |
|
jan@42466
|
1349 |
%JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
|
jan@42466
|
1350 |
%JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
|
neuper@42467
|
1351 |
%JR gefordert werden WN2...
|
neuper@42467
|
1352 |
%WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
|
neuper@42467
|
1353 |
%WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
|
neuper@42467
|
1354 |
%WN2 zusammenschneiden um die R"ander weg zu bekommen)
|
neuper@42467
|
1355 |
%WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
|
neuper@42467
|
1356 |
%WN2 png + pdf figures mitzuschicken.
|
jan@42463
|
1357 |
|
jan@42463
|
1358 |
\subsection{Notes on Problems with Traditional Notation}
|
jan@42463
|
1359 |
|
jan@42466
|
1360 |
\paragraph{During research} on these topic severely problems on
|
jan@42466
|
1361 |
traditional notations have been discovered. Some of them have been
|
jan@42466
|
1362 |
known in computer science for many years now and are still unsolved,
|
jan@42466
|
1363 |
one of them aggregates with the so called \emph{Lambda Calculus},
|
jan@42466
|
1364 |
Example~\ref{eg:lamda} provides a look on the problem that embarrassed
|
neuper@42464
|
1365 |
us.
|
jan@42463
|
1366 |
|
jan@42463
|
1367 |
\vbox{
|
jan@42463
|
1368 |
\begin{example}
|
jan@42463
|
1369 |
\label{eg:lamda}
|
jan@42463
|
1370 |
|
jan@42463
|
1371 |
\[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
|
jan@42463
|
1372 |
|
jan@42463
|
1373 |
|
jan@42463
|
1374 |
\[ f(p)=\ldots\; p \in \quad R \]
|
jan@42463
|
1375 |
|
jan@42463
|
1376 |
{\small\textit{
|
jan@42466
|
1377 |
\noindent Above we see two equations. The first equation aims to
|
jan@42466
|
1378 |
be a mapping of an function from the reel range to the reel one, but
|
jan@42466
|
1379 |
when we change only one letter we get the second equation which
|
jan@42466
|
1380 |
usually aims to insert a reel point $p$ into the reel function. In
|
jan@42466
|
1381 |
computer science now we have the problem to tell the machine (TP) the
|
jan@42466
|
1382 |
difference between this two notations. This Problem is called
|
neuper@42464
|
1383 |
\emph{Lambda Calculus}.
|
jan@42463
|
1384 |
}}
|
jan@42463
|
1385 |
\end{example}
|
jan@42463
|
1386 |
}
|
jan@42463
|
1387 |
|
jan@42466
|
1388 |
\paragraph{An other problem} is that terms are not full simplified in
|
jan@42466
|
1389 |
traditional notations, in {{\sisac}} we have to simplify them complete
|
jan@42466
|
1390 |
to check weather results are compatible or not. in e.g. the solutions
|
jan@42466
|
1391 |
of an second order linear equation is an rational in {{\sisac}} but in
|
jan@42466
|
1392 |
tradition we keep fractions as long as possible and as long as they
|
neuper@42464
|
1393 |
aim to be \textit{beautiful} (1/8, 5/16,...).
|
jan@42466
|
1394 |
\subparagraph{The math} which should be mechanized in Computer Theorem
|
jan@42466
|
1395 |
Provers (\emph{TP}) has (almost) a problem with traditional notations
|
jan@42466
|
1396 |
(predicate calculus) for axioms, definitions, lemmas, theorems as a
|
jan@42466
|
1397 |
computer program or script is not able to interpret every Greek or
|
jan@42466
|
1398 |
Latin letter and every Greek, Latin or whatever calculations
|
jan@42466
|
1399 |
symbol. Also if we would be able to handle these symbols we still have
|
jan@42466
|
1400 |
a problem to interpret them at all. (Follow up \hbox{Example
|
neuper@42464
|
1401 |
\ref{eg:symbint1}})
|
jan@42463
|
1402 |
|
jan@42463
|
1403 |
\vbox{
|
jan@42463
|
1404 |
\begin{example}
|
jan@42463
|
1405 |
\label{eg:symbint1}
|
jan@42463
|
1406 |
\[
|
jan@42463
|
1407 |
u\left[n\right] \ \ldots \ unitstep
|
jan@42463
|
1408 |
\]
|
jan@42463
|
1409 |
{\small\textit{
|
jan@42466
|
1410 |
\noindent The unitstep is something we need to solve Signal
|
jan@42466
|
1411 |
Processing problem classes. But in {{{\sisac}{}}} the rectangular
|
jan@42466
|
1412 |
brackets have a different meaning. So we abuse them for our
|
jan@42466
|
1413 |
requirements. We get something which is not defined, but usable. The
|
neuper@42464
|
1414 |
Result is syntax only without semantic.
|
jan@42463
|
1415 |
}}
|
jan@42463
|
1416 |
\end{example}
|
jan@42463
|
1417 |
}
|
jan@42463
|
1418 |
|
jan@42466
|
1419 |
In different problems, symbols and letters have different meanings and
|
jan@42466
|
1420 |
ask for different ways to get through. (Follow up \hbox{Example
|
neuper@42464
|
1421 |
\ref{eg:symbint2}})
|
jan@42463
|
1422 |
|
jan@42463
|
1423 |
\vbox{
|
jan@42463
|
1424 |
\begin{example}
|
jan@42463
|
1425 |
\label{eg:symbint2}
|
jan@42463
|
1426 |
\[
|
jan@42463
|
1427 |
\widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent
|
jan@42463
|
1428 |
\]
|
jan@42463
|
1429 |
{\small\textit{
|
jan@42466
|
1430 |
\noindent For using exponents the three \texttt{widehat} symbols
|
jan@42466
|
1431 |
are required. The reason for that is due the development of
|
jan@42466
|
1432 |
{{{\sisac}{}}} the single \texttt{widehat} and also the double were
|
neuper@42464
|
1433 |
already in use for different operations.
|
jan@42463
|
1434 |
}}
|
jan@42463
|
1435 |
\end{example}
|
jan@42463
|
1436 |
}
|
jan@42463
|
1437 |
|
jan@42466
|
1438 |
\paragraph{Also the output} can be a problem. We are familiar with a
|
jan@42466
|
1439 |
specified notations and style taught in university but a computer
|
jan@42466
|
1440 |
program has no knowledge of the form proved by a professor and the
|
jan@42466
|
1441 |
machines themselves also have not yet the possibilities to print every
|
jan@42466
|
1442 |
symbol (correct) Recent developments provide proofs in a human
|
jan@42466
|
1443 |
readable format but according to the fact that there is no money for
|
jan@42466
|
1444 |
good working formal editors yet, the style is one thing we have to
|
neuper@42464
|
1445 |
live with.
|
jan@42463
|
1446 |
|
jan@42463
|
1447 |
\section{Problems rising out of the Development Environment}
|
jan@42463
|
1448 |
|
jan@42463
|
1449 |
fehlermeldungen! TODO
|
jan@42463
|
1450 |
|
neuper@42464
|
1451 |
\section{Conclusion}\label{conclusion}
|
jan@42463
|
1452 |
|
jan@42463
|
1453 |
TODO
|
jan@42463
|
1454 |
|
jan@42463
|
1455 |
\bibliographystyle{alpha}
|
jan@42463
|
1456 |
\bibliography{references}
|
jan@42463
|
1457 |
|
jan@42463
|
1458 |
\end{document} |