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'' (a totally-ordered set) 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'' (reflexivity);
*if ''a ≤ b'' and ''b ≤ a'' then ''a'' = ''b'' (antisymmetry);
*if ''a ≤ b'' and ''b ≤ c'' then ''a ≤ c'' (transitivity);
*if ''a ≤ c'' and ''b ≤ c'' then ''a ≤ b'' or ''b ≤ a'' (downward totality).

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 (by definition totally ordered) 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''(''p''−) = ''f''(''p'')−. Similarly, a future of a point ''p''∈''P'' is the (prefix ordered) set ''p''+ = and ''f'' is future preserving if for all ''p''∈''P'' we find ''f''(''p''+) = ''f''(''p'')+.

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(S)'' returns for each set ''S∈P-'' the maximum element in terms of the order on P (i.e. ''max(p-) ≜ p'').

References

*
*
*

{{Order theory

Dynamical systems
Order theory
Trees (data structures)