Email Gateway (Aug 19 2022 at 17:33): Email Gateway (Aug 19 2022 at 17:33):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi all,
In private discussion with Tobias, René T., and Chris S., we agreed that the current syntax for (multiplicity-aware) multiset inclusion and the multiset (Dershowitz-Manna) ordering is confusing.
Focusing on the strict operators, the current situation is
< and ⊂ for multiset inclusion
<# and ⊂# for the multiset ordering
Our proposal:
< for the multiset ordering
<# and ⊂# for subset with multiplicities
(and analogously for the nonstrict operators). Apart from being less confusing (in our opinion), the new syntax would ensure the nice multiset ordering is used by the “ord” type class, which would be useful to some of us. Indeed if < is a linear order on 'a, with this change so would < be on multisets, or on multisets of multisets, etc.
Because the proposal is essentially a swapping (except for ⊂, which is no longer assigned), we would need to proceed in two steps.
First step (for Isabelle2015):
< and ⊂ for multiset inclusion
#<# and #⊂# for the multiset ordering
The symbols “#<#” and “#⊂#” are ugly, but they would vanish with the expected Isabelle2016 release, at which point our proposal would be fully implemented. [*]
Let us know if you have strong opinions on this, ideally as soon as possible, since we soon have to slow down development toward the next release.
Cheers,
Jasmin
[*] For isabelle-dev readers: In the Isabelle repository, the ugly symbols would appear in the coming days and vanish soon after the Isabelle2015 release.
Email Gateway (Aug 22 2022 at 09:10):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jasmin,
I am not sure whether it would be best to do the swap in one step.
In earlier days, we provided funny fix_foo tools (mostly perl scripts)
which would assist in performing such transitions, and the multiset
syntax IMHO looks feasible for this also.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 09:12):From: Johannes Hölzl <hoelzl@in.tum.de>
Hm, maybe nowadays a Scala or ML script can do the job? How do you
otherwise distinguish btw. < for orders and < for multiset?
Email Gateway (Aug 22 2022 at 09:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Johannes,
Hm, maybe nowadays a Scala or ML script can do the job? How do you
otherwise distinguish btw. < for orders and < for multiset?
thanks for the hint. Of course bare < etc. is not suitable for perl
magic. And this would surely be a candidate for a first
source-modifying tool using Isabelle/Scala.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 09:15):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Florian,
I am not sure whether it would be best to do the swap in one step.
Well, I am sure that I don’t want to do the swap in one step.
In earlier days, we provided funny fix_foo tools (mostly perl scripts)
which would assist in performing such transitions, and the multiset
syntax IMHO looks feasible for this also.
I don’t know how your fancy Perl scripts will deal with < and ⊂, based on the type.
Jasmin
Email Gateway (Aug 22 2022 at 09:17):From: Makarius <makarius@sketis.net>
Perl is indeed mostly out -- Isabelle/Scala has token over regex
operations quite successfully in recent years, together with convenient
I/O operations that follow Isabelle/ML customs.
The problem to operate on sources systematically, based on actual formal
content is rather old and well-known, but not yet done routinely. In
principle, the PIDE markup could be used to guide the text replacement --
some genuine "refactoring" of theories.
I am not proposing this concretely right now, but the technology is pretty
close to that.
Makarius
Email Gateway (Aug 22 2022 at 09:21):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi all,
I am not sure whether it would be best to do the swap in one step.
Actually, Florian’s email made me rethink about this, and maybe as many as three steps will be necessary (leading us to Isabelle2016-1 or Isabelle2017):
My goal is to maximize the number of cases where changes trigger clear errors when processing theories, and minimize subtle change of semantics. Even in a theorem prover, semantic changes can be difficult to debug. Combining steps 2 and 3 would lead to some confusion — a term like “A < B” would suddenly change semantics, without giving an immediate error.
Anyway, we will see. For the moment, if there are no voices against my implementing step 1, I will go ahead (e.g. next week).
Thanks to all for your feedback!
Jasmin
Email Gateway (Aug 22 2022 at 09:22):From: Larry Paulson <lp15@cam.ac.uk>
It would be great to get some feedback from the mailing list as to who would be affected by this change.
Existing users of multiset orderings, please speak up!
If hardly anybody is going to be affected, then the change should be implemented in full for the next release.
Larry
Email Gateway (Aug 22 2022 at 09:25):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Good point. We’ve had some off-lists discussions with the IsaFoR developers, who use multisets and multiset orderings heavily. But since they are currently based on the repository version, we could do the three-step transition there, all in time for Isabelle2015. Mathias, Dmitriy, and I are in a similar situation. Anybody else?
Jasmin
Last updated: Apr 25 2024 at 20:15 UTC