Email Gateway (Aug 19 2022 at 17:20): Email Gateway (Aug 19 2022 at 17:20):From: Tjark Weber <tjark.weber@it.uu.se>
Dear BNF experts,
HOL/Library/Countable_Set_Type.thy registers 'a cset, the type of
countable sets with elements from 'a, as a BNF.
I was trying to generalize this to the type of sets whose cardinality is
bounded by some index type 'i. This type may be defined, e.g., as
follows:
typedef ('i,'a) iset = "{A :: 'a set. ∃f::'i⇒'a. A ⊆ range f}"
by auto
Of course, 'a should be live, while 'i is dead. However, with the
obvious definitions for map, sets, bd, wits, and rel,
bnf "('i,'a) iset"
results in a proof obligation for the relator that I can only prove if
the cardinality of 'i × 'i is no greater than the cardinality of 'i.
Obviously, this only holds when 'i is infinite.
Could you maybe give some intuition for why this condition is
necessary, and more generally for what the properties are that the
relator needs to satisfy? The documentation, as far as I can see, is
relatively silent on this.
Best,
Tjark
Email Gateway (Aug 19 2022 at 17:21):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Tjark,
coincidentally, we (Johannes Hölzl, Andreas Lochbihler, and I) needed to
perform the same generalization for a formalization of the probabilistic
hierarchy [1]. The resulting BNF instance is attached (where we use the
library of cardinals instead of working with surjections). Indeed, we
also notice that the bounded set type is a BNF only for infinite bound
types (or as an exception for at-most-two-element sets, which is not
covered in the attached theory, but I can send you another one if you like).
The relator condition is equivalent to the condition on functor (F,
Fmap) to preserve weak pullback (not sure if this helps). A rough
intuition is that BNFs must be closed under zip, where the zip is some
function that takes two elements x y related by the relator "rel \<top>
x y" and returns you the element whose existence is guaranteed by the
relator (see e.g. the list.in_rel property)
rel R x y <-> ?z. set z <= {(x,y). R x y} & map fst z = x & map snd z = y
For plain lists one obtains the usual zip in that way; for sets the zip
is the Cartesian product. Hence for bounded sets |A \times A| =o |A| is
required. For some reason this intuition fails for sets of at most
cardinality 2---I still need to understand why.
Anyway, I'm curious to hear about your application of bounded sets.
Hope this helps,
Dmitriy
[1] Bartels, Sokolova, de Vink, A hierarchy of probabilistic system
types, TCS, 2004, http://dx.doi.org/10.1016/j.tcs.2004.07.019
Bounded_Set.thy
Email Gateway (Aug 19 2022 at 17:21):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Tjark,
more generally for what the properties are that the relator needs to satisfy?
Let me just add to Dmitriy's excellent answer a simple intuition that might also help: A (unary) BNF is essentially a functor (F,Fmap) on the category of sets and functions, equipped with a natural transformation Fset that returns the "atoms" of the "compound" elements in the image of F. Given these data, namely, (F,Fmap,Fset), there is a natural way to extend it to a functor (F,Frel) on the category of sets and relations -- this is according to the formula shown by Dmitriy:
Frel R x y <-> ? z. Fset z <= {(x,y). R x y} & Fmap fst z = x & Fmap snd z = y
If you draw a diagram, you will see that this is the "obvious" way to extend Fmap to Frel (in the presence of Fset).
Now, we simply require that (F,Frel) be also a functor.
All the best,
Andrei
Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.
If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS. There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.
Email Gateway (Aug 19 2022 at 17:21):From: Tjark Weber <tjark.weber@it.uu.se>
Dmitriy, Andrei,
Thank you for your answers. Perhaps the theory that you kindly attached
could be added to the Isabelle/HOL library at some point.
On Sat, 2015-03-14 at 08:41 +0100, Dmitriy Traytel wrote:
rel R x y <-> ?z. set z <= {(x,y). R x y} & map fst z = x & map snd z = y
For plain lists one obtains the usual zip in that way; for sets the zip
is the Cartesian product. Hence for bounded sets |A \times A| =o |A| is
required. For some reason this intuition fails for sets of at most
cardinality 2---I still need to understand why.
Note that for sets of cardinality at most 2, the relator condition
requires R to contain a bijection.
Anyway, I'm curious to hear about your application of bounded sets.
I am trying to model an infinitary logic, where one may form the
conjunction of a set of formulas to obtain a new formula.
Best,
Tjark
Email Gateway (Aug 19 2022 at 17:21):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Tjark,
On 14.03.2015 13:33, Tjark Weber wrote:
Dmitriy, Andrei,
Thank you for your answers. Perhaps the theory that you kindly attached
could be added to the Isabelle/HOL library at some point.
I'll add it next week.
On Sat, 2015-03-14 at 08:41 +0100, Dmitriy Traytel wrote:
rel R x y <-> ?z. set z <= {(x,y). R x y} & map fst z = x & map snd z = y
For plain lists one obtains the usual zip in that way; for sets the zip
is the Cartesian product. Hence for bounded sets |A \times A| =o |A| is
required. For some reason this intuition fails for sets of at most
cardinality 2---I still need to understand why.
Note that for sets of cardinality at most 2, the relator condition
requires R to contain a bijection.
Right, thanks.
Anyway, I'm curious to hear about your application of bounded sets.
I am trying to model an infinitary logic, where one may form the
conjunction of a set of formulas to obtain a new formula.
Ah, interesting.
Dmitriy
Email Gateway (Aug 19 2022 at 17:25):From: Dmitriy Traytel <traytel@in.tum.de>
See now Isabelle/7325ffa35038 .
I could not put the theory in Library, since it depends on the
cardinals. That's why it is now part of the HOL-Cardinals session.
Dmitriy
Last updated: Apr 26 2024 at 16:20 UTC