Re: [mizar] Private DB

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

Hi Freek,

> > The only ambiguity is whether "copy FOO" should only import
> > the environment declarations of FOO, or also the theorems,
> > clusters, etc. introduced in FOO (btw., the "vocabularies"
> > directive is already now pretty inconsistent with the rest of
> > directives in this sense). So perhaps "needs", "import", or
> > "include" could be less ambiguous (hopefully being understood
> > as including FOO as well)?
>
> Maybe "extends"?

Yes, sounds good to me.

> > I sincerely hate this sensitivity of "notations" (and
> > "definitions") to the ordering of directives. In my opinion,
> > something is wrong with the article, if such tweaking is
> > needed.
>
> I don't know: redefinitions are often used to make the typing
> of operations more specific, and those redefinitions have to
> come after the original definition too.  That's a matter of
> ordering on the notations as well, I think?

Here is an example of traditionally painful thing - the result type of 
intersection. You can have:

let A,B be set;
func A /\ B -> set; ::Def1 of /\_1

then you can have

let A,B be set;
redefine func A /\ B -> set;  ::Def2 of /\_2
commutativity;

Let's say that if for whatever reason (e.g. the proof was too difficult 
at the moment) you did not prove commutativity for Def1, then it is a good 
idea that Def2 completely shadows Def1 (i.e. there is no way how to refer 
to /\_1 after Def2). That's quite reasonable. Actually, if Def2 is in 
other article than Def1, and you put the directives in the wrong order, I 
suspect that you might end up using /\_1 (I am not completely sure 
though).

Then there can be:

let X,A be set; let B be Subset of X;
redefine func A /\ B -> Subset of X;  ::Def3 of /\_3

let Y,B be set; let A be Subset of Y;
redefine func A /\ B -> Subset of Y;  ::Def4 of /\_4

or even

let A,B be set;
redefine func A /\ B -> Subset of A; ::Def5 of /\_5

let A,B be set;
redefine func A /\ B -> Subset of B; ::Def6 of /\_6

(some of them might be redundant in presence of commutativity (not sure), 
but let's pretend it's not commutative now)

Then the possible cases are:

1) A,B are just sets - then /\_1 or /\_2 is used ... OK
2) A is set, B is Subset of X - the /\_3 is used, provided the notation 
directive for Def3 comes after those for Def1 and Def2; if not, Def3 will 
not be used
3) the same for B being set and A being subset of Y (and Def4 instead of 
Def3)
4) A is Subset of X, B is Subset of Y - what should be used now?? again, 
"anything goes", depending on the ordering of directives
5) Def5 or Def6 should probably shadow Def1 (resp. Def2), but what is the 
order of shadowing between Def5 and Def6??

My point is that while parametric polymorphism is probably quite natural 
(and many people know it from programming languages), this "directive 
order driven" resolving of overloading is fairly unreadable. Unless you 
are satisfied with what prof. Solovay recently described as "kicking the 
system in the right way, and hoping for the best" :-) (which is what this 
monkey-like shuffling of notation directives exactly is).

So I'd much rather like to be warned (and stopped) by the system when I 
write something possibly ambiguous, and forced to rephrase it in readable 
notation.

Best,
Josef