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

[Lukas Bulwahn]

On 08/19/2011 07:39 AM, Tobias Nipkow wrote:
> 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.
>
Andreas Lochbihler and I elaborate on this topic in our recent paper for 
the ITP, cf. 
http://pp.info.uni-karlsruhe.de/publication.php?id=lochbihler11itp (page 14)
We present some solutions for code generation when using underspecification.
Put simply, the message is: Do not use Hilbert's choice if you want to 
obtain an executable specification.

Of course, handling underspecification is an orthogonal issue to the 
subject of this thread.


Lukas

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