Re: [mizar] Private DB

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

Dear Andrzej,

Thank you for the long and very interesting mail.  I liked the
observations that importing too many clusters will bog the
system down so much that it becomes unusable, and also the
observation about [x] as a symbol when you want to write P[x].
(We used to have U for union, and we still have c= for
inclusion, those are similar problems, right?  How to parse
"a/b=c/d implies b*c=a*d"? :-))

But.  One more thought:

>As yet the Mizar project is quite anti-bourbakist one, we
>allow for different approaches.

I guess that Josef's point is that there really two different
levels in "experimenting with Mizar".  On the one hand there
is the MML, where more or less everyone can do whatever he/she
likes ("anti-bourabakist", yes, I like that word!)  But then
there's also the level of the pascal (delphi?) code of mizf.
And here people (even Josef!) cannot do whatever they like (or
can he?)

So example:  Suppose I would like to work in Mizar with "weak
types" (types that might not always be non-empty).  Suppose I
want to define a mode "Foo of X" that might be empty, a "weak
type".  (Maybe X is a cardinal number and "Foo of X" is the
type of all fields that have X elements.  So "Foo of 6" is the
type of fields with 6 elements (which don't exist, right?))

I can see two ways to go about it.

One is to stay on the MML level, and try to work around the
limitation by being creative.  For instance (just a random
possible approach, I don't really know whether it would work)
is to introduce a mode "Foo' of X" which really is the same as
"Foo of X", except that when Foo would be empty it contains
the empty set (the same trick used for Element).  And then I
also introdue an attribute "... is okay" on "Foo'", which
means that the object is _not_ one of those empty sets.  So
the idea is that one morally would have "mode Foo is okay Foo'",
apart from the fact that you won't be able to prove the cluster
needed for that.  Anyway, then you can write

	for x being Foo' st x is okay holds ...

every time you really would like to say

	for x being Foo holds ...

And you would get the possibility to express what you want,
and CHECKER and everything will do the right thing, as long as
you remember to put "x is okay" for every variable of type
Foo' that gets introduced somewhere.

And who knows, maybe it won't be _too_ painful (although of
course it will look incredibly clumsy.)  And who knows, maybe
when people do this often enough, it will be integrated in the
system in some way, and the system will grow and become better.

The other thing one might try to do is to "hack Mizar".  Dive
into the source code, add syntax for weak types, change the
internal data structures so they know about these weak types,
change the algorithms in CHECKER so they do the right thing
when there are weak types present, and so on and so on, and
hope you won't fuck it up too badly.  That way you won't need
clumsy tricks like this "okay" attribute, and Mizar will be
much better faster.

Now doing that will be much harder.  _I_ certainly won't be
able to do this.  But I think that Josef's point is:

You say you encourage different approaches, and it's true, you
do!  But you really do _not_ encourage it on the level of
fooling around with the mizf pascal source code.

Freek