Clever scheduling needed in absence of ACC?

[nomeata]

I’m worrying if rec-def may be unpure in the presence of infinite chains, i.e. when the Ascending Chain Condition does not hold.

Consider the type Maybe Natural, ordered by Just 0 ⊑ Just 1 ⊑ … ⊑ Nothing. The following operations are monotone and continuous:

max :: Maybe Natural -> Maybe Natural -> Maybe Natural
max Nothing _ = Nothing
max _ Nothing = Nothing
max (Just n1) (Just n2) = Just (max n1 n2)

succ :: Maybe Natural -> Maybe Natural
succ Nothing = Nothing
succ (Just n) = Just (succ n)

Now consider these these recursive equations:

n, m :: Maybe Natural
n = max (succ n) m
m = Nothing

a naive fix-pointing algorithm might initialize n and m to the bottom element Just 0, then keep updating n with max (succ n) m forever, without ever setting m to Nothing.

Or it might set m to Nothing eventually, which turns n to Nothing, and finds the fixed point.

So if the “Ascending Chain Condition” does not hold for all involved types, it seems that purity is non-trivial.

Would some form of “fair scheduling” fix this, and is that easily implementable?