[eru]

A slight tangent: there's also a related notion to termination, that allows you to describe event loops.

Basically it's about the loop making progress on every iteration, but we can have an infinite number of iterations.

I think the distinction is related to the one between data and co-data.