[isabelle] Multiset ordering vs. subset syntax

[Jasmin Blanchette]

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.

[Florian Haftmann]

Hi Jasmin,

< 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. [*]

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

[Johannes Hölzl]

Post by Florian Haftmann
Hi Jasmin,

Post by Jasmin Blanchette
< 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. [*]

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.

Hm, maybe nowadays a Scala or ML script can do the job? How do you
otherwise distinguish btw. < for orders and < for multiset?


- Johannes

[Florian Haftmann]

Hi Johannes,

Post by Johannes Hölzl
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

[Jasmin Blanchette]

Hi Florian,

Post by Florian Haftmann
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.

Post by Florian Haftmann
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

[Makarius]

Post by Florian Haftmann
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.

Post by Florian Haftmann
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.

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

[Jasmin Blanchette]

Hi all,

Post by Florian Haftmann
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):

1. Rename <# etc. to #<# (or whatever odd syntax).
2. Rename < and \<subset> to <# and \<subset>#.
3. Rename #<# to <.

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

[Larry Paulson]

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

Post by Jasmin Blanchette
Hi all,

Post by Florian Haftmann
I am not sure whether it would be best to do the swap in one step.

1. Rename <# etc. to #<# (or whatever odd syntax).
2. Rename < and \<subset> to <# and \<subset>#.
3. Rename #<# to <.
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

[Jasmin Blanchette]

Post by Larry Paulson
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.

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