Skip to content

Instantly share code, notes, and snippets.

@inamiy

inamiy/cata-ana-prefixed-postfixed-points.hs

Created August 3, 2020 02:45
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save inamiy/ee5eba3b612536a08078850ec35ef1fc to your computer and use it in GitHub Desktop.
Save inamiy/ee5eba3b612536a08078850ec35ef1fc to your computer and use it in GitHub Desktop.
Download ZIP
Raw
cata-ana-prefixed-postfixed-points.hs
-- For all `x` that is prefixed point of `f` (f x :< x),
-- it is upper bound of `f^n ⊥` (where n = 0, 1, 2, ...)
-- so that its least upper bound `Mu f` is always less than or equal to `x`.
cata :: (f x :< x) -> Mu f :< x
-- For all `x` that is postfixed point of `f` (x :< f x),
-- it is lower bound of `f^n ⊤` (where n = 0, 1, 2, ...)
-- so that its greatest lower bound `Nu f` is always greater than or equal to `x`.
ana : (x :< f x) -> x :< Nu f
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment