1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 22:06:39 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 22:44:56 2012 +0200
1.3 @@ -143,7 +143,7 @@
1.4 it's interpreter.
1.5
1.6 The report concludes with a positive proof of concept, states
1.7 -insuggicient usability of the prototype and captures the requirements
1.8 +insufficiency usability of the prototype and captures the requirements
1.9 for further development of both, the programming language and the
1.10 interpreter.
1.11 %
1.12 @@ -241,13 +241,13 @@
1.13 \begin{center}
1.14 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
1.15 %\includegraphics[width=140mm]{fig/isac-Ztrans-math}
1.16 -\caption{Step-wise problem solving guided by the TP-based program}
1.17 -\label{fig-interactive}
1.18 +\caption{Step-wise problem solving guided by the TP-based program
1.19 +\label{fig-interactive}}
1.20 \end{center}
1.21 \end{figure}
1.22
1.23 The problem is from the domain of Signal Processing and requests to
1.24 -determine the inverse ${\cal Z}$-transform for a given term.
1.25 +determine the inverse ${\cal z}$-transform for a given term.
1.26 Fig.\ref{fig-interactive}
1.27 also shows the beginning of the interactive construction of a solution
1.28 for the problem. This construction is done in the right window named
1.29 @@ -326,13 +326,13 @@
1.30 $\leq$ most of which are overloaded for various types.
1.31
1.32 HOL also supports some basic constructs from functional programming:
1.33 -{\it\label{isabelle-stmts}
1.34 +{\footnotesize\it\label{isabelle-stmts}
1.35 \begin{tabbing} 123\=\kill
1.36 \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
1.37 \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
1.38 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
1.39 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
1.40 -\end{tabbing} }
1.41 +\end{tabbing}}
1.42 \noindent The running example's program uses some of these elements
1.43 (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
1.44 let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
1.45 @@ -630,7 +630,7 @@
1.46 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
1.47 function, $n$ is the argument and the brackets indicate that the
1.48 arguments are discrete. Surprisingly, Isabelle accepts the rules for
1.49 -${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
1.50 +${\cal z}^{-1}$ in this traditional notation~\footnote{Isabelle
1.51 experts might be particularly surprised, that the brackets do not
1.52 cause errors in typing (as lists).}:
1.53 %\vbox{
1.54 @@ -640,16 +640,12 @@
1.55 123\=123\=123\=123\=\kill
1.56
1.57 \>axiomatization where \\
1.58 - \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\
1.59 - \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\
1.60 + \>\> rule1: ``${\cal z}^{-1}\;1 = \delta [n]$'' and\\
1.61 + \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal z}^{-1}\;z / (z - 1) = u [n]$'' and\\
1.62 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
1.63 -%TODO
1.64 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
1.65 -%TODO
1.66 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
1.67 -%TODO
1.68 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''
1.69 -%TODO
1.70 \end{tabbing}}
1.71 % \end{example}
1.72 %}
1.73 @@ -664,7 +660,7 @@
1.74 Isabelle provides a large body of knowledge, rigorously proven from
1.75 the basic axioms of mathematics~\footnote{This way of rigorously
1.76 deriving all knowledge from first principles is called the
1.77 -LCF-paradigm in TP.}. In the case of the ${\cal Z}$-Transform the most advanced
1.78 +LCF-paradigm in TP.}. In the case of the ${\cal z}$-Transform the most advanced
1.79 knowledge can be found in the theories on Multivariate
1.80 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
1.81 building up knowledge such that a proof for the above rules would be
1.82 @@ -715,45 +711,42 @@
1.83
1.84 The prototype rewrites using theorems only. Axioms which are theorems as well
1.85 have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
1.86 -assemble them in a rule-set and apply them as follows:
1.87 +assemble them in a rule-set and apply them in ML as follows:
1.88
1.89 {\footnotesize
1.90 \begin{verbatim}
1.91 - 01 ML {*
1.92 - 02 val inverse_z =
1.93 - 03 Rls
1.94 - 04 {id = "inverse_z",
1.95 - 05 rew_ord = dummy_ord,
1.96 - 06 erls = Erls,
1.97 - 07 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
1.98 - 08 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
1.99 - 09 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
1.100 - 10 errpatts = [],
1.101 - 11 scr = ""}
1.102 - 12 *}
1.103 + 01 val inverse_z = Rls
1.104 + 02 {id = "inverse_z",
1.105 + 03 rew_ord = dummy_ord,
1.106 + 04 erls = Erls,
1.107 + 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
1.108 + 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
1.109 + 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
1.110 + 08 errpatts = [],
1.111 + 09 scr = ""}
1.112 \end{verbatim}}
1.113
1.114 \noindent The items, line by line, in the above record have the following purpose:
1.115 \begin{description}
1.116 -\item[01..03] the ML-value \textit{inverse\_z} stores it's identifier
1.117 +\item[01..02] the ML-value \textit{inverse\_z} stores it's identifier
1.118 as a string for ``reflection'' when switching between the language
1.119 layers of Isabelle/ML (like in the Lucas-Interpreter) and
1.120 Isabelle/Isar (like in the example program on p.\pageref{s:impl} on
1.121 line {\rm 12}).
1.122
1.123 -\item[05..06] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
1.124 +\item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
1.125 \textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
1.126 (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
1.127 and (b) the assumptions of the \textit{rules} need not be evaluated
1.128 (they just go into the context during rewriting).
1.129
1.130 -\item[07..09] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
1.131 +\item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
1.132 also ML-functions (\S\ref{funs}) can come into this list as shown in
1.133 \S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm}
1.134 and \textit{Calc} respectively; for the purpose of reflection both
1.135 contain their identifiers.
1.136
1.137 -\item[10..11] are error-patterns not discussed here and \textit{scr}
1.138 +\item[08..09] are error-patterns not discussed here and \textit{scr}
1.139 is prepared to get a program, automatically generated by {\sisac} for
1.140 producing intermediate rewrites when requested by the user.
1.141
1.142 @@ -844,9 +837,9 @@
1.143 ML {*
1.144 fun eval_argument_in _
1.145 "Build_Inverse_Z_Transform.argument'_in"
1.146 - (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ =
1.147 + (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
1.148 if is_Free arg (*could be something to be simplified before*)
1.149 - then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg)))
1.150 + then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
1.151 else NONE
1.152 | eval_argument_in _ _ _ _ = NONE;
1.153 *}
1.154 @@ -869,7 +862,7 @@
1.155 {\small\it\label{s:impl}
1.156 \begin{tabbing}
1.157 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.158 -\>{\rm 05/6}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
1.159 +\>{\rm 05/06}\>\>\> (z::real) = argument\_in (lhs X\_eq) ;
1.160 \end{tabbing}}
1.161
1.162 \noindent because nested function calls would require creating redexes
1.163 @@ -1350,8 +1343,6 @@
1.164 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1.165 val SOME (str, t') = eval_argument_in ""
1.166 "Build_Inverse_Z_Transform.argument'_in" t 0;
1.167 - *}
1.168 - ML {*
1.169 term2str t';
1.170 *}
1.171 val it = "(argument_in X z) = z": string
1.172 @@ -1366,8 +1357,6 @@
1.173 ML {*
1.174 val rls = append_rls "test" e_rls
1.175 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1.176 - *}
1.177 - ML {*
1.178 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1.179 *}
1.180 val t' = Free ("z", "RealDef.real"): term
1.181 @@ -1445,13 +1434,11 @@
1.182 ("Isac",
1.183 ["Inverse", "Z_Transform", "SignalProcessing"],
1.184 ["SignalProcessing","Z_Transform","Inverse"]);
1.185 -
1.186 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1.187 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.188 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.189 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.190 - ...
1.191 -\end{verbatim}}
1.192 + ...\end{verbatim}}
1.193
1.194 \noindent Several dozens of calls for \texttt{me} are required to
1.195 create the lines in the calculation below (including the sub-problems
1.196 @@ -1483,8 +1470,8 @@
1.197 \>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
1.198 \> \>\>\>\> \_\_\_ \`- - -\\
1.199 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1.200 -\>{\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)}\\
1.201 -\>{\rm 13}\>\> $X^\prime z = {\cal Z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} prep\_for\_inverse\_z X'\_eq }\\
1.202 +\>{\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)}\\
1.203 +\>{\rm 13}\>\> $X^\prime z = {\cal z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} prep\_for\_inverse\_z X'\_eq }\\
1.204 \>{\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.205 \>{\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.206 \end{tabbing}}
1.207 @@ -1891,10 +1878,13 @@
1.208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
1.209
1.210 \section{Conclusion}\label{conclusion}
1.211 -This paper gives a first experience report about programming with a
1.212 -TP-based programming language.
1.213
1.214 -\medskip A brief re-introduction of the novel kind of programming
1.215 +%JR obvious
1.216 +
1.217 +%This paper gives a first experience report about programming with a
1.218 +%TP-based programming language.
1.219 +
1.220 +A brief re-introduction of the novel kind of programming
1.221 language by example of the {\sisac}-prototype makes the paper
1.222 self-contained. The main section describes all the main concepts
1.223 involved in TP-based programming and all the sub-tasks concerning