We study solutions to systems of stream inclusions 'f in T(f)', where T is assumed to be causal in the sense that elements in output streams are determined by a finite history of inputs. For solving these inclusions we develop a correspondence of causality and contraction with respect to the prefix distance on streams. Now, based on this causality-contraction correspondence, we apply fixpoint principles for the spherically complete ultrametric space of streams to obtain solutions for causal stream inclusions. The underlying fixpoint iterations induce fixpoint induction principles for reasoning about solutions of causal stream inclusions. In addition, these fixpoint approximations induce anytime algorithms for computing finite stream prefixes of solutions. We illustrate the use of these developments for some central concepts of system design.
翻译:暂无翻译