1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Wed Oct 31 14:22:03 2012 +0100
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Fri Nov 02 12:20:49 2012 +0100
1.3 @@ -235,8 +235,59 @@
1.4 Isabelle theory; this theory should provide guidelines for future programmers.
1.5 An excerpt from this theory is the main part of this paper.
1.6 \par
1.7 -The paper will use the problem in Fig.\ref{fig-interactive} as a
1.8 -running example:
1.9 +
1.10 +\medskip The major example resulting from the case study will be used
1.11 +as running example throughout this paper. This example requires a
1.12 +program resembling the size of real-world applications in engineering;
1.13 +such a size was considered essential for the case study, since there
1.14 +are many small programs for a long time (mainly concerned with
1.15 +elementary Computer Algebra like simplification, equation solving,
1.16 +calculus, etc.~\footnote{The programs existing in the {\sisac}
1.17 +prototype are found at
1.18 +http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})
1.19 +
1.20 +\paragraph{The mathematical background of the running example} is the
1.21 +following: In Signal Processing, ``the ${\cal Z}$-Transform for
1.22 +discrete-time signals is the counterpart of the Laplace transform for
1.23 +continuous-time signals, and they each have a similar relationship to
1.24 +the corresponding Fourier transform. One motivation for introducing
1.25 +this generalization is that the Fourier transform does not converge
1.26 +for all sequences, and it is useful to have a generalization of the
1.27 +Fourier transform that encompasses a broader class of signals. A
1.28 +second advantage is that in analytic problems, the $z$-transform
1.29 +notation is often more convenient than the Fourier transform
1.30 +notation.'' ~\cite[p. 128]{oppenheim2010discrete}. The $z$-transform
1.31 +is defined as
1.32 +\begin{equation*}
1.33 +X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}
1.34 +\end{equation*}
1.35 +where a discrete time sequence $x[n]$ is transformed into the function
1.36 +$X(z)$ where $z$ is a continuous complex variable. The inverse
1.37 +function is addressed in the running example and can be determined by
1.38 +the integral
1.39 +\begin{equation*}
1.40 +x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz
1.41 +\end{equation*}
1.42 +where the letter $C$ represents a contour within the range of
1.43 +convergence of the $z$- transform. The unit circle can be a special
1.44 +case of this contour. Remember that $j$ is the complex number in the
1.45 +domain of engineering. As this transformation requires high effort to
1.46 +be solved, tables of commonly used transform pairs are used in
1.47 +education as well as in engineering practice; such tables can be found
1.48 +at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.
1.49 +A completely solved and more detailed example can be found at
1.50 +~\cite[p. 149f]{oppenheim2010discrete}.
1.51 +
1.52 +Following conventions in engineering education and in practice, the
1.53 +running example solves the problem by use of a table.
1.54 +
1.55 +\paragraph{Support for interactive stepwise problem solving} in the
1.56 +{\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,
1.57 +the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:
1.58 +A student inputs formulas line by line on the \textit{``Worksheet''},
1.59 +and each step (i.e. each formula on completion) is immediately checked
1.60 +by the system such that at most one inconsistent formula can reside on
1.61 +the Worksheet (on the input line, marked by the red $\otimes$).
1.62 \begin{figure} [htb]
1.63 \begin{center}
1.64 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
1.65 @@ -245,74 +296,56 @@
1.66 \label{fig-interactive}}
1.67 \end{center}
1.68 \end{figure}
1.69 +If the student gets stuck and does not know the formula to proceed with,
1.70 +there is the button \framebox{NEXT} proceeding to the next step. The
1.71 +button \framebox{AUTO} immediately delivers the final result in case
1.72 +the student is not interested in intermediate steps.
1.73
1.74 -\paragraph{The Engineering Background of the Problem} comes out of the domain
1.75 -Signal Processing, which takes a major part n the authors field of education.
1.76 -The given Problem requests to determine the inverse $z$-transform for a
1.77 -given term.
1.78 -\par
1.79 -``The $z$-Transform for discrete-time signals is the counterpart of the
1.80 -Laplace transform for continuous-time signals, and they each have a similar
1.81 -relationship to the corresponding Fourier transform. One motivation for
1.82 -introducing this generalization is that the Fourier transform does not
1.83 -converge for all sequences, and it is useful to have a generalization of the
1.84 -Fourier transform that encompasses a broader class of signals. A second
1.85 -advantage is that in analytic problems, the $z$-transform notation is often
1.86 -more convenient than the Fourier transform notation.''
1.87 -~\cite[p. 128]{oppenheim2010discrete}
1.88 -\par
1.89 -The $z$-transform can be defined as:
1.90 -\begin{equation}
1.91 -X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}
1.92 -\end{equation}
1.93 -Upper equation transforms a discrete time sequence $x[n]$ into the function
1.94 -$X(z)$ where $z$ is a continuous complex variable. The inverse function (as it
1.95 -is used in the given problem) is defined as:
1.96 -\begin{equation}
1.97 -x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz
1.98 -\end{equation}
1.99 -The letter $C$ represents a contour within the range of converge of the $z$-
1.100 -transform. The unit circle can be a special case of this contour. Remember
1.101 -that $j$ is the complex number in the field of engineering.
1.102 -As this transformation requires high effort to be solved, tables of
1.103 -common transform pairs are used in education as well as in (TODO: real); such
1.104 -tables can be found at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.
1.105 -A completely solved and more detailed example can be found at
1.106 -~\cite[p. 149f]{oppenheim2010discrete}. The upcoming implementation tries to
1.107 -fit this example in the way it is toughed at the authors university.
1.108 +Adaptive dialogue guidance is already under
1.109 +construction~\cite{gdaroczy-EP-13} and the two buttons will disappear,
1.110 +since their presence is not wanted in many learning scenarios (in
1.111 +particular, {\em not} in written exams).
1.112
1.113 +The buttons \framebox{Theories}, \framebox{Problems} and
1.114 +\framebox{Methods} are the entry points for interactive lookup of the
1.115 +underlying knowledge. For instance, pushing \framebox{Theories} in
1.116 +the configuration shown in Fig.\ref{fig-interactive}, pops up a
1.117 +``Theory browser'' displaying the theorem(s) justifying the current
1.118 +step. All browsers allow to lookup all other theories, thus
1.119 +supporting indepentend investigation of underlying definitions,
1.120 +theorems, proofs --- where the HTML representation of the browsers is
1.121 +ready for arbitrary multimedia add-ons.
1.122
1.123 +% can be explained by having a look at
1.124 +% Fig.\ref{fig-interactive} which shows the beginning of the interactive
1.125 +% construction of a solution for the problem. This construction is done in the
1.126 +% right window named ``Worksheet''.
1.127 +% \par
1.128 +% User-interaction on the Worksheet is {\em checked} and {\em guided} by
1.129 +% TP services:
1.130 +% \begin{enumerate}
1.131 +% \item Formulas input by the user are {\em checked} by TP: such a
1.132 +% formula establishes a proof situation --- the prover has to derive the
1.133 +% formula from the logical context. The context is built up from the
1.134 +% formal specification of the problem (here hidden from the user) by the
1.135 +% Lucas-Interpreter.
1.136 +% \item If the user gets stuck, the program developed below in this
1.137 +% paper ``knows the next step'' and Lucas-Interpretation provides services
1.138 +% featuring so-called ``next-step-guidance''; this is out of scope of this
1.139 +% paper and can be studied in~\cite{gdaroczy-EP-13}.
1.140 +% \end{enumerate} It should be noted that the programmer using the
1.141 +% TP-based language is not concerned with interaction at all; we will
1.142 +% see that the program contains neither input-statements nor
1.143 +% output-statements. Rather, interaction is handled by the interpreter
1.144 +% of the language.
1.145 +%
1.146 +% So there is a clear separation of concerns: Dialogues are adapted by
1.147 +% dialogue authors (in Java-based tools), using TP services provided by
1.148 +% Lucas-Interpretation. The latter acts on programs developed by
1.149 +% mathematics-authors (in Isabelle/ML); their task is concern of this
1.150 +% paper.
1.151
1.152 -\paragraph{The educational aspect} can be explained by having a look at
1.153 -Fig.\ref{fig-interactive} which shows the beginning of the interactive
1.154 -construction of a solution for the problem. This construction is done in the
1.155 -right window named ``Worksheet''.
1.156 -\par
1.157 -User-interaction on the Worksheet is {\em checked} and {\em guided} by
1.158 -TP services:
1.159 -\begin{enumerate}
1.160 -\item Formulas input by the user are {\em checked} by TP: such a
1.161 -formula establishes a proof situation --- the prover has to derive the
1.162 -formula from the logical context. The context is built up from the
1.163 -formal specification of the problem (here hidden from the user) by the
1.164 -Lucas-Interpreter.
1.165 -\item If the user gets stuck, the program developed below in this
1.166 -paper ``knows the next step'' and Lucas-Interpretation provides services
1.167 -featuring so-called ``next-step-guidance''; this is out of scope of this
1.168 -paper and can be studied in~\cite{gdaroczy-EP-13}.
1.169 -\end{enumerate} It should be noted that the programmer using the
1.170 -TP-based language is not concerned with interaction at all; we will
1.171 -see that the program contains neither input-statements nor
1.172 -output-statements. Rather, interaction is handled by the interpreter
1.173 -of the language.
1.174 -
1.175 -So there is a clear separation of concerns: Dialogues are adapted by
1.176 -dialogue authors (in Java-based tools), using TP services provided by
1.177 -Lucas-Interpretation. The latter acts on programs developed by
1.178 -mathematics-authors (in Isabelle/ML); their task is concern of this
1.179 -paper.
1.180 -
1.181 -The paper is structured as follows: The introduction
1.182 +\bigskip The paper is structured as follows: The introduction
1.183 \S\ref{intro} is followed by a brief re-introduction of the TP-based
1.184 programming language in \S\ref{PL}, which extends the executable
1.185 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
1.186 @@ -330,14 +363,13 @@
1.187 \section{\isac's Prototype for a Programming Language}\label{PL}
1.188 The prototype of the language and of the Lucas-Interpreter is briefly
1.189 described from the point of view of a programmer. The language extends
1.190 -the executable fragment in the language of the theorem prover
1.191 +the executable fragment of Higher-Order Logic (HOL) in the theorem prover
1.192 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
1.193
1.194 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
1.195 The executable fragment consists of data-type and function
1.196 definitions. It's usability even suggests that fragment for
1.197 -introductory courses \cite{nipkow-prog-prove}. HOL (Higher-Order Logic)
1.198 -is a typed logic whose type system resembles that of functional programming
1.199 +introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming
1.200 languages. Thus there are
1.201 \begin{description}
1.202 \item[base types,] in particular \textit{bool}, the type of truth
1.203 @@ -1456,7 +1488,7 @@
1.204
1.205 This function allows to stepwise check the program:
1.206
1.207 -{\footnotesize
1.208 +{\footnotesize\label{ml-check-program}
1.209 \begin{verbatim}
1.210 01 ML {*
1.211 02 val fmz =
1.212 @@ -1470,7 +1502,8 @@
1.213 10 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.214 11 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.215 12 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.216 -13 ...\end{verbatim}}
1.217 +13 ...
1.218 +\end{verbatim}}
1.219
1.220 \noindent Several dozens of calls for \texttt{me} are required to
1.221 create the lines in the calculation below (including the sub-problems
1.222 @@ -1909,7 +1942,7 @@
1.223
1.224 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
1.225
1.226 -\section{Conclusion}\label{conclusion}
1.227 +\section{Summary and Conclusions}\label{conclusion}
1.228
1.229 %JR obvious
1.230
1.231 @@ -1920,7 +1953,7 @@
1.232 language by example of the {\sisac}-prototype makes the paper
1.233 self-contained. The main section describes all the main concepts
1.234 involved in TP-based programming and all the sub-tasks concerning
1.235 -respective implementation: mechanisation of mathematics and domain
1.236 +respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain
1.237 modeling, implementation of term rewriting systems for the
1.238 rewriting-engine, formal (implicit) specification of the problem to be
1.239 (explicitly) described by the program, implementation of the many components
1.240 @@ -1938,13 +1971,14 @@
1.241 development environment is hardly usable: error messages still address
1.242 the developer of the prototype's interpreter rather than the
1.243 application programmer, implementation of the many settings for the
1.244 -Lucas-Interpreter is cumbersome.
1.245 +Lucas-Interpreter is cumbersome.
1.246
1.247 -From these experiences a successful proof of concept can be concluded:
1.248 +\subsection{Conclusions and Expectations to the Future}
1.249 +From the above mentioned experiences a successful proof of concept can be concluded:
1.250 programming arbitrary problems from engineering sciences is possible,
1.251 in principle even in the prototype. Furthermore the experiences allow
1.252 to conclude detailed requirements for further development:
1.253 -\begin{itemize}
1.254 +\begin{enumerate}
1.255 \item Clarify underlying logics such that programming is smoothly
1.256 integrated with verification of the program; the post-condition should
1.257 be proved more or less automatically, otherwise working engineers
1.258 @@ -1962,18 +1996,104 @@
1.259 integration of programming and proving, with management not only of
1.260 Isabelle theories, but also of large collections of specifications and
1.261 of programs.
1.262 -\end{itemize}
1.263 +\item\label{CAS} Extend Isabelle's computational features in direction of
1.264 +\textit{verfied} Computer Algebra: simplification extended by
1.265 +algorithms beyond rewriting (cancellation of multivariate rationals,
1.266 +factorisation, partial fraction decomposition, etc), equation solving
1.267 +, integration, etc.
1.268 +\end{enumerate}
1.269 Provided successful accomplishment, these points provide distinguished
1.270 -components for virtual workbenches appealing to practitioner of
1.271 +components for virtual workbenches appealing to practitioners of
1.272 engineering in the near future.
1.273
1.274 -\medskip Interactive course material, as addressed by the title, then
1.275 +\subsection{Preview to Development of Course Material}
1.276 +Interactive course material, as addressed by the title,
1.277 can comprise step-wise problem solving created as a side-effect of a
1.278 -TP-based program: Lucas-Interpretation not only provides an
1.279 +TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an
1.280 interactive programming environment, Lucas-Interpretation also can
1.281 provide TP-based services for a flexible dialogue component with
1.282 adaptive user guidance for independent and inquiry-based learning.
1.283
1.284 +However, the {\sisac} prototype is not ready for use in field-tests,
1.285 +not only due to the above five requirements not sufficiently
1.286 +accomplished, but also due to usability of the fron-end, in particular
1.287 +the lack of an editor for formulas in 2-dimension representation.
1.288 +
1.289 +Nevertheless, the experiences from the case study described in this
1.290 +paper, allow to give a preview to the development of course material,
1.291 +if based on Lucas-Interpretation:
1.292 +
1.293 +\paragraph{Development of material from scratch} is too much effort
1.294 +just for e-learning; this has become clear with the case study. For
1.295 +getting support for stepwise problem solving just in {\em one} example
1.296 +class, the one presented in this paper, involved the following tasks:
1.297 +\begin{itemize}
1.298 +\item Adapt the equation solver; since that was too laborous, the
1.299 +program has been adapted in an unelegant way.
1.300 +\item Implement an algorithms for partial fraction decomposition,
1.301 +which is considered a standard normal form in Computer Algebra.
1.302 +\item Implement a specification for partial fraction decomposition and
1.303 +locate it appropriately in the hierarchy of specification.
1.304 +\item Declare definitions and theorems within the theory of ${\cal
1.305 +Z}$-Transformation, and prove the theorems (which was not done in the
1.306 +case study).
1.307 +\end{itemize}
1.308 +On the other hand, for the one the class of problems implemented,
1.309 +adding an arbitrary number of examples within this class requires a
1.310 +few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an
1.311 +example is called from an HTML-file by an URL, which addresses an
1.312 +XML-structure holding the respective data as shown on
1.313 +p.\pageref{ml-check-program}.} and the support for individual stepwise
1.314 +problem solving comes for free.
1.315 +
1.316 +\paragraph{E-learning benefits from Formal Domain Engineering} which can be
1.317 +expected for various domains in the near future. In order to cope with
1.318 +increasing complexity in domain of technology, specific domain
1.319 +knowledge is beeing mechanised, not only for software technology
1.320 +\footnote{For instance, the Archive of Formal Proofs
1.321 +http://afp.sourceforge.net/} but also for other engineering domains
1.322 +\cite{Dehbonei&94,Hansen94b,db:dom-eng}. This fairly new part of
1.323 +engineering sciences is called ``domain engineering'' in
1.324 +\cite{db:SW-engIII}.
1.325 +
1.326 +Given this kind of mechanised knowledge including mathematical
1.327 +theories, domain specific definitions, specifications and algorithms,
1.328 +theorems and proofs, then e-learning with support for individual
1.329 +stepwise problem solving will not be much ado anymore; then e-learning
1.330 +media in technology education can be derived from this knowledge with
1.331 +reasonable effort.
1.332 +
1.333 +\paragraph{Development differentiates into tasks} more separated than
1.334 +without Lucas-Interpretation and more challenginging in specific
1.335 +expertise. These are the kinds of experts expected to cooperate in
1.336 +development of
1.337 +\begin{itemize}
1.338 +\item ``Domain engineers'', who accomplish fairly novel tasks described
1.339 +in this paper.
1.340 +\item Course designers, who provide the instructional design according
1.341 +to curricula, together with usability experts and media designers, are
1.342 +indispensable in production of e-learning media at the state-of-the
1.343 +art.
1.344 +\item ``Dialog designers'', whose part of development is clearly
1.345 +separated from the part of domain engineers as a consequence of Lucas-Interpretation: TP-based programs are functional, as mentioned, and are only concerned with describing mathematics --- and not at all interaction, psychology, learning theory and the like, because there are no in/output statements. Dialog designers can expect a high-level rule-based language~\cite{gdaroczy-EP-13} for describing their part.
1.346 +\end{itemize}
1.347 +
1.348 +% response-to-referees:
1.349 +% (2.1) details of novel technology in order to estimate the impact
1.350 +% (2.2) which kinds of expertise are required for production of e-learning media (instructional design, math authoring, dialog authoring, media design)
1.351 +% (2.3) what in particular is required for programming new exercises supported by next-step-guidance (expertise / efforts)
1.352 +% (2.4) estimation of break-even points for development of next-step-guidance
1.353 +% (2.5) usability of ISAC prototype at the present state
1.354 +%
1.355 +% The points (1.*) seem to be well covered in the paper, the points (2.*) are not. So I decided to address the points (2.*) in a separate section ยง5.1."".
1.356 +
1.357 +For this decade there seems to be a window of opportunity opening from
1.358 +one side inreasing demand for formal domain engineering and from the
1.359 +other side from TP more and more gaining industrial relevance. Within
1.360 +this window, development of TP-based educational software can take
1.361 +benefit from the fact, that the TPs leading in Europe, Coq and
1.362 +Isabelle are still open source together with the major part of
1.363 +mechanised knowledge.%~\footnote{NICTA}.
1.364
1.365 \bibliographystyle{alpha}
1.366 {\small\bibliography{references}}