Email Gateway (Aug 22 2022 at 11:13): Email Gateway (Aug 22 2022 at 11:13):From: Andrei Popescu <a.popescu@mdx.ac.uk>
Hi Makarius,
First, I thank you very much for looking into this. I have a conference tutorial to prepare for this Sunday, and this is why I will be rather brief in my reply. Next week I'll address
the points you are raising in much greater detail.
Second, if you can, please ignore that reference to the technical report -- it is indeed a lingering reference, which we unfortunately forgot to remove. At the preparation of the camera-ready, we managed to
include sufficient technical details in the paper, especially since we received an extra page. So now the paper essentially includes that report. I am here to offer any missing technical details, should you
request any -- but if you read the paper in good faith, it is likely you will not even need additional explanations.
Third, I kindly ask you that, during our discussion about this, you respect my different opinion here, which can be summarized as follows:
BEGIN opinion
Even though Isabelle/HOL is implemented on top of a logical framework, we can conceptually speak about its structure as:
(A) a logic L, consisting of axioms and rules of deduction
(B) the logic L augmented with a definitional mechanism (namely, type and constant definitions) -- let me call it L_D
The current situation with Isabelle/HOL is the following: Even though L is consistent (in that it cannot prove False), L_D is inconsistent (in that it can prove False).
END opinion
Even though, as the developer of the Isabelle software , you believe the situation is much more complex, I kindly ask you to make an effort and understand this point of view.
The purpose of any logical framework (including Isabelle/Pure and Edinburgh LF) is to facilitate the implementation of a logic, not to intrude with the logic. I am sure that the implementation of
Isabelle/HOL inside Isabelle/Pure does a good job at achieving this. I am saying this as a fairly experienced user of Isabelle/HOL.
The development from our paper works with the logics L and L_D assumed above. Again, if you read the paper in good faith, you will be able to understand what is being proved there and perhaps
convince yourself that the proposed change to the system will at least achieve the following goal: prevent certain ways of proving False which is particularly disturbing to many many users.
Finally, I have a possibly strange request: Please do not trust your judgement alone, because you (like anybody else) may be wrong, and may not realize it because of the way you look at things.
There must be someone (at least one person) on this mailing list whose judgement you trust. Please ask that person for a second opinion about: (1) the actual problem discussed here and (2) the solution we propose in the paper.
If possible, please also make the name of that person public.
All the best and talk to you again soon,
Andrei
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.
Email Gateway (Aug 22 2022 at 11:13):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Sorry, a couple of further brief notes:
This proper distinction also explains, why typedefs were not treated in the past, because it is hard to understand them in generic Isabelle/Pure, without an unfriendly takeover of the framework by HOL troups.
It is of course impossible. We have to let the HOL troops in at this point, there is no way around this.
A few more notes on the paper: I actually liked the "Inconsistency Club" versus "Consistency Club", although it is hard to define that boundary. Just a single Boolean value to measure the reliability and robustness of a
proof assistant in black or white is a bit lacking. Apart from shades of grey, such a measure desparately needs more than one dimension.
"Consistency Club" here does not refer to bullet-proof systems, but to formal efforts of partly ensuring consistency (whatever that means :-) ). In particular, this club does not contain theorem provers, but formal developments.
All the best,
Andrei
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.
Email Gateway (Aug 22 2022 at 11:13):From: Makarius <makarius@sketis.net>
I joined this thread with the intention of a serious discussion, and I
still mean that.
Makarius
Email Gateway (Aug 22 2022 at 11:14):From: Makarius <makarius@sketis.net>
OK, so I take the pulished paper as is, taken from
http://www4.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf
In the third round of looking at it, I have now started to read the
technical part and have already learned many interesting things. I will
comment (and criticize) more later, when the big picture has evolved a bit
further.
I need to appeal again to the professional routine of the Isabelle
development and release process. Users will have true reasons to get
worried, when non-trivial changes to core system components and their very
foundations can be pushed-in just by making a lot of noise in public.
I've not been at the ITP talk, but I can imagine how it went, just by
extrapolating the style and manner of some paragraphs in the paper.
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.
Adapting the ideas presented in the presented paper in the proper way for
Isabelle will not take as long as BNF datatypes, but it is not immediate.
It could have been finished already, if we did not have serious
meta-problems that are still ignored by most participants of the debate.
This is why I spend so much time here, instead of looking through ML
sources.
Makarius
Email Gateway (Aug 22 2022 at 11:14):From: Larry Paulson <lp15@cam.ac.uk>
On 20 Sep 2015, at 14:12, Makarius <makarius@sketis.net> wrote:
Users will have true reasons to get worried, when non-trivial changes to core system components and their very foundations can be pushed-in just by making a lot of noise in public.
Quite true. However, we took the decision a long time ago to detect and reject cyclic constant definitions. In this example, a cycle evades detection because it involves a typedef. Closing this loophole would not represent any change in policy.
Email Gateway (Aug 22 2022 at 11:15):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi 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:
You wrote:
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,
Andrei
[*] 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.
Last updated: Apr 16 2024 at 12:28 UTC