Need for additional class variables

[Alexander van der Vekens]

While I am working on theorems for matrices and polynomials, I have increasing problems to find adequate class variables to formulate the theorems appropriately. The available capital letters seem to be not sufficient anymore. Therefore I would like to propose to add additional class variables to set.mm.

In my latest pull request, I made already a proposal for such an extension:

  $( Declare variable symbols that will be used to represent classes which are
     elements of a collection or of a base set of an extensible structure,
     often having the same name. These variables should only be used for sets
     which are required in assumptions, i.e. either in antecedents, e.g.
     ` ( ( ph /\ .a. e. A ) -> ps ) ` , or in essential hypotheses
     ($e statements), e. g. ` $e |- ( ph -> .a. e. A ) $. ` .  Another use
     case for these variables is a situation in which variables are substituted
     by classes, e.g. on expanding definitions given as mappings:
     ` def $e |- I = ( p e. L |-> V ) $. ` and
     ` defval $p |- ( ( ph /\ .p. e. L ) -> ( I ` .p. ) = ... ` .  As a
     concrete example, see ~ mply1topmatval : In this example the class
     variable ` P ` is already in use, so the new class variable ` .p. ` can be
     used to substitue the set variable ` p ` used in the definition. $)
  $v .a. $.
  $v .b. $.
  $v .c. $.
  $v .m. $.
  $v .p. $.

  $( Let ` .a. ` be a class variable. $)
  csA $f class .a. $.

  $( Let ` .b. ` be a class variable. $)
  csB $f class .b. $.

  $( Let ` .c. ` be a class variable. $)
  csC $f class .c. $.

  $( Let ` .m. ` be a class variable. Usually used for representing a matrix:
     If ` A = ( N Mat R ) ` is the algebra of N x N matrices over (a ring)
     ` R ` and ` B = ( Base ` A ) ` is its base set (i.e. the set of all N x N
     matrices over ` R ` ), then ` .m. e. B ` is a special N x N matrix over
     ` R ` . $)
  csM $f class .m. $.

  $( Let ` .p. ` be a class variable. Usually used for representing a
     polynomial: If ` P = ( Poly1 ` R ) ` is the algebra of (univariate)
     polynomials over (a ring) ` R ` and ` B = ( Base ` P ) ` is its base set
     (i.e. the set of all univariate polynomials over ` R ` ), then
     ` .p. e. B ` is a special univariate polynomials over ` R ` . $)
  csP $f class .p. $.

The two dots are taken from the approach for class variables representing constants and operations (like .0. and .X. ), but also only one dot could be used (e.g. .a analogous to .+ ).

Furthermore, I vacilate between using lower case or capital letters ( .a. versus .A. ) - lower case letters suggest that the represented classes should be sets, but capital letters make clear that these are variables for classes.

I think the five additional variables should be enough for the moment (actually I only need .m. and .p. for my current work).

Is there anybody else needing more class variables? How should they look like? Is my proposal acceptable, or is one of the alternatives preferred?

If accepted, the 5 class variables could be moved from my Mathbox into the main part (to the top of section "Class abstraction", where the other variables are declared, or into sections of the topics for which they are mainly used).

Alexander

[David A. Wheeler]

On Sat, 19 Oct 2019 08:05:37 -0700 (PDT), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:
> While I am working on theorems for matrices and polynomials, I have
> increasing problems to find adequate class variables to formulate the
> theorems appropriately. The available capital letters seem to be not
> sufficient anymore. Therefore I would like to propose to add additional
> class variables to set.mm.

Adding new class variables seems reasonable enough, we've done it before.
The last time we did it I think it made many things clearer.

> Furthermore, I vacilate between using lower case or capital letters ( .a.
> versus .A. ) - lower case letters suggest that the represented classes
> should be sets, but capital letters make clear that these are variables for
> classes.

I think we all agree that we should strive for clear notation.

