Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: nipkow@in.tum.de
Burkhart Wolff wrote:
recently, I came across an alternative way to define
a fold on finite sets. In contrast to the Isabelle
library version (discussed in the recent TPHOLs Paper),
it has a slightly more general type:fold : [['a, 'b] => 'b, 'b, 'a set] => 'b
The library version has type (b => b => b) => (a => b) => b => a set => b
which is not more specific but simply different. The one you suggest is the
one used in HOL4 which we briefly mention towards the end of section 2.2
where we also give a reference [2] that shows that both combinators are
interdefinable. Ours is based on the singleton-union (SU) view of set
generation, the one in HOL4 on the insert (I) view.
It is strictly more general:
see above.
you can define the cardinality of finite sets by this fold, but not
by the old one, for example.
At the end of section 3.5 we show how to define card in terms of our fold.
The one point that does make the I-fold more attractive than the SU-fold is
complexity: it is obvious how to define the latter in terms of the former,
but tricky the other way around. In fact, the tricky direction leads to a
situation where you call the SU-fold with a function which is not commutative
in general but only on the arguments arising in that computation. Hence our
library (ie the thms) would need to be generalized a little to accommodate
this situation. Just like the requirement of left-commutativity for the
argument of the I-fold is too strong in general.
The same algorithmic scheme would work for multi-sets too,
The duality between SU and I works for sets/multisets/lists.
See [2] for the details.
B) Wouldn't it be a better candidate
for the Isabelle/HOL library?
If there were multiple instances where the SU-fold is more cumbersome to use
than the I-fold, I might agree. But I am only aware of one instance,
transitive closure, and that is defined very differently anyway.
Tobias
[2] @inproceedings{TannenS-ICALP91,
author={Val Breazu-Tannen and Ramesh Subrahmanyam},
title = {Logical and computational aspects of programming with sets/bags/lists},
booktitle = {Automata, Languages and Programming (ICALP91)},
editor={J. Leach Albert and B. Monien and M. Rodr\'{\i}guez-Artalejo},
year = {1991},
pages = {60-75},
publisher = {Springer},series={LNCS},volume=510
}
Last updated: May 03 2024 at 08:18 UTC