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 be a complete partial order (cpo). is bifinite (or SFP) if there exists a sequence of continuous functions
which satisfies the following 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 we have
Hence, the can be thought of as approximating elements: for any the element 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 .
Lemma. The following are equivalent:
It follows that all bifinite/SFP domains are countably algebraic cpos.
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.
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.
Another way to describe a bifinite/SFP domain is as a special case of an algebraic cpo.
Let be an algebraic cpo with a basis .
* is mub-complete (or has the m-property) if: for every finite , if it has an upper bound then it has a minimal upper bound .
The mub-closure of a subset of is the smallest set that contains all its mubs.
A bifinite domain is then an algebraic cpo whose basis has a least element, is mub-complete, and whose finite subsets have a finite mub-closure.
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.
Streicher, Thomas. Domain-Theoretic Foundations of Functional Programming. World Scientific, 2006.