\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{prefix order}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{relations}{}\paragraph*{{Relations}}\label{relations}

[[!include relations - contents]]

\hypertarget{category_theory}{}\paragraph*{{$(0,1)$-Category theory}}\label{category_theory}

[[!include (0,1)-category theory - contents]]

\hypertarget{prefix_orders}{}\section*{{Prefix Orders}}\label{prefix_orders}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{as_a_set_with_extra_structure}{As a set with extra structure}\dotfill \pageref*{as_a_set_with_extra_structure} \linebreak
\noindent\hyperlink{as_a_partial_order_with_downward_totality}{As a partial order with downward totality}\dotfill \pageref*{as_a_partial_order_with_downward_totality} \linebreak
\noindent\hyperlink{history_preserving_functions}{History preserving functions}\dotfill \pageref*{history_preserving_functions} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

By a \emph{prefix order} we mean a [[partial order]] which is also downwards [[total order|totally ordered]].

The concept was introduced in (\hyperlink{Cuipers13a}{Cuipers 13a}, \hyperlink{Cuipers13b}{Cuipers 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, \hyperlink{Cuipers13a}{Cuipers 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, \hyperlink{FerlezCleavelandMarcus14}{Ferlez-Cleaveland-Marcus 14} discovered the definition of ``pointed prefix orders'' and named them ``generalized execution trees''.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

\hypertarget{as_a_set_with_extra_structure}{}\subsubsection*{{As a set with extra structure}}\label{as_a_set_with_extra_structure}

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

Given a [[set]] $S$, a \textbf{prefix order} on $S$ is a (binary) [[relation]] $\leq$ with the following properties:

\begin{itemize}%
\item [[reflexive relation|reflexivity]]: $x \leq x$ always;


\item [[transitive relation|transitivity]]: if $x \leq y \leq z$, then $x \leq z$;


\item [[antisymmetric relation|antisymmetry]]: if $x \leq y \leq x$, then $x = y$.


\item [[downward totality]]: if $x \leq z$ and $y \leq z$, then $x \leq y$ or $y \leq x$.



\end{itemize}
A \textbf{prefix ordered set} is a set equipped with a prefix order.

\hypertarget{as_a_partial_order_with_downward_totality}{}\subsubsection*{{As a partial order with downward totality}}\label{as_a_partial_order_with_downward_totality}

A prefix ordered set is precisely a [[poset]] satisfying the extra condition that $x \leq z$ and $y \leq z$ implies that $x \leq y$ or $y \leq x$.

\hypertarget{history_preserving_functions}{}\subsubsection*{{History preserving functions}}\label{history_preserving_functions}

The morphisms of prefix ordered sets are [[history preserving function]]s. Given $x \in S$, the \textbf{history} of $x$ is the set $x^- = \{ y \mid y \leq x \}$. A \textbf{history preserving function} $f$ from a prefix ordered set $S$ to a prefix ordered set $T$ is a [[function]] from $S$ to $T$ (seen as [[structured sets]]) such that $f(x^-) = f(x)^-$.

Equivalently, it is a [[monotone function]] between $S$ and $T$ (interpreted as [[posets]]) satisfying the additional property that for every $x \in S$ and $y \in T$ such that $y \leq f(x)$ there exists a $x' \in S$ with $x' \leq x$ and $f(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]])

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\begin{itemize}%
\item 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 $S$, the set $H = \{ x^- \mid x \in S \}$ is prefix ordered and isomorphic to $S$ (with `taking the history of an element' and `taking the maximum of a history' being the witnessing isomorphisms).


\item 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.


\item 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.



\end{itemize}
\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\begin{itemize}%
\item 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.

\end{itemize}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[partial order]]
\item 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.
\item 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.

\end{itemize}
\hypertarget{References}{}\subsection*{{References}}\label{References}

\begin{itemize}%
\item [[Pieter Cuijpers]], \emph{Prefix Orders as a General Model of Dynamics}, Proceedings of the \href{http://www.dcm-workshop.org.uk/2013/}{9th International Workshop on Developments in Computational Models (DCM)} p. 25–29 (\href{http://www.dcm-workshop.org.uk/2013/dcm-2013-pre-proc.pdf#page=30}{pdf})


\item [[Pieter Cuijpers]], \emph{The Categorical Limit of a Sequence of Dynamical Systems}, \href{https://www.win.tue.nl/expresssos2013/}{EPTCS 120 : Proceedings EXPRESS/SOS 2013}, p. 78-92, 2013 (\href{https://arxiv.org/abs/1307.7445}{arXiv:1307.7445}, \href{}{doi:10.4204/EPTCS.120.7})


\item James Ferlez, Rance Cleaveland, Steve Marcus, \emph{Generalized Synchronization Trees}, LLNCS 8412: Proceedings of FOSSACS'14, 2014, p. 304–319 ()



\end{itemize}
[[!redirects prefix ordered]] [[!redirects downward totality]] [[!redirects downward total relation]] [[!redirects history preserving function]] [[!redirects Pfx]]



\end{document}