Iteration in ACL2

TL;DR

This paper introduces an ACL2 analogue of the Common Lisp loop construct, enabling efficient and more natural iterative programming and reasoning within ACL2, which traditionally relies on recursion.

Contribution

The paper presents a novel ACL2 construct that mimics Lisp's loop, facilitating easier iteration and reasoning in ACL2 programs.

Findings

Provides an ACL2 analogue of the Lisp loop construct

Enables more efficient iterative programming in ACL2

Simplifies reasoning about iterative algorithms in ACL2

Abstract

Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- provides direct support for iteration. We describe an ACL2 analogue loop$ of loop that supports efficient ACL2 programming and reasoning with iteration.