[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Private DB





Hi Andrzej,

we probably should attempt to have some digest from the previous discussions on this topic (wiki is good for that), otherwise we'll just repeat the previous arguments over and over.

On Wed, 27 Sep 2006, Andrzej Trybulec wrote:

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.

:-)

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.

Mizar types have no "foundational role", the type mechanisms are intended
exactly for the purpose of avoiding "routine jobs", or for solving such "psychological problems". So why should users drag those "meaningfulness" assumptions along?

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 :-))

And three years ago (http://mizar.uwb.edu.pl/forum/archive/0311/msg00041.html) I MMLQueried for you that in this case there are only 11 cases where the assumption is not mentioned together with the type, in comparison with 46 cases where both are mentioned. So it does not exactly seem to save you much work in this case.

I also suggested (http://mizar.uwb.edu.pl/forum/archive/0311/msg00035.html) to have
"natural" as an attribute instead, and do things much more naturally :-)
with "weak clusters". And you actually surprised me
(http://mizar.uwb.edu.pl/forum/archive/0311/msg00021.html) with pointing
out that one already has "weak conditional clusters" like

let A be set, B be infinite set;
cluster onto -> infinite Function of A,B;

And I asked why should not the same be allowed at least for functor clusters (which was my original problem in osalg_3, very similar to that with the not necessarily existing "natural' transformations), to which you (sort of) agreed a year later in Bialystok (but it did not happen yet).

I still think that allowing even the full usage of weak types, e.g. to say something like

for t being natural transformation of F1,F2 ...

would be very useful.


Best,
Josef