Re: [mizar] Re: Mizar Parser

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Freek Wiedijk wrote:
> 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.

Yes, you're right in both points. 
First, the reconstruction from
constructor is difficult.  You may see an attempt to it
in MML Query in browser part.  All formulae are reconstructed
there.  I use there only first notation of original constructor
for simplicity.  The problem here is that in this case
composition of functions is represented according to the definition
of composition for relations where arguments are switched.

definition let f,g;  :: FUNCT_1
 redefine func f*g;
 synonym g*f;
end;

Also, the problem is to reconstruct 'or', 'implies', 'iff', and 'ex'
from formulae with 'not', '&', and 'for' only.  The term
"to reconstruct" here means rather to make it readable.

The problem is also taking into parentheses.  But it can be
easly solve like it is done in FM translation.

Second,
 "x is irrational", "not x is rational", "x is not irrational",
 "x is not non rational", "not x is non rational"
All these have the same internal representation.


Best,
Grzegorz