Directed-complete partial orders

The semantics of loops, iteration or recursion are often computed as limits of sequences of increasingly terminating computations. ...

Directed sets

Definition

Since we are primarily interested in bounded dcpos, we use a non-standard definition of directed set which permits empty sets. This allows us to treat the lower bound uniformly as a directed supremum.

Basic instances

Image through a monotonic function

DCPOs

A directed-complete partial order is a poset where every directed subset has a supremum. Since we define directed sets as possibly empty, the resulting structure is a bounded dcpo.

Properties of dsup

For convenience, we provide specialized versions of the supremum properties.

Least element

Binary case for dsup

In some proofs below we will need to express ordering in terms of directed suprema of pairs. Below we provide the relevant properties.

Pairs like the ones defined above are directed when the two elements are related.

Moreover, the supremum is the largest of the two elements.

Derived DCPOs

Binary products

Dependent products

Scott-continuous functions

Definition

A Scott-continuous function preserves directed suprema. The formulation below uses monotonicity as a starting point. This takes care of preserving the "upper bound" aspect of suprema, and we add the "least" as a separate condition. We use a flag strict to control whether the morphism is expected to preserve bot. This is done by apply the following condition to the index set used with dsup. NB: this could be incorporated into the Directed class, and the same approach could be used to jointly define bounded and not-necessarily-bounded DCPOs.

Our definition states that the image of dsup x is the supremum of the image of x. This way we don't need to involve the target dsup operation, which is only defined when f x is directed. The preservation of the "upper bound" condition is equivalent to monotonicity; the "least" condition is just stated as-is.

Any strict Scott-continuous functions is also non-strict Scott-continuous.

Equational statement

The definition above is equivalent to this statement.

Because suprema are unique, this means dsup is preserved.

For maximum generality, the lemma above is stated in terms of a pre-existing proof that the image set is directed, but when rewriting we will often need the following instance.

Composition

Category of DCPOs and strict Scott-continuous functions

Free DCPO

The free DCPO generated by a set X is the flat semilattice which extends X with a bottom element. This is in essence option X, however that computable version does not allow us to define the possibly infinite directed suprema we need. The version below allows these suprema to be defined at the expense of computability.

Definition

Our construction uses sets with at most one element. They are ordered under set inclusion.

Monad stuff / map from Set

Fixed point constructions

Overview

Every monotone function f : D → D in a DCPO D admits a least fixed point μf : D. This can be used to obtain semantics for loops and recursion that abstract away the numbers of unfolding steps involved in reaching a result, retaining only a distinction between computations based on whether they terminate, and the result they produce when they do. For example, consider the traditional example of a recursive function: fact n := if n=0 then 1 else n * fact (n-1). We would like to interpret this definition as ⟦fact⟧ : Z → fdc Z in the domain of partial functions from integers to integers, so that ⟦fact⟧(n) gives the result of calling fact with argument value n, or is undefined when this would result in a non-terminating computation. We can compute this partial function as a fixed point of the functional Φ : (Z → fdc Z) → (Z → fdc Z) defined as: Φ F n := if n=0 then 1 else n * F (n-1). Note that Φ avoids self-referentiality by "delegating" the computation of recursive calls to its function argument F. It is monotone in the sense that plugging in an F' defined for more n's but otherwise idendical to F will yield a similarly "more defined" Φ F ⊑ Φ F'. Hence, by our fixed point construction we can obtain a function μΦ : Z → fdc Z such that Φ μΦ = μφ. In other words, μΦ is a version of Φ which can handle its own recursive calls: μΦ n = Φ μΦ n = if n=0 then 1 else n * μΦ (n-1). Below we provide two constructions of the least fixed point in a DCPO. The Kleene-style fixed point requires Φ to be Scott-continuous, but is simpler to define and illustrates the basic ideas behind the construction. The Tarsky-style construction applies to all monotonic functions regardless of continuity, but requires generalizing the Kleene iteration to ordinal numbers.

Kleene fixed point

Approximation sequence

