October 05 2015

Of men and machines (doing mathematics)

Dr Giuseppe Primiero is Senior Lecturer in Computing Science and a member of the Foundations of Computing research group at Middlesex University. Here Giuseppe discusses the recent British Colloquium for Theoretical Computer Science, which he helped organise.

How many of the functionalities located today on your standard desktop or mobile computer were first the object of theoretical study by mathematicians and computer scientists? And which of today’s theoretical results will be essential to tomorrow’s computing technologies?

Often this theoretical work is at such a high level of abstraction that you would hardly recognise the relevance to the final working application, but essential it is.

By its own nature, Computer Science is a field of research that uniquely combines theory and applications, in a way no other scientific field really does. Computers are, after all, physical artefacts ruled by logical principles – a marriage of mathematics and technology born out of many distinct theoretical and practical results.

Notable among other figures is the role of the British mathematician Alan Mathison Turing. His theoretical device first proved the logical possibility of a general-purpose machine during a time when a ‘computer’ was principally a human doing computations. Only many years later did the word became widely and uniquely used for mechanical calculators.

Today research in Computer Science is still bred of the theoretical results that at first are motivated by computational problems. In this first, traditional sense, mathematics is at the core of computation and this theoretical research may take long routes before the results become essential to technologies of interest and profit for all mankind.

On the other hand though (and several decades after the birth of the first calculating machines), today’s research in mathematics and many other sciences is also led by machines working alongside their human counterparts. Their computational power, speed and large (although finite) memory are increasingly of aid when performing otherwise impossible calculations.

Hence, the progress of theoretical research (in particular in the mathematical field) relies heavily on the physical computations performed by machines. In this second and entirely novel sense, mathematics itself becomes a product of computation, and the way this inversed relation will affect the nature and principles of our knowledge and technology in the future is still to be discovered.

British Colloquium for Theoretical Computer Science

As a result of this, research in theoretical computer science is becoming more and more of direct interest and quick relevance to other fields outside of academia. It was with this in mind that the Foundations of Computing Group at Middlesex recently hosted the 31st edition of the British Colloquium for Theoretical Computer Science (BCTCS).

This meeting traditionally welcomes PhD students from across the country to present their work alongside talks from internationally renowned researchers – offering an overview of the most relevant trends in the research area.

This year, the remarkable list of invited speakers boasted two Turing Award winners and one Fields Medalist (roughly speaking these are like the Nobel Prizes in Informatics and Mathematics, respectively).

Sir Tony Hoare FRS (Microsoft Research, University of Cambridge) opened the colloquium discussing the interaction between concurrent and sequential processes.

Tony is well known for developing the formal language CSP (Communicating Sequential Processes) to specify the interactions of concurrent processes, which enables programmers to make machines execute processes in overlapping time periods (i.e. concurrently) as opposed to one after another (i.e. sequentially).

This has led to crucial improvements in speeding up computing technologies, and represents some of the essential mechanisms hidden in today’s computing technology which came about through theoretical investigations.

Per Martin-Löf (Stockholm University) opened proceedings on the second day with a talk on the mathematical structures underlying repetitive patterns and functional causal models. This very abstract talk was not surprising from a logician best-known for his type theory – a mathematical result that has been at the very basis of computer programs used today to perform proofs and obtain logical deduction in an automated way.

In the afternoon Samson Abramsky FRS (University of Oxford) offered his fascinating views on contextuality, a key feature of quantum mechanics that permits quantum information processing and computation to transcend the boundaries of classical computation. This could possibly be the next stage of our interaction with machines.

On the third day we welcomed, from Pittsburgh USA, Thomas Hales. Tom is best known for proving the Keppler Conjecture about the close packing of spheres.

Imagine a grocer selling oranges who wants to stack as many as possible in a small place. Most people naturally seek to build an arrangement known as face-centered cubic and the famous 17th century astronomer Johannes Keppler conjectured that this arrangement, filling space at a density around 74%, could not be beaten.

Remarkably it took more than 370 years before a proof appeared. The most trusted proof was given by Tom, but this had 250 pages and involved three gigabytes of computer programs, data and results. Reviewers of his work noted they were 99% certain of its accuracy but incredibly Tom was not satisfied with this and spent a decade engaging an automated theorem prover (running on a computer) to verify all parts of his proof. The climax of this tour de force was the announcement in 2015, by Tom and his many collaborators, of a formal proof for the Keppler Conjecture.

The theorem-proving theme continued in the afternoon when renowned mathematician Sir Tim Gowers FRS (University of Cambridge) spoke on his ideas of an extreme human-oriented, heuristic-based automated theorem prover that would be of use to everyday mathematicians. Tim spoke about his programme to remedy a lack of engagement between most working mathematicians and the automated theorem proving community.

The final day welcomed another star of Computer Science as Joseph Sifakis (University of Lausanne) spoke about rigorous system design. This talk was of interest to theorists and the more application-oriented alike, before the colloquium finished with Andrei Krokhin (Durham University) discussing recent research in the value constraint satisfaction problem.

Theoretical Computer Science is today experiencing an exciting phase in research methodology: the collaboration of men and machines is offering unforeseen possibilities, as well as problems. Theory and technology are becoming less distant and the effects of this collaboration are being seen stronger and faster in everyday life.

Share this post

 

Tags: computer science, mathematics, theoretical computer science