Many years ago, while out drinking after an algebraic topology seminar, someone mentioned the idea of using algebraic topology to analyse computer programs. I never did get the details but I'm guessing it must have been something like the material presented at this conference.
Anyway, the comment got me thinking. I spend much of my time refactoring code. This is making small modifications to software intended to restructure it to a better form without changing its behaviour (eg. I've just been dumped with a single C++ source file 0.25MB long most of which is one function and is in considerable need of some tidying up!). If you think of a program as a path to get you from an input to an output then a change to that program, that keeps the behaviour the same, is a kind of homotopy between paths. But I couldn't really get anywhere with that idea.
In Baez's This Week's Finds this week he talks about homotopies between proofs. These are ways to convert one proof of a proposition into another proof of the same proposition. Cut elimination is such an operation but there are surely others.
According to the Curry-Howard isomorphism, a computer program that maps type A to type B is essentially the same thing as a proof of B assuming A. So a homotopy between programs is the same thing as a homotopy between proofs. For example, Baez's example of converting between two proofs P -> R corresponds exactly to converting the piece of Haskell code f . ( g . h) to (f . g) . h using the associativity of . (. is Haskell for function composition.)
So, is there some kind of interesting topology to be extracted from this? Does the space of programs that map input x to output f(x) have interesting fundamental groups or homology groups? I guess a good place to start would be with two simple programs to perform the same operation that can't be transformed into each other by simple steps. And do I really need omega-categories to make sense of this?
Anyway, besides Baez's stuff there's also theo's comments with a real world example of what looks like a homotopy between proofs.
- ► 2011 (13)
- ► 2010 (20)
- ► 2009 (21)
- ► 2008 (35)
- ► 2007 (37)
- Quantum Probability
- A Neat Proof Technique
- The General Theory of Self-Reproducing Programs
- Stanislaw Lem has Passed Away
- The Most Amazing and Mysterious Thing in All of Ma...
- Sets, Classes and Voodoo
- The Representation of Integers by Quadratic Forms
- Category Theory Screws You Up!
- What can I do with adjoints? And Lemma 28.
- Answers and questions
- Homotopies between proofs and between programs
- Cellular automaton puzzle
- Coalgebras and Automata
- It's a square, square world!
- Blind Games
- When is one thing equal to some other thing?
- An Actual Application of Fractal Dimension
- A Cautionary Tale for Would-Be Generalisers
- ▼ March (20)