Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice

Zena M. Ariola, Paul Downen, Hugo Herbelin

TL;DR

The aim is to illustrate the expressive power of different notions of structural corecursion in the presence of classical reasoning, and study coiteration and corecursion combined with the classical callcc operator, which provides a computational interpretation of classical reasoning.

Abstract

Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural corecursion? Structural corecursion is an elegant technique, supported in languages like Haskell and proof assistants such as Rocq or Agda. It enables the design of compositional algorithms by decoupling the generation and consumption of potentially infinite or large data collections. Despite these strengths, structural corecursion is generally considered more advanced than structural recursion and is primarily studied in the context of pure functional programming. Our aim is to illustrate the expressive power of different notions of structural corecursion in the presence of classical reasoning. More specifically, we study coiteration and corecursion combined with the classical callcc operator, which provides a computational interpretation of classical reasoning. This combination enables interesting stream-processing algorithms. As an application, we present a corecursive, control-based proof of the Infinite Pigeonhole Principle and compare it with the continuation-passing proof of Escardó and Oliva in Agda. To further demonstrate the power of mixing corecursion and control, we give an implementation of the Axiom of Countable Choice. In contrast to the usual continuation-passing implementations of this axiom, which rely on general recursion whose termination is established externally, our approach justifies termination by coiteration alone.

Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice

TL;DR

The aim is to illustrate the expressive power of different notions of structural corecursion in the presence of classical reasoning, and study coiteration and corecursion combined with the classical callcc operator, which provides a computational interpretation of classical reasoning.

Abstract

Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural corecursion? Structural corecursion is an elegant technique, supported in languages like Haskell and proof assistants such as Rocq or Agda. It enables the design of compositional algorithms by decoupling the generation and consumption of potentially infinite or large data collections. Despite these strengths, structural corecursion is generally considered more advanced than structural recursion and is primarily studied in the context of pure functional programming. Our aim is to illustrate the expressive power of different notions of structural corecursion in the presence of classical reasoning. More specifically, we study coiteration and corecursion combined with the classical callcc operator, which provides a computational interpretation of classical reasoning. This combination enables interesting stream-processing algorithms. As an application, we present a corecursive, control-based proof of the Infinite Pigeonhole Principle and compare it with the continuation-passing proof of Escardó and Oliva in Agda. To further demonstrate the power of mixing corecursion and control, we give an implementation of the Axiom of Countable Choice. In contrast to the usual continuation-passing implementations of this axiom, which rely on general recursion whose termination is established externally, our approach justifies termination by coiteration alone.
Paper Structure (24 sections, 1 theorem, 28 equations, 4 figures)

This paper contains 24 sections, 1 theorem, 28 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Recursion.
  3. Corecursion.
  4. Patterns of corecursion.
  5. Infinite Pigeonhole Principle.
  6. Classical Countable Choice.
  7. Outline.
  8. Streams in Rocq
  9. Patterns of corecursion in Rocq
  10. Coiteration.
  11. Minimal Corecursion.
  12. Classical Corecursion.
  13. Infinite Pigeonhole Principle with corecursion
  14. Computing
  15. Proving
  16. ...and 9 more sections

Key Result

Theorem 3

For every infinite Boolean stream $bs$, there exists an increasing stream of indices $s$ such that each index points to the same truth value in $bs$:

Figures (4)

  • Figure 1: Search for infinite repetitions of a Boolean in a Boolean stream.
  • Figure 2: Program extracted to OCaml with Delimited control.
  • Figure 3: OCaml program extracted from the proof
  • Figure 4: Infinite Pigeonhole Principle with coiteration.

Theorems & Definitions (2)

  • Remark 2
  • Theorem 3: Infinite Pigeonhole Principle