Parks convergence criterea

Question

I guess most people who had a look into Parks paper from 1970 asked themself how Park defines least fixpoint.

At this point one does notice that he does not use the term fixpoint, rather he talks about convergence. When looking up the definition of convergence on wikipedia however, this will lead to filterconvergence (german link: https://de.wikipedia.org/wiki/Filterkonvergenz) and the term Berührpunkte.

The question is:

Conv(c) = <Conv_0(c),Conv_0(c),\dots Conv_{N-1}(c)>

Conv_i(c) = \bigcap{A_i|c(<A>) \subseteq <A> for some {A_k|k\not = i}}

Are Conv_i as defined by Park therefore Berührpunkte?

This leads to some confusion regarding pre-fixpoints, since Park uses a union of conv_i as criterion for convergence, while we learned that the least fixpoints is the intersection (not the union) of all pre-fixpoints and therefore conv_i can not be the pre-fixpoint but something else. Thus convergenve should be identical to either least fixpoints or greatest fixpoints? Are there some indices missing in the definition of Conv and Conv_i?

Answer 1

Well, convergence of a function and fixpoint computation are closely related. Both have their roots in topological space where continuous functions are defined in terms of neighbourhoods (see https://en.wikipedia.org/wiki/Topological_space).

A function f:X→Y between topological spaces is called continuous if for every x∈X and every neighbourhood N of f(x) there is a neighbourhood M of x such that f(M) ⊆ N. This means that when mapping an element x, then there is for every neighbourhood N of f(x) a neighbourhood M of x such that f(M) is inside of N. Convergence is defined here by means of filter which instantiates in special cases as described below.

Special topological spaces are metric spaces which are sets that are endowed with a metric, i.e., a function that maps two elements to a nonnegative real number that is called their distance. The metric has to satisfy some laws like the triangle inequality (see https://en.wikipedia.org/wiki/Metric_space). For metric spaces, continuous functions are characterized by the ε-δ definition that is usually used in analysis textbooks to define continuous functions. Based on that, one usually defines the convergence of a function.

Other special topological spaces are complete partial orders which can be seen by the Scott topology that can be defined for any complete partial order (see https://en.wikipedia.org/wiki/Scott_continuity). Continuous functions are characterized here by the equation sup(f(M)) = f(sup(M)) that has to hold for all directed subset M.

When briefly looking at Park's paper, I think he is using complete partial orders, since his definitions assume a set algebra with intersection and union as infimum and supremum operations. For any monotonic function f, he defines Conv(f) := ∩{ x | f(x)⊆x}, i.e. Conv(f) is the infimum of all post-fixpoints. It is easy to prove (which is the statement of the Tarski-Knaster theorem) that Conv(f) is indeed a fixpoint, and that it is even the least fixpoint. While monotonicity is sufficient for the existence of fixpoints, and even of least fixpoints, it is not that simple to compute them for monotonic functions. For the special case of continuous functions, this is however simple and can be done by the well-known fixpoint iteration sequence: x[0] := {}; x[i+1] := f(x[i]), and now we need "convergence" to prove that the least fixpoint is the limit of the sequence x[i]. Note that the sequence x[i] is monotonically growing and that its supremum is the least fixpoint of f. We can therefore also define y[i] = x[0]∪...∪x[i] = x[i] to see that µx.f(x) = ∪ x[i=0..∞].

In general, we have 

Comments

If I get this right, i can conclude that the least fixpoint is the infimum of the set of pre-fixpoints, as well as post-fixpoints? I thought only the intersection of pre-fixpoints would yield the least fixpoint, while union of post-fixpoints yields the greatest fixpoint.

---

No that is not the case, see my updated answer. The least fixpoint is contained in any pre-fixpoint, and it is the infimum of all pre-fixpoints. The greatest fixpoint contains all post-fixpoints, and it is the supremum of all post-fixpoints. See, e.g., https://es.cs.uni-kl.de/publications/datarsg/KoSc19.pdf for a proof of these facts.