Consider a Scott-continuous function f : D → D on a DCPO D. Since ⊥ ≲ f ⊥ and f is monotonic, we have f ⊥ ≲ f (f ⊥), and in turn f (f ⊥) ≲ f (f (f ⊥)) etc, so that by induction on n the iterates f^n ⊥ ≲ f (f^n ⊥) are aleady postfixed points of f and constitute an increasing sequence. By virtue of being a postfixed point, each iterate is either a fixed point with f^{n+1} = f (f^n) = f^n, or is succeeded by an approximation f^{n+1} ≠ f^n that is strictly greater than all preceding ones. Moreover, since ⊥ ≲ x and f^n x ≲ x for any prefixed point x, it must be the case that f^n ⊥ ≲ x for any fixed (and therefore prefixed) point x.

Limit

Although the sequence f^n ⊥ may never itself reach the actual least fixed point μf, its limit f^* ⊥ := dsup n, f^n ⊥ shares the property of being a postfixed point and below any prefixed point.

Properties

Moreover, if f is Scott-continuous, then f (f^* ⊥) = dsup n, f (f^n ⊥) = dsup n, f^(n+1) ⊥ = f^* ⊥ so that f^* ⊥ is indeed the least fixed point.

Unfortunately, in some applications the recursive processes we wish to study fail Scott-continuity. This is especially true in the context of concurrency and fair scheduling, which involve infinite nondeterminism. In that case, even f^* ⊥ may not be a fixed point yet, and further applications of f and taking limits may be necessary. To account for this process we must generalize the finite iterates f^n ⊥ from natural numbers n to ordinal numbers α and a corresponding notion of transfinite iterates f^α.

Ordinal numbers

To index our new approximation sequence, we need a representation of ordinal numbers. Ordinal numbers generalize natural numbers by allowing the construction of a least upper bound for any set of predecessor ("limit ordinals") as well as zero and successors.

Definition

We represent ordinals using an inductive type with a single constructor sup_succ {I} : (I → ord) → ord, where sup_succ α represents the limit ordinal ⋃ᵢ (αᵢ + 1). Zero can be represented as sup_succ (I := Empty_set) _ and the successor of α as sup_succ (I := unit) (fun _ ⇒ α). In other words, as with nat, the number being represented corresponds to the depth of the tree, but unlike nat the branching allows us to construct trees with infinite depths. This approach is used in the mechanization of ordinals published by the SNU Software Foundations Laboratory at https://github.com/snu-sf/Ordinal. Note that the representation is not canonical since multiple sets may have the same sup, but this does not matter for our purposes. For clarity, we name the universe Ord.U from which we draw the possible arities of sup_succ.

Ordering

Since every ordinal is a constructed as a sup, they can be ordered as follows.

Note that le is not antisymmetric but defines a preorder. There is an equivalence class in this preorder for each ordinal.

As expected, every ordinal is strictly greated than its predecessors.

Ordinals are totally ordered. This property is important because it means every increasing ord-indexed sequence in a dcpo is directed and therefore has a sup.

We can also define the associated strict order.

Ascending chains

The key property we will use to show that the transfinite iterates of f eventually reach a fixed point is that for every element of a well-founded set, we can construct an ordinal number α such that no strictly increasing α-chain reaches it.

The following predicate states that there exists an α-chain ending in y.

We can then describe the largest ordinal α such that there is an α-chain ending in y as follows.

This means we can define an ordinal larger than any chain.

Tarsky-style fixed point

To obtain the least fixed point, we generalize the Kleene construction used in the continuous case by constructing a family of approximants f_α such that f_(⋃ᵢ 1+αᵢ) = ⋁ᵢ f(f_αᵢ). Note that we recover the Kleene iterates as the special cases f_n = f^n(⊥) for n∈ℕ, and f_ω = f^*(⊥). This construction is documented for example in the paper "Constructive versions of Tarski's fixed point theorems" by Cousot & Cousot.

Specification

While we will eventually be able to construct f_α by recursion on the structure of α, the recursion step involves a supremum that is only defined by virtue of the set of predecessor approximants being directed. In turn this is true only because these approximants increase with α and the fact that ordinal numbers are totally ordered. Because of this somewhat circular dependency between the definition and some of its logical consequences, writing a specification first is more convenient.

To show that they can be constructed, we must first establish that the approximants increase with their ordinal index.

Construction step

Because ordinals are totally ordered, this means all sets of approximants are directed, and we can take their sup.

Definition

With all this in place we can now define the recursive construction of our approximants.

Well-foundedness

The set of approximants is well-ordered with respect to the underlying dcpo.

Based on this specification, we can show that the set of approximants generated in this way is well-founded.

Now we can show that this is indeed the least fixed point.

When f is Scott-continuous then the two constructions coincide.