Stream: General

Topic: No relator created for data type involving `set`

Wolfgang Jeltsch (Sep 10 2021 at 15:51):

Consider the following (contrived) example:

datatype 'a rep = Rep ‹'a set›

typedef 'a abs = "{Rep A | A :: 'a set. finite A}"
  by blast

setup_lifting type_definition_abs

The last line gives the following warning:

Generation of a parametrized correspondence relation failed.
Reason:  No relator for the type "rep" found.

And indeed no relator has been created for rep.

However, the following succeeds:

typedef 'a direct = "{A | A :: 'a set. finite A}"
  by blast

setup_lifting type_definition_direct

This shows that there is a relator for set and that setup_lifting can work with it.

Why isn’t there a relator for Rep? Furthermore, how is this problem fixed most easily? In the real, non-contrived development, there are multiple set fields.

Wolfgang Jeltsch (Sep 10 2021 at 18:58):

Hmm, let me have a guess: The set type is not a BNF, since its set function is the identity and a given set can have as many elements as the element type, so that an upper bound on the number of elements that is independent of the element type does not exist. However, datatype apparently generates a relator only for those type parameters that aren’t used as parameters of types that aren’t BNFs. Is this correct?

Dmitriy Traytel (Sep 11 2021 at 07:15):

Yes, this is correct. As a workaround, you can define your own relator on rep and register it with the Lifting package. See https://www.isa-afp.org/browser_info/current/AFP/BNF_CC/DDS.html for an example how this is done (there the function space is the culprit why the mapper/relator do not touch the 'a type variable). The relevant theorems for lifting are the ones carrying attributes (relator_eq, relator_mono, relator_distr, quot_map, and potentially also some of the transfer_rules although I'm not sure there which ones are strictly necessary).

Last updated: Apr 24 2024 at 16:18 UTC