an extension of the mizar language for dealing with article metadata

[Adam Naumowicz]

Hi,

On Tue, 2 Dec 2008, Freek Wiedijk wrote:

>>> Of course _I_ always want the vocabulary files to be part
>>> of the articles.
>>
>> Are you really serious about it?
>
> Yes!  Completely serious.
>
> I think I would like the articles to have three parts:
>
> environ
>  ...
> vocabulary
>  ...
> begin
>  ...
>
> So there wouldn't change too much, but there would be
> just one file that one would need to work on, and one
> "name space" that would be shared for naming both articles
> and vocabularies.

I also like the idea of "glueing together" the *.miz and *.voc files -
it's the way it is now. I think the 'vocabulary' (in singular) part would
only be used when writing the article - after submission it could be
transferred into mml.vct and removed from the article. This procedure,
however, would require importing (by default) a vocabulary named like the
processed article, provided it exists in mml.vct. Keeping that part in the
article seems useles as it's easier to use findvoc/listvoc to check the
contents of a vocaulary rather than searching *.miz files.

One minor disadvantage of keeping *.mi and *.voc as one file would be when
working with a local library - at he moment several articles can share a
local vocabulary and the change would require copying the 'vocabulary'
stuff into several files. But to me it's a minor problem, since this is
exactly what we usually do with the environment, anyway.


Regards,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. [phone]
Institute of Computer Science          tel. [phone] (office)
University of Bialystok                e-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================

[Adam Naumowicz]

On Wed, 3 Dec 2008, Adam Naumowicz wrote:

> I also like the idea of "glueing together" the *.miz and *.voc files - it's
> the way it is now.

Of course I wanted to say here that it's an unnecessary _nuisance_ for
many novice authors the way it is today :-)

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. [phone]
Institute of Computer Science          tel. [phone] (office)
University of Bialystok                e-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================

[Freek Wiedijk]

Hi Adam,

>I think the 'vocabulary' (in singular) part would
>only be used when writing the article - after submission
>it could be transferred into mml.vct and removed from
>the article.

Why remove it?  It shouldn't hurt to keep the article intact.
Of course you also should have the mml.vct file.  But it
can be a _copy,_ can it?

I like the idea that if somewhere on an old disk you would
find an old mml directory full of *.miz files, that it
would be self-contained.

I even think I would like the vocabulary to also be part
of the .abs files.

>This procedure, however, would require importing (by
>default) a vocabulary named like the processed article,
>provided it exists in mml.vct. Keeping that part in the
>article seems useles as it's easier to use findvoc/listvoc
>to check the contents of a vocaulary rather than searching
>*.miz files.

Again, you can easily have it in _both_ places.  I like the
idea that you can easily see the article together with its
vocabulary, even if it's "frozen" in the MML.

>One minor disadvantage of keeping *.mi and *.voc as one
>file would be when working with a local library - at the
>moment several articles can share a local vocabulary and
>the change would require copying the 'vocabulary' stuff
>into several files.

I don't know about implementation issues, but doesn't it
seem natural to just have the name of one of them in the
"vocabulary" directive of the others?

To make that work you would need to generate a "local"
version of mml.vct to supplement the real mml.vct when
running miz2prel.  I guess.

Freek

[trybulec]

Dear Freek,

we may glue a vocabulary into the article, which one?

There is no clear idea what it is the vocabulary of the article. There
are two possibilities:

1. historical: the symbols originally invented by the author of an article:
 What it means that somebody invented such symbols as '+' , 'even' or
'Function' ?
Maybe in the case of such (mode) symbols as  'DnT' or  'N_Sub_set_fam' I
would like to know who is the guy. :-)

2. pragmatical: the first ( in the order of processing - given on
MML.LAR) article in which the symbol is used.
It is true, that the names of vocabularies are (mostly) the same as the
names of articles. It is the result of a revision,
proposed by Piotr Rudnicki.  We put the symbol on a vocabulary with the
same name as the name of the article in which it was first used.
I was  very suspicious, but Piotr convinced me that it will be helpful
and he was right.

It is not stable: e.g.
'sequence' is on the vocabulary NORMSP_1 (335)
first used in  NAT_1 (62)
'non-zero' - on the vocabulary ANPROJ_1 (320)
first used in STRUCT_0 (275) and not used in ANPROJ_1 at all!

