On Tue, Jul 2, 2019 at 1:37 PM Benoit <[email protected]> wrote:
> On Saturday, June 15, 2019 at 4:42:22 PM UTC+2, David A. Wheeler wrote: >> >> On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro <[email protected]> >> wrote: >> > I would like to get away from label conventions in favor of something >> > machine readable and not hardcoded. >> >> I'm fine with adding additional mechanisms. >> However, I'd like to keep using & enforcing the label conventions. >> I find they're very helpful for the humans who are trying to read this >> stuff :-). >> And once the humans start depending on the conventions, it's wise >> to enforce the conventions so the fragile humans aren't misled. >> >> Label conventions are also "machine readable". You can make them >> not hardcoded by adding a mechanism to declare the label convention. > > > I also think that sticking as close as reasonably possible to label > conventions makes it easier to humans (and this contributes to making > metamath more attractive). > > > The mechanism I propose is: >> > >> > If an $a statement is given for a syntax typecode (i.e. not |-), then >> it >> > is a definition iff the immediately following statement is a >> definitional >> > axiom $a |- foo = ... which satisfies the usual rules. Otherwise, it is >> > treated as an axiom, and a warning is issued if the label convention >> > implies that the axiom would like to be treated as a definition and >> there >> > is no warning-suppressing pragma attached to the axiom. >> >> That's extremely strict. Even though we don't use it in set.mm today, >> I worry about being unable to escape it later. >> I'd prefer that to be the *normal* case, but with a special statement >> (say a $j) that means "it's a definition even though it's down here" >> statement. >> > > Indeed, I think that one should allow exceptions documented with a $j > statement. > To be more specific, by "warning-suppressing pragma" I mean a $j statement. Suppressing the "axiom treated as definition" warning on a particular definition has exactly the desired effect, of allowing definitions to "count" as definitions even if they don't meet any reasonable criterion for being one. > I ran into a concrete example recently: I want to eventually define > multiplication of extended complex numbers (~df-bj-mulc) from the > beginning, but in the infinite case, it requires ~clog (through complex > argument), which has to be defined much later. But this does not prevent > one to use multiplication in the finite case meanwhile. Therefore, the > whole thing would look like: > clog $a class > cmulc $a class > df-mulc $a |- > [many theorems] > df-log $a |- > There are probably several cases already in set.mm (although they should > be kept exceptional). > This is not a legal definition, this is mutual recursion which is not allowed. If you tried this in set.mm today you would get an error because mmj2 would not allow df-log to reference mulc. You would be forced to have an intermediate definition for the finite multiplication operation, even if you never use it / immediately eliminate it after the trio of definitions. Another example of this sort of thing is df-prds, which is a giant structure builder containing a number of slots that pertain to entire areas that haven't been introduced yet. We resolve this by actually moving the relevant definitions up, which is why df-topgen comes long before the first theorem that expands it, tgval. If it passes mmj2 definition checker today, then it is possible to move the df-* to immediately after the constant declaration, without breaking anything, so I know in advance that my proposal will work - we've been checking for it all along. > > > Some label changes I see (skimming through mmdefinitions.html) are: >> > > wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though >> df-bi >> > > is a special case >> > > df-v --> df-vv (to match cvv and avoid collision with cv) >> > >> > The general rule has been to make constant names as short as possible >> [...] >> > >> I think conventions are good, even if it would increase the size of >> set.mm. >> >> So I would support switching to "wDFNAME" everywhere. We've already been >> moving to increasingly keep our label names consistent with the "df-NAME" >> definitions. And while the constant names aren't usually >> visible to the user, in your lean translation they *ARE* directly >> visible, >> and they're also visible in the HTML showing definitions. >> > > I also think that having the label df-xxx correspond to wxxx or cxxx is a > good convention to stick to. As David says, the compressed size of set.mm > would not increase. > The size of set.mm would increase, because constant names appear in proof label lists. The compressed size (say with gzip) would probably only increase by a few bytes, but that's not the usual measure. I'm not going to commit to a position here, but that's at least been the historical justification for keeping the names minimal. > Side question: would you extend this rule to the $c-statements? i.e. have > blocks > $c smurf $. > csmurf $a class smurf $. > df-smurf $a smurf = ... $. > This would look more systematic. As suggested above, maybe one could also > standardize the comments, for example "Extend class notation to smurf / > Syntax for smurf / Define smurf, the function that..." ? > While I am not proposing this as part of a rigorously checked rule, I'm fine if we do this. But unlike term/definition pairs, which have to come in pairs (because any new constant requires a definition), there is no one to one relationship between $c constants and new syntax axioms. $c declarations are more about presentation, the token alphabet from which the CFG is defined. A new term can reuse old constants, or introduce new ones, so there might be no new $c's with a term (for example df-mpt2), or there might be more than one (for example df-itg). Additionally, metamath allows $c declarations to be bundled into one declaration, which makes it more convenient to declare them all in a single block. -- 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/CAFXXJSvS-oL%2BNrPx6apoBvg1r_AXwxGDVd1wKZ%2BuiBQ2NkJUCg%40mail.gmail.com.
