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



On 08/24/2016 12:35 PM, Andrei Popescu wrote:
> There is no a priori notion of 'meaningful' definition, apart from
> what the system accepts. So yes, from the point of view of the
> logical system these situations must be treated in the same way, in
> particular taken equally seriously. And this while ignoring the
> unnecessary reference to that malicious 'somebody who has studied the
> source code' -- who happens to be named Ondrej and happens to have
> been working on something else when he discovered that. But you know
> very well from day one the story behind this discovery and its
> ordeals.

Let me add my personal bit to Larry's "somebody who has studied the source code". Au contraire, I didn't study the source code at all. I wanted to prove that Local Typedef is a consistent extension of Isabelle/HOL and for that I needed semantics of Isabelle/HOL first. Frankly, my approach was fairly naive back then and I had to understand the logic of Isabelle/HOL first. When I realized that overloaded constants can be used in type definitions, an idea struck me and I could easily work out a cyclic definition and prove False from it.

That said, let me stress that the proof of False wasn't a consequence of studying the source code (which Larry seems to use in a derogatory way) but a consequence of a deeper understanding of Isabelle/HOL's logic while I was trying to work out a semantic explanation of the logic. So if somebody imagines that our work was started by a hacking session that discovered an implementation bug, then this is a misleading picture. I still claim that I stumbled upon a rather fundamental problem (regardless if it was documented in some form or not), namely how to combine overloading with type definitions in a consistent way.

Ondrej








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