tag:blogger.com,1999:blog-11295132.post7106042552186760212..comments2017-12-12T08:09:30.941-08:00Comments on A Neighborhood of Infinity: Desingularisation and its applicationsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger6125tag:blogger.com,1999:blog-11295132.post-67744622289820886782008-05-27T17:46:00.000-07:002008-05-27T17:46:00.000-07:00There is a minor bug in the desingularisation code...There is a minor bug in the desingularisation code: it is putting a zero dual part on the result of (D 0 a')/(D 0 b'). Here is an example that manifests the bug:<BR/><BR/>> desingularise (\x -> ((x*x)/x)/x) 0<BR/><BR/>I think the right thing to do is to put "D (a'/b') undefined" where the current version reads "D (a'/b') 0".<BR/>--<BR/>Barak A. Pearlmutter <barak@cs.nuim.ie>Barakhttps://www.blogger.com/profile/09369029379493432025noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-85412057414760755212008-05-14T13:17:00.000-07:002008-05-14T13:17:00.000-07:00It's entirely possible what you say is true, but s...It's entirely possible what you say is true, but since LL you'd be surprised what has a Curry-Howard (CH)style presentation. A really good example is the work of Caires on a semantic approach to types for concurrency. See http://ctp.di.fct.unl.pt/~lcaires/papers/CALCO-Caires-1.0.pdf<BR/><BR/>Also, i've been thinking about what the actual mathematical content of CH is and i'm starting to suspect it's captured rather simple. See my series of postings at biosimilarity.blogspot.comMeredithhttp://biosimilarity.blogspot.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-70667077790575032702008-05-14T11:56:00.000-07:002008-05-14T11:56:00.000-07:00Meredith,I suspect that the metatheorem that reduc...Meredith,<BR/><BR/>I suspect that the metatheorem that reduces proofs using infinitesimals to proofs not using them is far too complex to consider via Curry-Howard. Isn't it carried out with respect to an axiom system (ZF, I guess) that doesn't have an obvious computational interpretation via Curry-Howard? But otherwise what you're saying makes perfect sense to me.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-30403858999186682162008-05-14T10:19:00.000-07:002008-05-14T10:19:00.000-07:00So... i haven't taken the opportunity to read your...So... i haven't taken the opportunity to read your postings on infinitesimals in detail, but this idea of desingularization caught my eye as related to something i've wanted to pursue. Robinson and others have shown that non-standard analysis proofs can be reduced to standard ones. i've often thought that there might be a lovely analogy to proof normalization (cut reduction) -- which (via Curry-Howard) -- is beta-reduction in disguise. If so, there might be a computational method/engine for real computation lurking there. In other words, can we derive a beta-reduction-like method for real computation out of the algorithm for turning non-standard (analysis) proofs into standard (analysis) proofs? Or, is there an solution to the "equation"<BR/><BR/>cut-elimination : beta-reduction :: non-standard analysis to standard analysis proof xform : XMeredithhttp://biosimilarity.blogspot.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-62834760555935755412008-05-14T09:43:00.000-07:002008-05-14T09:43:00.000-07:00Mikael,There's a subtlety with this. If you apply ...Mikael,<BR/><BR/>There's a subtlety with this. If you apply desingularise to a function of type a -> a then internally it creates a function of type Dual a -> Dual a. So if you were to write a function that could apply desingularise n times then internally it must create objects of type Dual (Dual (Dual (... a))). I don't think the Haskell type system would allow the writing of such a function, though I'm not sure.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-67798868220193966512008-05-14T08:23:00.000-07:002008-05-14T08:23:00.000-07:00So, could one use something like fix desingularize...So, could one use something like <I>fix desingularize</I> or similar to take care of all finitely removable singularities?Mikaelhttps://www.blogger.com/profile/00008302080954798496noreply@blogger.com