I worry that the lower-case letters might be misunderstood as set variables.
So I would think that capital letters would be better, since these are new symbols
for class variables. But I'd be curious what others say.

More importantly: How would these *display* as in HTML and LaTeX?
Is the idea that these would have dotted underlines like .+ ?
In that case, I suspect that the new variables won't be obviously distinct enough
from other class variables. Other options include solid underscores,
double-underline, and boxes, and I suspect there are many others.

I think adding new class variables is probably a good idea, I just want
them clearly distinct from set variables & other symbols.

--- David A. Wheeler

[Benoit]

Not an answer, but a few remarks:

* The need for more than 26 variables may be a symptom of another problem than notation.  Can you give an example of a statement where you need them ?

* A common habit in math is to name variables with primes or indices, e.g. A' , A'' , A0 (displayed $A_0$), A1 etc.  Looks like someone already did that (see us2.metamath.org/mpeuni/mmascii.html).

* You write you prefer lower case to denote terms which are always sets, but I prefer to use the above "decorations" (primes and indices) to stay closer to other class variables.  And also: there is a confusion which was encouraged by the choice of words "set / class" for the types.  I insisted to change this, and now it is " setvar / class" (already better, but I had proposed "var / class" to really stop this confusion).  The real distinction is "variable versus term" (in Mario's metamath 0, this is "pure versus strict").

* Finally, I see in your mm-comments "Usually used for representing a..." but this is not enforceable and I think it is illusory to want future contributors (human or computer ones) to use $M$ for a matrix or $P$ for a polynomial, etc.

Benoit

[David A. Wheeler]

On Sat, 19 Oct 2019 09:11:36 -0700 (PDT), Benoit <benoit...@gmail.com> wrote:
...

> * A common habit in math is to name variables with primes or indices, e.g.
> A' , A'' , A0 (displayed $A_0$), A1 etc. Looks like someone already did
> that (see us2.metamath.org/mpeuni/mmascii.html).
>
> * You write you prefer lower case to denote terms which are always sets,
> but I prefer to use the above "decorations" (primes and indices) to stay
> closer to other class variables.

These are in the Mathbox for Jonathan Ben-Naim.
I also prefer the idea of using primes and indices if you want additional
variables, *especially* if they have some kind of relationship with another variable
(e.g., A and A' are likely to be related somehow).
It's the same as usual math practice *AND* it's clear; that sounds awesome.

If this is the intended direction, I recommend that we look at
promoting those items from
Jonathan Ben-Naim's mathbox, under the general rule that things generally get
promoted once someone wants to use something from someone else's mathbox.

> * Finally, I see in your mm-comments "Usually used for representing a..."
> but this is not enforceable and I think it is illusory to want future
> contributors (human or computer ones) to use $M$ for a matrix or $P$ for a
> polynomial, etc.

I'm perfectly happy to use variable name conventions if they help make things clear.
Sure, the verifier won't enforce them, but that's not critical.
Human readers could use all the help they can get :-).

--- David A. Wheeler

[Alexander van der Vekens]

Thanks a lot for your remarks. Below my comments:

On Saturday, October 19, 2019 at 6:11:36 PM UTC+2, Benoit wrote:

Not an answer, but a few remarks:

* The need for more than 26 variables may be a symptom of another problem than notation.  Can you give an example of a statement where you need them ?

The number of available variables is not the problem (within a single theorem). I try to use the same variable for the same concept for related theorems, and that is currently difficult.

* A common habit in math is to name variables with primes or indices, e.g. A' , A'' , A0 (displayed $A_0$), A1 etc.  Looks like someone already did that (see us2.metamath.org/mpeuni/mmascii.html).

Great, I didn't notice that there is already an approach in my intended direction. We should proceed with this, as David also proposed. I thought about maring the alternative variables by a bar above the letter, but primes or indices will also do. Considering primes, however, I am afraid that they can be confused with the accent grave used for function values, e.g. ( F' ` x' ).

* You write you prefer lower case to denote terms which are always sets, but I prefer to use the above "decorations" (primes and indices) to stay closer to other class variables.  And also: there is a confusion which was encouraged by the choice of words "set / class" for the types.  I insisted to change this, and now it is " setvar / class" (already better, but I had proposed "var / class" to really stop this confusion).  The real distinction is "variable versus term" (in Mario's metamath 0, this is "pure versus strict").

I completely agree.

* Finally, I see in your mm-comments "Usually used for representing a..." but this is not enforceable and I think it is illusory to want future contributors (human or computer ones) to use $M$ for a matrix or $P$ for a polynomial, etc.

Maybe we should not prescribe/restrict the usage at the place where the new variables are defined, but we can provide conventions which variables to use for which concept for a special topic, e.g. "If ` A = ( N Mat R ) ` is the algebra of N x N matrices over (a ring) ` R ` and ` B = ( Base ` A ) ` is its base set (i.e. the set of all N x N matrices over ` R ` ), then special N x N matrix over ` R ` (i.e. elements of ` B ` ) should be denoted by `M ` ,  ` M' ` , ` M" ` , ` M0 ` or ` M1' `. 

Benoit

[Alexander van der Vekens]

See also my comments on Benoit's remarks.

I think we agree on providing additional class variables in general. So how should we proceed? Shall we move all variables from Jonathan Ben-Naim's Mathbox to the main part? I think this would be too much (for the moment). Maybe we could move the class variables with one and two primes ( A' ,... , A" , ...) , and with the indices 0 and 1 (A0, ..., A1, ...) first.

On Saturday, October 19, 2019 at 6:24:53 PM UTC+2, David A. Wheeler wrote:

[David A. Wheeler]

On October 19, 2019 3:46:06 PM EDT, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>See also my comments on Banoit's remarks.

>I think we agree on providing additional class variables in general. So
>how
>should we proceed? Shall we move all variables from Jonathan Ben-Naim's
>
>Mathbox to the main part? I think this would be too much (for the
>moment).
>Maybe we could move the class variables with one and two primes ( A'
>,... ,
>A" , ...) , and with the indices 0 and 1 (A0, ..., A1, ...) first.

I think we should 1st agree on what should be moved, and then move them.

I'm a little leery of the indices, because there are other indices. We might eventually want to have a generalized way to write an index.

I propose that we start with the A' and A" collections (prime and double prime). What do others think?


--- David A.Wheeler

[Norman Megill]

If we do add more variables, I think we would want to keep using lowercase for setvar variables and uppercase for class variables, so that the only difference is the decoration.  The colors are hard for some people to distinguish, and knowing that lower/upper case means setvar/class is important.  (We make an exception with symbols-as-class-variables, but we have the dotted underline to indicate that, after long discussions about the problem.)

While I will agree that decorated variables can be useful in certain carefully chosen situations, overall I tend to dislike them except as a last resort.  I think they can be abused in subtle ways that can be detrimental.  If we do make them official, I would prefer that they be moved up from JBN's mathbox on an as-needed basis rather than doing a blanket move of the whole JBN collection.

There is a fine line between decorated variables being helpful and being confusing.  Maybe I have mild dislexia or something, but when I see a complex expression full of x, x', x'' I sometimes tend to see a jumble of x's and have trouble keeping them mentally distinguished.  On occasion I've actually rewritten (on paper) a complicated published expression with x, x', x'', using x, y, z in order to grasp the whole expression more clearly.  In a Metamath proof, an individual step can sometimes be very long, and (for me) the difficulty of reading a long expression would grow considerably if it used only x, x', x''.

Here's what I wrote in an email in 2009:

  ...we probably disagree about primed and subscripted variables.  I see
  them as a "last resort" when we run out of letters, and such a theorem
  is very rare (has never occurred in the main set.mm).  For "symmetry"
  [that you mention] I just group the letters; instead of x and x', I just
  use x and y, etc.  Sometimes [...] if I'm just consulting a book section
  quickly, I might have to dig back in the book to see if [a primed
  variable] is just a variable name or an operation.  Similarly for
  subscripted variables, which are normally used for members of a sequence
  - basically I find them mildly distracting in a textbook when overused,
  and it can be visually easier to distinguish i and j rather than i_1 and
  i_2 with tiny subscripts.

There are a couple of minor impacts on metamath.exe I'll mention.

For many years set.mm had maybe a dozen of each of the 3 variable types.  In 'show statement .../full', the list of "optional" variables available was small, and everything would usually fit conveniently on a terminal screen.  In 2010, all 26 letters were added for setvar and class variables; the /full list became much larger but still tolerable.  If we add the JBN variables, /full becomes rather annoying, as you can see with any theorem after JBN's mathbox, requiring scrolling through several screenfuls.  Perhaps /full isn't used much and most people may not care, but it is one side effect of adding more variables that we should at least be aware of.

Another small issue is that metamath.exe was written without anticipating a large number of variables, and the list of all (active) variables available in the current scope is reproduced for every $p statement so that they can be available in case a dummy variable is needed by the proof.  There are better ways to store this, of course, but it is not a simple change to the program.  Originally, the memory overhead to hold the active variables this way was small.  Now, with 30K $p statements, each additional variable near the beginning of set.mm incurs 30K x 8 = 1/4 MB of overhead.  This is one of the reasons JBN's mathbox was moved near the end.  Maybe this is a minor issue with today's CPU speeds and memory, but I thought I would mention it.

Norm

[Alexander van der Vekens]

Thank you, Norm, for this background information. I see the risk of a misuse of additional variables, and I also had concerns about using the primes ', " (which can be confused with the grave accent grave ` ).

My initial intend was to use special variables for special cases.

One of these cases (replacing a setvar variable in a definition by a class variable in a corresponding theorem) is described in my initial posting: ` def $e |- I = ( p e. L |-> V ) $. ` , ` defval $p |- ( ( ph /\ .p. e. L ) -> ( I ` .p. ) = ... ` . If P is not used elsewhere, it can be used instead of .p., but if it is already used, it is a littel bit strange to use P' in this case: ` defval $p |- ( ( ph /\ P' e. L ) -> ( I ` P' ) = ... ` .

Another case would be the need for class variables of the same kind, e.g. "Let ` M e. ( Base `` A ) `and ` M' e. ( Base `` A ) ` be two matrices ... ". Here, the "prime" solution is adequate, but could cause the difficulties explained by Norm.

A third case is the usage of setvar variables in antecedents/hypotheses, see, for example, ~ gsumcom3:

    gsumcom3.n $e |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) )

Here, j and k should be replaced by J and K or, if J and K are already in use, by J' and K'. I often thought that there is a theorem which could help me proving my theorem, until I find out that it requires setvar variables in its hypotheses, but in my case there is a class expression at this place - I have to revise/reprove the concerned theorem, or I have to perform a transfomation of the class (expression) into a setvar. Maybe it is not a good idea to allow free setvar variables in hypotheses/antecedents at all, because these could always cause such problems. But this is a different topic.

As a concrete example, in which I am running out of adequate available variables, are theorems about matrices having polynomials as entries. For these theorems, I use the following capitel letters as class variables with fixed meaning (in addition I also use symbols-as-class-variables for certain operations):

• ` R ` : represents a ring.
• ` B = ( Base `` R ) ` is its base set
• ` P = ( Poly1 `` R ) ` is the polynomial algebra over (the ring) ` R `
• ` K = ( Base `` P ) ` is its base set
• ` Y = ( var1 `` R ) ` is its variable
• ` E = ( .g `` ( mulGrp `` P ) ) ` is its exponentiation

• ` A = ( N Mat R ) ` is the algebra of N x N matrices over (the ring) ` R `.
• ` M = ( Base `` A ) ` is its base set
• ` C = ( N Mat P ) ` is the algebra of N x N matrices over (the polynomial ring) ` P `.
• ` D = ( Base `` C ) ` is its base set
  
• ` Q = ( Poly1 `` A ) ` is the polynomial algebra over (the matrix ring) ` A `.
• ` L = ( Base `` Q ) ` is its base set
• ` X = ( var1 `` A ) ` is its variable
• Z: Zero (if .0. is already used)
  
• O: One ( if .1. is already used)
  
• T: Transformation (e.g. of a matrix consisting of polynomials into a polynomial with matrix coefficients)
  
• F: diverse auxiliary mappings
• I,J: integers (indices, sum variables, etc)

That means only 7 letters are remaining: CGHSUVW. Usually, V and W are used for arbitrary classes, indicating that certain classes are sets (e.g. ` ( X e. V -> ... ) `), so only 5 capital letters are actually remaining: CGHSU. This means there is no large choice for concrete objects like matrices and polynomials to be represented.

Maybe a mechanism for local class variables (only visible/usable within the scope in which they are defined) could be helpful, but this would be a too heavy conceptual change of the metamath system, at least for the moment.

As a conclusion, I would propose not to provide additional class variables in general at the moment. As a first step, it may be helpful to provide a table listing all class variables (including the symbols-as-class-variables) and explainig for which mathematical concept they are used commonly/frequently. We can put this table into section "convention", adding the advice to use the shown variables for the indicated concept whenever possible/adequate. My list shown above could be a part of such a table...

[Mario Carneiro]

On Sun, Oct 20, 2019 at 5:19 AM 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

Thank you, Norm, for this background information. I see the risk of a misuse of additional variables, and I also had concerns about using the primes ', " (which can be confused with the grave accent grave ` ).

My initial intend was to use special variables for special cases.

One of these cases (replacing a setvar variable in a definition by a class variable in a corresponding theorem) is described in my initial posting: ` def $e |- I = ( p e. L |-> V ) $. ` , ` defval $p |- ( ( ph /\ .p. e. L ) -> ( I ` .p. ) = ... ` . If P is not used elsewhere, it can be used instead of .p., but if it is already used, it is a littel bit strange to use P' in this case: ` defval $p |- ( ( ph /\ P' e. L ) -> ( I ` P' ) = ... ` .

I would just use P for this, and plan around it so that I don't have to use P elsewhere. It's not especially important that all variables be one-letter abbreviations of something; consistency across multiple statements is more important.

Another case would be the need for class variables of the same kind, e.g. "Let ` M e. ( Base `` A ) `and ` M' e. ( Base `` A ) ` be two matrices ... ". Here, the "prime" solution is adequate, but could cause the difficulties explained by Norm.

As Norm suggested, this could be M and N. This is what "variable pairs" are about.

A third case is the usage of setvar variables in antecedents/hypotheses, see, for example, ~ gsumcom3:

    gsumcom3.n $e |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) )

