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.

翻译：结构递归是现代编程语言中程序员常用的技术，也是计算机科学入门课程的教学内容。但其对偶概念——结构共递归呢？结构共递归是一种优雅的技术，在Haskell等语言以及Rocq或Agda等证明助手中得到支持。它通过解耦潜在无限或大规模数据集合的生成与消费，实现了组合式算法的设计。尽管具有这些优势，结构共递归通常被认为比结构递归更高级，且主要在纯函数式编程的语境中被研究。我们的目标在于阐明在经典推理存在下，不同结构共递归概念的表达能力。具体而言，我们研究了与经典callcc算子相结合的共迭代与共递归，该算子为经典推理提供了计算解释。这种结合催生了有趣的流处理算法。作为应用，我们提出了基于控制的结构共递归对无限鸽巢原理的证明，并与Escardó和Oliva在Agda中基于延续传递风格的证明进行了比较。为进一步展示共递归与控制机制融合的威力，我们实现了可数选择公理。与此公理通常依赖外部验证终止性的一般递归的延续传递实现不同，我们的方法仅通过共迭代即可论证终止性。