Adding Apply to ACL2
J Strother Moore

Abstract: This is a series of seminars reporting ongoing
joint work with Matt Kaufmann.

Apply is a Common Lisp function that takes a function
and a list of arguments and returns the result of
applying the function to those arguments.  Naively
axiomatizing apply to handle all definable functions in
ACL2's first order logic produces an inconsistent
theory.  One source of inconsistency is that it is
possible to define non-terminating ``non-recursive''
functions.  Another has to do with ACL2's notion of
local events in encapsulate and include-book.  In this
talk we present a ``tame'' apply and a solution to the
local problem.

Our apply is provided in a certified ACL2 book and is
thus guaranteed sound but has some serious drawbacks
including (a) it may be so restrictive that it is of no
use to the ACL2 user, (b) theorems proved about it may
be vacuous in the sense that they have unsatisfiable
hypotheses, and (c) it cannot be executed.  Addressing
(c) would require changes to ACL2 itself, which would
not be worthwhile if the answers to (a) and (b) are
unsatisfactory.

In part 1 of this series we will address the pragmatic
adequacy of our restricted apply by defining various
mapping functions and proofs and uses of various lemmas
about them.

In part 2, we will explain tameness and how apply is
defined in a certifiable way.

In part 3 we will explore why we believe that this
solution (or a modification of it) is non-vacuous.