The number in parentheses is the place of the article on MML.LAR.

I cannot imagine how we could maintain MML with the vocabularies glued
in the articles.

Regards,
Andrzej

Freek Wiedijk wrote:

>I think I would like the articles to have three parts:
>
> environ
>  ...
> vocabulary
>  ...
> begin
>  ...
>
>So there wouldn't change too much, but there would be
>just one file that one would need to work on, and one
>"name space" that would be shared for naming both articles
>and vocabularies.
>
>For instance we would have (random example):
>
>  :: Some Basic Properties of Sets
>  ::  by Czes{\l}aw Byli\'nski
>  ::
>  :: Received February 1, 1989
>  :: Copyright (c) 1990 Association of Mizar Users
>
>  environ
>
>   vocabularies BOOLE, TARSKI, INCPROJ;
>   notations TARSKI, XBOOLE_0, ENUMSET1;
>   constructors TARSKI, XBOOLE_0, ENUMSET1;
>   registrations XBOOLE_0;
>   definitions TARSKI, XBOOLE_0;
>   theorems TARSKI, XBOOLE_0, ENUMSET1, XBOOLE_1;
>   schemes XBOOLE_0;
>
>  vocabulary
>
>    Rare_c=-comparable
>
>  begin
>
>  reserve v,x,x1,x2,y,y1,y2,z,A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set;
>
>  registration
>    let x, y be set;
>  [etc. etc.]
>
>I think it would be much better this way.
>
>Freek
>
>  
>

[Freek Wiedijk]

Dear Andrzej,

>It is true, that the names of vocabularies are (mostly)
>the same as the names of articles.

Precisely.  So making those names _exactly_ correspond
seems a very minor change to me.

>I cannot imagine how we could maintain MML with the
>vocabularies glued in the articles.

Why not?  Instead of having two files foo.voc and foo.miz
you would have one, but why does it matter how things are
distributed over _files?_  And if you do _not_ want to make
the names match up exactly, you could have dummy articles
that _just_ have a vocabulary.

I don't see the problem, sorry.  It is trivial to write a
perl script that transforms a directory with separate .voc
and .miz files into a directory in which the vocabularies
are in included in the .miz files.  So to "maintain" MML
one then could run that script, do whatever is needed for
maintenance, and then run the inverse script.

But I don't see why for maintenance the vocabularies couldn't
stay in the .miz files.  Can you explain?

Freek

[trybulec]

Dear Freek,

Freek Wiedijk wrote:

It is true, that the names of vocabularies are (mostly)
the same as the names of articles.
    

Precisely.  So making those names _exactly_ correspond
seems a very minor change to me.

  

The only exception that I know: the vocabulary 'ARYTM'. I do not know why it has such a name.

I cannot imagine how we could maintain MML with the
vocabularies glued in the articles.
    

Why not?  Instead of having two files foo.voc and foo.miz
you would have one, but why does it matter how things are
distributed over _files?_  And if you do _not_ want to make
the names match up exactly, you could have dummy articles
that _just_ have a vocabulary.
  

What is the relation between foo.miz and foo.voc? How it happened that they have the same name?

When you submit a new article, you submit, sometimes, a new vocabulary. The Library Committee asks you
to assign the same name to the vocabulary as to the article. To simplify book keeping.

What is on foo.voc is often accidental. E.g. When attributes 'negative' and 'positive' were introduced in
ASYMPT_0, 'positive' was placed on the vocabulary ASYMPT_0.VOC, but not 'negative', it already was
on the vocabulary ZF_REFLE.VOC.  After a revision the definitions of the attributes were moved to
XXREAL_0. But symbols are still on old vocabularies.

I don't see the problem, sorry.  It is trivial to write a
perl script that transforms a directory with separate .voc
and .miz files into a directory in which the vocabularies
are in included in the .miz files.  So to "maintain" MML
one then could run that script, do whatever is needed for
maintenance, and then run the inverse script.

  

I like the first part. Why I should do the second?

Actually the vocabularies are kept in one file: MML.VCT. With the exception of private vocabularies, of course.

But I don't see why for maintenance the vocabularies couldn't
stay in the .miz files.  Can you explain?

  

My mistake, if I restore MML.VCT, it will be no problem Only I do not like to do unnecessary job.

