Email Gateway (Apr 14 2023 at 18:50): Email Gateway (Apr 14 2023 at 18:50):From: Liam O'Connor <l.oconnor@ed.ac.uk>
Dear Isabelle-users,
For a project involving some denotational semantics we are working with HOLCF and its convenient powerdomains library.
We are working with a convex powerdomain over a flat domain (i.e. overall the output domain for our semantics is “state lift convex_pd" ), so it is conceptually straightforward to consider our domain as a (non-empty) set of states or a special divergence value.
Our question is: How does one convert from a convex_pd into such a set? We tried looking at the various representation functions for the typedefs for convex_pd and pd_basis etc, but were confused by the results we got. This feels like something that should already exist in the library somewhere, so I feel like I’m missing something.
Any help would be greatly appreciated,
With best wishes,
Liam
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
Email Gateway (Apr 14 2023 at 19:22):From: Liam O'Connor <l.oconnor@ed.ac.uk>
Dear Isabelle-users,
For a project involving some denotational semantics we are working with HOLCF and its convenient powerdomains library.
We are working with a convex powerdomain over a flat domain (i.e. overall the output domain for our semantics is “state lift convex_pd" ), so it is conceptually straightforward to consider our domain as a (non-empty) set of states or a special divergence value.
Our question is: How does one convert from a convex_pd into such a set? We tried looking at the various representation functions for the typedefs for convex_pd and pd_basis etc, but were confused by the results we got. This feels like something that should already exist in the library somewhere, so I feel like I’m missing something.
Any help would be greatly appreciated,
With best wishes,
Liam
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
Last updated: Apr 28 2024 at 16:17 UTC