People usually regard algorithms as more abstract than the programs that implement them. The natural way to formalize this idea is that algorithms are equivalence classes of programs with respect to a suitable equivalence relation. We argue that no such equivalence relation exists.
My first thought here -- and this is unusual for me, since I'm basically a discrete mathematician -- is that maybe the space of programs is "effectively continuous", in the same sense, that, say, reality is "effectively continuous" but actually has a discrete nature if you look closely enough, thanks to quantum physics. So the right thing to do would be to topologize the set of programs, so you can say that algorithms X and X' are "close to" each other, or perhaps to put a metric on it. But I naturally imagine that, say, if two programs differ by some small number of small changes then they would have to be considered the "same program" if we were looking for an equivalence relation. Imagine a graph whose vertices are programs, and two programs are connected by an edge if they differ by some small number of small changes; then we're naturally led to think of "algorithms" (if they are equivalence classes of programs) as connected components of that graph. But how do we decide what number of changes to allow, or how large they can be? Basically, the relation on the set of programs "expresses the same algorithm" doesn't seem to be transitive, as the authors point out, so "equivalence relation" is the wrong idea.
By the way, I speculate that calling the space of programs a metric space (say, with the metric induced from the graph I alluded to before) is wrong as well, but in a different way -- how does one assign lengths to the edges? That seems a bit subjective and squishy. Topology's the way to go here, although it's not like anybody's holding their breath waiting for an answer to this question. And it sort of feels like a question about moduli spaces (link goes to a post by Jordan Ellenberg), although I know next to nothing about those.
This reminds me (and the authors) of the question asked in Tim Gowers' post when are two proofs essentially the same. (In fact, is this the same question?)
3 comments:
What you want to do is consider a 2-category of programs. Objects are states, programs are morphisms, and "rewritings" of programs are 2-morphisms. Then you're thinking about trying to write a generating set for the 2-morphisms, and using that to define a graph metric on the collection of all 2-morphisms.
I have a feeling that, like happens in geometric group theory, the choice of generating set turns out not to matter up to quasi-isometry of the space.
This reminds me (and the authors) of the question asked in Tim Gowers' post when are two proofs essentially the same. (In fact, is this the same question?)
Despite the proofs/types/programs equivalence, this is not the same question for two reasons.
First, Gowers' idea is about human rigorous proofs, not formal proofs (in a logical system).
And second, there is a way of specifying an equivalence relation for formal proofs. see another set of Dershowitz' papers on Abstract Canonical Inference. (so in this sense algorithms and proofs are not the 'same' thing.
On an only slightly related note, I wonder if you could treat proofs topologically. That is, we could say that a correct proof would have genus 0, and in general a proof with n holes would have genus n.
Post a Comment