Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
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?
In the example I indeed could have written
definition
func F2 -> strict doubleLoopStr equals
doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
coherence;
end;
rather than
definition
func F2 -> doubleLoopStr equals
doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
coherence;
end;
but I chose to isolate the proof of strictness (I had thought that
this was a "first-order" property like, e.g., commutative) and put it
in a separate theorem because I wanted to keep as separate as possible
the proofs of the various properties of F2. Now I realize that the
attribute strict is different from other attributes. Imagine, though,
that I had written, say,
definition
func F2 -> commutative doubleLoopStr equals
doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
coherence;
end;
rather than
definition
func F2 -> doubleLoopStr equals
doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
coherence;
end;
theorem
F2 is commutative;
In the latter case, we can give a label to the theorem and refer to it
later, whereas in the former case, the property of commutativity is
part of the definition of F2, which seems to me to be unnatural.
There may be cases where it *is* natural to put properties of a term
into its definition and then prove that the term has those properties
in the correctness proofs, but in general that seems to me to be an
unnecessary tangling.