Accounting for Recursion: A Descriptive and Computational Study of Fixed Points

Abstract

A fixed point of a function can be described as a special mathematical object, with several powerful applications. This thesis studies fixed points in the context of two distinct frameworks. Common to both research strands is a method for dealing with the iterative nature of fixed points. The first part of the thesis looks at the computation of least fixed points in terms of closure ordinals of formulas in the modal mu­-calculus. Using annotated structures, a new framework is defined to describe how the iterations of a fixed point formula evolve in a transition system. Applying a pumping technique allows us to establish an upper bound for countable closure ordinals. The method is tailored to the lower levels of the alternation hierarchy, but the fragment covered is broad enough to allow for considerations on the effects of fixed point alternation. In the second part, fixed points are considered in the context of a cyclic proof system for intuitionistic arithmetic. Cyclic proofs internalise induction in their structure, suggesting a natural fitting with quantifiers defined in terms of fixed points. Using higher­-order recursion schemes generated from instances of cyclic proofs, we investigate the computational content implicit in the initial proof.