[mizar] Lexical resources

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

I asked Adam Naumowicz if we have a utility that reports the size of
lexical resources of MML. The answer, it is easy
to grep them. All vocabularies are kept now one file :  MML.VCT

The results:


                                          Qualifier
Number

Predicate symbols                  R                          586
Functor symbols                     O                        2273
Left Functor Brackets            K                            25
Right Functor Brackets           L                            25
Mode symbols                       M                          531
Attribute symbols                   V                          913
Selector symbols                    U                          103
Structure symbols                   G                            82

To grep e.g. the number of mode symbols write

      grep -c ^M c:\mizamml.vct
for other symbols one has change M to the proper qualifier.

A trap:

    every vocabulary starts with a line that begins with 'G' so after

     grep -c  ^G  c:\mizar\mml.vct

one gets the number of structure symbols + the number of vocabularies.

The number of vocabularies one gets after

    grep -c  ^#   c:\mizar\mml.vct


Remarks:

The number of left functor brackets is the same as the number of right
functor brackets. It is not accidental, in older Mizar if one started
i-th left functor bracket, it must be closed with i-th right functor
bracket. One may mix now functor brackets, the only example that I know:
the article MEASURE5: def 2, def 3, def 4, def 5

   Formats
       [.a,b.]    ].a,b.]   [.a,b.[   ].a,b.[
for respectively closed, open-closed, closed-open, open intervals of
real numbers. It a result of a revision, of course.

The homonymic tokens:
     Functor brackets     [ ]  and { }
     Predicate symbol   =
are not counted by grep.

Greetings,
Andrzej Trybulec