Hi Andrzej On Fri, 22 Sep 2006, Andrzej Trybulec wrote:
I agree that it is confusing. Even more confusing is (I often have such problem) if the registration is not in the article that already is used but in a different, sometimes very strange, place, On the other hand one have to be careful with adding new registrations, it may cause problems with the complexity and change the behavior of the 'notation' directive.But still, I often find that something does not work exactly the way it should (sometimes when I've already been working on an article for quite some time), and then after a long search it turns out that I miss some cluster from an article, which already turns out to be mentioned in one of the other directives in the environment! With a simplified way to import stuff that kind of confusion very probably wouldn't have happened.
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.
It happened. Maybe we should register such cases, or better to do some experiments. And I do not intend to agree with Josef, I just agree. The problem is with the policy. I agree with you that we do not want to have "the only correct way to write Mizar articles", (I hope I cited you precisely). With a liberal policy we must accept that some articles are not of the highest quality and one may have troubles using them.So, a question: does it ever happen that it is harmful to have _too many_ articles mentioned in the "environ". That the solution to some problem is to _remove_ an article from the registrations, say? (If that would ever happen, I would tend to say with Josef that it would be a problem with the library.)
These are two things: 1) MML policy for acceping articles 2) syntactic rules for Mizar articlesYou can emulate a lot of (2) by (1) (e.g. always have an "expert' to shuffle the notation directives properly), but at some moment we should really try to fix (2).
Of course, if differs for different directives. Maybe the most unpleasant are 'vocabularies'. E.g. with the CAT_4 vocabulary it is O.K to write 'P[y]' (in a scheme) but 'P[x]' is syntactically incorrect.
Again, there should be a limit to syntax abuse, even in Mizar.
The 'registration' directive is dangerous . It can cause very slow processing or even a combinatorial explosion.
The cluster mechanisms per se are just linear now. It may be just a matter of better data structures.
I am definitely for liberal policy. In is not the problem of freedom, we want to allow attempts to find possibly better solutions.
Yes, but not by writing a program which generates all permutations of the notation directive, and selects the one which gives no error. This is not a good degree of freedom the authors should explore.
To conclude, it is mainly of choice between the liberal policy (then I have to be able to be very precise with import from DB) or more restricted policy (quality, integrity) (then I can to construct the environment in a haphazard way). What we need is probably a compromise. So, we want the golden middle, and we have old problem: left or right.
I think a change in what the system allows would be appropriate. It should just make the maintanance of MML simpler, and importing previous articles too.
Best, Josef