wneuper/isa: comparison doc-src/isac/jrocnik/eJMT-paper/jrocnik

equal deleted inserted replaced

-:480aee713e3d
+:629324e62a24
 the latter, uses a novel kind of programming language. This language
 is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
 programming language''.
 This paper is the experience report of the first ``application
-programmer'' using this language, the experience gained from a
+programmer'' using this language for creating exercises in step-wise
-prototype of the programming language and of it's interpreter.
+problem solving for an advanced lab in Signal Processing. The tasks
+involved in TP-based programming are described together with the
+experience gained from a prototype of the programming language and of
+it's interpreter.
 The report concludes with a positive proof of concept, states
 insuggicient usability of the prototype and captures the requirements
 for further development of both, the programming language and the
 interpreter.
 % knowledge, in {\sisac} represented by Isabelle's theories.
 \subsection{Preparation of Simplifiers for the Program}\label{simp}
 All evaluation in the prototyp's Lucas-Interpreter is done by term rewriting on
-Isabelle's terms, see \S\ref{math} below; in this section some of respective
+Isabelle's terms, see \S\ref{meth} below; in this section some of respective
 preparations are described. In order to work reliably with term rewriting, the
 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
 then they are called (canonical) simplifiers. These properties do not go without
 saying, their establishment is a difficult task for the programmer; this task is
 not yet supported in the prototype.\par
 {\footnotesize
 \begin{verbatim}
 consts
 argument'_in :: "real => real" ("argument'_in _" 10)
+\end{verbatim}}
-ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
+%^3.2^    ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
-val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
+%^3.2^    val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real")
-$ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
+%^3.2^              $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
-\end{verbatim}}
+%^3.2^ \end{verbatim}}
+%^3.2^
-\noindent Parsing produces a term \texttt{t} in internal
+%^3.2^ \noindent Parsing produces a term \texttt{t} in internal
-representation~\footnote{The attentive reader realizes the
+%^3.2^ representation~\footnote{The attentive reader realizes the
-differences between interal and extermal representation even in the
+%^3.2^ differences between interal and extermal representation even in the
-strings, i.e \texttt{'\_}}, consisting of \texttt{Const
+%^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
-("argument'\_in", type)} and the two variables \texttt{Free ("X",
+%^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
-type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
+%^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
-constructor. The function body below is implemented directly in SML,
+%^3.2^ constructor.
+The function body below is implemented directly in SML,
 i.e in an \texttt{ML \{* *\}} block; the function definition provides
 a unique prefix \texttt{eval\_} to the function name:
 {\footnotesize
 \begin{verbatim}
 \label{eg:neuper2}
 {\small\begin{tabbing}
 123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
 %\hfill \\
 \>Specification:\\
-\>  \>input    \>: ${\it filterExpression} \;\;X\;z=\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
+\>  \>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}\}$\\
 \>\>precond  \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
 \>\>output   \>: stepResponse $x[n]$ \\
 \>\>postcond \>: TODO
 \end{tabbing}}
 02    (prepare_specification
 03      "pbl_SP_Ztrans_inv"
 04      ["Jan Rocnik"]
 05      thy
 06      ( ["Inverse", "Z_Transform", "SignalProcessing"],
-07        [ ("#Given", ["filterExpression X_eq"]),
+07        [ ("#Given", ["filterExpression X_eq", "domain D"]),
-08          ("#Pre"  , ["(rhs X_eq) is_continuous_in R\{1/2, -1/4}"]),
+08          ("#Pre"  , ["(rhs X_eq) is_continuous_in D"]),
 09          ("#Find" , ["stepResponse n_eq"]),
-10          ("#Post" , [" TODO "])],
+10          ("#Post" , [" TODO "])])
-11        append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)],
+11        prls
-12        NONE,
+12        NONE
-13        [["SignalProcessing","Z_Transform","Inverse"]]));
+13        [["SignalProcessing","Z_Transform","Inverse"]]);
 14 *}
 \end{verbatim}}
 Although the above details are partly very technical, we explain them
 in order to document some intricacies of TP-based programming in the
 specification in lines {\rm 07..10}.
 \item[06] is a key into the tree of all specifications as presented to
 the user (where some branches might be hidden by the dialog
 component).
 \item[07..10] are the specification with input, pre-condition, output
-and post-condition respectively; the post-condition is not handled in
+and post-condition respectively; note that the specification contains
+variables to be instantiated with concrete values for a concrete problem ---
+thus the specification actually captures a class of problems. The post-condition is not handled in
 the prototype presently.
-\item[11] creates a rule-set (abbreviated \textit{rls} in
+\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
-{\sisac}) which evaluates the pre-condition for the actual input data.
+rewriting determined by rule-sets.
-Only if the evaluation yields \textit{True}, a program can be started.
 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
 problem associated to a function from Computer Algebra (like an
 equation solver) which is not the case here.
 \item[13] is a list of methods solving the specified problem (here
 only one list item) represented analogously to {\rm 06}.
 % }
 \subsection{Implementation of the Method}\label{meth}
 A method collects all data required to interpret a certain program by
 Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
