Email Gateway (Aug 22 2022 at 21:10): Email Gateway (Aug 22 2022 at 21:10):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I would like to ask a question in relation to one of the existing user
packages: "conditional parametricity"
(HOL-Library.Conditional_Parametricity). Nevertheless, the issue is
slightly more fundamental, as it is concerned with the
integration/duplication of the user-level Isabelle/ML code.
It appears that there is a substantial overlap between the functionality of
one of the command tts_parametricity that is provided as part of the
extension of Types-To-Sets (https://gitlab.com/mikhail.chekhov/tts_extension)
and the existing command parametric_constant. Given that there have been
some discussions about the possibility of adding the extension of
Types-To-Sets to the AFP, I would like to ensure that the issue related to
the duplication of functionality is resolved in the appropriate manner long
before the potential submission (please note that the extension of
Types-To-Sets is still under development).
Unfortunately, I was unaware of the existence of the package "conditional
parametricity" while developing the code for the command tts_parametricity:
I would like to think that I have done everything I could to avoid
duplication. I have even asked a question about the possibility of the
existence of such a package on the list a while ago. Also, it does not seem
to appear anywhere in the standard documentation of Isabelle/HOL.
If my understanding of the functionality of the existing public interface
and the functionality of the package "conditional parametricity" is
correct, I cannot reuse the existing public interface effectively to
provide the functionality that I seek for the command tts_parametricity.
Firstly, tts_parametricity restricts the possible side conditions to
right_total and bi_unique. Secondly, tts_parametricity makes an attempt to
synthesize a new (parametrically related) constant if a given constant is
found to be non-conditionally parametric. Nevertheless, if a given constant
is found to be (conditionally) parametric, tts_parametricity provides the
parametricity property, like the command parametric_constant. If I have not
missed anything, the public interface of the "conditional parametricity"
does not allow for the restriction of the possible side conditions and does
not attempt to synthesize a new constant under any circumstances.
My primary question is what is the canonical solution to such a problem? I
feel that it is my moral duty to make the developers of the "conditional
parametricity" aware of my own development and allow them to decide the
fate of tts_parametricity. Naturally, any input from the community would
also be highly appreciated, as, I can imagine, similar problems arise in
the development of almost every open source project and every community has
some form of canonical procedures towards the resolution of such issues.
Would it be preferable for me to suggest amendments to the existing code
base of "conditional parametricity", instead of providing a new command?
Or, perhaps, on the contrary, the authors would prefer to keep our
developments separate? In the case of the latter, how should I attribute
your work?
Thank you,
Mikhail Chekhov
Email Gateway (Aug 22 2022 at 21:11):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
Please accept my apologies: there are misprints in my previous post. The
first sentence in the second paragraph should read:
It appears that there is a substantial overlap between the functionality of
one of the commands (tts_parametricity) that are provided as part of the
extension of Types-To-Sets (https://gitlab.com/mikhail.chekhov/tts_extension)
and the existing command parametric_constant.
Thank you,
Mikhail Chekhov
Email Gateway (Aug 22 2022 at 21:11):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Dear Mikhail,
the parametric_constant command was introduced in Isabelle2018 and is mentioned in the corresponding section of NEWS. The command has a truly minimalistic interface, therefore we didn't consider it necessary to add it to isar-ref (the NEWS entry refers to an example file). Maybe there should be an isar-ref description nonetheless.
We had considered to provide the user a way to specify side conditions on the involved relations, but decided against this in favor of a simpler user interface. The idea was that parametric_constant can be used in 90% of the cases where the synthesized conditions are the ones one wants to have anyway and in the remaining 10% the user can write the statement manually.
I don't see it as problematic, if you add a command that has a similar functionality, but has a different/extended user interface to the AFP. If there is an easy way of reducing one tool to the other (e.g., your command sets up the parametricity goal and then invokes the tactics from parametric_constants to discharge it), that would definitely be nice, but requires additional work.
I am also not against adding this functionality directly to parametric constants, but then we should have some (off-this-list) discussions about in what form the side constraints are specified.
Dmitriy
Last updated: Nov 21 2024 at 12:39 UTC