nLab prefix order

Redirected from "Pfx".
Prefix Orders

Prefix Orders

Idea

By a prefix order we mean a partial order which is also downwards totally ordered.

The concept was introduced in (Cuijpers 13a, Cuijpers 13b) in the context of semantics for programming languages, and in particular hybrid and cyber-physical systems, as need arose to generalize the notion of (execution) tree to something that would include a mix of continuous and discrete progress of time. After a lot of experimentation, Cuijpers 13a discovered that the generalization needed was something that expresses two things: time branches when it goes forward (due to different possible courses of action a system may take), but seems linear when looking backward.

A different way of looking at it, is that executions of systems have a natural prefix order on them. Trying to come up with a generic definition of what a ‘prefix’ is, Cuijpers could not find anything in literature and came up with the definition below. As it turns out, in roughly the same period, Ferlez-Cleaveland-Marcus 14 discovered the definition of “pointed prefix orders” and named them “generalized execution trees”.

Definition

As a set with extra structure

A prefix order may be understood as a set with extra structure.

Given a set SS, a prefix order on SS is a (binary) relation \leq with the following properties:

A prefix ordered set is a set equipped with a prefix order.

As a partial order with downward totality

A prefix ordered set is precisely a poset satisfying the extra condition that xzx \leq z and yzy \leq z implies that xyx \leq y or yxy \leq x.

History preserving functions

The morphisms of prefix ordered sets are history preserving functions. Given xSx \in S, the history of xx is the set x ={yyx}x^- = \{ y \mid y \leq x \}. A history preserving function ff from a prefix ordered set SS to a prefix ordered set TT is a function from SS to TT (seen as structured sets) such that f(x )=f(x) f(x^-) = f(x)^-.

Equivalently, it is a monotone function between SS and TT (interpreted as posets) satisfying the additional property that for every xSx \in S and yTy \in T such that yf(x)y \leq f(x) there exists a xSx' \in S with xxx' \leq x and f(x)=yf(x') = y.

In this way, prefix ordered sets form a category Pfx. Furthermore, they are sometimes also viewed as a concrete category over Pos (rather than Set), with history preserving maps preserving the way in which executions of a system unfold, while order preserving maps preserve only the way in which the executions are observed by external observers. (For an example of why this distinction is useful, see also the article on embedding open maps? as a generalization of bisimulation)

Properties

  • Every prefix order is isomorphic to its set of histories under subsets, leading to the intuition that the elements of a prefix order ‘are’ their histories. Formally: given a prefix ordered set SS, the set H={x xS}H = \{ x^- \mid x \in S \} is prefix ordered and isomorphic to SS (with ‘taking the history of an element’ and ‘taking the maximum of a history’ being the witnessing isomorphisms).

  • Products of prefix orders are not the usual Cartesian products, but rather are formed by all possible ‘mergings’ of the histories of elements of the combined prefix orders.

  • In the work of Cleaveland, a different type of products was defined, but at this point I do not know of a notion of morphism on prefix ordered sets that would result in that product.

Examples

  • Be careful. Products of prefix orders are not the usual Cartesian products, rather the histories of a prefix order are ‘merged’. When taking the product of a countable and an uncountable history, unexpected phenomena may happen that leave one with an empty set. A ‘cure’ for this seems to be to restrict to prefix orders in which each history has a minimum.
  • partial order
  • In some books on order theory, a partially ordered set that is downward well-ordered is used as a characterization of a tree. Prefix orders relax this definition to downward total orders.
  • Any partial order can be viewed as an Alexandroff topology. When viewing prefix orders as an Alexandroff topology, the history preserving maps translate to continuous open maps.

References

Last revised on March 9, 2021 at 18:23:30. See the history of this page for a list of all contributions to it.