Thursday, 19 April 2007, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: We are today at the dawn of a new way of doing mathematics
and computer science. Computers are increasingly used to develop and
verify mathematical theories. On the other hand, computer programming
is becoming richer, with more expressive data types and programming
techniques. Eventually the two fields will converge and become a
single entity: Computer Mathematics.

I will discuss the relations between mathematics, logic, and computer science. I hope to convince you that dramatic advances in these connections are on the horizon that will radically change these fields.

From ancient times until 1800s, mathematics was mostly concerned with computing solutions to problems. In the second half of the nineteenth century, abstract notions were developed and the doctrine of mathematics as the study of pure absolute truth took hold.

As mathematics grew more and more incorporeal and nonconstructive, two other important developments took place: a deep crisis in the logical foundations of mathematics and, later, the development of the cornerstones of computer science.

A connection between logic and computer science, called realizability, was developed. It represented proofs in predicate logic as natural numbers and proof steps as arithmetical operations. A refinement of this conception led to represent proofs as programs in a typed language. This is called the Curry-Howard isomorphism. Per Martin-Löf developed a rich type theory that can be seen at the same time as a programming language, a logical system, and a mathematical universe.

Subsequently the theory grew by additions of new constructs and operations. However, many problems still need to be solved, before type theory becomes a complete environment to develop mathematics on a computer. Here are the problems that I consider more pressing:

- Extensionality/Intensionality: in Mathematics two functions are considered equal when they give the same result on every argument. In computer science two programs are considered different if they implement different algorithms, even if they give the same results. We must find a satisfying way to conciliate the two conceptions.
- Subsets and Quotients are essential in mathematics, but they are difficult to represent in type theory.
- Reflection: when mathematicians think about a problem, they often step outside the mathematical process and reason about it at a higher level. A good computer mathematics system must possess a similar ability.
- Computation: Even if type theory is a powerful and expressive programming language, it is not Turing complete. We must find a good way to represent, compute, and reason about general computable functions.

Tarmo Uustalu

Last update 27.4.2007