[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Proving Axiom correct, derivations, and CAD

From: Tim Daly
Subject: [Axiom-developer] Proving Axiom correct, derivations, and CAD
Date: Sun, 18 Sep 2016 23:21:27 -0400

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

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...


[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 Towards
Inferential Programming" in R. E. A. Mason (Ed.)
Information Processing 83 New York, North Holland

[2] Collins, George E. "Quantifier elimination for the elementary
theory of real closed fields" Lecture Notes in Computer Science
33:134-183 (1975)

reply via email to

[Prev in Thread] Current Thread [Next in Thread]