haskellari / lattices

Fine-grained lattice primitives for Haskell
BSD 3-Clause "New" or "Revised" License
35 stars 15 forks source link

Antinone functions? #63

Open kindaro opened 6 years ago

kindaro commented 6 years ago

As I understand, you are implying that for us to find a greatest fixed point of a function, it must be antinone. Not that I contend the point; it's just that, unfortunately, I don't know what "antinone" is. A quick search doesn't help either. (In fact, this very haddock is the top link.) I looked through the index of Introduction to Lattices and Order, which is considered a standard intro to lattices and it does not seem to mention "antinone" at all. (While "monotone" is, of course, there.) So, I still don't know what it means and whether I could use gfpFrom with any of my functions.

I suggest adding some elaboration on the meaning of "antinone" to the relevant parts of the haddock.

kindaro commented 5 years ago

Maybe what is meant is antitone, with t ?

A monotone function is also called isotone, or order-preserving. The dual notion is often called > antitone, anti-monotone, or order-reversing. Hence, an antitone function f satisfies the property

x ≤ y implies f(x) ≥ f(y),

for all x and y in its domain.

emilypi commented 1 year ago

Should be antitone, but the author wrote the wrong thing basically everywhere.