Peano numbers as types and universal quantification

1

According to Peano and Dedekind, the natural numbers can be defined in terms of the successor function. We can represent this successor function as a type constructor, define arithmetic operations and let the compiler verify propositions about natural numbers.

For a longer explanation, see

"Proving that 1 + 1 = 2 in Rust" by gretingz,
"Proving that 1 + 1 = 10 in Rust" by Tavian Barnes.

The following program verifies the proposition 1 + 1 = 2 in a brief formulation and slightly modified terminology.

struct Zero;
struct Succ<N>(N);

trait Nat {}
impl Nat for Zero {}
impl<N: Nat> Nat for Succ<N> {}

trait Plus<B> {type Value;}
type Add<A, B> = <A as Plus<B>>::Value;

impl<B: Nat> Plus<B> for Zero {
    type Value = B;
}

impl<A: Nat + Plus<B>, B: Nat> Plus<B> for Succ<A> {
    type Value = Succ<Add<A, B>>;
}

macro_rules! assert_type_eq {
    ($a:ty, $b:ty) => {
        const _: Option<$a> = Option::<$b>::None;
    }
}

type One = Succ<Zero>;
type Two = Succ<One>;

assert_type_eq!(Add<One, One>, Two);

Now consider an universal quantification like

∀(n: Nat). n + 0 = n.

How to find a program to verify this proposition? Is it possible at all?

2

Here's one for ∀(n: Nat). 0 + n = n (but not for ∀(n: Nat). n + 0 = n).

// A bunch of `Default` derives and bounds, then

fn for_all<T: Nat>() -> T {
    Add::<Zero, T>::default()
}
3

Without having to magic terms out of thin air using Option or Default :slight_smile:

fn zero_is_additive_left_identity<N: Nat>(n: N) -> Add<Zero, N> {
    n
}

BTW, I love how helpful rustc is if you try to prove a falsehood, eg.

type Three = Succ<Two>;

fn one_plus_two_equals_three(three: Add<One, One>) -> Three {
    three
}

25 |     three
   |     ^^^^^ expected struct `Succ`, found struct `Zero`
   |
   = note: expected struct `Succ<Succ<Succ<Zero>>>`
              found struct `Succ<Succ<Zero>>`
help: try wrapping the expression in `Succ`
   |
25 |     Succ(three)
   |     +++++     +

ie. "silly programmer, 3 = 1+1+1, not 1+1" :smiley:

1 Like
4

Not possible because you're missing the Axiom of Induction, and without it it's not necessarily true.

What induction means in Rust terms would be that the only types implementing Nat are Zero and Succ<N: Nat> and no other.

Currently there is no such constraint. For instance:

struct AnotherNumber;

impl Nat for AnotherNumber {}

impl<B: Nat> Plus<B> for AnotherNumber {
    type Value = B;
}

And now Add<AnotherNumber, Zero> is Zero rather than AnotherNumber, so the theorem that Add<N, Zero> = N is false.

You could express the principle of induction by using a sealed trait, but I don't know if type inference uses that information (I don't think so).

1 Like
5

Looks like a profound counterargument. In simple terms, the induction axiom ensures the non-existence of parallel structures. By implementing Nat for a further type one establishes such a structure, and can subsequently do mischief with it.

6

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.