Email Gateway (Aug 22 2022 at 18:53): Email Gateway (Aug 22 2022 at 18:53):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
Recently I started working on a small personal project in Isabelle/HOL. The
work evolved from several posts on Stack Overflow and another independent
project on GitHub (https://github.com/AresEkb/Simple_OCL). The
aforementioned posts on Stack Overflow are presented in the enumerated list
below:
1. What kind of functions preserve properties of closure?
<https://stackoverflow.com/questions/52565266/what-kind-of-functions-preserve-properties-of-closure/>
2. How to lift a transitive relation from elements to lists?
<https://stackoverflow.com/questions/52962519/how-to-lift-a-transitive-relation-from-elements-to-lists/>
3. How to lift a transitive relation to finite maps?
<https://stackoverflow.com/questions/53580515/how-to-lift-a-transitive-relation-to-finite-maps/>
However, a significant part of the content of the project is not directly
related to the aforementioned posts and the aforementioned repository. The
development of the project (HOL-DS_Ext) that I would like to discuss in
this email is being done in the context of a GitHub repository
<https://github.com/xanonec/HOL-DS_Ext> that can be found at
https://github.com/xanonec/HOL-DS_Ext.
A description of the project is provided on the front page of the
repository. However, I also provide a brief summary in the form of an
enumerated list below. The main contributions are related to the type
alist from
the theory HOL-Library.DAList and the theory HOL-Library.AList. However,
hopefully, the project contains other useful results.
1. It is indicated with the relevant FIXME comments in the theory
HOL-Library.DAList that the theory does not provide many results for the
type alist that already exist in the standard library for the type list.
The project that I am working on addresses this issue and transfers many
results about the type list to the type alist.
2. The project makes an attempt to integrate the theories
HOL-Library.AList and HOL-Library.Permutation by providing congruence rules
for many functions that are defined in the theory HOL-Library.AList under
certain mild conditions. Furthermore, the project includes a theory of
permutation for the type alist.
3. A new type that can be shown to be isomorphic to the type fmap is
defined as a quotient type of the type alist. This type provides an easy
way of transferring the results from the type list to the type fmap through
the results about the type alist. Some of the relevant transfer rules are
provided and applied to several results about the type list (e.g. the
induction rule list_all2_induct).
I would like to discuss the project briefly with the Isabelle/HOL community:
1. The subject of the project is closely related to the theories that
already exist in the standard library of Isabelle. In fact, I believe, the
project could be seen as a natural extension of the existing theories List,
HOL-Library.Permutation, HOL-Library.AList, HOL-Library.DAList and
HOL-Library.FMap. Given that the subject of the aforementioned theories
falls into the category of general data structures, I can only imagine that
there would be a substantial amount of interest from many independent
parties to develop these theories further. I am, somewhat, external to the
Isabelle/HOL community as a whole (I consider Isabelle/HOL to be a past
time activity). Thus, I cannot be aware of all ongoing developments outside
of the official repository. Furthermore, shamefully, I am rediscovering the
standard library of Isabelle almost every day. Hence, I cannot be entirely
certain that some of the work that I have done or intend to do in the
context of this project has not been done or is being done by someone else
concurrently. Therefore, I would appreciate any comments or advice in
relation to this matter from the developers of the aforementioned theories
or anyone else who may be working in this area. In particular, I seek
answers to the following questions:
1. Have the results that are presented in the repository already been
formalised somewhere else?
2. Is something similar to the project that is presented in the
repository already being done in the context of the development of the
standard library?
3. Is something similar to the project that is presented in the
repository already being done in the context of the development of an
independent library on the AFP?
4. Is something similar to the project that is presented in the
repository already being done by someone privately?
2. If the answers to the questions 1.1-1.4 are "no", then I would also
like to obtain a preliminary assessment of the relevance of the results
that I propose in the context of the project. Do you believe that such
results could make an appropriate subject for an entry in the AFP? If so,
do you foresee that there could be further interest in adding some of the
results from the project to the standard library in the future? When/if
answering these questions please note that the project is still in the
early stages of the development: many sections are incomplete and some of
the proofs are of substandard quality (these issues would be addressed and
further results would be added before making an attempt to submit the
repository to the AFP).
Thank you
Email Gateway (Aug 22 2022 at 18:53):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hi Xanonec,
I am not the right person to answer all yours questions. I just would like
to remark that there is an interesting approach to List and Permuation
using homotopy type theory due to Vladimir Voevodsky. I provide you the
references in Coq:
https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/Lists.v
https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/StandardFiniteSets.v
In his lectures at Oxford, Voevodsky explains his approach:
all the lectures (see point 9 in the list of lectures):
https://www.math.ias.edu/vladimir/Lectures
this particular lecture talking about permutations:
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/141126-2.mp4
Coq is not the only way to use HoTT. Here is a link to a project of HoTT in
Isabelle: https://github.com/jaycech3n/Isabelle-HoTT
So, if you are interested in exploring List and Permutations in Isabelle,
following Voevodsky's approach, you have all you need.
Which are the advantages of combinatorics developed from the point of view
of Homotopy Type Theory which respect to his counterpart in Simple Type
Theory? Well, I will speculate a little bit: Topological Quantum Computing
http://math.uchicago.edu/~may/REU2016/REUPapers/Lee.pdf
I guess that Homotopy Type Theory will be a natural framework for formal
verification of programs written for a topological quantum computer. Of
course, some skeptic people may disagree. Here is an example of such a
program (an algorithm for knots-invariants):
https://www.youtube.com/watch?v=smX2lSyi2js
By the way, there will be a Workshop on Univalent Mathematics:
https://unimath.github.io/bham2019/
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 18:53):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear José Manuel Rodriguez Caballero,
Thank you for your reply. I highly value your comments and the references
that you provided. Indeed, it would be interesting to explore lists and
permutations in Isabelle using HoTT. Nevertheless, this would have to be a
subject for a different project.
I believe that my question may not have been entirely transparent. Within
the context of the project in the repository
<https://github.com/xanonec/HOL-DS_Ext>, I am merely transferring certain
existing results about the type list from the theory List to the types
alist (defined in the theory HOL-Library.DAList) and fmap (defined in the
theory HOL-Library.Finite_Map). I am using the project, primarily, to learn
more about the datatype infrastructure and the lifting/transfer package in
Isabelle/HOL. However, I would like to understand if any of the results
from this project may be useful. After all, I believe, some of these
results address the FIXME comments that I noticed in the theory
HOL-Library.DAList.
The type fmap can be viewed as an associative list invariant under the
permutation of its elements, as an fset from the theory HOL-Library.FSet
and as a map from the theory Map. The process of the transfer of the
results from the type map (from the theory Map) to the type fmap has
already been nearly completed in the context of the development of theory
HOL-Library.Finite_Map. However, I believe that many results that can be
found in the standard library about the types list and fset do not have
their equivalents for the type fmap. In general, it is my goal for the
project in the repository to provide for each lemma in the standard library
about the types list and fset, a similar lemma (under some mild
restrictions) for the type fmap using the transfer package. Also, given
that I found that it is convenient to perform the transfer of the results
about the type list to the type fmap using the type alist, there is an
additional benefit of enriching the theory of the type alist with the
results about the type list that have not yet been transferred to the type
alist.
Thank you
Last updated: Apr 26 2024 at 20:16 UTC