John Vivian Tucker is a British computer scientist and expert on computability theory, also known as recursion theory. Computability theory is about what can and cannot be computed by people and machines. His work has focused on generalising the classical theory to deal with all forms of discrete/digital and continuous/analogue data; and on using the generalisations as formal methods for system design; and on the interface between algorithms and physical equipment.
Classical computability theory is based on the data types of strings or natural numbers. In general, data types, both discrete and continuous, are modelled by universal algebras, which are sets of data equipped with operations and tests. Tucker's theoretical work tackles the problems of: how to define or specify properties of the operations and tests of data types; how to program and reason with them; and how to implement them. In a series of theorems and examples, starting in 1979, Jan Bergstra and Tucker established the expressive power of different types of equations and other algebraic formulae on any discrete data type. For example, they showed that The results combined techniques of universal algebra and recursion theory, including term rewriting and Matiyasevich's theorem. For the other problems, he and his co-workers have developed two independent disparate generalisations of classical computability/recursion theory, which are equivalent for many continuous data types. The first generalisation, created with Jeffrey Zucker, focuses on imperative programming with abstract data types and covers specifications and verification using Hoare logic. For example, they showed that: The second generalisation, created with Viggo Stoltenberg-Hansen, focuses on implementing data types using approximations contained in the ordered structures of domain theory. The general theories have been applied as formal methods in microprocessor verifications, data types, and tools for volume graphics and modelling excitable media including the heart.
Work on computability and physics
Since 2003, Tucker has worked with Edwin Beggs and Felix Costa on a general theory analysing the interface between algorithms and physical equipment. The theory answers various questions concerning:
how algorithms can be boosted by special purpose physical devices acting as "oracles";
how algorithms control physical experiments that are designed to make measurements.
By transforming the idea of oracle in computability theory, they combine algorithmic models with precisely specified models of physical processes. For example, they ask the question: Their central idea is that, just as Turing modelled the human computer in 1936 by a Turing machine, they model a technician, performing an experimental procedure that governs an experiment, by a Turing machine. They show that the mathematics of computation imposes fundamental limits on what can be measured in classical physics:
In 2007 Tucker founded the History of Computing Collection at Swansea University. He has lectured on the history of computation since 1994, he is a founding member of the editorial board of the Springer book series History of Computing. He also lectures on the history of science and technology in Wales and is a founding member of the editorial board of the University of Wales Press book series Scientists of Wales.