3
$\begingroup$

Let's say we work in a dependent type theory with W-types and we want to have a type for binary natural numbers. We don't want to add quotient types or higher inductive types to the system.

How to represent the idea that leading zeroes don't change the natural number? Do we necessarily enter setoid territory at this point?

$\endgroup$
4
$\begingroup$

Use an auxiliary type of positive natural numbers.

data positive : Set where
  one : positive
  s0  : positive → positive -- multiply by 2
  s1  : positive → positive -- multiply by 2 and add 1

data N : Set where
  zero : N
  pos : positive → N

Supplemental: Another option, which I found on my whiteboard today (probably put there by Egbert Rijke months ago) is this:

-- Dyadic natural numbers without redundancy
data N : Set where
  zero : N      -- 0
  suc0 : N → N  -- suc1 n = 2 * n + 2
  suc1 : N → N  -- suc1 n = 2 * n + 1

I think you'll probably prefer this one.

$\endgroup$
3
  • 1
    $\begingroup$ You want to omit “one” from the whiteboard definition, as it already has a different representation. These are the dyadic numerals, by the way, rather than binary. $\endgroup$ – Emil Jeřábek Mar 17 at 16:58
  • 1
    $\begingroup$ Better link: en.wikipedia.org/wiki/Bijective_numeration. $\endgroup$ – Emil Jeřábek Mar 17 at 17:01
  • $\begingroup$ Thanks for the links and the useful information. I fixed the definition. $\endgroup$ – Andrej Bauer Mar 17 at 18:28

Your Answer

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