A finite set that is a CompleteLattice

Stream: Is there code for X?

[Mai]

I wanna use docs#OrderHom.lfp to get the least fixpoint of a function Finset a -> Finset a, but it doesn't implement docs#CompleteLattice. Set does implement it, it seems, but I need a finite result

[Aaron Liu]

Finset isn't a complete lattice on an infinite type

[Mai]

I am not sure why?

[Snir Broshi]

Because there are infinite chains, e.g. {1}, {1,2}, {1,2,3}, ... and the supremum isn't a finset

[Aaron Liu]

the supremum of all singletons isn't finite anymore

[Riccardo Brasca]

@Mai do you understand that Finset a is not a finite set, but the (usually infinite) collection of finite sets whose elements are of type a?

[Snir Broshi]

Aaron Liu said:

Finset isn't a complete lattice on an infinite type

But shouldn't it be a docs#ConditionallyCompleteLattice on any type?
(might not help the fixpoint problem, but maybe)

[Snir Broshi]

Also it seems that docs#OrderHom.lfp only needs the fact that infimum is monotone (s ⊆ t → sInf s ≤ sInf t), which I think is true for finsets.

[Mai]

Riccardo Brasca said:

Mai do you understand that Finset a is not a finite set, but the (usually infinite) collection of finite sets whose elements are of type a?

Yes, I am aware. My monotone function takes a set and adds elements to it

[Aaron Liu]

how do you know its least fixpoint is finite

[Mai]

There's a finite set of elements the function may add to the set, regardless of the argument

[Aaron Liu]

Then if S is the finset of elements your function f can add then f^[S.card] ∅ should be the least fixpoint of f

[Mai]

I guess so :grimacing: feels a little hacky though