[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Re: ACL2 and Axiom
From: |
Tim Daly |
Subject: |
[Axiom-developer] Re: ACL2 and Axiom |
Date: |
Sat, 02 Oct 2010 14:24:08 -0400 |
User-agent: |
Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.9) Gecko/20100825 Thunderbird/3.1.3 |
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
>
>