Here, j and k should be replaced by J and K or, if J and K are already in use, by J' and K'. I often thought that there is a theorem which could help me proving my theorem, until I find out that it requires setvar variables in its hypotheses, but in my case there is a class expression at this place - I have to revise/reprove the concerned theorem, or I have to perform a transfomation of the class (expression) into a setvar. Maybe it is not a good idea to allow free setvar variables in hypotheses/antecedents at all, because these could always cause such problems. But this is a different topic.

It is almost always the case that set variables in an antecedent are there because they have to be. It's not an equivalent theorem if you replace j with J here, it is stronger, and often not true.

In the deduction style, something like

|- ( A. x e. A ps -> ch )

can be rewritten as

$e |- ( ( ph /\ x e. A ) -> ps )

$a |- ( ph -> ch )

You can easily convert between ( ( ph /\ x e. A ) -> ps ) and ( ph -> A. x e. A ps ) using ralrimiva and r19.21bi. They are equivalent as hypotheses. By contrast,

$e |- ( ( ph /\ X e. A ) -> ps )

$a |- ( ph -> ch )

is equivalent to

|- ( ( X e. A -> ps ) -> ch )

which is not at all equivalent and is usually useless, because it is unlikely that the hypothesis X e. A holds so it can't be used in the proof.

As a concrete example, in which I am running out of adequate available variables, are theorems about matrices having polynomials as entries. For these theorems, I use the following capitel letters as class variables with fixed meaning (in addition I also use symbols-as-class-variables for certain operations):

