[Axiom-developer] Re: ACL2 and Axiom

[Matt Kaufmann]

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

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.

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