Unravelling Abstract Cyclic Proofs into Proofs by Induction

TL;DR

This paper presents a method to convert cyclic proofs into finite proofs by extending proof systems with induction, enabling a better understanding and handling of infinite proof structures through finite representations.

Contribution

It introduces an extension of cyclic proof systems with a well-founded induction principle and a novel annotated proof representation for transforming cyclic proofs into finite proofs.

Findings

Transformation preserves cyclic proof structure

Handles non-linear inductive sorts

Applicable to recursive functions satisfying size-change termination

Abstract

Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract cyclic proof systems with a well-founded induction principle, and transform any cyclic proof into a finite proof in the extended system. Moreover, this transformation preserves the structure of the cyclic proof. Our results leverage an annotated representation of cyclic proofs, which allows us to extract induction hypotheses and to determine their introduction order. The representation is essentially a reset proof with one key modification: names must be covered in a uniform way before a reset. This innovation allows us to handle cyclic proofs where the underlying inductive sort is non-linear. Our framework is general enough to cover recursive functions satisfying the size-change termination principle, which are viewed as cyclic proofs under the Curry-Howard correspondence.