1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 18:27:17 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 21:34:20 2012 +0200
1.3 @@ -794,7 +794,7 @@
1.4 shall extract the argument \textit{z}.
1.5
1.6 \medskip In order to be recognised as a function constant in the
1.7 -program source the function needs to be declared in a theory, here in
1.8 +program source the constant needs to be declared in a theory, here in
1.9 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
1.10 the context \textit{ctxt} of that theory:
1.11 {\footnotesize
1.12 @@ -809,12 +809,14 @@
1.13 \end{verbatim}}
1.14
1.15 \noindent Parsing produces a term \texttt{t} in internal
1.16 -representation, consisting of \texttt{Const ("argument'\_in", type)}
1.17 -and the two variables \texttt{Free ("X", type)} and \texttt{Free ("z",
1.18 -type)}, \texttt{\$} is the term constructor. The function body below is
1.19 -implemented directly in ML, i.e in an \texttt{ML \{* *\}} block; the
1.20 -function definition provides a unique prefix \texttt{eval\_} to the
1.21 -function name:
1.22 +representation~\footnote{The attentive reader realizes the delicate
1.23 +differences between interal and extermal representation even in the
1.24 +strings, i.e \texttt{'\_}}, consisting of \texttt{Const
1.25 +("argument'\_in", type)} and the two variables \texttt{Free ("X",
1.26 +type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
1.27 +constructor. The function body below is implemented directly in ML,
1.28 +i.e in an \texttt{ML \{* *\}} block; the function definition provides
1.29 +a unique prefix \texttt{eval\_} to the function name:
1.30
1.31 {\footnotesize
1.32 \begin{verbatim}
1.33 @@ -1250,91 +1252,152 @@
1.34 IDEs.
1.35
1.36 \subsection{Preparations and Trials}\label{flow-prep}
1.37 +The many sub-tasks to be accomplished {\em before} the first line of
1.38 +program code can be written and tested suggest an approach which
1.39 +step-wise establishes the prerequisites. The case study underlying
1.40 +this paper~\cite{jrocnik-bakk} documents the approach in a separate
1.41 +Isabelle theory,
1.42 +\textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
1.43 +II in the study comprises this theory, \LaTeX ed from the theory by
1.44 +use of Isabelle's document preparation system. This paper resembles
1.45 +the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
1.46 +implementation work involves several iterations.
1.47
1.48 +\bigskip For instance, only the last step, implementing the program
1.49 +described in \S\ref{meth}, reveals details required. Let us assume,
1.50 +this is the ML-function \textit{argument\_in} required in line {\rm 06}
1.51 +of the example program on p.\pageref{s:impl}; how this function needs
1.52 +to be implemented in the prototype has been discussed in \S\ref{funs}
1.53 +already.
1.54
1.55 - --- the re-use
1.56 -of
1.57 +Now let us assume, that calling this function from the program code
1.58 +does not work; so testing this function is required in order to find out
1.59 +the reason: type errors, a missing entry of the function somewhere or
1.60 +even more nasty technicalities \dots
1.61
1.62 -
1.63 -
1.64 -
1.65 -and so it is for
1.66 -interactive program development; the specific requirements raised by interactive
1.67 -programming will be mentioned separately.
1.68 -
1.69 -The development in the {\sisac}-prototype was done in a separate
1.70 -theory~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}.
1.71 -The workflow tackled the tasks more or less following the order of the
1.72 -above sections from \S\ref{isabisac} to \S\ref{funs}. At each stage
1.73 -the interactivity of Isabelle/jEdit is very supportive. For instance,
1.74 -as soon as the theorems for the Z-transform are established (see
1.75 -\S\ref{isabisac}) it is tempting to see them at work: First we need
1.76 -technical prerequisites not worth to mention and parse a string to a
1.77 -term using {\sisac}'s function \textit{str2term}:
1.78 -
1.79 -.\\.\\.\\
1.80 -
1.81 -\cite{jrocnik-bakk}
1.82 -
1.83 -.\\.\\.\\
1.84 -
1.85 -{\footnotesize\label{exp-spec}
1.86 +{\footnotesize
1.87 \begin{verbatim}
1.88 ML {*
1.89 - val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.90 - val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.91 + val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1.92 + val SOME (str, t') = eval_argument_in ""
1.93 + "Build_Inverse_Z_Transform.argument'_in" t 0;
1.94 *}
1.95 + ML {*
1.96 + term2str t';
1.97 + *}
1.98 + val it = "(argument_in X z) = z": string
1.99 \end{verbatim}}
1.100 -Then we call {\sisac}'s rewrite-engine directly by \textit{rewrite\_} (instead via Lucas-Interpreter by \textit{Rewrite}) and yield
1.101 -a rewritten term \textit{t'} together with assumptions:
1.102 -{\footnotesize\label{exp-spec}
1.103 +
1.104 +\noindent So, this works: we get an ad-hoc theorem, which used in
1.105 +rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
1.106 +reduction and create a rule-set \texttt{rls} for that purpose:
1.107 +
1.108 +{\footnotesize
1.109 \begin{verbatim}
1.110 ML {*
1.111 - val SOME (t', asm) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
1.112 + val rls = append_rls "test" e_rls
1.113 + [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1.114 *}
1.115 + ML {*
1.116 + val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1.117 + *}
1.118 + val t' = Free ("z", "RealDef.real"): term
1.119 + val asm = []: term list
1.120 \end{verbatim}}
1.121 -And any evaluation of an \texttt{ML} section immediately responds with the
1.122 -values computed, for instance with the result of the rewrites, which above
1.123 -have been returned in the internal term representation --- here are the more
1.124 -readable string representations:
1.125 -{\footnotesize\label{exp-spec}
1.126 +
1.127 +\noindent The resulting term \texttt{t'} is \texttt{Free ("z",
1.128 +"RealDef.real")}, i.e the variable \texttt{z}, so all is
1.129 +perfect. Probably we have forgotten to store this function correctly~?
1.130 +We review the respective \texttt{calclist} (again an
1.131 +\textit{Unsynchronized.ref} to be removed in order to adjust to
1.132 +IsabelleIsar's asyncronous document model):
1.133 +
1.134 +{\footnotesize
1.135 +\begin{verbatim}
1.136 + calclist:= overwritel (! calclist,
1.137 + [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1.138 + ...
1.139 + ]);
1.140 +\end{verbatim}}
1.141 +
1.142 +\noindent The entry is perfect. So what is the reason~? Ah, probably there
1.143 +is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1.144 +right, the function \texttt{argument\_in} is not contained in the respective
1.145 +rule-set \textit{srls} \dots this just as an example of the intricacies in
1.146 +debugging a program in the present state of the prototype.
1.147 +
1.148 +\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.149 +Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
1.150 +usually developed within several iterations, the program can be
1.151 +assembled; on p.\pageref{s:impl} there is the complete program of the
1.152 +running example.
1.153 +
1.154 +The completion of this program required efforts for several weeks
1.155 +(after some months of familiarisation with {\sisac}), caused by the
1.156 +abundance of intricacies indicated above. Also writing the program is
1.157 +not pleasant, given Isabelle/Isar/ without add-ons for
1.158 +programming. Already writing and parsing a few lines of program code
1.159 +is a challenge: the program is an Isabelle term; Isabelle's parser,
1.160 +however, is not meant for huge terms like the program of the running
1.161 +example. So reading out the specific error (usually type errors) from
1.162 +Isabelle's message is difficult.
1.163 +
1.164 +\medskip Testing the evaluation of the program has to rely on very
1.165 +simple tools. Step-wise execution is modelled by a function
1.166 +\texttt{me}, short for mathematics-engine~\footnote{The interface used
1.167 +by the fron-end which created the calculation on
1.168 +p.\pageref{fig-interactive} is different from this function}:
1.169 +%the following is a simplification of the actual function
1.170 +
1.171 +{\footnotesize
1.172 +\begin{verbatim}
1.173 + ML {* me; *}
1.174 + val it = tac -> ctree * pos -> mout * tac * ctree * pos
1.175 +\end{verbatim}}
1.176 +
1.177 +\noindent This function takes as arguments a tactic \texttt{tac} which
1.178 +determines the next step, the step applied to the interpreter-state
1.179 +\texttt{ctree * pos} as last argument taken. The interpreter-state is
1.180 +a pair of a tree \texttt{ctree} representing the calculation created
1.181 +(see the example below) and a position \texttt{pos} in the
1.182 +calculation. The function delivers a quadrupel, beginning with the new
1.183 +formula \texttt{mout} and the next tactic followed by the new
1.184 +interpreter-state.
1.185 +
1.186 +This function allows to stepwise check the program:
1.187 +
1.188 +{\footnotesize
1.189 \begin{verbatim}
1.190 ML {*
1.191 - term2str t';
1.192 - terms2str (asm);
1.193 - *}
1.194 - val it = "- ?u [- ?n - 1] + z / (z - α) + 1": string
1.195 - val it = "[|| z || < 1]": string
1.196 -\end{verbatim}}
1.197 -Looking at the last line shows how the system will reliably handle
1.198 -assumptions like the convergence radius.
1.199 -%WN gerne w"urde ich oben das Beispiel aus subsection {*Apply Rules*}
1.200 -%WN aus http://www.ist.tugraz.at/projects/isac/publ/Build_Inverse_Z_Transform.thy.
1.201 -%WN Leider bekomme ich einen Fehler --- siehst Du eine schnelle Korrektur ?
1.202 + val fmz =
1.203 + ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1.204 + "stepResponse (x[n::real]::bool)"];
1.205 + val (dI,pI,mI) =
1.206 + ("Isac",
1.207 + ["Inverse", "Z_Transform", "SignalProcessing"],
1.208 + ["SignalProcessing","Z_Transform","Inverse"]);
1.209 +
1.210 + val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1.211 + val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.212 + val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.213 + val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.214 + ...
1.215 +\end{verbatim}}
1.216
1.217 +\noindent Several douzens of calls for \texttt{me} are required to
1.218 +create the lines in the calculation below (including the sub-problems
1.219 +not shown). When an error occurs, the reason might be located
1.220 +many steps before: if evaluation by rewriting, as done by the prototype,
1.221 +fails, then first nothing happens --- the effects come later and
1.222 +cause unpleasant checks.
1.223
1.224 -.\\.\\.\\
1.225 -
1.226 -TODO test the function \textit{argument\_of} which is embedded in the
1.227 -ruleset which is used to evaluate the program by the Lucas-Interpreter.
1.228 -
1.229 -.\\.\\.\\
1.230 -
1.231 -%JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich
1.232 -%JR: eingefügt; das war der beinn unserer Arbeit in
1.233 -%JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei
1.234 -%JR: jedem neuen Programm nötigen Schritte.
1.235 -
1.236 -\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.237 -
1.238 -\paragraph{At the beginning} of the implementation it is good to decide on one
1.239 -way the problem should be solved. We also did this for our Z-Transformation
1.240 -Problem and have choosen the way it is also thaugt in the Signal Processing
1.241 -Problem classes.
1.242 -\subparagraph{By writing down} each of this neccesarry steps we are describing
1.243 -one line of our upcoming program. In the following example we show the
1.244 -Calculation on the left and on the right the tactics in the program which
1.245 -created the respective formula on the left.
1.246 +The checks comprise watching the rewrite-engine for many different
1.247 +kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
1.248 +particular the environment and the context at the states position ---
1.249 +all checks have to rely on simple functions accessing the
1.250 +\texttt{ctree}. So getting the calculation below (which resembles the
1.251 +calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
1.252 +finished successfully is a relief:
1.253
1.254 {\small\it\label{exp-calc}
1.255 \begin{tabbing}
1.256 @@ -1377,13 +1440,22 @@
1.257 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.258 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.259
1.260 -.\\.\\.\\
1.261 +\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1.262 +Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
1.263 +and the knowledge accumulated in it can be distributed to appropriate
1.264 +theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
1.265 +sub-problem accomplishing the partial fraction decomposition to
1.266 +\textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
1.267 +internals, this kind of distribution is not trivial. For instance, the
1.268 +function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
1.269 +string with the theory it has been defined in, so this string needs to
1.270 +be updated from \texttt{Build\_Inverse\_Z\_Transform} to
1.271 +\texttt{Atools} if that function is transferred to theory
1.272 +\textit{Atools.thy}.
1.273
1.274 -\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1.275 -TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
1.276 -
1.277 -
1.278 -http://www.ist.tugraz.at/projects/isac/publ/Inverse\_Z\_Transform.thy
1.279 +In order to obtain the functionality presented in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive} data must be exported from SML-structures to XML.
1.280 +This process is also rather bare-bones without authoring tools and is
1.281 +described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
1.282
1.283 % \newpage
1.284 % -------------------------------------------------------------------