On Tue, 9 Jan 2007, Adam Naumowicz wrote:
On Tue, 9 Jan 2007, Jesse Alama wrote:Adam Naumowicz <adamn@math.uwb.edu.pl> writes:BTW: it's better to state such properties of F2 as functorial registrations rather than theorems - this way they could be used automatically by the checker when one would import your registrations.I see your point, and when I was looking in the MML for examples on which I could base my definition of F2, I found that functorial registrations were the customary way of accomplishing my task. Although I don't want to break with the custom and I understand the value for the checker if I follow it, I do think that it is more natural to express the properties of a new term as theorems rather than as functorial registrations. By expressing properties in terms of functorial registrations, one is writing for the MIZAR checker, not for human readers. It seems to me that using functorial registrations takes MIZAR away from rather than toward the mathematical vernacular. (Though perhaps one could argue that the MIZAR custom of functorial registrations is actually captures what's going on in the mathematical vernacular.)Yes, it's a clear-cut example of a trade-off between sticking close to the mathematical vernacular and adding more automation with new language constructs. In this case, however, the registrations look painfully technical in their *.miz form, but various forms of presentation may 'smooth' them a bit - e.g. the relevant theorems could be printed in the *.xml presentation next to the registrations. And in the TEX'ed form of Formalized Mathematics the presentation looks more or less like a mathematical statement, e.g.: "One can verify that ... is ...".
I think you can have both the theorem and the registration (trivially justified by the theorem). Another "more human" way would be just to have a theorem-property (analogy of definitional properties like "symmetry"), which would tell the checker to use the theorem for the automations. Perhaps a better word than "property" would be Andrzej's "pragma" in this case (e.g. keyword "register"). But I think the current explicit writing of registrations does not hurt much, and the explicit writing has its advantages. Also, in the example, wasn't it possible to put "strict" directly in the result type of F2 instead of having an extra registration for it?
Last thing: the confusion with different versions of "strict" can be already now avoided by using synonyms, e.g.:
notation let G be LoopStr; synonym G is strict_LoopStr for G is strict; end;It wouldn't hurt to add such synonyms automatically to each article accepted to MML, so that when the context is overloaded, people could make sure that they get what they want (if they do not look at the HTML, or other semantic explanation).
Best, Josef