-the running example is embedded in the following method:
+the running example is embedded on the last line in the following method:
 %The methods represent the different ways a problem can be solved. This can
 %include mathematical tactics as well as tactics taught in different courses.
 %Declaring the Method itself gives us the possibilities to describe the way of
 %calculation in deep, as well we get the oppertunities to build in different
 %rulesets.
 01  store_method
 02    (prep_method
 03      "SP_InverseZTransformation_classic"
 04      ["Jan Rocnik"]
 05      thy
-06      (["SignalProcessing", "Z_Transform", "Inverse"],
+06      ( ["SignalProcessing", "Z_Transform", "Inverse"],
-07       [("#Given" ,["filterExpression (X_eq::bool)"]),
+07        [ ("#Given", ["filterExpression X_eq", "domain D"]),
-08        ("#Pre"  , ["(rhs X_eq) is_continuous_in R\{1/2, -1/4}"]),
+08          ("#Pre"  , ["(rhs X_eq) is_continuous_in D"]),
-09        ("#Find"  ,["stepResponse (n_eq::bool)"])],
+09          ("#Find" , ["stepResponse n_eq"]),
-10       {rew_ord = tless_true, rls  = rls,
+10        rew_ord  erls
-11        srls = srls, calc = [],
+11        srls  prls  nrls
-12        prls = prls, crls = crls,
+12        errpats
-13        nrls = nrls,
+13        program);
-14        errpats = []},
+14 *}
-15        program));
-16 *}
 \end{verbatim}}
 \noindent The above code stores the whole structure analogously to a
-specification,
+specification as described above:
 \begin{description}
 \item[01..06] are identical to those for the example specification on
 p.\pageref{exp-spec}.
 \item[07..09] show something looking like the specification; this is a
-{\em guard}: as long as not all \texttt{Given} items are present and
+{\em guard}: as long as not all \textit{Given} items are present and
-the \texttt{Pre}-conditions is not true, interpretation of the program
+the \textit{Pre}-conditions is not true, interpretation of the program
 is not started.
-\item[01..09]
+\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
+\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
-\item[01..09]
+\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
+\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}
-\item[01..09]
+and (c) is required for the derivation-machinery checking user-input formulas.
-\item[01..09]
+\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}.
 \end{description}
+The many rule-sets above cause considerable efforts for the
+programmers, in particular, because there are no tools for checking
-.\\.\\.\\
+essential features of rule-sets.
 % is again very technical and goes hard in detail. Unfortunataly
 % most declerations are not essential for a basic programm but leads us to a huge
 % range of powerful possibilities.
 %
 % empty. Follow up \S\ref{progr} for informations on how to implement this
 % \textit{main} part.
 % \end{description}
 \subsection{Implementation of the TP-based Program}\label{progr}
-So finally all the prerequisites are described and the very topic can
+So finally all the prerequisites are described and the final task can
 be addressed. The program below comes back to the running example: it
 computes a solution for the problem from Fig.\ref{fig-interactive} on
 p.\pageref{fig-interactive}. The reader is reminded of
 \S\ref{PL-isab}, the introduction of the programming language:
 {\footnotesize\it\label{s:impl}
 \begin{tabbing}
 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
-\>        \>ML \{*
+\>{\rm 00}\>ML \{*\\
 \>{\rm 00}\>val program =\\
 \>{\rm 01}\>  "{\tt Program} InverseZTransform (X\_eq::bool) =   \\
 \>{\rm 02}\>\>  {\tt let}                                       \\
 \>{\rm 03}\>\>\>  X\_eq = {\tt Take} X\_eq ;   \\
-\>{\rm 04}\>\>\>  X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
+\>{\rm 04}\>\>\>  X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
 \>{\rm 05}\>\>\>  (X\_z::real) = lhs X\_eq ;       \\ %no inside-out evaluation
 \>{\rm 06}\>\>\>  (z::real) = argument\_in X\_z; \\
 \>{\rm 07}\>\>\>  (part\_frac::real) = {\tt SubProblem} \\
 \>{\rm 08}\>\>\>\>\>\>\>\>  ( Isac, [partial\_fraction, rational, simplification], [] )\\
 %\>{\rm 10}\>\>\>\>\>\>\>\>\>  [simplification, of\_rationals, to\_partial\_fraction] ) \\
 \>{\rm 09}\>\>\>\>\>\>\>\>  [ (rhs X\_eq)::real, z::real ]; \\
 \>{\rm 10}\>\>\>  (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
-\>{\rm 11}\>\>\>  X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@   \\
+\>{\rm 11}\>\>\>  X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@   \\
 \>{\rm 12}\>\>\>\>\>  $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
 \>{\rm 13}\>\>  {\tt in } \\
 \>{\rm 14}\>\>\>  X'\_eq"\\
-\>        \>*\}
+\>{\rm 15}\>*\}
 \end{tabbing}}
 % ORIGINAL FROM Inverse_Z_Transform.thy
 % "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
 % "(let X = Take X_eq;                                "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
 % "  X' = Rewrite ruleZY False X;                     "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
 the steps of calculation towards a solution (and interactive tutoring
 in step-wise problem solving) are created as a side-effect by
 Lucas-Interpretation.  The side-effects are triggered by the tactics
 \texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
 \texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
