[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Jasmin Christian Blanchette]

Hi all,

Let me describe the implications of reintroducing "'a set" for Sledgehammer's and Nitpick's performance.

Am 12.08.2011 um 11:27 schrieb Alexander Krauss:

> What are, actually, the losses when going back? This has not yet been touched by this thread at all (except the compatibility/import issue mentioned by Brian), and at least myself I wouldn't feel comfortable answering this question just now...

For Sledgehammer, reverting would be a (fairly) small loss. At the ATP level, types are erased (or encoded), and it doesn't really matter if something is a "'a set" or a "'a => bool". Higher-order functions and predicates are translated as simple values of the universe, and when they are applied this is done using an explicit operator called "hAPP". Apart from the order of the arguments, there is no difference between "hAPP" and "Set.member".

Hence, the main difference to the ATPs is whether we have "mem_def"/"Collect_def" to bridge the two worlds or the weaker "mem_Collect_def". "mem_def" and "Collect_def" seem more flexible in that respect, and it's no coincidence that several "metis" calls with one or the other were found when reintroducing "'a set". (On the other hand, one could argue that "mem_def"/"Collect_def" are more useful to prove things today in the current state of mismatch, cf. "Multivariate_Analysis", than they would have been a few years ago right after the elimination of "'a set".)

Sledgehammer and Metis also have a flag that preprocesses away all "member" and "Collect" before doing the proof search. For Sledgehammer, the success rate for a single prover went up by about .5% -- which is good but not fantastic. This option is still off by default because it needs a more thorough evaluation and it broke at least one Metis proof (for no deep reason, except what I'd call "a failure to perform").

For Nitpick, reintroducing sets wouldn't make any difference in terms of performance one way or the other, since "'a set" and "'a => bool" are isomorphic and hence as many bits are required to code one or the other. I would need to spend some time to make Nitpick (and Refute) work smoothly, though, and there are many more urgent things on my plate, so don't hold your breath.

My personal gut feeling is that if we are to have "Collect" and "member" at all, then it might be just as well that we keep them separated from the rest using type discipline, to catch various stylistic horrors. But beyond from this I'm not leaning one way or another.

Jasmin