what is a numeral

Stream: general

[Kevin Buzzard]

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]

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]

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

[Rob Lewis]

"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]

Then you wouldn't call 3.7 a numeral?

[Rob Lewis]

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]

So

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

is right.

[Anne Baanen]

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]

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]

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]

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

[Kevin Buzzard]

Thanks a lot for these comments!

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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