17.12.2018
Limited Second-Order Functionality in a First-Order Setting
Erschienen in: Journal of Automated Reasoning | Ausgabe 3/2020
EinloggenAktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
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.