Work variable syntax

[Marlo Bruder]

Hello metamath community,

I'm still working on my upcoming mmj2 inspired proof assistant called mmt1 and I am now getting around to implementing work variables. This got me thinking about the design of work variables in mmj2 and I wanted to share some thoughts with you.

First, what happens when a database has a symbol declared that is the same as a work variable (e.g. &W1)? Does the symbol become unusable or will mmj2 stop treating it like a work variable?

Second, what happens when multiple typecodes start with the same letter? Will they have different looking work variables?

Third, what happens when a typecode starts with a number or a non-letter symbol? This doesn't necessarily break the design, but it could make for some weird looking work variables.

Note that the questions above are more or less rhetorical and if you don't happen to know the answers I wouldn't recommend looking for them, as that could take some time. What I am more interested in is what you guys think a proof assistant SHOULD do.

To me it almost seems that you would have to completely redesign the syntax of work variables to fix these issues. One way would be to change the & to a $, so that you can't define symbols that look like work variables. Then you could change the capital first letter of the typecode to allowing any variable with that typecode. This then leads to another problem: What if a variable ends in a number? To solve this you could move the dollar between the variable and the work variable number. This would then give you work variables like: ph$1, x$2, A$3.

This leads me to my main set of questions: Would you prefer this more universal syntax over the old one? Are the problems I described so rare that it all doesn't really matter. What should the proof assistant do if a database nevertheless has these problems? Just reject it?

Thanks for any answers in advance!
Marlo Bruder

[Glauco]

Here

yamma configuration for working vars

you can see how yamma allows the user to configure prefixes for working variables.

Since this is theory-dependent, in principle you could also use a $j comment in a .mm file to suggest such prefixes.  

[Jim Kingdon]

> What I am more interested in is what you guys think a proof assistant SHOULD do.

Any of the proposals in your message sound fine to me. The mmj2 system doesn't seem to constrain the way we can name things in set.mm enough to seem like a problem to me, but some of the other options seem also aesthetically pleasing enough and a bit more elegant in terms of avoiding the potential for name conflicts.