• ` R ` : represents a ring.
• ` B = ( Base `` R ) ` is its base set
• ` P = ( Poly1 `` R ) ` is the polynomial algebra over (the ring) ` R `
• ` K = ( Base `` P ) ` is its base set
• ` Y = ( var1 `` R ) ` is its variable
• ` E = ( .g `` ( mulGrp `` P ) ) ` is its exponentiation

• ` A = ( N Mat R ) ` is the algebra of N x N matrices over (the ring) ` R `.
• ` M = ( Base `` A ) ` is its base set
• ` C = ( N Mat P ) ` is the algebra of N x N matrices over (the polynomial ring) ` P `.
• ` D = ( Base `` C ) ` is its base set
  
• ` Q = ( Poly1 `` A ) ` is the polynomial algebra over (the matrix ring) ` A `.
• ` L = ( Base `` Q ) ` is its base set
• ` X = ( var1 `` A ) ` is its variable
• Z: Zero (if .0. is already used)
  
• O: One ( if .1. is already used)
  
• T: Transformation (e.g. of a matrix consisting of polynomials into a polynomial with matrix coefficients)
  
• F: diverse auxiliary mappings
• I,J: integers (indices, sum variables, etc)

That means only 7 letters are remaining: CGHSUVW. Usually, V and W are used for arbitrary classes, indicating that certain classes are sets (e.g. ` ( X e. V -> ... ) `), so only 5 capital letters are actually remaining: CGHSU. This means there is no large choice for concrete objects like matrices and polynomials to be represented.

