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 CurryHoward 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 omegacategories 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.
Wednesday, March 15, 2006
Subscribe to:
Post Comments (Atom)
Blog Archive

▼
2006
(92)

▼
March
(20)
 Quantum Probability
 A Neat Proof Technique
 The General Theory of SelfReproducing Programs
 Stanislaw Lem has Passed Away
 The Most Amazing and Mysterious Thing in All of Ma...
 6
 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
 Hyperfun!
 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 WouldBe Generalisers

▼
March
(20)
Some Links
About Me

Dan Piponi
 Blog: A Neighborhood of InfinityCode: GithubTwitter: sigfpeHome page: www.sigfpe.com
3 comments:
Jon Cohen (http://thatlogicblog.blogspot.com) was trying to teach me about cartesian closed categories and refresh my memory about homotopies enough to help him come up with such a topology, when I was in Australia last year. He's very sharp, and seems good at motivating people, so I wouldn't be surprised if he's got some more relevant stuff by now.
I'm busy giving myself a crash course in category theory at the moment. Though I studied algebraic topology years ago I never did category theory for its own sake. Among other things I'm wondering about some down to earth stuff  using linear logic to do linear mathematics. Eg. linear types allow you to do matrix and vector operations more efficiently in place.
Normalisation of proofs in Natural Deduction has been shown to be related to finding normal forms of lambda terms via the howardcurry correspondance. I imagine that finding equivelent lambda terms is closely related to homotopies of proofs.
Post a Comment