Limited Second-Order Functionality in a First-Order Setting

We describe how we have defined in ACL2 a weak version of the Common Lisp functional apply, which takes a function and list of actuals and applies the function to the actuals. Our version, called apply$, does not operate on functions but on ordinary objects—symbols and lists representing lambda expressions—some of which are interpreted as functions. We define a syntactic notion of “tameness” to identify the interpretable objects. This makes our apply$ weaker than a true second-order functional but we believe apply$ is powerful enough for many uses in ACL2. To maintain soundness and the conservativity of our Definitional Principle we require that certain hypotheses, called “warrants”, be present in any theorem relying on the behavior of apply$ on non-primitives. Within these constraints we can define “functionals” such as sum and foldr which map tame “functions” over lists and accumulate the results. This allows the ACL2 user to avoid defining specialized recursive functions for each such application. We can prove and use general-purpose lemmas about these “functionals.” We describe the formalization, explain how we keep the Definitional Principle conservative, show examples of useful functions using apply$ and theorems about them, sketch the proof that there is a model of any extension of the system using the new primitives, discuss issues arising in making these functions executable, and show some preliminary performance results.