Strictly causal functions have a unique fixed point

摘要

The denotational semantics of a deterministic timed system can be described by a function F : (T --> V) --> (T --> V) with T partially ordered. The semantics of a feedback loop then is usually defined by a special (unique) fixed point of F but it is not always obvious that such a fixed point exists. This paper proves that every function F in the very general class of strictly causal functions has a unique fixed point. (C) 2000 Elsevier Science B.V. All rights reserved. [References: 8]