On Wed, Sep 2, 2020 at 7:28 AM Thierry Arnoux <[email protected]> wrote:
> I’ve done a mock-up of this conversion (including index translation), you > can find it here: > http://us2.metamath.org:88/mpeuni/lmat22e11.html > That's a whole lot of boilerplate, I would hope that most of that can be broken into a lemma specialized for proving the entries of a 2x2 matrix (instantiated 4 times) and a 3x3 matrix (instantiated 9 times). I'm thinking something like: |- M = ( litMat ` S ) |- K e. NN0 |- L e. NN0 |- ( K + 1 ) = I |- ( L + 1 ) = J |- ( S ` K ) = T |- ( ph -> ( T ` L ) = X ) $p |- ( ph -> ( I M J ) = X ) But the index translation is only a small added pain in this lemma application. > On the other hand, does any one have any idea or suggestion about how I > could have expressed the Laplace expansion without integer indices, on any > finite set index? > The laplace expansion of the determinant (just one level of expansion, not recursive) requires a choice of row to expand over (which is an element of the index set), and then it's an unordered finite sum. No integers needed. Mario > > Le 2 sept. 2020 à 18:54, Mario Carneiro <[email protected]> a écrit : > > > 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 > <https://groups.google.com/d/msgid/metamath/CAFXXJSvm%3D0YNAOj_ZF8XBvuoWbfaTEHVsymViqGnX0czV6tHhw%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/1F73E402-F4BB-4446-9AA6-D0C287C40186%40gmx.net > <https://groups.google.com/d/msgid/metamath/1F73E402-F4BB-4446-9AA6-D0C287C40186%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/CAFXXJSucdngkAJ%3DRsL90v%3Dry80HRMnSN49woe1QHWHM7Akz-Fw%40mail.gmail.com.
