[Axiom-developer] Re: ACL2 and Axiom

[Tim Daly]

On 10/2/2010 9:47 AM, Matt Kaufmann wrote:
> Hi, Tim --
>
> I wonder if another possibility might be to view Axiom as a sort of
> slave to ACL2, rather than the other way around.  The sequence of
> steps would be: (1) build ACL2 as usual; (2) start up ACL2 and exit
> its read-eval-print loop (by typing :q); (3) load the Axiom files; and
> (4) save an image.  The Axiom user could then do his usual stuff, but
> when necessary, enter ACL2 to do whatever is necessary to discharge
> proof obligations.  With such an approach, if ACL2 cannot prove a goal
> automatically, then at least one could enter the ACL2 read-eval-print
> loop and interact with it to come up with a proof.
I see a few uses for ACL2/Axiom. One is as a build-time proof checker
to raise the level of system quality. A second is as a basis for some
research ideas I have about provisos. A third is as an end-user set of
Axiom domains for doing proofs (e.g. exporting a "prove" function)

The first issue of raising the level of system quality would involve
build-time proof checking which, if it failed, would be expected to stop 
the
build. There would be no need for a user interface.

The second issue of proviso work is "unpublished ideas" involving 
interactions
between Axiom domains. I have some ideas for symbolic intervals and I 
think that
ACL2 would be useful there. This also does not involve a user interface
since it only interacts with dynamically created Axiom objects. This
involves a pile of "scope issues" since sets of provisos would live in
a tree structure which Axiom needs to manage.

The third issue of the end-user "cover" functions would capture and expose
the ACL2 functionality (e.g. prove) applied to Axiom objects (e.g.
rationals, aka Fraction(Integer) in Axiom-speak). This might involve
user interaction with ACL2 but I haven't given that issue any thought.
It may be that the interactive portion "just works" depending on who
is reading the user input at the time. If the system falls into an ACL
interactive loop doing its own reads then Axiom won't know or care.
There is no such thing as a simple job, of course.


In the long term plan I want Axiom to have a solid, proven set of algorithms
but the proofs are static. The build times would be much longer but the end
user wouldn't see that. They would only see "certified" results. I would
consider it a milestone if I could automatically prove that Axiom's 
Euclidean
algorithm was correct. Just getting this right would be a whole PhD 
thesis :-)

So the long term goal is a computer algebra system with proven algorithms
rather than a system that proves things and uses a computer algebra system.
Hence ACL2 lives "inside" Axiom by design.

> I see two other potential advantages I can see for keeping ACL2
> intact.  The first is that by avoiding modifications to ACL2, even in
> small ways that you have in mind, you avoid the risk of unforeseen
> tricky issues (after many years I'm still often surprised by
> subtleties that arise when modifying ACL2), and you avoid having to
> maintain your mods over time as ACL2 evolves.  The second is that an
> ACL2 user could perhaps employ Axiom as a trusted oracle (using the
> so-called "trust tag" mechanism for external tools), so that
> computations done by Axiom are stored as ACL2 theorems (input =
> output).
I've created a git repository to track changes. That way I can pull the
latest ACL2 and merge my patches over your master code. I expect that there
will be several kinds of changes.

The first would be some #-Axiom conditionals to remove things like GCL
specific configurations that Axiom already does. Since we live in different
packages I don't think there will be function/macro name collisions. These
will not be of interest to you upstream.

The second will be adding bi-directional functions to convert ACL2 data
(e.g. rationals) and Axiom data (Fraction(Integer)). These will not be of
interest to you upstream.

The third will be some work on "proviso" or "interval" books.
These would be of interest to you and I'd push them upstream.

Another issue, from the Axiom side, is that Axiom is a literate program.
I'd like the proofs to also be literate since the intended audience for
the proofs is a human. I'm not yet familiar enough with the ACL2 code base
to have an informed opinion on this.
> By the way, I suspect though that Axiom traffics in real (and complex)
> numbers, or at least floating point numbers.  ACL2, however, is
> restricted to rational (and complex rational) numbers.  So you might
> want to consider instead Ruben Gamboa's modification ACL2(r) of ACL2,
> which is distributed with ACL2 but built with a different "make"
> command.  That system supports reals and complexes, though still not
> floats.
Axiom supports a lot of number types, including roman numerals :-)
My initial interest is intervals with a mixture of rational and symbolic
endpoints.

Machine reals (aka Axiom DoubleFloats) are of interest in that I'm
working on some numerics. It would be of interest to prove that no
reordering of Axiom-defined arithmetic operators causes results to
deviate by more than a small bounded number of low-order bits.

I've spent the last 5 years of my professional life at CMU (Axiom
is a hobby not related to work) developing the Intel machine level
semantics of instructions. We can now reason about machine code
sequences using conditional-concurrent assignments (CCAs). This
research is part of the Linger-Mills-Witt function semantics. It
will be interesting to see if there is a useful connection between
the function extraction semantics work and ACL2 machine-level proofs.

Floats (Axiom floats, that is) just make my head hurt. I don't think
I'm man enough to prove anything about them :-)

Tim

> I'd be happy to discuss any of this with you further, either on the
> list if you think others want to join in, or individually.
>
> -- Matt
>     X-IronPort-MID: 59165724
>     X-IronPort-MID: 220655909
>     X-SBRS: -0.5
>     X-IronPort-Anti-Spam-Filtered: true
>     X-IronPort-Anti-Spam-Result: AvAFAPvIpkzRh4wmX2dsb2JhbACiSR5IwRuFRASNPoga
>     X-IronPort-AV: E=Sophos;i="4.57,271,1283749200";
>        d="scan'208";a="220655909"
>     Date: Sat, 02 Oct 2010 11:56:02 -0400
>     From: Tim Daly<address@hidden>
>     CC: address@hidden, address@hidden,
>            address@hidden
>     X-Loop: address@hidden
>     X-Sequence: 218
>     X-no-archive: yes
>     List-Owner:<mailto:address@hidden>
>     X-SpamAssassin-Status: No, hits=-0.7 required=5.0
>     X-UTCS-Spam-Status: No, hits=-96 required=165
>
>       J
>
>     Ok. Once I climb the learning curve I'll look at that
>     in more detail.
>
>     I've put up a git repository to contain the changes I
>     need to make to embed ACL2. Both Axiom and ACL2 can sit
>     in the same lisp image. I have to figure out some Axiom
>     "cover" domains that export things like a "prove" function
>     and a compatible set of domains to cover the data representation.
>
>     I looked at the code a bit last night. Most of the code changes
>     would involve things like #- conditionally removing the ACL2
>     user I/O and GCL initialization.
>
>     Tim
>
>     On 10/2/2010 4:29 AM, J Strother Moore wrote:
>     >  Hi Tim.  You asked
>     >
>     >>  Does ACL2 handle reasoning about interval arithmetic?
>     >>  Are there particular books in ACL2 I should study?
>     >  I am not aware of an interval arithmetic book.
>     >  There have been several undergraduate student
>     >  projects to build simple interval arithmetic books
>     >  but none made it into the distribution.  Of
>     >  course, I presume you're aware of ACL2's extensive
>     >  collection of rational and integer arithmetic
>     >  books, e.g., arithmetic-5/top and the modulo
>     >  arithmetic of ihs and the
>     >  register-transfer/floating point stuff of rtl
>     >  (most recently rtl8).
>     >
>     >  J
>     >
>     >