1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 06:25:30 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 17:39:07 2012 +0200
1.3 @@ -136,8 +136,11 @@
1.4 programming language''.
1.5
1.6 This paper is the experience report of the first ``application
1.7 -programmer'' using this language, the experience gained from a
1.8 -prototype of the programming language and of it's interpreter.
1.9 +programmer'' using this language for creating exercises in step-wise
1.10 +problem solving for an advanced lab in Signal Processing. The tasks
1.11 +involved in TP-based programming are described together with the
1.12 +experience gained from a prototype of the programming language and of
1.13 +it's interpreter.
1.14
1.15 The report concludes with a positive proof of concept, states
1.16 insuggicient usability of the prototype and captures the requirements
1.17 @@ -702,7 +705,7 @@
1.18 \subsection{Preparation of Simplifiers for the Program}\label{simp}
1.19
1.20 All evaluation in the prototyp's Lucas-Interpreter is done by term rewriting on
1.21 -Isabelle's terms, see \S\ref{math} below; in this section some of respective
1.22 +Isabelle's terms, see \S\ref{meth} below; in this section some of respective
1.23 preparations are described. In order to work reliably with term rewriting, the
1.24 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
1.25 then they are called (canonical) simplifiers. These properties do not go without
1.26 @@ -932,19 +935,21 @@
1.27 \begin{verbatim}
1.28 consts
1.29 argument'_in :: "real => real" ("argument'_in _" 10)
1.30 +\end{verbatim}}
1.31
1.32 - ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
1.33 - val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
1.34 - $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
1.35 -\end{verbatim}}
1.36 -
1.37 -\noindent Parsing produces a term \texttt{t} in internal
1.38 -representation~\footnote{The attentive reader realizes the
1.39 -differences between interal and extermal representation even in the
1.40 -strings, i.e \texttt{'\_}}, consisting of \texttt{Const
1.41 -("argument'\_in", type)} and the two variables \texttt{Free ("X",
1.42 -type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
1.43 -constructor. The function body below is implemented directly in SML,
1.44 +%^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
1.45 +%^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
1.46 +%^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
1.47 +%^3.2^ \end{verbatim}}
1.48 +%^3.2^
1.49 +%^3.2^ \noindent Parsing produces a term \texttt{t} in internal
1.50 +%^3.2^ representation~\footnote{The attentive reader realizes the
1.51 +%^3.2^ differences between interal and extermal representation even in the
1.52 +%^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
1.53 +%^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
1.54 +%^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
1.55 +%^3.2^ constructor.
1.56 +The function body below is implemented directly in SML,
1.57 i.e in an \texttt{ML \{* *\}} block; the function definition provides
1.58 a unique prefix \texttt{eval\_} to the function name:
1.59
1.60 @@ -1102,7 +1107,7 @@
1.61 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
1.62 %\hfill \\
1.63 \>Specification:\\
1.64 - \> \>input \>: ${\it filterExpression} \;\;X\;z=\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
1.65 + \> \>input \>: ${\it filterExpression} \;\;X\;z=\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}, \;{\it domain}\;\mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$\\
1.66 \>\>precond \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
1.67 \>\>output \>: stepResponse $x[n]$ \\
1.68 \>\>postcond \>: TODO
1.69 @@ -1133,13 +1138,13 @@
1.70 04 ["Jan Rocnik"]
1.71 05 thy
1.72 06 ( ["Inverse", "Z_Transform", "SignalProcessing"],
1.73 - 07 [ ("#Given", ["filterExpression X_eq"]),
1.74 - 08 ("#Pre" , ["(rhs X_eq) is_continuous_in R\{1/2, -1/4}"]),
1.75 + 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1.76 + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1.77 09 ("#Find" , ["stepResponse n_eq"]),
1.78 - 10 ("#Post" , [" TODO "])],
1.79 - 11 append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
1.80 - 12 NONE,
1.81 - 13 [["SignalProcessing","Z_Transform","Inverse"]]));
1.82 + 10 ("#Post" , [" TODO "])])
1.83 + 11 prls
1.84 + 12 NONE
1.85 + 13 [["SignalProcessing","Z_Transform","Inverse"]]);
1.86 14 *}
1.87 \end{verbatim}}
1.88
1.89 @@ -1165,11 +1170,12 @@
1.90 the user (where some branches might be hidden by the dialog
1.91 component).
1.92 \item[07..10] are the specification with input, pre-condition, output
1.93 -and post-condition respectively; the post-condition is not handled in
1.94 +and post-condition respectively; note that the specification contains
1.95 +variables to be instantiated with concrete values for a concrete problem ---
1.96 +thus the specification actually captures a class of problems. The post-condition is not handled in
1.97 the prototype presently.
1.98 -\item[11] creates a rule-set (abbreviated \textit{rls} in
1.99 -{\sisac}) which evaluates the pre-condition for the actual input data.
1.100 -Only if the evaluation yields \textit{True}, a program can be started.
1.101 +\item[11] is a rule-set (defined elsewhere) for evaluation of the pre-condition: \textit{(rhs X\_eq) is\_continuous\_in D}, instantiated with the values of a concrete problem, evaluates to true or false --- and all evaluation is done by
1.102 +rewriting determined by rule-sets.
1.103 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
1.104 problem associated to a function from Computer Algebra (like an
1.105 equation solver) which is not the case here.
1.106 @@ -1233,7 +1239,7 @@
1.107 \subsection{Implementation of the Method}\label{meth}
1.108 A method collects all data required to interpret a certain program by
1.109 Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
1.110 -the running example is embedded in the following method:
1.111 +the running example is embedded on the last line in the following method:
1.112 %The methods represent the different ways a problem can be solved. This can
1.113 %include mathematical tactics as well as tactics taught in different courses.
1.114 %Declaring the Method itself gives us the possibilities to describe the way of
1.115 @@ -1248,41 +1254,39 @@
1.116 03 "SP_InverseZTransformation_classic"
1.117 04 ["Jan Rocnik"]
1.118 05 thy
1.119 - 06 (["SignalProcessing", "Z_Transform", "Inverse"],
1.120 - 07 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.121 - 08 ("#Pre" , ["(rhs X_eq) is_continuous_in R\{1/2, -1/4}"]),
1.122 - 09 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.123 - 10 {rew_ord = tless_true, rls = rls,
1.124 - 11 srls = srls, calc = [],
1.125 - 12 prls = prls, crls = crls,
1.126 - 13 nrls = nrls,
1.127 - 14 errpats = []},
1.128 - 15 program));
1.129 - 16 *}
1.130 + 06 ( ["SignalProcessing", "Z_Transform", "Inverse"],
1.131 + 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1.132 + 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1.133 + 09 ("#Find" , ["stepResponse n_eq"]),
1.134 + 10 rew_ord erls
1.135 + 11 srls prls nrls
1.136 + 12 errpats
1.137 + 13 program);
1.138 + 14 *}
1.139 \end{verbatim}}
1.140
1.141 \noindent The above code stores the whole structure analogously to a
1.142 -specification,
1.143 +specification as described above:
1.144 \begin{description}
1.145 \item[01..06] are identical to those for the example specification on
1.146 p.\pageref{exp-spec}.
1.147
1.148 \item[07..09] show something looking like the specification; this is a
1.149 -{\em guard}: as long as not all \texttt{Given} items are present and
1.150 -the \texttt{Pre}-conditions is not true, interpretation of the program
1.151 +{\em guard}: as long as not all \textit{Given} items are present and
1.152 +the \textit{Pre}-conditions is not true, interpretation of the program
1.153 is not started.
1.154
1.155 -\item[01..09]
1.156 +\item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case
1.157 +\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets
1.158 +\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
1.159 +\textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analoguous to the specification in line 11 on p.\pageref{exp-spec}
1.160 +and (c) is required for the derivation-machinery checking user-input formulas.
1.161
1.162 -\item[01..09]
1.163 -
1.164 -\item[01..09]
1.165 -
1.166 -\item[01..09]
1.167 +\item[12..13] \textit{errpats} are error-patterns~\cite{gdaroczy-EP-13} for this method and \textit{program} is the variable holding the example from p.\pageref {s:impl}.
1.168 \end{description}
1.169 -
1.170 -
1.171 -.\\.\\.\\
1.172 +The many rule-sets above cause considerable efforts for the
1.173 +programmers, in particular, because there are no tools for checking
1.174 +essential features of rule-sets.
1.175
1.176 % is again very technical and goes hard in detail. Unfortunataly
1.177 % most declerations are not essential for a basic programm but leads us to a huge
1.178 @@ -1321,7 +1325,7 @@
1.179 % \end{description}
1.180
1.181 \subsection{Implementation of the TP-based Program}\label{progr}
1.182 -So finally all the prerequisites are described and the very topic can
1.183 +So finally all the prerequisites are described and the final task can
1.184 be addressed. The program below comes back to the running example: it
1.185 computes a solution for the problem from Fig.\ref{fig-interactive} on
1.186 p.\pageref{fig-interactive}. The reader is reminded of
1.187 @@ -1330,12 +1334,12 @@
1.188 {\footnotesize\it\label{s:impl}
1.189 \begin{tabbing}
1.190 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.191 -\> \>ML \{*
1.192 +\>{\rm 00}\>ML \{*\\
1.193 \>{\rm 00}\>val program =\\
1.194 \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1.195 \>{\rm 02}\>\> {\tt let} \\
1.196 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1.197 -\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
1.198 +\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
1.199 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1.200 \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1.201 \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1.202 @@ -1343,11 +1347,11 @@
1.203 %\>{\rm 10}\>\>\>\>\>\>\>\>\> [simplification, of\_rationals, to\_partial\_fraction] ) \\
1.204 \>{\rm 09}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1.205 \>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1.206 -\>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@ \\
1.207 +\>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@ \\
1.208 \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1.209 \>{\rm 13}\>\> {\tt in } \\
1.210 \>{\rm 14}\>\>\> X'\_eq"\\
1.211 -\> \>*\}
1.212 +\>{\rm 15}\>*\}
1.213 \end{tabbing}}
1.214 % ORIGINAL FROM Inverse_Z_Transform.thy
1.215 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.216 @@ -1377,7 +1381,7 @@
1.217 Lucas-Interpretation. The side-effects are triggered by the tactics
1.218 \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
1.219 \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1.220 -{\rm 12} respectively. These tactics produce the lines in the
1.221 +{\rm 12} respectively. These tactics produce the respective lines in the
1.222 calculation on p.\pageref{flow-impl}.
1.223
1.224 The above lines {\rm 05, 06} do not contain a tactics, so they do not
1.225 @@ -1576,14 +1580,14 @@
1.226 all checks have to rely on simple functions accessing the
1.227 \texttt{ctree}. So getting the calculation below (which resembles the
1.228 calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
1.229 -finished successfully is a relief:
1.230 +is the result of several weeks of development:
1.231
1.232 {\small\it\label{exp-calc}
1.233 \begin{tabbing}
1.234 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1.235 \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1.236 \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
1.237 -\>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\
1.238 +\>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} prep\_for\_part\_frac X\_eq}\\
1.239 \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
1.240 \>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
1.241 \>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
1.242 @@ -1594,10 +1598,13 @@
1.243 \> \>\>\>\> \_\_\_ \`- - -\\
1.244 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1.245 \>{\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.246 -\>{\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 }\\
1.247 +\>{\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.248 \>{\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.249 \>{\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.250 \end{tabbing}}
1.251 +The tactics on the right margin of the above calculation are those in
1.252 +the program on p.\pageref{s:impl} which create the respective formulas
1.253 +on the left.
1.254 % ORIGINAL FROM Inverse_Z_Transform.thy
1.255 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.256 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.257 @@ -2008,7 +2015,7 @@
1.258 respective implementation: mechanisation of mathematics and domain
1.259 modelling, implementation of term rewriting systems for the
1.260 rewriting-engine, formal (implicit) specification of the problem to be
1.261 -(explicitly) described by the program, implement the many components
1.262 +(explicitly) described by the program, implementation of the many components
1.263 required for Lucas-Interpretation and finally implementation of the
1.264 program itself.
1.265
1.266 @@ -2041,7 +2048,7 @@
1.267 \item Extend the prototype's Lucas-Interpreter such that it also
1.268 handles functions defined by use of Isabelle's functions package; and
1.269 generalize Isabelle's code generator such that efficient code for the
1.270 -whole of the defined programming language can be generated (for
1.271 +whole definition of the programming language can be generated (for
1.272 multi-core machines).
1.273 \item Develop an efficient development environment with
1.274 integration of programming and proving, with management not only of
1.275 @@ -2052,15 +2059,15 @@
1.276 components for virtual workbenches appealing to practictioner of
1.277 engineering in the near future.
1.278
1.279 -\medskip And all programming with a TP-based language will
1.280 -subsequently create interactive tutoring as a side-effect:
1.281 -Lucas-Interpretation not only provides an interactive programming
1.282 -environment, Lucas-Interpretation also can provide TP-based services
1.283 -for a flexible dialog component with adaptive user guidance for
1.284 -independent and inquiry-based learning.
1.285 +\medskip Interactive couse material, as addressed by the title, then
1.286 +can comprise step-wise problem solving created as a side-effect of a
1.287 +TP-based program: Lucas-Interpretation not only provides an
1.288 +interactive programming environment, Lucas-Interpretation also can
1.289 +provide TP-based services for a flexible dialog component with
1.290 +adaptive user guidance for independent and inquiry-based learning.
1.291
1.292
1.293 \bibliographystyle{alpha}
1.294 -\bibliography{references}
1.295 +{\small\bibliography{references}}
1.296
1.297 \end{document}
1.298 \ No newline at end of file