Re: [mizar] Private DB

[Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>]

Dear Freek,

to be honest I do not understand the whole fuss about weak types. Maybe 
because when the rule that type must be not empty I believed that it is 
small but definite achievement of Mizar. The permissiveness was 
introduced instead to give the Authors better control on what they do. 
In Mizar-3 fortunately never published :-) we experimented with 
postponing correctness conditions. In your example it was allowed to 
write something like this:

definition let x be Cardinal;
 mode Foo of X -> Field means
    Card the carrier of it = X;
end;

definition  let x be prime natural number;
 redefine mode Foo of X;
existence;
end;

definition let x be infinite Cardinal;
 redefine mode Foo of X;
existence;
end;

but then processing original 'Foo of X' was a nuisance.     

So, what we do? Instead of introducing mode with possibly empty types we 
use permissive definition of the form

definition let l_1, ..., l_k;
 assume
Z:  meaningfulness_of_Foo_for L_1, ..., l_k;
   mode Foo of L_1, ..., l_k;
 existence by Z;
end;

and the same redefinitions as above. Let us look to examples (NATTRA_1):

definition let A,B be Category, F1,F2 be Functor of A,B;
pred F1 is_transformable_to F2 means
 for a being Object of A holds Hom(F1.a,F2.a) <> {};
reflexivity by CAT_1:56;
end;

definition let A,B be Category, F1,F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2;
mode transformation of F1,F2 ->
        Function of the Objects of A, the Morphisms of B means
:Def3: for a being Object of A holds it.a is Morphism of F1.a,F2.a;
existence
 proof
   ....
 end;
end;

Please observe  that automatically generated predicate 
'meaningfulness_of_Transformation_for F1,F2' would be rather
      ex f being  Function of the Objects of A, the Morphisms of B
        st for a being Object of A holds it.a is Morphism of F1.a,F2.a
much more complicated than necessary. So, it is better that Author can 
control what the 'guarding' predicate is.

I remember that I was unhappy with this (particularly because I had to 
repeat this for natural transformations). I think it is psychological 
problem: we do not want to repeat the same routine job.

If one writes about transformations of F1,F2 one wants of course F1 
being transformable to F2. With an explicit guarding predicate we 
sometimes may omit an assumption:

    for F1,F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to 
F3 holds ...

'F1 is_transformable_to F3' is not necessary  because the predicate is 
transitive (NATTRA_1:19 :-))

I was looking for a better example, e.g.

    definition let G,H be Group;
       assume
Z:      G,H are isomorphic;
       mode  Isomorphism of G,H means ....;
       existence by Z;
    end;

but I did not found. So, it seems that even experienced Mizar Authors 
are reluctant to use the mechanism. I wonder why?
Maybe we have to talk more about the permissiveness, to get better 
understanding of it.

Albeit, it is not practical problem (if we have weak types) but rather 
matter of taste.
    
Regards,
Andrzej

Freek Wiedijk wrote:

> 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?))
>
> 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.
>
>