1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 21:45:38 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Tue Sep 11 22:27:50 2012 +0200
1.3 @@ -206,7 +206,7 @@
1.4 % impact of {\sisac}'s prototype on the issue and others.
1.5 %
1.6
1.7 -\paragraph{Traditional course material} in engineering disciplines lacks an
1.8 +Traditional course material in engineering disciplines lacks an
1.9 important component, interactive support for step-wise problem
1.10 solving. Theorem-Proving (TP) technology can provide such support by
1.11 specific services. An important part of such services is called
1.12 @@ -222,7 +222,7 @@
1.13 interpreter will be briefly re-introduced in order to make the paper
1.14 self-contained.
1.15
1.16 -\subparagraph{The main part} of the paper is an account of first experiences
1.17 +\paragraph{The main part} of the paper is an account of first experiences
1.18 with programming in this TP-based language. The experience was gained
1.19 in a case study by the author. The author was considered an ideal
1.20 candidate for this study for the following reasons: as a student in
1.21 @@ -232,7 +232,7 @@
1.22 {\sisac}'s programming language and interpeter, thus a novice to the
1.23 language.
1.24
1.25 -\subparagraph{The goal} of the case study was (1) some TP-based programs for
1.26 +\paragraph{The goal} of the case study was (1) some TP-based programs for
1.27 interactive course material for a specific ``Adavanced Signal
1.28 Processing Lab'' in a higher semester, (2) respective program
1.29 development with as little advice from the {\sisac}-team and (3) records
1.30 @@ -251,7 +251,7 @@
1.31 \end{center}
1.32 \end{figure}
1.33
1.34 -\paragraph{The problem is} from the domain of Signal Processing and requests to
1.35 +The problem is from the domain of Signal Processing and requests to
1.36 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}
1.37 also shows the beginning of the interactive construction of a solution
1.38 for the problem. This construction is done in the right window named
1.39 @@ -705,16 +705,18 @@
1.40
1.41 \subsection{Preparation of Simplifiers for the Program}\label{simp}
1.42
1.43 -\paragraph{If it is clear} how the later calculation should look like and when
1.44 +If it is clear how the later calculation should look like and when
1.45 which mathematic rule should be applied, it can be started to find ways of
1.46 simplifications. This includes in e.g. the simplification of reational
1.47 expressions or also rewrites of an expession.
1.48 -\subparagraph{Obligate is the use} of the function \texttt{drop\_questionmarks}
1.49 +\par
1.50 +Obligate is the use of the function \texttt{drop\_questionmarks}
1.51 which excludes irrelevant symbols out of the expression. (Irrelevant symbols may
1.52 be result out of the system during the calculation. The function has to be
1.53 applied for two reasons. First two make every placeholder in a expression
1.54 useable as a constant and second to provide a better view at the frontend.)
1.55 -\subparagraph{Most rewrites are represented} through rulesets this
1.56 +\par
1.57 +Most rewrites are represented through rulesets this
1.58 rulesets tell the machine which terms have to be rewritten into which
1.59 representation. In the upcoming programm a rewrite can be applied only in using
1.60 such rulesets on existing terms.
1.61 @@ -723,59 +725,66 @@
1.62 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the
1.63 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
1.64 transformation tables).
1.65 -\paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
1.66 -use of axiomatizations like shown in Example~\ref{eg:ruledef}. This rules can be
1.67 -collected in a ruleset (collection of rules) and applied to a given expression
1.68 -as follows in the next example code.
1.69 +\par
1.70 +Rules, in {\sisac{}}'s programming language can be designed by the use of
1.71 +axiomatization. In this axiomatization we declare how a term has to look like
1.72 +(left side) to be rewritten into another form (right side). Every line of this
1.73 +axiomatizations starts with the name of the rule.
1.74
1.75 %\begin{example}
1.76 +{\footnotesize
1.77 \label{eg:ruledef}
1.78 - \hfill\\
1.79 +% \hfill\\
1.80 \begin{verbatim}
1.81 axiomatization where
1.82 rule1: ``1 = $\delta$[n]'' and
1.83 rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1.84 - rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1.85 - \end{verbatim}
1.86 + rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''\end{verbatim}
1.87 %\end{example}
1.88 +}
1.89 +
1.90 +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.
1.91
1.92 %\begin{example}
1.93 - \hfill\\
1.94 +% \hfill\\
1.95 \label{eg:ruleapp}
1.96 \begin{enumerate}
1.97 +
1.98 \item Store rules in ruleset:
1.99 - \begin{verbatim}
1.100 + {\footnotesize\begin{verbatim}
1.101 val inverse_Z = append_rls "inverse_Z" e_rls
1.102 [ Thm ("rule1",num_str @{thm rule1}),
1.103 Thm ("rule2",num_str @{thm rule2}),
1.104 Thm ("rule3",num_str @{thm rule3})
1.105 - ];
1.106 - \end{verbatim}
1.107 + ];\end{verbatim}}
1.108 +
1.109 \item Define exression:
1.110 - \begin{verbatim}
1.111 - val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";
1.112 - \end{verbatim}
1.113 + {\footnotesize\begin{verbatim}
1.114 + val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}}
1.115 +
1.116 \item Apply ruleset:
1.117 - \begin{verbatim}
1.118 + {\footnotesize\begin{verbatim}
1.119 val SOME (sample_term', asm) =
1.120 - rewrite_set_ thy true inverse_Z sample_term;
1.121 - \end{verbatim}
1.122 + rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}}
1.123 +
1.124 \end{enumerate}
1.125 %\end{example}
1.126
1.127 The use of rulesets makes it much easier to develop our designated applications,
1.128 but the programmer has to be careful and patient. When applying rulesets
1.129 two important issues have to be mentionend:
1.130 -\subparagraph{How often} the rules have to be applied? In case of
1.131 +\begin{enumerate}
1.132 +\item How often the rules have to be applied? In case of
1.133 transformations it is quite clear that we use them once but other fields
1.134 reuqire to apply rules until a special condition is reached (e.g.
1.135 a simplification is finished when there is nothing to be done left).
1.136 -\subparagraph{The order} in which rules are applied often takes a big effect
1.137 +\item The order in which rules are applied often takes a big effect
1.138 and has to be evaluated for each purpose once again.
1.139 -\par
1.140 -In our special case of Signal Processing and the rules defined in
1.141 -Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
1.142 -constants. After this step has been done it no mather which rule fit's next.
1.143 +\end{enumerate}
1.144 +In the special case of Signal Processing the rules defined in the
1.145 +Example upwards have to be applied in a dedicated order to transform all
1.146 +constants first of all. After this first transformation step has been done it no
1.147 +mather which rule fit's next.
1.148
1.149 \subsection{Preparation of ML-Functions}\label{funs}
1.150 The prototype's Lucas-Interpreter uses the {\sisac}-rewrite-engine for
1.151 @@ -1104,7 +1113,7 @@
1.152 calculation in deep, as well we get the oppertunities to build in different
1.153 rulesets.
1.154
1.155 -{\small
1.156 +{\footnotesize
1.157 \begin{verbatim}
1.158 01 store_met
1.159 02 (prep_met thy "SP_InverseZTransformation_classic" [] e_metID
1.160 @@ -1131,26 +1140,33 @@
1.161 \begin{description}
1.162 \item[01..02] stores the method with the given name into the system under a global
1.163 reference.
1.164 -\item[03] specifies the topic under which the method can be used.
1.165 -\item[04..05] as the requirements for different methods can deviant we
1.166 +\item[03] specifies the topic within which context the method can be found.
1.167 +\item[04..05] as the requirements for different methods can be deviant we
1.168 declare what is \emph{given} and and what to \emph{find} for this specific method.
1.169 -\item[06] \emph{rewrite order} is the order of this rls, which one theorem of is
1.170 -used for rewriting one single step.
1.171 -\item[07] \texttt{rls} is the currently used ruleset for this method,
1.172 -\texttt{e\_rls} specifies a
1.173 -ruleset where conditions can be used within it.
1.174 -\item[08] we can add this method to a predefined tree of calculations ore leave
1.175 -it independend.
1.176 -\item[09] \texttt{srls}, can be used to evaluate list expressions in the source
1.177 -\item[10] \texttt{prls} indicates predicates which can be used in model patterns.
1.178 -\item[11] \texttt{crls}, gives us the possibility for checking formulas
1.179 -lementwise
1.180 +The code again helds on the topic of the case studie, where the inverse
1.181 +z-transformation does a switch between a term describing a electrical filter into
1.182 +its step response. Also the datatype has to be declared (bool - due the fact that
1.183 +we handle equations).
1.184 +\item[06] \emph{rewrite order} is the order of this rls (ruleset), where one
1.185 +theorem of it is used for rewriting one single step.
1.186 +\item[07] \texttt{rls} is the currently used ruleset for this method. This set
1.187 +has already been defined before.
1.188 +\item[08] we would have the possiblitiy to add this method to a predefined tree of
1.189 +calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
1.190 +independend.
1.191 +\item[09] The \emph{source ruleset}, can be used to evaluate list expressions in
1.192 +the source.
1.193 +\item[10] \emph{predicates ruleset} can be used to indicates predicates within
1.194 +model patterns.
1.195 +\item[11] The \emph{check ruleset} summarizes rules for checking formulas
1.196 +elementwise.
1.197 \item[12] \emph{error patterns} which are expected in this kind of method can be
1.198 -specified.
1.199 -\item[13] \texttt{crls}, declares the canonical simplifier for the specific method
1.200 -\item[14] for this time we don't specify the programm itself and keep it empty.
1.201 -Follow up \S\ref{progr} for informations on how to implement this \textit{main}
1.202 -part.
1.203 +pre-specified to recognize them during the method.
1.204 +\item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier
1.205 +of the specific method.
1.206 +\item[14] for this code snipset we don't specify the programm itself and keep it
1.207 +empty. Follow up \S\ref{progr} for informations on how to implement this
1.208 +\textit{main} part.
1.209 \end{description}
1.210
1.211 \subsection{Implementation of the TP-based Program}\label{progr}
1.212 @@ -1159,7 +1175,8 @@
1.213 computes a solution for the problem from Fig.\ref{fig-interactive} on
1.214 p.\pageref{fig-interactive}. The reader is reminded of
1.215 \S\ref{PL-isab}, the introduction of the programming language:
1.216 -{\small\it\label{s:impl}
1.217 +
1.218 +{\footnotesize\it\label{s:impl}
1.219 \begin{tabbing}
1.220 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.221 \>{\rm 00}\>val program =\\