Search papers, labs, and topics across Lattice.
This paper explores the expressive power of structural corecursion combined with classical control operators (callcc) for stream processing. It presents a corecursive, control-based proof of the Infinite Pigeonhole Principle, contrasting it with existing continuation-passing proofs. Furthermore, the authors provide a novel implementation of the Axiom of Countable Choice using coiteration, achieving termination through coiteration alone, unlike traditional approaches relying on general recursion.
Corecursion plus classical control yields surprisingly elegant and terminating implementations of mathematical principles like the Infinite Pigeonhole Principle and Axiom of Countable Choice.
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\'o 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.
