Re: [mizar] Re: Mizar Parser

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrea,

>(we also hope that the the internal representation is a bit
>more stable than the syntax).

With the EMM project (the Mizar "encyclopedia", right?),
constructors will move between articles, and so constructor
references (which, I suppose, will consist of an article
name, a letter representing a constructor type and a sequence
number) will change.  You should realize that the MML changes
_all the time._  Much more often than Coq or PVS or Isabelle
or systems like those.

>The kind of work we plan to explore then is:
>1. to rebuild an hypertextual vernacular-like presentation,
>as close as possible to the input.

What more would it be than the web pages under
<http://mizar.org/JFM/mmlident.html>?  That's as hypertextual
as I can imagine you can be, as well as vernacular-like
(Mizar is meant to be a vernacular-like language.)

If you think of transforming it into "more natural language
like" text, so to depart from Mizar input syntax, I think
that's useless (<- strong statement, but I feel it that
strongly)  You need to work with the Mizar syntax anyway if
you want to do anything interesting with the stuff, and Mizar
is close enough to natural language for me in the first
place.  There is of course the FM TeX translation already,
which is something like a "natural language" translation of a
Mizar abstract too, but I think that that is just as
useless.  I never look at this TeX version of things anyway.
Are there others that do?

Also, you should realize that to reconstruct something like
Mizar input from a term that's built from constructors is
difficult.  For instance: how do you know which of the
synonyms is meant to be used?  Or, for instance, whether to
pretty print something like "x is irrational" or like "not x
is rational" (I expect their internal representations to be
identical).  Or, different example, whether to pretty print
an inequality as "x < y" or "y > x" or "not x >= y", etc.

>2. building functionalities for searching/retrieving
>logical items inside the library, explicitating
>dependencies, etc. Here we have some tools we are
>developing for Coq, and we would like to test on a
>different repository of mathematical documents.

This seems close to what's on Grzegorz's webpages (although
somehow I've never managed to see this: when I look for them
the server never seems to work; so where are they at the
moment?)  Or to Joseph's stuff in emacs.  So what would it
give us that's not there already?

Also: I would like to have it offline, as I use Mizar most
often on the train.  So would I need to install web server
and a database and a lot of overhead like that for it to be
usable in that environment?  Because then I probably wouldn't
use it.  I don't want so much stuff running on my system just
to be able to search the MML.  I really would prefer it to be
a simple standalone program.

BTW: I never used Grzeorz and Josephs systems.  I use grep.
But it would be wonderful to be able to say "give me all the
theorems of which the statement has these-and-these
constructors".  Although to be really useful you'd need to be
able to phrase those constructors in Mizar input form (using
the environment and context of a certain position in an
article, I guess.)

>We would NOT be interested in the proof-checking part,

But would you be interested in storing the proofs?  Or are
just talking about the information that's in the abstracts (I
think that's about what Joseph called the "prel"s.)

Freek