1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 21:40:22 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 22:06:39 2012 +0200
1.3 @@ -129,7 +129,7 @@
1.4 support, guiding the learner towards a solution, another kind of
1.5 technology is required. %TODO ... connect to prototype ...
1.6
1.7 -Both kinds of support can be acchieved by so-called
1.8 +Both kinds of support can be achieved by so-called
1.9 Lucas-Interpretation which combines deduction and computation and, for
1.10 the latter, uses a novel kind of programming language. This language
1.11 is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
1.12 @@ -209,7 +209,7 @@
1.13 programming language''. In the
1.14 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
1.15 a language is prototyped in line with~\cite{plmms10} and built upon
1.16 -the theorem prover
1.17 +the theorem prover.
1.18 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
1.19 The TP services are coordinated by a specific interpreter for the
1.20 programming language, called
1.21 @@ -224,11 +224,11 @@
1.22 Telematics (computer science with focus on Signal Processing) he had
1.23 general knowledge in programming as well as specific domain knowledge
1.24 in Signal Processing; and he was {\em not} involved in the development of
1.25 -{\sisac}'s programming language and interpeter, thus a novice to the
1.26 +{\sisac}'s programming language and interpreter, thus a novice to the
1.27 language.
1.28
1.29 The goal of the case study was (1) some TP-based programs for
1.30 -interactive course material for a specific ``Adavanced Signal
1.31 +interactive course material for a specific ``Advanced Signal
1.32 Processing Lab'' in a higher semester, (2) respective program
1.33 development with as little advice from the {\sisac}-team and (3) records
1.34 and comments for the main steps of development in an Isabelle theory;
1.35 @@ -247,7 +247,8 @@
1.36 \end{figure}
1.37
1.38 The problem is from the domain of Signal Processing and requests to
1.39 -determine the inverse ${\cal Z}$-transform for a given term. Fig.\ref{fig-interactive}
1.40 +determine the inverse ${\cal Z}$-transform for a given term.
1.41 +Fig.\ref{fig-interactive}
1.42 also shows the beginning of the interactive construction of a solution
1.43 for the problem. This construction is done in the right window named
1.44 ``Worksheet''.
1.45 @@ -268,7 +269,7 @@
1.46 TP-based language is not concerned with interaction at all; we will
1.47 see that the program contains neither input-statements nor
1.48 output-statements. Rather, interaction is handled by the interpreter
1.49 -pf the language.
1.50 +of the language.
1.51
1.52 So there is a clear separation of concerns: Dialogues are adapted by
1.53 dialogue authors (in Java-based tools), using TP services provided by
1.54 @@ -276,7 +277,7 @@
1.55 mathematics-authors (in Isabelle/ML); their task is concern of this
1.56 paper.
1.57
1.58 -\paragraph{The paper is structed} as follows: The introduction
1.59 +\paragraph{The paper is structured} as follows: The introduction
1.60 \S\ref{intro} is followed by a brief re-introduction of the TP-based
1.61 programming language in \S\ref{PL}, which extends the executable
1.62 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
1.63 @@ -286,7 +287,7 @@
1.64 prepare domain knowledge, implement the formal specification of the
1.65 problem, prepare the environment for the interpreter, implement the
1.66 program in \S\ref{isabisac} to \S\ref{progr} respectively.
1.67 -The workflow of programming, debugging and testing is
1.68 +The work-flow of programming, debugging and testing is
1.69 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
1.70 give directions identified for future development.
1.71
1.72 @@ -370,13 +371,13 @@
1.73 The prototype extends Isabelle's language by specific statements
1.74 called tactics~\footnote{{\sisac}'s tactics are different from
1.75 Isabelle's tactics: the former concern steps in a calculation, the
1.76 -latter concern proofs.} and tacticals. For the programmer these
1.77 +latter concern proofs.} and tactics. For the programmer these
1.78 statements are functions with the following signatures:
1.79
1.80 \begin{description}
1.81 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
1.82 term} * {\it term}\;{\it list}$:
1.83 -this tactic appplies {\it theorem} to a {\it term} yielding a {\it
1.84 +this tactic applies {\it theorem} to a {\it term} yielding a {\it
1.85 term} and a {\it term list}, the list are assumptions generated by
1.86 conditional rewriting. For instance, the {\it theorem}
1.87 $b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
1.88 @@ -385,7 +386,7 @@
1.89
1.90 \item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
1.91 term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
1.92 -this tactic appplies {\it ruleset} to a {\it term}; {\it ruleset} is
1.93 +this tactic applies {\it ruleset} to a {\it term}; {\it ruleset} is
1.94 a confluent and terminating term rewrite system, in general. If
1.95 none of the rules ({\it theorem}s) is applicable on interpretation
1.96 of this tactic, an exception is thrown.
1.97 @@ -432,10 +433,10 @@
1.98 derive the formula from this context --- or give feedback, that no
1.99 derivation can be found.
1.100
1.101 -\subsection{Tacticals as Control Flow Statements}
1.102 +\subsection{Tactics as Control Flow Statements}
1.103 The flow of control in a program can be determined by {\tt if then else}
1.104 and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
1.105 -by additional tacticals:
1.106 +by additional tactics:
1.107 \begin{description}
1.108 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
1.109 term}$: iterates over tactics which take a {\it term} as argument as
1.110 @@ -462,9 +463,9 @@
1.111 {\it tactic} is applied to the first {\it term} yielding an
1.112 intermediate term (not appearing in the signature); the intermediate
1.113 term is added to the environment the first {\it term} is evaluated in
1.114 -etc as long as the first {\it term} is true.
1.115 +etc. as long as the first {\it term} is true.
1.116 \end{description}
1.117 -The tacticals are not treated as break-points by Lucas-Interpretation
1.118 +The tactics are not treated as break-points by Lucas-Interpretation
1.119 and thus do neither contribute to the calculation nor to interaction.
1.120
1.121 \section{Concepts and Tasks in TP-based Programming}\label{trial}
1.122 @@ -626,7 +627,7 @@
1.123 The running example requires to determine the inverse $\cal
1.124 Z$-transform for a class of functions. The domain of Signal Processing
1.125 is accustomed to specific notation for the resulting functions, which
1.126 -are absolutely summable and are called step-response: $u[n]$, where $u$ is the
1.127 +are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
1.128 function, $n$ is the argument and the brackets indicate that the
1.129 arguments are discrete. Surprisingly, Isabelle accepts the rules for
1.130 ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle
1.131 @@ -664,7 +665,7 @@
1.132 the basic axioms of mathematics~\footnote{This way of rigorously
1.133 deriving all knowledge from first principles is called the
1.134 LCF-paradigm in TP.}. In the case of the ${\cal Z}$-Transform the most advanced
1.135 -knowledge can be found in the theoris on Multivariate
1.136 +knowledge can be found in the theories on Multivariate
1.137 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
1.138 building up knowledge such that a proof for the above rules would be
1.139 reasonably short and easily comprehensible, still requires lots of
1.140 @@ -704,7 +705,7 @@
1.141
1.142 \subsection{Preparation of Simplifiers for the Program}\label{simp}
1.143
1.144 -All evaluation in the prototyp's Lucas-Interpreter is done by term rewriting on
1.145 +All evaluation in the prototype's Lucas-Interpreter is done by term rewriting on
1.146 Isabelle's terms, see \S\ref{meth} below; in this section some of respective
1.147 preparations are described. In order to work reliably with term rewriting, the
1.148 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
1.149 @@ -791,13 +792,13 @@
1.150 \end{verbatim}}
1.151
1.152 \noindent The resulting term \textit{t} and the assumptions
1.153 -\textit{asm} are converted to readablle strings by \textit{term2str}
1.154 +\textit{asm} are converted to readable strings by \textit{term2str}
1.155 and \textit{terms2str}.
1.156
1.157 \subsection{Preparation of ML-Functions}\label{funs}
1.158 Some functionality required in programming, cannot be accomplished by
1.159 rewriting. So the prototype has a mechanism to call functions within
1.160 -the rewrite-engine: certain redexes in Isabelle terms call these
1.161 +the rewrite-engine: certain regexes in Isabelle terms call these
1.162 functions written in SML~\cite{pl:milner97}, the implementation {\em
1.163 and} meta-language of Isabelle. The programmer has to use this
1.164 mechanism.
1.165 @@ -852,13 +853,13 @@
1.166 \end{verbatim}}
1.167
1.168 \noindent The function body creates either creates \texttt{NONE}
1.169 -telling the rewrite-engine to search for the next redex, or creates an
1.170 +telling the rewrite-engine to search for the next regex, or creates an
1.171 ad-hoc theorem for rewriting, thus the programmer needs to adopt many
1.172 technicalities of Isabelle, for instance, the \textit{Trueprop}
1.173 constant.
1.174
1.175 \bigskip This sub-task particularly sheds light on basic issues in the
1.176 -design of a programming language, the integration of diffent language
1.177 +design of a programming language, the integration of differential language
1.178 layers, the layer of Isabelle/Isar and Isabelle/ML.
1.179
1.180 Another point of improvement for the prototype is the rewrite-engine: The
1.181 @@ -1040,7 +1041,7 @@
1.182 \item[01..02]\textit{store\_specification:} stores the result of the
1.183 function \textit{prep\_specification} in a global reference
1.184 \textit{Unsynchronized.ref}, which causes principal conflicts with
1.185 -Isabelle's asyncronous document model~\cite{Wenzel-11:doc-orient} and
1.186 +Isabelle's asynchronous document model~\cite{Wenzel-11:doc-orient} and
1.187 parallel execution~\cite{Makarius-09:parall-proof} and is under
1.188 reconstruction already.
1.189
1.190 @@ -1052,7 +1053,7 @@
1.191 \item[05] is the Isabelle \textit{theory} required to parse the
1.192 specification in lines {\rm 07..10}.
1.193 \item[06] is a key into the tree of all specifications as presented to
1.194 -the user (where some branches might be hidden by the dialog
1.195 +the user (where some branches might be hidden by the dialogue
1.196 component).
1.197 \item[07..10] are the specification with input, pre-condition, output
1.198 and post-condition respectively; note that the specification contains
1.199 @@ -1164,7 +1165,7 @@
1.200 \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
1.201 \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
1.202 \textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
1.203 -\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}
1.204 +\textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec}
1.205 and (c) is required for the derivation-machinery checking user-input formulas.
1.206
1.207 \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}.
1.208 @@ -1304,7 +1305,7 @@
1.209 The program code, above presented as a string, is parsed by Isabelle's
1.210 parser --- the program is an Isabelle term. This fact is expected to
1.211 simplify verification tasks in the future; on the other hand, this
1.212 -fact causes troubles in error detectetion which are discussed as part
1.213 +fact causes troubles in error detection which are discussed as part
1.214 of the workflow in the subsequent section.
1.215
1.216 \section{Workflow of Programming in the Prototype}\label{workflow}
1.217 @@ -1313,7 +1314,7 @@
1.218 {\sisac}-prototype re-uses this IDE as a programming environment. The
1.219 experiences from this re-use show, that the essential components are
1.220 available from Isabelle/jEdit. However, additional tools and features
1.221 -are required to acchieve acceptable usability.
1.222 +are required to achieve acceptable usability.
1.223
1.224 So notable experiences are reported here, also as a requirement
1.225 capture for further development of TP-based languages and respective
1.226 @@ -1378,7 +1379,7 @@
1.227 perfect. Probably we have forgotten to store this function correctly~?
1.228 We review the respective \texttt{calclist} (again an
1.229 \textit{Unsynchronized.ref} to be removed in order to adjust to
1.230 -IsabelleIsar's asyncronous document model):
1.231 +IsabelleIsar's asynchronous document model):
1.232
1.233 {\footnotesize
1.234 \begin{verbatim}
1.235 @@ -1428,7 +1429,7 @@
1.236 \texttt{ctree * pos} as last argument taken. The interpreter-state is
1.237 a pair of a tree \texttt{ctree} representing the calculation created
1.238 (see the example below) and a position \texttt{pos} in the
1.239 -calculation. The function delivers a quadrupel, beginning with the new
1.240 +calculation. The function delivers a quadruple, beginning with the new
1.241 formula \texttt{mout} and the next tactic followed by the new
1.242 interpreter-state.
1.243
1.244 @@ -1452,7 +1453,7 @@
1.245 ...
1.246 \end{verbatim}}
1.247
1.248 -\noindent Several douzens of calls for \texttt{me} are required to
1.249 +\noindent Several dozens of calls for \texttt{me} are required to
1.250 create the lines in the calculation below (including the sub-problems
1.251 not shown). When an error occurs, the reason might be located
1.252 many steps before: if evaluation by rewriting, as done by the prototype,
1.253 @@ -1929,7 +1930,7 @@
1.254 \item Combine the prototype's programming language with Isabelle's
1.255 powerful function package and probably with more of SML's
1.256 pattern-matching features; include parallel execution on multi-core
1.257 -machines into the language desing.
1.258 +machines into the language design.
1.259 \item Extend the prototype's Lucas-Interpreter such that it also
1.260 handles functions defined by use of Isabelle's functions package; and
1.261 generalize Isabelle's code generator such that efficient code for the
1.262 @@ -1941,14 +1942,14 @@
1.263 of programs.
1.264 \end{itemize}
1.265 Provided successful accomplishment, these points provide distinguished
1.266 -components for virtual workbenches appealing to practictioner of
1.267 +components for virtual workbenches appealing to practitioner of
1.268 engineering in the near future.
1.269
1.270 -\medskip Interactive couse material, as addressed by the title, then
1.271 +\medskip Interactive course material, as addressed by the title, then
1.272 can comprise step-wise problem solving created as a side-effect of a
1.273 TP-based program: Lucas-Interpretation not only provides an
1.274 interactive programming environment, Lucas-Interpretation also can
1.275 -provide TP-based services for a flexible dialog component with
1.276 +provide TP-based services for a flexible dialogue component with
1.277 adaptive user guidance for independent and inquiry-based learning.
1.278
1.279