tag:blogger.com,1999:blog-264226589944705290.post3890478403141053803..comments2021-12-14T05:53:12.175-08:00Comments on God Plays Dice: When are two algorithms the same?Michael Lugohttp://www.blogger.com/profile/15671307315028242949noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-264226589944705290.post-83104042884081655482008-04-02T19:47:00.000-07:002008-04-02T19:47:00.000-07:00On an only slightly related note, I wonder if you ...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.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-264226589944705290.post-14722894876348222412008-03-25T11:54:00.000-07:002008-03-25T11:54:00.000-07:00This reminds me (and the authors) of the question ...<I>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?)</I><BR/><BR/>Despite the proofs/types/programs equivalence, this is not the same question for two reasons.<BR/><BR/>First, Gowers' idea is about human rigorous proofs, not formal proofs (in a logical system).<BR/><BR/>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.Mitchhttps://www.blogger.com/profile/06352106235527027461noreply@blogger.comtag:blogger.com,1999:blog-264226589944705290.post-69665594117188680792008-03-22T13:07:00.000-07:002008-03-22T13:07:00.000-07:00What you want to do is consider a 2-category of pr...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 <I>all</I> 2-morphisms.<BR/><BR/>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.Anonymousnoreply@blogger.com