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

equal deleted inserted replaced

-:5f8f02e1ea9f
+:264803a0c13e
 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
 The problem of the running example is textually described in
 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em
 formal} specification of this problem, in traditional mathematical
-notation, could look lik is this:
+notation, could look like is this:
 %WN Hier brauchen wir die Spezifikation des 'running example' ...
 %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
 %JR der post condition - die existiert für uns ja eigentlich nicht aka
 \hfill \\
 Specification:\\
 \>input    \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\
 \>precond  \>: filterExpression continius on $\mathbb{R}$ \\
 \>output   \>: stepResponse $x[n]$ \\
-\>postcond \>:{\small  $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\
+\>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}
-\>     \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land
-(\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\
+\paragraph{Remark on post-conditions:} Defining the postcondition requires a
-\end{tabbing}
+high amount mathematical knowledge, the difficult part in our case is not to
-}
+set up this condition nor it is more to define it in a way the interpreter is
+able to handle it. Due the fact that implementing that mechanisms is quite
-And this is the implementation of the formal specification in the present
+the same amount as creating the programm itself, it is not avaible in our
+prototype.\label{rm:postcond}
+\paragraph{The implementation} of the formal specification in the present
 prototype, still bar-bones without support for authoring:
 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
 {\footnotesize
 \begin{verbatim}
 01  store_specification
 \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
-the prototype presently.
+the prototype presently. (Follow up Remark in Section~\ref{rm:postcond})
 \item[11] creates a term rewriting system (abbreviated \textit{rls} in
 {\sisac}) which evaluates the pre-condition for the actual input data.
 Only if the evaluation yields \textit{True}, a program con be started.
 \item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
 problem associated to a function from Computer Algebra (like an
 \subsection{Implementation of the Method}\label{meth}
 %WN <--> \chapter 7 der Thesis
 TODO
 \subsection{Preparation of Simplifiers for the Program}\label{simp}
-TODO
+%JR: ich denke wir können diesen punkt weglassen, methoden wie
+%JR: drop_questionmarks und ähnliche sind im arical nicht ersichtlich und im
+%JR: grunde nicht relevant (ihre erstellung gleich wie functionen im nächsten
+%JR: Punkt)
 \subsection{Preparation of ML-Functions}\label{funs}
-%WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr}
-%WN brauchst
+\paragraph{Explicit Problems} require explicit methods to solve them, and within
-TODO
+this methods we have some explicit steps to do. This steps can be unique for
+a special problem or refindable in other problems. No mather what case, such
+steps often require some technical functions behind. For the solving process
+of the Inverse Z Transformation and the corresponding partial fraction it was
+neccessary to build helping functions like \texttt{get\_denominator},
+\texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
+to filter the deonimonator or numerator out of a fraction, last one helps us to
+get to know the bound variable in a equation.
+\par
+By taking \texttt{get\_denominator} we want to explain how to implement new
+functions into the existing system and how we can later use them in our program.
+\subsubsection{Find a place to Store the Function}
+The whole system builds up on a well defined structure of Knowledge. This
+Knowledge sets up at\ttfamily src/Tools/isac/Knowledge\normalfont. For the
+implementation of the Function \texttt{get\_denominator}, which let us now
+the denominator of a fraction we have choosen the Theory (file)
+\texttt{Rational.thy}.
+\subsubsection{Write down the new Function}
+\begin{example}
+\begin{verbatim}
+ML {*
+(*
+*("get_denominator",
+*  ("Rational.get_denominator", eval_get_denominator ""))
+*)
+fun eval_get_denominator (thmid:string) _
+(t as Const ("Rational.get_denominator", _) $
+(Const ("Rings.inverse_class.divide", _) $num
+$denom)) thy =
+SOME (mk_thmid thmid ""
+(Print_Mode.setmp []
+(Syntax.string_of_term (thy2ctxt thy)) denom) "",
+Trueprop $ (mk_equality (t, denom)))
+| eval_get_denominator _ _ _ _ = NONE;
+*}\end{verbatim}
+\end{example}
+\subsubsection{Add a test for the new Function}
+\subsubsection{Use the new Function}
 \subsection{Implementation of the TP-based Program}\label{progr}
 %WN <--> \chapter 8 der Thesis
 .\\.\\.\\
 {\small\it\begin{tabbing}
 .\\.\\.\\
 \section{Workflow of Programming in the Prototype}\label{workflow}
-\cite{makar-jedit-12}
 \subsection{Preparations and Trials}\label{flow-prep}
 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''
 .\\.\\.\\
+%JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich
+%JR: eingefügt; das war der beinn unserer Arbeit in
+%JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei
+%JR: jedem neuen Programm nötigen Schritte.
 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
-TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
-.\\.\\.\\
+\paragraph{At the beginning} of the implementation it is good to decide on one
+way the problem should be solved. We also did this for our Z-Transformation
-below: calculation on the left; on the right are the tactics in the
+Problem and have choosen the way it is also thaugt in the Signal Processing
-program which created the respective formula on the left.
+Problem classes.
+\subparagraph{By writing down} each of this neccesarry steps we are describing
+one line of our upcoming program. In the following example we show the
+Calculation on the left and on the right the tactics in the program which
+created the respective formula on the left.
+\begin{example}
+\hfill\\
 {\small\it
 \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 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 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}}
+\end{example}
 % 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*)
 In our special case of Signal Processing and the rules defined in
 Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
 constants. After this step has been done it no mather which rule fit's next.
 \subsubsection{Helping Functions}
