[Question][General]Different definitions of CPO (or domain)

[yusungsim]

Hi. Not a serious question but I just want to clarify my previous understanding on domain theory.

In [Theories of Programming Languages] by John C. Reynolds, chain is is defined as follows

A chain is a countably infinite increasing sequence, x_0 < x_1 < x_2 < ... The least upper bound of a chain is called its limit. A chain is said to be interesting if it does not contain its own limit or, equivalently, if it contains an infinite number of distinct elements.

Under this definition, a concept of 'completeness of chain' corresponds to predomain. But predomain does not always have a least element, or bottom. A predomain with the bottom element is called domain. And least fixpoint theorem applies to this domain.

In contrast, our lecture defines a chain as any totally ordered subset of a poset.

Definition (Chain). Let (D, <) be a partial ordered set. A subset X \subset D is called chain if X is totally ordered

So under this definition, the increasing sequence in chain can be finite, or even empty (in case of the empty set). And in our lecture, a 'completeness of chain' concept corresponds to CPO, which every chain, even a finite one, has a lub. Thus, by lemma (lecture3, p25), CPO should always have a bottom element.

---

I understand that CPO is equivalent to domain in Reynold's definition. What I think somewhat counterintuitive is that chain can be a finite subset. While we're interested in finding lub of chains, defining finite, or "not-interesting" chains seems unnecessary (because finding its limit is very trivial).

Especially when we're reasoning with specific chains in the CPO (or domain), we are really interested in 'interesting' chains, because they are really a useful target of LFP theorem. Also any finite totally ordered sequence can be extended to infinite chain, (x_0 < x_1 < ... < x_n < x_n < x_n < ...). What really exceptional is when thinking under CPO, one should care exceptional case for empty set, which is not a really a sequence or something, but is defined to be 'chain' (because it is chain). In this sense, I think Reynold's definition is simpler, considering only 'interesting' infinite chains to be used in proofs or constructions or whatsoever.

Or, even if some set is not a CPO (or domain), one can define a partial order so that make the set as predomain, and reason about many chains exist in that set. This is also useful for some applications of abstract interpretation, when selecting initial state for analysis, or the 'bottom element' for transfer function. When computing lfp of transfer function, using specific element instead of global bottom can be utilized for situations when specific initial states for the runtime are defined.

---

Later in the same chapter, Reynolds mention that

It should be mentioned that the term "domain" has no universally accepted definition; it has been used with different meanings by different authors, and even by the same author in different publications.

So, I just wonder what is motivation behind defining CPO as always equipped with bottom elements. Also, what definitions of domains (for abstract interpretation's abstract domain) are generally accepted in academia?

Again, not a really important question but just came across this question while I was solving HW3, but would be happy to discuss about backgrounds for formal concepts.

---

Reference

John C. Reynolds, Theories of Programming Languages, Cambridge University Press, 1998

[KihongHeo]

Hi Yusung,

Very good question. Below I try to do my best to first summarize your questions and answer to them one by one. Any further discussions are always welcome.

• Definition of "chain": As Reynolds mentioned, different authors use different definitions. For example, this book, Wikipedia, etc use the same definition as in the lecture note. BTW, I also recommend you take a look at the book by Patrick Cousot (founder of abstract interpretation), if you are interested in the deep inside of AI (Abstract Interpretation, for sure).

• "any finite totally ordered sequence can be extended to infinite chain, (x_0 < x_1 < ... < x_n < x_n < x_n < ...).": That is not true. Because a chain is a set, not a list, so it does not allow duplications (i.e., x_n, x_n).

• Why do we care of finite chain? We often define finite height abstract domains. AI is a theory that can handle finite and infinite abstract domain. In my opinion, talking about finite chains would be unnecessary, as you mentioned, when we are only concerned with concrete domains. However, AI is concerned with finite domains also.

• What is the motivation behind defining CPO as always equipped with bottom elements? In my opinion, the main motivation is to make a general framework that is applicable to a wide range of static analyses. By doing so, we can have the fixed point transfer theorem, which is based on the Kleene's fixed point theorem, which provides a very general method to find a least fixed point. See the proof of the fixed point transfer theorem. The existence of bottom in abstract domain plays an important role (i.e., base case of induction).

  Of course, there can be many ways to design sound static analyses without using AI. In such cases, you may not need bottom, CPO, etc. You can design your own method and provide your own proof. For example, type systems typically do not use the AI framework and have their own way to prove their soundness (i.e., preservation and progress). They don't consider bottom, CPO, etc, explicitly. Also you may design a completely different algorithm to find LFP depending on your specific situation.

  In short, AI is not the only one way to design static analyses but the most general and simplest framework to provide a guidance for soundness guarantee.

[yusungsim]

Thank you for the comment, professor! I guess I'll check out the book from P. Cousot and study more about domain theory used in abstract interpretation, specifically ...:)