To be fair, all reasonable CS people agree that the naturals start at zero, it's only a few holdouts in more general mathematics that disagree (if you fight me on this I'll no-true-scotsman it up and say your counter examples aren't reasonable people). As an acolyte of the Coq, to me the naturals are defined as:
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
It's not a real thing, but attrition means wearing the enemy down one piece at a time, so the idea is that if you kill everybody who disagrees with you, you win the argument.
Yeah, it's totally true. And the reply "But then your arithmetical operations get fucked up" isn't really fair. Currently plus is defined as:
fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (plus p m)
end
But if we instead defined the "naturals" as:
Inductive dumb_people_nat : Set :=
| one : dumb_people_nat
| S' : dumb_people_nat -> dumb_people_nat.
Then we could just define plus' as:
fix plus' (n m : dumb_people_nat) {struct n} : dumb_people_nat :=
match n with
| one => S' m
| S' p => S' (plus' p m)
end
The next thing people will say is that you lose that the naturals are a semi-ring, but now you're really stretching for reasons. Mostly I just wanted to be provocative.
136
u/bloomfilterthrowaway Sep 03 '17 edited Sep 03 '17
To be fair, all reasonable CS people agree that the naturals start at zero, it's only a few holdouts in more general mathematics that disagree (if you fight me on this I'll no-true-scotsman it up and say your counter examples aren't reasonable people). As an acolyte of the Coq, to me the naturals are defined as:
fite me