Termination in ACL2 Using Multiset Relations

Abstract

We present in this paper a case study of the use of the ACL2 system, describing an ACL2 formalization of multiset relations, and showing how multisets can be used to prove non-trivial termination properties. Every relation on a set A induces a relation on finite multisets over A; it can be shown that the multiset relation induced by a well-founded relation is also well-founded. We prove this property in the ACL2 logic, and use it by functional instantiation in order to provide well-founded relations for the admissibility test of recursive functions. We also develope a macro defmul, to define well-founded multiset relations in a convenient way. Finally, we present three examples illustrating how multisets are used to prove nontrivial termination properties in ACL2: a tail-recursive version of a general binary recursion scheme, a definition of McCarthy’s 91 function and a proof of Newman’s lemma for abstract reduction relations. These case studies show how non-trivial mathematical results can be stated and proved in the ACL2 logic, in spite of its apparent lack of expressiveness.