[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