Mathematics and Computation

Occasionally I hear claims that uncountable and uncomputable sets cannot be represented on computers. More generally, there are all sorts of misguided opinions about representations of data on computers, especially infinite data of mathematical nature. Here is a quick tutorial on the matter whose main point is:

It is meaningless to discuss representations of a set by a datatype without also considering operations that we want to perform on the set.

(more…)

Andrej has invited me to write about certain surprising functional programs. The first program, due to Ulrich Berger (1990), performs exhaustive search over the “Cantor space” of infinite sequences of binary digits. I have included references at the end. A weak form of exhaustive search amounts to checking whether or not a total predicate holds for all elements of the Cantor space. Thus, this amounts to universal quantification over the Cantor space. Can this possibly be done algorithmically, in finite time?

A tutorial presented at the Mathematical Foundations of Programming Semantics XXIII Tutorial Day.
(more…)

The famous theorem by Cantor states that the cardinality of a powerset `P(A)` is larger than the cardinality of `A`. There are several equivalent formulations, and the one I want to consider is

Theorem (Cantor): There is no onto map `A -> P(A)`.

In this post I would like to analyze the usual proof of Cantor’s theorem and present an insightful reformulation of it which has applications outside set theory. (more…)

For the benefit of the topology seminar audience at the math department of University of Ljubljana, I have written a self-contained explanation of the Kleene tree, which is an interesting object in computability theory. For the benefit of the rest of the planet, I am publishing it here.
(more…)

You may have heard at times that there are mathematicians who think that all functions are continuous. One way of explaining this is to show that all computable functions are continuous. The point not appreciated by many (even experts) is that the truth of this claim depends on what programming language we use.
(more…)

I recently lectured at an EST training workshop in Fischbachau, Germany. There were also a number of student talks, one of which was given by Luca Chiarabini from Munich. He talked about extraction of programs from proofs, using (a variant of) Curry-Howard isomorphism, also known as propositions-as-types. He had some very interesting ideas which were obviously related to old programming tricks, but he approached them from the logical point of view, rather than the programmer’s point of view. It got me thinking about how to write certain recursive programs as proofs. Since it is a nice application of program extraction, I want to share it with you here.

(more…)

In constructive mathematics even very small sets can be quite a bit more interesting than in classical mathematics. Since you will not believe me that sets with at most one element are very interesting, let us look at the set of truth values, which has “two” elements.

(more…)

Ordinary mathematicians usually posses a small amount of knowledge about logic. They know their logic is classical because they believe in the Law of Excluded Middle (LEM):

For every proposition `p`, either `p` or `not p` holds.

To many this is a self-evident truth. Therefore they cannot understand why someone would reject such a law, and a useful one at that, since many neat proofs depend on it. An equivalent law of logic is reductio ad absurdum or proof by contradiction:

For every proposition `p`, if `not p` does not hold, then `p` holds.

Constructive mathematicians do indeed reject LEM. But this does not mean they accept its negation! Unfortunately, many ordinary mathematicians seem to think precisely that, and so naturally they conclude that constructive mathematics is garbage. In fact, both classical and constructive mathematics prove quite easily that the negation of LEM is false. So what do constructive mathematicians believe?

(more…)