[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