[mizar] proposal for absolute notation

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

as already discussed about a year ago on this list, there are serious 
difficulties, when translating the internal (constructor) format of 
Mizar formulas back to the user-readable (and also Mizar-parsable) 
format.

The main reason for this difficulty is overloading of symbols, which  
however seems to be indispensable for any larger library of mathematics.

This means that output of many Mizar utilities working on the internal 
level cannot be used as input to the Mizar parser, which causes that a 
lot of work (revision, experimental, etc.) that could be done 
automatically, has to be done manually. 

I think that with the growth of MML, this is becoming untenable, and the 
current enormous amount of manual work, resulting from the recent 
schematizer reimplementation (not published yet), shows it very clearly.

Another big problem caused by this overloading, appears when writing 
advanced articles, that make use of a lot of previous facts from 
different parts of MML. If several meanings of an overloaded symbol are 
needed in one article, the writer has to do increasingly funny and 
complicated exercises with environment and redefinitions, to be able to 
write simple formulas. Even if such effort succeeds, it makes 
understanding of such articles difficult.

There is also a third problem connected with this, even though maybe not 
directly perceived by authors of Mizar articles now. 
MML is now the largest body of formalized mathematics, written and 
managed in an internally consistent manner, and it provides formal 
conventions for many advanced concepts. There are many other people 
working on some kind of "digitalization" of mathematics, or making use of 
it. 
When cooperating with MML, such people are mostly interested in the 
semantics of MML, which can however be only expressed in the internal 
(constructor) Mizar format. The usual approach to this format (used e.g. 
by MML Query or MPTP) is numbering of article constructors, giving names 
like "XBOOLE_0:func 1" to the empty set.
Apart from the obvious nonintuitivness of such names, they also make such 
semantic presentations very unstable across various versions of MML.
E.g. revision adding a new functor definition at the beginning of 
XBOOLE_0, make the previous semantic presentation hopelessly obsolete.


I think all these problems could be solved by adding the following simple 
MML policy rule:

Whenever a symbol is being overloaded (i.e. a new definition or 
a redefinition is introduced for symbol previously used in MML),
the author has to provide a unique (and possibly intuitive) synonym for 
it, which must not be redefined later (this could be checked by some 
simple utility).

This should solve the output-used-as-input problem, since we can always 
resort to the absolute synonym, and similarly, the absolute synonym
can be used to resolve the overloading in advanced environments.

It could also help the third (presentation) problem, because the 
absolute synonyms can be used instead of names like "XBOOLE_0:func 1", 
making semantic presentations much more understandable, and (even more 
important) much less fragile with revisions of MML.

I would also like to add some sort of a second rule, saying that the 
format of such symbols has to be uniform in some way, e.g. allowing only 
prefix notation, only alphanumeric characters and '_', or even starting 
with low letter (to conform to simple theorem proving notations ;-),
so that it is easy for others to work with such absolute notation.


Thanks for any comments,
Josef Urban