Stream: Beginner Questions

Topic: minimal

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

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.

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

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...

Mathias Fleury (Jul 18 2022 at 14:46):

According to

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

Mathias Fleury (Jul 18 2022 at 14:46):

there is linorder.Min

Mathias Fleury (Jul 18 2022 at 14:47):

but I am not sure how easy it is to use

Manuel Eberl (Jul 18 2022 at 14:52):

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

Manuel Eberl (Jul 18 2022 at 14:53):

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

Manuel Eberl (Jul 18 2022 at 14:53):

Which may be too strong a requirement, alas…

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)

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: Apr 19 2024 at 20:15 UTC