Re: [isabelle] Why no HOL set type in 2008?



One of those times when I regret my wasted education as a Z weenie,  
but my amateur viewpoint really sees this as concerning. Some points  
of debate follow.

On 12/12/2008, at 7:26 PM, Tobias Nipkow wrote:

> There were two main motivations:
>
> 1. Avoiding pointless coercions between the two worlds. In  
> particular, given a predicate P you had to write {x. P(x)} to turn  
> it into a set. Now you have to worry less as to whether 'a set or 'a  
> => bool is more appropriate.

Isn't this an argument for using ZF over HOL? Surely there are  
benefits to strong typing? Probably the people who actually worry  
about this question, want to worry about it. More likely, people who  
always chose 'a => bool, occasionally realise that {f x | x y. t x y}  
is a way more convenient (and disciplined) way of writing (% z. (! x  
y. z = f x & t x y)) and get annoyed they need a coercion to make use  
it. In any case, they won't use set notations very often, I guarantee  
that the predicate oriented user will not write { (x, y) | x y. t x y}  
instead of (% x y. t x y). A proper theory of predicates would be more  
to their liking, with a (generalised) predicate comprehension and  
predicate conjunction, disjunction, and negation operators. This would  
pretty much need little more than the introduction of a  
boolean_algebra class and the generalisation of the boolean operators  
to this class.

Biggest irony of all, the Collect coercion operator hasn't gone away  
as it is needed to support print translations. Only the strong typing  
on sets has gone! Why does this cause problems (other than the  
problems always caused by weak typing)?

In effect, this equates sets with meta-abstraction, as there is  
already effectively no object-level "function" type in HOL. Thus set  
instances suffer from the same "higher-order unification" problems  
that make arg_cong and fun_cong a pain to work with in Isar. It is now  
necessary to instantiate set reasoning rules far more often than  
previously.

Isar only allows a single reasoning set. With a distinguished set  
type, this could be worked around to a degree. Now there is no way to  
say, "just do set-style reasoning here." Auto fails to terminate in  
many more situations now.

I'll continue evaluating the situation, but the chances are that I'll  
be investigating the feasibility making a copy of Set.thy with

datatype 'a set = Collect "'a => bool"

replacing

types 'a set = "'a => bool".

Brendan



IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914.  If you have received this email in error, you are requested to contact the sender and delete the email.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.