EVL：一种处理通用事件的高阶函数语言 桑德拉阿尔维斯，Maribel Fernandez，米格尔·拉莫斯.

可在www.sciencedirect.com在线获取理论计算机科学电子笔记351（2020）3-23www.elsevier.com/locate/entcsEVL：一种类型化的高阶事件函数语言桑德拉阿尔维斯1DCC-FCUP裂纹波尔图大学，葡萄牙Maribel Fernandez2部 信息学伦敦大学国王米格尔·拉莫斯3DCC-FCUP裂纹波尔图大学，葡萄牙摘要我们定义了EVL，一种用于处理通用事件的最小高阶函数语言。概念通用事件的概念扩展了传统上用于各种领域的众所周知的事件概念，例如数据库管理，并发性，反应式系统和网络安全。 引入了通用事件在元模型的上下文中处理访问控制系统中的义务。事件规范被表示为记录，我们使用多态记录类型在我们的语言中输入事件。我们展示了如何在复杂事件处理（CEP）的背景下使用EVL的高阶功能，以定义处理通常CEP技术的高阶参数化函数。保留字：事件、访问控制、义务、记录类型。1介绍在当今动作的发生或事件称为事件，处理事件流的技术称为复杂事件1电子邮件：sandra@fc.up.pt2电子邮件：maribel. kcl.ac.uk3电子邮件：jmiguelsramos@gmail.comhttps://doi.org/10.1016/j.entcs.2020.08.0021571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。4S. Alves等人/理论计算机科学电子笔记351（2020）3处理（CEP），已经存在了几十年[6，23，15]。大多数CEP系统专注于现实生活中的应用，因此投资于可扩展性，容错性，分布等问题，但往往缺乏正式的语义，使它们难以理解，扩展或概括。在安全的上下文中，特别是在建模访问控制时，通常情况下，授予或拒绝对某些资源的访问取决于特定事件的发生[7，21，8]。这在处理义务的访问控制系统中甚至更为关键，其中特定义务的状态通常根据系统中的事件发生来定义，并且处理义务的几个模型基于类别的访问控制和义务元模型（CBACO [2]）定义了基于泛型关系的义务概念的公理化，以类型化事件并提取事件间隔。该模型中的一个关键概念是区分事件方案和特定事件，事件方案提供了对特定系统中可能发生的事件类型的一般描述，特定事件描述了已经发生的实际事件。请注意，事件可以采取各种形式，这取决于所考虑的系统（例如，通过网络交换的消息，系统用户执行的操作，物理现象的发生，如磁盘错误或火灾警报等）。为了以统一的方式处理事件分类，Alves et. [1]定义了一种基于事件的通用术语语言。在这种语言中，事件被表示为类型化术语，由用户定义的签名构建，即特定于所建模系统的特定类型化函数符号集。使用这种方法，可以定义通用函数来实现事件类型并计算事件间隔，而无需知道事件的确切类型在这种情况下，复合事件[1]链接了一组可能在历史中单独发生的事件，但应被识别为单个事件的发生。为了简单起见，在[1]中，复合事件被假定为历史中的单个事件，为将来的工作留下了对复合事件更详细和更现实的处理。复合或复合事件的概念也是CEP系统的一个关键特征，CEP系统非常强调检测输入事件流的复杂模式并建立排序和排序关系的能力。[1]中使用类型不仅是为了确保表示事件的术语尊重所研究系统的特定类型签名，而且还正式定义了事件实例化的概念，通过子类型的隐式概念将特定事件与通用事件相关联，受到Ohori多态记录类型系统的启发由于类型化记录的隐式子类型规则，[1]中定义的系统允许对事件指定进行类型检查，但不能处理事件指定的大多数一般类型在本文中，我们进一步定义了EVL，一种高阶多态类型语言，旨在促进事件的指定和处理。我们的语言既是Ohori的多态记录演算的限制，也是它的扩展事件处理系统中传统使用的语言S. Alves等人/理论计算机科学电子笔记351（2020）35--L通常是从关系语言，特别是关系代数和SQL，扩展了额外的ad-hoc操作符，以更好地支持信息流或命令式编程。本文探讨了在这种情况下，无论是在类型系统的水平，以及探索语言的高阶能力的功能范式的潜力。本文的主要贡献是：• EVL的设计：一种用于事件处理的高阶类型多态记录演算。我们的目标是有一个最小的语言，但这是表达足以指定和操纵事件。• EVL的一个可靠而完整的类型推理算法，定义为[24]中ML风格记录演算的扩展和限制• 全面研究EVL高阶/功能能力及其在CEP背景概述在第2节中，我们定义了EVL语言及其类型集。在第3节中，我们定义了EVL的类型系统，在第4节中，我们给出了一个类型推理算法，该算法被证明是可靠和完备的。在第5节中，我们将讨论CEP，并探讨EVL我们将在第6节讨论相关工作，最后在第7节总结并讨论进一步的工作。2EVL类型化语言在本节中，我们将介绍EVL，一种用于指定事件的最小类型语言EVL是λ演算的扩展，它包括记录，一种灵活的数据结构，用于处理[1]中定义的事件规范 更确切地说，事件规范是一个标记结构（或记录），其形式为l1=v1，.，l n=v n，表示一组标签l1，.，l n，具有相关联的值v1，...，v;我们假设对λ-演算有一定的了解（详细参考见[5]2.1方面我们首先正式定义EVL术语集。在下文中，令x，y，z，. . . 在一个可数的变量集上的范围和l，l1，. 在可数的标签集上的范围。定义2.1EVL项的集合由以下语法给出：M：：=x|MM| λx.M|如果M则M else M设x=M，在M中|letEv x=M in M{1=M，...，l=M}| M.L|modify（M，l，M）记法：我们将使用记法let x x1. xn=M，且letEv x x1. X n=M对于令x=λx1.λx n.M和令Ev x=λx1.λx n. M。 作为6S. Alves等人/理论计算机科学电子笔记351（2020）3--在示例中，我们将为函数、标签和事件使用更有意义的名称。此外，事件名称将始终以大写字母开头，以帮助将它们与函数区分开来。我们选择不向语言中添加其他可能有用的构造函数，例如pairs和projects，因为我们的目标是最小化语言。尽管如此，我们可以很容易地编码对（M1，M2）和投影π1M和π2M在我们的语言通过记录的形式fst =M1，snd =M2和M。fst，M. 然后，分别这可以简单地扩展到一般的元组，我们在编写示例时经常使用这种表示法示例2.2在这个简单的示例中，FireDanger报告特定位置的火灾危险级别。设Ev FireDanger=λ lλ d。{location= l，fire_danger= d}在火灾危险“波尔图““低“为了使我们的例子更可读，我们还将使用以下术语，缩写列表结构：n i l = {empty = true}缺点xl i st = {empty = f a l s e，head = x，ta i l = l i st}。请注意，与元组的情况非常相似，这种表示法中特定列表的类型将与所讨论的列表的大小密切相关。一个更现实的方法是在语言中添加列表和列表类型作为原始概念，但是，正如我们之前提到的，我们专注于最小语言。此外，在我们的示例中，我们经常使用常量（数字，布尔值，字符串等）和运算符然而，遵循最简方法，我们不向语法中添加常量/运算符，而是使用自由变量来表示它们。同样，在更一般的方法中，我们可以用其他数据结构和运算符来扩展语法，如数字、布尔值、列表等。例2.3考虑以下示例，该示例说明了通用事件FireDanger的定义和函数检查，该函数检查使用与特定位置相关的天气信息来确定该位置是否存在火灾爆发的危险。函数检查创建一个适当的FireDanger实例，以报告适当的火灾危险级别。让Ev火灾危险LD = {location =我，火灾危险 =d}在L e t中，检查x= i f（x .温度>29和x .风力>32和x .湿度20和x . p沉淀50），然后火灾危险x。位置“高”e l s e火灾危险X . 位置“低“在检查中{温度=10，风=20，湿度=30，前峰 =十、位置=“波尔图“}2.2类型我们现在定义类型的集合，以及EVL语言的类型系统。 我们使用记录类型来类型标记的结构以下OhoriS. Alves等人/理论计算机科学电子笔记351（2020）37∀我们的优势联系我们U}{}∈{形态记录类型[24]。这扩展了Damas和Milner [ 13 ]的参数多态的标准类型系统。在Ohori的系统中，多态类型由形式为α：：κ.σ的类型模式定义，其中类型变量α被限制为一组称为kind的类型κ。我们假设一个常数ty pes的有限集合B和一个type变量的连续表集合V，我们将使用b，b1， . . . ，α，α1， . . 以及κ，κ1，. 分别表示常量类型、类型变量和种类。常量类型的集合B将始终包含类型bool。定义2.4类型σ和种类κ的集合由下面的文法指定。σ：：= τ |α：：κ.στ：：= α|B|τ→τ|{1：τ，...，l：τ}ρ：：= α|B|τ→ ργ：：= τ→ {1：ρ，.，l：ρ}|{1：ρ，.，l：ρ}κ：：= U |{{1：τ，.，l：τ}}根据Damas和Milner更确切地说，σ代表所有类型，τ代表所有单型。 我们用ρ（包含在τ中）表示事件场的类型，用γ（也包含在τ中）表示事件定义的类型。 这种区分对于充分地键入事件定义是必要的，并且其目的将在类型系统的定义中变得清楚我们用的是表示每一种可能的类型，以及类型l1：τ1，.，l n：τ n表示至少包含字段l1，.，ln，具有类型τ1，.，τ n，分别。我们不允许嵌套事件，为此，我们明确区分了事件定义的类型，用γ表示，它们是用τ表示的一般类型的子集。但是，我们允许一般类型的嵌套记录。下面是一个使用嵌套记录类型键入的术语{empty = f a l s e，head = 1，t a i l = {空= f a l s e，head = 2，t a i l = {empty = t r u e}。设F在函数上的范围是从有限个标签集到类型。我们写{F}，{{F}}分别表示由F标识的记录类型和由F标识的记录种类对于两个函数F1和F2，我们将函数F写成F1±F2，使得dom（F）=dom（F1）≠dom（F2），并且使得对于l∈dom（F），如果l∈dom（F1），则F（l）=F1（l）;否则F（l）=F2（l）。记法：按照上面介绍的对的记法，我们写为（σ1×σ2）对于对应于{fst：σ1，snd：σ2}的产品类型。类型化环境Γ是一组语句x：σ，其中所有主体x都是不同的。我们写dom（Γ）来表示类型化环境Γ=x1：σ1，.的域，xn：σ n，这是集合x1，.，x n. 变量的类型x idom（Γ）是Γ（xi）=σ i，我们写Γx来表示Γx：Γ（x）. 亲切的环境K是一组语句α：：κ。 同样地，一个友善的环境K={α1：：κ1，.，α n：：κ n}，记为dom（K），是集合{α1，...，α n}和当αi∈dom（K）时，K（α i）=κ i. 出现在类型/种类中的类型变量α8S. Alves等人/理论计算机科学电子笔记351（2020）3∀∀ ∈⊆∀ ∈⊆⊆⊆ ∈⊆∈是有界的，如果它发生在α上的-quantifier的范围内，否则它是自由的。我们用FTV（σ）（FTV（κ））表示σ（分别为κ）的自由变量集。我们说，一个类型σ和一个种类κ在一个kinding环境K下是良构的，如果FTV（σ）dom（K）和FTV（κ）dom（K）。一个类型环境Γ在一个类环境K下是良构的，如果xdom（Γ），Γ（x）在K下是良构的.如果α dom（K），FTV（K（α））dom（K），则Kinding环境K是良构的.这反映了这样一个事实，即表达式中的每个自由类型变量都必须受到kinding环境中的一种类型的限制。因此，每个类型变量要么受到类型方案中的类型的限制，要么受到kinding环境中的类型的限制。此外，我们考虑一个类型的本质自由类型变量的集合σ在类环境K下（记为EFTV（K，σ））为最小集合，使得FTV（σ）EFTV（K，σ），如果α EFTV（K，σ），则FTV（K（α））EFTV（K，σ）.这反映了这样一个事实：在kinding环境K下，如果α在σ中自由或在K中的限制中自由，则类型变量α在σ中本质自由。定义2.5设τ为单型，κ为类，K为类环境。然后我们说τ在K下有kindκ（记为KDτ：：κ），如果τ：：κ可以通过应用以下规则获得：KDτ：：U对于所有在K下良构的τKDα：：{{11：τ1，...，l n：τ n}}如果K（α）={{l1：τ1，.，l n：τ n，. }}个文件夹K D {11：τ1，.，l n：τ n，. }：：{{ l1：τ1，.，l n：τ n}}如果{11：τ1，...，l n：τ n，. }在K注意，如果KDσ：：κ，则σ和κ在K下是良构的。例2.6设τ=α1→{l2：int，l3：（α2×α3）}. 然 后 ，τ在K1={α1：：U，α2：：U，α3：：U}下是良构的，因为FTV（τ）是随机的（K1），但在K2={α1：：U，α2：：U}，因为α3dom（K2），因此FTV（τ）/dom（K2）。因为τ在K1下是良构的，我们可以写为K1Dτ：：U。3类型分配我们现在定义如何将类型分配给EVL术语。因为我们正在处理多态类型模式，我们需要定义泛型实例的概念，我们首先需要讨论良构替换。代入S=[σ1/α1， . . . ，σn/αn]在类环境K下是良型的，如果对所有αdom（S），S（α）在K下是良型的. 这反映了这样一个事实，即将替换应用于在kindingenvironmentK下是良构的类型，将导致在K下也是良构的类型。一个类置换是一个类赋值K和一个在K下合式的置换S的对（K，S）。这反映了这样一个事实，即替换S应该只应用于在S下是良构的类型，使得所得到的类型被K类化。S. Alves等人/理论计算机科学电子笔记351（2020）39⊆⊆⊆ ∀∈1n1M1n例3.1设S=[α2/α1]是一个代换。 则dom（S）={α1}，S（α1）=α2，FTV（α2）={α2}。对于K1={α2：：κ}的kinding环境，由于α 2 ∈ dom（K1），我们得到S在K1下是良构的.另一方面，对于kinding环境 K2={α3：：κ}，由于α2/∈ dom（K2），我们得到S在K2下不是良构的.定义3.2我们说一个类代换（K1，S）尊重一个类环境K2，如果<$α∈dom（K2），K1DS（α）：：S（K2（α））.例3.3 设K1={α1： ：{{l1：α2}}， α2： ：U}，S=[{l1：int}/α1]. 然后，限制替换（K1，S）尊重K2={α1：：{{l1：int}，因为对于dom（K2）={α1}，我们有：K1DS（α1）：：S（K2（α1））K1DS（α1）：：S（{{l1：int}}）K1DS（α1）：：{{l1：S（int）}}K1D{l1：int}：：{{l1：int}}引理3.4如果FTV（σ）dom（K）和（K1，S）尊重K，则FTV（S（σ））dom（K1）.证据如果（ K1，S）尊重K，则我们知道<$α∈dom（K）， K1DS（α）：：S（K（α））. 这意味着，如果FTV（σ）dom（K），则αJFTV（σ），K1DS（αJ）：：S（K（αJ））.因此，S（αJ）和S（K（αJ））在K1下都是良好形成的，这意味着FTV（S（αJ））随机（K1）和FTV（S（K（αJ）随机（K1）。因此，现在很容易看出FTV（S（σ））不确定性（K1）。Q引理3.5若KDσ：：κ，且类代换（K1，S）尊重K，则K1D S（σ）：：S（κ）.证据 证明遵循KDσ：：κ Q的定义定 义 3.6 设 σ1 是 kinding 环 境 K 下 的 良 型 。 则 σ2 是 σ1 在 K 下 的 一 般 实 例 （ 记 为KDσ1≥σ2），如果σ1=α1：：κ1· · ·αn：：κ1.τ1，σ2=β1：：κ2· · ·βm：：κ2.τ2，且存在一个替换S使得dom（S）={α1，...，α n}，（K∈{β1：：κ2，.，β m：：κ2}，S）方面1mK{α1：：κ1，.， α n：：κ1}，τ2= S（τ1）。定义3.7设Γ是一个类型环境，τ是一个类型，两者都在一个类型环境K下良构。τ在Γ和K下的闭包（记为Cls（K，Γ， τ））是一对（K J，α1：：κ1· · ·α n：：κn.τ），满足K J∈{α1：：κ1， . . α n：：κ n}= K且{α1，.， α n}= EFTV（K，τ）\EFTV（K，τ）.例3.8设K={α2：：U，α3：：U，α4：：U，α1：：{{ll：α2}，{x：α1}，τ={l1：α2，l4：bool} → {l2：int，l3：（α3×α4）}。然后Cls（K，r， τ）=（{α2：：U，α1：：{{11：α2}，α3：：U. α4：：U. {l1：α2，l4：bool} →{l2：int，l3：（α3×α4）}），因为K={α2：：U，α1：：{{ l1：α2}10S. Alves等人/理论计算机科学电子笔记351（2020）3{α3：：U，α4：：U}，EFTV（K，T）={α2，α3，α4，α1}，EFTV（K，T）={α1，α2}，以及EFTV（K，τ）\EFTV（K，Γ）={α2，α3，α4，α1}\{α1，α2}={α3，α4}.EVL的类型分配系统如图1所示，可以看作是Ohori类型系统对记录类型的限制和扩展与Ohori不同，我们在这个系统中不处理变量类型，但我们有额外的语言构造函数，如条件和显式事件定义。我们使用K，Γ<$M：σ来表示EVL项M具有σ型，分别给定类型和种类环境Γ和K。KDΓ（x）≥τ，Γ在K（Var）K，Γx：τK，ΓM1：τ1→τ2K，ΓM2：τ1（App）K，τM1M2：τ2K，Γx<${x：τ1} <$M：τ2（Abs）K，Γx<$λx.M：τ1→τ2K′，Γx<$M1：τ′Cls（K′，Γx， τ′）=（K，σ）K，Γx<${x：σ} <$M2：τ（Let）K，Γx∈x=M1inM2：τK′，Γx<$M1：γCls（K′，Γx， γ）=（K，σ）K，Γx<${x：σ} <$M2：τ（LetEv）K，Γx，Evx=M1，M2：τK，Γ<$Mi：τi，1≤i≤n（Rec）K，r ={11=M1，...，l n=M n}：{l1：τ1，.，l n：τ n}，n≥ 1K，ΓM：τ′KDτ′：：{{l：τ}}（Sel）K，τ，M.l：τK，ΓM1：τ K，ΓM2：τ′KDτ：：{{l：τ′}}（修改）K，τ_modify（M1，1，M2）：τK，ΓM1：布尔K，ΓM2：τ K，ΓM3：τ（条件）K，rifM1thenM2elseM3：τFig. 1. EVL的类型分配系统例 3.9 设 M={location=l ， fire_danger=d} ， τ1={location ： α1 ，fire_danger：α2}，τ2=α1：：U. τ2：：U.α1→α2→τ1，τ3={location：l型，火险：fd型}，τ4=l型→fd型→τ3，和Γ ={”Porto“：l型，“low“：fd型}。图2给出了M的类型推导。引理3.10若K，Γ <$M：σ且（K1，S）尊重K，则K1，S（Γ）<$M：S（σ）.证据 通过对K的归纳，得到了Γ<$M：σ.QS. Alves等人/理论计算机科学电子笔记351（2020）3113 2type（App）=∀∈⇒1（Var）（Var）{α1：：U，α2：：U}，{l：α1，d：α2}}{α1：：U，α2：：U}，{l：α1，d：α2}}{r}d：α2（Rec）{α1：：U，α2：：U}，{l：α1，d：α2} τrτM：τ1（绝对值）Φ={α1：：U，α2：：U}，{1：α1}<$r <$λd.M：α2→τ1（Abs）{α1：：U，α2：：U}，Γελl.λd.M：α1 →α2 →τ1Φ2=Cls（{α1：：U，α2：：U}，Γ，α1→α2→τ1）=（{}，τ2）（Var）（Var）Φ3={}，{FireDanger：τ2}{FireDanger：τ4}{}，{FireDanger：τ2}{F ire D an g e r：τ 2（应用程序）{}，{FireDanger：τ2}{F ireDangerΦ{}，{FireDanger：τ}火灾危险{}，{FireDanger：τ2} {FireDangerΦ1Φ2Φ4（LetEv）{}，Γ_（？图二、M=letEvF ireDanger=λl.λd.MinFireDanger“P or to o““l o w“的类型推导4EVL的一种类型推理算法我们现在调整Ohori它使用了Robinson统一算法[ 27 ]的改进我们首先讨论EVL类型的类统一。4.1Kinded统一一个类方程组是一个对（K，E），其中K是类环境，E是在K下良构的类型对（τ1，τ2）的集合。一个类代换（K，S）是类方程组（K，E）的一个单位元，如果在E中出现的每个类型都尊重K，并且（τ1，τ2）E，S（τ1）=S（τ2）（S满足E）。一个类代换（K1，S1）是（K，E）的最一般的单位元，如果它是（K，E）的一个单位元，并且如果对于（K，E）的任何其他单位元（K2，S2）有某个代换S3使得（K2，S3）尊重K1并且S2=S3<$S1。类统一算法U（E，K）由图3中的变换规则定义。每个规则的形式为（E1，K1，S1）（E2，K2，S2），其中E1，E2是K1，K2是类环境，S1，S2是替换。经过一个转换步骤后，E2保持类型对的集合被统一，K2指定要验证的类型约束，S2是从E中删除的类型对的统一结果。给定一组方程（K1，E1），算法U（E1，K1）通过应用变换规则到（E1，K1，S），直到没有更多的规则可以应用，导致三元组（E，K，S）。如果E=0，则返回（K，S）对，否则报告失败。例4.1设α1和α2是两个类型变量，K={α1：：{{location：α3}}，Φ412S. Alves等人/理论计算机科学电子笔记351（2020）3关于我们{11221212（E<${（τ，τ）}，K，S）<$（E，K，S）（E<${（α，τ）}，K<${（α，U）}，S）<$（[τ/α]E，[τ/α]K，[τ/α]S<${（α，τ）}）（E<${（τ，α）}，K<${（α，U）}，S）<$（[τ/α]E，[τ/α]K，[τ/α]S<${（α，τ）}）（E <${（α1，α2）}，K <${（α1，{{F1}}），（α2，{{F2}}）}，S）<$（[α2/α1]（E <${（F1（l），F2（l）|l ∈ dom（F1）{dom（F2）}），[α2/α1]（K）<${（α2，[α2/α1]（{{F1±F2}}）}，[α2/α1]（S）<${（α1，α2）}）（E <${（α，{F2}）}，K <${（α，{{F1}}）}，S）<$（[{F2}/α]（E <${（F1（l），F2（l）））|l ∈dom（F1）}），[{F2}/α]（K），[{F2}/α]（S）<${（α，{F2）}）}）若dom（F1）≠dom（F2）且α/∈FTV（{F2}）（E <${（{F2}，α）}，K <${（α，{{F1}}）}，S）<$（[{F2}/α]（E <${（F1（l），F2（l）））|l ∈dom（F1）}），[{F2}/α]（K），[{F2}/α]（S）<${（α，{F2）}）}）若dom（F1）≠dom（F2）且α/∈FTV（{F2}）（E <${（{F1}，{F2}）}，K，S）<$（E <${（F1（l），F2（l））|l ∈ dom（F1）}，K，S）如果dom（F1）=dom（F2）（E<${（τ1→τ2，τ1→τ2}，K，S）<$（E<${（τ1，τ1），（τ2，τ2）}，K，S）图三. Kinded统一α2：：{{fire_danger：fdtype，location：ltype}}，α3：：U}.（{（α1，α2）}，{（α1，{{location：α3}}），（α2，{{fire_danger：fdtype，location：ltype}}），（α3，U）}，{}）（{（α3，ltype）}，{（α2，{{fire_danger：fdtype，location：α3}}），（α3， U）}，{（α1，α2）}）（{}，{（α2，{{fire_danger：fdtype，location：ltype}}）}，{（α1，α2），（α3，ltype）}）α 1和α 2之间最一般的单位是类替换（α2：：fir_danger：fd type，location：ltype，[α2/α1，ltype/α3]）。根据Ohori的表示法，在类统一算法中，此外，请注意，[24]中的统一算法有一个kind赋值作为一个额外的参数，用于记录在统一过程中遇到的已解决的kind约束。然而，我们选择忽略这个参数，因为它的信息只在[24]中的证明中使用，而不是在统一过程中。在[24]中，证明了类统一化算法的正确性和完备性，在这个意义上，它采用任何类方程组并计算其最一般的统一器，如果存在的话，否则报告失败S. Alves等人/理论计算机科学电子笔记351（2020）3134.2类型推断类型推断算法WK（K，Γ，M）在图4中定义。给定kinding环境K、typing环境Γ和EVL项M，则WK（K1，Γ，M）=14S. Alves等人/理论计算机科学电子笔记351（2020）3◦ ◦ ◦◦}→ → {}→ →{UU→ →{}{{}联系我们（KJ，S，σ），使得σ是M在类环境KJ和分型环境S（Γ）下的型.它隐含地假设，如果unification或任何子项的递归调用失败，则推理算法失败。WK（K，Γ，x）=如果x∈ dom（Γ）则失败否则设τα1：：κ1· · ·ταn：：κn.τ=Γ（x），S =[β1/α1，.，β n/α n]（β1，...，β n是新鲜的）在（K{β1：：S（κ1），.，β n：：S（κ n）}，id，S（τ））WK（K，T，M1M2）=let（K1，S1，τ1）= WK（K，T，M1）（K2，S2，τ2）=WK（K1，S1（T），M2）（K3，S3）=U（K2，{（S2（τ1），τ2→α）}）（α是新鲜的）在（K3，S3<$S2<$S1，S3（α））中WK（K，Γ，λx.M）=let（K1，S1，τ）=WK（K<${α：：U}， Γ<${x：α}，M）（αfresh）in（K1，S1，S1（α）→τ）WK（K，Γ，令x=M1，在M2中）=令（K1，S1，τ1）= WK（K，Γ，M1）（K1′，σ）=Cls（K1，S1（Γ），τ1）（K2，S2，τ2）=WK（K1′，S1（Γ）<${x：σ}，M2）在（K2，S2<$S1，τ2）WK（K，Γ，letEvx=M1inM2）=let（K1，S1，γ）= WK（K，Γ，M1）（K1′，σ）=Cls（K1，S1（Γ）， γ）（K2，S2，τ2）=WK（K1′，S1（Γ）<${x：σ}，M2）在（K2，S2<$S1，τ2）WK（K，r，{11= M1，...， I n= M n}）= let（K1，S1，τ1）= WK（K，τ，M1）（Ki，Si，τi）=WK（Ki−1，Si−1<$· ·<$S1（Γ），Mi）（2≤i≤n）在（Kn，Sn<$··<$S2<$S1，{11：Sn =S n · · ·Sn2（τ1）， . ，li：Sn_i · · ·Sn_i+1（τi）， . ，ln：τn}）W K（K，Γ， M. l） =let（K1，S1，τ1）=WK（K，T， M）（K2，S2）=U（K1<${α1：：U，α2：：{{l：α1}，{（α2，τ1）}）（α1，α2fresh）in（K2，S2<$S1，S2（α1））WK（K，T，modify（M1，1，M2））=let（K1，S1，τ1）= WK（K，T，M1）（K2，S2，τ2）=WK（K1，S1（T），M2）（K3，S3）=U（K2<${α1：：U，α2：：{{l：α1}，{（α1，τ2），（α2，S2（τ1））}）（α1，α2为新鲜）在（K3，S3<$S2<$S1，S3（α2））中WK（K，r，ifM1thenM2elseM3）=let（K1，S1，τ1）= WK（K，r，M1）（K2，S2）=U（K1，{（τ1，bool）}）（K3，S3，τ2）=WK（K2，S2<$S1（Γ），M2）（K4，S4，τ3）=WK（K3，S3<$S2<$S1（Γ），M3）（K5，S5）=U（K4，{（S4（τ2），τ3）}）在（K5，S5<$S4<$S3<$S2<$S1，S5<$S4（τ2））中见图4。 类型推理算法示例4.2 例如 3.9，我们 考虑 M=位置为l，火灾危险=d，τ1=location：α1，fire_danger：α2，τ2=α1：：. α2：：.α1α2τ1，τ3=location：l type，fire_danger：fd type，andτ4=l type fd typeτ3，我们进一步考虑τ5=location：α3，fire_danger：S. Alves等人/理论计算机科学电子笔记351（2020）315α4 ， τ6=α3 ： ： 。 α4 ： ： .α3α4τ5 ， τ7= 位 置 ： α5 ， 火 险 ： α6 ， S1=[ltype/α5][α5/α3，α6/α4]，S2=[fdtype/α6]S1[α4/α2][α3/α1]。在FireDanger“Porto““low“中运行letEvFireDanger=λl.λd.M的算法16S. Alves等人/理论计算机科学电子笔记351（2020）3►►如图5所示。WK（{}，{}，letEvFireDanger=λl.λd.MinFireDangerW K（{}，{}，λl. λd. M）=（{α3：：U，α4：：U}，[α4/α2]<$[α3/α1]，α3→α4→τ5）W K（{α1：：U}，{l：α1}，λd. M）=（{α3：：U，α4：：U}，[α4/α2]<$[α3/α1]，α4→τ5）WK（{α1：：U，α2：：U}，{l：α1， d：α2}， M）=（{α3：：U，α4：：U}，[α4/α2]<$[α3/α1]，τ5）WK（{α1：：U，α2：：U}，{l：α1， d：α2}，l）=（{α2：：U，α3：：U}，[α3/α1]，α3）WK（{α2：：U，α3：：U}，{l：α3， d：α2}，d）=（α3：：U，α4：：U}，[α4/α2]，α4）Cls（{α3：：U，α4：：U}，{}，α3→α4→τ5）=（{}，τ6）WK（{}，{FireDanger：τ6}， F ireDangerWK（{}，{FireDanger：τ6}， F ireDangerWK（{}，{FireDanger：τ6}， F ireDanger）=（{}，[α5/α3，α6/α4]，α5→α6→τ7）WK（{}，{FireDanger：τ6}，U（{}，（α5，ltype））=（{}，[ltype/α5]）WK（{}，{FireDanger：τ6}，U（{}，（α6， fdtype））=（{}，[fdtype/α6]）图五、在FireDanger“Porto o““l ow“中为letEvF i r eDanger=λl.λd.M运行类型4.3WK的合理性和完整性在这一节中，我们建立了我们的类型推理算法的可靠性和完备性的结果定理4.3若WK（K，Γ，M）=（KJ，S，τ）则（KJ，S）关于K，并且在我们的型系统中存在一个导子使得KJ，S（Γ）<$M：τ.证据 证明是通过归纳M的结构。Q定理4.4若WK（K，Γ，M）=fail，则不存在（K0，S0）和τ0使得（K0，S0）关于K和K0，S0（Γ）M：τ0.若WK（K，r，M）=（KJ，S，τ），则若K0，S0（r）M：τ0对于某个（K0，S0）且τ0使得（K0，S0）尊重K，则存在某个SJ使得（K0，SJ）尊重KJ，τ0= SJ（τ）且S0（r）= Sj<$S（r）.证据 证明是通过归纳M的结构。Q5EVL用于复杂事件处理在本节中，我们将研究EVL在复杂事件处理（CEP）背景下的应用参见[15]关于该区域的详细参考。CEP领域包括一系列处理事件流的技术，例如事件处理、模式和关系检测、过滤、转换和抽象等。由于EVL是一种高阶函数语言，我们将探索高阶功能，以定义处理通常CEP技术的高阶参数化函数S. Alves等人/理论计算机科学电子笔记351（2020）317∀···∀5.1事件处理事件处理的规范模型[10，15]基于生产者-消费者模型：事件处理代理（EPA）从事件生产者获取事件并将其分发给事件消费者。这个过程通常涉及过滤或翻译。可能会发生过滤，因为并非每个事件都对每个消费者感兴趣或可用：在某些情况下，访问控制策略可能会限制消费者可能接收的事件。翻译事件允许我们根据特定的消费者更改、添加或删除代理中的信息事件的处理可以以一个事件输入/一个事件输出的形式完成，但是也可以使事件处理代理作为整体处理事件的集合或产生一组事件作为结果：例如，传入事件可以被分成多个事件，每个事件包含来自原始事件的信息的子集。EVL可用于对事件处理代理进行编程。它能够处理由某些事件处理系统产生的原始事件，并生成派生事件。然后，这些派生事件可以传递给事件使用者。主体类型允许我们识别事件处理代理。事件处理代理是其主类型具有以下形式的任何函数α1：：κ1α n：：κ n.γ.在下面的部分中，我们将探讨不同类型的事件处理代理。5.1.1事件处理代理的类型事件处理代理根据它们处理传入事件所执行的操作进行分类：• 过滤代理-过滤代理获取传入的事件对象，并应用测试来决定是否丢弃它或是否将其传递给后续代理进行处理测试通常是无状态的，即仅基于事件实例的内容。• 转换代理-转换代理修改它们接收的事件对象的内容。这些代理可以根据其输入和输出的基数进一步分类（翻译，拆分，聚合或组合代理）• PatternDetect代理-PatternDetect代理收集传入的事件对象并对其进行检查，以查看它们是否可以发现特定模式的出现。我们现在将更深入地研究不同类型的事件处理代理。我们所要提出的所有定义都可以在[15]中找到。定义5.1[过滤事件处理代理]过滤器代理是一个只执行过滤的事件处理代理，因此它不会转换输入事件。例5.2这个例子描述了一个事件处理代理，它使用一个高阶的过滤器函数filter（稍后定义）根据事件的位置来过滤事件。18S. Alves等人/理论计算机科学电子笔记351（2020）3l e tpX =（x .位置==“波尔图“）I nλx。（过滤器p x）定义5.3[转换事件处理代理]转换事件处理代理是一个事件处理代理，它包括一个派生步骤，还可以选择一个过滤步骤。转换事件处理代理可以是无状态的（如果处理事件时不考虑之前或之后的事件），也可以是有状态的（如果处理事件的方式受之前或之后事件的影响）。在前一种情况下，事件被单独处理。在后者中，处理事件的方式可以取决于之前或之后的 事 件 。 转 换 事 件 可 以 进 一 步 分 类 为 translate ， split ， aggregate 或 composeagents。在下文中，我们将描述一些我们将要关注的转换事件5.4[翻译事件处理代理]翻译事件处理代理可用于将事件从一种类型转换为另一种类型，或者添加、删除或修改事件属性的值目前EVL不允许我们添加或删除属性。可以根据传入事件的属性创建新事件，也可以修改现有属性的值。我们遵循Ohori对记录类型的处理，因此我们不考虑用新字段扩展记录或从记录中删除现有字段的操作。这是我们当前演算的