Re: [mizar] Once more: empty types

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

Hi Piotr,

Thanks for answering my mail.  So I _was_ right that _only_
me and Josef seem to think that the non-emptiness is a
real problem...

> - I have never run into a situtation when a possibly
>   empty type would make a formalization more natural.

Really!  The "Element of" weirdness doesn't bother you?
And, for instance, you don't think that "Function of A,B"
should be an empty type when B is empty but A is not?  Or,
another random example, in algebra (or in category theory,
for that matter), the type called "Homomorphism of A,B":
what if there _is_ no homomorphism?  (Or do you think that
there always is a homomorphism between algebraic structures?)

Or take for instance, when I formalized Newman's Lemma (see
section 6 of <http://www.cs.ru.nl/~freek/notes/sketches1.pdf>),
then I _very much_ wanted to have a type of "NormalForm of A"
for A in an abstract reduction system.  But the problem of
course then was that A in general does not need to _have_
a normal form...

Or (to slightly differently make the point about Element
and Function) take the redefinition from the start of my
recent article about Arrow's theorem:

definition
 let A,B' be non empty set;
 let B be non empty Subset of B';
 let f be Function of A,B;
 let x be Element of A;
 redefine func f.x -> Element of B;
end;

Why the hell are all those "non empty"s there?  Don't you
think that I hate my work when I submit an article with
an articificial restriction like that in it?  This should
true for _any_ set A and B!  And it's not just _me_ that
has these crazy non emptinesses in there.  In FUNCT_2 I find

definition let C be non empty set, D be set; let f be Function of C,D;
  let c be Element of C;
  redefine func f.c -> Element of D;
end;

Which is exactly the same lack of generality.

So what generally happens to me when I try to work with
Mizar is that I think: "Ah, this is nice, I can have a nice
mode for this concept!"  And then only when I start proving
the existence correctness condition do I realize that,
"Oh, I forgot!  For some arguments it actually won't be
non empty!  Aaargh, this is stupid!  It _shouldn't matter_
that it is not _always_ non empty!"  And then I again and
again consider dropping Mizar altogether, and permanently
move a system that is more elegant.

But of course I come back to Mizar anyway.  Despite this
very irritating ugliness of types having to be non empty (and
some other irritations), it is a seductive system anyway.

>   The discussion from a year ago was inconclusive as
>   I did not see answers to Andrzej's arguments how to work
>   around possibly empty types.

The answer is that one can work around _anything,_ but
that that doesn't make it pleasant.  Nor does it even make
it acceptable, really.  You can do arithmetic with Roman
numerals, but that doesn't prevent the positional notation
for numbers from being much better.  You might do set theory
without having an empty set, and work around _that._ But
I don't want to calculate with Roman numerals, or have set
theory without the empty set.  Or have a type system that
does not allow me to define the types in a natural way.

> - Changing anything in the Mizar verifier is a problem since there
>   are so few people that can modify the code (I am not one of them). 

Now that's the _real_ problem, I agree.  I don't know a
solution to this.  _Some_ people would say that if only
Mizar were open source, this might not be a problem, but I
don't agree with that.  (The Coq source _is_ open, and there
are only a few who can modify that code as well.  I think.)

So I can imagine that Josef might be able to do this
(you did not mean "can" as in "is allowed to", right?),
but I'm not sure about that either.

I can imagine, though, trying to figure out what needs to
be changed in CHECKER (the way I understand how it works,
from Andrzej's explanations) without actually implementing
it in the system.  It still might be a small step in the
right direction.

Freek