Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu



On 21.08.2016 12:21, Lawrence Paulson wrote:

This question is a perfect example why I dislike the use of the word âinconsistency" in connection with the work of KunÄar and Popescu. Probably most people associate that word with some sort of incorrect logical reasoning. However, their work is concerned with Isabelle's automatic detection and rejection of circular definitions.

Indeed, this misleading tale told around the work by Kuncar / Popescu greatly subtracts from otherwise fine technical improvements.

I have already pointed out many times that it was mainly a change of the documented situation in Isabelle/HOL. Before there was a section in the manual saying clearly that typedefs are not fully checked. Afterwards, the officially supported typedefs were (1) extended to typedefs depending on overloaded consts (which was previously not covered) and (2) the extended scheme checked by the system.

Thus the isar-ref manual entry of HOL typedef could be changed accordingly: the system has become more user-friendly, since the user is no longer blamed implicitly for not having read the manual when something goes wrong; instead the system complains explicitly. In practice, such a situation was never seen, though, because the counter-example from the paper by Kuncar / Popescu was constructed synthetically to illustrate a theoretical point.


        Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.