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.
翻译:我们研究形如'f in T(f)'的流包含系统的解,其中T被假定为因果性的,即输出流中的元素由输入的有限历史决定。为求解这些包含关系,我们建立了因果性与关于流上前缀距离的收缩性之间的对应关系。基于这种因果-收缩对应,我们应用球形完备超度量空间上的不动点原理,以获得因果流包含的解。基础的不动点迭代推导出用于推理因果流包含解的不动点归纳原理。此外,这些不动点近似值产生了用于计算解的有限流前缀的随时算法。我们通过系统设计中的若干核心概念展示了这些发展的应用。