Special Session in Honour of Norbert Müller's Retirement

Special Session in Honour of Norbert M¨uller’s Retirement Continuity, Computability, Constructivity 2025 – From Logic to Algorithms September 2025, Swansea, UK Jens Blanck: A Domain Theoretical Understanding of the iRRAM The iRRAM is a successful implementation of Exact Real Arithmetic. We will look at the implementation from a domain theoretic perspective and at some of the important choices made in its implementation. Pieter Collins: Exact Real Computation and the iRRAM One of the main goals of research into computable analysis is to develop tools for real number computation which are both exact and efficient. Norbert M¨uller’s iRRAM, originating from the mid 1990s, was the first system to do just this, and is still competitive today. In this talk, I’ll look at the development of iRRAM and perspectives for the future of exact real computation. Michal Koneˇcn´y: Multi-Valued Limits in iRRAM and cAERN Some real-valued problems are only computable as non-deterministic functions. For example, the complex square root is not computable as a function but it is computable as a multi-valued function that returns one of the two roots non-deterministically. Moreover, the non-deterministic result is sometimes computed as a limit: The terms of the limit are non-deterministic and yet converge to one of the possible valid results. I recall and contrast the multi-valued limit operators provided by iRRAM, AERN and cAERN. Each has some subtle aspects that require careful description. In summary: •The iRRAM version is more efficient, •The AERN version is simpler, •cAERN provides a way to formally verify uses of the AERN multivalued limit. cAERN’s multivalued dependent choice axiom is similar to iRRAM’s mechanism for achieving convergence of a multivalued limit. (Joint work with Sewon Park and Holger Thies) Dieter Spreen: Computing with Compact Sets In collaboration with U. Berger, a general framework was presented for extracting algorithms that compute on elements of compact metric spaces and their compact subsets from proofs in a many-sorted intuitionistic first-order predicate logic, extended by strictly positive inductive and coinductive definitions. The approach is computationally equivalent to Weihrauch’s type-two theory of effectivity. Unlike this approach, however, it is purely logical and representation-free. Representations of the computed objects are obtained via a realizability interpretation of the logic. Note that although the logic is fundamentally intuitionistic, much of classical logic is nevertheless available: any genuine disjunction-free formula can be used as an axiom. In this talk, we discuss the mathematical framework introduced for the treatment of elements and nonempty compact subsets of compact metric spaces in formal logic. Furthermore, we present a generalization of Berger’s nested coinductive inductive characterization of uniformly continuous functions of the unit interval to the general case of compact metric spaces. This characterization enables the treatment of (constructively) uniformly continuous functions in the aforementioned first-order logical calculus and the derivation of programs for computing such functions. We re-prove some well-known results in metric space theory based on the characterization. The proofs now use coinduction and induction in a nested manner and differ significantly from the usual proofs of classical topology.