What is the concept of Chain Complete?

Question

I'm reading the book called 'Thinking Functionally with Haskell' by Richard Bird, and encountered the notion of Chain Complete regarding induction over infinite lists. It says:

A property P is called chain complete if whenever xs0, xs1,... is a sequence of partial lists with limit xs, and P(xsn) holds for all n, then P(xs) also holds.

As an example of chain complete property, it says:

All equations e1 = e2, where e1 and e2 are Haskell expressions involving universally quantified free variables, are chain complete.

I'm having trouble to understand how this example fits the property of chain complete here. And it also states inequalities e1 =/= e2 are not necessarily chain complete. How do I understand these properties in terms of this Chain Complete-ness ?

By the way this may not necessarily be a question regarding Haskell, but a question in terms of mathematics.

Answer 1

Here's an example.

Suppose that you have an increasing sequence of lists xs_1, xs_2, ... with limit xs.

For every k, we have that map id xs_k is equal to xs_k.

By chain completeness (AKA Scott continuity) we get that map id xs is xs.

This gives us a way to prove properties on limit lists xs, which may be infinite, by verifying them only on their approximations xs_k.

The intuition here is that, for xs to be a limit list, each xs_k must be equal to xs or some shorter prefix of the form x1:x2:...:xn:undefined. Note the undefined tail, representing a looping computation (e.g. infinite recursion). Because of this, if we compare f xs_k and f xs, we find that the latter must be at least as terminating as the former. The general idea here is that if we pass a more or as defined input we get a more or as defined output. Mathematically, this notion is captured by monotonicity on the Scott ordering.

Scott omega-continuity, or chain completeness, goes further. It tells us the f xs is exactly the same a the limit of the sequence f xs_k. The final result is approximated by the results of f on the approximations. In rough words, you can make the output converge by making the input converge.

Inequality does not work in a chain complete fashion. Indeed, take xs = [0..] as an infinite list, and approximations xs_k = 0:...:k:undefined. It is clear that xs_k is not equal to xs, for each k. But we do not take the limit of that inequality, which would state that xs is not equal to xs.

Concluding, the topic here is quite broad. If you are interested, I'd suggest you read about denotational semantics, for instance reading the Winskel's book.