Without the preprocessing the problem is that an article may use a vocabulary that has the name of article that is processed later. 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.

Probably in such situation somebody would find that the vocabulary should be in a separate file. This would be a big discovery. And a big relief. :-)

Regards,
Andrzej

[trybulec]

Hi:

Thanks for the explanation.

It would be nice to same same mark commands in Coq and Mizar, and other
systems, too.

The reason of designing XML was to have a uniform solution to it. I
still do not understand why

<AUTHOR>
   XXX YYY
</AUTHOR>

is so much less readable than

 author XXX YYY;

or

 author {* XXX YYY *}

Regards,
Andrzej Trybulec

Makarius wrote:

>Isabelle/Isar supports basically three kinds of "comments":
>
>  (1) Source comments  (* like this *)  which are stripped from the text
>      as it is being processed, i.e. they behave like comments in most
>      programming languages, or % in TeX.
>
>  (2) Document comments  -- {* like this *}  which are considered part of
>      the formal langaguage and are included in the final typesetting.
>
>  (3) Explicit markup commands, notably
>
>      chapter {* ... *}
>      section {* ... *}
>      subsection {* ... *}
>      text {* ... *}
>
>      These are full commands, just like 'theorem' or 'proof', but the do
>      not affect the logical context.
>
>The argument text {* ... *} of document comments and markup commands can
>refer to logical entities from the context of the text, by using document
>antiquotations.  For example:
>
>  text {* blah blah @{term "x + y = z"} blah blah @{thm lemma1} ... *}
>
>These antiquotations are checked according to the full logical context,
>and pretty printed with the syntax of the context (although I would prefer
>annotating the original input source, instead of printing internal
>entities).
>
>
>Since this thread was initially about meta data for theories, what we have
>in Isabelle/Isar is only this:
>
> header {* ... *}
>
> theory A ...
> begin
>   ...
> end
>
>Here the 'header' provides free-form text, it is usually typeset like
>'section'.  Adding extra commands for 'author' etc. would be straight
>forward, but we have never really needed this yet.  In Isabelle/Isar
>documents the title/author is usually part of the outermost root.tex that
>assembles all the generated LaTeX sources in the end.
>
>
> Makarius
>
>  
>

[Josef Urban]

On Sun, 14 Dec 2008, trybulec wrote:

> The reason of designing XML was to have a uniform solution to it. I still do
> not understand why
>
> <AUTHOR>
>  XXX YYY
> </AUTHOR>
>
> is so much less readable than
>
> author XXX YYY;
>
> or
>
> author {* XXX YYY *}

People can get used to a lot of things. The ACL2 people would say that
Lisp notation for mathematics is not a problem, HOL and Isabelle people
put quotes around math expressions, FOL is usualy Prolog-ish, there is
this thing called "Polish notation" :-), etc.

But I think syntax like:

<Theorem kind="T"> <For> <Typ kind="G" nr="15">
<Cluster> <Adjective nr="204"/> <Adjective nr="259"/> <Adjective
nr="261"/> </Cluster> </Typ> <For> ...

would not be particularly attractive as a language for human
mathematicians.

I agree that if there is just little markup like in your example, it is
not a big deal. XML is really a good technology, but using it extensively
for humans is a misuse in my opinion. One good reason for having things
like XML, Lisp and Prolog, is that they are easy to parse. But it is
strange to use this reason in our situation, because Mizar already has a
very complex parser (producing XML from the natural syntax) anyway.

Josef

> Makarius wrote:
>
>> Isabelle/Isar supports basically three kinds of "comments":
>>
>>  (1) Source comments  (* like this *)  which are stripped from the text
>>      as it is being processed, i.e. they behave like comments in most
>> programming languages, or % in TeX.
>>
>>  (2) Document comments  -- {* like this *}  which are considered part of
>> the formal langaguage and are included in the final typesetting.
>>
>>  (3) Explicit markup commands, notably
>>
>>      chapter {* ... *}
>>      section {* ... *}
>>      subsection {* ... *}
>>      text {* ... *}
>>
>>      These are full commands, just like 'theorem' or 'proof', but the do
>> not affect the logical context.
>>
>> The argument text {* ... *} of document comments and markup commands can
>> refer to logical entities from the context of the text, by using document
>> antiquotations.  For example:
>>
>>  text {* blah blah @{term "x + y = z"} blah blah @{thm lemma1} ... *}
>>
>> These antiquotations are checked according to the full logical context, and
>> pretty printed with the syntax of the context (although I would prefer
>> annotating the original input source, instead of printing internal
>> entities).
>>
>>
>> Since this thread was initially about meta data for theories, what we have
>> in Isabelle/Isar is only this:
>>
>> header {* ... *}
>>
>> theory A ...
>> begin
>>   ...
>> end
>>
>> Here the 'header' provides free-form text, it is usually typeset like
>> 'section'.  Adding extra commands for 'author' etc. would be straight
>> forward, but we have never really needed this yet.  In Isabelle/Isar
>> documents the title/author is usually part of the outermost root.tex that
>> assembles all the generated LaTeX sources in the end.
>>
>>
>> Makarius
>>
>>
>
>

[trybulec]

Josef Urban wrote:

>
>
> But I think syntax like:
>
> <Theorem kind="T"> <For> <Typ kind="G" nr="15"> <Cluster> <Adjective
> nr="204"/> <Adjective nr="259"/> <Adjective nr="261"/> </Cluster>
> </Typ> <For> ...
>
> would not be particularly attractive as a language for human
> mathematicians.
>

I completely agree. I propose XML only for metadata. I am even not sure
if "propose" is a correct word.
I would not reject such solution.

> I agree that if there is just little markup like in your example, it
> is not a big deal. XML is really a good technology, but using it
> extensively for humans is a misuse in my opinion. One good reason for
> having things like XML, Lisp and Prolog, is that they are easy to
> parse. But it is strange to use this reason in our situation, because
> Mizar already has a very complex parser (producing XML from the
> natural syntax) anyway.


Right. But I believe that the metadata probably will evolve
independently and I hope we will reach common solution with other
systems. So I would like to have them separated from "pure" Mizar.

Regards,
Andrzej

[Freek Wiedijk]

Dear Andrzej,

>What is on foo.voc is often accidental.

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.

>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.

>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.

Freek

[Josef Urban]

On Sun, 14 Dec 2008, trybulec wrote:

>> I agree that if there is just little markup like in your example, it is not
>> a big deal. XML is really a good technology, but using it extensively for
>> humans is a misuse in my opinion. One good reason for having things like
>> XML, Lisp and Prolog, is that they are easy to parse. But it is strange to
>> use this reason in our situation, because Mizar already has a very complex
>> parser (producing XML from the natural syntax) anyway.
>
>
> Right. But I believe that the metadata probably will evolve independently and

Independently from the Mizar parser? I think complete independence (i.e.,
putting metadata into comments) is suboptimal (though certainly better to
have metadata in comments than not at all). For presenting in HTML (and
other systems), it would be good if metadata were present in the XML form
of article produced by the Mizar parser. That means the parser should be
aware of them, at least to some minimal extent (e.g., recognize the start
and end bracket of metadata, and treat everything in between as a string,
and output this in a proper place in the XML).

> I hope we will reach common solution with other systems.

One standard is the Dublin Core (DC), my Perl hack currently produces
proper DC XML elements from the starting comments in .miz files. There is
no reason why the Mizar parser could not do it too from whatever
human-friendly syntax.

Josef

[trybulec]

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

[trybulec]

Josef Urban wrote:

>
>
> On Sun, 14 Dec 2008, trybulec wrote:

>> Right. But I believe that the metadata probably will evolve
>> independently and
>
>
> Independently from the Mizar parser? I think complete independence
> (i.e., putting metadata into comments) is suboptimal (though certainly
> better to have metadata in comments than not at all). For presenting
> in HTML (and other systems), it would be good if metadata were present
> in the XML form of article produced by the Mizar parser. That means
> the parser should be aware of them, at least to some minimal extent
> (e.g., recognize the start and end bracket of metadata, and treat
> everything in between as a string, and output this in a proper place
> in the XML).

Actually, I would rather have a cross reference to the metada in a comment.

Like

::?  SECTION  ABC

and at ABC are the metadata related to the section.

I accept that you want the metadata be presented in XML, why they should
be produced by the Mizar parser?
What is the difference to you how you get them?

