Alg-top in CS

In a post below, I mentioned algebraic topology in computer science. A nice application of alg-top is for study of concurrency in distributed systems. For instance, one approach is to consider execution traces of a computational system being represented by time-directed paths through a space, and then to use alg-top methods to ask and answer questions about the structure of this space.

This approach leads naturally to a concept of homotopies of paths, equivalence classes of paths which may be transformed into one another via other paths in the space. What is different from traditional homotopy theory is that the paths are directed, and so these are referred to as directed homotopies or dihomotopies. Paths which are not dihomotopically equivalent represent execution traces on which there are events not reachable from one to another. For more on this, start with the GETCO conference pages.

New uses for Grothendieck topologies

I’ve been saying for a while that the big problems in computer science (eg, P vs NP; a theory of distributed systems; effective GO-playing machines; etc) need radical new methods, and I have suggested algebraic topology as a likely source of ideas. Joel Friedman has just applied some alg-top to boolean complexity, motivated by the P vs. NP problem, in Cohomology in Grothendieck Topologies and Lower Bounds in Boolean Complexity.

Lothaire is back!

A few months ago I claimed that there was a “new“ Lothaire book, Algebraic Combinatorics on Words. This was a brazen lie on my part — the book, published in 2002, has already reached the advanced age of 3. I came across the web page of Jean Berstel, which has a link to an an actual new Lothaire book, Applied Combinatorics on Words. This one really is published in 2005.

Berstel also has a link to the text of Theory of Codes, a book he cowrote with Dominique Perrin.

The Muddy Children Problem

Many mathematicians grew up on a diet of puzzles like those set by Raymond Smullyan and Martin Gardner. Unfortunately, ingenious and elegant as these puzzles often are, they frequently have solution methods that don’t give rise to generalisable theory.

So I was recently surprised to find that one of my favourite puzzles of this type, the Muddy Children Problem, is actually an important example that appears in courses on mathematical logic, epistemology, computer science and even quantitative finance. If you haven’t met the problem before then have a go at solving it before looking at the various papers and courses on the subject. A fairly detailed elementary treatment can be found here though there are easier to understand informal arguments in existence.

The main academic approaches to the problem are via modal logic and Kripke models.

In less politically correct days it was known as the unfaithful wives problem and Smullyan’s version of this problem involved logicians with coloured hats.

Did I mention that it’s also a drinking game?

Expander Graphs

It’s basically impossible to know all of the important concepts and results in mathematics. It’s impossible to even have heard of all of the important concepts and results in mathematics. For example, I’d never heard of expander graphs, which apparently have widespread applications in combinatorics and computer science, and even have an interpretation in terms of group representations.

Michael Nielsen has a series of posts on expander graphs beginning here. For more background, he links to lecture notes on the subject by Linial and Wigderson.

Programming Language and Logic Links

These thread on Lambda the Ultimate has several interesting links to online papers and books about the links between logic and functional programming languages.

What’s interesting is that, with one giant exception (category theory), the mathematics used is among the least fashionable. Most mathematicians can go through their entire careers without learning anything about proof theory and intuitionistic logic, and I think the reason is that both undermine the naive model of mathematical foundations that most mathematicians carry around in their heads. Mathematicians hate thinking about foundations. Whenever a famous open problem turns out to be equivalent to the Continuum Hypothesis, it’s like a family member died, or worse joined a cult.

Proof theory is disconcerting because it treats mathematican proofs as purely syntactic. Mathematicians, whatever their actual philosophy, adopt a working philosophy of Platonism: symplectic manifolds and 7-spheres and von Neumann regular algebras all exist in some nebulous “out there”. While mathematicians occasionally argue that mathematics is just the formal manipulation of symbols, in practice they think of a 7-sphere as an actual object.

In proof theory, mathematics really is just a formal manipulation of symbols. The more elementary parts of proof theory consist of proving one method of representing proof symbolically is the same as another. More advanced proof theory consists of studying topics such as proof normalization, where it is shown that proofs can be systematically rewritten in a particular form. Here are some further links to proof theory texts.

Intuitionistic logic is another field more prominent in computer science than in mathematics. Intuitionistic logic unnerves mathematicians by removing the law of the excluded middle: that a statement is true, or its negation is true. In classical logic, every statement can be (in principle) assigned a value of either true or false. To do the same for intuitionistic logic, some statements must be assigned intermediate truth values (in fact, infinitely many intermediate values become possible). Most mathematicians regard intuitionism as a historical curiosity not particularly of study.

Intuitionism is attractive to computer scientists, because whether or not its axioms correctly model truth, they do model knowability. The law of excluded middle doesn’t apply to knowability. A statement that is not known to be true may also be not known to false. Curry-Howard correspondence between logical formulas and function types has insired study of even weaker logical systems.