-{\rm 12} respectively. These tactics produce the lines in the
+{\rm 12} respectively. These tactics produce the respective lines in the
 calculation on p.\pageref{flow-impl}.
 The above lines {\rm 05, 06} do not contain a tactics, so they do not
 immediately contribute to the calculation on p.\pageref{flow-impl};
 rather, they compute actual arguments for the \texttt{SubProblem} in
 kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
 particular the environment and the context at the states position ---
 all checks have to rely on simple functions accessing the
 \texttt{ctree}. So getting the calculation below (which resembles the
 calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
-finished successfully is a relief:
+is the result of several weeks of development:
 {\small\it\label{exp-calc}
 \begin{tabbing}
 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
 \>{\rm 01}\> $\bullet$  \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing])       \`\\
 \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$       \`{\footnotesize {\tt Take} X\_eq}\\
-\>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$          \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\
+\>{\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}\\
 \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification]        \`{\footnotesize {\tt SubProblem} \dots}\\
 \>{\rm 05}\>\>\>  $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$    \`- - -\\
 \>{\rm 06}\>\>\>  $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$                                   \`- - -\\
 \>{\rm 07}\>\>\>  $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ )                      \`- - -\\
 \>{\rm 08}\>\>\>\>   $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
 \>{\rm 09}\>\>\>\>   $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$           \`- - -\\
 \>{\rm 10}\>\>\>\>   $z = \frac{1}{2}\;\lor\;z =$ \_\_\_                                           \`- - -\\
 \>        \>\>\>\>   \_\_\_                                                                        \`- - -\\
 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$                   \`\\
 \>{\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)}\\
-\>{\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 }\\
+\>{\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 }\\
 \>{\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}\\
 \>{\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}}
 \end{tabbing}}
+The tactics on the right margin of the above calculation are those in
+the program on p.\pageref{s:impl} which create the respective formulas
+on the left.
 % ORIGINAL FROM Inverse_Z_Transform.thy
 %    "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
 %    "(let X = Take X_eq;                                "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
 %    "  X' = Rewrite ruleZY False X;                     "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
 %    "  (X'_z::real) = lhs X';                           "^(*            ?X' z*)
 self-contained. The main section describes all the main concepts
 involved in TP-based programming and all the sub-tasks concerning
 respective implementation: mechanisation of mathematics and domain
 modelling, implementation of term rewriting systems for the
 rewriting-engine, formal (implicit) specification of the problem to be
-(explicitly) described by the program, implement the many components
+(explicitly) described by the program, implementation of the many components
 required for Lucas-Interpretation and finally implementation of the
 program itself.
 The many concepts and sub-tasks involved in programming require a
 comprehensive workflow; first experiences with the workflow as
 pattern-matching features; include parallel execution on multi-core
 machines into the language desing.
 \item Extend the prototype's Lucas-Interpreter such that it also
 handles functions defined by use of Isabelle's functions package; and
 generalize Isabelle's code generator such that efficient code for the
-whole of the defined programming language can be generated (for
+whole definition of the programming language can be generated (for
 multi-core machines).
 \item Develop an efficient development environment with
 integration of programming and proving, with management not only of
 Isabelle theories, but also of large collections of specifications and
 of programs.
 \end{itemize}
 Provided successful accomplishment, these points provide distinguished
 components for virtual workbenches appealing to practictioner of
 engineering in the near future.
-\medskip And all programming with a TP-based language will
+\medskip Interactive couse material, as addressed by the title, then
-subsequently create interactive tutoring as a side-effect:
+can comprise step-wise problem solving created as a side-effect of a
-Lucas-Interpretation not only provides an interactive programming
+TP-based program: Lucas-Interpretation not only provides an
-environment, Lucas-Interpretation also can provide TP-based services
+interactive programming environment, Lucas-Interpretation also can
-for a flexible dialog component with adaptive user guidance for
+provide TP-based services for a flexible dialog component with
-independent and inquiry-based learning.
+adaptive user guidance for independent and inquiry-based learning.
 \bibliographystyle{alpha}
-\bibliography{references}
+{\small\bibliography{references}}
 \end{document}

changeset 42507	629324e62a24
parent 42506	480aee713e3d
child 42508	373a9b713684
child 42509	89ce7be69cfa