Email Gateway (Aug 22 2022 at 19:25): Email Gateway (Aug 22 2022 at 19:25):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to ask a question in relation to the further development of
the functionality of the framework "Types-To-Sets".
I am working on several personal projects that rely on "Types-To-Sets".
However, as was previously noted on the mailing list, the framework does
have its limitations. I would be interested in improving the functionality
of the framework. However, before I do any work in this direction I would
like to understand if anyone else is already working towards this goal and
whether or not there exists a development plan for this framework.
Naturally, if anyone has any particular ideas about how the framework can
be improved, I would be interested in learning about them.
Background information
In the last two months I relativised a substantial number of results about
algebraic structures and abstract spaces from the main HOL library using
the methodology suggested in [1] and collected the results in an
independent library (of course, please keep in mind that the library is a
work in progress):
https://github.com/xanonec/HOL-Types_To_Sets_Ext
The initial goal was to obtain a locale-based topology library similar to
HOL-Algebra. As it stands now, the library can be seen as a complement to
the HOL main library. For each axiomatic type class/locale whose carrier
set is a universe (of course, not every class/locale was relativised yet),
the library provides a relativised locale with an explicitly defined
carrier set.
For example, for the class topological_space from the main library
class topological_space = "open" +
assumes open_UNIV [simp, intro]: "open UNIV"
assumes open_Int [intro]: "open S ⟹ open T ⟹ open (S ∩ T)"
assumes open_Union [intro]: "∀S∈K. open S ⟹ open (⋃K)"
the library of relativised results provides a locale
locale topological_space_ow =
fixes 𝔘 :: "'at set" and τ :: "'at set ⇒ bool"
assumes open_UNIV[simp, intro]: "τ 𝔘"
assumes open_Int[intro]: "⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)"
assumes open_Union[intro]: "⟦ K ⊆ Pow 𝔘; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)"
Of course, the definitions associated with a given type class or even a
combination of type classes were relativised as well. For example, the nhds
filter for the type class topological_space
definition (in topological_space) nhds :: "'a ⇒ 'a filter"
where "nhds a = (INF S∈{S. open S ∧ a ∈ S}. principal S)"
is relativised as
definition nhds :: "'at ⇒ 'at filter" where
"nhds a = (Inf_on 𝔘 (principal ` {S. S ⊆ 𝔘 ∧ τ S ∧ a ∈ S}))"
In certain cases, more creative approaches were employed. For example, for
reasons of compatibility with the main class-based library, the type filter
was reused by providing new constants filter_on, inf_on and Inf_on to make
the type suitable for interpretation as complete/distributive lattices on
an explicit carrier sets, e.g.
interpretation filter_clow:
complete_lattice_ow "{F. filter_on 𝔘 F}" "(≤)" "(<)" "inf_on 𝔘" sup
bot "principal 𝔘" "Inf_on 𝔘" Sup
Once all definitions were provided, the theorems were relativised in a
semi-automatic manner. For example,
lemma tendsto_compose: "g ─l→ g l ⟹ (f ⤏ l) F ⟹ ((λx. g (f x)) ⤏ g l) F"
is relativised as
lemma tendsto_compose:
assumes "g 𝔘A ⊆ 𝔘B"
and "l ∈ 𝔘A"
and "f 𝔘C ⊆ 𝔘A"
and "filter_on 𝔘C F"
and "(on 𝔘B with τb: g ⤏⇩o⇩w g l) (on 𝔘A with τa at l)"
and "(on 𝔘A with τa: f ⤏⇩o⇩w l) F"
shows "(on 𝔘B with τb: (λx. g (f x)) ⤏⇩o⇩w g l) F"
Nevertheless, as noted previously, "Types-To-Sets" does have limitations
and, at the moment, it is not very user-friendly. The library certainly
contains a substantial amount of boilerplate code, which I would like to
reduce. However, it seems that this cannot be done without providing
extensions/amendments to "Types-To-Sets" at the ML level.
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.
Email Gateway (Aug 22 2022 at 19:27):From: Lawrence Paulson <lp15@cam.ac.uk>
Let me just offer my enthusiastic encouragement for you to continue!
I have never managed to figure out how Types-To-Sets can be used, despite scrutinising example developments, so you deserve full credit simply for that. It definitely needs to be made more usable.
Meanwhile the next release will contain tens of thousands of lines of new material about relativised concepts, not using Types-To-Sets but simply with new proofs ported from HOL Light. This is independent from your work, of course, but maybe the efforts can eventually be combined.
Larry
Email Gateway (Aug 22 2022 at 19:27):From: Makarius <makarius@sketis.net>
Recall that it is just an experiment to support a research paper in 2016
by Ondřej Kunčar and Andrei Popescu
https://link.springer.com/chapter/10.1007%2F978-3-319-43144-4_13
In 2016 and 2017 I have provided a lot of concrete feedback on the
implementation to turn it into more usable state (e.g. proper use of
Isar context commands), but somehow the project seems to have become
inactive.
In the meantime Fabian Immler has made some improvements, but it is
still only experimental.
Overall, there is also a high-level question about the use (or better
non-use of Types-To-Set). It is based on a genuine extension of the HOL
logic, and I am unsure what other HOL users say about it. For me this
discussion is still pending.
Meta note: I am not communicating with people that don't expose there
real name. I have just seen a bit too many recent reports about
anonymous authors doing mischief on Wikipedia.
A proper open-source project works like scientific research, by people
who stand with their own name and reputation for what they do and describe.
Makarius
Email Gateway (Aug 22 2022 at 19:27):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Lawrence Paulson/All,
Thank you for your reply.
I have followed the development of HOL-Analysis in the last several months.
Indeed, the work that is being done in the context of this development is
very impressive.
Thank you for your kind words about my work. However, of course, the credit
for the development of Types-To-Sets belongs to the authors of the original
article and the credit for the development of the methodology that I am
using belongs to Fabian Immler and Bohua Zhan.
With my application of Types-To-Sets, I wanted to obtain a mathematics
library that is based entirely on classes and locales and uses a uniform
('software') structure both for algebraic structures and abstract spaces.
The main library of Isabelle/HOL, effectively, already achieves this goal.
However, the carrier sets for all structures are UNIVs. Types-To-Sets
allows for a nearly seamless conversion of each class/locale that treats
the carrier sets as UNIV to an equivalent locale with an explicitly defined
carrier set in a semi-automated manner. The main selling points of this
approach are
1. Both explicit carrier sets and UNIV are treated in a uniform manner
(also, my intention, is to introduce a database that relates the
relativised and non-relativised theorems somehow).
2. The results about explicit carrier sets are obtained from the results
about UNIV in a semi-automatic manner, which implies less typing and
fewer loc.
3. Uniform 'software' structure for all algebraic structures and
abstract spaces.
4. It promotes the development of the main Isabelle/HOL library.
To elaborate on clause 3, please see the comparison of the locale
topological_space_ow (relativisation of the class topological_space from
the theory Topological_Spaces) and the locale group_add_ow (relativisation
of the class group_add from the theory Groups):
locale topological_space_ow =
fixes 𝔘 :: "'at set" and τ :: "'at set ⇒ bool"
assumes open_UNIV[simp, intro]: "τ 𝔘"
assumes open_Int[intro]: "⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)"
assumes open_Union[intro]: "⟦ K ⊆ Pow 𝔘; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)"
locale group_add_ow =
minus_ow 𝔘 minus + uminus_ow 𝔘 uminus + monoid_add_ow 𝔘 plus zero
for 𝔘 :: "'ag set"
and plus (infixl "⇧+⇩o⇩w" 65)
and minus (infixl "-⇩o⇩w" 65)
and uminus :: "'ag ⇒ 'ag" ("-⇩o⇩w _" [81] 80)
and zero ("0⇩o⇩w") +
assumes left_inverse: "a ∈ 𝔘 ⟹ (-⇩o⇩w a) ⇧+⇩o⇩w a = 0⇩o⇩w"
and add_inv_conv_diff: "⟦ a ∈ 𝔘; b ∈ 𝔘 ⟧ ⟹ a ⇧+⇩o⇩w (-⇩o⇩w b) = a
-⇩o⇩w b"
As you can guess, it is now a very small step to provide the relativisation
of the class topological_group_add on an explicit carrier set.
Please accept my apologies for another sales pitch. The main reason why I
am drawing so much attention to the development is that there is no other
way for me to find out whether or not someone else is doing something
similar, which is, of course, a grave concern to me.
As a side note, I noticed that my previous email contains a great number of
typographical errors (normally, I do not confuse types and type
constructors).
Thank you
Email Gateway (Aug 22 2022 at 19:27):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Makarius Wenzel/All,
Thank you for you reply. I would be very interested in learning more about
the concrete feedback that you provided in 2016 and 2017. Has it been
published anywhere? Would it be possible to provide any hyperlinks to this
feedback?
I would also like to provide feedback with regard to your concerns about my
identity:
1. I have already mentioned on this mailing list that I can provide my
name/real contact details upon request, with the understanding that you
agree not mention them on the mailing list. In fact, I have recently edited
my signature for this email account to include this information. Given that
you expressed your concerns about my identity and possibility of me being
involved in mischief, I will send you a letter from the email that I
normally use for professional correspondence later today. Of course, if I
will ever make an attempt to submit any of my work to the AFP, it will be
under my real name.
2. There is a number of reasons why I do not wish to disclose my
identity.
1. In the past, I had problems with spam and online/telephone scam. I
had to close two email accounts, one Skype account and had to change my
mobile telephone number twice. I can only assume that I was
targeted due to
a combination of my country of origin (Eastern Europe) and
having some kind
of public profile at a certain point in my life. Some people will go
through great lengths if they suspect that you have money and may be,
somehow, susceptible to share it :).
2. At the moment, Isabelle/formal proof is merely a hobby for me.
Given that I have no publications in this area, I would prefer potential
employers not to know too much about my involvement in this area, given
that most of my previous experience was in an area that was not closely
related. I believe that I will become more forthcoming about my
involvement
if I will ever submit anything to the AFP.
3. I have further, slightly more personal reasons, for not wishing to
disclose my identity publicly.
3. While I have no evidence, I can only guess that there may be poorly
written articles on wikipedia that were written by people who disclosed
their identities. However, I have little doubt that there are also many
good contributions from people who did not wish to disclose their
identities. For what it is worth, I have seen published articles in
academic journals of good standing that were (many years after their
publication) shown to contain substantial errors and served to cause great
confusion. Also, there are many regular users of Stack Overflow who
provided good answers without disclosing their identities.
4. We owe Bitcoin to an anonymous contributor :).
Thank you
Email Gateway (Aug 22 2022 at 19:27):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Recall that it is just an experiment to support a research paper in 2016
by Ondřej Kunčar and Andrei Popescu
https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flink.springer.com%2Fchapter%2F10.1007%252F978-3-319-43144-4_13&data=02%7C01%7Ca.popescu%40mdx.ac.uk%7Cb30c5557591845e8acc508d6c18d0028%7C38e37b88a3a148cf9f056537427fed24%7C0%7C0%7C636909208665363247&sdata=eRLNFLsiaQEq%2B%2BtqlqThR%2B3q9BUGUg1YCEijWZWDYeE%3D&reserved=0
In 2016 and 2017 I have provided a lot of concrete feedback on the
implementation to turn it into more usable state (e.g. proper use of
Isar context commands), but somehow the project seems to have become
inactive.
In the meantime Fabian Immler has made some improvements, but it is
still only experimental.
Overall, there is also a high-level question about the use (or better
non-use of Types-To-Set). It is based on a genuine extension of the HOL
logic, and I am unsure what other HOL users say about it. For me this
discussion is still pending.
Meta note: I am not communicating with people that don't expose there
real name. I have just seen a bit too many recent reports about
anonymous authors doing mischief on Wikipedia.
A proper open-source project works like scientific research, by people
who stand with their own name and reputation for what they do and describe.
Makarius
Email Gateway (Aug 22 2022 at 19:27):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
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:
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.
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.
Email Gateway (Aug 22 2022 at 19:27):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Last updated: Apr 24 2024 at 12:33 UTC