Re: vocabularies

trybulec <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>
Freek Wiedijk wrote:

>The location of _almost everything_ in MML is often
>accidental.  If you consider this a serious issue then you
>should move around stuff in MML much more than currently
>happens.
>
>  
>
We intend to.

>>After a revision the definitions of the attributes were
>>moved to XXREAL_0. But symbols are still on old
>>vocabularies.
>>    
>>
>
>That's a bad argument: just move the symbols also to XXREAL_0
>(or to yet another article if that's a more natural place
>for them).  Sorry, but I don't see the point of this example.
>
>  
>
That's a very good argument. To move a symbol from a vocabulary A to a 
vocabulary B
is a lot of work. At least:
1. To look to all 1000 or so articles and change if necessary the 
'vocabularies' directive.
2. To modify data for JFM
3. To check if parsing is still correct, of all MML. Actually it may be 
worse, the parsing is correct
but the meaning of the article has been changed.
and probably more.

What is the natural place for the attribute symbol 'negative'?
1. an article on logic (which one: ZF_LANG, QC_LANG1, MODAL_1,MODELC_1, 
MODELC_2, ABCMIZ_1)
 to keep it together with
    'conjunctive' 'atomic' 'existential'
2. an article on real numbers
    together with 'positive'
or another place: an article on ortholattices or maybe ordered rings?

>>What I have in mind that (without preprocessing) we should
>>move symbols from one article to the other, any time we
>>change the order of processing.
>>    
>>
>
>I would expect this to be minor.  Doesn't this kind of
>thing also happen with definitions and notations and so on?
>It seems more of the same.
>
>  
>
I am ready to do a lot of work, if necessary. Why I should do more work, 
if it is not necessary.
Just to keep vocabularies inserted into the articles? Be serious.
Nothing to gain, only troubles.

We have now more flexible system keeping the lexical resources separated 
from articles.
It works pretty well, why to changed it?

Regards,
Andrzej
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.