Re: PVS GPLed

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