Department Seminar

Wednesday, 2 December 2026, Aula G

16:30

Dirk Pattinson (Australian National University)

Computable functions, coinductively

We investigate a representation of computable functions as total functions over the set of finite and infinite sequences of elements from {0,1}. In this model, infinite sequences are interpreted as non-terminating computations, while finite sequences represent the sum of their digits. We introduce a new definition principle, function space corecursion, which generalizes both minimization and primitive recursion. This defines the class of computable corecursive functions, which is closed under composition and function space corecursion. We prove that computable corecursive functions represent all partial recursive functions and demonstrate—by translating them into the untyped lambda calculus—that all such functions are indeed computable. Finally, we outline how this representation of computable functions can be further developed into an algebraic approach to computability and complexity.

Prof. Pattinson currently is visiting professor within the University of Verona’s internationalisation programme PIA.

Page on the University of Verona website
Link.