[opentheory-users] numerals

[Joe Hurd]

There are a lot of different possible representations for numerals,
and as we discussed some time ago all the HOL theorem provers use a
different one:

http://www.gilith.com/opentheory/mailing-list/2011-January/000062.html

For the OpenTheory standard theory library I'd like to use a
representation that is *standard* and *simple*. For me this means:

1. No theorem prover specific tagging (e.g., NUMERAL).

2. I agree with Rob that unary notation is best avoided: some
applications use large numbers (formalizing the Suite B cryptography
standard would require representing 384 bit numbers).

3. Using the current set of OpenTheory primitive inferences rules out
the "infinite family of natural number constants" that ProofPower
uses.

This leaves:

1. Standard binary notation (bit0 and bit1).
2. Norrish numerals (bit1 and bit2).
3. Decimal (digit0 ... digit9).

These are all good options, with positives and negatives. My own
preference is standard binary used by HOL Light and inherited by the
OpenTheory standard theory library. Decimal is arguably more standard
and closer to the printed theory, but not as simple. Norrish numerals
are just as simple as standard binary, but less standard. They have
the nice property that there is a unique representation for each
natural number. I have tried to mitigate the multiple representation
problem in OpenTheory in the theory pretty printing: only terms of the
form

zero | (bit0 | bit1)* bit1 zero

are printed as decimal numbers, and everything else is printed like a
normal term.

It is possible to convert between numeral representations as part of
the interface between OpenTheory and the HOL theorem prover, with more
or less fiddliness. One possible scheme for this is to carry out
numeral calculations in the local representation, and only convert the
assumptions and theorems of the theory interface to the OpenTheory
standard numerals (perhaps as a post-processing phase).

> I think it is safe to assume that systems that implement article readers
> will come equipped with decision procedures for formulas made from numeric
> literals using the usual arithmetic operations and predicates. So one
> option would be to omit the proofs of any theorem whose conclusion is a
> true instance of such a formula and mark such a theorem when it appears as
> antecedents to an inference rule (so that the reader knows to apply the
> decision procedure).
>
> The same idea would also
> allow a writer to omit proofs of propositional tautologies.

This is an interesting idea; the theorems with missing proofs could
just turn into assumptions of the theory. However, the standard theory
library is intended to be a "complete" set of theories with no missing
proofs, so it would be good to also support a way to export these
proofs in OpenTheory format.

Cheers,

Joe