Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "partial order" type?


view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: John Wickerson <jpw48@cam.ac.uk>
Hello,

I want to write a function that takes a partial-order as a parameter. Specifically, I want the following function...

fun interleave :: "'a list => 'a list => 'a partialorder => 'a list set"

... which takes two lists and a partialorder, and returns the set of all interleavings of the elements of those lists which respect the partial order.

I know that I could replace "'a partialorder" above with "('a \<times> 'a) set", and then prove a lemma saying "if that parameter is a partial-order then interleave has such-and-such a property". But it would be rather nice just to put the partial-order-ness of that parameter straight into its type. Can I do that, and if so how?

Thanks very much,
john

view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: Peter Gammie <peteg42@gmail.com>
John,

You can use a type class. See the lattice theories in the HOL distribution, i.e. HOL/Lattices.thy, or the partial order setup in HOLCF.

The problem (in general) with this approach is that it only allows each type to be partially ordered in one way. If this is an issue then I suggest you use a locale instead, or your original approach.

cheers
peter

view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: Steven Obua <steven.obua@googlemail.com>
you can also define a new type ala

typedef 'a partial_order = those "('a \<times> 'a) set" which correspond to partial orders

I don't have the exact syntax at hand right now, but that should point you in the right direction, and it will work. Not sure if it is worth the effort though, you might be better off using an explicit assumption.

Cheers,

Steven

view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: Brian Huffman <brianh@cs.pdx.edu>
On Sun, Nov 13, 2011 at 9:45 PM, John Wickerson <jpw48@cam.ac.uk> wrote:

Thanks very much Brian, that all makes sense to me. I was expecting you to tell me to tap into the type class "order" in some way (which is defined in http://isabelle.in.tum.de/dist/library/HOL/Orderings.html). Which is to say: do I really have to define my own "is_partialorder" predicate from scratch?

[I forgot to reply also to the list with my first response; now we're
back on the list again.]

Now to answer your follow-up question: If you want to avoid defining
an is_partialorder predicate from scratch, you can use the locale
predicates that come from the existing type classes. The only
complication here is that the locale predicate for class order takes
two arguments, one for "op <=" and one for "op <":

"class.order"
:: "('a => 'a => bool) => ('a => 'a => bool) => bool"

(Also note that the relations are modeled as binary predicates, rather
than as sets of pairs.)

So you could define your type in terms of pairs of relations, like this:

typedef 'a partialorder = "{(le :: 'a => 'a => bool, lt :: 'a => 'a =>
bool). class.order le lt}"

The definition of a partial order is still simple enough that I'm not
sure if using the class predicate like this is worth the trouble. For
other, more complicated type classes it would probably be worth it,
though.

If your main concern is getting copies of all the theorems that exist
in class "order", then you could achieve this with a locale
instantiation. Specifically, you could define parameterized versions
of "op <=" and "op <" with these types:

my_le :: 'a partialorder => 'a => 'a => bool
my_lt :: 'a partialorder => 'a => 'a => bool

And then do a locale instantiation like this:

instantiation my_partialorder: order "my_le r" "my_lt r"
<proof>

after which you would have copies of all the theorems from the order class.

On 13 Nov 2011, at 18:58, Brian Huffman wrote:

On Sun, Nov 13, 2011 at 7:26 PM, John Wickerson <jpw48@cam.ac.uk> wrote:

Hello,

I want to write a function that takes a partial-order as a parameter. Specifically, I want the following function...

fun interleave :: "'a list => 'a list => 'a partialorder => 'a list set"

... which takes two lists and a partialorder, and returns the set of all interleavings of the elements of those lists which respect the partial order.

I know that I could replace "'a partialorder" above with "('a \<times> 'a) set", and then prove a lemma saying "if that parameter is a partial-order then interleave has such-and-such a property". But it would be rather nice just to put the partial-order-ness of that parameter straight into its type. Can I do that, and if so how?

Hi John,

Yes, you certainly can do this. You just need to define the type 'a
partialorder with a typedef, something like this:

typedef 'a partialorder = "{r::('a * 'a) set. is_partialorder r}"

where "is_partialorder" should be defined ahead of time as a predicate
asserting that the given relation is a partial order. The typedef will
require a nonemptiness proof, but that should be easy since the
equality relation on any type is always a partial order.

For an example of this kind of definition, have a look at
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space, which defines
a type called 'a topology consisting of all the possible topologies on
type 'a.

Hope this helps,
- Brian

view this post on Zulip Email Gateway (Aug 18 2022 at 18:45):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,

I want to write a function that takes a partial-order as a parameter.
Specifically, I want the following function...

fun interleave :: "'a list => 'a list => 'a partialorder => 'a list set"

... which takes two lists and a partialorder, and returns the set of
all interleavings of the elements of those lists which respect the
partial order.

here a short overview of the design space which combines everything said
on that here (@all: please comment if you think I've missed something)
with Isabelle folklore:

a) use (existing) type classes

+ lightweight
+ code can be generated directly
- only one instantiation per type
- no explicit carrier

b) use locales abstracting over the algebraic structure (which is
typically represented as a record)

+ explicit carrier
+ more flexible due to parametrisation
- more involved in application
- no direct code generation

c) use abstract type definition which encapsulates the properties of the
structure

+ combines nicely with b) via interpretation
+ explicit carrier
+ code generation possible

Examples for a) can be found in the HOL standard theories, for b) in the
HOL-Algebra session.

For b) and c), the locale predicates for existing type classes can be
reused of course.

c) is quite a recent thought which I have not yet thought of thoroughly,
so I do not know about pitfalls etc. It seems worth exploring.

Hope this helps,
Florian
signature.asc


Last updated: Mar 29 2024 at 08:18 UTC