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. 

Breve CV: 

Dirk Pattinson says he is a mathematician turned computer scientist. Before joining Australian National University he was senior lecturer at Imperial College London, lecturer at the University of Leicester and research associate at the University of Munich.