Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)



Dear Anonymous, 

Personally, I think that your goals 1 and 2 are wisely chosen, and could bring a very nice contribution. As for the question of other projects related to the topic, I don't know of other work (besides that of Fabian Immler and Bohua Zhan which you cite and the ones mentioned by Rene Thiemann in a previous thread). 

Best wishes, 

Andrei 


From: mailing-list anonymous <mailing.list.anonymous at gmail.com>
Sent: 16 April 2019 00:08
To: Andrei Popescu; cl-isabelle-users at lists.cam.ac.uk
Cc: Makarius; Lawrence Paulson; ondrej.kuncar at gmail.com
Subject: Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)

Dear Andrei Popescu/All,

After using Types-To-Sets for the relativisation of the results from the main library of Isabelle/HOL for a little while, I came to a conclusion that the two main problems with the existing methodology are the 'boilerplate' code associated with having  to restate the names of the relativised theorems at least twice and, more importantly, forward compatibility with the potential changes to the class/locale that is being relativised (of course, it would also be interesting to understand if there could be a  negative impact associated with the extension of HOL logic and I would like to know more about the arguments that were presented on this subject in the past). I must admit that I am not certain whether further automation, i.e. automatic generation of the relativised  definitions, would be beneficial and make the framework more user-friendly than it is at the moment: usually there are several equivalent ways to present a given relativised definition and I see no reason to force the users to use a pre-defined default.  

In the short-/mid-term, I would like to provide the following functionality that will not require any modifications to the critical code:
1. For the relativisation of definitions, I would like to discharge the necessary proof obligations automatically and store a 'connection' between the original and the relativised definitions as (retrievable) data. 
2. For the relativisation of theorems, I would like to combine the application of a chain of attributes in a single parameterisable command/attribute and (provide an option to) discharge the proof obligations for further user amendments of the relativised  results (e.g. consider the case of an empty carrier set for topological spaces) automatically. Naturally, this would also include the automation of the naming conventions and, therefore, result in a significant reduction of the boilerplate code. Also, the  'connection' between the relativised and non-relativised theorems would be made available as retrievable data. 
  
I believe that having an ability to see whether a given const/theorem was relativised or not and where should be sufficient to make the framework forward compatible with changes to the original class/locale, which, for me, is the main problem with the  large scale application of the framework. The relativised definitions would still need to be provided by the user and the transfer rules would still need to be proven manually. However, at least, the user will not need to provide the statements of the theorems  for the transfer rules explicitly.

In summary, my plan is to introduce several changes to the interface associated with the methodology and not the critical code. 

I am not, specifically, asking for any help with the technical matters, but I would appreciate any insight. I am merely trying to do understand whether or not there are any active R&D projects related to "Types-To-Sets". Given that this project does not  have the highest priority for me and I have much to learn about Isabelle at the ML level, it is likely that I will be working on this project for several months to come in small intervals. I am merely trying to reassure myself that this will not be a wasted  effort because someone else is already working on something better. As a side note, of course, as I mentioned previously, if anyone has any particular ideas about what can be done beyond what is suggested in [1] and in this email, I would be interested in  learning about them. Also, if you suspect that I might be trying to take this work in the wrong direction, I would be thankful to hear from you. 

Thank you

[1] F. Immler and B. Zhan, “Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL,” in Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, ser. CPP 2019. New York, NY, USA: ACM, 2019, pp. 65–77,  event-place: Cascais, Portugal.


On Mon, Apr 15, 2019 at 4:53 PM Andrei Popescu <A.Popescu at mdx.ac.uk> wrote:
 
Dear Makarius, Larry and Anonymous Contributor, 

I thank you for your support of, and contribution to the types-to-sets methodology. I believe the underlying local typedef rule is a very useful (yet gentle) upgrade of HOL, and have always advocated its candidacy for HOL citizenship. (Incidentally, one of  my original motivations was to simplify our BNF/(co)datatype package constructions back in 2011, but in the end the package was developed without it.) 

However, I cannot help with making the types-to-sets machinery more user-friendly since I am not fluent in Isabelle/ML. It is Ondrej Kuncar who has implemented the local typedef rule and the accompanying "unoverloading" rule. And since Ondrej is also a co-developer  of the lifting and transfer package, he is in an ideal position to make things happen; or to share some insights with people who might be interested in taking on such a development. Without more progress on this front, only power-users will use types-to-sets  -- this is a shame, since types-to-sets could be part of the regular users' daily menu. 

Best wishes, 

Andrei 

           



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