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

[Tobias Nipkow]

Am 19/08/2011 00:00, schrieb Stefan Berghofer:
> Alexander Krauss wrote:
>> I want to emphasize that the limitation of the code generator mentioned
>> here not only applies to sets-as-predicates but also to
>> maps-as-functions and other abstract types that are often specified in
>> terms of functions (finite maps, almost constant maps, etc.). Thus,
>> having good old 'a set back is does not fully solve this problem as a
>> whole, just one (important) instance of it.
>>
>> My view on this whole topic is outlined in the report I recently sent
>> around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated
>> since last time). In the long run, I would prefer to see flexible
>> transport machinery to move stuff between isomorphic types.
> 
> Hi Alex,
> 
> thanks for your excellent report, I fully agree with this view. There is
> often a tradeoff between executability and conciseness / abstractness of
> specifications, so I don't think it is a good idea to tweak the logic in
> such a way that it is more suitable for code generation.

Having a separate type set is more not less abstract. Just like LISP is
not more abstract than ML. It allows us to regain a few important things
we lost. Sets as predicates are indeed more concise (you don't need {x.
P x} and %x. x : S), but this is just a matter of degree, not a complete
loss of some feature.

If we could freely mix sets and predicates as we had hoped, it would be
different. But proof support is lacking. Not just in Isabelle/HOL, but
Michael Norrish tells me that in HOL4 it is also better not to mix sets
and predicates if you want proof automation.

> For example,
> HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element
> from the worklist, which is highly non-executable but more abstract, since
> one does not have to commit to a particular strategy for selecting the element.

This is a misunderstanding. The SOME operator *does* commit to a
particular strategy, but we do not know which one. Which means that we
can never prove it equivalent to any strategy. SOME is both abstract and
concrete in a way that defeats implementation.

Tobias

> Greetings,
> Stefan
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev