1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 10:39:58 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 18:27:17 2012 +0200
1.3 @@ -469,13 +469,13 @@
1.4 The tacticals are not treated as break-points by Lucas-Interpretation
1.5 and thus do not contribute to the calculation nor to interaction.
1.6
1.7 -\section{Development of a Program on Trial}\label{trial}
1.8 -As mentioned above, {\sisac} is an experimental system for a proof of
1.9 -concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The
1.10 -latter interprets a specific kind of TP-based programming language,
1.11 -which is as experimental as the whole prototype --- so programming in
1.12 -this language can be only ``on trial'', presently. However, as a
1.13 -prototype, the language addresses essentials described below.
1.14 +\section{Concepts and Tasks in TP-based Programming}\label{trial}
1.15 +%\section{Development of a Program on Trial}
1.16 +
1.17 +This section presents all the concepts involved in TP-based
1.18 +programming and all the tasks to be accomplished by programmers. The
1.19 +presentation uses the running example which has been introduced in
1.20 +Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
1.21
1.22 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
1.23
1.24 @@ -625,8 +625,7 @@
1.25 % allows to omit proofs. Such a theorem is shown in
1.26 % Example~\ref{eg:neuper1}.
1.27
1.28 -The running example, introduced by Fig.\ref{fig-interactive} on
1.29 -p.\pageref{fig-interactive}, requires to determine the inverse $\cal
1.30 +The running example requires to determine the inverse $\cal
1.31 Z$-transform for a class of functions. The domain of Signal Processing
1.32 is accustomed to specific notation for the resulting functions, which
1.33 are absolutely summable and are called TODO: $u[n]$, where $u$ is the
1.34 @@ -750,14 +749,17 @@
1.35 [ Thm ("rule1",num_str @{thm rule1}),
1.36 Thm ("rule2",num_str @{thm rule2}),
1.37 Thm ("rule3",num_str @{thm rule3})
1.38 - ];\end{verbatim}
1.39 + ];
1.40 + \end{verbatim}
1.41 \item Define exression:
1.42 \begin{verbatim}
1.43 - val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
1.44 + val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";
1.45 + \end{verbatim}
1.46 \item Apply ruleset:
1.47 \begin{verbatim}
1.48 val SOME (sample_term', asm) =
1.49 - rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
1.50 + rewrite_set_ thy true inverse_Z sample_term;
1.51 + \end{verbatim}
1.52 \end{enumerate}
1.53 %\end{example}
1.54
1.55 @@ -776,99 +778,176 @@
1.56 constants. After this step has been done it no mather which rule fit's next.
1.57
1.58 \subsection{Preparation of ML-Functions}\label{funs}
1.59 +The prototype's Lucas-Interpreter uses the {\sisac}-rewrite-engine for
1.60 +all kinds of evaluation. Some functionality required in programming,
1.61 +however, cannot be accomplished by rewriting. So the prototype has a
1.62 +mechanism to call ML-functions during rewriting, and the programmer has
1.63 +to use this mechanism.
1.64
1.65 -\paragraph{Explicit Problems} require explicit methods to solve them, and within
1.66 -this methods we have some explicit steps to do. This steps can be unique for
1.67 -a special problem or refindable in other problems. No mather what case, such
1.68 -steps often require some technical functions behind. For the solving process
1.69 -of the Inverse Z Transformation and the corresponding partial fraction it was
1.70 -neccessary to build helping functions like \texttt{get\_denominator},
1.71 -\texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
1.72 -to filter the denominator or numerator out of a fraction, last one helps us to
1.73 -get to know the bound variable in a equation.
1.74 -\par
1.75 -By taking \texttt{get\_denominator} as an example, we want to explain how to
1.76 -implement new functions into the existing system and how we can later use them
1.77 -in our program.
1.78 +In the running example's program on p.\pageref{s:impl} the lines {\rm
1.79 +05} and {\rm 06} contain such functions; we go into the details with
1.80 +\textit{argument\_in X\_z;}. This function fetches the argument from a
1.81 +function application: Line {\rm 03} in the example calculation on
1.82 +p.\pageref{exp-calc} is created by line {\rm 06} of the example
1.83 +program on p.\pageref{s:impl} where the program's environment assigns
1.84 +the value \textit{X z} to the variable \textit{X\_z}; so the function
1.85 +shall extract the argument \textit{z}.
1.86
1.87 -\subsubsection{Find a place to Store the Function}
1.88 +\medskip In order to be recognised as a function constant in the
1.89 +program source the function needs to be declared in a theory, here in
1.90 +\textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
1.91 +the context \textit{ctxt} of that theory:
1.92 +{\footnotesize
1.93 +\begin{verbatim}
1.94 + consts
1.95 + argument'_in :: "real => real" ("argument'_in _" 10)
1.96 +
1.97 + ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
1.98
1.99 -The whole system builds up on a well defined structure of Knowledge. This
1.100 -Knowledge sets up at the Path:
1.101 -\begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
1.102 -For implementing the Function \texttt{get\_denominator} (which let us extract
1.103 -the denominator out of a fraction) we have choosen the Theory (file)
1.104 -\texttt{Rational.thy}.
1.105 + val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
1.106 + $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
1.107 +\end{verbatim}}
1.108
1.109 -\subsubsection{Write down the new Function}
1.110 +\noindent Parsing produces a term \texttt{t} in internal
1.111 +representation, consisting of \texttt{Const ("argument'\_in", type)}
1.112 +and the two variables \texttt{Free ("X", type)} and \texttt{Free ("z",
1.113 +type)}, \texttt{\$} is the term constructor. The function body below is
1.114 +implemented directly in ML, i.e in an \texttt{ML \{* *\}} block; the
1.115 +function definition provides a unique prefix \texttt{eval\_} to the
1.116 +function name:
1.117
1.118 -In upper Theory we now define the new function and its purpose:
1.119 +{\footnotesize
1.120 \begin{verbatim}
1.121 - get_denominator :: "real => real"
1.122 -\end{verbatim}
1.123 -This command tells the machine that a function with the name
1.124 -\texttt{get\_denominator} exists which gets a real expression as argument and
1.125 -returns once again a real expression. Now we are able to implement the function
1.126 -itself, upcoming example now shows the implementation of
1.127 -\texttt{get\_denominator}.
1.128 + ML {*
1.129 + fun eval_argument_in _
1.130 + "Build_Inverse_Z_Transform.argument'_in"
1.131 + (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ =
1.132 + if is_Free arg (*could be something to be simplified before*)
1.133 + then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg)))
1.134 + else NONE
1.135 + | eval_argument_in _ _ _ _ = NONE;
1.136 + *}
1.137 +\end{verbatim}}
1.138
1.139 -%\begin{example}
1.140 - \label{eg:getdenom}
1.141 - \begin{verbatim}
1.142 +\noindent The function body creates either creates \texttt{NONE}
1.143 +telling the rewrite-engine to search for the next redex, or creates an
1.144 +ad-hoc theorem for rewriting, thus the programmer needs to adopt many
1.145 +technicalities of Isabelle, for instance, the \textit{Trueprop}
1.146 +constant.
1.147
1.148 -01 (*
1.149 -02 *("get_denominator",
1.150 -03 * ("Rational.get_denominator", eval_get_denominator ""))
1.151 -04 *)
1.152 -05 fun eval_get_denominator (thmid:string) _
1.153 -06 (t as Const ("Rational.get_denominator", _) $
1.154 -07 (Const ("Rings.inverse_class.divide", _) $num
1.155 -08 $denom)) thy =
1.156 -09 SOME (mk_thmid thmid ""
1.157 -10 (Print_Mode.setmp []
1.158 -11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1.159 -12 Trueprop $ (mk_equality (t, denom)))
1.160 -13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
1.161 -%\end{example}
1.162 +\bigskip This sub-task particularly sheds light on basic issues in the
1.163 +design of a programming language, the integration of diffent language
1.164 +layers, the layer of Isabelle/Isar and Isabelle/ML.
1.165
1.166 -Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
1.167 -there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
1.168 -splittet
1.169 -into its two parts (\texttt{\$num \$denom}). The lines before are additionals
1.170 -commands for declaring the function and the lines after are modeling and
1.171 -returning a real variable out of \texttt{\$denom}.
1.172 +Another point of improvement for the prototype is the rewrite-engine: The
1.173 +program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
1.174 +and {\rm 06} to
1.175
1.176 -\subsubsection{Add a test for the new Function}
1.177 +{\small\it\label{s:impl}
1.178 +\begin{tabbing}
1.179 +123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.180 +\>{\rm 05/6}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
1.181 +\end{tabbing}}
1.182
1.183 -\paragraph{Everytime when adding} a new function it is essential also to add
1.184 -a test for it. Tests for all functions are sorted in the same structure as the
1.185 -knowledge it self and can be found up from the path:
1.186 -\begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
1.187 -This tests are nothing very special, as a first prototype the functionallity
1.188 -of a function can be checked by evaluating the result of a simple expression
1.189 -passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
1.190 -\textit{just} created function \texttt{get\_denominator}.
1.191 +\noindent because nested function calls would require creating redexes
1.192 +inside-out; however, the prototype's rewrite-engine only works top down
1.193 +from the root of a term down to the leaves.
1.194
1.195 -%\begin{example}
1.196 -\label{eg:getdenomtest}
1.197 -\begin{verbatim}
1.198 +How all these ugly technicalities are to be checked in the prototype is
1.199 +shown in \S\ref{flow-prep} below.
1.200
1.201 -01 val thy = @{theory Isac};
1.202 -02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1.203 -03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1.204 -04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1.205 -05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
1.206 -%\end{example}
1.207 -
1.208 -\begin{description}
1.209 -\item[01] checks if the proofer set up on our {\sisac{}} System.
1.210 -\item[02] passes a simple expression (fraction) to our suddenly created
1.211 - function.
1.212 -\item[04] checks if the resulting variable is the correct one (in this case
1.213 - ``b'' the denominator) and returns.
1.214 -\item[05] handels the error case and reports that the function is not able to
1.215 - solve the given problem.
1.216 -\end{description}
1.217 +% \paragraph{Explicit Problems} require explicit methods to solve them, and within
1.218 +% this methods we have some explicit steps to do. This steps can be unique for
1.219 +% a special problem or refindable in other problems. No mather what case, such
1.220 +% steps often require some technical functions behind. For the solving process
1.221 +% of the Inverse Z Transformation and the corresponding partial fraction it was
1.222 +% neccessary to build helping functions like \texttt{get\_denominator},
1.223 +% \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
1.224 +% to filter the denominator or numerator out of a fraction, last one helps us to
1.225 +% get to know the bound variable in a equation.
1.226 +% \par
1.227 +% By taking \texttt{get\_denominator} as an example, we want to explain how to
1.228 +% implement new functions into the existing system and how we can later use them
1.229 +% in our program.
1.230 +%
1.231 +% \subsubsection{Find a place to Store the Function}
1.232 +%
1.233 +% The whole system builds up on a well defined structure of Knowledge. This
1.234 +% Knowledge sets up at the Path:
1.235 +% \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
1.236 +% For implementing the Function \texttt{get\_denominator} (which let us extract
1.237 +% the denominator out of a fraction) we have choosen the Theory (file)
1.238 +% \texttt{Rational.thy}.
1.239 +%
1.240 +% \subsubsection{Write down the new Function}
1.241 +%
1.242 +% In upper Theory we now define the new function and its purpose:
1.243 +% \begin{verbatim}
1.244 +% get_denominator :: "real => real"
1.245 +% \end{verbatim}
1.246 +% This command tells the machine that a function with the name
1.247 +% \texttt{get\_denominator} exists which gets a real expression as argument and
1.248 +% returns once again a real expression. Now we are able to implement the function
1.249 +% itself, upcoming example now shows the implementation of
1.250 +% \texttt{get\_denominator}.
1.251 +%
1.252 +% %\begin{example}
1.253 +% \label{eg:getdenom}
1.254 +% \begin{verbatim}
1.255 +%
1.256 +% 01 (*
1.257 +% 02 *("get_denominator",
1.258 +% 03 * ("Rational.get_denominator", eval_get_denominator ""))
1.259 +% 04 *)
1.260 +% 05 fun eval_get_denominator (thmid:string) _
1.261 +% 06 (t as Const ("Rational.get_denominator", _) $
1.262 +% 07 (Const ("Rings.inverse_class.divide", _) $num
1.263 +% 08 $denom)) thy =
1.264 +% 09 SOME (mk_thmid thmid ""
1.265 +% 10 (Print_Mode.setmp []
1.266 +% 11 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1.267 +% 12 Trueprop $ (mk_equality (t, denom)))
1.268 +% 13 | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
1.269 +% %\end{example}
1.270 +%
1.271 +% Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
1.272 +% there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont)
1.273 +% splittet
1.274 +% into its two parts (\texttt{\$num \$denom}). The lines before are additionals
1.275 +% commands for declaring the function and the lines after are modeling and
1.276 +% returning a real variable out of \texttt{\$denom}.
1.277 +%
1.278 +% \subsubsection{Add a test for the new Function}
1.279 +%
1.280 +% \paragraph{Everytime when adding} a new function it is essential also to add
1.281 +% a test for it. Tests for all functions are sorted in the same structure as the
1.282 +% knowledge it self and can be found up from the path:
1.283 +% \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
1.284 +% This tests are nothing very special, as a first prototype the functionallity
1.285 +% of a function can be checked by evaluating the result of a simple expression
1.286 +% passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
1.287 +% \textit{just} created function \texttt{get\_denominator}.
1.288 +%
1.289 +% %\begin{example}
1.290 +% \label{eg:getdenomtest}
1.291 +% \begin{verbatim}
1.292 +%
1.293 +% 01 val thy = @{theory Isac};
1.294 +% 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1.295 +% 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1.296 +% 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1.297 +% 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
1.298 +% %\end{example}
1.299 +%
1.300 +% \begin{description}
1.301 +% \item[01] checks if the proofer set up on our {\sisac{}} System.
1.302 +% \item[02] passes a simple expression (fraction) to our suddenly created
1.303 +% function.
1.304 +% \item[04] checks if the resulting variable is the correct one (in this case
1.305 +% ``b'' the denominator) and returns.
1.306 +% \item[05] handels the error case and reports that the function is not able to
1.307 +% solve the given problem.
1.308 +% \end{description}
1.309
1.310 \subsection{Specification of the Problem}\label{spec}
1.311 %WN <--> \chapter 7 der Thesis
1.312 @@ -1159,15 +1238,27 @@
1.313 of the workflow in the subsequent section.
1.314
1.315 \section{Workflow of Programming in the Prototype}\label{workflow}
1.316 -The previous section presented all the duties and tasks to be accomplished by
1.317 -programmers of TP-based languages. Some tasks are interrelated and comprehensive,
1.318 -so first experiences with the workflow in programming are noted below. The notes
1.319 -also capture requirements for future language development.
1.320 +The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
1.321 +step forward for interactive theory and proof development. The
1.322 +{\sisac}-prototype re-uses this IDE as a programming environment. The
1.323 +experiences from this re-use show, that the essential components are
1.324 +available from Isabelle/jEdit. However, additional tools and features
1.325 +are required to acchieve acceptable usability.
1.326 +
1.327 +So notable experiences are reported here, also as a requirement
1.328 +capture for further development of TP-based languages and respective
1.329 +IDEs.
1.330
1.331 \subsection{Preparations and Trials}\label{flow-prep}
1.332 -% Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''
1.333 -The new graphical user-interface of Isabelle~\cite{makar-jedit-12} is a great
1.334 -step forward for interactive theory and proof development --- and so it is for
1.335 +
1.336 +
1.337 + --- the re-use
1.338 +of
1.339 +
1.340 +
1.341 +
1.342 +
1.343 +and so it is for
1.344 interactive program development; the specific requirements raised by interactive
1.345 programming will be mentioned separately.
1.346
1.347 @@ -1180,6 +1271,13 @@
1.348 \S\ref{isabisac}) it is tempting to see them at work: First we need
1.349 technical prerequisites not worth to mention and parse a string to a
1.350 term using {\sisac}'s function \textit{str2term}:
1.351 +
1.352 +.\\.\\.\\
1.353 +
1.354 +\cite{jrocnik-bakk}
1.355 +
1.356 +.\\.\\.\\
1.357 +
1.358 {\footnotesize\label{exp-spec}
1.359 \begin{verbatim}
1.360 ML {*
1.361 @@ -1238,9 +1336,7 @@
1.362 Calculation on the left and on the right the tactics in the program which
1.363 created the respective formula on the left.
1.364
1.365 -\begin{example}
1.366 -\hfill\\
1.367 -{\small\it
1.368 +{\small\it\label{exp-calc}
1.369 \begin{tabbing}
1.370 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1.371 \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1.372 @@ -1260,9 +1356,6 @@
1.373 \>{\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}\\
1.374 \>{\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}}
1.375 \end{tabbing}}
1.376 -
1.377 -\end{example}
1.378 -
1.379 % ORIGINAL FROM Inverse_Z_Transform.thy
1.380 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.381 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)