Dear Andrzej, Adam,I also agree that using attributes/clusters as Andrzej suggests (i.e. the (b) method from my previous message) is better now than using type (re)definitions. If we do more general attributes (i.e. with explicit parameters) later, it will be easy to refactor.
I think that this kind of problems is exactly what should drive the discussion/development of Mizar, and slightly disagree with the philosophy "let's hack it now somehow, and solve it generally later". It usually produces no general solutions :-). Obviously, if the "general solution" is too difficult, it's the only way, but it does not seem to be the case here. On the other hand, if the implementation is easy, it might be better to do it right the first time.
So a bit more on the "best of both worlds" proposal: - termination would have to be ensured for registrations like"Y subset -> X subset"; I guess it would be safe if no functor symbols and no new variables are allowed in the consequent (e.g. functors give infinite loops for registrations like "n element -> (n+1) element" (leading to "((n+1)+1) element", etc.))
- hence if we still want to have functor symbols in mode (re)definitions, then the new parameterized attributes cannot fully replace current modes (there are now type hierarchies like "Relation of X,Y -> Element of bool [:X,Y:]")
- and hence the simple question: how much are functors needed in result types of mode (re)definitions? It seems that a lot of them is there just to ensure that the mode ultimately widens to "Element of", and the fraenkel operator (i.e. comprehension/replacement) is (now) easy to use. Provided that we make fraenkel more general (which is tha plan anyway - some "smallness" or "sethood" property), what are the examples/reasons for allowing functors in the result types of modes?
Best, Josef On Wed, 13 Sep 2006, Andrzej Trybulec wrote:
Dear Adam,I appreciate what Josef wrote, but it is rather about the extension of Mizar, and I guess you asked what to do now. Without revision nothing can be done, I think. So, the definition must be repeated.The solution, that I like, is to use 'real-valued' and 'ext-real-valued' attributes (it is now 'real-yielding', I think that 'real-valued' is better name, have anybody an opinion about it?). Then instead of 'PartFunc of X,REAL' we should use 'real-valued ManySortedSet of X'. With proper registration it widens to 'ext-real-valued ManySortedSet of X'. So we need a 'VALUED' article dealing with Functions (or rather with Relations) similar to the 'MEMBERED' article that takes care of sets.It works of course only for "important" sets. I agree with criticism expressed by Josef: the necessity to have explicitly defined attribute for each "important set"but it seems that it is all that can be done with Mizar as it is. Regards, AndrzejOn Sun, 10 Sep 2006, Adam Grabowski wrote:Dear all, in one of the articles recently submitted to the Mizar Mathematical Library (currently under review process) one can find the following definition: definition let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; let f be PartFunc of X,REAL; func Integral(M,f) -> Element of ExtREAL equals Integral(M,R_EAL f); coherence; end; where "Integral" was defined in MESFUNC5 for "f" of the type PartFunc of X, ExtREAL (the remaining variables are of the same type as in the above definition). Even if the set "REAL" (the set of all real numbers) is a subset of "ExtREAL" (the set extending REAL by the infinite values), the Mizar system does not give automatically a type "PartFunc of X,ExtREAL" to partial functions of X, REAL. This could result in the duplication of notions, even if only some casting functions are used instead of defining notions from scratch. (as R_EAL f just assigns the type "PartFunc of X, ExtREAL" to f which is a partial function from X into REAL). Very similar problem apeared in the case of the type "Element of REAL" and "Element of COMPLEX" (with the earlier not extending to the latter). Now we force the users to use "real number" and "complex number", respectively. Thanks to the mechanism of the conditional clusters with the registration as follows: definition cluster real -> complex number; coherence; :: with some easy proof to be found in XREAL_0 end; a number of duplications can be avoided. I would like to know your opinion about the best solution (or at least, the better one) in the case of partial functions (and hopefully, some general guidelines for the future). Regards, Adam Grabowski Library Committee of the Association of Mizar Users