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

equal deleted inserted replaced

-:988e6bd123c4
+:07dcff533c1d
 % on mathematics in \emph{STEOP}, the introductory orientation phase in
 % Austria. \emph{STEOP} is considered an opportunity to investigate the
 % impact of {\sisac}'s prototype on the issue and others.
 %
-\paragraph{Traditional course material} in engineering disciplines lacks an
+Traditional course material in engineering disciplines lacks an
 important component, interactive support for step-wise problem
 solving. Theorem-Proving (TP) technology can provide such support by
 specific services. An important part of such services is called
 ``next-step-guidance'', generated by a specific kind of ``TP-based
 programming language''. In the
 programming language, called
 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
 interpreter will be briefly re-introduced in order to make the paper
 self-contained.
-\subparagraph{The main part} of the paper is an account of first experiences
+\paragraph{The main part} of the paper is an account of first experiences
 with programming in this TP-based language. The experience was gained
 in a case study by the author. The author was considered an ideal
 candidate for this study for the following reasons: as a student in
 Telematics (computer science with focus on Signal Processing) he had
 general knowledge in programming as well as specific domain knowledge
 in Signal Processing; and he was not involved in the development of
 {\sisac}'s programming language and interpeter, thus a novice to the
 language.
-\subparagraph{The goal} of the case study was (1) some TP-based programs for
+\paragraph{The goal} of the case study was (1) some TP-based programs for
 interactive course material for a specific ``Adavanced Signal
 Processing Lab'' in a higher semester, (2) respective program
 development with as little advice from the {\sisac}-team and (3) records
 and comments for the main steps of development in an Isabelle theory;
 this theory should provide guidelines for future programmers. An
 \caption{Step-wise problem solving guided by the TP-based program}
 \label{fig-interactive}
 \end{center}
 \end{figure}
-\paragraph{The problem is} from the domain of Signal Processing and requests to
+The problem is from the domain of Signal Processing and requests to
 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
 also shows the beginning of the interactive construction of a solution
 for the problem. This construction is done in the right window named
 ``Worksheet''.
 \par
 The language for both axes is defined in the axis at the bottom, deductive
 knowledge, in {\sisac} represented by Isabelle's theories.
 \subsection{Preparation of Simplifiers for the Program}\label{simp}
-\paragraph{If it is clear} how the later calculation should look like and when
+If it is clear how the later calculation should look like and when
 which mathematic rule should be applied, it can be started to find ways of
 simplifications. This includes in e.g. the simplification of reational
 expressions or also rewrites of an expession.
-\subparagraph{Obligate is the use} of the function \texttt{drop\_questionmarks}
+\par
+Obligate is the use of the function \texttt{drop\_questionmarks}
 which excludes irrelevant symbols out of the expression. (Irrelevant symbols may
 be result out of the system during the calculation. The function has to be
 applied for two reasons. First two make every placeholder in a expression
 useable as a constant and second to provide a better view at the frontend.)
-\subparagraph{Most rewrites are represented} through rulesets this
+\par
+Most rewrites are represented through rulesets this
 rulesets tell the machine which terms have to be rewritten into which
 representation. In the upcoming programm a rewrite can be applied only in using
 such rulesets on existing terms.
 \paragraph{The core} of our implemented problem is the Z-Transformation
 (remember the description of the running example, introduced by
 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the
 transformation itself would require higher math which isn't yet avaible in our system we decided to choose the way like it is applied in labratory and problem classes at our university - by applying transformation rules (collected in
 transformation tables).
-\paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
+\par
-use of axiomatizations like shown in Example~\ref{eg:ruledef}. This rules can be
+Rules, in {\sisac{}}'s programming language can be designed by the use of
-collected in a ruleset (collection of rules) and applied to a given expression
+axiomatization. In this axiomatization we declare how a term has to look like
-as follows in the next example code.
+(left side) to be rewritten into another form (right side). Every line of this
+axiomatizations starts with the name of the rule.
 %\begin{example}
+{\footnotesize
 \label{eg:ruledef}
-\hfill\\
+%  \hfill\\
 \begin{verbatim}
 axiomatization where
 rule1: ``1 = $\delta$[n]'' and
 rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
-rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
+rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''\end{verbatim}
-\end{verbatim}
 %\end{example}
+}
+Rules can be summarized in a ruleset (collection of rules) and afterwards tried to be applied to a given expression as puttet over in following code.
 %\begin{example}
-\hfill\\
+%  \hfill\\
 \label{eg:ruleapp}
 \begin{enumerate}
 \item Store rules in ruleset:
