泛型类型保持遍历策略 RS Lammel

理论计算机科学电子笔记57（2001）网址：http://www.elsevier.nl/locate/entcs/volume57.html23页泛型类型保持遍历策略Ralf Lammel1CWI，Kruislaan 413，NL-1098 SJ AmsterdamVrije Universiteit，De Boelelaan 1081a，NL-1081 HV Amsterdam摘要本文提出了一种覆盖通用遍历的策略重写的类型化模型。对应的演算例如是策略运算符2（），它将参数策略应用于所有直接子项。为了给泛型策略提供一个典型的模型，我们必须识别与签名无关的类型，也就是泛型类型。在本文中，我们将自己限制在TP|所有T型-P保留策略的一般类型。TP很容易集成到一个标准的多排序类型系统中进行重写。为了适应TP，我们需要引入一个（左偏）类型驱动的选择操作符。如果给定项的类型为ts，则运算符应用其左参数（对应于多排序策略），否则运算符诉诸右参数（对应于泛型默认值）。这种方法要求策略应用的语义必须在一定程度上依赖于类型。1导言战略改写几种重写框架都是用来描述策略的（与那些假定固定的标准化/评估内置策略的框架相反）。例如，支持策略的是规范形式主义Maude[14，7]和ELAN [3，4]。此外，微积分[5]也非常适合于策略的定义.基于系统S[21]的程序设计语言ESPRGO[20]完全致力于战略编程。重写策略的思想可以追溯到Paulson关于重写策略的高阶实现的工作[18]。策略可用于描述评估和标准化策略，例如，为了控制某些重写规则的重写，这些重写规则在被认为是标准重写系统时是不一致的或不终止的。策略对于指定遍历特别有用1 电子邮件：Ralf. cwi.nlc2001年由Elsevier Science B出版。V. CC BY-NC-ND许可下的开放访问。Lammel2BGg3 c c（二）（三）（四）b btrue[3，5]Gg4 c c 3 c c图1. 通用导线为了在标准重写中描述遍历（没有对遍历的额外支持），必须求助于辅助函数符号，并且必须使用重写规则来执行手头签名的实际遍历（通常每个项构造函数一个重写规则）。泛型遍历原语在编程中支持泛型的一个重要方面。例如，在[19]中，通用遍历策略用于语言实现：自由变量收集，替换，union等算法以通用的方式定义，即通过适当参数化的通用遍历以独立于语言的方式定义。泛型遍历在图1中，示出了有意通用遍历的四个示例（I）{（IV）在（I）中，给定项（比如树）中的所有自然项都如重写规则N所建模的那样递增！succ（N）.我们需要把这个规则转换成一个遍历策略，因为当被认为是重写系统时，规则本身是不会终止的该战略应当是通用的，也就是说，它应当适用于任何术语。在（II）中，根据重写规则g（P）重写特定模式！ g0（P）. 假设我们想要控制该替换，使得它以自底向上的方式执行，并且仅重写第一匹配项。在术语中定位所需节点的策略是完全通用的。 例子（III）和（IV）是类型改变遍历的FH5FH6（一）FGHG'5Lammel3例子，实际上它们是类型统一遍历，Lammel4[12][11]。在（III）中，我们可以测试项的某些性质，例如，如果真的有自然现象的话在（IV）中，我们使用从左到右的遍历来收集术语中的所有自然值。打字价值这篇文章的贡献是一个类型系统，它涵盖了上述示例所需的通用transversals。在本文中，我们将自己限制在类型保持策略上。包括类型改变策略在内的更详尽的处理可以在[10]中找到。让我们理解为什么类型是有价值的。一般来说，类型化显然应该防止我们构造类型不好的术语。通用遍历通常使用许多排序的成分（比如重写规则）。类型系统和相应的动态语义应该确保以类型安全的方式应用特定的成分。例如，考虑增量N的重写规则！succ（N），如上面的例子（I）中所假设的。这种一步重写规则应该只应用于遍历过程中的自然值。另一方面，完整的遍历必须能够处理任何项。类型系统还应该防止程序员以某些不希望的方式将特殊策略和泛型策略例如，考虑一个左偏选择“+Id”，如果可能的话，应用普通重写规则“，否则触发\generic default”Id“。有人可能会说，这种策略是通用的，因为ID适用于所有可能的术语。实际上，我们赞成另外两种可能的解释。我们要么完全拒绝这种选择（因为我们坚持认为论证策略的类型是相同的），要么将非类属论证类型作为复合策略的类型。事实上，策略不应该太容易变得通用，因为否则我们会失去一个多排序类型系统的有价值的精度。即使不能构造类型错误的类型，泛型策略也可能会意外地拒绝术语（导致失败），或者它们以不可追踪的方式保持术语不变打字困难一些策略组合子比其他的更容易输入。不同种类的选择，顺序组合，签名特定的同余运算符和其他的组合器很容易在多排序设置中输入。可能需要使用重载和/或参数类型。实际上，ELAN就是基于这样一个多排序类型系统。相比之下，通用遍历原语（例如，2（s）将策略s应用于由系统S）提供的给定项的所有直接子项更具挑战性，因为标准的多排序类型不适用，并且其他成熟的概念如多态性不足以建模所需的泛型。泛型遍历策略必须适用于任何类型的术语（或者至少适用于某类类型）。泛型遍历在某种意义上是依赖于类型的（与多态性相对），因为它们通常是从特定成分（比如重写规则）派生出来的，以处理某些特殊的排序。Lammel5以特定的方式。我们还建议读者参考[19，11]，其中认为类型化泛型遍历是困难的。如果涵盖了类型更改策略，则泛型遍历的类型化将更加复杂[10]。文章的贡献和结构在第2节中，我们简要回顾了包括遍历原语在内的无类型策略。在第3节中，我们讨论了类型保持策略的标准多排序类型。2在第4节中，我们提供了一个类型系统，其中包含一个泛型策略类型TP，用于泛型类型保持策略。为此，我们还需要引入一个依赖于类型的选择操作符来在多排序策略和泛型策略之间进行调解在第5节中，我们讨论了实施问题。在文章的过程中，我们表明，我们的类型系统的战略是明智的战略程序员的角度来看。 我们设想，所提出的类型系统纪律战略计划（采用通用遍历）在一个有用的，而不是过于限制性的方式。我们还表明，通用的类型保持策略可以（或多或少）很容易实现。文章在第6节结束。确认作者的工作得到了NWO在项目“程序转换系统的生成”中的部分支持。本文中提出的想法是在作者访问洛里亚南希的Protheo集团期间形成的。我特别感谢与我的同事Joost Visser的互动|在南希和一般。非常感谢Christophe Ringeissen，他与Joost和我分享了一个深入而富有洞察力的ELAN会议。我想感谢DavidBasin，Hora-tiuCirstea，HeleneKirc hner，ClaudeKirc hner，PaulKlint，Pierre-EtienneMoreau， Christophe Ringeissen，Jurgen Vinju和Eelco Visser对本文主题的讨论。最后，非常感谢匿名研讨会裁判的建设性批评。2非类型化策略我们建立了一个重写的微积分，很大程度上受到了ELAN的启发，微积分，系统S。我们非常简短的解释，例子和语义的细节。一些基本的战略改写知识（如[2，21，5]）是阅读本文的有用背景。首先，我们对我们要研究的策略组合子进行了概述，并说明了如何利用策略定义来构造新的策略组合子。然后，我们解释了策略应用的语义模型。最后我们2 至于术语，我们甚至使用术语\type”来表示多排序项的类型（与术语\sort”相反）。术语“类型”在类型系统的上下文中更为常见。此外，我们可以轻松地超越多排序的术语，并处理多态数据库。Lammel61n对我们框架中包含的通用遍历原语进行了详细的解释。2.1策略组合子我们有以下语法用于策略表达式：s：：=t！tjIdjFailjs; sj s+ sj s+ sjf（ s; ：; s）j2（ s）j3（ s）有一种战略T！的t0一步规则适用于词根。我们采用一些常见的重写规则的限制 左边的t决定了约束变量。（自由）变量在右边-t0 侧也发生在测试中。如果应用了替换，则我们假设- 皈依。除了规则形成之外，身份策略（Id），失败策略（Fail），顺序组合（;），对称选择（+），不对称左偏选择（+）。 策略f（s 1;：; s n）表示函数符号f的同余策略。 3形式2（）和3（）是变换本原。 策略2（s）将参数策略s应用于给定项的所有直接子项（例如，c项）。 策略3（s）将优化策略s应用于给定项的某个子项。对2（）和3（）进行了详细的讨论。例2.1让我们考虑在一棵二叉树中，把自然数放在叶子上，从而把我们假设以下符号来构造这样的树：零：自然Succ：Nat！纳特：纳特！ 树fork：Tree Tree！ 树N和T|可选地带撇号或下标|分别用作Nat和Tree排序的变量。我们可以用一个标准的项重写系统来指定ipping顶层子树的问题。我们需要使用辅助函数符号ip-top来获得终止重写系统：ip-top（leaf（N））！叶（N）ip-top（fork（T 1; T 2））！叉（T 2; T 1）或者，我们可以使用策略ip-top而不引入额外的函数符号。我们通过+组合了两个单步重写规则。规则“1”模拟叶的保存，而规则“2”模拟顶级子树：`1= leaf（N）！ 叶（N）`2= fork（T 1; T 2）！ 叉（T 2; T 1）ip-top=`1+`23 也就是说，策略f（s;：;s）将参数策略应用于术语的参数f作为最外层符号，否则策略无条件失败。Lammel6新的策略组合子可以通过一种我们称之为策略定义的抽象机制来定义ELAN、S系统和ELAN提供了类似的机制。 定义“（1; ：;n）=sin”引入了n元策略组合器“. 的应用'（s1; ：;sn）'表示'的定义的主体的实例s[1：=s1; ：;n：=sn]。策略定义可以是递归的。4示例2.2一些示例定义如下：try（）= +Idrepeat（）= try（; repeat（））ip-top=try（`2）前两种策略是通用的。try（s）应用s，但如果s失败，则其行为类似于Id。repeat（s）重复地尽可能频繁地应用s。策略ip-top在本质上是特殊的它重构了前面在例2.1中介绍的同名策略。这个重构说明了try的用法。2.2语义模型将策略s应用于项t表示为hs it。对于动态语义，我们采用了一个判断策略应用`h s i t;r，其中r是约简，其中h是项t0， 或用y““表示的故障。 这个模型是从S系统中引进的。注意，给出的判断不足以定义策略定义的应用的语义为此，我们必须通过上下文参数传播定义还请注意，我们假设策略只应用于基础项，然后也产生基础项。5.我们采用某种特定的风格来指定演绎规则。我们给积极的规则的情况下，减少是一个术语，我们给消极的规则，其余的情况下，失败的减少。我们在图2中显示了评估判断的摘录。它涵盖了非对称左偏选择的积极和消极规则。这些规则也说明了为什么我们需要将失败作为归约。否则，语义无法查询某个应用程序是否未成功（参见 [lchoice+：2]）。2.3泛型遍历原语让我们仔细看看通用遍历原语，将策略s应用于所有child（2（s））或某些child（3（s））。 运算符2（）和3（）类似于系统S中的运算符。 简言之，我们不考虑来自系统S的将策略应用于一个或多个半导体的混合操作器32。4 递归定义在ELAN中是常见的，而系统S和实用的ELAN则使用了一种特殊的递归算子**5 该假设与标准重写一致，特别是对于普通的一阶重写规则。Lammel7策略应用积极规则消极规则hsit;t0hs+s0it;t0【lchoice+：1】“是的，是的。”“是的，是的。”^ `hs0it;t0hs+s0it;t0【lchoice+：2】^ `hs0it;“`hs+s0it;“[lchoice]图2. 左偏选择应用的正负规则类似的运算符也可以在- 微积分（cf. （s）和 （s）in[5]对应于2（s）和3（s））。在图3中，我们展示了根据2（）和3（）定义的一些有用的可导出的通用遍历策略。 除最后一个定义外，其他定义均采用[2]中的定义。请注意，在所有这些定义中，它都是策略的元变量。topdown（）=;2（topdown（））（以自上而下的方式应用）bottomup（）int n =2（int n）;（适用自下而上的方式）翁塞特=+3（onc etd（））（适用一次以自上而下的方式）oncebu（）=3（on ceb u（））+（以自底向上的方式应用一次）inner（）= repeat（oncebu（））（最内层的评估策略）stoptd（）=+ 2（停止d（））（适用以自上而下的方式与\cut”）图3. 一些派生的泛型遍历策略例2.3让我们来解决本文引言中图1nat= zero+ succ（Id）transverse （ I ） =stoptd （ nat;N！ succ（N））t ravers e （II ）=on ceb u（g（P）！g0（P））nat是一个辅助策略测试自然的一致性策略为零和succ。我们使用nat作为类型检查来启用重写规则N的适用性！在遍历的定义（I）中succ`Hsit; RLammel8（N）。回想一下，遍历（I）意味着增加所有的自然数。相应的策略是根据通用策略stoptd定义的（参见。图3）下降Lammel9不不`h2（s）if（t; ： ; t）;f（t0; ：;t0）不0`h3（s）if（t; ：; t）;f（t; ：;t0; ：; t）00只要论点策略不成功，就可以将其放入给定的术语中。 这正是我们需要在树中增加所有自然数的遍历方案。以自上而下的方式遇到自然词时，我们应用递增规则，但随后我们不进一步下降到术语。如果我们使用自顶向下而不是stoptd，我们描述了一个非终止策略。遍历（II）的定义也很容易阅读。遍历（II）以自底向上的方式（根据需要）结束形式g（x）的第一个模式，并将其替换为yg0（x）（如重写规则所表示的）。注意遍历（I）和遍历（II）的通用性。它们可以应用于任何术语。当然，这些策略有些特殊，因为它们依赖于一些常数或函数符号，即ze ro，su cc，g和g0。顺便说一句，由于本文只讨论了类型保持策略，我们无法实现引言中的其他两个问题2（）和3（）的位置语义规则如图4所示。 规则[all+：1]是指当2（s）应用于常数时，立即成功，因为不存在必须应用2（s）的掩码。规则[all+：2]直接编码了将s应用于项f（t 1;：; t n）的所有子项的含义。请注意，函数符号f在结果中保留。3（s）的定义类似。 规则[one+：1]表示s应用于f（t 1;：; t n）的某个子项t i。策略应用`h2（s）ic;c[all+：1]hsit1;1- -^ `hsitn;n【全部+：2】1n1n9i2f1; ：;ng：`hsiti;i【1+：1】1n1in图4. 2（s）和3（s）的评价3多分类策略作为热身，我们提供了一个类型系统（非泛型，比如多排序）类型保持策略。首先，我们将解释类型系统的模型.然后，我们详细讨论了实际的演绎规则。最后我们`Hsit; RLammel10讨论类型系统的一些设计属性，主要是为覆盖泛型策略的扩展做准备（如本文的主要部分，即第4节所述）。3.1述类型模型有两个层次的类型。我们有多排序项的类型和策略的类型。我们使用范围在排序，范围在术语类型，torange范围over strategy战略types类型. 类型表达式的形式最初是由以下语法定义：：：=（术语类型）--=！（策略类型）在类型判断中，我们使用上下文参数来记录将常量符号c、函数符号f、项变量x、策略变量和组合子'映射到类型。我们在上下文中使用以下语法：：= ; j[（上下文作为集合）Jjc：jf：！（ 签 字 部分 ） jx ：J： （ 期 限 和 战 略 变 量 ） j“道：！（策略组合器）因此，包含了一个多排序的术语签名，变量声明（术语变量和策略变量），以及来自策略定义的组合子类型声明。让我们陈述一些格式良好的要求。我们假设各种符号和变量没有混淆（即，有不同的命名空间），并且符号和变量与中的不同类型没有关联（特别是，我们不考虑重载）。在某些声明中使用的所有类型也必须引入。所有的声明都必须是格式良好的（w.r.t.下面定义的格式良好性判断）。 注意假设是静态的（比如给定的），所有即将到来的判决因此，我们假设各种变量和符号都有显式的类型声明。6.相反，很容易推断。类型系统的主要判断是策略的类型判断。它的形式是s：，如果策略s是上下文中的策略类型， 则 它 成 立 。6 变量、重写函数和策略的声明在用于重写的若干框架中是常见的，例如，ASF+SDF和ELAN。Lammel113.2扣费规则各种判断的演绎规则如图5所示。为了简洁起见，我们省略了策略定义的类型规则类型保持是由策略类型的良构性判断所规定的规则[pi：1]）。其他一些规则也显式地强制类型保持（cf. rules [comp：1]、[apply]、[rule]、[id]、[fail]和[r]）。多类策略的类型系统不应视为本文的贡献。这是相当直接的，它非常符合ELAN所假设的类型系统。为了方便起见，让我们读一些推理规则。规则[apply]指出，如果策略s的类型为，则策略应用程序h s i t是良好类型的！，并且项t是类型的。策略Id和Fail有多种类型，即任何类型！在那里，“保持”（cf.规则[id]和[fail]）。复合策略的策略类型由规则[seq]、[choice]、[lchoice]和[r]管理复合策略s1;s2是指对可组合类型的辅助判断。对于多排序类型保持策略，可组合类型是根据规则[comp：1]简单定义的。复合策略s1+s2和s1+s2是良型的，如果两个策略s1和s2是一个共同的类型，这也决定了复合策略的类型。3.3讨论从积极的方面来看，我们可以为某些策略分配类型，如下面的例子所示。例 3.1 例 2.1 中的 策略 ip-top 是类 型保 持的 。因 此， 类型 ip-top ：Tree！树的定义可以被认可。消极的一面是，没有办法给我们到目前为止看到的某些其他策略分配类型。当然，我们不能将类型分配给泛型遍历，因为它们不限于特定的排序。但是我们甚至不能给一些不涉及遍历的策略分配类型。例如，例2.2中定义的try和repeat类型是什么？在某种意义上，这些组合子采用类型保持策略，并返回类型保持策略。与Id和Fail一样，try和repeat组合子可以与许多类型相关联。然而，这种观点与类型单一性的理想相抵触。实际上，Id和Fail的类型规则也违反了类型的唯一性，但由于它们是原语，这种违反可以被视为重载的可接受公式，或参数类型的编码77 稍后我们将讨论参数类型的可能使用Lammel121nTerm类型战略2的策略类型的”“是的！方面c：2【τ：1】【圆周率：1】[const]`t：^`t0：不！t0：！的‘伊得：！的“失败！1：1^2：2[规则][ID][失败]`c：^1Æ二、[seq]F级：1你好！ 2^一比一- -^`tn：n[有趣]s1;s2：第一条：^第二条：s1+s2：[选择]`f（t1; ： ;tn）：x：2X`x：可组合类型的！Æ！;！[var][comp：1]s1+s2：s1+s2：F级：1你好！ 2^第一条：一个！1- -^`sn：n ！n`f（s ;：;s ）：！[lchoice][r]策略应用s：！^`t：`hsit：[适用]的的`s：`t：1Æ2 ;`Hsi：Lammel13图5. 多类保型策略Lammel144一般战略2（s）和3（s）的重要性在于，它们被假设为适用于任何种类的项，即，它们是通用的。显然，这也是Id和Fail的情况。 与重写规则相比。它只适用于特定排序的术语，因为它是从特定类型的术语构造注意，遍历原语的参数也必须是泛型类型的例如，考虑2（s）。 参数s必须潜在地适用于任何类型的子项。因此，我们需要在类型模型中添加一种泛型策略类型然后，我们能够在volving2（）和3（）中为策略分配类型（同时，我们还解决了Id和Fail的唯一性问题，并且我们可以为try和repeat等策略分配类型）。首先，我们将引入一个类型来对泛型类型保持策略进行建模。然后，考虑了多类策略和一般策略之间的中介问题。最后，我们指出了一些方便的性质所产生的类型系统。4.1所有类型保持策略我们扩展了策略类型的语法，也就是说，我们为通用类型添加了一个case。在这篇文章中，我们只考虑一个特定的泛型类型，即TP表示所有T类型-P保留策略的类型。在[10]中，我们还考虑了类型改变策略。我们的类型语法扩展如下：：：=J* =TP例4.1图3中的所有策略都是泛型类型保持策略。此外，所有定义的参数策略都是TP类型。这同样适用于例2 - 2中定义的尝试和重复策略。因此，我们假设类型TP！所有这些策略定义的TP。在图6中，我们扩展了类型判断。 我们使用类型的偏序来度量类型的泛型。多排序类型比泛型类型更“少”泛型或通用。Rule [typeless：1]axiomatisesTP.规则规定， ！所有格式良好的TP. 这直接表达了类型保持策略的一部分TP类型的策略可以应用于任何类型的术语。Id和Fail被定义为规则[i d]和[fail]中的（通用）类型保持策略。 2（s）和3（s）以及它们的排序策略s在规则[all]和[one]中也被定义为类型保持的。类型系统严格区分了多排序策略（如重写规则）和泛型策略（如2（）的应用）。就目前而言，我们不能把多种分类的策略变成通用的策略，也不能反过来。我们将提供相应的回复策略Lammel15的策略类型应用`TP[pi：2]泛型的的：^`t：^！`hsit：[适用]！ TP可组合类型[无：1]战略`Id：TP[id]公司简介TP; TP[组件：2]`失败：TP[失败]中文（简体）`2（s）：TP[全部]中文（简体）`3（s）：TP[一]图6. 泛型类型保持策略微积分很快。策略应用的良好类型规则（参见[apply]）当然阐明了如何将通用策略应用于特定类别的术语。4.2种属中介既然我们已经键入了泛型遍历操作符，问题是我们如何驻留TP。到目前为止，我们只有两个TP类型的平凡常量，即Id和Fail。我们希望从重写规则中构建通用策略。事实证明，我们缺乏一个以类型化方式执行居住的构造。我们还需要放松一些现有组合子的类型规则，以便在特定上下文中轻松应用泛型策略。如果由于类型原因，多排序策略不适用，则一种方法是使用通用默认值（最初是Id和Fail，但不仅仅是这些）例如，我们可以尝试使用` + Id或` + Fail形式将重写规则`转换为通用策略。 这不是一个好主意，因为运算符+关注的是由成功和失败控制的选择。我们在特定策略的资格化背景下寻找的是一种我们需要一种依赖于类型的选择形的：hs：01Æ2 ;Lammel16式，如果实际的术语被其域覆盖，则选择特定的策略。否则，通用策略（作为Lammel17默认类型）。我们引入一个相应的操作符：s：：=jss左参数是多排序策略，而右参数是通用默认值。图7中定义了操作符的静态和动态语义。例4.2我们回想起例2.3中介绍的第一个问题的解。原 始 的（类似于Nat ; N的）解决方案是不可输入的，因为一个多排序策略，即nat;N！ succ（N）被传递给stoptd，stoptd需要一个泛型参数。我们通过以下遍历的定义来恢复可类型性（I）：transverse（I）=stoptd（（nat; N！成功（N））失败）=stoptd（（N！成功（N））失败）这个解决方案说明了我们可以限定特定的重写规则成为通用的。顺便说一句，类型化模型支持消除自然值测试的简化。重写规则的类型必然限制其适用性。例2.3中的另一个策略遍历（II）也可以用同样的方法进行。该算子根据应用程序中术语的类型，用于不对称的左偏策略选择正如演绎规则所详述的，如果s1s2应用于类型为t的项，并且s1的类型与！ ，则s1是chosen（cf. [lplus+：1]）。否则，我们将求助于通用的策略s2（比照 [lplus+：2]）。&从这个意义上说，&是左偏的w.r.t.类型敏感性，而 + 偏左w.r.t.成功与失败这种分离使我们想成为泛型的地方变得明确。没有什么隐藏的方式可以让特定的成分意外地变得通用。如果不将这两种选择分开，策略很容易（比如说意外地）变得通用和可类型化。请注意，语义判断需要能够确定特定策略的类型以及给定术语的类型为此，我们在策略应用的判断中加入了类型上下文。的否定语义规则也显示在图7中，因为它们具有指导性。人们可以清楚地看到如何使用该术语的类型来确定左操作数s1在s1s2中的可应用性。这种类型敏感性可以被视为一种范式转变。我们推迟讨论如何消除语义规则中确定hs1s2 it成分类型的前提到目前为止，我们只考虑了调解的一个方向我们还应该重新定义类型系统，以便泛型策略可以很容易地应用于多种类型的上下文中。这个要求相当于简单地放松了策略组合子的参数策略的类型。基本上，我们要声明的是，像s1;s2和s1+s2这样的复合策略的类型是由下式决定的：一个多排序的参数（如果有的话）。至于一致性策略，我们简单地Lammel1812212良型性s1：！^第二条：s：0！0^`t：- -啊！^`hsit;t0[lplus+：2]s1s2：[lplus]0hs1sit;t积极规则s1：！消极规则s1：！^`t：^`hs1 it;“`hs1s2it;“[lplus：1]^`t：^`hsit;t0【lplus+：1】0 0s1：！0hs1sit;t^`t：- -^`hs2 it;“`hs1s2it;“[lplus：2]图7. 将具体战略转化为一般战略用于关联形式和实际参数类型。没有毛-其他非通用上下文的给定组合子套件。 我们的类型系统的一个相应的元素在图8中定义。至于;，我们放宽了可组合类型的定义，以涵盖两种可能顺序的specic和generic类型的组合（参见。规则[comp：3][4 ][5]。至于+(and因此对于+我们也不坚持但是我们假设我们可以确定类型w.r.t.的最大下界。（参见规则[选择]）。最后，我们通过关系放松了一致策略的论元类型。 从某种意义上说，这种方法自动化了泛型策略的类型特化。这不被认为是问题（与多排序策略成为泛型的隐藏方式相反），因为当程序员试图在泛型上下文中应用该策略时，意外的多排序策略很容易被程序员实现，也就是说，类型系统将捕获这种意外。4.3微积分的性质我们最终的类型化策略演算是从多排序策略开始得到的（参见图5），并使用操作员更新它（参见图7）hsit;r0`s：0Lammel19TPTPTP可组合类型的！ÆTP;！的公司简介！;！[comp：3][comp：4]1：1^2：2^1U二、s1+s2：F级：1你好！ 2^第一条：1 ^一个！11- -^`sn：n ^n ！n n`f（s1; ： ;sn）：！[选择][r]图8.在潜在的特定环境中应用一般策略以及来自BOVE的弛豫（cf. 图8）。我们称之为微积分S0（到它与系统S密切相关。以下定理总结了S0的理想性质 .定理4.3 S0的类型系统(i) 策略满足类型的唯一性。遵守以下规定：(ii) 策略应用满足分型的单一性。(iii) 策略应用的语义满足主题约简。证明1. 通过归纳在良好类型判断中的策略：基本情况：重写规则的类型（cf.规则[rule]）由所涉及的术语唯一地定义。当然，类型的唯一性也适用于词项的类型判断。常量策略Id和Fail的类型是唯一定义的（参见规则[id]和[fail]）。归纳步骤：所有组合子的所有论元策略的类型在归纳假设下是唯一的。对于二元运算符;，结果类型被定义为由参数类型组成的类型。对于+和+，结果类型被定义为参数类型的最大下界。相应的判决Æ;及u ;显然编码功能。因此，类型的唯一性成立。的一致性策略（Congruence Strategy）rule [rule]）由格式良好的上下文指定，该上下文用于查找手头的函数符号的排序 2（s）和3（s）的类型被唯一地定义为TP。 s1&s2的类型是s 2的类型。`s：1Æ2 ;