函数式反应式编程中连续信号的实现及优化方法

理论计算机科学电子笔记193（2007）29-45www.elsevier.com/locate/entcs用箭头Hai Liu和Paul Hudak1耶鲁大学New Haven，CT 06511，美国摘要函数式反应式编程中概念连续信号的实现详细研究了。我们表明，递归信号在标准实现中使用流和延续导致潜在的严重的时间和空间泄漏，根据传统的呼叫需要评估。然而，通过移动到信号函数的级别，并围绕箭头构建设计，可以避免此类时间和空间泄漏。我们进一步表明，使用最优约简也可以避免这个问题，代价是一个更复杂的评估。保留字：编程语言，函数式编程，箭头，Haskell1引言函数式反应式编程（Functional Reactive Programming，简称FRP）是一种以声明式风格编程混合系统的方法FRP已用于各种应用，包括计算机动画[10]，移动机器人[24，25]，人形机器人[13]，实时系统[31]，并行处理[12]和图形用户界面[7]。在本文中，我们专注于连续性的FRP，而忽略其反应成分。由于FRP的连续性只是一种理想，因此必须在实际实现中近似。FRP的原始实现使用时间排序的值流来进行这种近似[9，10]。1电子邮件：hai. yale.edu和paul. yale.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.10.00630H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29后来的实现使用了一种简单的延续，并且还使用箭头进行结构化[16，22，15]。尽管FRP已成功地用于许多应用中，但大多数实施方案都存在不同程度的空间泄漏。有趣的是，在我们称之为Yampa[8]的FRP的最新化身中观察到空间泄漏程度的显著改善（即减少）。Yampa 空间利用率提高的原因相当微妙，到目前为止大多是轶事。事实上，本文的主要目的是描述FRP中的一类特殊空间泄漏，说明它们发生的原因，并准确解释Yampa中如何避免它们在本文的其余部分，我们首先描述了FRP的两个标准的非基于箭头的实现，并表明它们都容易受到严重的空间泄漏。然后，我们在第3节中描述箭头，并在第4节中使用它们设计一个与Yampa类似的FRP新实现。我们在第5节中展示了这个新的实现不会像标准实现那样遇到相同的空间泄漏问题。在第6节中，我们讨论了解决空间泄漏问题的一些替代方法。我们假设熟悉Haskell [26]和基本的函数式编程概念[14]。2两个标准实现从概念上讲，FRP中的连续值（称为信号）是时变值，可以认为是时间的函数信号α时间→αFRP的强大之处在于，编程是在信号级完成的。例如，两个信号s1和s2可以相加在一起，如s1+s2，其在概念上是表示s1和s2的函数的逐点和。(And Haskell更重要的是，可以对信号执行诸如积分和微分的有状态计算例如，信号s1的积分仅仅是积分s1。 用这种方法，很容易写出常用于描述动态系统的积分或微分方程尽管连续信号具有吸引人的性质，并且它们作为时间函数的优雅表示，但在实践中，我们感兴趣的是计算H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2931→→→newtype S a=S（[DTime][a]）type DTime=DoubleintegralS：： Double→S Double→S DoubleintegralSi（Sf）=S（λdts→scanl（+）i（zipWith（λ）dts（fdts）runS：：S Double[Double]runS（Sf）=f（repeatdt）Fig. 1.流基FRPnewtype C a= C（a， DTime→ Ca）integralC：： Double→C Double→C DoubleintegralCi（Cp）=C（i，λdt→integralC（i+fstp<$dt）（sndpdt））runC：：CDouble [Double]runC（C p）=fstp： runC（snd pdt）图二. 基于连续的FRP这些值在数字计算机上的连续流，因此上述表示所暗示的功能实现是不切实际的。在下文中，我们将描述我们使用过的两个最简单的实现，它们足以演示我们感兴趣的。2.1流基FRP在《哈斯克尔表达式学派》一书中，连续信号被称为行为，并被定义为一个从离散时间样本列表到一系列的价值观。 图1给出了一个简化版本，对于时间样本，我们使用时间间隔（我们称之为还包括积分函数的定义，它将在我们的空间泄漏示例中发挥关键作用。integralS取一个初始值，并返回一个信号，该信号是使用欧拉法则的输入信号2.2基于连续的FRP实现FRP的另一种方法是将信号视为一对，由其当前值和一个简单的延续组成，在时间间隔上产生它的未来值。完整定义见图2。请注意，运行S和运行C都假定固定的增量时间dt。我们这样做是为了方便，但实际上，delta时间在程序执行过程中会发生变化，并取决于处理器速度、计算负载、中断等。32H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29→2.3第一千一百一十一章空间泄露尽管函数式语言有很多优点，但它们最大的缺点可能是有时候很差，而且往往是不可预测的空间消耗，特别是对于非严格（懒惰）语言，如Haskell。已经提出了许多优化技术，包括尾调用优化，CPS转换，垃圾收集，严格性分析，森林砍伐等[6，1，29，30，28，21]。这些技术中的许多现在是现代编译器（如Glasgow Haskell编译器（GHC））的标准。不然而，所有的优化技术在任何时候都是有效的，在某些情况下可能会导致更差的性能而不是更好的性能[11]。也有关于相对泄漏的工作[5，11，4]，其中研究和比较了不同优化技术或抽象机器的空间行为事实上，上述两种FRP实现，由于它们看起来很无辜的定义，都可能导致空间泄漏。 特别地，假设我们定义了一个递归信号，例如指数值e的定义，它直接反映了它的数学公式：e=integralC 1 e我们的直觉告诉我们，展开e在时间上应该是线性的，并且是常数在太空时间复杂度为O（n），空间复杂度为O（n）。因此，在任何标准的Haskell编译器中，计算e的连续值很快就会崩溃，消耗内存，并且计算每个 值 所 花 费 的 时 间 越 来 越 长 。 (The 如 果 我 们 使 用 integralS 而 不 是integralC，也会出现同样的问题。）要查看泄漏发生在何处，让我们使用按需调用评估来逐步展开计算。除了缺乏正式性之外，我们采用了一种熟悉的风格，使用let表达式来表示术语的共享[18，2，20]。图3中示出了游程C e的展开，其中e =integralC1 e。这里的问题是，标准的按需调用评估规则无法识别该函数：f=λdt→integralC（1+dt）（f dt）是相同的：f=λdt令x=integralC（1+dt）xinx前一种定义导致在递归调用f时重复工作，而在后一种情况下，计算是共享的。这导致O（n）空间和O（n2）时间来计算n个值的流，而不是O（1）空间和O（n）时间，我们希望。H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2933→∗→ →∗→→ →∗→∗→∗→→→∗→→e=integralC 1 e<$ 令p=（1，λdt integral C（1+fstpdt）（sndpdt））inCpf=（1，f）f=λdt integral C（1+1 dt）（fdt）inCp设 f=λ dt integral C（1+1dt）（fdt）inC（1，f）runC e（C（1，f））<$1：runC（f dt）<$1：runC（integralC（1+1dt）（f dt））i：runC（令if=λdt integral Cig=λ dt integral C（i<$→λ点图三. 展开运行图4以图形方式显示了信号e和e1 = snd e dt，其中e1的大小明显增加。runC e的进一步展开将导致更多的生长和重复的子结构。 理想情况下，我们想要的是e1 = integralC i 'e1的等价物，但是按需调用求值不会给我们这个结果。(a) e（b） e1见图4。 e和e1的图2.4一个类比为了更好地理解这个问题，描述一个更简单但类似的例子可能会有所帮助。假设我们想定义一个函数，它无限地重复它的参数：repeat x=x：重复x或者，用西班牙语：repeat=λx→x：重复x这需要O（n）空间。但是我们可以通过写来实现O（1）空间：重复= λx设xs= x：xsxs中34H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29然而，这个例子的时间和空间复杂度仍然是上面e所展示的时间和空间复杂度的n为了模拟O（n2）时间复杂度，假设我们不重复一个数，而是无限地递增它。这样做的一种方法如下：successors n=n：map（+1）（successors n）但是，这需要O（n2）步来计算第n个值。为了解决这个问题，我们可以这样做：successors n=letns=n：map（+1）ns在ns值得注意的是，如果delta时间固定为常数dt，我们可以重新设计实现如下：新类型Ca=C（a，Ca）integralC：： Double→C Double→C DoubleintegralCi （ C p ） =C （ i ， integralC （ i+fstp <$dt ） （ sndp））现在请注意，C与Haskell的列表数据类型同构（类似的简化也可以用于流实现。但事实上，如前所述，在FRP的实际实现中，我们不能假设delta时间是固定的（即使在runS和runC的简单实现中它是固定的），因此我们不能消除函数类型。有更好的解决办法吗3箭头简介箭头[16，15]是单子的概括，放松了单子所施加的严格这个原则是通过要求组合以“无点”风格来执行的-即组合子用于组合函数而不直接引用函数的值。这些组合子在Arrow类型类中捕获：classArrow a wherearr*（b→ c）→ab c（>）：：abc→a cd→ab d首先：：abc→a（b，d）（c，d）H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2935→⇒→将函数提升为“纯”箭头计算;即，输出完全依赖于输入（类似于Monad类中的return）。（>）通过将第一个的输出连接到第二个的输入来组成两个箭头计算（类似于Monad类中的bind（（>>=））但是除了线性地组合箭头之外，还希望并行地组合有几种方法可以做到这一点，但通过简单地定义Arrow类中的第一个首先将采用一个输入和一个结果的箭头计算转换为采用两个输入和两个结果的箭头原始箭头应用于输入的第一部分，结果成为输出的第一部分。输入的第二部分直接馈送到输出的第二部分其他组合子可以使用这三个原语来定义例如，first的对偶可以定义为：second：：（Arrowa）a b c a（d，b）（d，c）secondf=letswapA=（λ（a，b）（b，a））在swapA中>第一个f> swapA最后，有时需要写“循环”的箭头为此，需要一个额外的组合子（不能从三个基本组合子派生），并在ArrowLoop类中捕获：class ArrowLoop a whereloop：：a（b，d）（c，d）→a bc我们发现，箭头最好用图画来观察，特别是对于通常与FRP一起使用的应用。图5以这种方式显示了基本的组合子，包括循环。4Yampa：箭头型FRPFRP实现的最新变体Yampa使用Arrow类作为信号函数的抽象[15]，在概念上可以被视为：SFαβ信号α→信号β在信号功能级而不是在信号级编程在模块化和输入/输出方面具有某些优势。但除此之外，正如我们将看到的，它通常导致更少的空间泄漏。信号函数的上述概念实现在实现中没有多大用处。务实地说，遵循延续风格，36H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29→F箭头a→（b→c）→a b c（>>>）：：箭头a→abc→a cd→ab d（）：：箭头a→a cd→abc→ab d第一：：箭头a→abc→a（b，d）（c，d）第二：：箭头a→abc→a（d，b）（d，c）（*） ：：箭头a→abc→abloop：：Arrow a→ a（b，d）（c，d）→ab c(a)f（b）sf1>sf2（c）第一sf（d）sf1sf2（e）loopsf图五. 常用的箭头组合器函数是一个函数，给定当前输入，产生一个由其当前输出和延续组成的对newtype SF a b=SF（a→（b，DTime→SF ab））SF的完整定义是一个箭头，一个积分函数的定义，和运行函数的定义，在图6中给出。（省略的是溪流风格中箭头型FRP的另一种定义，它同样适用。使用信号函数编程的一个缺点是，它们必须使用Arrow类组合子以无点的方式组合，这可能导致程序难以处理。幸运的是，最近流行了一种方便的箭头语法，使得这样的程序更容易编写，并且在FRP的情况下，增强了信号处理的直观性[23]。例如，我们的指数信号的运行示例可以使用箭头语法定义为信号函数，如下所示：eSF：：SF（）Double eSF=proc（）dorece← integralSF 1− Ee返回A − EeH. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2937◦→→→→→newtype SF a b=SF（a→（b，DTime→SF ab））实例Arrow SF，其中f=SF（λx（fx，λdt f））首先（SFf）=SF（λ（x，z）令（y，在（（y，z），第一个f'）SFf> SF g=SF（λxlet（y，（z，in（z，λdt→f实例ArrowLoop SF，其中loop（SFf）=SF（λx→let（（y，z），in（y，loop {integralSF：： Double→ SF Double DoubleintegralSFi=SF（λx→（i，λdt→integralSF（i+dt<$x）runSF：：SF（）Double[Double] runSF（SFf）=v：runSF（c dt）其中（v，c）=f（）见图6。 箭基FRP注意，信号函数integral1的输入（右侧）和输出（左侧）相同（即e），因此这是一个循环信号。这个程序扩展到对Arrow类组合子的适当调用，以及对ArrowLoop类中的循环组合子的调用（因为e的递归性质），如附录所示5泄漏分析也许令人惊讶的是，runSF eSF没有时间或空间泄漏-它在线性时间和恒定空间中运行。它这样做是因为计算永远不需要共享函数应用程序的结果。我们在图7中以图表的方式显示了eSF和eSF 1 = snd（eSF（））dt它们的词汇展开，相当乏味，在附录中给出比较eSF和e的定义可以发现，主要的区别在于它们使用的定点算子。e使用Haskell38H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29→(a)eSF（b）eSF 1fix f=f（fixf）图7.第一次会议。 eSF和eSF 1示意图另一方面，eSF是用循环组合子来定义的，它比标准的定点运算符更紧密地联系着循环特别是，请注意图6中的循环将值级别的固定点计算为z，但在延续部分中重用了这是避免空间泄漏的关键。事实上，图6中定义的所有信号函数组合器都有一个共同的特性。也就是说，它们在下一个时间步的延续与当前时间步相同，除了参数之外，因此它们有助于在每次展开时保持eSF注意，数据结构SF和C是相似的：两者都是基于连续的，并且都由值和函数组成。 e和eSF都是某个高阶函数的不动点，因为积分函数都是al。递归定义的。必须计算递归定义的高阶函数的不动点，以及标准的按需调用评估无法正确检测新兴的垂直共享，这是前两个FRP实现中时间和空间泄漏为了强调计算固定点的方法的重要性，我们注意到还有另一种有效的方法来定义指数函数，即：eSF=eSF > integralSF 1在这里，我们依赖于Haskell不幸的是，这个定义源于我们之前看到的时间和空间泄漏问题事实上，我们注意到，对于指数信号函数，标准的箭头组合子假设我们定义一个特殊的不动点算子：fixSF：：SF a a SF（）a fixSF（SFf）=SF（λ（）→let（y，c）=fyin（y，λ dt→ fixSF（cdt）H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2939×并将指数重新定义为：eSF=fixSF（integralSF 1）它没有空间泄漏。6各种途径在按需调用的语言中，计算高阶函数的不动点似乎是所有邪恶的根源，我们有理由问我们是否可以独立于FRP设置来解决这个问题。在图8中，我们表明，事实上，在等式推理的帮助下，通过项重写可以获得e这个变换的结果变成了一个固定点，展开g并没有分解闭包;相反，它重用了同一个g和一个不同的i。因此，它还以类似于Arrow循环组合子的方式避免了空间泄漏问题然而，试图将这种巧妙的转换推广为重写规则是困难的。它适用于FRP的原因是这些递归定义的信号的结构都有一个共同的特征，即它们的未来值保持相同的结构。但一般情况下未必如此或者，我们可以通过使用比按需调用更聪明的评估策略来恢复运行时共享的损失，而不是重写源项以揭示其递归结构。Levy [19]在1990年引入了最优约简的概念，Lamping [17]是第一个为lambda演算发明最优约简的人。Liechti和Guerrini [3]将最优约简总结为：lambda演算=线性lambda演算+共享最优约简的目的是仔细跟踪所有共享结构，以便永远不会发生冗余约简事实上，最优约简能够恢复所有形式的共享，只要它被编码在原始表 达 式 中 ， 包 括 前 面 提 到 的新 兴 的 垂 直 共 享 问 题 。 通 过 我 们 的Lambdas-cope[27]（一种最佳算法）和使用交互网的标准按需调用算法的实现来验证，我们在e n =（runC e）的展开过程中比较了beta约简和算术运算2的数量！中n图9. 数据证实，展开的时间复杂度不，2 我们把下一个dti j=dti+j算作3次操作，因为在项中有3个redice下一个dti j.40H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29→→→→→∗→→∗→→→ →∗→ →∗→ →∗◦e<$ integralC 1 e<$ fix（integralC 1）--使用fix<$ let gi=fix（integralCi）在g1中--引入gi=integralCi（gi）在g1中--展开固定<$ let gi=let f=integralCif在f在g1中--引入f<$→设gi=设f=（i，λdt →integralC（i+dtfstf）（snd f dt））在C fin g 1-- unfolded integral<$ let gi=letf=（i，λdt设h=integralC（i+ dti）（snd fdt）in h）在C f于g1-- reduce（fst f）， introduceh<$ let gi=letf=（i，λdt设h=integralC（i+ dti）h inh）在C f于g1--fold（sndfdt）as h<$ let gi=let f=（i，λdt fix（integralC（i+dti）inC f于g1--使用fix<$ let gi=letf=（i，λdtg（i+dti））inC f以g-- fold（fixintegralC）作为g<$ 令gi=C（i，λdtg（i+dti））在g1中--消去f见图8。重写eExp按需呼叫最优beta算术beta算术e1133113e2289166e35018219e479302612e5115453115e6158633618e7208844121见图9。展开游程e的简化步骤der call-by-need是二次的而不是指数的，因为它冗余地重新计算en−1。事实上，我们有：stepscbn（n）stepsopt（n）+stepscbn（n−1）H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2941其中步骤opt（n）在n中是线性的。另一方面，最优并不一定意味着最有效。在最优评价过程中，共享分析的额外簿记会引起时间和空间的巨大操作开销。 与相对成熟的按需调用编译技术相比，对最佳评估的探索要少得多，而且还不存在真正实用的实现。7结论我们已经描述了FRP中连续信号的两个标准（尽管是简化的）实现，一个基 于流 ， 另 一个 基 于连 续 。 不幸 的 是， 递 归信 号 表示 使 用这 两 个implementa- tions有严重的空间和时间泄漏时，使用传统的呼叫按需评估。问题的根源在于无法识别递归lambda表达式内部出现的共享。相反，如果我们转移到信号函数的水平，这自然会导致基于箭头的设计，泄漏可以被消除。这是因为实现了递归信号的固定点的更严格的计算，其中共享被恢复。更严格的固定点可以通过在箭头框架中适当定义循环组合子来实现，或者通过设计专用的固定点运算符来实现。我们进一步表明，使用最优约简也可以避免泄漏，代价是一个更复杂的评估。最优约简器能够识别递归lambda下的共享，从而避免冗余计算。8确认这项研究部分得到了DARPA STTR合同06 ST 1 -0016下Galois Connections的资助，以及Kempner基金会奖学金下耶鲁大学的资助。还要感谢IFIPWG2.8函数式编程工作组（特别是Simon Peyton Jones）在研究的初步介绍中提出引用[1] Andrew W.阿佩尔继续编译。剑桥大学出版社，纽约，纽约，美国，1992年。[2] 泽纳M. Ariola，Matthias Felleisen，John Maraist，Martin Odersky，and Philip Wadler.按需调用lambda演算。见POPL，第23342H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29[3] 安德里亚·科蒂和斯特凡诺·盖里尼。函数式编程语言的最佳实现。剑桥大学出版社，纽约，纽约，美国，1998年。[4] 亚当·贝克韦尔相对空间效率的运算理论。 博士论文，约克大学，2001年12月。[5] 亚当·贝克韦尔和科林·朗西曼一个比较懒惰计算器的空间使用的模型。声明式编程的原则和实践，第151-162页，2000年[6] William D.粘人适当的尾递归和空间效率。PLDI'98：Proceedings of the ACM SIGPLAN 1998conference on Programming language design and implementation，第174-185页，美国纽约州纽约市，1998年Press.[7] 安东尼·考特尼和科纳尔·艾略特。增强功能性用户界面。2001年Haskell研讨会论文集，2001年9月。[8] 安东尼·考特尼亨利克·尼尔森和约翰·彼得森 扬帕拱廊。 2003年ACM SIGPLAN Haskell研讨会论文集（Haskell'03），第7-18页，瑞典乌普萨拉，2003年8月Press.[9] 科纳尔·艾略特连续建模动画的功能实现。 在PLILP/ALP '98的会议记录Springer-Verlag，1998.[10] 科纳尔·埃利奥特和保罗·胡达克功能反应动画。函数式编程国际会议，第263-273页，1997年6月[11] 约根·古斯塔夫松和大卫·桑兹按需呼叫空间改进的可能性和局限性。函数式编程，265-276页，2001年。[12] L. Huang，P. Hudak，and J. Peterson. Hporter：使用箭头组合并行进程。《声明性语言的实践方面》，第275-289页。Springer Verlag LNCS 4354，2007年1月。[13] Liwen Huang 和 Paul Hudak 。 Dance ： 用 于 控 制 类 人 机 器 人 的 声 明 性 语 言 。 技 术 报 告YALEU/DCS/RR-1253，耶鲁大学，2003年8月。[14] 保 罗 · 胡 达 克 Haskell School of Expression ： Learn Functional Programming ThroughMultimedia（Haskell表达学派：通过多媒体学习函数式编程）剑桥大学出版社，纽约，美国，2000年。[15] 保罗·胡达克安东尼·考特尼亨利克·尼尔森和约翰·彼得森箭头、机器人和函数式反应式编程。在Summer School on Advanced Functional Programming 2002中，牛津大学，Lecture Notes inComputer Science，第2638卷，第159-187页。Springer-Verlag，2003.[16] 约翰·休斯。把单子推广到箭头。Science of Computer Programming，37：67[17] 约翰·兰坪一种最优lambda演算约简算法在POPLPress.[18] 约翰·朗奇伯里一个自然的懒惰计算语义。会议记录第二十届ACM SIGPLAN-SIGACT程序设计语言原理研讨会，第144-154页，查尔斯顿，南卡罗来纳州，1993年。[19] 让-雅克·莱维。 在计算机中的R′教育或Rectes和optimales。博士论文，Uni versi t'eParis VI，1978年。[20] John Maraist，Martin Odersky，and Philip Wadler. 按需调用lambda演算。 杂志FunctionalProgramming，8（3）：275 -317，1998.[21] 西蒙·马洛高阶函数程序的森林砍伐。 博士论文，格拉斯哥大学，1996年。[22] 亨利克·尼尔森安东尼·考特尼和约翰·彼得森功能反应编程，继续。ACM SIGPLAN 2002 Haskell研讨会，2002年10月。H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2943◦→→[23] 罗斯·帕特森箭头的新符号。 在ICFP[24] 约翰·彼得森，格雷戈里·海格，保罗·胡达克.一种用于声明式机器人编程的语言。1999年国际机器人与自动化。[25] 约翰·彼得森，保罗·胡达克，还有科纳尔·埃利奥特Lambda in motion：用Haskell控制机器人第一届声明性语言实践国际研讨会。1999年1月，锡格兰[26] Simon Peyton Jones等，The Haskell 98 language and libraries：The revised report. JournalofFunctionalProgramming，13（1）：0-255，Jan2003.http://www.haskell.org/definition/。[27] Vincent van Oostrom，Kees-Jan van de Looij，and Marijn Zwitserkan. Lambdascope是微积分的另一个最佳实现。在2004年的代数和逻辑编程系统（ALPS）研讨会上[28] P. Wadler砍伐森林：改变计划以消灭树木。在88年的员工持股计划中。European Symposium onProgramming，Nancy，France，1988（Lecture Notes in Computer Science，vol. 300），pages 344-358. 柏林：施普林格出版社，1988年.[29] P. L.瓦德勒有限域上抽象解释的非可拓域的精确性分析. In S. Abramsky和C. Hankin，编辑，声明性语言的抽象解释。埃利斯·霍伍德，奇切斯特，英国，1987年。[30] 菲利普湖瓦德勒使用垃圾收集器修复一些空间泄漏。Software Practice and Experience，17（9）：595[31] Zhanyong Wan，Walid Taha，and Paul Hudak.实时FRP。第六届ACM SIGPLAN函数式编程国际会议论文集，意大利佛罗伦萨，2001年9月。ACM。附录因为SF同构于函数类型，我们不使用箭头语法的eSF的直接定义是：eSF=loop（second（integralSF 1）>循环2），其中第二个f（z，x）=（（z，y），第二个dup2（x， y）=（y，y）eSF的减少如下：ESF<$ loop（second（integralSF 1）>循环2）<$ let f=second（integralSF 1）> dup2in loop f-- introduce f请注意，在一个步骤中，它达到了与图7（a）中的图表相对应的形式。没有必要进一步减少eSF，因为再减少一步循环f将导致弱头范式。按需调用下eSF 1的减少如下（为了节省空间，当没有歧义时，多个步骤合并为一个eSF1<$→snd（eSF（））dt44H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）29→→→→→→→→→→→◦<$ let f=second（integralSF 1）> dup2在snd（loop f（））dt--unfold eSF中，引入f<$ let f=second（integralSF 1）> dup2 f1dt=loop（f2 dt）((z2，z），f2）=f（（）， z）在f1 dt--展开循环，减少snd，引入f1<$ let f=second（integralSF 1）>dup2 g((z2，z），f2）=f（（）， z）在g' -- reduce（f1 dt）中，引入g'<$设g1=second（integralSF1）h1=dup 2fx1=（z1，λdtg1（z1，((z2，z），f2）=f（（）， z）ing' -- introduce g1 h1，unfold ><$设g1=second（integralSF1）h1=dup 2(y1，（z1，((z2，z），f2）=（z1，λdtg1ing' -- reduce（f（（），z））<$设g1=second（integralSF1）h1=dup 2(y1，(z1，f在循环f引入f接下来，为了表明eSF 1确实与图7（b）中所示的相同，我们需要通过进一步减小g1'和h1'来证明fF'<$设g1=second（integralSF1）h1=dup 2(y1，(z1，(z2，z）=z1ing1设k=integralSF 1g1=第二个kh1=重复 2(y1，(z1，(z2，z）=z1在g1设k=integralSF 1h1=重复2（y1，(z1，(z2，z）=z1ing1<$→设h1=dup2(y1，（x，H. Liu，P.Hudak/Electronic Notes in Theoretical Computer Science 193（2007）2945◦∗→∗→→→∗→∗→∗(z1，(z2，z）=z1在g1设h1=dup2（y1，(z2，z）=z1在g1设h1=dup2i(z1，(z2，z）=z1在第二（integralSF介绍一下设iy1=（（），1）(z1，in second（integralSF设iz1=（1，1）h1在第二（integralSF设i在第二（integralSF