Re: [isabelle] Isabelle Foundation & Certification (answer to Makarius)
I propose splitting this thread in two (as other people also implicitly suggested):
(1) Should cyclicity checks through typedefs be introduced, to prevent situations such as Example 2?
I have to say that this paragraph from your postings has made my day:
>> The proposed changes of the present paper are genuine feature additions
>> that go beyond the known and documented model of Isabelle/HOL. This is
>> why I reduced the priority to a reasonable level. And in fact, we are
>> talking here about a few months latency of TODO-list pipeline -- things
>> routinely take much longer than that. Isabelle is not a research
>> prototype that can be changed arbitrarily at a high rate.
If I read it correctly, your answer to the question is "Yes, but let's do it properly."
I don't think anybody can argue with the fact that you are the person to do it properly.
But emphasizing the "Yes" part, and perhaps placing it at the beginning of your first answer
on this thread would have helped immensely.
(2) Should typedef really be axiomatic, or should it be made definitional in Isabelle/HOL?
Here, you also seem to not be completely satisfied with the current status:
>> Of course, one could argue if it is a good idea to treat typedef like
>> that. This would lead to the very start of a serious discussion -- one
>> without rumors and unnecessary confusion caused by worrying about
>> publicity or "bad press"
Here, I have many things to add. In fact, I would like to argue strongly for having typedef definitional in Isabelle/HOL, and would like
to invoke the results from our paper as a justification for the possibility of enforcing *and claiming* definitionality.
I know there will be a long discussion here, because our notions of definitionality differ and because our notions
of logical framework differ. I am sure that at the end of this discussion I will convince you that I have a point, and probably
you will show me that my point needs to be refined in order to be applicable to the real Isabelle/HOL.
But I am looking forward to have this discussion in a relaxed manner,^[*] outside of the issue (1).
>> You may remember yourself that the initial idea of BNF (co)datatypes was
>> expected to be implemented in one year, or so. Ultimately it required
>> many years, and several wizards to finish the job. Behind the scenes we
>> even had to get David Matthews involved, to extend the playground of the
>> ML platform. I also had to make "dangerous experiments" again -- as you
>> call it in the paper -- in order to have it all go through smoothly.
Interesting -- I did not know about the required extension of the infrastructure. And of course
I appreciate the support you offered with the BNF package; I also hope you find it to be a useful addition to the system.
All the best,
[*] We had such a (very fruitful and pleasant) discussion the first time I showed you the plan for the BNF package.
Btw, that package is designed with the assumption that typedef is/can-be definitional. If we truly thought of typedef as (hopelessly)
axiomatic, I and my coauthors would not have gone to the trouble to reduce a sophisticated (co)datatype universe all the way down to typedef.
And this is also true about the previous datatype package by Stefan.
Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.
If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS. There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.
This archive was generated by a fusion of
Pipermail (Mailman edition) and