|
1 \documentclass{article} |
|
2 \usepackage{a4} |
|
3 \usepackage{times} |
|
4 \usepackage{latexsym} |
|
5 \bibliographystyle{alpha} |
|
6 \usepackage{graphicx} |
|
7 |
|
8 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
9 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
|
10 \def\Problem{ {\tt Problem }} |
|
11 |
|
12 \title{Upcoming Userinterfaces for Computer Theorem Provers.\\ |
|
13 The case of Isabelle |
|
14 } |
|
15 |
|
16 \author{G. Schafhauser, A. Schulhofer, M. Steger\\ |
|
17 Knowledge Management Institute (KMI)\\ |
|
18 TU Graz} |
|
19 |
|
20 \begin{document} |
|
21 \maketitle |
|
22 \abstract{ |
|
23 TODO} |
|
24 |
|
25 \section{Introduction}\label{intro} (WN) |
|
26 Computer theorem proving (CTP)\footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}, |
|
27 |
|
28 graphical user interfaces (GUI) |
|
29 |
|
30 %Georg |
|
31 \section{State of the art in CTP Interfaces} |
|
32 |
|
33 \subsection{A European technology: Coq and Isabelle}\label{ctp-techn} |
|
34 http://en.wikipedia.org/wiki/Coq\\ |
|
35 http://coq.inria.fr/ |
|
36 |
|
37 http://en.wikipedia.org/wiki/Isabelle\_(theorem\_prover)\\ |
|
38 http://isabelle.in.tum.de/index.html |
|
39 |
|
40 why math -- functional: some of the languages have been specifically designed for constructing software for symbolic computation (SC). |
|
41 %+ required for \ref{ml-users} |
|
42 |
|
43 SC http://en.wikipedia.org/wiki/Symbolic\_computation |
|
44 % mainly does not compute numerical values, but terms containing variables like functions (symbols) |
|
45 |
|
46 The LCF project |
|
47 http://hopl.murdoch.edu.au/showlanguage.prx?exp=8177 |
|
48 specifically designed a 'meta language' (ML) |
|
49 http://en.wikipedia.org/wiki/ML\_(programming\_language) |
|
50 \cite{pl:milner97} |
|
51 for developing CTP |
|
52 |
|
53 |
|
54 \subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa} |
|
55 CoqIDE, .. |
|
56 http://coq.inria.fr/what-is-coq?q=node/57\\ |
|
57 earlier than Isabelle/jEdit |
|
58 |
|
59 ProofGeneral for Isabelle |
|
60 http://proofgeneral.inf.ed.ac.uk/\\ |
|
61 emacs stone age ? |
|
62 |
|
63 \subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir} |
|
64 @ interaction close to tty (Telegraph)\\ |
|
65 BUT: separate parts in {\em one} proof could be processed in parallel |
|
66 |
|
67 @ http://www.informatik.uni-bremen.de/uitp/ |
|
68 |
|
69 @ ... see\\ |
|
70 http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
|
71 http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
|
72 |
|
73 %Andreas |
|
74 \section{Isabelle's plans for new user-interfaces}\label{gui-plans} |
|
75 http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
|
76 http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
|
77 |
|
78 theorem proving will be integrated into software development |
|
79 |
|
80 hundreds of proof obligations are generated during a software verification process |
|
81 |
|
82 so the final goald of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE). |
|
83 |
|
84 still many principal issues need to be clarified with respect to integration of CTP and other development tools. So engaging into details makes no sense at the present, and Isabelle will approach the final goal via experimental intermediate steps of integration. |
|
85 |
|
86 \subsection{Connect ML-world to the users' world via JVM}\label{ml-users} |
|
87 In Sect.\ref{ctp-techn} reasons have been given, why mathematics software at the state-of-the-art cannot be written in Java or the like. On the other side, Sect.\ref{gui-requir} stated requirements for mathematical user interfaces, which cannot be accomplished by ML-like languages. These requirements can be best accomplished by languages like Java, which have powerful libraries available for convenient assembly of GUIs. |
|
88 |
|
89 \paragraph{Example: a functional mathematics engine} as the experimental one in the \sisac-project is given by the following signature: |
|
90 {\it |
|
91 \begin{tabbing} |
|
92 \=xx\=xxxxxxxxxxxxxxxxxxxxxxxxx\=\kill |
|
93 \>signature INTERPRETER =\\ |
|
94 \>sig\\ |
|
95 \>\>type calcstate\\ |
|
96 \>\>type step = formula * position * tactic\\ |
|
97 \>\> \\ |
|
98 \>\>val do\_next : program $\rightarrow$ calcstate $\rightarrow$ (calcstate * step)\\ |
|
99 \>\>val apply\_tactic : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ tactic $\rightarrow$ (calcstate * step list)\\ |
|
100 \>\>val apply\_formula : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ formula $\rightarrow$ (calcstate * step list)\\ |
|
101 %\\ |
|
102 %\>\>val get\_next : program $\rightarrow$ calcstate $\rightarrow$ step\\ |
|
103 %\>\>val get\_applicable\_tactics : program $\rightarrow$ calcstate $\rightarrow$ tactic list\\ |
|
104 %\>\>val get\_intermediate : program $\rightarrow$ calcstate $\rightarrow$ position * position $\rightarrow$ step list\\ |
|
105 \>end |
|
106 \end{tabbing}} |
|
107 The three essential functions are \textit{do\_next}, which reads a \textit{program} for determining the next \textit{step} in a calculation, the function \textit{apply\_tactic}, which applies a \textit{tactic} input by the user to the current \textit{position} in a calculation and thus may produce a list of \textit{step}s and the function \textit{apply\_formula}, which applies an input \textit{formula} accordingly. |
|
108 |
|
109 Now, the point with functional programming is, that the functions do {\em not} cause persistent updates in some memory, rather: all three functions above take the current state of the calculation, \textit{calcstate}, as an argument and after they have done they work return the updated \textit{calcstate}. |
|
110 |
|
111 There are several advantages of this kind of programming: more straight forward verification, which is not discussed here, and other features. For instance, given the three functions above, it is easy to undo steps of calculations, or go back to an earlier step of calculations: one just needs to store the \textit{calcstate}s (in a list), even without knowing the details of the \textit{calcstate}, which thus can be encapsulated for internal access only. |
|
112 |
|
113 \paragraph{Example: an object-oriented wrapper} as required for embedding the above mathematics engine into an object-oriented system. Such a wrapper looks like this: |
|
114 |
|
115 TODO |
|
116 |
|
117 \subsection{Scala as a mediator between ML and JVM}\label{scala-medi} |
|
118 {\em new} language --- what for, ideas ... |
|
119 |
|
120 \subsection{Support for parallel processing}\label{actors} |
|
121 actors copied from erlang |
|
122 |
|
123 % Marco |
|
124 \section{Planned contributions at TU Graz} |
|
125 |
|
126 \subsection{Make Isabelle process structured derivations}\label{struct-der} |
|
127 Structured Derivations (SD) is a format for calculational reasoning, which has been established by \cite{back-grundy-wright-98}. This is an example calculation: |
|
128 {\it\begin{tabbing} |
|
129 123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill |
|
130 \> $\bullet$\> \Problem [ maximum\_by, calculus ]\\ |
|
131 \>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$\\ |
|
132 \>\> $\bullet$\> \Problem [make, diffable, funtion]\\ |
|
133 \>\> \dots\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\ |
|
134 \>\> $\bullet$\> \Problem [on\_interval, for\_maximum, differentiate, function]\\ |
|
135 \>\>\> $\vdash$\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\ |
|
136 \>\>\> $\bullet$\> \Problem [differentiate, funtion]\\ |
|
137 \>\>\> \dots\> $\overline{A}^\prime(\alpha) = 8\cdot r^2\cdot(-(\sin\alpha)^2+(\cos\alpha)^2 - 2\cdot\sin\alpha\cdot\cos\alpha)$\\ |
|
138 \>\>\> $\bullet$\> \Problem [on\_interval, goniometric, equation]\\ |
|
139 \>\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\ |
|
140 \>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\ |
|
141 \>\> $\bullet$\> \Problem [tool, find\_values]\\ |
|
142 \>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ]\\ |
|
143 \> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate ! |
|
144 \end{tabbing}} |
|
145 The plan is to use the machinery provided Isabelle/Isar as a 'logical operating system' ~\cite{isar-impl} and adapt the machinery such that is accepts SC in parallel to the Isar proof language~\cite{wenzel:isar}. |
|
146 |
|
147 This plan involves the following details. |
|
148 |
|
149 \subsection{Add a plug-in to jEdit}\label{plugin} |
|
150 file structure, copied from example project ... |
|
151 |
|
152 \subsection{Details of NetBeans projects}\label{netbeans} |
|
153 Scala + Java: html project files |
|
154 |
|
155 \subsection{Use interfaces between Java and Scala}\label{java-scala} |
|
156 how are data exchanged between Scala and Java ... |
|
157 |
|
158 |
|
159 \section{Conclusion and future work} |
|
160 |
|
161 |
|
162 \bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl} |
|
163 \end{document} |