理论计算机科学电子笔记153（2006）37-54www.elsevier.com/locate/entcs同步数据流模式匹配1Gr'egoireHamon2计算机科学系，查尔姆斯理工大学，瑞典哥德堡摘要我们在同步数据流语言中引入了变体类型和模式匹配操作。这些语言用于反应式系统的设计。随着这些系统变得越来越复杂，对抽象机制的需求，特别是数据和控制结构，是至关重要的。变量类型提供了一种精确地对结构化数据建模的机制。被定义为时钟操作符的模式匹配操作提供了有效的控制结构。关键词：同步语言，数据流，模式匹配，归纳类型，时钟演算，控制结构，数据结构1介绍反应式系统[1]是需要与其环境持续交互的系统，并以环境所施加的速度这样的系统随处可见，而且数量还在不断增加：线控系统、手机、洗衣机等。除了它们的数量，它们的复杂性也在急剧增加。面对这种日益增加的复杂性，设计人员需要有效的抽象机制，使反应式系统的实现和认证更加容易。我们感兴趣的是扩展同步数据流语言的数据和控制结构。为此，我们建议增加一个变体，1本材料是基于美国国家科学基金会通过伊利诺斯2电子邮件：hamon@cs.chalmers.se1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.02438G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37类型和模式匹配，函数式语言的两个关键特性变量类型允许结构化数据的精确定义模式匹配被定义为控制结构。1.1同步数据流语言同步数据流语言专门用于设计反应式系统。它们结合了同步方法和数据流编程。同步方法[2]假设系统对任何刺激都是即时这允许系统的并发和确定性描述数据流语言是无限流上的函数式语言结合这两种方法允许有效的描述反应系统的连续行为，在大多数控制系统，TEMS。同步数据流语言包括LUSTRE[3]及其工业对应物SCADE，SIGNAL[4]（严格地说，SIGNAL不是函数的，而是关系的）和LUCID SYNCHRONE[5]。1.2对数据结构同步数据流语言不支持广泛的数据类型。LUSTRE支持基本类型（布尔、整数、浮点数）和一些形式的数组，SAGA[6]引入了命名记录。其他数据结构必须从宿主语言导入。然后，需要用这种宿主语言编写的访问函数来操作数据。这使得编写程序变得困难，因为结构的组件不能直接访问。此外，程序认证由于需要检查宿主语言的属性而变得复杂随着系统复杂性的增加，对更复杂的数据结构的需求变得至关重要。像SCADE这样的同步数据流语言的工业用户表示需要定义和使用自己的数据类型。1.3需要控制结构同步数据流语言非常适合表示连续对象。然而，用一组方程来表达连续或演化的行为是相当具有挑战性的。为了设计真正的进化系统，像ESTEREL这样的命令式同步语言更适合。这个问题仍然悬而未决的系统描述为一个组成的几个连续的被访者。一些作品已经考虑了形式主义的组合（LUSTRE和ESTEREL，LUSTRE和ARGOS[7]，Synchronous Ei Eidel和SynchronieG. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）3739[8] ， Ptolemy [9] ） 。 ESTEREL 的 最 新 发 展 扩 展 了 带 有 方 程 的 语 言（ESTERELv7）。另一种可能性是用控制结构扩展SCADE提供了条件激活，Mode- Automata [10]在LUSTRE上添加了自动机作为控制结构。这些添加并不能很好地与语言的其余部分混合，例如模式自动机必须考虑LUSTRE的子集。1.4时钟作为控制结构数据流同步语言提供了一种通过时钟机制激活/去激活程序某些部分的方法。时钟表示表达式的速度，可以使用特殊运算符指定。处理以不同速度发展的表达式可能会引入不一致性。为了避免它们，使用称为时钟演算的静态分析。时钟提供了一种语义清晰的方式来建模以不同速度演化的并发进程它们也被编译器（SIGNAL，RELUC[11]和LUCID SYNCHRONE）用来生成高效的代码。尽管如此，使用时钟来表达控制已被证明是困难的，该机制使用起来很复杂。LUCIDSYNCHRONE语言的工作表明，时钟演算可以被定义为一个接近ML类型系统的类型系统[12，13]。ML已经展示了将强大的类型系统和易用性结合起来的可能性Lucid S ynchrone的我们通过定义与变体类型相关的模式匹配操作来研究这个问题1.5计划在第2节中，我们介绍了时间变量和模式匹配操作使用的例子。这些想法在第3节中正式化。第4节研究汇编问题。在第5节中，我们比较了我们的方法与相关的作品，并讨论了使用时钟结构的程序的选择。2时间变量和模式匹配2.1将变体提升到流中数据流语言中的简单类型是通过提升标量类型构建的：整数流是由整数组成的流同样，变量类型可以40G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37可以自然地定义：变量流是由来自相应标量变量类型的值组成的流。2.1.1第一个例子我们考虑一个程序，它将鼠标事件作为输入，并根据此输入进行计数可以接收三个不同的事件：左击、中击或右击。这个信息可以被编码为一个整数或一对布尔值;然而，创建一个变体类型更可读，更不容易出错类型event =左|中间|权这种类型的值是一个流，随着时间的推移而发展：左左权中间权...我们实现了一个计数器，在左键单击时增加，右键单击时减少，中键单击时重新开始：letup_down mouse = count whererec count = 0->匹配鼠标与| 当c + 1时，在c=>（前计数）时 向 左| 中间=>0| 当c - 1时，在c=>（预计数）上向右函数up down接受一个event类型的参数mouse。它定义了一个值计数，这是一个流。它的第一个值是0，后面是（如->运算符所示）匹配表达式定义的值匹配区分鼠标的可能值。单击鼠标左键，它返回计数器的前一个值（预先计数），增加1，单击鼠标中键为0，单击鼠标右键，它减少计数器。when操作符用于过滤流。在这里，pre count在每个时刻都产生一个值，我们在每个分支中过滤它，以便仅在分支被采用时返回一个值一个可能该程序的执行是：e中左左右左...向上向下E01212...G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37412.1.2带参数的构造函数可以携带参数。我们添加了一个Key事件，每当用户按下数字键盘上的一个键时就会发生。此事件携带一个整数值：类型event =左|权|中间|int的键我们可以使用键盘改变计数器的步长letup_downevent = count whererec count，step =（0，1）->匹配事件| 在c=>（（前计数）+步骤，前步骤）时向左c| 当c=>0时，（步骤前）中间| 当c=>（（precount）-step，prestep）时，| c上的键i=>（预计数）当c，i此程序的一个可能执行是：e中间左关键3 左权...向上向下E01140...在这两个例子中，使用变量和模式匹配操作符是编写程序的一种明确方法。如果没有这些功能，事件将不得不编码为整数或布尔值，或者从宿主语言导入。我们的解决方案给出了一个更简单的程序，更接近程序的规范2.1.3递归类型递归类型很有趣，并且主要用于泛型语言。然而，它们与递归函数相关联，由于同步原因，同步数据流语言不支持递归函数。我们这里不考虑这种类型。2.2时钟和模式匹配我们现在详细描述模式匹配操作的时钟这使得我们可以使用这种结构作为一种控制结构。42G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）372.2.1每个分支变体流可以被看作是互补流的组合在这个例子中，e是四个流的组成e中向左键3向左向右.左左左...中间...对...钥匙3...这些流由模式定义：在我们的示例中，每个流对应一个它们也有互补的时钟：在每一个时刻，它们中只有一个是存在的。因此，模式匹配的每个分支都定义了一个时钟，即分支时钟，只有当分支被采用时，它才是真的。在模式Keyi中，只有当事件的形式为Key时，才定义变量i*：i的时钟是分支时钟。这些分支时钟有着有趣的产品特性：• 它们都是匹配元素（这里是E）的时钟的子时钟：如果该元素不存在，则所有分支都不存在。• 它们是排他的：在每个时刻只采用一个分支这种排他性是模式匹配操作的一个属性，通常，如果模式本身不是排他性的，则使用第一个匹配参数的模式• 它们是互补的：在每个时刻，如果过滤的元素存在，则将存在一个分支（我们强制模式匹配完成）。对于定义控制结构的模式匹配，我们要求与每个分支关联的代码位于相应的分支时钟上：它是“存在”的，因此只有当分支时钟为真时才该构造将所有分支的结果组合在一起。例如：type number = int的Int|浮动letfloat_of_number n =match n with| Inti=>float i| Floatf=>f类型编号有两个构造函数，Int和Float。该函数将数字转换为浮点数。假设n有时钟cl：G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）3743• 分支Inti定义时钟c1，i在c1上的时钟cl上。表达浮点i在时钟C1上，在C1上。• 分支Float f定义时钟c2，f在c2上的时钟cl上。表达F在C2上的时钟C1上。此外，我们在c1和c2上有以下性质：c1c2=假c1c2=cl由于这些属性，作为分支的组合的模式匹配的结果被唯一地定义并且在时钟cl上。2.2.2分支时钟在我们的示例中，我们使用on模式构建匹配事件...| （键i）在c=>（预计数）时，c，i此名称用于抽样预计数。否则，它的时钟会比分支本身更快，因为count本身更快（是匹配的结果）。我们可能想让这种机制隐式化：命名分支时钟是对分支表达式的自由变量进行采样所必需的我们可以用分支时钟系统地（隐式地）采样所有自由变量然而，这样做，我们失去了一些表现力，下面两个表达式：pre（x whenc）(pre x）当c是不等价的。使用隐式过滤机制，我们只能定义第一个（即表达式pre x，其中x被隐式过滤对应于表达式pre（x when c））。更一般地说，隐式机制虽然允许更轻量级的语法，但只允许过滤变量而不是子表达式。构造本身可以用来对表达式进行采样匹配事件，（预先计数），...| （Keyi），pc=>（pc，i）通过过滤pre count并让它用一个平凡的模式匹配每个分支，我们得到一个变量pc，它位于分支时钟上，具有预期的44G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37值这里不需要命名机制然而，当要过滤的子表达式的数量增加时，该解决方案显然不能缩放3形式化我们通过考虑流上的小函数语言来形式化这些想法，并使用变体类型和模式匹配来丰富它。 然后，我们给它一个语义和时钟演算。前面的例子可以非常简单地翻译成这个核心语言。3.1核心语言核心语言包含的表达式要么是常量c（提升到流的标量常量或函数的定义），要么是变量x，要么是标量运算符op的应用，要么是fby的应用（->和pre是从这里定义的），when，whenot，要么是merge运算符。定义associate名称到表达式、函数应用程序或时钟，并且可以并发（AND）或顺序（IN）组合。主程序是一个x形式的定义d，其中D在声明D中返回x的值。e：：= c |X |op（e，e）|c fby e|当eD：：= D和D|DinD|X = e|x = e（e）c ：：= i|有趣的x。ywithDd：：=xwithDi：：= true|法阿尔塞|0|......这是什么？操作：：=+|......这是什么？这种语言被赋予了一种操作语义，表达程序如何在瞬间与其环境交互。这种语义是由以下形式的规则组成的：vJRJJvJRe →eRD→DRd→d其中R在将值与变量相关联的环境中。值v可以是常量，也可以是“不存在”的特殊值（注[]）。规则表达了这样的事实，即在环境R中，表达式e（resp.一个声明D，一个定义d）在表达式eJ（resp.一个声明DJ，一个定义dJ），并产生值v（分别为新环境RJ，G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）3745值v）。我们在这里不详细说明规则，它们在附录A中给出。这个语义的完整描述可以在[14]中找到语义是部分的：非同步程序没有语义（例如，x+y只有在x和y都存在或都不存在时才被定义）。确保程序是同步的是通过时钟演算静态完成这个时钟演算被定义为一个类型系统。时钟的语言如下：σ：：= σα1，.，αm。第一，... K k.cln，m，k ∈ IN cl：：= cl→cl|S|（k：s）s：：=base|sonk|αk：：=x|K时钟是功能时钟C1→C1、流时钟S或从属时钟（k：s）。流时钟是基本时钟基，k上的子时钟s，或时钟变量α。依赖项k要么是一个名字x（由letclock定义），要么是一个依赖变量K。我们也有时钟方案σ。时钟演算由形式的谓词定义He：clHD：HJHd：cl说明在时钟环境H中，将时钟与变量相关联，表达式e（resp.一个声明D，一个定义d）具有时钟cl（resp.定义时钟环境HJ，有时钟cl）。这些规则载于附录B。这个时钟演算的完整描述可以在[14]中找到3.2添加变体和模式匹配3.2.1扩展语言该语言扩展了变量类型声明。它们具有以下形式：类型（α1，...，α m）t = τ 1的C1|......这是什么？| C nof τnα1，... α m是t，C1，.的类型参数， C n是类型t，τ1，.的构造函数，τ n是构造函数的参数。如果F（u）是自由变量的集合，F（τi）∈{α1，. ，αn}。我们不能接受递归类型i。t∈/F（τi）。这样的声明用类型t的表达式和模式扩展了语言。模式匹配操作是一个声明，其中分支-46G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37C-[]Re →e[]CJR e→sveJC（e）→C（eJ）[]我我R/C（e） →C（eJ）Ci（sv）我我Fig. 1. 模式归约规则clock被命名（在具体语法中，如示例中所示，名称可以省略），与每个分支相关联的代码是一个定义：e：：=. |......这是什么？|... |C n (e)P：：= c |X |C1（P）|......这是什么？ |Cn（P）x=匹配eD：：=. || P on x ⇒ d...| Ponxx3.2.2语义操作语义被扩展到处理具有构造函数和模式匹配的表达式。瞬时值，在常量或不存在（[]）的情况下，需要使用应用于常量参数的构造函数进行扩展sv：：= c |C1（sv）|......这是什么？ |C n（sv）v：：=sv|[客户端]构造函数不能应用于[]。构造表达式的归约规则如图1所示。它们是同步的：当且仅当其参数不存在时，表达式返回不存在模式匹配的约简规则如图2所示。它们遵循建议的行为：• 如果过滤表达式不存在（规则匹配-[]）：所有分支时钟都是false（ci取F值），所有分支都不存在，结果不存在。• 否则（规则匹配）：对应于过滤表达式的分支时钟的分支G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）3747匹配-[]R，[[]/x]e→e[]Ji ∈ {1，.，n} R，[[]/x]，[[]/x i]，[F/c i] di→ di[]Jx=匹配ex =匹配eJ与R| P (x ) on c ⇒ d1 11 1[[]/x]→| P (x ) on c ⇒ dJ1 111......| P (x ) on c ⇒ dn nn n| P (x ) on c ⇒dJn nnn匹配R，[v/x]e→ePj（vj）JR，[v/x]，[v/x]，[T/c]Δd→vJ JJ JDJ Ji∈{1，. ，n}such_h_h_i=h_j，x=匹配eR，[v/x]，[[]/xi]，[F/ci]→dix =匹配eJ与[]JR| P (x ) on c ⇒ d1 11 1[v/x]→| P (x ) on c ⇒ dJ1 111......| P (x ) on c ⇒ dn nn n| P (x ) on c ⇒dJn nnn图二. 模式匹配3.2.3时钟演算新规则见图3。构造表达式有其参数的时钟在模式匹配中，每个分支都在其分支时钟上：在分支Pioncidi中，如果滤波表达式在时钟cl上，则di必须在时钟clonci上。我们通过禁止分支时钟出现在时钟环境中来限制分支时钟的范围。 这种限制不是强制的，但使模式匹配更接近控制结构。整个表达式的时钟是匹配表达式的时钟。时钟演算扩展的时钟演算已经被证明是正确的关于扩展的语义：任何时钟良好的程序在这个演算评估的扩展语义。该证明类似于核心语言的时钟演算的正确性证明，只是需要考虑新的情况完整的证明在[14]（第80页）中给出48G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37C-HHe：sH2OC（e）：s匹配-HH，[x：cl]电子：cli ∈ {1，.， n}：H，Hi P i：cl on c iH，Hi，[x：cl] d i：cl onc iHci∈/fvcl（H），Dom（Hi）=fvPix=匹配e| P1在C1上，D1上 ：[x：cl]...| P nonc n d n图三. 扩展时钟演算4汇编问题我们的目标是使用模式匹配操作作为控制结构。因此，有效地编制这一结构是很重要的在传统语言中编译模式匹配是一个已知的问题[15]。为了编译我们的结构，我们将其翻译成目标语言中的类似结构（在我们的例子中，OCAML[16]）。对于简单的例子，分支中的所有子表达式都在分支时钟上，编译很简单：程序可以按原样翻译。然而，如果一些子表达式不在其分支时钟上，则转换并不简单：使v与…相配| trueonc=>letrec nat= 0fby（nat+1）in(nat当c）| 返回0当c在c上的分支时钟cl上时，nat（其中cl是v的时钟）。因此，nat及其定义是在时钟cl上，它比分支快钟：我们该程序相当于以下程序：令recnat= 0 fby（nat+ 1）匹配v，G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）3749| trueonc=>natwhen c| 返回0nat是在建筑之外定义的。分支内部发生的所有计算都在分支时钟上，匹配可以按原样编译重写由编译器自动完成，使用表情不幸的是，这并不总是足够的：使v与…相配| trueonc=>letrec nat= 0fby（nat+1）inletx =（merge c nat 0）in（xwhenc）| 返回0如果v有时钟cl;x，当c在分支时钟上时（cl在c上），x在时钟cl上（比分支时钟快），nat在分支时钟上。像以前一样，x的定义需要移到结构之外。然而，计算之间的依赖关系（x当c依赖于x时，x依赖于nat，这使得它很难。此程序相当于以下程序：设nat，c =匹配c，| true=>letrec nat= 0fby（nat+1）innat，true| false=>0，false in设x = merge c（natwhen c）0inmatch v with| true=> x当c| 返回0时钟和依赖性都得到尊重，分支中的每个表达式都在其分支时钟上。然而，程序的结构并没有被翻译所保持这违背了建筑作为控制结构的想法该实现将match的使用限制在不需要这种重写的程序中。5结论我们已经介绍了在同步数据流语言中添加变量类型和模式匹配。变体的增加提出了对这些语言中数据结构需求的回答。它们允许结构化数据的高效和清晰的表示模式匹配的相关操作提供了同步数据流语言中的控制结构50G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）375.1相关作品数据流语言中的数据类型很少有人关注，大多数语言都通过抽象运算符提供对宿主语言类型的访问直接在语言中支持自定义数据类型和相关的控制使用ab-bandwidth运算符需要使用两种不同的语言，并且在需要基于数据类型的控制结构时需要进行一些编码语言中控制结构的定义与模态自动机的工作有关，更一般地说，与形式主义的组合有关。模态自动机通过在L ustre之上提供一个控制结构（自动机）来回答形式主义的组合问题。 有了这种结构，具有多个连续行为的系统可以被有效地定义和编译。 我们在这里遵循类似的方法，在语言中提供一个控制结构。然而，match结构在这里是语言的一部分，并且可以顺利地集成到语言中。模式自动机中对语言的限制（没有时钟，没有函数，pre只对变量）是不必要的。这种平滑的集成是通过使用时钟来定义控制。在[17]中，提出了一种模式自动机在LUCID SYNCHRONE中的编码。使用变体类型和模式匹配使这种编码更简单，更容易理解。匹配构造的使用允许编译器产生高效的代码，自动机的每个模式对应于模式匹配操作的一个分支。5.2改编这里介绍的变量类型和模式匹配在当前版本的LUCIDSYNCHRONE编译器中实现按照同样的思路，我们可以想象不同的结构。出现在分支中的自由变量可以隐式过滤，如2.2.2节所讨论的。编译问题消失了：在这种情况下，分支子表达式不能比分支快。SCADE编译器的实验版本RELUC[11]支持类似的构造，仅限于枚举类型（没有参数的构造函数）。我们由于编译问题4而施加的限制并没有被施加。该构造可以被编译为宿主语言中的几个控制结构这种构造用于在语言中对自动机进行建模。G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37515.3从函数式到同步数据流语言这一增加表明，同步数据流语言可以从为函数式语言开发的结构中受益。它还表明，即使时钟演算是一种复杂的机制，基于它的构造也很容易使用。时钟演算是必不可少的，它允许以安全的方式描述以不同速度演化的并发进程。虽然直接使用它来定义控制是困难的，但它可以通过专门的结构更容易“时钟作为类型”的观点允许推理和良好的诊断，这在定义这种结构时是必不可少的就像ML中的类型系统对程序员是一种帮助而不是负担一样，时钟演算在组合并发进程时必须是一种帮助6确认作者要感谢Marc Pouzet和Jean-Louis Colaco对这项工作的建议，以及Carmella Schaecher的深刻评论。匿名审稿人对改进这篇论文有很大帮助。引用[1] 哈雷尔，D.，Pnueli，A.：关于反应系统的发展。并发系统的逻辑和模型，NATO AdvancedStudy Institute on Logics and Models for Verification and Specification of Concurrent Systems，Springer Verlag（1985）[2] Halbwachs，N.： 反应系统的同步编程。 Kluwer Academic Pub.（一九九三年）[3] Halbwachs，N.，Caspi，P.，Raymond，P.，Pilaud，D.：同步数据流编程语言光彩照人。IEEE会议录79（1991）1305[4] 一本杂志，P。，Bes n ard，L. ，G u ernic，P. L. ：对我们的语言信号进行动态同步的改进。在：编程语言设计和实现会议，加利福尼亚州拉霍亚（1995年）163[5] Caspi，P.，Pouzet，M.：Lustre的功能 在马萨诸塞州奥贡， Ashcroft，E.A.， 编辑：有意编程语言国际研讨会，悉尼，澳大利亚，世界科学（1995年）[6] Bergerand，J.L.，Pilaud，E.：自动控制可靠性软件开发环境。In：SAFECOMP '88，PergamonPress（1988）[7] Maraninchi，F.： Argos语言：自动机的图形表示和反应系统的描述。在：IEEE视觉语言研讨会，神户，日本（1991年）[8] Poign'e，A. ，M. ，Ma eiss，O. ，Holend er sk i，L. 、Budd e、R. ：TheSyncronousAprochtoDesigning Reactive Systems.系统设计中的形式化方法12（1998）163-187[9] Girault，A.，李，B.，Lee，E.A.：具有多个并发模型的分层有限状态机。IEEE Transactions OnComputer-Aided Design Of Integrated Circuits And Systems18（1999）52G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37[10] Mar an in c h i，F. ，R′emon d，Y. ：Mo d e-automata：针对活动系统的数据库和状态。In：European Symposium On Programming，Lisbon（Portugal），Springer-Verlag（1998）[11] Colaco，J.L.：（个人通信）[12] Caspi ， P. ， Pouzet ， M. ： 同 步 卡 恩 网 络 。 ACM SIGPLAN International Conference onFunctional Programming，Philadelphia，Pennsylvania（1996）[13] 可乐，J。L. ，Pou zet，M. ：Clocksasfr stclasab st racty pes. 在：ACMSIGPLANINTR NAIONAL会议上，关于嵌入式软件。计算机科学讲义第2855Springer-Verlag（2003）134[14] 早上好，G。：计算的时间表将被重新定义为L u c id S y n c h r o n e e，而非常规的时间表将被重新定义为S y n c h r o n e `a M L。PhDthesis，UniversiteParis6（2002）[15] Le Fessant，F.，Maranget，L.：优化模式匹配。2001年函数式编程国际会议论文集，ACM出版社（2001年）[16] Leroy，X.：Objective Caml系统版本3.07文档和用户手册。 技术报告，INRIA（2003年）[17] Hamon，G.，Pouzet，M.：同步数据流程序的模块化复位.在：ACM声明式编程原则和实践国际会议（PPDPA操作语义学操作-[]IM-[][]Rc →cIMR→ccOP拉紧R，[v/x]x→vx[]J[]Jc1Jc2JRe1→ e1Re2→ e2Re1→e1 R→E c=op（c1，c2）[]JJR op（e， e）→cop（eJ，eJ）Rop（e1，e2）→op（e1，e2）1 21 2FBY-[][]JFBYcJJRe →eRe →e[]JR cfbye→ccJfbyeJRcfbye →cfbye当-[][]J[]J当-TCJ真JRe1→e1Re2→e2R1→R2→R3→e2[]JJR ewhene→ceJwheneJ当e2时R →e1当e21 21 2当-FR e→ceJ雷假J112 →e2[]J J当e2时R →e1当e2G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）3753→x=eJ在R1JR2J和R1JR2JR <$D1→D1R，R1<$D2→D2R，R2<$D1→D1R，R1<$D2→D2R2J JR1，R2J JR在D2中的D 1 →D2中的DR/D1和D2→d1和d2DECL-ER，[v/x]ve→veJDEFRJ R，RJx→vxRx=[v/x]JRD→DR x，hD→vx与DJDECL-应用程序R，[v/y]有趣的x。z与D→fR，[v/y]（x=eandD）iny=zRJ，[v/y]→D[v/y]Ry=f（e） →DB时钟演算IM-HHi：α.αABS-HH，[x：cl1]C3D：H0genH（H0）C3y：cl2Hubfunx. y与D：cl1→cl2OP-H时间1：s时间2：sH_∞（e1，e2）：FBY-H时间1：s时间2：s上一页下一页尾页当-HHe1：sHe2：（K：s）当e2：s在K上时，H =e1eJJJ54G. Hamon/Electronic Notes in Theoretical Computer Science 153（2006）37INST-Hcl=inst（σ）H，[K：σ]K：clDECL-E-HH，[x：cl]电子：clHx=e：[x：cl]DECL-APP -HH，[x：cl1]Rf：cl2→cl1H，[x：cl1]Rf：cl2Hx=f（e）：[x：cl1]和-HH，H2D1：H1H，H1D2：H2HD1和D2：H1，H2IN-HHD1：H1H，genH（H1）D2：H2HD1 在D2：H2DEF-HHD：H0H，genH（H0）x：cl带D的H x：cl
我的内容管理
展开
