Re: vocabularies

How about removing the "vocabularies" directive completely? The 
"notations" would say to the parser which symbols are available. It seems 
to me that "cutting-off" some notation by forbidding its symbol (i.e. by 
not including the vocabulary) belongs to the "black magic" part of Mizar 
that can bring more grieve to the users rather than substantial benefits.

The newly defined symbols could be recognized just by having a suitable 
syntax for definitions, which would allow a shallow parse to extract the 
symbols.

The FM translation technology should rather use notation (pattern) for 
mapping to TeX than the symbol level, because one Mizar symbol can have 
very different contexts of use, and possibly very different TeX notations 
(I think we already talked about this one with Grzegorz some time ago).

Josef

On Sun, 21 Dec 2008, trybulec wrote:

> Freek Wiedijk wrote:
>
>>> 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.
>>> 
>> 
>> But it is exactly the same in the current situation (where
>> the .voc files are not in the .miz files), if you would
>> choose to move a symbol between vocabularies!  I don't
>> see why this is an argument to not have the text of the
>> vocabularies be part of the .miz files.
>> 
>> 
> The "big" difference is in the fact that I am not pressed to move
> a symbol to another vocabulary if I changed the order of processing.
>
>> I you would change Mizar in such a way that all vocabularies
>> would be automatically available in all articles, so that
>> there wouldn't be a vocabularies directive in the environ
>> anymore, then I agree that it would be strange to have them
>> be part of the article.  _Then_ it would be natural to have
>> them be part of a global file mml.vct.  But is that where
>> you want to go to, eventually?
>> 
>> 
> It is no feasible to have all vocabularies available to all articles. The 
> reasons:
>
> 1. a symbol that has the form of an identifier may be used in an article as 
> identifier
>   (if its vocabulary is not in the environment)
> 2. composite cymbols like '+*', '{}.' may cause a differnet parsing when they 
> become available.
> 3.  some symbols are just traps. It is well know that one has to be careful 
> using 'c='
> if one writes
>                               a \ c= a \ b
> 'c' is not recognized as an identifier. Less known is the symbol for 
> Cartesian product
>                                   [x]
> (the vocabulary CAT_4) I wrote a scheme with something like
>
>           P[x] & P[y] implies  ....
> after adding the vocabulary CAT_4 I got wrong parsing
>      P [x]
> and a syntactic error.
>
> So, maybe we should redistribute symbols between vocabularies.
>
> A huge vocabulary with common symbols (HIDDEN resembles it, only it is not 
> huge; I do not like it, because
> it is not controlled by the user).
>
> One symbol vocabularies for such symbols like
>    [x]
> or
>     x.
> in ZF_LANG. (Well, we rarely use the identifier 'x' for functions).
>
>> But I don't see why anything would be more work if the
>> vocabularies would be part of the .miz and .abs files.
>> I'm just asking for a slight redistribution of existing
>> text among files, not to significantly change anything.
>> 
>
> Under the assumption that we restore MML.VCT, you are right.
>
>> To repeat myself (and maybe I just should shut up, as it's
>> clear that you won't follow this suggestion of mine): what
>> does it matter where the text of the vocabularies is stored
>> in the file system, as long as the way you use the system
>> stays essentially the same?
>> 
>
> I appreciate the discussion, it made some problems more clear for me.
>
>> Maybe I'm missing something in this discussion, but then
>> I don't see what.
>> 
>> 
> Let's try to fix it.
>
>> Ah well.  Leave it the way it is, then.  But don't ask me
>> not to tell people that I find Mizar a bit rococo :-)
>> 
>
> Never crossed my mind.
>
>
> Merry Christmass,
> Andrzej
>