Divergence characterises whether something surely diverges.
Models a subset lattice of the following exhaustive set of divergence
results:
- n nontermination (e.g. loops)
- i throws imprecise exception
- p throws precise exception
- c converges (reduces to WHNF).
The different lattice elements correspond to different subsets,
indicated by juxtaposition of indicators (e.g.
nc definitely
doesn't throw an exception, and may or may not reduce to WHNF).
Dunno (nipc)
|
ExnOrDiv (nip)
|
Diverges (ni)
As you can see, we don't distinguish
n and
i. See Note
[Precise exceptions and strictness analysis] for why
p is so
special compared to
i.