Email Gateway (Apr 09 2021 at 11:23): Email Gateway (Apr 09 2021 at 11:23):From: Lawrence Paulson <lp15@cam.ac.uk>
Having done quite a few proofs involving locales recently, I’ve noticed an issue with locale interpretation that is logically superficial but can make a big difference in proofs. It is that the argument lists of locales can grow drastically, and if users try to control this growth by “bundling up” adjacent, related arguments, they will be punished when the time comes to instantiate the locale. Example (thanks to Chelsea Edmonds):
interpretation add_point_in_sys: incidence_system "points (add_point p)" "blocks (add_point p)”
sorry
interpretation del_point_sys: incidence_system "points (delete_point p)" "blocks (delete_point p)”
sorry
Here we want the locale “incidence_system” to have virtually one argument, the pair of “points” and “blocks”, but the interpretation command requires the full argument list to be written out. It would be nice to be able to do something like this:
abbreviation “incidence_system’ X == incidence_system (points X) (blocks X)”
interpretation add_point_in_sys: "incidence_system’ (add_point p)”
interpretation del_point_in_sys: "incidence_system’ (del_point p)”
Any thoughts on this?
Larry
Email Gateway (Apr 11 2021 at 09:53):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Larry,
There is indeed functionality missing in locales: there are no means of
declaring and reusing morphisms in interpretations, so each parameter
needs to be dealt with manually in every interpretation. This creates
the desire of "bundling up" parameters, which I believe is not a good
thing as it reduces flexibility. As you say, this is not a logical but a
significant practical limitation.
I haven't understood what the parameters of the "unbundled" locale
"incidence_system" would have looked like. For unbundling them you would
have to have fixed sets of point and block parameters.
This approach would require an abbreviation per locale, so it's probably
not as effective as dealing with morphisms directly.
Clemens
Email Gateway (Apr 11 2021 at 17:01):From: Lawrence Paulson <lp15@cam.ac.uk>
Hi Clemens, perhaps you’ve seen this recent AFP entry:
https://www.isa-afp.org/entries/Grothendieck_Schemes.html
It was inspired by your own work and builds upon it. In fact, we have other (very different) work in the pipeline also following your locale-based approach, which seems to be extremely general.
The suggestion in my email was intended as a minimal, lightweight solution to the issue. A more principled solution would be great provided it doesn’t introduce implementation or foundational issues.
Best.
Larry
Last updated: Apr 23 2024 at 12:29 UTC