-\begin{verbatim}
+{\footnotesize\begin{verbatim}
 val inverse_Z = append_rls "inverse_Z" e_rls
 [ Thm ("rule1",num_str @{thm rule1}),
 Thm ("rule2",num_str @{thm rule2}),
 Thm ("rule3",num_str @{thm rule3})
-];
+];\end{verbatim}}
-\end{verbatim}
 \item Define exression:
-\begin{verbatim}
+{\footnotesize\begin{verbatim}
-val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";
+val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}}
-\end{verbatim}
 \item Apply ruleset:
-\begin{verbatim}
+{\footnotesize\begin{verbatim}
 val SOME (sample_term', asm) =
-rewrite_set_ thy true inverse_Z sample_term;
+rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}}
-\end{verbatim}
 \end{enumerate}
 %\end{example}
 The use of rulesets makes it much easier to develop our designated applications,
 but the programmer has to be careful and patient. When applying rulesets
 two important issues have to be mentionend:
-\subparagraph{How often} the rules have to be applied? In case of
+\begin{enumerate}
+\item How often the rules have to be applied? In case of
 transformations it is quite clear that we use them once but other fields
 reuqire to apply rules until a special condition is reached (e.g.
 a simplification is finished when there is nothing to be done left).
-\subparagraph{The order} in which rules are applied often takes a big effect
+\item The order in which rules are applied often takes a big effect
 and has to be evaluated for each purpose once again.
-\par
+\end{enumerate}
-In our special case of Signal Processing and the rules defined in
+In the special case of Signal Processing the rules defined in the
-Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
+Example upwards have to be applied in a dedicated order to transform all
-constants. After this step has been done it no mather which rule fit's next.
+constants first of all. After this first transformation step has been done it no
+mather which rule fit's next.
 \subsection{Preparation of ML-Functions}\label{funs}
 The prototype's Lucas-Interpreter uses the {\sisac}-rewrite-engine for
 all kinds of evaluation. Some functionality required in programming,
 however, cannot be accomplished by rewriting. So the prototype has a
 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.
-{\small
+{\footnotesize
 \begin{verbatim}
 01 store_met
 02  (prep_met thy "SP_InverseZTransformation_classic" [] e_metID
 03  (["SignalProcessing", "Z_Transform", "Inverse"],
 04   [("#Given" ,["filterExpression (X_eq::bool)"]),
 range of powerful possibilities.
 \begin{description}
 \item[01..02] stores the method with the given name into the system under a global
 reference.
-\item[03] specifies the topic under which the method can be used.
+\item[03] specifies the topic within which context the method can be found.
-\item[04..05] as the requirements for different methods can deviant we
+\item[04..05] as the requirements for different methods can be deviant we
 declare what is \emph{given} and and what to \emph{find} for this specific method.
-\item[06] \emph{rewrite order} is the order of this rls, which one theorem of is
+The code again helds on the topic of the case studie, where the inverse
-used for rewriting one single step.
+z-transformation does a switch between a term describing a electrical filter into
-\item[07] \texttt{rls} is the currently used ruleset for this method,
+its step response. Also the datatype has to be declared (bool - due the fact that
-\texttt{e\_rls} specifies a
+we handle equations).
-ruleset where conditions can be used within it.
+\item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
-\item[08] we can add this method to a predefined tree of calculations ore leave
+theorem of it is used for rewriting one single step.
-it independend.
+\item[07] \texttt{rls} is the currently used ruleset for this method. This set
-\item[09] \texttt{srls}, can be used to evaluate list expressions in the source
+has already been defined before.
-\item[10] \texttt{prls} indicates predicates which can be used in model patterns.
+\item[08] we would have the possiblitiy to add this method to a predefined tree of
-\item[11] \texttt{crls}, gives us the possibility for checking formulas
+calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
-lementwise
+independend.
+\item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
+the source.
+\item[10] \emph{predicates ruleset} can be used to indicates predicates within
+model patterns.
+\item[11] The \emph{check ruleset} summarizes rules for checking formulas
+elementwise.
 \item[12] \emph{error patterns} which are expected in this kind of method can be
-specified.
+pre-specified to recognize them during the method.
-\item[13] \texttt{crls}, declares the canonical simplifier for the specific method
+\item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
-\item[14] for this time we don't specify the programm itself and keep it empty.
+of the specific method.
-Follow up \S\ref{progr} for informations on how to implement this \textit{main}
+\item[14] for this code snipset we don't specify the programm itself and keep it
-part.
+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
 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:
-{\small\it\label{s:impl}
+{\footnotesize\it\label{s:impl}
 \begin{tabbing}
 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
 \>{\rm 00}\>val program =\\
 \>{\rm 01}\>  "{\tt Program} InverseZTransform (X\_eq::bool) =   \\
 \>{\rm 02}\>\>  {\tt let}                                       \\

changeset 42502	07dcff533c1d
parent 42501	988e6bd123c4
child 42503	67921e3c60ff