Prefix order


In mathematics, especially order theory, a prefix ordered set generalizes the intuitive concept of a tree by introducing the possibility of continuous progress and continuous branching. Natural prefix orders often occur when considering dynamical systems as a set of functions from time to some phase space. In this case, the elements of the set are usually referred to as executions of the system.
The name prefix order stems from the prefix order on words, which is a special kind of substring relation and, because of its discrete character, a tree.

Formal definition

A prefix order is a binary relation "≤" over a set P which is antisymmetric, transitive, reflexive, and downward total, i.e., for all a, b, and c in P, we have that:
  • a ≤ a ;
  • if a ≤ b and b ≤ a then a = b ;
  • if a ≤ b and b ≤ c then a ≤ c ;
  • if a ≤ c and b ≤ c then a ≤ b or b ≤ a.

Functions between prefix orders

While between partial orders it is usual to consider order-preserving functions, the most important type of functions between prefix orders are so-called history preserving functions. Given a prefix ordered set P, a history of a point p∈''P is the set p''− =. A function f: P → Q between prefix orders P and Q is then history preserving if and only if for every p∈''P we find f'' = f−. Similarly, a future of a point p∈''P is the set p''+ = and f is future preserving if for all p∈''P we find f'' = f+.
Every history preserving function and every future preserving function is also order preserving, but not vice versa.
In the theory of dynamical systems, history preserving maps capture the intuition that the behavior in one system is a refinement of the behavior in another. Furthermore, functions that are history and future preserving surjections capture the notion of bisimulation between systems, and thus the intuition that a given refinement is correct with respect to a specification.
The range of a history preserving function is always a prefix closed subset, where a subset S ⊆ P is prefix closed if for all s,t ∈ P with t∈S and s≤t we find s∈S.

Product and union

Taking history preserving maps as morphisms in the category of prefix orders leads to a notion of product that is not the Cartesian product of the two orders since the Cartesian product is not always a prefix order. Instead, it leads to an arbitrary interleaving of the original prefix orders. The union of two prefix orders is the disjoint union, as it is with partial orders.

Isomorphism

Any bijective history preserving function is an order isomorphism. Furthermore, if for a given prefix ordered set P we construct the set P- ≜ we find that this set is prefix ordered by the subset relation ⊆, and furthermore, that the function max: P- → P is an isomorphism, where max returns for each set S∈P- the maximum element in terms of the order on P.