Email Gateway (Aug 18 2022 at 12:45): Email Gateway (Aug 18 2022 at 12:45):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
Can anyone speak to reasoning behind the decision to remove the set
type from HOL in Isabelle 2008?
I find it strangely disconcerting not to have a syntactic distinction
between sets and predicates. Obviously it has some technical
inconveniences, but perhaps they are outweighed by some advantages?
Dr Brendan Mahony
C3I Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
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.
Email Gateway (Aug 18 2022 at 12:45):From: Tobias Nipkow <nipkow@in.tum.de>
Brendan,
There were two main motivations:
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.
Compatibility with other HOLs.
Tobias
Dr. Brendan Patrick Mahony wrote:
Email Gateway (Aug 18 2022 at 12:46):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
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.
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.
Email Gateway (Aug 18 2022 at 12:46):From: Tobias Nipkow <nipkow@in.tum.de>
Brendan, you are certainly right that in some situations proofs are less
automatic. We were aware of this but found that in the theories we have
access to it was not too bad, only a few times per theory on average.
However we concede that depending on your application this could be
worse. I'm very sorry if you were particularly affected.
Concerning boolean algebras (and lattices), we do intend to develop this
connection further.
Regards
Tobias
Dr. Brendan Patrick Mahony schrieb:
Email Gateway (Aug 18 2022 at 12:49):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
The latest problem encountered in in developing instances of
axclasses. No set type means no set instance claims for axclasses.
Obviously function type instance proofs are very different.
Brendan
Dr Brendan Mahony
C3I Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
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.
Email Gateway (Aug 18 2022 at 12:50):From: Stefan Berghofer <berghofe@in.tum.de>
Dr. Brendan Patrick Mahony wrote:
Hi Brendan,
when porting the theories in the Isabelle distribution to the new encoding
of sets as predicates, we found that most of the instance proofs for sets
could be replaced by appropriate instance proofs for functions and booleans
in a rather straightforward way. Could you give an example of an instance proof
for sets that you could not easily replace by instance proofs for functions and
booleans?
Greetings,
Stefan
Last updated: Nov 21 2024 at 12:39 UTC