On Mon, 15 Sep 2008, Freek Wiedijk wrote:
The correct parse tree can actually be *changed* by adding or removing functor definitions.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 think a part of what Bill means is that type/overloading disambiguation is part of "parsing" (in Mizar lingo: "parsing" is distributed across the "Parser" and "Analyzer" pass). With this definition "parse tree" (as in XML after "Parser" and "Analyzer") really includes (actually: mainly consists of) the "interpretation of symbols" ("constructors"), so it will be different. Obviously a very frequent case is that there will be no parse tree when a definition is changed/added/removed, because a type error will occur.
Josef