Email Gateway (Aug 19 2022 at 09:19): Email Gateway (Aug 19 2022 at 09:19):From: Simon Foster <simon.foster@york.ac.uk>
Hi,
I'm trying to devise a HOLCF cpo for finite sets, which I intend to use as
part of a larger domain type via indirect recursion. One way of doing this
would seem to be by creating a cpo of totally ordered slists, e.g.
cpodef (open) 'a fset = "{l. ordslist l}"
And then build all the standard set stuff on top of this. Ordlist is an
inductive predicate requiring a strict ordering on the elements. The main
advantage of this definition is that it is flat, and therefore easier to
use. The big problem with this definition is that it can't easily be used
recursively as it depends on the fset's parameter being in linorder, which
of course it isn't when creating the domain.
I'm wondering though if I'm missing a trick and if there's a simpler way of
doing it than this? Obviously sets in HOL can be be made finite either
through the finite predicate or by using the FSet quotient type, but I
don't see an obvious way that either of them can be carried over into a
domain, particularly whilst retaining flatness.
I also saw that instances of countable are made an instance of domain under
lift. Since finite sets of countables are again countable, could I make use
of this somehow? Although again this may be difficult because of indirect
recursion.
Alternatively has this already been done, and I just haven't searched
adequately?
Many thanks,
Email Gateway (Aug 19 2022 at 09:19):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
just checking: What will your order relation be? Because if it is just
going to be subset, then you will not be able to construct a cpo, as the
limit of a chain of finite sets can be infinite (unless the type of the
elements is finite, of course).
I have a theory of finite maps with the HOLCF setup done
(http://darcs.nomeata.de/isa-launchbury/FMap-HOLCF.thy), but depending
on the order relation that you need, this is not going to help you.
Greetings,
Joachim
signature.asc
Last updated: Apr 20 2024 at 04:19 UTC