«Abstract. One major goal of Mathematical Knowledge Management is building extensive repositories, in which the mathematical knowledge has been ...»
After the change of the loci type (the submission obtained grade D, of course) from FinSequence of REAL into real-yielding FinSequence in the EUCLID article the earlier deﬁnition was no longer needed which helped to simplify the structure of notions in this new submission.
The decision is not a typical result of majority voting, because referees giving C grade point out possible improvements, so usually the lowest grade counts (luckily, in case of E marks, all three referees agreed).
To summarize the grades for 2006, let us look at Table 1.
Table 1. Number of submissions to the MML and their grades in 2006
Basically, all ten submissions graded A and B were included into the MML, and among C and D candidate articles, which were returned to authors, other 15 were accepted; in total there were 25 Mizar articles accepted in 2006, the ﬁrst year the reviewing procedure as described above was introduced.
All in all we have seen that reviewing MML submissions indeed addresses only the ﬁrst point mentioned in Section 2. Of course a thorough reviewing process will improve the quality of MML articles and may even pilot authors into the direction of a good style of “Mizar writing”. As we can conclude from Table 1, this is the case of the majority of submissions because the authors should enhance the articles according to the referees’ suggestions. However there remain situations in which the MML as a whole should be improved; in the long term mere reviewing of submissions cannot avoid this. Here even carefully reviewing of Mizar articles – as already indicated by rate D above – can only help to detect the need for such revisions.
4 MML Enhancing The Library Committee has been established on November 11, 1989. Its main aim is to collect Mizar articles and to organize them into a repository – the MML.
Recently, from this agenda a new additional one was created – the Development Committee, which takes care of the quality of the library as a whole.
4.1 Types of Revisions For the reasons we tried to point out before, the Mizar Mathematical Library is
continuously revised. Roughly speaking, there are diﬀerent kinds of revisions:
– an authored revision – consists of small changes in some articles in the library when somebody writing a new article notices a theorem or a deﬁnition in an old article that can be generalized. This is also the case of D grade as described above. To do this generalization, sometimes it is necessary to change (improve) some older articles that depend on the change. As a rule, a small part of the library is aﬀected.
– an automatic revision – takes place frequently whenever either a new revision software is developed (e.g. software for checking equivalence of theorems, which enables to remove one or two equivalent theorems) or the Mizar veriﬁer is strengthened and existing revision programs can use it to simplify articles.
– a reorganization of the library – although was very rare before, as of now it happens rather frequently. It consists in changing the order of processing articles when the Mizar data base is created. Its main steering force is the division of the MML into concrete and
4.2 MML Versions
Apart of the Mizar version numbering, the MML has also separate indexing scheme. As of the end of 2006, the latest oﬃcial distribution of the MML has number 4.76.959.
As a rule, the last number, currently 959 shows how many articles are there in the library (this number can be sometimes diﬀerent because 26 items were removed so far from the MML, but some additional items such as EMM articles, and “Addenda” which do not count as regular submissions, were added). The second number (76) changes if a bigger revision is ﬁnished and the version is made oﬃcial. Although it is relatively small comparing with the age of the library, the changes are much more frequent.
4.3 Some Statistics
The policy of the head of Library Committee – to accept virtually all submissions from the developers and, if needed, enhance it by himself, was then very liberal. For these nearly twenty years there were only three persons taking a chair of a head of the Committee (Edmund Woronowicz, Czeslaw Byli´ ski, and curn rently Adam Grabowski); their decisions were usually consulted with the other members of the committee, though.
Such an openness of the repository was justiﬁed: in the early years of the Mizar project the policy “to travel to Bialystok and to get acquaintance with the system straight from its designer” resulted in the situation all authors knew each other personally, now the situation changed.
The MML evolved from the project, frankly speaking, considered rather an experiment of how to model mathematics to allow many users beneﬁt from a kind of parallel development. Now, when the role of the library is to be much closer to the reality and the MML itself is just one among many mathematical repositories, the situation is signiﬁcantly diﬀerent.
As it can be seen, the ﬁrst two years were extremely fruitful. No doubt, the ﬁrst one was most inﬂuential, when the fundamentals, such as basic properties of sets, relations, and functions, the arithmetics, and vector spaces were established – to enumerate among many these most important. Some articles from that time were more or less straight translation from those written in older dialect of the Mizar language (Mizar PC, Mizar-2 etc., see ). Especially the subsequent year – 1990, when many authors could beneﬁt from introducing the basics, hence they were able to work on various topics in parallel, brought into the Mizar Mathematical Library the bigest number of submissions so far (136 by year), then the number stabilized.
4.4 Towards Concrete and Abstract Mathematics As it was announced in 2001 , the MML will be gradually divided into two parts. As the library is based on the Tarski-Grothendieck set theory, the part devoted to the set theory (and related objects, as relations, functions, etc.) is indispensable. There is, however, huge amount of knowledge for which set theory is essential, but basing on the notion of structure by means of the Mizar language.
There are three parts of the Mizar Mathematical Library:
– concrete, which does not use the notion of structure (here of course comes standard set theory, relations, functions, arithmetic and so on);
– abstract, i.e. STRUCT_0 and its descendants, operating on the level of Mizar structures; both parts are not completely independent – here the concrete part is also reused (abstract algebra, general topology including the proof of the Jordan Curve Theorem, etc.);
– SCM, the part Random Access Turing Machines are modelled, i.e. mathematical model of a computer is described.
This division is reﬂected in the ﬁle mml.lar in the distribution in which is the order of processing of articles when creating Mizar data base is given – the “concrete” articles go ﬁrst, at the end are those devoted to the SCM series. The process of separating these three parts is very stimulating for the quality of the Mizar library – many lemmas are better clustered as a result of this activity.
As of the beginning of 2007, the division can be summarized in Table 3.
Note that apart of the revisions suggested by the referees when giving Dgrades, any user can via TWiki mechanism suggest the change; he may of course also send improved version via email to the Library Committee; as an example, lemmas needed for the G¨del Completeness Theorem were reformulated to o provide its better understanding as a result of the external call.
4.5 Library Management As a ﬁrst tool of collaborative work on the library we can enumerate Mizar TWiki (wiki.mizar.org) which gradually changes its proﬁle from an experimental – and rarely used – forum into the place where suggestions/experiences with the MML can be described.
As the most important, and probably one of the better known MML tools, we can point out MML Query . It has proven its feasibility when subsequent EMM items were created. Also researchers, when writing their Mizar articles, can ﬁnd it useful. But usually, typical author does not care too much if his lemma which takes some ten lines of Mizar code is already present in the library.
Actually, searching for such auxiliary fact can take much more time than just proving it. This results in many repetitions in the library MML Query cannot cope with. And although the author can feel uncomfortable with multiple hits of the same fact, annotating such situations and reporting it to the MML developers is usually out of his focus.
This is the area where another tool comes in handy. Potentially very useful for the enhancement of the MML as a whole, MoMM (Most of Mizar Matches) developed by Josef Urban was primarily developed to serve as assistant during authoring Mizar articles . It is a fast tool for fetching matching theorems, hence existing duplications can be detected and deleted from the MML (according to , more than two percent of main Mizar theorems is subsumed by the others). The work with the elimination of these lemmas is still to be done – many of detected repetitions are useful special cases so their automatic removal is at least questionable.
Another popular software, MML CVS – the usual concurrent version system for the MML was active for quite some time, but then was postponed because the changes were too cryptic for the reader due to the lack of proper marking of items. Actually, one of the most general problems is that there are no absolute names for MML items and the changes are usually too massive to ﬁnd out what really matters.
5 Traps for the Developer Usually, the revision process via generalization of notions improves the MML.
There are some dangerous issues, however; we address some of them in this section.
5.1 Mind the Gap!
Let us cite an example from the article ABIAN :
definition let i be Integer;
attr i is even means :: ABIAN:def 1 ex j being Integer st i = 2*j;
These are usual deﬁnitions of odd and even integer numbers.
definition let i be Integer;
attr i is odd means ex j being Integer st i = 2*j+1;
Then, among the others, the theorem stating that all integer numbers are either odd or even, was proven; the proof was very simple, but there was something in it to do, at least both deﬁnitions were involved.
for i being Integer holds i is odd or i is even;
However, after the revision (which was done by the author of ABIAN, after
all), the second deﬁnition got simpliﬁed as follows:
notation let i be Integer;
antonym i is odd for i is even;
Still, it seems perfectly correct, introducing antonym we obtain the law of excluded middle automatically, in a sense, and the proof of the above lemma labeled LEM was no longer necessary.
But we made a step too far, as it seems. Because in the deﬁnition of even number, the integer was not needed (remember the type Integer is a shorthand for integer number), it was dropped in both – deﬁnition of an attribute and its
antonym, and the latter got simpliﬁed into the form:
notation let i be number; antonym i is odd for i is even;end;
Unfortunately, e.g. number Pi (the Mizar symbol for the usual constant π) can be proven to be odd which can be considered really odd. Observe that any automation of the process of dropping assumption about the types of used loci in the deﬁnition of attributes, however possible, could be dangerous.
5.2 Permissive Deﬁnitions There are two unities for vector spaces deﬁned in the MML – with symbol 1.
and 1_, and the following deﬁnitions:
definition let FS be multLoopStr;
func 1.FS - Element of FS equals :: VECTSP_1:def 9 the unity of FS;
definition let G be non empty HGrStr such that G is unital;
func 1_G - Element of G means :: GROUP_1:def 5 for h being Element of G holds h * it = h & it * h = h;
where multLoopStr is HGrStr enriched by an additional selector, namely unity and the adjective unital in the permissive assumption (after such that) assures that the proper neutral element exists.
At ﬁrst glance, the earlier approach is better – the less complicated a type in a locus, the less problems we have to assure the required type. In the second deﬁnition however, the underlying structure has only two selectors instead of three.
5.3 Meaningless Predicates
Suppose we have the following:
definition let a,b be natural number;
assume a 0;
pred a divides b means ex x being natural number st b = a * x;
Well, we can freely delete the assumption, in Mizar predicate deﬁnitions do not require any correctness conditions proven. But, if we forget for a while that within the MML division by zero is deﬁned, does it make any mathematical sense for any pair of natural numbers? According to the current policy of the Library Committee, we allow for any such underspeciﬁcation.
5.4 Apparent Generalizations
There are sometimes cases the price for the revision is too high comparing to gains or the enhancing is apparent. If we remind that pathwise connectedness of the topological space T denotes the existence of a function from the unit interval into T which has the values a and b in 0 and 1, respectively, for any pair of points a, b of T, a path between two points is just an underlying mapping, if it exists.
It is enough however to have an assumption about the existence of appropriate function for just the pair of points currently under considerations.
definition let T be TopStruct; let a, b be Point of T;
assume a, b are_connected;
mode Path of a, b - Function of I, T means :: BORSUK_2:def 2 it is continuous & it.0 = a & it.1 = b;