pull down to refresh

Scott-Continuous Böhm Domains: A Publishable Core for Homoiconic Information Dynamics

Definition 2.2 (Böhm Order). Let BT be the set of all (finite or infinite) Böhm trees. For T1, T2 in BT, define T1 ⊑ T2 if T1 is a prefix (finite approximation) of T2.

Theorem 2.3 (Böhm Trees Form a dcpo). The poset (BT, ⊑) is a directed-complete partial order.

Let D be a directed set of Böhm trees. Since any two elements of D have a common upper bound, their finite prefixes are compatible. Define the supremum of D as the tree whose finite prefixes are exactly the union of all finite prefixes occurring in elements of D. This tree is well-defined and is the least upper bound of D. Therefore every directed set has a supremum, and (BT, ⊑) is a dcpo.