Re: [isabelle] Isabelle/ML - function for automatic generation of parametricity relations from types
- To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] Isabelle/ML - function for automatic generation of parametricity relations from types
- From: mailing-list anonymous <mailing.list.anonymous at gmail.com>
- Date: Sat, 26 Oct 2019 15:52:06 +0300
- In-reply-to: <CALaF1U+j=7jfg+_H6HgkgD2E=8A9di65P2mYmcRvccF8zMj45w@mail.gmail.com>
- References: <CALaF1U+j=7jfg+_H6HgkgD2E=8A9di65P2mYmcRvccF8zMj45w@mail.gmail.com>
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
On Sun, May 5, 2019 at 10:28 PM mailing-list anonymous <
mailing.list.anonymous at gmail.com> wrote:
> Dear All,
> This may be another naive question in relation to Isabelle/ML sources.
>  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.
>  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.
> Please accept my apologies for posting anonymously. This is done to
> protect my privacy. I can make my identity and my real contact details
> available upon request in private communication under the condition that
> they are not to be mentioned on the mailing list.
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and