|
1 %WN mit diesen 3 Zeichen beginnen meine Kommentare |
|
2 |
1 \documentclass[12pt,a4paper]{article} |
3 \documentclass[12pt,a4paper]{article} |
2 \usepackage{a4} |
4 \bibliographystyle{alpha} |
3 \usepackage[naustrian]{babel} |
5 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
4 \usepackage[latin1]{inputenc} |
6 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
5 \usepackage{calc} |
7 %\usepackage{a4} |
6 \usepackage{amsmath} |
8 %\usepackage[naustrian]{babel} |
7 \usepackage{epsfig} |
9 %\usepackage[latin1]{inputenc} |
8 \usepackage{graphicx} |
10 %\usepackage{calc} |
9 \usepackage{xcolor} |
11 %\usepackage{amsmath} |
10 \usepackage{amsfonts} |
12 %\usepackage{epsfig} |
11 |
13 %\usepackage{graphicx} |
12 % Seitenräder einstellen und Höhe der Seitenzahlen |
14 %\usepackage{xcolor} |
13 \usepackage{geometry} |
15 %\usepackage{amsfonts} |
14 \geometry{a4paper, left=2.5cm, right=2cm, top=3cm, bottom=2.8cm} |
16 % |
15 \setlength{\footskip}{2cm} |
17 %WN BITTE DIESE DEFINITIONEN WEGLASSEN ... |
16 |
18 %% Seitenräder einstellen und Höhe der Seitenzahlen |
17 |
19 %\usepackage{geometry} |
18 %Zähler definieren und Starwert setzen: |
20 %\geometry{a4paper, left=2.5cm, right=2cm, top=3cm, bottom=2.8cm} |
19 \newcommand{\R}{\mathbb R} |
21 %\setlength{\footskip}{2cm} |
20 %\newcommand{\N}{\mathbb N} |
22 % |
21 %\newcommand{\Q}{\mathbb Q} |
23 % |
22 %\newcommand{\C}{\mathbb C} |
24 %%Zähler definieren und Starwert setzen: |
23 |
25 %\newcommand{\R}{\mathbb R} |
24 |
26 %%\newcommand{\N}{\mathbb N} |
25 \newcounter{ctr} |
27 %%\newcommand{\Q}{\mathbb Q} |
26 \setcounter{ctr}{0} |
28 %%\newcommand{\C}{\mathbb C} |
27 |
29 % |
28 \newcounter{Teubner} |
30 % |
29 \newcounter{Klingenberg} |
31 %\newcounter{ctr} |
30 \newcounter{T} |
32 %\setcounter{ctr}{0} |
31 \newcounter{Vo} |
33 % |
32 \newcounter{Se} |
34 %\newcounter{Teubner} |
33 \newcounter{E} |
35 %\newcounter{Klingenberg} |
34 \newcounter{Bwl} |
36 %\newcounter{T} |
35 \newcounter{Int} |
37 %\newcounter{Vo} |
36 \newcounter{Prim} |
38 %\newcounter{Se} |
37 \newcounter{Z} |
39 %\newcounter{E} |
38 \setcounter{Z}{0} |
40 %\newcounter{Bwl} |
39 \setcounter{Teubner}{1} |
41 %\newcounter{Int} |
40 \setcounter{Klingenberg}{2} |
42 %\newcounter{Prim} |
41 \setcounter{T}{1} |
43 %\newcounter{Z} |
42 \setcounter{Vo}{7} |
44 %\setcounter{Z}{0} |
43 \setcounter{Se}{2} |
45 %\setcounter{Teubner}{1} |
44 \setcounter{E}{3} |
46 %\setcounter{Klingenberg}{2} |
45 \setcounter{Bwl}{4} |
47 %\setcounter{T}{1} |
46 \setcounter{Int}{5} |
48 %\setcounter{Vo}{7} |
47 \setcounter{Prim}{6} |
49 %\setcounter{Se}{2} |
48 %BSP |
50 %\setcounter{E}{3} |
49 \newenvironment{myBsp}{ |
51 %\setcounter{Bwl}{4} |
50 \begin{list}{\textbf{\textsc{Bsp:}}}{ |
52 %\setcounter{Int}{5} |
51 \setlength{\labelwidth}{8Pc} |
53 %\setcounter{Prim}{6} |
52 \setlength{\labelsep}{0.5Pc} |
54 %%BSP |
53 \setlength{\rightmargin}{0Pc} |
55 %\newenvironment{myBsp}{ |
54 \setlength{\leftmargin}{2Pc} |
56 % \begin{list}{\textbf{\textsc{Bsp:}}}{ |
55 \setlength{\parsep}{0ex plus 0.5ex} |
57 % \setlength{\labelwidth}{8Pc} |
56 \setlength{\listparindent}{1em} |
58 % \setlength{\labelsep}{0.5Pc} |
57 \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
59 % \setlength{\rightmargin}{0Pc} |
58 \setlength{\topsep}{0.5Pc} |
60 % \setlength{\leftmargin}{2Pc} |
59 }} |
61 % \setlength{\parsep}{0ex plus 0.5ex} |
60 {\end{list} |
62 % \setlength{\listparindent}{1em} |
61 } |
63 % \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
62 |
64 % \setlength{\topsep}{0.5Pc} |
63 |
65 % }} |
64 %Lemma |
66 % {\end{list} |
65 \newenvironment{myLemma}{ |
67 %} |
66 \begin{list}{\textsc{\textbf{Lemma:\ \ \ }}}{ |
68 % |
67 \setlength{\labelsep}{-0.5Pc} |
69 % |
68 \setlength{\leftmargin}{1Pc} |
70 %%Lemma |
69 \setlength{\parsep}{0ex plus 0.5ex} |
71 %\newenvironment{myLemma}{ |
70 \setlength{\listparindent}{1em} |
72 % \begin{list}{\textsc{\textbf{Lemma:\ \ \ }}}{ |
71 \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
73 % \setlength{\labelsep}{-0.5Pc} |
72 \setlength{\topsep}{0.5Pc} |
74 % \setlength{\leftmargin}{1Pc} |
73 }} |
75 % \setlength{\parsep}{0ex plus 0.5ex} |
74 {\end{list} |
76 % \setlength{\listparindent}{1em} |
75 } |
77 % \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
76 %Korollar |
78 % \setlength{\topsep}{0.5Pc} |
77 \newenvironment{myKorollar}{ |
79 % }} |
78 \begin{list}{\textsc{\textbf{Korollar: }}}{ |
80 % {\end{list} |
79 \setlength{\labelwidth}{8Pc} |
81 %} |
80 \setlength{\labelsep}{0.5Pc} |
82 %%Korollar |
81 \setlength{\rightmargin}{0Pc} |
83 %\newenvironment{myKorollar}{ |
82 \setlength{\leftmargin}{4Pc} |
84 % \begin{list}{\textsc{\textbf{Korollar: }}}{ |
83 \setlength{\parsep}{0ex plus 0.5ex} |
85 % \setlength{\labelwidth}{8Pc} |
84 \setlength{\listparindent}{1em} |
86 % \setlength{\labelsep}{0.5Pc} |
85 \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
87 % \setlength{\rightmargin}{0Pc} |
86 \setlength{\topsep}{0.5Pc} |
88 % \setlength{\leftmargin}{4Pc} |
87 }} |
89 % \setlength{\parsep}{0ex plus 0.5ex} |
88 {\end{list} |
90 % \setlength{\listparindent}{1em} |
89 } |
91 % \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
90 |
92 % \setlength{\topsep}{0.5Pc} |
91 %Theorem |
93 % }} |
92 \newenvironment{myTheorem}{ |
94 % {\end{list} |
93 \begin{list}{\textsc{\textbf{Theorem: }}}{ |
95 %} |
94 \setlength{\labelwidth}{8Pc} |
96 % |
95 \setlength{\labelsep}{0.5Pc} |
97 %%Theorem |
96 \setlength{\rightmargin}{0Pc} |
98 %\newenvironment{myTheorem}{ |
97 \setlength{\leftmargin}{5Pc} |
99 % \begin{list}{\textsc{\textbf{Theorem: }}}{ |
98 \setlength{\parsep}{0ex plus 0.5ex} |
100 % \setlength{\labelwidth}{8Pc} |
99 \setlength{\listparindent}{1em} |
101 % \setlength{\labelsep}{0.5Pc} |
100 \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
102 % \setlength{\rightmargin}{0Pc} |
101 \setlength{\topsep}{0.5Pc} |
103 % \setlength{\leftmargin}{5Pc} |
102 }} |
104 % \setlength{\parsep}{0ex plus 0.5ex} |
103 {\end{list} |
105 % \setlength{\listparindent}{1em} |
104 } |
106 % \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
105 |
107 % \setlength{\topsep}{0.5Pc} |
106 |
108 % }} |
107 %Proportion |
109 % {\end{list} |
108 \newenvironment{myProp}{ |
110 %} |
109 \begin{list}{\textsc{\textbf{Proportion: }}}{ |
111 % |
110 \setlength{\labelwidth}{8Pc} |
112 % |
111 \setlength{\labelsep}{0.5Pc} |
113 %%Proportion |
112 \setlength{\rightmargin}{0Pc} |
114 %\newenvironment{myProp}{ |
113 \setlength{\leftmargin}{4Pc} |
115 % \begin{list}{\textsc{\textbf{Proportion: }}}{ |
114 \setlength{\parsep}{0ex plus 0.5ex} |
116 % \setlength{\labelwidth}{8Pc} |
115 \setlength{\listparindent}{1em} |
117 % \setlength{\labelsep}{0.5Pc} |
116 \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
118 % \setlength{\rightmargin}{0Pc} |
117 \setlength{\topsep}{0.5Pc} |
119 % \setlength{\leftmargin}{4Pc} |
118 }} |
120 % \setlength{\parsep}{0ex plus 0.5ex} |
119 {\end{list} |
121 % \setlength{\listparindent}{1em} |
120 } |
122 % \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex} |
121 |
123 % \setlength{\topsep}{0.5Pc} |
122 %Farben |
124 % }} |
123 |
125 % {\end{list} |
124 \newcommand{\red}[1]{\textcolor[rgb]{0.7,0,0}{\bf #1}} |
126 %} |
125 \newcommand{\rd}[1]{\color{red}{#1}} |
127 % |
126 \newcommand{\white}[1]{\textcolor[rgb]{1,0,0}{\bf #1}} |
128 %%Farben |
127 \newcommand{\w}[1]{\color{white}{#1}} |
129 % |
128 \newcommand{\g}[1]{\color{myColor}{#1}} |
130 %\newcommand{\red}[1]{\textcolor[rgb]{0.7,0,0}{\bf #1}} |
129 |
131 %\newcommand{\rd}[1]{\color{red}{#1}} |
130 \usepackage{color} |
132 %\newcommand{\white}[1]{\textcolor[rgb]{1,0,0}{\bf #1}} |
131 \definecolor{myColor}{rgb}{0.9,0.9,0.9}% Wir definieren im RGB-Farbraum |
133 %\newcommand{\w}[1]{\color{white}{#1}} |
132 |
134 %\newcommand{\g}[1]{\color{myColor}{#1}} |
133 |
135 % |
134 \newcommand{\myDef}[1]{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\w .}\\[-0.2cm]\textbf{Definition\ \Nummer:}\\#1}} |
136 %\usepackage{color} |
135 \newcommand{\mySatz}[2]{\colorbox{myColor}{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\g .}\\[-0.2cm]\textbf{Satz\ \Nummer:}\ #1\\ #2}}} |
137 %\definecolor{myColor}{rgb}{0.9,0.9,0.9}% Wir definieren im RGB-Farbraum |
136 \newcommand{\myBeweis}[1]{\textit{\textbf{Beweis:}\\ #1}} |
138 % |
137 \newcommand{\myAlg}[2]{\parbox{\columnwidth}{\addtocounter{ctr}{1}\textbf{Algorithmus\ \Nummer:}\ \ #1\\#2}} |
139 % |
138 \newcommand{\myProg}[1]{\fbox{\parbox{\columnwidth}{#1}}} |
140 %\newcommand{\myDef}[1]{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\w .}\\[-0.2cm]\textbf{Definition\ \Nummer:}\\#1}} |
139 |
141 %\newcommand{\mySatz}[2]{\colorbox{myColor}{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\g .}\\[-0.2cm]\textbf{Satz\ \Nummer:}\ #1\\ #2}}} |
140 \newcommand{\add}[1]{\addtocounter{#1}{1}} |
142 %\newcommand{\myBeweis}[1]{\textit{\textbf{Beweis:}\\ #1}} |
141 \newcommand{\zahl}[1]{\setcounter{#1}{Z}} |
143 %\newcommand{\myAlg}[2]{\parbox{\columnwidth}{\addtocounter{ctr}{1}\textbf{Algorithmus\ \Nummer:}\ \ #1\\#2}} |
142 \newcommand{\Q}[2]{\parbox{\columnwidth}{$^{[\arabic{#1}/#2]}$ }} |
144 %\newcommand{\myProg}[1]{\fbox{\parbox{\columnwidth}{#1}}} |
143 |
145 % |
144 \newcommand{\Nummer}{\thesection.\arabic{ctr}} |
146 %\newcommand{\add}[1]{\addtocounter{#1}{1}} |
145 |
147 %\newcommand{\zahl}[1]{\setcounter{#1}{Z}} |
|
148 %\newcommand{\Q}[2]{\parbox{\columnwidth}{$^{[\arabic{#1}/#2]}$ }} |
|
149 % |
|
150 %\newcommand{\Nummer}{\thesection.\arabic{ctr}} |
|
151 % |
146 %---------- --------------------------------------------------- Beginn ----------------------------------------------------------------------- |
152 %---------- --------------------------------------------------- Beginn ----------------------------------------------------------------------- |
147 |
153 |
148 \title{Greatest common divisor \\ for multi variable Polynomials} |
154 \title{Greatest Common Divisor \\ for Multivariate Polynomials} |
149 \author{By\\Diana Meindl\\meindl$_-$diana@yahoo.com} |
155 \author{Diana Meindl\\meindl\_diana@yahoo.com} |
150 \date{} |
156 \date{\today} |
151 |
157 |
152 \begin{document} |
158 \begin{document} |
153 \maketitle |
159 \maketitle |
154 {\w .}\\[12cm] |
160 %{\w .}\\[12cm] |
155 \begin{center} |
161 %\begin{center} |
156 Presented to \\ |
162 %Presented to \\ |
157 A.Univ.Prof. Dipl.-Ing. Dr. Wolfgang Schreiner (RISC Insitute)\\ |
163 %A.Univ.Prof. Dipl.-Ing. Dr. Wolfgang Schreiner (RISC Insitute)\\ |
158 and\\ |
164 %and\\ |
159 Dr. techn. Walther Neuper (Institut für Softwaretechnologie, TU Graz) |
165 %Dr. techn. Walther Neuper (Institut für Softwaretechnologie, TU Graz) |
160 \end{center} |
166 %\end{center} |
|
167 %\newpage |
|
168 %{\w .}\hspace{6.5cm}\textbf{Abstact}\\[0.5cm] |
|
169 |
|
170 \abstract{ |
|
171 This is a proposal for a Masters Thesis at RISC, the Research Institute for Symbolic Computation at Linz University.\\ |
|
172 |
|
173 Calculation with fractions is an important part of Computer Algebra Systems (CAS). This proposal aims at a specific part of such calculations, the greatest common divisor (GCD) used for cancellation, but in the very general context of multivariate polynomials. Cancellation of multivariate polynomials is a settled topic in Computer Algebra, respective algorithms well documented and implementations available in all CASs. |
|
174 |
|
175 This proposal claims for novelty with respect to the context of implementation in Computer Theorem Proving (CTP). On CTP's present development towards industrial use in software and systems verification, specific domain models involve demand on more and more mathematics, and within mathematics involve demand for more and more features. The proposed implementation of GCD and cancellation follows an actual demand. |
|
176 |
|
177 If the implementation is successful, it might be included into the distribution of Isabelle, one of the two dominating CTPs in Europe. |
|
178 } |
|
179 |
161 \newpage |
180 \newpage |
162 {\w .}\hspace{6.5cm}\textbf{Abstract}\\[0.5cm] |
181 %WN vorerst zu Zwecken der "Ubersicht lassen ... |
163 Calculation with fractions is an important part of Computer-Algebra-Systems (CAS). Therefor you need algorithms for canceling fractions, respectively for the greatest common divisor (GCD). |
182 \tableofcontents |
|
183 |
164 \section{Background} |
184 \section{Background} |
165 The ISAC-project is a research and development project at the Institute for Software Technology of the Graz University of Technology. It is an educational mathematics assistant, a single-stepping system for applied mathematics based on the computer theorem prover Isabelle. The special is an easy readable knowledge base including Isabelles HOL-theories and a transparently working knowledge interpreter (a generalization of 'single stepping' algebra systems). |
185 The \sisac-project is a research and development project at the Institute for Software Technology of the Graz University of Technology. It is an educational mathematics assistant, a single-stepping system for applied mathematics based on the computer theorem prover Isabelle. The special is an easy readable knowledge base including Isabelles HOL-theories and a transparently working knowledge interpreter (a generalization of 'single stepping' algebra systems). |
166 The background to both, development and research, is given by actual needs in math education as well as by fundamental questions about 'the mechanization of thinking' as an essential aspect in mathematics and in technology. |
186 The background to both, development and research, is given by actual needs in math education as well as by foundamental questions about 'the mechanization of thinking' as an essential aspect in mathematics and in technology. |
167 The ISAC-system under construction comprises a tutoring-system and an authoring-system. The latter provides for adaption to various needs of individual users and educational institutions and for extensions to arbitrary fields of applied mathematics. |
187 The \sisac-system under construction comprises a tutoring-system and an authoring-system. The latter provides for adaption to various needs of individual users and educational institutions and for extensions to arbitrary fields of applied mathematics. |
168 |
188 |
|
189 TODO:\\ |
|
190 European provers: Isabelle \cite{Nipkow-Paulson-Wenzel:2002}, Coq \cite{Huet_all:94}\\ |
|
191 American provers: PVS~\cite{pvs}, ACL2~\footnote{http://userweb.cs.utexas.edu/~moore/acl2/}\\ |
|
192 |
169 \section{Goal of the thesis} |
193 \section{Goal of the thesis} |
170 \subsection{Current situation} |
194 \subsection{Current situation} |
171 At the time there is no good implementation for the problem of canceling fractions in Isac and or in Isabelle. But because canceling is important for calculating with fractions a new implementation is necessary. |
195 At the time there is no good implimentation for the problem of canceling fractions in \sisac and or in Isabelle. But because canceling is important for calculating with fractions a new implimentation is necessary. |
172 |
196 |
173 \subsection{Problem} |
197 \subsection{Problem} |
174 The wish is to handle fractions in Isac not only in one variable also in more. So the goal of this thesis is to find, assess and evaluate the existing algorithms and methods for finding the GCD. This will be an functional program with the possibility to include it into Isabelle. |
198 The wish is to handle fractions in \sisac not only in one variable also in more. So the goal of this thesis ist to find, assess and evaluate the existing algorithms and methods for finding the GCD. This will be an functional programm with the posibility to include it into Isabelle. |
|
199 |
|
200 %WN eine pr"azisere Beschreibung des Problems kann ich mir nicht vorstellen (englische Version der Mail haben wir auch, aber sie passt nicht zur deutschen Antwort von Prof.Nipkow) ... |
|
201 \bigskip |
|
202 TODO Mail to Prof. Nipkow, leader of the development of Isabelle \cite{Nipkow-Paulson-Wenzel:2002} at TU M\"unchen, Mon, 23 May 2011 08:58:14 +0200: |
|
203 \begin{verbatim} |
|
204 Eine erste Idee, wie die Integration der Diplomarbeit f"ur |
|
205 einen Benutzer von Isabelle aussehen k"onnte, w"are zum |
|
206 Beispiel im |
|
207 |
|
208 lemma cancel: |
|
209 assumes asm3: "x2 - x*y \<noteq> 0" and asm4: "x \<noteq> 0" |
|
210 shows "(x2 - y2) / (x2 - x*y) = (x + y) / (x::real)" |
|
211 apply (insert asm3 asm4) |
|
212 apply simp |
|
213 sorry |
|
214 |
|
215 die Assumptions |
|
216 |
|
217 asm1: "(x2 - y2) = (x + y) * (x - y)" and asm2: "x2 - x*y = x * (x - y)" |
|
218 |
|
219 im Hintergrund automatisch zu erzeugen (mit der Garantie, |
|
220 dass "(x - y)" der GCD ist) und sie dem Simplifier (f"ur die |
|
221 Rule nonzero_mult_divide_mult_cancel_right) zur Verf"ugung zu |
|
222 stellen, sodass anstelle von "sorry" einfach "done" stehen kann. |
|
223 Und weiters w"are eventuell asm3 zu "x - y \<noteq> 0" zu vereinfachen, |
|
224 eine Rewriteorder zum Herstellen einer Normalform festzulegen, etc. |
|
225 \end{verbatim} |
|
226 %WN und eine bessere Motivation f"ur eine Master Thesis kann ich mir auch nicht vorstellen ... |
|
227 Response of Prof. Nipkow: |
|
228 |
|
229 \begin{verbatim} |
|
230 Unser Spezialist fuer die mathematischen Theorien ist Johannes H"olzl. |
|
231 Etwas allgemeinere Fragen sollten auf jeden Fall an isabelle-dev@ |
|
232 gestellt werden. |
|
233 |
|
234 Viel Erfolg bei der Arbeit! |
|
235 Tobias Nipkow |
|
236 \end{verbatim} |
|
237 |
|
238 |
175 \subsection{Expected results} |
239 \subsection{Expected results} |
176 Find good algorithms for the different problems, and find out which one will be the best for the special problem.\\ |
240 Find good algorithms for the different problems, and find out which one will be the best for the special problem.\\ |
177 The program should handling: |
241 The program should handling: |
178 \begin{itemize} |
242 \begin{itemize} |
179 \item[]real and rational coefficients. Maybe also imaginary coefficients. |
243 \item[]real and rational coefficients. Maybe also imaginary coefficients. |
180 \item[]Multi variable polynomials canceling and adding, when they are in normal form. |
244 \item[]Multi variable polynomials canceling and adding, when they are in normal form. |
181 \end{itemize} |
245 \end{itemize} |
182 For the program should be used a functional programing language with good commentaries. And it should be based on Isabelle and works correctly in Isac. |
246 For the program should be used a functional programming language with good commentaries. And it should be based on Isabelle and works correctly in \sisac. |
183 \newpage |
|
184 |
247 |
185 \section{State of the art} |
248 \section{State of the art} |
186 Was ist vorhanden, was kann ich aus welchen Büchern für meine Arbeit verwenden |
249 In a broad view the context of this thesis can be seen as ``computation and deduction'': simplification and in particular cancellation of rational terms is concern of \textbf{computation} implemented in Computer Algebra Systems (CAS) --- whereas the novelty within the thesis is given by an implementation of cancellation in a computer theorem prover (CTP), i.e. in the domain of \textbf{deduction} with respective logical rigor not addressed in the realm of CAS. |
187 Es gibt verschiedene CAS die bereits einen Algrotihmus implimentiert haben, wie haben die das gemacht, und welcher ist für mich am besten. |
250 |
188 |
251 Below, after a general survey on computation, represented by CAS, and on deduction, represented by CTP, a more narrow view on ``CAS-functionality in CTP'' is pursued. |
189 \newpage |
252 |
|
253 \subsection{Computer Algebra and Proof Assistants} |
|
254 %WN achtung: diese subsection is fast w"ortlich kopiert aus \cite{plmms10} -- also in der Endfassung bitte "uberarbeiten !!! |
|
255 Computer Algebra and Proof Assistants have coexisted for a many years so there is much research trying to bridge the gap between these approaches from both sides. We shall continue to abbreviate Computer Algebra (Systems) by ``CAS'', and in analogy we shall abbreviate proof assistants by CTP, computer theorem provig (comprising both, interactive theorem proving (ITP) and automated theorem proving (ATP), since in CTP there are ATP-tools included today.) |
|
256 |
|
257 First, many CTPs already have CAS-like functionality, |
|
258 especially for domains like arithmetic. They provide the user |
|
259 with conversions, tactics or decision procedures that solve |
|
260 problems in a particular domain. Such decision procedures present |
|
261 in the standard library of HOL Light~\footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} are used inside the |
|
262 prototype described in Sect.\ref{cas-funct} on p.\pageref{part-cond} for arithmetic's, |
|
263 symbolic differentiation and others. |
|
264 |
|
265 Similarly some CAS systems provide environments that allow |
|
266 logical reasoning and proving properties within the system. Such |
|
267 environments are provided either as logical |
|
268 extensions (e.g.~\cite{logicalaxiom}) or are implemented within a |
|
269 CAS using its language~\cite{theorema00}. |
|
270 |
|
271 There are numerous architectures for information exchange between |
|
272 CAS and CTP with different levels of \emph{degree of trust} |
|
273 between the prover and the CAS. In principle, there are several approaches. |
|
274 If CAS-functionality is not fully embedded in CTP, CAS can be called as ``oracles'' nevertheless (for efficiency reasons, in general) --- their results are regarded like prophecies of Pythia in Delphi. There are three kinds of checking oracles, however: |
|
275 \begin{enumerate} |
|
276 \item Just adopt the CAS result without any check. Isabelle internally marks such results. |
|
277 \item Check the result inside CTP. There are many cases, where such checks are straight forward, for instance, checking the result of factorization by multiplication of the factors, or checking integrals by differentiation. |
|
278 \item Generate a derivation of the result within CTP; in Isabelle this is called ``proof reconstruction''. |
|
279 \end{enumerate} |
|
280 A longer list of frameworks for |
|
281 information exchange and bridges between systems can be found |
|
282 in~\cite{casproto}. |
|
283 |
|
284 There are many approaches to defining partial functions in proof |
|
285 assistants. Since we would like the user to define functions |
|
286 without being exposed to the underlying logic of the proof |
|
287 assistant we only mention some automated mechanisms for defining |
|
288 partial functions in the logic of a CTP. |
|
289 Krauss~\cite{krauss} has developed a framework for defining |
|
290 partial recursive functions in Isabelle/HOL, which formally |
|
291 proves termination by searching for lexicographic combinations of |
|
292 size measures. Farmer~\cite{farmer} implements a scheme for |
|
293 defining partial recursive functions in \textrm{IMPS}. |
|
294 |
|
295 \subsection{Motivation for CAS-functionality in CTP} |
|
296 In the realm of CTP formuas are dominated by quantifiers $\forall$, $\exists$ and $\epsilon$ (such) and by operations like $\Rightarrow$, $\land$ and $\lor$. Numbers were strangers initially; numerals have been introduced to Isabelle not much before the year 2000~\footnote{In directory src/Provers/Arith/ see the files cancel\_numerals.ML and cancel\_numeral\_factor.ML in the Isabelle distribution 2011. They still use the notation $\#1,\#2,\#3,\dots$ from before 2000~!}. However, then numerals have been implemented with {\em polymorphic type} such that $2\cdot r\cdot\pi$ ($2$ is type \textit{real}) and $\pi_{\it approx}=3.14\,\land\, 2\cdot r\cdot\pi_{\it approx}$ can be written as well as $\sum_i^n i=\frac{n\cdot(n+1)}{2}$ ($2$ is type \textit{nat}). The different types are inferred by Hindle-Milner type inference \cite{damas-milner-82,Milner-78,Hindley-69}. |
|
297 |
|
298 1994 was an important year for CTP: the Pentium Bug caused excitement in the IT community all around the world and motivated INTEL to invest greatly into formal verification of circuits (which carried over to verification of software). Not much later John Harrison mechanized real numbers as Dedekind Cuts in HOL Light \footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} and derived calculus, derivative and integral from that definition \cite{harr:thesis}, an implementation which has been transferred to Isabelle very soon after that~\footnote{In the directory src/HOL/Multivariate\_Analysis/ see the files Gauge\_Measure.thy, Integration.thy, Derivative.thy, Real\_Integration.thy, Brouwer\_Fixpoint.thy, Fashoda.thy}. |
|
299 |
|
300 Harrison also says that ``CAS are ill-defined'' and gives, among others, an example relevant for this thesis on cancellation: TODO ... meromorphic functions ... |
|
301 |
|
302 \medskip |
|
303 The main motivation for further introduction of CAS-functionality to CTP is also technology-driven: In this decade domain engineering is becoming an academic discipline with industrial relevance \cite{db:dom-eng}: vigorous efforts extend the scope of formal specifications even beyond software technology, and thus respective domains of mathematical knowledge are being mechanized in CTP. The Archive of Formal Proofs~\footnote{http://afp.sourceforge.net/} is Isabelle's repository for such work. |
|
304 |
|
305 \subsection{Simplification within CTP} |
|
306 Cancellation, the topic of this thesis, is a specific part of simplification of rationals. In the realm of CAS cancellation is {\em not} an interesting part of the state of the art, because cancellation has been implemented in the prevailing CAS more than thirty years ago --- however, cancellation of multivariate polynomials is {\em not} yet implemted in any of the dominating CTPs. |
|
307 %WN: bitte mit Anfragen an die Mailing-Listen nachpr"ufen: Coq, HOL, ACL2, PVS |
|
308 |
|
309 As in other CTPs, in Isabelle the simplifier is a powerful software component; the sets of rewrite rules, called \textit{simpsets}, contain several hundreds of elements. Rewriting is still very efficient, because the simpsets are transformed to term nets \cite{term-nets}. |
|
310 |
|
311 Rational terms of multivariate polynomials still have a normal form \cite{bb-loos} and thus equivalence of respective terms is decidable. This is not the case, however, with terms containing roots or transcedent functions. Thus, CAS are unreliable by design in these cases. |
|
312 |
|
313 In CTP, simplification of non-decidable domains is already an issue, as can be seem in the mail with subject ``simproc divide\_cancel\_factor produces error'' in the mailing-list \textit{isabelle-dev@mailbroy.informatik.tu-muenchen.de} from Thu, 15 Sep 2011 16:34:12 +0200 |
|
314 {%\footnotesize --- HILFT NICHTS |
|
315 \begin{verbatim} |
|
316 Hi everyone, |
|
317 |
|
318 in the following snippet, applying the simplifier causes an error: |
|
319 |
|
320 ------------------------------------------ |
|
321 theory Scratch |
|
322 imports Complex_Main |
|
323 begin |
|
324 |
|
325 lemma |
|
326 shows "(3 / 2) * ln n = ((6 * k * ln n) / n) * ((1 / 2 * n / k) / 2)" |
|
327 apply simp |
|
328 ------------------------------------------ |
|
329 |
|
330 outputs |
|
331 |
|
332 ------------------------------------------ |
|
333 Proof failed. |
|
334 (if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) = |
|
335 2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k)) |
|
336 1. n \not= Numeral0 \rightarrow k * (ln n * (2 * 6)) / (k * 4) = k * (ln n * 12) / (k * 4) |
|
337 1 unsolved goal(s)! |
|
338 The error(s) above occurred for the goal statement: |
|
339 (if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) = |
|
340 2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k)) |
|
341 ------------------------------------------ |
|
342 \end{verbatim} |
|
343 } |
|
344 Mail ``Re: simproc divide\_cancel\_factor produces error'' on Fri, 16 Sep 2011 22:33:36 +0200 |
|
345 \begin{verbatim} |
|
346 > > After the release, I'll have to think about doing a complete overhaul |
|
347 > > of all of the cancellation simprocs. |
|
348 You are very welcome to do so. Before you start, call on me and I will |
|
349 write down some ideas I had long ago (other may want to join, too). |
|
350 \end{verbatim} |
|
351 %WN: bist du schon angemeldet in den Mailing-Listen isabelle-users@ und isabelle-dev@ ? WENN NICHT, DANN WIRD ES H"OCHSTE ZEIT !!! |
|
352 |
|
353 \subsection{Open Issues with CAS-functionality in CTP}\label{cas-funct} |
|
354 There is at least one effort explicitly dedicated to implement CAS-functionality in CTP \cite{cezary-phd}. %WN bitte unbedingt lesen (kann von mir in Papierform ausgeborgt werden) !!! |
|
355 In this work three issues has been identified: partiality conditions, multi-valued functions and real numbers. These issues are addressed in the subsequent paragraphs, followed by a forth issue raised by \sisac. |
|
356 |
|
357 \paragraph{Partiality conditions}\label{part-cond} are introduced by partial functions or by conditional rewriting. An example of how the CAS-functionality \cite{cezary-phd} looks like is given on p.\pageref{fig:casproto}. |
|
358 \cite{cezary-phd} gives an introductory example (floated to p.\pageref{fig:casproto}) which will be referred to in the sequel. |
|
359 \input{thol.tex} |
|
360 %WN das nachfolgende Format-Problem l"osen wir sp"ater ... |
|
361 \begin{figure}[hbt] |
|
362 \begin{center} |
|
363 \begin{holnb} |
|
364 In1 := vector [\&2; \&2] - vector [\&1; \&0] + vec 1 |
|
365 Out1 := vector [\&2; \&3] |
|
366 In2 := diff (diff (\Lam{}x. \&3 * sin (\&2 * x) + |
|
367 \&7 + exp (exp x))) |
|
368 Out2 := \Lam{}x. exp x pow 2 * exp (exp x) + |
|
369 exp x * exp (exp x) + -- \&12 * sin (\&2 * x) |
|
370 In3 := N (exp (\&1)) 10 |
|
371 Out3 := #2.7182818284 + ... (exp (\&1)) 10 F |
|
372 In4 := x + \&1 - x / \&1 + \&7 * (y + x) pow 2 |
|
373 Out4 := \&7 * x pow 2 + \&14 * x * y + \&7 * y pow 2 + \&1 |
|
374 In5 := sum (0,5) (\Lam{}x. \&x * \&x) |
|
375 Out5 := \&30 |
|
376 In6 := sqrt (x * x) assuming x > &1 |
|
377 Out6 := x |
|
378 \end{holnb} |
|
379 \end{center} |
|
380 \caption{\label{fig:casproto}Example interaction with the prototype |
|
381 CAS-like input-response loop. For the user input given in the |
|
382 \texttt{In} lines, the system produces the output in \texttt{Out} |
|
383 lines together with HOL Light theorems that state the equality |
|
384 between the input and the output.} |
|
385 \end{figure} |
|
386 In lines {\tt In6, Out6} this examples shows how to reliably simplify $\sqrt{x}$. \cite{caspartial} %TODO |
|
387 gives more details on handling side conditions in formalized partial functions. |
|
388 |
|
389 Analoguous to this example, cancellations (this thesis is concerned with) like |
|
390 $$\frac{x^2-y^2}{x^2-x\cdot y}=\frac{x+y}{x}\;\;\;\;{\it assuming}\;x-y\not=0\land x\not=0$$ |
|
391 produce assumptions, $x-y\not=0, x\not=0$ here. Since the code produced in the framework of this thesis will be implemented in Isabelle's simplifier (outside this thesis), the presentation to the user will be determined by Isabelle and \sisac{} using the respective component of Isabelle. Also reliable handling of assumptions like $x-y\not=0, x\not=0$ is up to these systems. |
|
392 |
|
393 \paragraph{Multi-valued functions:}\label{multi-valued} |
|
394 \cite{seeingroots,davenp-multival-10} discuss cases where CAS are error prone when dropping a branch of a multi-valued function~\footnote{``Multivalued \textit{function}'' is a misnomer, since the value of a function applied to a certain argument is unique by definition of function.}. Familiar examples are ... |
|
395 %WN ... zur Erkl"arung ein paar Beispiele von http://en.wikipedia.org/wiki/Multivalued_function |
|
396 |
|
397 \paragraph{Real numbers} cannot be represented by numerals. In engineering applications, however, approximation by floating-point numbers are frequently useful. In CTP floating-point numbers must be handled rigorously as approximations. Already \cite{harr:thesis} introduced operations on real numerals accompanied by rigorous calculation of precision. \cite{russellphd} describes efficient implementation of infinite precision real numbers in Coq. |
|
398 |
|
399 \paragraph{All solutions for equations} must be guaranted, if equation solving is embedded within CTP. So, given an equation $f(x)=0$ and the set of solutions $S$ of this equation, we want to have both, |
|
400 \begin{eqnarray} |
|
401 \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut} |
|
402 x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0 \label{all-solut} |
|
403 \end{eqnarray} |
|
404 \end{eqnarray} |
|
405 where (\ref{all-solut}) ensures that $S$ contains {\em all} solutions of the equation. The \sisac-project has implemented a prototype of an equation solver~\footnote{See \textit{equations} in the hierarchy of specifications at http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}. |
|
406 |
|
407 There is demand for fullfledged equation solving in CTP, including equational systems and differential equations, because \sisac{} has a prototype of a CTP-based programming language calling CAS functions; and Lucas-Interpretation \cite{wn:lucas-interp-12} makes these functions accessible by single-stepping and ``next step guidance'', which would automatically generate a learning system for equation solving. |
|
408 |
190 \section{Thesis structure} |
409 \section{Thesis structure} |
191 The proposed table of contents of the thesis on the chapter level is as follows: |
410 The proposed table of contents of the thesis on the chapter level is as follows: |
192 \begin{enumerate} |
411 \begin{enumerate} |
193 \item Introduction (2-3 pages) |
412 \item Introduction (2-3 pages) |
194 \item Computer Algebra Systems (CAS) (5 - 7 pages)\\ |
413 \item Computer Algebra Systems (CAS) (5 - 7 pages)\\ |
195 Which different CAS exists and whats the focus of them. |
414 Which different CAS exists and whats the focus of them. |
196 \item The \textit{ISAC}-Project (5 - 7 pages)\\ |
415 \item The \sisac-Project (5 - 7 pages)\\ |
197 This chapter will describe the \textit{ISAC}-Project and the goals of the project. |
416 This chapter will describe the \sisac-Project and the goals of the project. |
198 \item Univariate Polynomials (15-20 pages)\\ |
417 \item Univariate Polynomials (15-20 pages)\\ |
199 This chapter will describe different Algorithms for univariate polynomials, with different coefficients. |
418 This chapter will describe different Algorithms for univariate polynomials, with different coefficients. |
200 \item Multivariate Polynomials (20-25 pages)\\ |
419 \item Multivariate Polynomials (20-25 pages)\\ |
201 This chapter will describe different Algorithms for multivariate polynomials, with different coefficients |
420 This chapter will describe different Algorithms for multivariate polynomials, with different coefficients |
202 \item Functional programing and SML(2-5 pages)\\ |
421 \item Functional programming and SML(2-5 pages)\\ |
203 The basic idea of this programing languages. |
422 The basic idea of this programming languages. |
204 \item Implementation in \textit{ISAC}-Project (15-20 pages) |
423 \item Implimentation in \sisac-Project (15-20 pages) |
205 \item Conclusion (2-3 pages) |
424 \item Conclusion (2-3 pages) |
206 \end{enumerate} |
425 \end{enumerate} |
207 %\newpage |
426 %\newpage |
208 |
427 |
209 \section{Time line} |
428 \section{Timeline} |
210 %Werd nie fertig.\\ |
429 %Werd nie fertig.\\ |
211 \begin{center} |
430 \begin{center} |
212 \begin{tabular}{|l|l|l|} |
431 \begin{tabular}{|l|l|l|} |
213 \hline |
432 \hline |
214 \textbf{Time}&\textbf{Thesis}&\textbf{Project}\\ |
433 \textbf{Time}&\textbf{Thesis}&\textbf{Project}\\ |
215 \hline |
434 \hline |
216 & Functional programing & Learning the basics and the idea\\ |
435 & Functional programming & Learning the basics and the idea\\ |
217 & & of functional programing\\ |
436 & & of funcional programming\\ |
218 \hline |
437 \hline |
219 & Different CAS & Can they handle the problem \\ |
438 & Different CAS & Can they handle the problem \\ |
220 & &and which algorithm do they use?\\ \hline |
439 & &and which algorithm do they use?\\ \hline |
221 & Univariate Polynomials & Implementation of the Algorithm\\ |
440 & Univariate Polynomials & Implementation of the Algorithm\\ |
222 & & for univariate Polynomials \\ \hline |
441 & & for univariate Polynomials \\ \hline |
223 & Multivariate Polynomials & Implementation of the Algorithm\\ |
442 & Multivariate Polynomials & Implementation of the Algorithm\\ |
224 & & for multivariate Polynomials \\ \hline |
443 & & for multivariate Polynomials \\ \hline |
225 & The Isac-Project &\\ \hline |
444 & The \sisac-Project &\\ \hline |
226 & Conclusion and Introduction & Find good examples for testing\\ |
445 & Conclusion and Introduction & Find good examples for testing\\ |
227 \hline |
446 \hline |
228 \end{tabular} |
447 \end{tabular} |
229 \end{center} |
448 \end{center} |
230 |
449 |
231 \newpage |
450 %WN oben an passender stelle einf"ugen |
|
451 \cite{einf-funct-progr} \cite{Winkler:96} |
232 |
452 |
233 \section{Bibliography} |
453 |
234 %mindestens 10 |
454 \bibliography{references} |
235 \begin{enumerate} |
455 %\section{Bibliography} |
236 \item Bird/Wadler, \textit{Einführung in die funktionale Programmierung}, Carl Hanser and Prentice-Hall International, 1992 |
456 %%mindestens 10 |
237 \item Franz Winkler, \textit{Polynomial Algorithms in Computer Algebra}, Springer,1996 |
457 %\begin{enumerate} |
238 \item %M. Mignotte, \textit{An inequality about factors of polynomial} |
458 % \item Bird/Wadler, \textit{Einführung in die funktionale Programmierung}, Carl Hanser and Prentice-Hall International, 1992 |
239 \item %M. Mignotte, \textit{Some useful bounds} |
459 % \item Franz Winkler, \textit{Polynomial Algorithms in Computer Algebra}, Springer,1996 |
240 \item %W. S. Brown and J. F. Traub. \textit{On euclid's algorithm and the theory of subresultans}, Journal of the ACM (JACM), 1971 |
460 % \item %M. Mignotte, \textit{An inequality about factors of polynomial} |
241 \item %Bruno Buchberger, \textit{Algorhimic mathematics: Problem types, data types, algorithm types}, Lecture notes, RISC Jku A-4040 Linz, 1982 |
461 % \item %M. Mignotte, \textit{Some useful bounds} |
242 |
462 % \item %W. S. Brown and J. F. Traub. \textit{On euclid's algorithm and the theory of subresultans}, Journal of the ACM (JACM), 1971 |
243 \item %Tateaki Sasaki and Masayuki Suzuki, \textit{Thre new algorithms for multivariate polynomial GCD}, J. Symbolic Combutation, 1992 |
463 % \item %Bruno Buchberger, \textit{Algorhimic mathematics: Problem types, data types, algorithm types}, Lecture notes, RISC Jku A-4040 Linz, 1982 |
244 \item |
464 % |
245 \item |
465 % \item %Tateaki Sasaki and Masayuki Suzuki, \textit{Thre new algorithms for multivariate polynomial GCD}, J. Symbolic Combutation, 1992 |
246 \item |
466 % \item |
247 \end{enumerate} |
467 % \item |
|
468 % \item |
|
469 %\end{enumerate} |
248 |
470 |
249 \end{document} |
471 \end{document} |
|
472 |
|
473 WN110916 grep-ing through Isabelle code: |
|
474 |
|
475 neuper@neuper:/usr/local/isabisac/src$ find -name "*umeral*" |
|
476 ./HOL/ex/Numeral.thy |
|
477 ./HOL/Tools/nat_numeral_simprocs.ML |
|
478 ./HOL/Tools/numeral_syntax.ML |
|
479 ./HOL/Tools/numeral.ML |
|
480 ./HOL/Tools/numeral_simprocs.ML |
|
481 ./HOL/Matrix/ComputeNumeral.thy |
|
482 ./HOL/Library/Numeral_Type.thy |
|
483 ./HOL/Numeral_Simprocs.thy |
|
484 ./HOL/Import/HOL/numeral.imp |
|
485 ./HOL/Code_Numeral.thy |
|
486 ./HOL/Nat_Numeral.thy |
|
487 ./ZF/Tools/numeral_syntax.ML |
|
488 ./Provers/Arith/cancel_numeral_factor.ML |
|
489 ./Provers/Arith/cancel_numerals.ML |
|
490 ./Provers/Arith/combine_numerals.ML |
|
491 |
|
492 neuper@neuper:/usr/local/isabisac/src$ find -name "*ancel*" |
|
493 ./HOL/Tools/abel_cancel.ML |
|
494 ./Provers/Arith/cancel_div_mod.ML |
|
495 ./Provers/Arith/cancel_numeral_factor.ML Paulson 2000 !!! |
|
496 ./Provers/Arith/cancel_sums.ML |
|
497 ./Provers/Arith/cancel_numerals.ML Paulson 2000 |