[opentheory-users] a standalone tactic translating numeral encodings

[Ramana Kumar]

On Thu, Apr 5, 2012 at 5:07 AM, Joe Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> This is extremely impressive work - nice job!
>
> By the way, I tried calling it from HOL Light but couldn't make it
> work - does it use your standard convention that the conversion
> accepts an axiom of the form `K F n[N]` and returns a theorem of the
> form `|- n[N] = n[B]`? My attempt is at the bottom of the file
> opentheory/cloud.ml in my HOL Light fork.
>

Yes I believe it is using that convention.
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.
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...)


>
> > Specific design questions I have:
> >  - would it be better to somehow write articles without going via a type
> of
> > proofs (i.e. just directly log as theorems are built)? I tried to figure
> out
> > a way to do that but failed, and also stopped thinking it would be better
>
> I like the way you have it right now with a datatype of proofs.
>
> >  - would it be more efficient to store conclusions with proofs rather
> than
> > computing them with concl? but I think Haskell memoises anyway...
>
> My gut reaction is that this would be a false economy. It's much
> clearer the way you have it now.
>

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..)


>
> >  - is there a better algorithm for converting between these numeral
> > encodings?
>
> From reading your code it's not entirely clear what your algorithm is.
> Could you briefly explain it?
>

The function n2b near the top of the file is the algorithm.
It's been a while, so let's see if I can figure out the algorithm just by
reading that code...
Recursive descent on the structure of Norrish numerals.
Easy cases:
n2b 0 = 0,
n2b (bit1 n) = bit1 (n2b n).
Difficult case:
n2b (bit2 n) =
we use a theorem |- bit2 n = suc (bit1 n)
then use the function binc to turn the suc into binary.
binc just does the obvious recursion using the following theorems:
|- suc 0 = bit1 0
|- suc (bit0 n) = bit1 n
|- suc (bit1 n) = bit0 (suc n)


>
> >  - my articles always leave tonnes of stuff on the stack because they
> just
> > def everything... is there an efficient algorithm for only deffing things
> > you'll actually use (and maybe removing them after you won't any more)?
>
> I don't think it's worth being super clean for "temporary articles"
> used in cloud tactics. The opentheory tool does a clean up of "archive
> articles" as part of installing theories to your local opentheory
> directory.
>

fair enough


>
> >  - probably lots of obvious things I'm doing less nicely than is
> possible...
>
> There are many people in the world who are more of a Haskell expert
> than me, but one thing that jumps out at me is that most of your
> top-level declarations don't have type declarations, which are good
> compiler-checked documentation.
>

true... I was busy being impressed by type inference...

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120405/5bfd92f4/attachment-0001.html>