Re: [mizar] weak types

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

Hi Freek,

> Also, you don't get anymore from "for x holds P[]" (where x
> doesn't occur in P[]) that "P[]" itself has to hold.

Yes, this is now hard-wired at least in the checker (removing fictitious 
variables).

> >Or is there any deeper reason for avoiding them?
> 
> It would be surprising.  PVS and Coq and NuPRL all support
> types that can be empty.

One more thing to watch would be permissive definitions, like:
assume A1: contradiction;
func foo -> NonInhabitedType means ...;
correctness by A1;

But asssumption are already watched now, and e.g. forbiden 
for redefinitions, so that would cost very little. Also "the fixed type" 
could not be used, if we ever implement it.

> (So what about existential clusters? :-))

It is the same for them, though the hard-wired stuff may differ a bit for 
modes and for attributes. Actually I wrote about this, because I am lazy 
to prove one tough existential cluster, and not proving it spoils the type 
mechanism now.

> By the way: a "cheap" way to implement these "possibly empty
> types" would be to have them internally be represented by a
> predicate, and then before trying to run CHECKER replacing
> them by those predicates.  So
> 
> 	for x being Large_Cardinal_that_may_not_exist
> 	  holds ...
> 	
> would be first transformed into
> 
> 	for x being set st Large_Cardinal_that_may_not_exist x
> 	  holds ...
> 
> and then the old CHECKER would be correct (but maybe too weak?)

I think you do not have to have a special predicate, just rewriting it 
using "is" (i.e. "for x st x is Large_Cardinal_that_may_not_exist ...")
could be sufficient to prevent checker from doing the dangerous stuff.
It can be done now this way with attributes.
I think that checker is now even strong enough to do the type matching for 
universal formulas rewritten in such way, so e.g. if we wanted to prove 
"P[c]"  for some constant c having the type (or just attribute) T already, then
"for x being set st x is T holds P[x]" is sufficient for the checker.

On the other hand, maybe that the removing of fictitious variables is the 
only hard-wired obstacle, so in that case a straightforward 
reimplementation might be even cheaper (and cleaner).

Josef