Bifinite domain

A bifinite or SFP domain (Sequences of Finite inductive Partial orders) or effectively algebraic domain is a type of domain with really good "approximation" properties. It arises in modelling purely functional programming languages.

Let D be a complete partial order (cpo). D is bifinite (or SFP) if there exists a sequence of continuous functions

  (h_i : D \to D)_{i \in \mathbb{N}}

which satisfies the following properties.

1. The sequence is a chain: h_i \sqsubseteq h_{i+1} (pointwise)
2. Every h_i is a projection, i.e. an idempotent function below the identity: h_i \circ h_i = h_i \sqsubseteq \textsf{id}_D
3. Every h_i is finitary, in the sense that the image h_i[D] is a finite set.
4. The limit of this chain is the identity: \bigsqcup_{i \in \mathbb{N}} h_n = \textsf{id}_D.

Properties

Bifinite/SFP domains are extremely well-behaved.

The category of bifinite domains is closed under products, function spaces, coalesced sum, and bilimits - so it is cartesian closed. It is also closed under the Hoare powerdomain and Plotkin powerdomain constructions (but not under the Smyth powerdomain).

The final condition on the list above implies that for an arbitrary d \in D we have

d = \bigsqcup_{i \in N} h_i(d)

Hence, the h_i(d) can be thought of as approximating elements: for any d \in D the element h_i(d) is its "i'th approximation". In fact, it can be shown that all such elements are compact, and all compact elements appear in the image of h_i(d).

Lemma. The following are equivalent:

• e \in D is a compact element of D.
• e = h_i(e) for some i \in \mathbb{N}.

It follows that all bifinite/SFP domains are countably algebraic cpos.

Alternative definitions

There are many ways to define what it means for a domain to be bifinite/SFP.

The one given above is summarised by Abramsky and Jung 1994 as

There exists a directed collection (#1) of idempotent deflations (#2 + #3) whose supremum equals the identity (#4).

Equivalently,

The set of all idempotent deflations (#2 + #3) is directed and yields the identity as its join.

Categorical description

Abramsky and Jung 1994 mention the following "categorical" description, due to Plotkin 1976, as Theorem 4.2.7.

Theorem. A dcpo is bifinite iff it is a bilimit of an expanding system of finite pointed posets.

Description through a basis

Another way to describe a bifinite/SFP domain is as a special case of an algebraic cpo.

Let D be an algebraic cpo with a basis B.

*B is mub-complete (or has the m-property) if: for every finite M \sqsubseteq_\text{fin} B, if it has an upper bound then it has a minimal upper bound \textsf{mub}(M).

The mub-closure of a subset of B is the smallest set that contains all its mubs.

A bifinite domain is then an algebraic cpo whose basis B has a least element, is mub-complete, and whose finite subsets have a finite mub-closure.

Occurrences

All the domains used in the Scott model of PCF are bifinite.

Many references define Scott domains to be exactly bifinite/SFP domains with continuous binary infima. This is equivalent to the usual definition.

References

• A textbook treatment of bifinite/SFP domains appears in