Second-Order Functions and Theorems in ACL2

TL;DR

SOFT is a tool that enables the simulation of second-order functions and theorems within ACL2's first-order logic, facilitating program refinement and theorem proving involving higher-order concepts.

Contribution

It introduces a systematic method to mimic second-order functions and theorems in ACL2, expanding its capability to handle higher-order reasoning.

Findings

Enables systematic generation of second-order function instances

Supports program refinement through predicate sequences

Facilitates higher-order theorem proving in ACL2

Abstract

SOFT ('Second-Order Functions and Theorems') is a tool to mimic second-order functions and theorems in the first-order logic of ACL2. Second-order functions are mimicked by first-order functions that reference explicitly designated uninterpreted functions that mimic function variables. First-order theorems over these second-order functions mimic second-order theorems universally quantified over function variables. Instances of second-order functions and theorems are systematically generated by replacing function variables with functions. SOFT can be used to carry out program refinement inside ACL2, by constructing a sequence of increasingly stronger second-order predicates over one or more target functions: the sequence starts with a predicate that specifies requirements for the target functions, and ends with a predicate that provides executable definitions for the target functions.