[opentheory-users] a standalone tactic translating numeral encodings

Ramana Kumar ramana.kumar at gmail.com
Fri Feb 17 01:59:49 UTC 2012

I've written a Haskell program that acts as a conversion between Norrish
numerals and binary numerals.
It reads an OpenTheory article encoding a Norrish numeral n[N] (made with
bit1, bit2, and zero) and writes an article that proves the theorem:
|- n[N] = n[B]
where n[B] is the binary encoding of n (made with bit0, bit1, and zero).
You can access it as a "standalone tactic" at http://cam.xrchz.net/n2b.cgi.
It may use up to 6 theorems as axioms (which are all proved in the standard

The Haskell source code is here
https://github.com/xrchz/typed-conv/blob/master/numeral/n2b.hs (around 500
I'm pretty new to Haskell, so I'd very much appreciate any comments on the
A lot of the infrastructure should be resuable by future standalone tactics
in Haskell.

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
 - would it be more efficient to store conclusions with proofs rather than
computing them with concl? but I think Haskell memoises anyway...
 - is there a better algorithm for converting between these numeral
 - 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)?
 - probably lots of obvious things I'm doing less nicely than is possible...
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120217/25b64d30/attachment.htm>

More information about the opentheory-users mailing list