[isabelle] Isabelle/ML - function for automatic generation of parametricity relations from types



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.

-- 
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 MHonArc.