[Question on Formalization] How can I write number in base other than 10

[Kunhao Zheng]

Hello all!

    I'm quite a beginner on metamath. Recently I search on representing numbers in base other than 10, like in base 3 or base 7 when I formalize some exercises in number theory. For example, I want to write 2121_3 - 212_3 (both in base 3).

I browse through the Th.List on the website and it seems that I didn't find relevant information. Any hint is welcome!

Bests Regards

Kunhao

[Jim Kingdon]

On April 23, 2021 3:27:19 AM PDT, Kunhao Zheng <dye...@gmail.com> wrote:
> For example, I want to write
>2121_3 - 212_3 (both in base 3).

The obvious way to represent the left hand number is ((3 · 2) + ((3 · 1) + ((3 · 2) + 1))) .

As for whether there is a more convenient notation, have we come up with an arbitrary-base version of http://us.metamath.org/mpeuni/df-dec.html or do we just have it for base 10?

[Jim Kingdon]

On April 23, 2021 4:33:58 PM PDT, Jim Kingdon <kin...@panix.com> wrote:
>The obvious way to represent the left hand number is ((3 · 2) + ((3 ·
>1) + ((3 · 2) + 1))) .

Uh, I think I parenthesized that wrong. But hopefully it is clear what I meant.

[Norman Megill]

You are right that numbers use only base 10 in set.mm, via the definition

df-dec $a |- ; A B = ( ( 10 x. A ) + B ) $.

This definition (due to Mario) nicely incorporates decimal number notation into set.mm with a standard definition, without extending the the Metamath language or introducing another variable type (so that we still have wff, setvar, and class as the only types). A slightly awkwardness compared to other languages is that we have to add a ";" prefix for each additional digit, so that 312 base 10 is represented as "; ; ; 3 1 2", but I see that as a small price to pay in order to avoid complicating the metamathematical justification of definitions.

Overall, we prefer to have a single standard base for the majority of the work in set.mm in order to avoid duplicate theorems with numbers in different bases (or frequently having to convert between bases inside of proofs). I think it is unlikely that we will add additional bases for the main part of set.mm because of this.

When Mario first introduced the idea of df-dec, he started with base 4 because it may have offered certain technical advantages for some of his work, but in the end he (thankfully) settled on base 10, which of course is the most readable to most humans for most purposes.

Even though we are unlikely to add other bases for the main part of set.mm, people are free to do whatever they want (up to a point) in their mathboxes. If you want to play around with say base 3, you could introduce a new symbol, say ";3", and a definition like

df-ter $a |- ;3 A B = ( ( 3 x. A ) + B ) $.

in your mathbox, so that 2121_3 - 212_3 would be represented as

;3 ;3 ;3 2 1 2 1 - ;3 ;3 2 1 2

which even though a little ugly, at least clearly lets the reader know you're working in base 3.  If the "3" in ";3" is deemed to be too confusing, another symbol could be used, for example ";;;" (3 semicolons).

With more complexity you could have a variable base as an additional argument to the definition, but it would probably be unpleasant to read.

Another alternative is the one suggested by Jim Kingdon of summing terms consisting of explicit powers of the base multiplied by the corresponding digit.  That would involve no new notation, but of course would involve longer expressions.

Norm

[Glauco]

Hi Kunhao,

in addition to the answers you already got about the representation, in case you don't already know about

http://us.metamath.org/mpegif/df-dig.html

in Alexander's mathbox: "Definition of an operation to obtain the k_th digit of a nonnegative real number in the positional system with base b.  k=-1   corresponds to the first digit of the fractional part"

I don't know if Alexander has also done some work on an "efficient" way for generic base representations.

Glauco

[Glauco]

I've never played with Words in set.mm, but it looks like you could define something like

