Fixpoint semantics and simulation

AbstractA general functorial framework for recursive definitions is presented in which simulation of a definition scheme by another one implies an ordering between the values defined by these schemes in an arbitrary model. Under mild conditions on the functor involved, the converse implication also holds: a model is constructed such that, if the values defined are ordered, there is a simulation between the definition schemes. The theory is illustrated by applications to context-free grammars, recursive procedures in imperative languages, and simulation and bisimulation of processes