[mizar] A. Asperti's offer

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

I would like to comment on the offer by A. Asperti to export the
"internal structure" of Mizar into XML.  I think that we should
support this offer and encourage whoever is willing to do it.

The main reason for doing so are widely understood Public Relations
(PR for short, I realize that these are my initials but they also stand
for Polynomial Ring, Primitive Recursiveness and probably other things).

Even when we do not foresee immediate usage of such a thing for Mizar
authors, there is some potential for the future.  I have browsed
through A. Asperti's papers on the formal mathematics and XML and I
would not want to do such a thing but if they do, we should offer them
our help (I am writing here 'we' realizing how little I can
contribute).

Doing XML rendition of Mizar texts may discover what really needs to
be done to have formal mathematics present on the web through the XML
technology although I doubt that it will lead to a smashing success
right away.  Such work may also reveal many rough edges of Mizar
similar to these that are showing up in the design of Grzegorz's MML
Query.

Freek's remark that Mizar evolves and the guts of MML and Mizar
processor change frequently runs against Andrea's hope that they are
more stable than Mizar syntax.  An XML representation of any
repository of formal mathematics must be capable of following the
evalution of the system, otherwise we are dealing with a stillborn
idea.

Freek also asks whether transformation of Mizar texts into "more
natural language like" text is worth the effort.  There are many uses
of such a thing if it existed, foremost translation into other than
English natural languages.  Peter Koepke from Bonn made that clear to
me from the perspective of teaching mathematics and at least he sees a
big value behind it.  The TeX'ed FM rough translation into English is
probably of little use for Mizar authors but plays a nontrivial role for
Public Relations.  Whenever presenting Mizar to someone I see how they
are impressed by FM.  I do not quite understand why, but so it is.
And also, I find it very useful for my discussion with my chairman
when he wants to know what I am doing.  Plain Mizar articles
definitely do not have the same appeal to outsiders as does something
that looks almost like English.  Again, I do not quite understand why
as our chairman seems to be a smart guy.

My conclusion is: let us support Asperti's offer, finally it is he and
his group that want to do it.

Cheers,

PR

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr