Note that an expression such as <" <" A B C "> <" D E F "> <" G H I "> "> has the type (0..^N) -> ((0..^N) -> R), which would have to be converted anyway to match the expected I x I -> R type used by square matrices. If we take I to be (0..^N) then this is just an uncurry, but if the official index set for matrices is instead (1...N) then the index remapping could be performed at the same time.
On Wed, Sep 2, 2020 at 5:17 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > For clarification: there *is* already a definition of (square) matrices > based on arbitrary finite sets used as index sets (see ~df-mat, contributed > by Stefan O'Rear). The theorems which I needed to proof Cramer's rule are > based on this definion. If I understand Thierry correctly, he does not want > to replace this definition, but to provide an additional, more specialized > definition with an ordered index set, which can be used for special > theorems like the Laplace expansion (I was not able to prove it for > arbitrary finite sets...). > > The column vectors which I used for the matrix vector multiplication > `maVecMul` are also indexed by arbitrary finite sets, as mentioned by > Thierry, so this also covers the general case Mario is asking for. > > - > Alexander > > On Wednesday, September 2, 2020 at 9:49:50 AM UTC+2 Thierry Arnoux wrote: > >> Indeed, we do have matrix vector multiplication, ` maVecMul `, introduced >> by Alexander, and used in his proof of Cramer's rule. >> That operation considers vectors as functions of a single variable, >> indexed by any finite set. >> >> This can only identify with Words (` Word X `, which can be input as ` <" >> A B C "> ` ) if that set is of the form ` ( 0 ..^ N ) ` ... >> >> _ >> Thierry >> >> >> On 02/09/2020 15:15, Mario Carneiro wrote: >> >> I will reiterate my suggestion to use finite sets for indexing when >> possible, which sidesteps the question, but while I would like to defer to >> Norm here, I really think a lack of consistency is going to cause actual >> problems in this area. What is the definition of a matrix multiplied by a >> vector? Surely the vector has to be using the same indexing as the matrix. >> Perhaps we can have a separate type for vectors than words, but this seems >> superfluous and repetitive. >> >> I am willing to defer to decisions on convention making but I would like >> to see some clear path forward for the main definitions here and how they >> are not better served by a minor variation on the definition such as >> reindexing. >> >> Mario >> >> On Wed, Sep 2, 2020 at 12:30 AM Thierry Arnoux <[email protected]> >> wrote: >> >>> Thanks for all feedback! >>> >>> There are valid arguments on both sides, so we need Norm or Mario to do >>> a final call. >>> >>> >>> On 29/08/2020 08:06, Norman Megill wrote: >>> >>> While I'm not an expert, my guess is that the major uses of 0-based >>> arrays are in computer science and some computer programming languages, >>> where they can offer an advantage for some algorithms. >>> >>> But mathematics is meant for humans, and humans tend to count from 1. >>> That's why we number the proof steps on our web pages starting with 1. >>> Having the "first" step numbered with 0 would seem unnatural to me. >>> >>> As AV pointed out, we haven't been able to find a linear algebra >>> textbook with matrices numbered from 0. On Wikipedia, there are 4 subtopics >>> listed under >>> https://en.wikipedia.org/wiki/Vector#Mathematics_and_physics which are: >>> >>> https://en.wikipedia.org/wiki/Euclidean_vector >>> https://en.wikipedia.org/wiki/Row_and_column_vectors >>> https://en.wikipedia.org/wiki/Vector_space >>> https://en.wikipedia.org/wiki/Vector_field >>> >>> These all show 1-based indices. >>> >>> I have always wanted to see set.mm to be as close to mathematical >>> literature as possible or practical. Apparently almost all of linear >>> algebra literature uses 1-based matrices and vectors, so I think that is >>> what set.mm should do. Even if for some purposes it would be more >>> convenient to have matrices 0-based, it hasn't seemed to have harmed the >>> field. >>> >>> My vote is to conform to the literature and have matrices and vectors >>> 1-based. >>> >>> On Friday, August 28, 2020 at 2:20:35 PM UTC-4 di.... gmail.com wrote: >>> >>>> My vote is also in favor of starting with 0, or even better, doing >>>> everything over generic finite sets when possible and falling back on ( 0 >>>> ..^ N ). I realize that close correspondence with papers is considered >>>> important here but mathematicians write for their own ease. In a math >>>> paper, you can write either a_0, ..., a_(n-1) or a_1, ..., a_n - which is >>>> easier? Besides the strictness of a few inequalities this is probably the >>>> only difference, so a_1, ..., a_n is preferred because it is very slightly >>>> shorter. >>>> >>>> In formalization, we should also write for our own ease. In this case, >>>> that means better interfacing with the theory of finite words, which uses ( >>>> 0 ..^ N ). There are also other reasons to prefer 0 based indexing but in >>>> this case I think consistency with words (viewed as 1D vectors) is more >>>> important than that. >>>> >>>> On Fri, Aug 28, 2020 at 1:43 PM Benoit wrote: >>>> >>>>> I'm still in favor of words starting at 0. As for matrix rows and >>>>> columns, it would be more...wait for it... natural to start at 0, but >>>>> since >>>>> the literature overwhelmingly prefers to start at 1, maybe it's better to >>>>> conform with it (there are a few "historical accidents" like that, for >>>>> instance defining \pi as half what it should be, and since the >>>>> consequences >>>>> are very mild, it stays like that). >>>>> And to state the obvious: since most results using the fact that rows >>>>> and columns are natural numbers have them intervene in the form >>>>> (-1)^{i+j}, >>>>> shifting both row and column indices by 1 does not change the parity of >>>>> the >>>>> sum, so these statements are unaffected. >>>>> >>>>> Benoit >>>>> >>>>> On Friday, August 28, 2020 at 6:14:57 PM UTC+2 Alexander van der >>>>> Vekens wrote: >>>>> >>>>>> >>>>>> There was a discussion in >>>>>> https://groups.google.com/g/metamath/c/UwTUuNPgaB0/m/NdWefzG4AgAJ >>>>>> about the indices for words. Currently, the indices for words start with >>>>>> 0, >>>>>> and the proposal to change this was not accepted. >>>>>> >>>>>> For matrices, however, the things are different: The indices for rows >>>>>> and colums usually start with 1, as Thierry explained, so I agree with >>>>>> Thierry. And having the planned conversion function should dispel any >>>>>> doubt. >>>>>> >>>>>> Alexander >>>>>> >>>>>> On Friday, August 28, 2020 at 9:45:33 AM UTC+2 Thierry Arnoux wrote: >>>>>> >>>>>>> Hi all, >>>>>>> >>>>>>> I recently formalized a proof of the Laplace expansion of >>>>>>> determinants (~ mdetlap), which I think would be useful to pull to the >>>>>>> main >>>>>>> part of set.mm. Because the formula makes calculation based on the >>>>>>> row and column indices of the element of the matrix, I'm using matrix >>>>>>> with >>>>>>> integer indices (in contrast with the rest of the development on >>>>>>> matrices >>>>>>> which is based on arbitrary sets). >>>>>>> >>>>>>> I chose indices in ` ( 1 ... N ) ` , so that the top-left matrix >>>>>>> element is a11 (in set.mm written ` ( 1 A 1 ) ` ). It seems using >>>>>>> indices starting from one is the convention used for mathematics, I have >>>>>>> not found yet a reference with indices starting at zero (and neither did >>>>>>> Norm), however we would like to run this through the community. Most >>>>>>> programming languages start indices with zero, with the exception of R >>>>>>> and >>>>>>> several others. >>>>>>> >>>>>>> In set.mm words indices start with zero. >>>>>>> >>>>>>> What's your opinion? Should matrix indices start with one or zero? >>>>>>> >>>>>>> Thanks for your input! >>>>>>> >>>>>>> BR, >>>>>>> _ >>>>>>> Thierry >>>>>>> >>>>>>> >>>>>>> PS. I would later like to define a "literal" matrix function which >>>>>>> would be used like this to transform words (for any matrix size up to >>>>>>> 8x8) >>>>>>> into matrices : >>>>>>> >>>>>>> ( litMat ` <" <" A B C "> <" D E F "> <" G H I "> "> ) >>>>>>> >>>>>>> This would allow a bridge/conversion. >>>>>>> >>>>>> -- >>>>> >>>>> -- >>> 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/7eeabd5a-29c3-431b-aaba-87f457827d53n%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/7eeabd5a-29c3-431b-aaba-87f457827d53n%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >>> -- >>> 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/d605c6c1-20ff-3b46-228b-4645c704db08%40gmx.net >>> <https://groups.google.com/d/msgid/metamath/d605c6c1-20ff-3b46-228b-4645c704db08%40gmx.net?utm_medium=email&utm_source=footer> >>> . >>> >> -- >> 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/CAFXXJSspwoKtV5cGUwenJJ4MF4js-a_mzhVyi-7vi9KAkkJKRw%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAFXXJSspwoKtV5cGUwenJJ4MF4js-a_mzhVyi-7vi9KAkkJKRw%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> >> -- > 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/d5e41385-2659-49b1-8176-011144637d9dn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/d5e41385-2659-49b1-8176-011144637d9dn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvm%3D0YNAOj_ZF8XBvuoWbfaTEHVsymViqGnX0czV6tHhw%40mail.gmail.com.