toNum = ( b e. NN , n e. Word ( 0 ..^ b ) |-> sum_ k e. dom n ( ( n ` k ) x. ( b ^ k ) ) )

where b is your base and n is your representation in base b

(please, note that  ( n ` 0 ) would be your least significant digit, you should change the ( n ` k ) expression if you want it to be your most significant digit)

Glauco

Il giorno venerdì 23 aprile 2021 alle 15:29:37 UTC+2 dye...@gmail.com ha scritto:

[Mario Carneiro]

I also want to mention that Jim Kingdon's suggestion of simply using ((3 · ((3 · 2) + 1)) + 2) has official support in set.mm, in that for every dec* theorem there is a corresponding num* theorem about the generalized base representation of numbers. As Norm says, this suite of theorems was used when I was working in base 4, but they are not hard coded to any particular base, unlike df-dec which is base-10 specific.

> To represent numbers in any basis, we can also use finite sequences of figures (aka words) and implement the operations
accordingly. It has the advantage that we can make collections of numbers represented by position,
what is not allowed by Mario Carneiro's denotation.

Another variation on this that has come up in lean is to use the base X and form a polynomial instead of a number. However you can't do carrying with this representation, because it is base-dependent, so you have to live with non-canonical representations of numbers like X*1 + 13 with X = 10.

> (The same representation duality exists for fractions and should also be implemented, since it is the only
way to implement concepts like that of irreductible fractions.)

It's possible to talk about irreducible fractions without an actual representation like this - you can simply have a hypothesis a is coprime to b and then talk about some property of a/b.

> P.S. Does anyone know what is going on at Lean. Why did they have to change the concept of monoid?

Monoids have recently been changed to incorporate the monoid power operation into the structure, even though it is formally redundant, in order to solve some definitional equality issues that metamath does not have to deal with because it is based on ZFC.

On Sat, Apr 24, 2021 at 6:27 PM Norman Megill <n...@alum.mit.edu> wrote:

FL asked me to post this for him.

-------- Forwarded Message --------
Subject: Positional representation
Date: Sat, 24 Apr 2021 13:25:26 +0200 (CEST)
From: frederic.line
To: Megill Norman

‌Hi Norm,

can you post this mail:

To represent numbers in any basis, we can also use finite sequences of figures (aka words) and implement the operations
accordingly. It has the advantage that we can make collections of numbers represented by position,
what is not allowed by Mario Carneiro's denotation.

(The same representation duality exists for fractions and should also be implemented, since it is the only
way to implement concepts like that of irreductible fractions.)

P.S. Does anyone know what is going on at Lean. Why did they have to change the concept of monoid?

--
FL

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/10bcbe8b-ed80-407b-b965-7614752e8b21n%40googlegroups.com.

[Norman Megill]

Sorry for the duplicate post. I deleted the original to edit a detail that FL didn't want publicly exposed. (In Aug. 2020, Google Groups removed the ability to edit posts.)

[Alexander van der Vekens]

On Saturday, April 24, 2021 at 10:35:03 PM UTC+2 Glauco wrote:

Hi Kunhao,

in addition to the answers you already got about the representation, in case you don't already know about

http://us.metamath.org/mpegif/df-dig.html

in Alexander's mathbox: "Definition of an operation to obtain the k_th digit of a nonnegative real number in the positional system with base b.  k=-1   corresponds to the first digit of the fractional part"

I don't know if Alexander has also done some work on an "efficient" way for generic base representations.

 No, I haven't done anything more for generic base representations. I just needed a generalization of http://us2.metamath.org:88/mpeuni/df-bits.html which is applicable also for reals instead of integers only, the generalization from base two to arbitrary bases was just a by-product.

[Alexander van der Vekens]

On Saturday, April 24, 2021 at 11:01:09 PM UTC+2 Glauco wrote:

I've never played with Words in set.mm, but it looks like you could define something like

toNum = ( b e. NN , n e. Word ( 0 ..^ b ) |-> sum_ k e. dom n ( ( n ` k ) x. ( b ^ k ) ) )

where b is your base and n is your representation in base b

(please, note that  ( n ` 0 ) would be your least significant digit, you should change the ( n ` k ) expression if you want it to be your most significant digit)

This is really a good idea. By such a definition, we can use the representations of short words (up to a length of 8, see http://us2.metamath.org:88/mpeuni/df-s1.html etc.).  If the order of the digits is reversed, as Glauco suggests, i.e. defining

toNum = ( b e. NN , n e. Word ( 0 ..^ b ) |-> sum_ k e. dom n ( ( n ` k ) x. ( b ^ ( ( ( # ` n ) - 1 ) - k ) ) ) )

then ( 3 toNum <" 2 1 2 1 "> ) would represent the ternary number 2121, which is ( 2 * 3 ) + 1 ) * 3 ) + 2 ) * 3 ) +1 = 70. The length of the word n = <" 2 1 2 1 "> is ( # ` n ) = 4, therefore 1 must be subtracted in the exponent in the definition of toNum. By reversing the order of the arguments, and using the name _b instead of isNum:

_b = ( n e. Word ( 0 ..^ b ) ,  b e. NN |-> sum_ k e. dom n ( ( n ` k ) x. ( b ^ ( ( ( # ` n ) - 1 ) - k ) ) ) )

we would get ( <" 2 1 2 1 "> _b 3 )= ; 70, which seems to be a quite good and natural representation.

By the way, with such a definition, we would have ( <" 2 5 7 0 "> _b 10 ) = ; ; ; 2 5 7 0

Alexander

[Mario Carneiro]

You can use `reverse` in order to reverse the word, by the way, rather than baking the index arithmetic into the `_b` function.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b5d17ac3-7437-47a2-b23c-9ff261fe5178n%40googlegroups.com.

[Alexander van der Vekens]

On Saturday, May 1, 2021 at 4:39:17 PM UTC+2 di....@gmail.com wrote:

You can use `reverse` in order to reverse the word, by the way, rather than baking the index arithmetic into the `_b` function.

That means

_b = ( n e. Word ( 0 ..^ b ) ,  b e. NN |-> sum_ k e. dom n ( ( ( reverse ` n ) ` k ) x. ( b ^ k ) ) )

[Glauco]

we would get ( <" 2 1 2 1 "> _b 3 )= ; 70, which seems to be a quite good and natural representation.

I agree, nice representation.

[David A. Wheeler]

On May 1, 2021, at 10:01 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
> we would get ( <" 2 1 2 1 "> _b 3 )= ; 70, which seems to be a quite good and natural representation.

+1, I agree, that’s really clean.

> That means
> _b = ( n e. Word ( 0 ..^ b ) , b e. NN |-> sum_ k e. dom n ( ( ( reverse ` n ) ` k ) x. ( b ^ k ) ) )

That seems like a nice higher-level definition.

I can easily imagine a number of general-purpose theorems building on this notation.

--- David A. Wheeler

[Kunhao Zheng]

Thank you all for these suggestions! I think I'll be playing with the  ( <" 2 1 2 1 "> _b 3 )= ; 70 and see how that will bring me.

Bests

Kunhao