Re: [mizar] Private DB

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

>That's why I am suggesting to have some reasonable
>restrictions on the allowed kinds of overloading, and change
>the resolving mechanism. It is too wild now.

I think I really do oppose this.  I don't think that changing
this aspect of the language will make Mizar more attractive.
It will make it more understandable, yes, maybe, but it also
will make it much less flexible and powerful and interesting.

>Again, there should be a limit to syntax abuse, even in Mizar.

It seems to me that this should be about the MML, and not
about the Mizar language.

>Yes, but not by writing a program which generates all
>permutations of the notation directive, and selects the one
>which gives no error.

I think that there is a "canonical" partial order on the MML
articles through the way the refer to each other in environ
references.  So then you could run a "topological sort" on
that (see the "tsort" program in unix), i.e., find a total
order that is compatible with that partial order.   I guess
that the order in which they are submitted to MML is such a
total order that is compatible with this partial order?  Let's
call this "MML order".  (Which article is first in this order?
TARSKI?)

So does it ever happen that a Mizar article _stops_ working
when one puts the notations directive in that specific MML
order?

Could one write a small program that reorders the notations to
have that specific order (so it won't touch the rest of the
article, but just change the order of the notations
directive)?  Or maybe have it put _all_ directives in this
order (to make the environ a bit nicer) as I think that for
all the directives _but_ notations the order is irrelevant?

Freek