Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computation by infinite descent made explicit

Sebastian Enqvist

TL;DR

This work introduces a non-wellfounded sequent calculus for intuitionistic logic enriched with inductive and coinductive definitions, using ordinal-annotated fixpoints to capture descent. It provides a computability semantics showing that every valid proof is computable, which yields a normalization result for finitary formulas and guarantees that proofs of certain Sequent forms encode total functions on natural numbers. A Curry–Howard-style interpretation is developed via a term notation and reduction rules, and a categorical model is constructed in which least and greatest fixpoints correspond to initial algebras and final coalgebras, respectively. The paper also discusses the relationship to bouncing-thread validity and outlines future work on full cut-elimination and representation of bouncing-thread proofs within this framework.

Abstract

We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. We explore the computational content of this system, in particular we introduce a notion of computability and show that every valid proof is computable. As a consequence, we obtain a normalization result for proofs of what we call finitary formulas. A special case of this result is that every proof of a sequent of the appropriate form represents a unique function on natural numbers. Finally, we derive a categorical model from the proof system and show that least and greatest fixpoint formulas correspond to initial algebras and final coalgebras respectively.

Computation by infinite descent made explicit

TL;DR

This work introduces a non-wellfounded sequent calculus for intuitionistic logic enriched with inductive and coinductive definitions, using ordinal-annotated fixpoints to capture descent. It provides a computability semantics showing that every valid proof is computable, which yields a normalization result for finitary formulas and guarantees that proofs of certain Sequent forms encode total functions on natural numbers. A Curry–Howard-style interpretation is developed via a term notation and reduction rules, and a categorical model is constructed in which least and greatest fixpoints correspond to initial algebras and final coalgebras, respectively. The paper also discusses the relationship to bouncing-thread validity and outlines future work on full cut-elimination and representation of bouncing-thread proofs within this framework.

Abstract

We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. We explore the computational content of this system, in particular we introduce a notion of computability and show that every valid proof is computable. As a consequence, we obtain a normalization result for proofs of what we call finitary formulas. A special case of this result is that every proof of a sequent of the appropriate form represents a unique function on natural numbers. Finally, we derive a categorical model from the proof system and show that least and greatest fixpoint formulas correspond to initial algebras and final coalgebras respectively.

Paper Structure

This paper contains 45 sections, 17 theorems, 85 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Proof system
  3. Formulas
  4. Ordinal variables, constraints and sequents
  5. Proof rules
  6. Example: bouncing threads
  7. Cut reductions and Curry-Howard
  8. Term notation
  9. Substitution of ordinal variables
  10. Reduction rules
  11. $\vee$-reduction
  12. $\wedge$-reduction
  13. $\rightarrow$-reduction
  14. $\mu$-reduction
  15. $\nu$-reduction
  16. ...and 30 more sections

Key Result

Proposition 3.1

If $u$ is a valid proof of the sequent $\mathcal{O}, \Gamma \vdash A$ and $a$ is a child of $\infty$ in $\mathcal{O}$, then $u[a:=\infty]$ is a valid proof of $\mathcal{O}[\infty/a], \Gamma[\infty/a] \vdash A[\infty/a]$.

Figures (5)

  • Figure 1: Logical rules
  • Figure 2: Structural rules
  • Figure 3: Logical rules
  • Figure 4: Structural rules
  • Figure 5: Substitution for ordinal variables

Theorems & Definitions (40)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Proposition 3.1
  • proof
  • Definition 3.2
  • Proposition 3.3: Confluence
  • proof
  • Proposition 4.1
  • proof
  • ...and 30 more