Inmathematics, especiallyorder theory, aprefix ordered set generalizes the intuitive concept of atree by introducing the possibility of continuous progress and continuous branching. Natural prefix orders often occur when consideringdynamical systems as a set of functions fromtime (atotally-ordered set) to somephase space. In this case, the elements of the set are usually referred to asexecutions of the system.
The nameprefix order stems from the prefix order on words, which is a special kind ofsubstring relation and, because of its discrete character, a tree.
Aprefix order is abinary relation "≤" over asetP which isantisymmetric,transitive,reflexive, anddownward total, i.e., for alla,b, andc inP, we have that:
While between partial orders it is usual to considerorder-preserving functions, the most important type of functions between prefix orders are so-calledhistory preserving functions. Given a prefix ordered setP, ahistory of a pointp∈P is the (by definition totally ordered) setp− = {q |q ≤p}. A functionf:P →Q between prefix ordersP andQ is thenhistory preserving if and only if for everyp∈P we findf(p−) =f(p)−. Similarly, afuture of a pointp∈P is the (prefix ordered) setp+ = {q |p ≤q} andf is future preserving if for allp∈P we findf(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 arefinement of the behavior in another. Furthermore, functions that are history and future preservingsurjections capture the notion ofbisimulation between systems, and thus the intuition that a given refinement iscorrect with respect to a specification.
Therange of a history preserving function is always aprefix closed subset, where a subsetS ⊆ P isprefix closed if for alls,t ∈ P witht∈S ands≤t we finds∈S.
Taking history preserving maps asmorphisms in thecategory of prefix orders leads to a notion of product that isnot the Cartesian product of the two orders since the Cartesian product is not always a prefix order. Instead, it leads to anarbitrary interleaving of the original prefix orders. The union of two prefix orders is thedisjoint union, as it is with partial orders.
Any bijective history preserving function is anorder isomorphism. Furthermore, if for a given prefix ordered setP we construct the setP- ≜ { p- | p∈ P} we find that this set is prefix ordered by the subset relation ⊆, and furthermore, that the functionmax: P- → P is an isomorphism, wheremax(S) returns for each setS∈P- the maximum element in terms of the order on P (i.e.max(p-) ≜ p).