# Proving Axiom correct, derivations, and CAD

 Classic List Threaded
2 messages
Reply | Threaded
Open this post in threaded view
|

## Proving Axiom correct, derivations, and CAD

 Axiom now has the necessary machinery to process proofsat build time (ACL2 for Lisp, COQ for Spad). While ponderingthe subject I ended up reading "The Semantics of DestructiveLisp"[0]. There is an interesting quote from Scherlis and Scott[1]which leads me to think there is a crossover from Collin's workon Cylindrical Algebraic Decomposition.[2] The first thought involves the difference between a verificationproof and a derivation proof. Verification involves proving analgorithm that already exists. Derivation involves transformationsfrom 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 anorder of magnitude of efficiency. This is very appealing, especially innumeric domains where it can be proven that things cannot overflow.Collins works in semialgebraic sets, basically polynomials with a fewcomparison limits and parameters. CAD could be "bent" to use it asa compile step so that a CAD result would generate a program. Notonly would this give a complete specification, it would provide a solidtheoretical basis for the code. Can this be extended to derive otheralgorithms? Matrices can be viewed as polynomials. Can numeric algorithmsbe derived from the specification (e.g. LAPACK programs) thatguarantee behavior?Much more reading to do...Tim[0] Mason, Ian A. "The Semantics of Destructive Lisp"CSLI Lecture Notes Number 5, ISBN 0-937073-06-7 (1986)[1] Scherlis, W. L. and Scott, D. S. "First Steps TowardsInferential Programming" in R. E. A. Mason (Ed.) Information Processing 83 New York, North Holland[2] Collins, George E. "Quantifier elimination for the elementarytheory of real closed fields" Lecture Notes in Computer Science33:134-183 (1975) _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: Proving Axiom correct, derivations, and CAD

 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