Re: [mizar] Strong Mizar wish: linking to consider (fwd)

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

> For the moment I would be already 
> happy to
> reach some agreement on the representation of 
> mathematical EXPRESSIONS. 

The Mizar syntax is at http://mizar.uwb.edu.pl/language/syntax.html. The 
terms are quite standard, some less common things might be Fraenkel terms 
(i.e. terms can contain formulas), explicit typing formulas... e.g.
"-4/-2 is natural number"; as Freek noted, the term-dependent types, and 
the possibility to prefix types with clusters .. e.g. "finite non empty 
set". 
It is probably not a big problem to represent them in the current formats 
(having glanced at OMDoc). 

I think a more substantial changes are necessary to accommodate the Mizar 
overloading mechanisms. E.g. MathML has a presentation and content 
mark-up, which in Mizar would correspond to the user-symbol level and the 
constructor level. But there is another (theory dependent) "notation" 
level between these two in Mizar, implementing some syntactic sugar 
(e.g. synonyms, expandable definitions) and overloading. Without 
information about this level, it is impossible to do some transformations 
of the presentation correctly.

The constructor (content) level can be used, but it generally doesn't have 
a unique translation to the user or notation level (it is a price for 
having the syntactic sugar). 
E.g. the mode definition "Subset of X" expands to "Element of bool X" and
"Subset-Family of X" expands to "Subset of bool X". So if we have 
"Element of bool bool X" on the constructor level, there are (usually) 
three possible user-level representations.
 

Regards,
Josef