Dear Jesse,
In Algol 60 a comment was a part of the language. The syntax was
comment TEXT ;
where TEXT was an arbitrary string of characters ( the semicolon itself
was not allowed)
We treat now comments as something that actually is not a part of the
language. I would rather
have "pure Mizar" with only these informations that are necessary for the
verifier.
We have now some features that should not be in pure Mizar and probably
should be replaced by pragmas:
they may be classified in the following categories:
i. temporary pragmas: '@proof' - to suspend verification
ii. library pragmas: 'canceled' - to keep numeration correct
iii. editorial pragmas: repeated 'begin' - to divide article into
section.
iv. maybe some others
We tried - on our seminar - to find common solution, but the categories
are so different that probably
there is none.
Recently, after reading your letter, we discussed the problem again with
Czeslaw and it seems that for the metadata the proper solution is to have
an XML-envelope of the Mizar article. Maybe something like
<DOCUMENT>
"the place for metadata"
<ARTICLE>
"the Mizar article"
</ARTICLE>
</DOCUMENT>
(mind you, I know almost nothing on XML, so it might quite naive).
Then from such XML document we may extract the Mizar article and process
it in the usual way.
"the Mizar article" is probably not the exact citation: we have '<' as a
symbol in Mizar. Still extracting the Mizar article should not be too
complicated. Maybe we can be more precise and have the form
<DOCUMENT>
"the place for metadata"
<ARTICLE>
<ENVIRONMENT DECLARATION>
"directives"
</ENVIRONMENT DECLARATION>
<TEXT PROPER>
"the text proper"
</TEXT PROPER>
</ARTICLE>
</DOCUMENT>
Then, 'environ' and 'begin' (if necessary) may be added while extracting
the Mizar article. The directives and the text proper are written in two
different languages, anyway.
<DOCUMENT>
"the place for metadata"
<ARTICLE>
<ENVIRONMENT DECLARATION>
"directives"
</ENVIRONMENT DECLARATION>
<TEXT PROPER>
<SECTION>
"the text proper"
</SECTION>
...
<SECTION>
"the text proper"
</SECTION>
</TEXT PROPER>
</ARTICLE>
</DOCUMENT>
Then we may put in the <SECTION> the title and maybe even the summary of
the section. And the grammar of Mizar will be a little bit simpler: no
repetition of 'begin'.
Regards,
Andrzej
Jesse Alama wrote:
As it stands now, the title of an article, its author(s), and the name
of sections aren't actually a formal part of a mizar text: we
customarily include this information as comments
:: Introduction to XYZ Theory
::
:: by Joe the MIZAR Writer
environ
...
begin :: Preliminaries
...
begin :: Main Lemma
...
begin :: Main Theorem
...
I propose to put this information into the body of the article, to move
it from comments to non-comments. Perhaps we could introduce new
keywords like `title', `author', and `section'. Then, articles could
look like
title{Introduction to XYZ Theory}
author{Joe the MIZAR Writer}
environ
<stuff>
begin{Preliminaries}
definition ...
theorem ...
theorem ...
begin{Main Lemma}
definition ...
begin{Main Theorem}
theorem ...
This would make the sections and article title part of the text; as it
stands, these features are not represented in the mizar grammar (because
customarily they are tucked away within comments).
The primary motivation for this idea is to help improve Josef Urban's
semantic MML presentation. Currently he has to do some hacking to
extract metadata like article titles and authors; extracting section
information (currently unsupported) would be similarly complicated. The
problem is that the article metadata isn't represented in the XML
representation of an article; it has to be inferred from the original
mizar source.
Additionally, this new syntax might help to simplify processing of FM
articles: with this approach one wouldn't need the BibTeX fields
SECTION1, SECTION2, etc., because these could be inferred from the
article.
Thoughts?
Best,
Jesse