3
$\begingroup$

A while ago I wondered about how Proof Assistants like Coq prove $m \leq n$ and the like. It looks like they actually need to traverse the natural numbers based on the successor/predecessor formulation:

Coq < Eval compute in le_lt_dec 100000 1000000. Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed). Stack overflow.

One of the answers suggested using the BinInt (Binary Integers representation) to perform this operation.

When a mathematician looks at a claim like $1000 ≤ 1000000$ and says "obviously", they are taking advantage of the fact that we wrote the claim in decimal notation. If you want to do something similar in CoQ, you could try to prove, e.g., $10∗10∗10≤10∗10∗10∗10∗10$.

So I'm wondering if there is a standard way of representing numbers as types without defining them like Peano's axioms style, using successor/predecessor and the like. Something that allows you to prove two numbers have a relation such as $m \leq n$ or $m \neq n$ or do other common things with numbers like adding/subtracting, in such a way where the "formal definition" (i.e. succ/pred) of the numbers is combined with some more computationally optimal version so you can use it in practice. Not sure what best-practice is to do here, but I would like to define a numbers type and have it gain all the advantages of proof theory / proof assistants, while also being the actual type definition used to construct i.e. integers.

$\endgroup$
  • 1
    $\begingroup$ You certainly can: just represent it as an array of digits, and enumerate the digits as an algebraic data type! $\endgroup$ – xuq01 Jun 21 '18 at 16:31
7
$\begingroup$

There's nothing stopping you from defining binary numbers in type theory, and this should give greater efficiency in practice.

For example:

https://coq.inria.fr/library/Coq.Numbers.BinNums.html

EDIT: Why not base 10?

Comparison on binary numbers can be done in $O(\log_2 n))$ time. If you have base 10, you can do it in $O(\log_{10} n)$ time. But if we apply the change of base formula, $O(\log_{10} n) = O(\log_{2} n / \log_{2} 10) = O(\log_2 n)$, since $O(\log_2 10)$ is constant.

There's a speed tradeoff. You get constant speedup for some operations, but you get constant slowdown for others. For example, each pattern match now has 11 options instead of 3. So, given that they have the same asymptotic behavior, we usually go with the simplest one.

Finally, the advantage with base 2 is that, if you limit yourself to 32 or 64 bits, you can represent them using machine integers, for example, if you extract your Coq code to OCaml, which means you can get very fast extracted code.

$\endgroup$
  • $\begingroup$ The advantage is that you need fewer nested constructor symbols for representing the same number with succ and 0 (i.e. unary), right? Wouldn't base 10 then be a better option? I guess the reason for not choosing arbitrary large bases is that Coq's internal memory consumption would rise. $\endgroup$ – ComFreek Jun 20 '18 at 12:55
  • 1
    $\begingroup$ @ComFreek I've extended the answer to address this. $\endgroup$ – jmite Jun 20 '18 at 18:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.