[Axiom-developer] Re: ACL2/Axiom recommendation

[Matt Kaufmann]

Hi, Tim --

Cool!  Sure, I can imagine reasoning about data structures and
rational arithmetic of Axiom.

I don't know what "Special Functions" means, but since you mention
floating point I should say that reasoning about floating point
operations can be tricky -- much trickier in general, I'd say, than
rational operations.  That's because rationals are a primitive data
type in ACL2, but floating point operations need to be implemented in
terms of bit-level and rational operations (grab exponent, mantissa
and sign fields; then do stuff to the corresponding rationals; then
transform back to floating point).  You're right that there's been
work on floating point -- see directory books/rtl/rel7/lib/ that comes
with ACL2 -- but still, that's relatively complex stuff I'd say.

Finite fields would be a cool application, but I don't know of
existing work, so you'd probably be building specifications and
theorems from the ground up.  You could query the acl2 or acl2-help
list in case someone knows of work with ACL2 in finite fields.  But
the limits you mention make me wonder if a tool based more directly on
decision procedures might be more appropriate -- where ACL2 could
shine is in proving general properties, rather than using "brute
force" to check properties of a particular finite field's addition and
multiplication tables.

I'm pretty bad at knowing about (or remembering) previous work, but
you could try the "SEARCH" link that's near the top of the ACL2 home
page, or query the mailing list(s) as mentioned above.

I hope this helps.  If you haven't used ACL2, you might want to look
at some introductory materials such as:

- The "Tours", "demos", and "Hyper-Card" links on the home page
- The topic ACL2-TUTORIAL in the user's manual
- The ACL2 books, especially "Computer-Aided Reasoning: An Approach"
  (see
  http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books)
- The introductory and tutorial stuff at
  http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/index.html

-- Matt
   From: address@hidden
   Date: Fri, 22 Feb 2008 15:13:24 -0600
   Cc: address@hidden, address@hidden
   X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   X-UTCS-Spam-Status: No, hits=-82 required=165

   Matt and J,

   I've been looking at ACL2 in order to look at proving Axiom programs 
correct. 

   Besides the proof mechanism, ACL2 has the desirable property that it
   can co-exist with Axiom in the same image and thus have direct access
   to internal Axiom data structures. The idea would be to decorate domains
   with theorems and look at automatically propagating the theorems,
   bringing theorems in and out of scope, based on the hierarchy.

   I'm undecided what the most productive area might be to concentrate upon.
   Perhaps you can make a suggestion.

   Data Structure -- this might be useful because there is a large body
   of literature about the issue of proving sorting correct.

   Rational Arithmetic -- this has properties that fit in areas that ACL2
   already knows, such as the properties of abs().

   Special Functions -- this has properties of manipulation of floating point
   values which ACL2 has already explored.

   Finite Fields -- this might be easier due to the limits of the size and
   number of elements under consideration.

   Given your experience can you give me some high level advice and 
   potential pointers to previous work?

   Tim Daly
   address@hidden