Email Gateway (Aug 22 2022 at 19:46): Email Gateway (Aug 22 2022 at 19:46):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
This may be another naive question in relation to Isabelle/ML sources.
[1] contains the following statement in section 6:
"The relation between the two constants is obtained purely syntactically:
we start with the type (e.g., (β → γ) → bool for inj) and replace every
type that does not change (γ and bool) by the identity relation =, every
nonnullary type constructor by its corresponding relator (→ by ==> and list
by list_all2) and every type that changes by the corresponding transfer
relation (β by T)"
Essentially, the statement above outlines a simple procedure for the
automatic construction of the parametricity relations based on the types of
terms for which they need to be derived (under some mild assumptions). It
should enable the design of a function similar to
"fun typ_to_pr T Tts : typ -> (typ * term) list -> term"
that converts a given type T into a parametricity relation, under the
assumptions that Tts provides a lookup table that maps the types that
change to the terms that represent appropriate relations (of course, side
conditions can be introduced later, as required).
I would like to understand if there exists an implementation of a similar
function somewhere in the Isabelle/ML source code. I did look around before
asking the question, but I am still not familiar with the entire
Isabelle/ML code base. This seems like a very likely candidate for
something that I cannot seem to notice and, I thought that there would be
many regular users of the mailing list who could point me in the
right direction without having to do any investigation.
Also, if this function exists, I am curious to know whether/why it is not
available to the end users. It would be useful to be able to generate a
parametricity relation given two terms of matching types automatically.
[1] O. Kunčar and A. Popescu, “From Types to Sets by Local Type Definitions
in Higher-Order Logic,” in Interactive Theorem Proving, J. C. Blanchette
and S. Merz, Eds. Cham: Springer International Publishing, 2016, vol. 9807,
pp. 200–218.
Email Gateway (Aug 22 2022 at 20:50):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to provide a reply to one of my own old questions. Apparently,
there are two files in the Isabelle/HOL Library that provide the
functionality that I was seeking: "HOL-Library.Conditional_Parametricity.ML"
and "HOL-Library.Conditional_Parametricity.thy". Moreover, the
parametricity property is also proven automatically. Annoyingly, until
recently, I was not aware of the existence of these files and, by now, I
have written my own module that provides the functionality that is nearly
identical to the functionality of the aforementioned theories :-). I am
writing this reply, primarily, to minimize the risk of someone else getting
into the same trap. I am also curious as to why this module has not been
used anywhere in the source files of Isabelle/HOL. In my opinion, it would
be useful to update the existing source files to raise the awareness of the
existence of the module and minimize the boilerplate code. Also, in my
view, it would be useful is someone could integrate it with the Transfer
package.
Thank you
Last updated: Nov 21 2024 at 12:39 UTC