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 -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b5d17ac3-7437-47a2-b23c-9ff261fe5178n%40googlegroups.com.
