Data Definitions in the ACL2 Sedan

TL;DR

The paper introduces a data definition framework for ACL2s that simplifies defining, testing, and reasoning about data types, supporting pedagogical and advanced use, with formal characterization and practical implementation.

Contribution

It presents a novel data definition framework for ACL2s that supports common data types, polymorphism, and formal characterization, enhancing usability and teaching.

Findings

Framework supports list, map, and record types.

Provides formal tau rule characterization of data definitions.

Enables effective counterexample generation in ACL2s.

Abstract

We present a data definition framework that enables the convenient specification of data types in ACL2s, the ACL2 Sedan. Our primary motivation for developing the data definition framework was pedagogical. We were teaching undergraduate students how to reason about programs using ACL2s and wanted to provide them with an effective method for defining, testing, and reasoning about data types in the context of an untyped theorem prover. Our framework is now routinely used not only for pedagogical purposes, but also by advanced users. Our framework concisely supports common data definition patterns, e.g. list types, map types, and record types. It also provides support for polymorphic functions. A distinguishing feature of our approach is that we maintain both a predicative and an enumerative characterization of data definitions. In this paper we present our data definition framework via a sequence of examples. We give a complete characterization in terms of tau rules of the inclusion/exclusion relations a data definition induces, under suitable restrictions. The data definition framework is a key component of counterexample generation support in ACL2s, but can be independently used in ACL2, and is available as a community book.