Axiom now has the necessary machinery to process proofs at build time (ACL2 for Lisp, COQ for Spad). While pondering the subject I ended up reading "The Semantics of Destructive Lisp"[0]. There is an interesting quote from Scherlis and Scott[1] which leads me to think there is a crossover from Collin's work on Cylindrical Algebraic Decomposition.[2] The first thought involves the difference between a verification proof and a derivation proof. Verification involves proving an algorithm that already exists. Derivation involves transformations from an initial set to a final result. Both proofs work but [2] says "The traditional correctness proof -- that a program is consistent with its specifications -- does not constitute a derivation of the program. Conventional proofs, as currently presented in the literature, do little to justify the structure of the program being proved, and they do even less to aid in the development of new programs that may be similar to the program that was proved. That is, they neither explicate existing programs nor aid in their modification and adaptation. We intend that program derivations serve as conceptual or idealized histories of the development of programs. That is, a program derivation can be considered an idealized record of the sequence of design decisions that led to a particular realization of a specification. Stripped down to essentials, our claim is that the programs of the future will in fact be descriptions of program derivations. Documentation methods based on stepwise-refinement methodologies are already strong evidence that there is movement toward this approach. These documentation methods also provide support for the hypothesis that program derivations offer a more intuitive and revealing way to explain programs than do conventional proofs of correctness. The proofs may succeed in convincing the reader of the correctness of the algorithm without giving him any hint of why the algorithm works or how it came about. On the other hand, a derivation may be thought of as an especially well-structured constructive proof of correctness of the algorithm, taking the reader step by step from an inital abstract algorithm he accepts as meeting the specifications of the problem to a highly connected and efficient implementation of it." For mathematical algorithms, Mason [0] points out that it is possible to mechanically specialize an algorithm for a given case, often with an order of magnitude of efficiency. This is very appealing, especially in numeric domains where it can be proven that things cannot overflow. Collins works in semialgebraic sets, basically polynomials with a few comparison limits and parameters. CAD could be "bent" to use it as a compile step so that a CAD result would generate a program. Not only would this give a complete specification, it would provide a solid theoretical basis for the code. Can this be extended to derive other algorithms? Matrices can be viewed as polynomials. Can numeric algorithms be derived from the specification (e.g. LAPACK programs) that guarantee behavior? Much more reading to do... Tim 33:134-183 (1975) _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Greetings! I am considering pushing some pathname ansi fixes from
master into the upcoming gcl release. This has exposed an axiom issue. #'pathname cannot take a symbol argument. Here is a patch, which I think is backward compatible (testing): --- axiom-20140801.orig/books/bookvol5.pamphlet +++ axiom-20140801/books/bookvol5.pamphlet @@ -23115,7 +23115,7 @@ o )history (cond ((eq fullopt '|ifthere|) (setq ifthere t)) ((eq fullopt '|quiet|) (setq quiet t)))) - (setq ef (|pathname| /editfile)) + (setq ef (or (|pathname| /editfile) "")) (when (eq (|pathnameTypeId| ef) 'spad) (setq ef (|makePathname| (|pathnameName| ef) "*" "*"))) (if arg @@ -37660,8 +37660,9 @@ The localdatabase function tries to find (if make-database? (setq noexpose t)) (when dir (setq nrlibs (processDir dir thisdir))) (dolist (file filelist) - (let ((filename (pathname-name file)) - (namedir (directory-namestring file))) + (let* ((file (string file)) + (filename (pathname-name file)) + (namedir (directory-namestring file))) (unless namedir (setq thisdir (concatenate 'string thisdir "/"))) (cond ((setq file (probe-file @@ -38708,7 +38709,7 @@ filetype and filemode. We also UPCASE ev (defun |pathname| (p) (cond ((null p) p) - ((pathnamep p) p) + ((pathnamep p) p)((symbolp p) (pathname (string p))) ((null (consp p)) (pathname p)) (t (when (> (|#| p) 2) (setq p (cons (elt p 0) (cons (elt p 1) nil)))) --- axiom-20140801.orig/src/interp/patches.lisp.pamphlet +++ axiom-20140801/src/interp/patches.lisp.pamphlet @@ -106,9 +106,9 @@ previous definition. (cond ((null filename) (dribble) (TERPRI) (reset-highlight)) - ((probe-file (car filename)) + ((probe-file (string (car filename))) (error (format nil "file ~a already exists" (car filename)))) - (t (dribble (car filename)) + (t (dribble (string (car filename))) (TERPRI) (clear-highlight)) )) There may be other places, but this seems close to minimal. Suggestions? Take care, -- Camm Maguire [hidden email] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |