1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 17:39:07 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 21:20:05 2012 +0200
1.3 @@ -671,36 +671,37 @@
1.4 reasonably short and easily comprehensible, still requires lots of
1.5 work (and is definitely out of scope of our case study).
1.6
1.7 -At the state-of-the-art in mechanization of knowledge in engineering
1.8 -sciences, the process does not stop with the mechanization of
1.9 -mathematics traditionally used in these sciences. Rather, ``Formal
1.10 -Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
1.11 -description of physical items. Signal Processing, for instance is
1.12 -concerned with physical devices for signal acquisition and
1.13 -reconstruction, which involve measuring a physical signal, storing it,
1.14 -and possibly later rebuilding the original signal or an approximation
1.15 -thereof. For digital systems, this typically includes sampling and
1.16 -quantization; devices for signal compression, including audio
1.17 -compression, image compression, and video compression, etc. ``Domain
1.18 -engineering''\cite{db:dom-eng} is concerned with {\em specification}
1.19 -of these devices' components and features; this part in the process of
1.20 -mechanization is only at the beginning in domains like Signal
1.21 -Processing.
1.22 -
1.23 -TP-based programming, concern of this paper, is determined to
1.24 -add ``algorithmic knowledge'' to the mechanised body of knowledge.
1.25 -% in Fig.\ref{fig:mathuni} on
1.26 -% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.27 -% starts with a formal {\em specification} of the problem to be solved.
1.28 -% \begin{figure}
1.29 -% \begin{center}
1.30 -% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
1.31 -% \caption{The three-dimensional universe of mathematics knowledge}
1.32 -% \label{fig:mathuni}
1.33 -% \end{center}
1.34 -% \end{figure}
1.35 -% The language for both axes is defined in the axis at the bottom, deductive
1.36 -% knowledge, in {\sisac} represented by Isabelle's theories.
1.37 +%REMOVED DUE TO SPACE CONSTRAINTS
1.38 +%At the state-of-the-art in mechanization of knowledge in engineering
1.39 +%sciences, the process does not stop with the mechanization of
1.40 +%mathematics traditionally used in these sciences. Rather, ``Formal
1.41 +%Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
1.42 +%description of physical items. Signal Processing, for instance is
1.43 +%concerned with physical devices for signal acquisition and
1.44 +%reconstruction, which involve measuring a physical signal, storing it,
1.45 +%and possibly later rebuilding the original signal or an approximation
1.46 +%thereof. For digital systems, this typically includes sampling and
1.47 +%quantization; devices for signal compression, including audio
1.48 +%compression, image compression, and video compression, etc. ``Domain
1.49 +%engineering''\cite{db:dom-eng} is concerned with {\em specification}
1.50 +%of these devices' components and features; this part in the process of
1.51 +%mechanization is only at the beginning in domains like Signal
1.52 +%Processing.
1.53 +%
1.54 +%TP-based programming, concern of this paper, is determined to
1.55 +%add ``algorithmic knowledge'' to the mechanised body of knowledge.
1.56 +%% in Fig.\ref{fig:mathuni} on
1.57 +%% p.\pageref{fig:mathuni}. As we shall see below, TP-based programming
1.58 +%% starts with a formal {\em specification} of the problem to be solved.
1.59 +%% \begin{figure}
1.60 +%% \begin{center}
1.61 +%% \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
1.62 +%% \caption{The three-dimensional universe of mathematics knowledge}
1.63 +%% \label{fig:mathuni}
1.64 +%% \end{center}
1.65 +%% \end{figure}
1.66 +%% The language for both axes is defined in the axis at the bottom, deductive
1.67 +%% knowledge, in {\sisac} represented by Isabelle's theories.
1.68
1.69 \subsection{Preparation of Simplifiers for the Program}\label{simp}
1.70
1.71 @@ -710,204 +711,89 @@
1.72 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
1.73 then they are called (canonical) simplifiers. These properties do not go without
1.74 saying, their establishment is a difficult task for the programmer; this task is
1.75 -not yet supported in the prototype.\par
1.76 -
1.77 -% If it is clear how the later calculation should look like
1.78 -% %WN3 ... Allgem.<-->Konkret ist gut: aber hier ist 'calculation'
1.79 -% %WN3 zu weit weg: der Satz geh"ort bestenfalls gleich an den
1.80 -% %WN3 Anfang von \sect.3
1.81 -% %WN3
1.82 -% %WN3 Im Folgenden sind einige Ungenauigkeiten:
1.83 -% and when
1.84 -% which mathematic rule
1.85 -% %WN3 rewrite-rule oder theorem ! Ein Paper enth"alt viele Begriffe
1.86 -% %WN3 und man versucht, die Anzahl so gering wie m"oglich zu halten
1.87 -% %WN3 und die verbleibenden so pr"azise zu definieren wie m"oglich;
1.88 -% %WN3 das Vermeiden von Wiederholungen muss mit anderen Mitteln erfolgen,
1.89 -% %WN3 als dieselbe Sache mit verschiedenen Namen zu benennen;
1.90 -% %WN3 das gilt insbesonders f"ur technische Begriffe wie oben
1.91 -% should be applied, it can be started to find ways of
1.92 -% simplifications.
1.93 -% %WN3 ... zu allgemein. Das Folgende w"urde durch einen Verweis in
1.94 -% %WN3 das Programm auf S.12 gewinnen.
1.95 -% This includes in e.g. the simplification of reational
1.96 -% expressions or also rewrites of an expession.
1.97 -% \par
1.98 -% %WN3 das Folgende habe ich aus dem Beispielprogramm auf S.12
1.99 -% %WN3 gestrichen, weil es aus prinzipiellen Gr"unden unsch"on ist.
1.100 -% %WN3 Und es ist so kompliziert dass es mehr Platz zum Erkl"aren
1.101 -% %WN3 braucht, als es wert ist ...
1.102 -% Obligate is the use of the function \texttt{drop\_questionmarks}
1.103 -% which excludes irrelevant symbols out of the expression. (Irrelevant symbols may
1.104 -% be result out of the system during the calculation. The function has to be
1.105 -% applied for two reasons. First two make every placeholder in a expression
1.106 -% useable as a constant and second to provide a better view at the frontend.)
1.107 -% \par
1.108 -% %WN3 Da kommt eine ganze Reihe von Ungenauigkeiten:
1.109 -% Most rewrites are represented through rulesets
1.110 -% %WN3 ... das ist schlicht falsch:
1.111 -% %WN3 _alle_ rewrites werden durch rule-sets erzeugt (per definition
1.112 -% %WN3 dieser W"orter).
1.113 -% this
1.114 -% rulesets tell the machine which terms have to be rewritten into which
1.115 -% representation.
1.116 -% %WN3 ... ist ein besonders "uberzeugendes Beispiel von Allgem.<-->Konkret:
1.117 -% %WN3 so allgemein, wie es hier steht, ist es
1.118 -% %WN3 # f"ur einen Fachmann klar und nicht ganz fachgem"ass formuliert
1.119 -% %WN3 (a rule-set rewrites a certain term into another with certain properties)
1.120 -% %WN3 # f"ur einen Nicht-Fachmann trotz allem unverst"andlich.
1.121 -% %WN3
1.122 -% %WN3 Wenn schon allgemeine S"atze, dann unmittelbar auf das Beispiel
1.123 -% %WN3 unten verweisen,
1.124 -% %WN3 oder besser: den Satz dorthin schreiben, wo er unmittelbar vom
1.125 -% %WN3 Beispiel gefolgt wird.
1.126 -% In the upcoming programm a rewrite can be applied only in using
1.127 -% such rulesets on existing terms.
1.128 -% %WN3 Du willst wohl soetwas sagen wie ...
1.129 -% %WN3 rewriting is the main concept to step-wise create and transform
1.130 -% %WN3 formulas in order to proceed towards a solution of a problem
1.131 -% %WN3 ...?
1.132 -% \paragraph{The core} of our implemented problem is the Z-Transformation
1.133 -% %WN3 ^^^^^ ist nicht gut: was soll THE CORE vermitteln, wenn man die
1.134 -% %WN3 Seite "uberfliegt ? Dass hier das Zentrum Deiner Arbeit liegt ?
1.135 -% %WN3
1.136 -% %WN3 Das Folgende ist eine allgemeine Design-"Uberlegung, die entweder
1.137 -% %WN3 vorne zur Einf"uhrung des Beispiels geh"ort,
1.138 -% %WN3 oder zur konkreten L"osung durch die Rechnung auf S.15/16.
1.139 -% (remember the description of the running example, introduced by
1.140 -% Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the
1.141 -% 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.142 -% transformation tables).
1.143 -% \par
1.144 -% %WN3 Zum Folgenden: 'axiomatization' ist schon in 3.1. angesprochen:
1.145 -% %WN3 entweder dort erg"anzen, wenn's wichtig ist, oder weglassen.
1.146 -% Rules, in {\sisac{}}'s programming language can be designed by the use of
1.147 -% axiomatization. In this axiomatization we declare how a term has to look like
1.148 -% (left side) to be rewritten into another form (right side). Every line of this
1.149 -% axiomatizations starts with the name of the rule.
1.150 +not yet supported in the prototype.
1.151
1.152 The prototype rewrites using theorems only. Axioms which are theorems as well
1.153 have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
1.154 assemble them in a rule-set and apply them as follows:
1.155
1.156 -% %WN3 Die folgenden Zeilen nehmen Platz weg: von hier auf S.6 verweisen
1.157 -% %\begin{example}
1.158 -% {\footnotesize
1.159 -% \label{eg:ruledef}
1.160 -% % \hfill\\
1.161 -% \begin{verbatim}
1.162 -% axiomatization where
1.163 -% rule1: ``1 = $\delta$[n]'' and
1.164 -% rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
1.165 -% rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
1.166 -% \end{verbatim}
1.167 -% %\end{example}
1.168 -% }
1.169 +{\footnotesize
1.170 +\begin{verbatim}
1.171 + 01 ML {*
1.172 + 02 val inverse_z =
1.173 + 03 Rls
1.174 + 04 {id = "inverse_z",
1.175 + 05 rew_ord = dummy_ord,
1.176 + 06 erls = Erls,
1.177 + 07 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
1.178 + 08 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
1.179 + 09 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
1.180 + 10 errpatts = [],
1.181 + 11 scr = ""}
1.182 + 12 *}
1.183 +\end{verbatim}}
1.184
1.185 -% 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.186 -%WN3 ... ist schon mehrmals gesagt worden. 1-mal pr"azise sagen gen"ugt.
1.187 -%WN3
1.188 -%WN3 mit dem append_rls unten verbirgst Du die ganze Komplexit"at von
1.189 -%WN3 rule-sets --- ich w"urde diese hier ausbreiten, damit man die
1.190 -%WN3 Schwierigkeit von TP-based programming ermessen kann.
1.191 -%WN3 Eine Erkl"arung wie in 3.4 und 3.5 braucht viel Platz, der sich
1.192 -%WN3 meines Erachtens mehr auszahlt als die allgemeinen S"atze
1.193 -%WN3 am Ende von 3.2 auf S.8.
1.194 -%WN3
1.195 -%WN3 mache ein 'grep -r "and rls";
1.196 -%WN3 auch in Build_Inverse_Z_Transform.thy hast Du 'Rls'
1.197 +\noindent The items, line by line, in the above record have the following purpose:
1.198 +\begin{description}
1.199 +\item[01..03] the ML-value \textit{inverse\_z} stores it's identifier
1.200 +as a string for ``reflection'' when switching between the language
1.201 +layers of Isabelle/ML (like in the Lucas-Interpreter) and
1.202 +Isabelle/Isar (like in the example program on p.\pageref{s:impl} on
1.203 +line {\rm 12}).
1.204
1.205 -%\begin{example}
1.206 -% \hfill\\
1.207 +\item[05..06] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
1.208 +\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
1.209 +(a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
1.210 +and (b) the assumptions of the \textit{rules} need not be evaluated
1.211 +(they just go into the context during rewriting).
1.212
1.213 - \label{eg:ruleapp}
1.214 - \begin{enumerate}
1.215 +\item[07..09] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
1.216 +also ML-functions (\S\ref{funs}) can come into this list as shown in
1.217 +\S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm}
1.218 +and \textit{Calc} respectively; for the purpose of reflection both
1.219 +contain their identifiers.
1.220
1.221 - \item Store rules in ruleset:
1.222 - {\footnotesize\begin{verbatim}
1.223 -01 val inverse_Z = append_rls "inverse_Z" e_rls
1.224 -02 [ Thm ("rule1",num_str @{thm rule1}),
1.225 -03 Thm ("rule2",num_str @{thm rule2}),
1.226 -04 Thm ("rule3",num_str @{thm rule3})
1.227 -05 ];\end{verbatim}}
1.228 +\item[10..11] are error-patterns not discussed here and \textit{scr}
1.229 +is prepared to get a program, automatically generated by {\sisac} for
1.230 +producing intermediate rewrites when requested by the user.
1.231
1.232 - \item Define exression:
1.233 - {\footnotesize\begin{verbatim}
1.234 -06 val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}}
1.235 +\end{description}
1.236
1.237 +\noindent It is advisable to immediately test rule-sets; for that
1.238 +purpose an appropriate term has to be created; \textit{parse} takes a
1.239 +context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
1.240 +Z}^{-1}$) and creates a term:
1.241
1.242 -%WN3 vergleiche bitte obige Zeile mit den letzten 3 Zeilen aus S.8,
1.243 -%WN3 diese entsprechen dem g"angigen functional-programming Stil.
1.244 +{\footnotesize
1.245 +\begin{verbatim}
1.246 + 01 ML {*
1.247 + 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
1.248 + 03 *}
1.249 + 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1",
1.250 + 05 "RealDef.real => RealDef.real => RealDef.real") $
1.251 + 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...)
1.252 +\end{verbatim}}
1.253
1.254 +\noindent The internal representation of the term, as required for
1.255 +rewriting, consists of \textit{Const}ants, a pair of a string
1.256 +\textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
1.257 +\textit{Free} and the respective constructor \textit{\$}. Now the
1.258 +term can be rewritten by the rule-set \textit{inverse\_z}:
1.259
1.260 +{\footnotesize
1.261 +\begin{verbatim}
1.262 + 01 ML {*
1.263 + 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
1.264 + 03 term2str t';
1.265 + 04 terms2str asm;
1.266 + 05 *}
1.267 + 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
1.268 + 07 val it = "|| z || > 1 & || z || > </alpha>" : string
1.269 +\end{verbatim}}
1.270
1.271 -
1.272 -%WN3 Super w"ar's, wenn Du hier schon die interne Darstellung von
1.273 -%WN3 Isabelle Termen zeigen k"onntest, dann w"urde ich den entsprechenden Teil
1.274 -%WN3 am Ende von S.8 und Anfang S.9 (erste 2.1 Zeilen) l"oschen.
1.275 -
1.276 -%JR ich habe einige male über seite acht gelesen, finde aber dass der teil über
1.277 -%JR die interne representation dorthin besser passt da diese in unserem
1.278 -%JR gezeigten beispiel ja in direkter verbindung zur gezeigtem funktion besteht
1.279 -%JR und so der übergang exzellent ist.
1.280 -
1.281 - \item Apply ruleset:
1.282 - {\footnotesize\begin{verbatim}
1.283 -07 val SOME (sample_term', asm) =
1.284 -08 rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}}
1.285 -
1.286 - \end{enumerate}
1.287 -%\end{example}
1.288 -
1.289 -%WN3 Wie oben gesagt, die folgenden allgemeinen S"atze scheinen
1.290 -%WN3 weniger wert als eine konkrete Beschreibung der rls-Struktur.
1.291 -%WN3
1.292 -%WN3 Ich nehme an, wir l"oschen das Folgende
1.293 -%WN3 und ich spare mir Kommentare (ausser Du hast noch Zeit/Energie
1.294 -%WN3 daf"ur und fragst extra nach).
1.295 -
1.296 -% The use of rulesets makes it much easier to develop our designated applications,
1.297 -% but the programmer has to be careful and patient. When applying rulesets
1.298 -% two important issues have to be mentionend:
1.299 -% \begin{enumerate}
1.300 -% \item How often the rules have to be applied? In case of
1.301 -% transformations it is quite clear that we use them once but other fields
1.302 -% reuqire to apply rules until a special condition is reached (e.g.
1.303 -% a simplification is finished when there is nothing to be done left).
1.304 -% \item The order in which rules are applied often takes a big effect
1.305 -% and has to be evaluated for each purpose once again.
1.306 -% \end{enumerate}
1.307 -% In the special case of Signal Processing the rules defined in the
1.308 -% Example upwards have to be applied in a dedicated order to transform all
1.309 -% constants first of all. After this first transformation step has been done it no
1.310 -% mather which rule fit's next.
1.311 -
1.312 -%WN3 Beim Paper-Schreiben ist mir aufgefallen, dass eine Konstante ZZ_1
1.313 -%WN3 (f"ur ${\cal Z}^{-1}$) die eben beschriebenen Probleme gel"ost
1.314 -%WN3 h"atte: auf S.6 in rule1, auf S.12 in line 10 und in der Rechnung S.16
1.315 -%WN3 hab' ich die Konstante schon eingef"uhrt.
1.316 -%WN3
1.317 -%WN3 Bite bei der rewrite_set_ demo oben bitte schummeln !
1.318 -
1.319 -%JR TODO es is klein z bitte auf S.6 in rule1, auf S.12 in line 10 ausbessern
1.320 -%JR ${\cal z}^{-1}$
1.321 -
1.322 -
1.323 -In the first step of upper code we extend the method's own ruleset with
1.324 -the predefined rules.\par
1.325 -When adding rules to this set we already have to take care on the order the
1.326 -rules we be applied in later context, this can be an important point when it
1.327 -comes to a case where one rule has to be applied explicite before an other.
1.328 -\par Rules are added to the ruleset with an unique name and a reference to their
1.329 -defined theorem. After summerizing this rules we still have the posibility to
1.330 -pick out a single one.
1.331 -\par In upper example we define an expression, as it comes up in our running
1.332 -example, it can be useful to take a look at \S\ref{funs} on p.\pageref{funs} to
1.333 -get to know {\sisac}'s' internal representation of variables.
1.334 -\par Upper step three is the final use of a ruleset for rewriting expression.
1.335 -The inline declared \ttfamily sample\_term' \normalfont is the result of applying the upper
1.336 -rule set one time to the before defined \texttt{sample\_term'}.
1.337 -
1.338 +\noindent The resulting term \textit{t} and the assumptions
1.339 +\textit{asm} are converted to readablle strings by \textit{term2str}
1.340 +and \textit{terms2str}.
1.341
1.342 \subsection{Preparation of ML-Functions}\label{funs}
1.343 Some functionality required in programming, cannot be accomplished by
2.1 --- a/test/Tools/isac/Test_Some.thy Thu Sep 13 17:39:07 2012 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Thu Sep 13 21:20:05 2012 +0200
2.3 @@ -12,34 +12,6 @@
2.4 text {**}
2.5 ML {* (*==================*)
2.6 *}
2.7 -text {*
2.8 -In order to be recognised as a function constant in the program source (see p. line)
2.9 -the function needs to be declared in the theory; then it can be parsed:
2.10 -*}
2.11 -consts
2.12 - argument'_in :: "real => real" ("argument'_in _" 10)
2.13 -
2.14 -ML {*
2.15 -print_depth 55;
2.16 - val SOME t = parseNEW ctxt "argument_in (X (z::real))";
2.17 - (*Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real \<Rightarrow> RealDef.real") $ (Free ("...", "'a \<Rightarrow> RealDef.real") $ Free ("z...", "'a")): term*)
2.18 -*}
2.19 -text {* The function body is then implemented directly in ML; the function definition
2.20 -provides a unique prefix \textit{eval\_} to the function name:*}
2.21 -ML {*
2.22 - fun eval_argument_in _
2.23 - "Build_Inverse_Z_Transform.argument'_in"
2.24 - (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $ (f $ arg))) _ =
2.25 - if is_Free arg (*could be something to be simplified before*)
2.26 - then SOME (term2str t ^ " = " ^ term2str arg, Trueprop $ (mk_equality (t, arg)))
2.27 - else NONE
2.28 - | eval_argument_in _ _ _ _ = NONE;
2.29 -*}
2.30 -text {* The function body needs to adopt to many technicalities of Isabelle, for instance,
2.31 -*}
2.32 -ML {*
2.33 -
2.34 -*}
2.35 ML {*
2.36 *}
2.37 ML {* (*==================*)