## Stream: general

### Topic: what is a numeral

#### Kevin Buzzard (Jan 15 2022 at 16:02):

My understanding is that 37 is a numeral. Is (37 : real) a numeral? My understanding is that real.pi is not a numeral. Is -37 a numeral? Is 1/37 a numeral? What is a numeral? I would not expect norm_num to prove pi>3 but I would expect it to prove 1/37>0. The documentation of norm_num says it proves theorems about numerical expressions. Is the idea that 1/37 is not a numeral but it's a "numerical expression"? Sorry for such weird questions, I'm writing notes for my course and I'd rather get things right the first time than have people complain that I'm not using terminology correctly.

#### Anne Baanen (Jan 15 2022 at 16:51):

By numeral, I mean a "numeric literal", so an expression denoting a fixed number that cannot be decomposed into subexpressions. So 37, 3.7, 0x25 and 0b00100101 are all numerals in Lean, -37 is not a numeral since it applies the - operator to 37.

I believe @Rob Lewis introduced me to this term, so he may have a more authoritative opinion.

#### Anne Baanen (Jan 15 2022 at 16:53):

Presumably "numerical expressions" in this context means expressions consisting only of numerals and operators known to norm_num.

#### Rob Lewis (Jan 15 2022 at 16:57):

"Cannot be decomposed into subexpressions" is maybe a bit off, since 37 is built of applications of docs#bit0, docs#bit1, etc. In the Lean 3 context specifically, I'd say a numeral is either has_zero.zero or a sequence of 0 or more applications of bit0 and bit1 to has_one.one. The type class requirements on these defintions mean that this only make sense over a type with 0, 1, and +.

#### Anne Baanen (Jan 15 2022 at 16:58):

Then you wouldn't call 3.7 a numeral?

#### Rob Lewis (Jan 15 2022 at 16:58):

37, 0x25 are numerals in this sense. 3.7 is not, but it is a "numerical expression": a sequence of applications of ring operations to numerals.

#### Rob Lewis (Jan 15 2022 at 17:00):

So

Is the idea that 1/37 is not a numeral but it's a "numerical expression"?

is right.

#### Anne Baanen (Jan 15 2022 at 17:00):

Right, I should make clear that by "subexpressions" I mean subexpressions in the source code. In the way that a + b can be decomposed into a, + and b, but not into has_add.add nor nat.has_add.

#### Rob Lewis (Jan 15 2022 at 17:03):

At least in the original C++ implementation of norm_num there was a third distinction, "generalized numerals" or something like that, which would have included 1/37 and -37. It's supposed to capture the notion of a fully reduced numeral expression.

#### Rob Lewis (Jan 15 2022 at 17:03):

Something like, "a numeral, or the negation of a numeral, or the division of two numerals, or the negation of the division of two numerals"

#### Rob Lewis (Jan 15 2022 at 17:04):

norm_num applied to a numeral expression should produce a generalized numeral.

#### Kevin Buzzard (Jan 15 2022 at 17:34):

Thanks a lot for these comments!

#### Mario Carneiro (Jan 15 2022 at 18:48):

I believe I have used the term "rational numeral" or "integer numeral" to refer (in norm_num docs) to what Rob calls "generalized numeral"

#### Mario Carneiro (Jan 15 2022 at 18:49):

so 1/3 is a rational numeral but 2/6 is not, and -13 is an integer numeral

#### Mario Carneiro (Jan 15 2022 at 18:50):

it is like "simp-normal form" but for norm_num instead

#### Mario Carneiro (Jan 15 2022 at 18:50):

Usually, when I say numeral without qualification I mean natural numeral though, so 0 or 1 or 37 but not 2+2 or -5

#### Mario Carneiro (Jan 15 2022 at 18:53):

the term overlaps a lot with "numeric literal" which deals with the actual parser input, so for example 0x20 is a hexadecimal literal and 32 is a (decimal) numeric literal. I probably use the terms interchangeably most of the time

Last updated: Aug 03 2023 at 10:10 UTC