# zbMATH — the first resource for mathematics

Limited second-order functionality in a first-order setting. (English) Zbl 1468.68291
Summary: 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.
##### MSC:
 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) 03B35 Mechanization of proofs and logical operations 68N15 Theory of programming languages 68N18 Functional programming and lambda calculus
##### Keywords:
ACL2; theorem proving; higher-order logic; functionals
##### Software:
OTTER; TPS; LISP; HOL; LEO-II; Satallax; ACL2; Isabelle; NQTHM; ML ; Haskell; Coq
Full Text: