Stream: Beginner Questions

Topic: minimal


view this post on Zulip zibo yang (Jun 02 2021 at 13:17):

Is there any function like min::"int set => int" to get the minimal element in one int set

view this post on Zulip Manuel Eberl (Jun 02 2021 at 13:19):

It's called Min, but it only works for finite sets. There's also Inf, the infimum, which also works on infinite sets as long as they are bounded from below.

view this post on Zulip zibo yang (Jun 02 2021 at 14:02):

Manuel Eberl said:

It's called Min, but it only works for finite sets. There's also Inf, the infimum, which also works on infinite sets as long as they are bounded from below.

thanks. that is what I want

view this post on Zulip Taro Yoshioka (Jul 18 2022 at 14:38):

Hello, does there also exist a function of type "('a => 'a => bool) => 'a set => 'a"? I need both the order ('a => 'a => bool) and the (finite) set ('a set) to be variable...

view this post on Zulip Mathias Fleury (Jul 18 2022 at 14:46):

According to

find_theorems "_ :: ('a => 'a => bool) => 'a set => 'a"

view this post on Zulip Mathias Fleury (Jul 18 2022 at 14:46):

there is linorder.Min

view this post on Zulip Mathias Fleury (Jul 18 2022 at 14:47):

but I am not sure how easy it is to use

view this post on Zulip Manuel Eberl (Jul 18 2022 at 14:52):

If there is a unique minimum, you can indeed use that, yes.

view this post on Zulip Manuel Eberl (Jul 18 2022 at 14:53):

And if your relation is indeed a linear ordering on the entire type.

view this post on Zulip Manuel Eberl (Jul 18 2022 at 14:53):

Which may be too strong a requirement, alas…

view this post on Zulip Manuel Eberl (Jul 18 2022 at 14:55):

Otherwise you can use something I made: Link to AFP entry

definition Max_wrt_among :: "'a relation ⇒ 'a set ⇒ 'a set" where
  "Max_wrt_among R A = {x∈A. R x x ∧ (∀y∈A. R x y ⟶ R y x)}"

Here, 'a relation is just a type synonym for 'a ⇒ 'a ⇒ bool.

It should be easy to adapt this to minimum (e.g. by applying it to the dual relation).

Note that this returns a set, not a single element. You'd then have to define a version for linear orderings that just returns a single element (Max_wrt_among or Min_wrt_among will then always be singleton sets, so you can use e.g. the_elem to get that element)

view this post on Zulip Taro Yoshioka (Jul 18 2022 at 15:11):

wow thanks I will try out! (yes in general it's only an order on the provided set)


Last updated: Sep 25 2022 at 22:23 UTC