John V. Tucker
Encyclopedia
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 generalizing the classical theory to deal with all forms of discrete/digital
and continuous/analogue
data; and on using the generalizations as formal methods
for system design; and on the interface between algorithms and physical equipment.
(BA in 1973), and studied mathematical logic and the foundations of computing at University of Bristol
(MSc in 1974, PhD in 1977). He has held posts at Oslo University, The CWI Amsterdam, and at Bristol and Leeds Universities, before returning to Wales as Professor of Computer Science at Swansea University
in 1989. In addition to theoretical computer science, Tucker also lectures on the history of computing and on the history of science and technology and Wales.
Tucker founded the British Colloquium for Theoretical Computer Science
in 1985 and served as its president from its inception until 1992. He is a Fellow
of the British Computer Society
and editor of several international scientific journals and monograph series. At Swansea, he has been Head of Computer Science (1994–2008) and Head of Physical Sciences (2007–11). He is Member of Academia Europaea
.
Outside of Computer Science, Tucker is a Trustee of the Welsh think-tank, the Institute of Welsh Affairs
and the chair of the Swansea Bay
branch. He is also a Trustee of the South Wales Institute of Engineers Educational Trust
.
Professor Tucker is married to Dr. T.E. Rihll, Reader in Ancient History at Swansea University.
Professor Tucker is a Founding Fellow of the Learned Society of Wales
and in July 2010 he was appointed as its inaugural General Secretary.
s, 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.
1. how algorithms can be boosted by special purpose physical devices acting as “oracles”;
2. 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:
United Kingdom
The United Kingdom of Great Britain and Northern IrelandIn the United Kingdom and Dependencies, other languages have been officially recognised as legitimate autochthonous languages under the European Charter for Regional or Minority Languages...
computer scientist and expert on computability theory
Computability theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
, also known as recursion theory
Recursion theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
. Computability theory is about what can and cannot be computed by people and machines. His work has focused on generalizing the classical theory to deal with all forms of discrete/digital
Digital
A digital system is a data technology that uses discrete values. By contrast, non-digital systems use a continuous range of values to represent information...
and continuous/analogue
Analog signal
An analog or analogue signal is any continuous signal for which the time varying feature of the signal is a representation of some other time varying quantity, i.e., analogous to another time varying signal. It differs from a digital signal in terms of small fluctuations in the signal which are...
data; and on using the generalizations as formal methods
Formal methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
for system design; and on the interface between algorithms and physical equipment.
Biography
Born in Cardiff, Wales, he was educated at Bridgend Boys' Grammar School, where he was taught mathematics, logic and computing. He read mathematics at University of WarwickUniversity of Warwick
The University of Warwick is a public research university located in Coventry, United Kingdom...
(BA in 1973), and studied mathematical logic and the foundations of computing at University of Bristol
University of Bristol
The University of Bristol is a public research university located in Bristol, United Kingdom. One of the so-called "red brick" universities, it received its Royal Charter in 1909, although its predecessor institution, University College, Bristol, had been in existence since 1876.The University is...
(MSc in 1974, PhD in 1977). He has held posts at Oslo University, The CWI Amsterdam, and at Bristol and Leeds Universities, before returning to Wales as Professor of Computer Science at Swansea University
Swansea University
Swansea University is a university located in Swansea, Wales, United Kingdom. Swansea University was chartered as University College of Swansea in 1920, as the fourth college of the University of Wales. In 1996, it changed its name to the University of Wales Swansea following structural changes...
in 1989. In addition to theoretical computer science, Tucker also lectures on the history of computing and on the history of science and technology and Wales.
Tucker founded the British Colloquium for Theoretical Computer Science
British Colloquium for Theoretical Computer Science
The British Colloquium for Theoretical Computer Science is an organisation that hosts an annual event for UK-based researchers in theoretical computer science...
in 1985 and served as its president from its inception until 1992. He is a Fellow
Fellow
A fellow in the broadest sense is someone who is an equal or a comrade. The term fellow is also used to describe a person, particularly by those in the upper social classes. It is most often used in an academic context: a fellow is often part of an elite group of learned people who are awarded...
of the British Computer Society
British Computer Society
The British Computer Society, is a professional body and a learned society that represents those working in Information Technology in the United Kingdom and internationally...
and editor of several international scientific journals and monograph series. At Swansea, he has been Head of Computer Science (1994–2008) and Head of Physical Sciences (2007–11). He is Member of Academia Europaea
Academia Europaea
Academia Europæa is a European non-governmental scientific academy founded in 1988. Its members are scientists and scholars who collectively aim to promote learning, education and research. It publishes European Review through Cambridge Journals....
.
Outside of Computer Science, Tucker is a Trustee of the Welsh think-tank, the Institute of Welsh Affairs
Institute of Welsh Affairs
The Institute of Welsh Affairs is an independent, membership-based think-tank based in the capital of Wales, Cardiff, owing no allegiance to any political or economic interest group...
and the chair of the Swansea Bay
Swansea Bay
Swansea Bay is a bay on the Bristol Channel on the South Wales coast. Places on the bay include Mumbles, Swansea and Port Talbot. The River Neath, River Tawe, River Afan and Blackpill stream flow into the bay....
branch. He is also a Trustee of the South Wales Institute of Engineers Educational Trust
South Wales Institute of Engineers
South Wales Institute of Engineers was founded in 1857 as a learned society for engineers and scientists in the area, arranging lectures and publishing the Proceedings of the South Wales Institute of Engineers. In 2007, the body was re-constituted as South Wales Institute of Engineers Educational...
.
Professor Tucker is married to Dr. T.E. Rihll, Reader in Ancient History at Swansea University.
Professor Tucker is a Founding Fellow of the Learned Society of Wales
Learned Society of Wales
The Learned Society of Wales is a society that exists to “celebrate, recognise, preserve, protect and encourage excellence in all of the scholarly disciplines”.The society was launched on 25 May 2010 at the National Museum of Wales...
and in July 2010 he was appointed as its inaugural General Secretary.
Work on computability and data types
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 algebraUniversal algebra
Universal algebra is the field of mathematics that studies algebraic structures themselves, not examples of algebraic structures....
s, 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
Jan Bergstra
Jan A. Bergstra is a Dutch computer scientist. His work has focussed on logic and the theoretical foundations of software engineering, especially on formal methods for system design...
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
On any discrete data type, functions are definable as the unique solutions of small finite systems of equations if, and only if, they are computable by algorithms.
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
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
. For example, they showed that:
All computable functions on the real numbers are the unique solutions to a single finite system of algebraic formulae.
The second generalisation, created with Viggo Stoltenberg-Hansen
Viggo Stoltenberg-Hansen
Viggo Stoltenberg-Hansen, born 1942, professor at Uppsala University, Department of Mathematics, is a Swedish mathematician/logician and expert on domain theory and recursion theory...
, focuses on implementing data types using approximations contained in the ordered structures of domain theory
Domain theory
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
.
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 analyzing the interface between algorithms and physical equipment. The theory answers various questions concerning:1. how algorithms can be boosted by special purpose physical devices acting as “oracles”;
2. 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:
If a physical experiment were to be completely controlled by an algorithm, what effect would the algorithm have on the physical measurements made possible by the experiment?
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:
There is a simple Newtonian experiment to measure mass, based upon colliding particles, for which there are uncountably many masses m such that for every experimental procedure governing the equipment it is only possible to determine finitely many digits of m, even allowing arbitrary long run times for the procedure. In particular, there are uncountably many masses that cannot be measured.
External links
- Home page
- http://hocc.swan.ac.uk/