Order of variables in DV statements

[Alexander van der Vekens]

$d statements (disjoint variable restrictions) can contain two or more variables (wff, setvar and class variables). The order of them is arbitrary, but it could be helpful to have conventions how they should be ordered. These conventions should be also implemented in the tools which create $d-statements.

Until now, it seems that there are the (unwritten) conventions that class variables and wff variables should be at the beginning or the end, and that setvar variables are alphabetically ordered.

* In the Metamath book and  https://us.metamath.org/mpeuni/mmset.html#distinct, class variables and wwf variables are always at the end.

* mmj2 creates d$ statements with class variables and wwf variables at the beginning.

* the html pages for the theorems display class variables and wwf variables at the beginning.

mm-lamp, however, seems to create $d statements in arbitrary order (at least it puts class variables in the middle, see ~ cplgredgex, and does not always order the setvar variables alphabetically).

In my opinion, we should fix the conventions (in section "Conventions" in set.mm) that:

* each $d statement should contain at most one class or wff variable

* the class variable and the wff variable should be at the beginning or the end

* that setvar variables should be alphabetically ordered

The tools should respect these conventions.

[Mario Carneiro]

IMO class/wff variables should come at the beginning, with the list of setvars being read as a (non)dependency specification for the class/wff variable. I most recently visited this question for mm-web-rs, which does not put the class/wff variables first - it just sorts all the variables, meaning classes come first but "ph" comes between "p" and "q" - because you need to be set.mm specific to treat class/wff variables differently from other variables. This is likely to be a problem for other metamath processors which try not to be set.mm specific, unless we introduce a new $j command or interpret an existing one as a way to say that setvars come after other things.

But also, this is not a thing that users should ever have to think about. It should be implemented in the set.mm formatter so that even if an authoring tool comes up with a weird order it is automatically normalized. (But tools should also strive to honor the default convention because it's best if the formatter doesn't need to do anything.)

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a976c123-c431-4ec8-a3a2-f14c5ff88527n%40googlegroups.com.

[BTernary Tau]

I've filed a feature request for metamath-lamp to follow mmj2's behavior: https://github.com/expln/metamath-lamp/issues/172

[Igor Ieskov]

Metamath-lamp version 20 supports reordering of variables in DV conditions.

Variables are ordered by type and name. Ordering by type may be customized on the Settings tab by the "Sort disjoint variables by type" setting. It contains space separated list of types in the order which should be used in DV conditions. Omitted types will be placed at the end of DV conditions. By default, it is "class wff".