Do all of these appear simultaneously in the same theorem? You can still achieve consistent naming while double-booking some of the letters, as long as they don't appear together in the same statement (and even in this case it might be worth it to sacrifice some consistency locally due to a naming conflict). V and W can certainly be double-booked, they can be used for vector spaces or individual vectors, and other letters can be used as arbitrary classes if necessary - that's a pretty low priority naming convention.

Maybe a mechanism for local class variables (only visible/usable within the scope in which they are defined) could be helpful, but this would be a too heavy conceptual change of the metamath system, at least for the moment.

As a conclusion, I would propose not to provide additional class variables in general at the moment. As a first step, it may be helpful to provide a table listing all class variables (including the symbols-as-class-variables) and explainig for which mathematical concept they are used commonly/frequently. We can put this table into section "convention", adding the advice to use the shown variables for the indicated concept whenever possible/adequate. My list shown above could be a part of such a table...

While I am okay with using such a table as documentation, it should not be considered binding. The "conventions" I am talking about re: naming are all locally defined, generally within a single section, and I wouldn't want to tie peoples' hands with a rigid global convention, especially if it paints people into a corner, as you seem to be.

I've never had issues with needing many variable names, but this may be a consequence of my laissez-faire attitude to variable name assignments. As long as you have at most 26 variables, you can make it work (and with symbol variables it's even more than that).

I think it's too late for local variables in metamath. I agree with the sentiment, but the verifier support is spotty and the metamath language doesn't lend itself well to this style without a whole lot of verbosity. Insert plug for MM0 that anticipated this problem and uses local variables everywhere, so that you can actually have variables with *names* like "pos" or "start" or "len".

Mario