diff --git a/books/bookvol6.pamphlet b/books/bookvol6.pamphlet index 5d1fb99..aeb08fd 100644 --- a/books/bookvol6.pamphlet +++ b/books/bookvol6.pamphlet @@ -7126,6 +7126,71 @@ WildFunctionFieldIntegralBasis XExponentialPackage ZeroDimensionalSolvePackage @ +\chapter{Research Topics} +These are included here as ideas that may get expanded in more detail later. +\section{Proofs} +The goal would be to prove that Axiom's algorithms are correct. + +For instance, show that the GCD algorithm is correct. This involves several +levels of proof. At one level we need to prove that the GCD algorithm is +mathematically correct and that it terminates. This can be picked up from +the literature. + +A second level of correctness involves proving that the implementation of +the algorithm is correct. This involves using something like ACL2 [KMJ00] +and proof of the common lisp implementation. + +A third level is to show that the binary implementation conforms to the +semantics of the common lisp implementation. This involves using something +like Function Extraction (FX) [LMW79] to extract the machine-level behavior of +the program and comparing it to the specification. + +\section{Indefinites} +There are times when it would be convenient to write algorithms in terms +of indefinite values. For instance, we would like to be able to declare +that X and Y are matrices and compute X*Y symbolically. We would like to +be able to do the same with arbitrary integers, I and J. In general, for +a given domain we would like to create domain elements that are not fully +specified but have the computation proceed with these ``indefinite'' values. +\section{Provisos} +We would like to create ``provisos'' on statements such as: +\[\frac{1}{x} {\rm\ provided\ } x \ne 0\] + +We would then like to rewrite this in terms of intervals to create three +``continuations'' where each continuation is a separate domain of computation +(and could thus be computed in parallel). So for the above example we would +generate: +\[\frac{1}{x} {\rm\ such\ that\ } x \in [-\infty,0)\] +\[\frac{1}{x} {\rm\ such\ that\ } x \in (0,0)\] +\[\frac{1}{x} {\rm\ such\ that\ } x \in (0,\infty]\] + +When a new proviso is added, for instance, when we divide by y then there +would be further subdivision of the computation, forming a tree: +\[\frac{1}{xy} {\rm\ such\ that\ } x \in [-\infty,0) + {\rm\ and\ } y \in [-\infty,0)\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in (0,0) + {\rm\ and\ } y \in [-\infty,0)\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in (0,\infty] + {\rm\ and\ } y \in [-\infty,0)\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in [-\infty,0) + {\rm\ and\ } y \in (0,0)\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in (0,0) + {\rm\ and\ } y \in (0,0)\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in (0,\infty] + {\rm\ and\ } y \in (0,0)\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in [-\infty,0) + {\rm\ and\ } y \in (0,\infty]\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in (0,0) + {\rm\ and\ } y \in (0,\infty]\] +\[\frac{1}{xy} {\rm\ such\ that\ } x \in (0,\infty] + {\rm\ and\ } y \in (0,\infty]\] + +Interesting questions arise, such has how to recover the function over +the real line. Of course, the domain and range are not restricted to the +real line in general but could, for instance, range over the complex plane. + +Note that the provisos need not be an interval. They could be anything +such as a polynomial or a property like ``$f(x)$ is entire''. \chapter{Makefile} \section{Environment variables} <>= diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet index 3df6699..2c7407d 100644 --- a/books/bookvolbib.pamphlet +++ b/books/bookvolbib.pamphlet @@ -1050,6 +1050,10 @@ Dover Publications, Mineola, NY ISBN 0-486-45312-X (1981) \bibitem[Je04]{Je04} Jeffrey, Alan ``Handbook of Mathematical Formulas and Integrals'' Third Edition, Elsevier Academic Press ISBN 0-12-382256-4 +\bibitem[KMJ00]{KMJ00} +Kaufmann, Matt; Manolios, Panagiotis, and Moore J Strother +``Computer-Aided Reasoning: An Approach'' Springer, July 31. 2000 +ISBN 0792377443 \bibitem[Knu84]{Knu84} Knuth, Donald, {\it The \TeX{}book} \\ Reading, Massachusetts, Addison-Wesley Publishing Company, Inc., @@ -1071,6 +1075,10 @@ Bull. Soc. Math. France, vol. 116, 1988, pp. 231--253. Daniel Lazard and Renaud Rioboo. ``Integration of rational functions: Rational computation of the logarithmic part'' {\sl Journal of Symbolic Computation}, 9:113-116:1990 +\bibitem[LMW79]{LMW79} +Linger, Richard C.; Mills, Harlan D.; and Witt, Bernard I. +``Structured Programming: Theory and Practice'' +Addison-Wesley (March 1979) ISBN 0201144611 \bibitem[Lio1833a]{Lio1833a} Joseph Liouville. Premier m\'{e}moire sur la d\'{e}termination des int\'{e}grales dont la valeur est diff --git a/changelog b/changelog index 9286eca..46505f3 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,6 @@ +20101005 tpd src/axiom-website/patches.html 20101005.01.tpd.patch +20101005 tpd books/bookvol6 add a research ideas section +20101005 tpd books/bookvolbib add Kaufmann [KMJ00] and Linger [LMW79] 20101004 tpd src/axiom-website/patches.html 20101004.03.tpd.patch 20101004 tpd src/interp/parsing.lisp treeshake compiler 20101004 tpd books/bookvol9 treeshake compiler diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index d2db0f8..10b725f 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -3190,5 +3190,7 @@ books/bookvol9 treeshake compiler
books/bookvol9 treeshake compiler
20101004.03.tpd.patch books/bookvol9 treeshake compiler
+20101005.01.tpd.patch +books/bookvol6 add a research ideas section