What is the concept of "chain complete"?

Question

I am reading Richard Bird's book entitled "Thinking Functionally with Haskell," and came across the concept of "Chain Complete" regarding induction over endless lists. It says:

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

As an example of a chain property, he says:

All equations e1 = e2, where e1 and e2 are Haskell expressions containing universally quantized free variables, are complete.

It’s hard for me to understand how this example fits the chain property. And it also indicates the inequalities e1 = / = e2, not necessarily integers. How can I understand these properties in terms of this chain?

By the way, this is not necessarily a question about Haskell, but a question in mathematics.

Answer 1

Here is an example.

Suppose you have an increasing sequence of lists xs_1, xs_2, ... with the restriction xs .

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

From the chain (AKA Scott continuity) we get that map id xs is xs .

This gives us a way to prove the properties in the limit lists xs , which can be infinite, checking them only on their approximations xs_k .

The intuition here is that for xs as a limit list, each xs_k must be equal to xs or a shorter prefix of the form x1:x2:...:xn:undefined . Notice the undefined tail, which represents a calculation loop (like infinite recursion). Because of this, if we compare f xs_k and f xs , we find that the latter should be at least as final as the first. The general idea here is that if we pass more or as a specific input, we will get more or as a specific result. Mathematically, this concept is captured by monotony in Scott's ordering.

Scott's omega-continuity, or whole completeness, goes further. This suggests that f xs exactly matches the limit of the sequence f xs_k . The final result is approximated by the results of f on approximations. Roughly speaking, you can infer convergence by making the entry convergent.

Inequality does not work in the whole chain. Indeed, take xs = [0..] as an infinite list and approximations xs_k = 0:...:k:undefined . Clearly, xs_k not equal to xs , for each k . But we do not take the limit of this inequality, which would argue that xs not equal to xs .

In conclusion, the topic here is quite broad. If this interests you, I would advise you to read about denotational semantics, for example, by reading the Winskel book.