> One standard is the Dublin Core (DC), my Perl hack currently produces
> proper DC XML elements from the starting comments in .miz files. There
> is no reason why the Mizar parser could not do it too from whatever
> human-friendly syntax.
>
There is no reason for the Mizar verifier to bother with metadata.

Regards,
Andrzej

[Freek Wiedijk]

Dear Andrzej,

>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.

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?

>What is the natural place for the attribute symbol
>'negative'?

ZF_LANG, apparently :-)  (Or maybe ASYMPT_0, as that's where
"positive" seems to be :-))

>I am ready to do a lot of work, if necessary. Why I should
>do more work, if it is not necessary.

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.

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?

Maybe I'm missing something in this discussion, but then
I don't see what.

>Nothing to gain, only troubles.

No, no troubles either!  And the gain would be that you just
have one file for your article, instead of two, which is much
simpler.  Also no "dict" directories would be needed.  _And_
MML would be more "self contained".  Currently you need the
mml/*.miz files _and_ the mml.vct file to make sense of it.
Then you only would need the stuff in the mml directory.

>We have now more flexible system keeping the lexical
>resources separated from articles.
>It works pretty well, why to changed 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 :-)

Freek

[Josef Urban]

>>> Right. But I believe that the metadata probably will evolve independently
>>> and
>>
>>
>> Independently from the Mizar parser? I think complete independence (i.e.,
>> putting metadata into comments) is suboptimal (though certainly better to
>> have metadata in comments than not at all). For presenting in HTML (and
>> other systems), it would be good if metadata were present in the XML form
>> of article produced by the Mizar parser. That means the parser should be
>> aware of them, at least to some minimal extent (e.g., recognize the start
>> and end bracket of metadata, and treat everything in between as a string,
>> and output this in a proper place in the XML).
>
>
> Actually, I would rather have a cross reference to the metada in a comment.
>
> Like
>
> ::?  SECTION  ABC
>
> and at ABC are the metadata related to the section.
>
> I accept that you want the metadata be presented in XML, why they should be
> produced by the Mizar parser?
> What is the difference to you how you get them?

The difference is in reconstructing the article in HTML. The syntax in
comments allows users to do stupid things like:

theorem Foo
a+b =
::?SECTION Blah
b+a
proof ... end;

It is easy for the Mizar parser to disallow this stupidity. It is not easy
for a lightweight parser which is not aware of the standard Mizar syntax.

>
>> One standard is the Dublin Core (DC), my Perl hack currently produces
>> proper DC XML elements from the starting comments in .miz files. There is
>> no reason why the Mizar parser could not do it too from whatever
>> human-friendly syntax.
>>
> There is no reason for the Mizar verifier to bother with metadata.

If you by "Mizar verifier" also refer to the Mizar parser, then there is
the above reason. The other passes (analyzer, checker) obviously will not
deal with the metadata at all.

Josef

[trybulec]

Josef Urban wrote:

>
> The difference is in reconstructing the article in HTML. The syntax in
> comments allows users to do stupid things like:
>
> theorem Foo
> a+b =
> ::?SECTION Blah
> b+a
> proof ... end;
>
> It is easy for the Mizar parser to disallow this stupidity. It is not
> easy for a lightweight parser which is not aware of the standard Mizar
> syntax.

A good argument. The place of this pragma must be controlled. Perhaps
some others, too.  Does it mean
that we should introduce a reserved word for it?

section XXXX;

It results in an advantage for the parser: better reporting of errors.
E.g. reporting unpaired 'proof'.

Merry Christmass,

Andrzej

[trybulec]

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

[Freek Wiedijk]

Dear Andrzej,

>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.

Okay, I see the point now.  Although this seems to me is
not something that would happen very often?  Also, the same
thing already happens with the notations and registrations,
I guess.  So it just seems to be a little bit more of the
same thing?

>Merry Christmas,

Thanks, my best wishes to you too.  And to all other Mizar
users around the world!

Freek

[Freek Wiedijk]

Hi Josef,

A happy new year!

>How about removing the "vocabularies" directive
>completely? The "notations" would say to the parser which
>symbols are available.

To me this seems a much more drastic change than what I
was proposing.  I guess it also would mean unifying the
vocabulary and article name spaces?

Freek

[Josef Urban]

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
>