Higher-order and Symbolic Computation Manuscript No. Keeping Calm in the Face of Change towards Optimisation of Frp by Reasoning about Change

Higher-order and Symbolic Computation Manuscript No. Keeping Calm in the Face of Change towards Optimisation of Frp by Reasoning about Change
复制标题

高阶符号计算手稿号《面对变化保持冷静,通过变化推理实现FRP优化》

DOI:
--
复制
发表时间:
--
期刊:
影响因子:
--
通讯作者:
Henrik Nilsson
Henrik Nilsson
中科院分区:
--
文献类型:
--
作者:
Neil Sculthorpe;Henrik Nilsson

文献摘要

被引文献

相似文献

功能反应编程(FRP)是一种反应编程的方法,其中系统被构造为对信号进行操作的功能网络。FRP基于同步数据流范例,同时支持(近似)连续时间和离散时间信号(混合系统)。使FRP有别于大多数其他类似应用的语言的是,它支持具有动态结构的系统和更高阶的反应性结构(例如,携带信号的信号或信号上的函数)。本文通过研究n元信号函数在连续时间和离散时间混合信号上的结构动态网络环境中的信号变化和变化传播的概念,有助于提高FRP实现的技术水平。我们首先为这种FRP定义了一种理想的指称语义(时间是真正连续的),以及用时间逻辑表示的信号的时态属性以及与变化和变化传播有关的信号函数。然后,使用这个框架,我们展示了如何对变化进行推理;具体地说,我们识别并证明了一些可能的优化,例如避免重新计算不变的值。注意,由于结构的动态性,以及信号函数的输出可能会改变的事实,因为即使输入是不变的,时间也在流逝,这一问题比具有静态结构的网络中的标准改变传播要复杂得多。
Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both (an approximation to) continuous-time and discrete-time signals (hybrid systems). What sets FRP apart from most other languages for similar applications is its support for systems with dynamic structure and for higher-order reactive constructs (e.g. signals carrying signals or functions on signals). This paper contributes towards advancing the state of the art of FRP implementation by studying the notion of signal change and change propagation in a setting of structurally dynamic networks of n-ary signal functions operating on mixed continuous-time and discrete-time signals. We first define an ideal denotational semantics (time is truly continuous) for this kind of FRP, along with temporal properties, expressed in temporal logic, of signals and signal functions pertaining to change and change propagation. Using this framework, we then show how to reason about change; specifically, we identify and justify a number of possible optimisations, such as avoiding recomputation of unchanging values. Note that due to structural dynamism, and the fact that the output of a signal function may change because time is passing even if the input is unchanging, the problem is significantly more complex than standard change propagation in networks with static structure.