<div class="gmail_quote">On Thu, Apr 5, 2012 at 5:07 AM, Joe Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> Hi Ramana,<br> <br> This is extremely impressive work - nice job!<br> <br> By the way, I tried calling it from HOL Light but couldn't make it<br> work - does it use your standard convention that the conversion<br> accepts an axiom of the form `K F n[N]` and returns a theorem of the<br> form `|- n[N] = n[B]`? My attempt is at the bottom of the file<br> opentheory/<a href="http://cloud.ml" target="_blank">cloud.ml</a> in my HOL Light fork.<br></blockquote><div><br>Yes I believe it is using that convention.<br>My guess is that you're generating an article with HOLLight.BIT2 rather than Number.Natural.bit2, but I haven't actually run your attempt.<br> If that's not the problem it would be helpful if you could send me the article that gets passed to the web tactic (or maybe I should have some infrastructure for saving it...)<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div class="im"><br> > Specific design questions I have:<br> > - would it be better to somehow write articles without going via a type of<br> > proofs (i.e. just directly log as theorems are built)? I tried to figure out<br> > a way to do that but failed, and also stopped thinking it would be better<br> <br> </div>I like the way you have it right now with a datatype of proofs.<br> <div class="im"><br> > - would it be more efficient to store conclusions with proofs rather than<br> > computing them with concl? but I think Haskell memoises anyway...<br> <br> </div>My gut reaction is that this would be a false economy. It's much<br> clearer the way you have it now.<br></blockquote><div><br>I guess if the performance is bad then profiling or benchmarks will decide this (and for now there's no real need to obscure the code..)<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div class="im"><br> > - is there a better algorithm for converting between these numeral<br> > encodings?<br> <br> </div>From reading your code it's not entirely clear what your algorithm is.<br> Could you briefly explain it?<br></blockquote><div><br>The function <span style="font-family:courier new,monospace">n2b</span> near the top of the file is the algorithm.<br>It's been a while, so let's see if I can figure out the algorithm just by reading that code...<br> Recursive descent on the structure of Norrish numerals.<br>Easy cases:<br><span style="font-family:courier new,monospace">n2b 0 = 0,</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">n2b (bit1 n) = bit1 (n2b n).</span><br> Difficult case:<br><span style="font-family:courier new,monospace">n2b (bit2 n) = </span><br>we use a theorem <span style="font-family:courier new,monospace">|- bit2 n = suc (bit1 n)</span><br>then use the function <span style="font-family:courier new,monospace">binc</span> to turn the <span style="font-family:courier new,monospace">suc</span> into binary.<br> <span style="font-family:courier new,monospace">binc</span> just does the obvious recursion using the following theorems:<br><span style="font-family:courier new,monospace">|- suc 0 = bit1 0</span><br style="font-family:courier new,monospace"> <span style="font-family:courier new,monospace">|- suc (bit0 n) = bit1 n</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">|- suc (bit1 n) = bit0 (suc n)</span><br> </div> <blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div class="im"><br> > - my articles always leave tonnes of stuff on the stack because they just<br> > def everything... is there an efficient algorithm for only deffing things<br> > you'll actually use (and maybe removing them after you won't any more)?<br> <br> </div>I don't think it's worth being super clean for "temporary articles"<br> used in cloud tactics. The opentheory tool does a clean up of "archive<br> articles" as part of installing theories to your local opentheory<br> directory.<br></blockquote><div><br>fair enough<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div class="im"><br> > - probably lots of obvious things I'm doing less nicely than is possible...<br> <br> </div>There are many people in the world who are more of a Haskell expert<br> than me, but one thing that jumps out at me is that most of your<br> top-level declarations don't have type declarations, which are good<br> compiler-checked documentation.<br></blockquote><div><br>true... I was busy being impressed by type inference... <br></div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <br> Cheers,<br> <br> Joe<br> <br> _______________________________________________<br> opentheory-users mailing list<br> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br> </blockquote></div><br>