[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] PVS GPLed




On Mon, 15 Sep 2008, Freek Wiedijk wrote:

Josef:

No.  The parse tree will be the same.  The interpretation of
the symbols will change, but the parse tree will be the same.
This all depends on the exact definitions of these notions.
I understand what you're saying here.

Still I want to make the point that the _tree_ (as a tree)
will be the same.
We talked about a _parse tree_, which is labeled: 
http://en.wikipedia.org/wiki/Parse_tree. Even for a (unlabeled) _tree_ 
there is e.g. the problem of hidden arguments (a redefined functor 
may take some more arguments on the semantic level, so there will be 
additional edges in the tree). Or expandable vs. normal types - again 
change already the _tree_ on the semantic level.
And there might be some weird cases even without this, e.g. when 
constructors with the same name are defined for several arities ...
Josef