Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unravelling Abstract Cyclic Proofs into Proofs by Induction

Lide Grotenhuis, Daniël Otten

TL;DR

This paper develops a general, proof-relevant translation from abstract cyclic proofs to finite inductive proofs. By extending an abstract cyclic system $\mathcal{C}$ with a well-founded induction principle to form $\mathcal{C}_{\text{ind}}$, the authors show that every $\mathcal{C}$-proof has a corresponding finite $\mathcal{C}_{\text{ind}}$-proof of the same statement, while preserving the original proof’s structure. The translation relies on an annotated cyclic representation and a reset-proof apparatus to extract induction hypotheses and define a coherent induction order, enabling a two-stage transformation that also accommodates multiple sorts. The framework recovers known conservativity results (e.g., CHA over HA) and extends to multi-sort settings, providing a modular bridge between cyclic and inductive proof systems with potential for constructive interpretation. Overall, the work offers a general method to finitize cyclic proofs while preserving their computational content and structure.

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.

Unravelling Abstract Cyclic Proofs into Proofs by Induction

TL;DR

This paper develops a general, proof-relevant translation from abstract cyclic proofs to finite inductive proofs. By extending an abstract cyclic system with a well-founded induction principle to form , the authors show that every -proof has a corresponding finite -proof of the same statement, while preserving the original proof’s structure. The translation relies on an annotated cyclic representation and a reset-proof apparatus to extract induction hypotheses and define a coherent induction order, enabling a two-stage transformation that also accommodates multiple sorts. The framework recovers known conservativity results (e.g., CHA over HA) and extends to multi-sort settings, providing a modular bridge between cyclic and inductive proof systems with potential for constructive interpretation. Overall, the work offers a general method to finitize cyclic proofs while preserving their computational content and structure.

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.
Paper Structure (25 sections, 11 theorems, 41 equations, 2 figures)

This paper contains 25 sections, 11 theorems, 41 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Cycles versus (co)induction.
  3. Type-theoretic conservativity.
  4. Proof-theoretic conservativity.
  5. Our goal.
  6. Contribution.
  7. Method.
  8. Related work.
  9. Structure of the article.
  10. Abstract cyclic systems
  11. Induced inductive system
  12. General idea and case studies
  13. General idea.
  14. An annotated cyclic representation
  15. Reset proofs
  16. ...and 10 more sections

Key Result

theorem 1

Every $\mathcal{C}$-proof $\pi$ has a cyclic representation $\pi_{\sf{cyc}}$ such that for every branch $n_0,\dots, n_s,\dots ,n_t$ with bud $n_t$ and sprout $n_s=\sf{sprout}(n_t)$ we have:

Figures (2)

  • Figure 1: Annotations for Examples \ref{['exam:run0']} and \ref{['exam:run1']}.
  • Figure 2: An example and a nonexample of reachability.

Theorems & Definitions (21)

  • definition 1: size-change graph
  • definition 2: cyclic call system
  • definition 3: terminating function
  • definition 4: cyclic proof system
  • definition 5: derivation
  • definition 6: proof
  • definition 7: cyclic representation
  • definition 8: induced cyclic proof system
  • definition 9: Annotations
  • theorem 1: existence of a reset proof
  • ...and 11 more