-%get denom, argument in
+\paragraph{New Programms require,} often new ways to get through. This new ways
+means that we handle functions that have not been in use yet, they can be
+something special and unique for a programm or something famous but unneeded in
+the system yet. In our dedicated example it was for example neccessary to split
+a fraction into numerator and denominator; the creation of such function and
+even others is described in upper Sections~\ref{simp} and \ref{funs}.
 \subsubsection{Trials on equation solving}
 %simple eq and problem with double fractions/negative exponents
+\paragraph{The Inverse Z-Transformation} makes it neccessary to solve
+equations degree one and two. Solving equations in the first degree is no
+problem, wether for a student nor for our machine; but even second degree
+equations can lead to big troubles. The origin of this troubles leads from
+the build up process of our equation solving functions; they have been
+implemented some time ago and of course they are not as good as we want them to
+be. Wether or not following we only want to show how cruel it is to build up new
+work on not well fundamentials.
+\subparagraph{A simple equation solving,} can be set up as shown in the next
+example:
+\begin{example}
+\begin{verbatim}
+val fmz =
+["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
+"solveFor z",
+"solutions L"];
+val (dI',pI',mI') =
+("Isac",
+["abcFormula","degree_2","polynomial","univariate","equation"],
+["no_met"]);\end{verbatim}
+\end{example}
+Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
+a short overview on the commands; at first we set up the equation and tell the
+machine what's the bound variable and where to store the solution. Second step
+is to define the equation type and determine if we want to use a special method
+to solve this type.) Simple checks tell us that the we will get two results for
+this equation and this results will be real.
+So far it is easy for us and for our machine to solve, but
+mentioned that a unvariate equation second order can have three different types
+of solutions it is getting worth.
+\subparagraph{The solving of} all this types of solutions is not yet supported.
+Luckily it was needed for us; but something which has been needed in this
+context, would have been the solving of an euation looking like:
+$-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
+before (remember that befor it was no problem to handle for the machine) but
+now, after a simple equivalent transformation, we are not able to solve
+it anymore.
+\subparagraph{Error messages} we get when we try to solve something like upside
+were very confusing and also leads us to no special hint about a problem.
+\par The fault behind is, that we have no well error handling on one side and
+no sufficient formed equation solving on the other side. This two facts are
+making the implemention of new material very difficult.
 \subsection{Formalization of missing knowledge in Isabelle}
 \paragraph{A problem} behind is the mechanization of mathematic
 theories in TP-bases languages. There is still a huge gap between

changeset 42469	264803a0c13e
parent 42468	5f8f02e1ea9f
child 42470	aafbbd5a85a5