[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Private DB

Hi Freek,


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 do not know what exactly you oppose, since I do not know what exactly I 
propose ;-). What I wrote earlier was about having allowed some kind of 
parametric polymorphism (variant with more special types always wins), 
possibly complemented by some global prioritizing. And getting rid of 
resolving imported notation by their order in the header.

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.

Yes, removing sensitivity of notations to their order in the header 
definitely "loses information" (and it seems to be fairly welcome loss to 
me). Parametric polymorphism prevents the "more general" variant to win 
over the "more special", which is now usually done by proper ordering of 
the notations. So yes, in some sense it prevents you from "shooting 
yourself in the leg" by bad ordering of notations. I don't know if e.g. 
prioritizing should be allowed to override this (seems fairly useless), 
and even with the existing mechanisms ("qua", "reconsider") you can do it. 
I quite agree with Andrzej that this is a matter of experimental research 
over existing MML.

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.

What I said before is that when it is from the MML experience clear that 
something is bad, we should try to restrict it in the language. Otherwise 
new (and even old) users will be puzzled by the strange Mizar behaviour 
again and again.

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?)

See mml.lar in the Mizar distro (hidden and tarski have to be prepended). 
I wrote some simple Prolog utilities for playing with this on top of MPTP 
- see 
http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/*checkout*/MPTP2/env_utils.pl.

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

I haven't tried. As I said, the worse option is that it does not stop, and 
just silently changes the semantics.

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?

I am not sure about the "definitions" directive. Otherwise there is no 
problem, maybe it is already done, I don't know.

Josef