Inductive Invariants for Nested Recursion

Abstract. We show that certain input-output relations, termed inductive invariants are of central importance for termination proofs of algorithms defined by nested recursion. Inductive invariants can be used to enhance the standard recdef definition package in Isabelle/HOL. We also offer a formalized theory in higher-order logic that incorporates inductive invariants and that can be used as an alternative to recdef in difficult cases. The use of this theory is demonstrated on a large example of the BDD algorithm Apply. Finally, we introduce a related concept of inductive fixpoints with the property that for every functional in higher-order logic there exists a largest partial function that is such a fixpoint.

• Type: Conference
• Year: 2003
• Where: TPHOL
• Authors: Sava Krstic, John Matthews
• Keywords: Artificial Intelligence, Certain Input-output Relations, Inductive Invariants, Recdef Definition Package, TPHOL 2003