理论计算机科学电子笔记136（2005）3-21www.elsevier.com/locate/entcs类型前序和递归项法比奥·阿莱西1数学与信息学专业研究与开发Via delle Scienze 208，33100 Udine（Italy）Mariangiola Dezani-Ciancaglini德扎尼-钱卡格里尼2，3Dipartimento diInformaticaUniversit`adegliStudidiTorinoCorso Svizzera 185，10149 Torino（Italy）摘要我们展示了如何使用交集类型来构建富含递归项的λ-演算的模型，其预期含义是最小不动点。作为副产品，我们证明了一个有趣的一致性结果。保留字：λ-模型，不动点，相交类型，简单术语1介绍相交类型是在70年代后期由Coppo和Dezani [5，6，3]引入的它们是一种非常有表现力的类型语言，允许描述和捕获λ-项的各种属性。例如，它们已被用于Pottinger [19]中，以给出强正规化项的第一类理论表征，并在Coppo et1电子邮件：alessi@dimi.uniud.it2电子邮件：dezani@di.unito.it3由欧盟在FET -全球计算倡议、DART IST-2001-33477项目和MURST项目McTati内提供部分支助。供资机构不负责对本文所列结果的任何使用。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.0174F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21[7]以捕获持续的标准化术语和标准化术语。参见Dezani et al.[8]这是一个更完整的研究路线在本文中，我们关注的是λrec-演算，它是从标准λ演算中通过添加rec-抽象而获得的，根据语法：t：：= x|TT| λx。不|rec x. 不我们用Λrec表示这组项。再抽象的归约规则是(red-rec） recx. t→t [x：= recx. t]这个规则证实了rec x的直觉。t为λx的固定点。测试：recx. t =（λx. t）（recx. t）→t [x：= rec x. t]在某种意义上，我们的rec运算符可以被看作是Plotkin PCF [18]中的递归运算符和ML语言[15]中的定点运算符的无类型版本。在本文中，我们证明了相交类型对于构建λrec-演算模型是足够有表达力的，其中rec被解释为最小不动点算子。假设我们使用满足生成定理的合适的交集类型结构（我们将使用简单的结构），我们只需要向标准的类型分配系统添加由rec x的解释导出的自然规则。t是λx的最小不动点。t，以获得λrec演算的模型此类型规则为：r， x：AQt：BrQrecx. t：A（rec）rQrecx. t：B这种合理性来自于我们构建模型的目的，其中术语的解释是可以分配给它们的类型的集合。 因此，与规则（red-rec）一致，我们需要为rec x导出相同的类型。不并且t[x]=recx。t]。本文给出了一种关于Γ<$qt[x：=recx. B通常不会是其中结论是关于cx的次推导。t：Ai，对于somei∈I，因为rec x。t是t [x：= rec x]的子项。t]。我们可以很容易地将这种当A = byrule（λI）时，对Γ， x：AλQt：B的一个定义（参见定义2. 6）wegetrQrecx. t：A.i∈IAi. 此外一个自然的问题是，为什么我们没有简单地将rec解释为一个固定点组合子：我们将在结论中讨论这一点，因为它需要本文中介绍的一些符号约定Coppo在[4]中证明了交型指派系统中可分型的λ-项集恰当地包含可用ML分型的λF. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）35let规则[15]，关于将“let x = u in t“关联到“（λx. t）u如果我们将ML的定点运算符Fix映射到递归运算符rec，这种包容就不再成立了。实际上，Fix的ML类型规则是：（修正）r，x：At：Ax. t：A允许为所有类型A派生Fixx.x：A，而我们的规则（rec）允许为recx.x获取与通用类型等价的类型。这符合recx.x的解释是底部元素的要求请注意，Mycroft的letrec类型规则[16]，[9]甚至比规则（Fix）更宽松，然后它增加了递归项可导出的类型集。比较规则（rec）和（Fix），可以观察到规则（rec）不要求x和t是相同类型的，但它有一个要求条件，即x的类型必须对整个递归项rec x可导出。t. 这意味着递归项的每个类型派生都必须从总是通过给它赋一个通用的类型作为我们的建设的副产品，我们可以证明一个有趣的一致性结果有关简单的容易的条款。 粗略地说，一个简单易行的术语 是一个术语，可以通过适当地扩展（以保守的方式）类型上的前序来分配任意的交集类型。 键属性在扩展类型前序中，术语不接收“太多”类型。值得注意的是，简单的容易意味着容易：我们记得，根据雅科皮尼[12]，如果对于任何其他闭项u，理论λβ+{t=u}是相容的，则闭项t是容易的。 我们证明，给定任何简单的易项e，我们可以向微积分中添加可数数量的方程（e） t∈ Λ rec. e（λx. t）= rec x. 不并且所得的理论λrec+（εe）仍然是相容的。证明使用[1]的技术，该技术允许构建过滤器模型，该模型将简单术语的解释等同于合适的域运算符。这个由语义工具证明的一致性结果与λ-演算中基于使用语法工具的主流一致性证明形成对比（参见Kuper [13]及其参考文献）。至于语义工具的应用，我们可以提到Alessi等人的参考文献[1]。2交叉口类型分配系统交集类型是通过闭合给定集合而归纳构建的语法对象原子类型（基类型）加上函数类型构造函数→下的通用类型<$1和交集类型构造函数<$2。6F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21定义2.1[交集类型语言]设是可数的基类型集合。 上的交集类型语言，表示为=（ ），由以下抽象语法定义：=||→|- 是的符号：大写罗马字母，即A，B，.。. ，将表示任意类型。希腊字母α，β，. 将表示中的常数。在编写交集类型时，我们应使用以下约定：• 构造函数的优先级高于构造函数→;• 右为左为右。•i∈I Ai，其中I ={1，...， n}且n ≥ 1是（（. （A1A2）.. . ）An）;•i∈IAi，其中I=是。交集类型规则的大部分表达能力来自于这样一个事实，即类型可以被赋予一个满足图1中列出的公理和规则集q的前序关系≤，因此导出了一个关于的交半格的结构，顶部元素是。我们在这里回顾一下在Alessi和Lusin [ 2 ]中首次引入的易交类型理论的概念。在下文中，我们写A<$B作为A≤BB≤A的缩写。定义2.2[简单的交集类型理论]设=（）是一个交集类型语言。易交型理论（简称EITT）是所有可从q导出的判断A≤B的集合，其中Q是一组公理和规则，使得（我们写A <$B，对于A ≤ B &B ≤ A）：(i) Q包含图1所示的公理和规则的集合Q;（反式）A≤A（反式）A≤AJB≤BJA≤BB≤C（星期一）A<$B≤AJ<$BJ（同上）A≤A<$A（包括L）AB≤A（包括R）AB≤BAJ≤AB≤ BJ（→ A）（A→B）<$（A→C）≤A→B<$C（η）A→B ≤AJ →BJ（n）A≤n（n-η）n≤n → nFig. 1. 公理和规则的集合QF. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）37KHKKK(ii) Q−，定义为Q\Q，只包含以下两种形式的公理α≤αJ，αh∈H（h→Eh），其中α，αJ∈ ，h∈{(iii) 对于每个α∈，在Q−中恰好有一个形式为α∈的公理Eh）;h∈H（h→(iv) 设Q−包含α（h→E）和αjk∈K（2011年12月31日）→EJk ）. 然后Q−也包含α≤αJ当且仅当对于每个k∈K，存在hk∈H使得， E h ≤EJk都在Q−中。例2.3取={ω}和Q−={ωω→ω}，我们得到EITT。Honsell和Ronchi [11]证明了这个EITT导出了一个与Parkλ-模型[17]同构的滤波λ-模型（根据第3节给出的构造）请注意：(a) 由于由（π）和（π-η）得到的π∈ π（，Q），则可以得出，等价于合适的箭头类型（的交点）;(b) （modulo(c) 在上述定义EJ的最后一句中，和Ehk必须是恒定类型（但我们不用希腊字母表示它们，因为这是一个推论，而不是一个假设）。记法：当我们考虑一个EITT（，Q）时，我们将写Qfor，Qfor（）和q为（，Q）。此外，A≤QB将是（A≤B）∈ <$Q的缩写，并且A<$q B是A≤QB≤QA的缩写。 我们将考虑类型的句法等价“ ” ， 直 到 的 结合 性 和 交 换 性 。EITT的一个很好的特性是箭头交叉点之间的顺序与阶跃函数连接之间的顺序一致。这个性质，它意味着所有连续函数在诱导滤波器λ-模型中的可表示性（见第3节），并在[8]的第2节中得到充分解释，依赖于下一个定理，其证明可以在[1]中找到h∈H8F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21i ii∈Ii iQ定理2.4对任意的I，且A，B，C，D∈Q，（A→B）≤C→D，如果且仅当i∈JBi≤QD，其中J={i∈I|C≤QAi}。注意，在定理2.4的陈述中，集合J可以是空的，在这种情况下，我们得到QD。在给出交叉型分配系统的关键概念之前，我们介绍了基和一些相关的定义。F. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）39定义2.5[基]Q-基是一组（可能无限）形状为x：A的语句，其中A∈Q，所有变量不同。我们将使用以下表示法：(i) x∈Γ是（x：A）∈Γ的简称;(ii) 如果Γ是Q-基且A∈Q，则Γ，x：A是Γ∈{x：A}的简称，当x∈/Γ;(iii) 设Γ和ΓJ是Q-基. Q基Γ Γ J定义如下：Γ Γ J={x：A<$B|x：A∈Γ且x：B∈ΓJ}{x：A|x：A∈Γandx∈/ΓJ}{x：B|x：B∈ΓJ和x∈/Γ}。定义2.6[类型赋值系统]相对于EITT_Q的交集类型赋值系统，记作λ_Q，是一个形式系统，用于导出r_m_q_t：A的判断元素，其中主语t是一个单位元dλ-t_m，谓语A在Q中，且r是一个Q-基。它的公理和规则是：（x：A）∈Γ（Ax）Γ<$Qx：A（Ax-ε）ΓεQt：εr， x：A<$Qt：B（→I）Γ<$Qλ x. t：A→B（→E）ΓQt：AΓQt：BrQt：A→BrQu：AQtu：BrQt：AA≤QB（一）Γ<$Qt：A<$B（≤Q）Qt：B（rec）r， x：AQt：BrQrecx. t：ArQrecx. t：B例2.7λx项在所有λ<$Q中，xy可以很容易地被类型化，如下面的推导所示（为了空间的缘故，我们称E为类型λ →A）x：E，y：Qx：Ex：E，y：Qy：（→E）x：E，y：qxy：Ax：EQrecy. xy：0x：EQrecy. xy：A（→I）►Qλx。接收器y.xy：E→A（rec）10F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21注意，由于公理（Ax-λ）的存在，可以在不假设所有自由变量的类型的情况下对项进行F. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）311通常我们考虑λ-项模α-转换。请注意，区间消除规则（英）联系我们Qt：A联系我们Qt：B在任何λ<$q中都是可导的此外，下列规则是可以接受的：r，x：A，t：BAJ≤A（W）（≤μL）Γrt：Bx∈/Γr，x：Art：Br，x：AJt：BΓ， x：A<$t：Bx∈/F V（t）（S）联系我们在给出生成定理之前因此，在对导子进行归纳证明时，我们需要考虑我们应用规则（rec）的次数。定义2.8给出了判决函数f x的一个导数D。t：A，ν（D）是D中规则（rec）的应用次数，其中rec x。作为结论的主体注意，ν（D）没有考虑（rec）对作为结论主题的项的适当子项的下面的生成定理的前四点已经在[1]中给出;最后一点表征rec项可以很容易地通过导子的归纳来检查。定理2.9（生成定理）(i) Asoul A /soul A/soula. 证明了Γ≠qx：A当且仅当（x：B）∈Γ且B≤qA对于某个B∈Q;(ii) Γ<$Qtu：A当且仅当Γ<$Qt：B→A，且对某些B∈Q;(iii) Γ<$Qλ x. t：A当且仅当Γ， x：B►Qt：C和（B→C）≤ A，我对某些I和Bi，Ci∈Q;ii∈Ii iQ[4]回想一下，如果对于规则的每一个实例，在系统中存在从其前提推导其结论的演绎，则规则在系统中是可导出的。一个规则在系统中是可容许的，如果对于该规则的每个实例，如果它的前提在系统中是可导出的，那么它的结论也是可导出的。12F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21(iv) Γ<$Qλ x. t：B→C当且仅当Γ， x：B<$Qt：C;(v) 设A/q. 导数D是Γ-Εrx的导数。t：A当且仅当存在非空集合I、导子Di和类型Ci、Bi，即：• 对任意i∈I，Di是D的具有约束的超导数，其中r ∈ {\displaystyle r}为函数x。测试：Bi;• i∈I. r， x：Bi，Qt：Ci;•i∈ICi≤QA;•i∈Iν（Di）+|我|= ν（D）.注意，在前面定理的（i）和（v）点中，我们必须假设A/，否则我们可以导出x：和rec x。t：仅使用公理（Ax-θ）。定理m2.10（Substitution引理）Γ <$qt[z：=u] ：A当且仅当存在D∈Q使得Γ， z：D<$qt：A和Γ<$qu：D.证据（1）是生成定理的一个推论，它是由t的结构上的归纳推理得出的。我们只考虑trecx的情况。v.我们对ν（D）作进一步的归纳，其中D是Γ-Εr_x的导数. v：A.若ν（D）= 0，则A，命题是平凡的。 否则，一般来说，定理，点（v），存在I，Di，Ci，Bi，使得(i) 对任意yi∈I，Di是Γ， z：D∈Qrecx在D中的次导数。v：Bi;(ii) i∈I. r， z：D，x：Bi，Qv：Ci;(iii)i∈ICi≤QA;(iv)i∈Iν（Di）+|我|= ν（D）.将ν（D）上的归纳应用于（i）和项上的归纳应用于（ii），我们有，对于任何i∈I，• rQrecx. v[z：=u]：Bi;• r， x：Bi，Qv[z：=u]：Ci。在对最后两个判决的应用中，我们有一个很好的判决。v[z：=u]：Ci，其中nyi∈I. By（iii），规则（？I）和d（≤Q）都是r∈Qrecx. v[z：=u]：A.（10）我们再次通过归纳法对t的结构进行推理，在t = recx的情况下，使用v（D）上的嵌套归纳法。v.我们只考虑应用和递归两种情况。 Le tttt[z=u]：A，其中ttt=1t2。By一般情况下，在定理（ii）中，有X是AJ，满足h_i=1[z：= 1]。u] ：AJ→A， r=qt2[z：=u] ：AJ. 通过引入，存在类型D1、D2，使得：- Γ， z：D1<$qt1：AJ→A;F. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）313- r， z：D2Qt2：AJ;rQu：D2.根据规则（I），我们得到ΓQu：D1<$D2。根 据 规则（≤λL ） ，我们有一个ver， z ： D1<$D2<$qt1 ： AJ→A 和r， z ：D1<$D2<$QT2：AJ. 通过应用（→E）i如下r， z：D1<$D2<$qt1t2：A. 通过选择DD1D2，完成了此情况下的程序。LetD是对r∈Qt[z：=u] ：A的一种推导，其中cx为零。v.我们通过对ν（D）的归纳来证明。如果ν（D）= 0，则A且可以选择D。否则，根据生成定理，点（v），存在I，Di，Ci，Bi，使得：(i) 对任意yi∈I，Di是Γ_（？）q-反应c_x在D中的次导数. v[z：=u]：Bi;(ii) i∈I. r， x：Bi<$Qv[z：=u]：Ci;(iii)i∈ICi≤QA;(iv)i∈Iν（Di）+|我|= ν（D）.对（i）应用归纳法，对任意yi∈I，x∈Disuchthatr， z：DiQrecx. v：Bi和ΓQu：Di。将归纳法应用于（ii），对于任何yi∈I，existDJsuchth a tr， z：DJ， x：BiQv：Ci和rQu：DJ。LetD我我我Ji∈I（Di<$Di）. 根据规则（≤L），它如下：• i∈I. r， z：DQrecx. v：Bi和Γ_（？）Qu：Di;• i∈I. r， z：D，x：BiQv：Ci.应用规则（rec），接着规则（rec I）和（≤recL），并使用规则（iii），我们得到了r， z：D∈recx. v：A. 将规则（RUI）应用于关于u的判决，我们可以得到r_Qu：D_i 。D.Q我们以替换引理的一个重要结论结束本节，即关于规则（red-rec）的类型赋值的不变性：一个类型对于rec x是可导的。t当且仅当它对于t [x：= rec x是可导的。t]。Pro posi tion2.11rQrecx. t：A当且仅当r∈Qt[x：=recx. t]：A.我的律师。 （3）SupposerQrecx. t：A. 根据遗传定理，poi nt（v），存在xi，Bi，Ci，使得对任意yi∈I，r∈cx。t：Bi，Γ， x：：Bi<$Qt：Ci且m或eoveri∈ICi≤QA. 利用替换引理对于任意i∈I ， r∈qt[x：=recx. t] ：Ci，因此，使用（I）和（≤L），我们gtrQt[x：=recx. t]：A.（3）SupposerQt[x：=recx. t] ：A. 利用代换引理，证明了存在有一个Γ-正则表达式cx的D. t：D和r， x：D<$Qt：A。通过应用规则（rec），我们可以在r_（？）Q_（？）t：A.Q14F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21ρ3滤波器模型在进入如何从交集类型构建模型的细节之前，我们必须关注λrec演算模型的精确概念。实际上，我们从λ-modela'l a Hindley-Longo（see[10]）的cl a s i c a l定义开始，进一步的条件迫使对recx的解释。t为λx的固定点。t.定义3.1[λrec-calculus的模型]λ rec-calculus的模型由一个三元组D，·，[[]]D组成，使得D是一个集合，·：D×D→D，Env：V ar→D，解释函数[ ]D：Λ×Env→D满足：（一） [x]]D=ρ（x）;(ii)[tu]]D=[[t]]D·[[u]]D;ρ ρ ρ(iii) [λx. t]]D·[[u]]D=[[t]]DD;ρ[x：=[[u]]ρ](iv) 若对任意x∈FV（t），ρ（x）=ρJ（x），则[t]]D=[[t]]D;ρ ρJ(v) I f y∈/FV（t），n[λ x. t]]D=[[λ y. int[x：=y]]D;(vi) 如果d∈D.[[t]]Dρ=[[u]]Dρ，则[λx. t]] D=[[λx. ]]numb;ρ[ x：= d](vii) [rec x. t]]D=[[t]]Dρ[x：=d]ρ ρD.ρρ[X：=[[recX. t]]ρ]当nx∈FV（t）时，模D，·，[[]]D是外延的[[λx. tx]] D=[[t]] D。ρ ρ我们现在讨论如何从类型理论中构建λ模型。 我们从定义过滤器开始。 然后我们展示如何把空间 过滤器变成一个实用的结构。我们定义了从滤波器空间到其连续函数空间的连续映射，反之亦然。由于这些映射的合成是恒等式，我们得到标准λ-模型（滤波器模型）。递归项的解释，然后通过使用最小不动点算子。定义3.2[过滤器](i) 一个Q-滤波器（或Q上的滤波器）是一个集合X<$Q，使得：• n ∈X;• 若A≤QB且A∈X，则B∈X;• 若A，B∈X，则A<$B∈X;(ii) FQ表示Q上的Q-滤子的集合;(iii) 如果X<$Q，则↑QX表示由X生成的Q滤波器;(iv) 一个Q滤子是主滤子，如果它的形状是↑Q{A}，对于某个类型A。我们将↑Q{A}简单地表示为↑QA。F. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）315FFF众所周知，FQ是一个ω-代数格，它的紧（或有限）元的偏序集同构于通过将q上的前序用Q表示而得到的逆偏序集。这意味着紧致元是对于某个类型A的形式为↑ q A的滤波器，顶部元素是Q，底部元素是↑Q。此外，两个滤波器的并是由它们的并诱导的滤波器，两个滤波器的交是它们的交集，即：XHY= ↑Q（X<$Y）XHY = XY。F的关键性质是在ω-代数完备格和Scott-连续函数范畴中是自反对象。这一点通过赋予过滤器的空间以应用的概念而变得清晰，从F_ q到它的函数空间[FQ→FQ]的连续映射和向量空间a.定义3.3[应用](i) 应用：FQ× FQ→FQ定义为X·Y ={B| <$A∈Y. A→ B∈X};(ii) 连续映射FQ：FQ→[F Q→F Q]和GQ：[FQ→F Q]→FQ定义为：FQ（X）=λY∈FQ.X·Y;GQ（f）=↑Q{A → B |B∈f（↑QA）}.请注意，前面的定义是合理的，因为很容易验证X·Y是Q滤波器。正如所预料的那样，FQ和GQ是彼此相反的：依赖于定理2.4的证明在[1]中给出。引理3.4FQGQ =id[FQ→FQ];GQ<$FQ= idQ.我们现在可以解释λrec演算了。 设EnvQ是Env q上从项变量集到F q和ρrange的所有映射的集合。设fix为最小不动点算子，即：• <$X∈FQ. X·（fix（X））= fix（X）;• <$X，Y∈FQ.X·Y=Y<$fix（X）<$Y.16F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21ρρρ[ X：= x]Fρ[[x]]Q=p（x）;[[tu]]Q=FQ（[[t]]Q）（[[u]]Q）;ρ ρ ρ[[λ x. t]]Q =GQ（λX∈FQ. [[t]]Q）;[[recx. t]] Q=fix（[[λ x. t]]Q）。ρ ρ图二. λrec项的解释通过映射FQ和GQ，Figure 2定义了λ rec -项在[[]]Q中的一个新的映射：Λrec×EnvQ→FQ.众所周知，引理3.4意味着FQ诱导一个扩张λ-模型，因为它是ω -的carnival闭范畴中的自反对象。代数格，因此定义3.1中的所有方程都成立，但对于（vii），紧接着定义不动点算子。下一步是将上面的解释的抽象概念与类型赋值系统联系起来。更具体地说，我们想证明，对于任何EITTQ，λrec项t和环境ρ，我们有[[t]]Q={A∈Q|∃Γ|=ρ。{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}{{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}其中，符号Γ |= ρ意味着如果（x：B）∈Γ则B∈ρ（x）。鉴于此，我们需要将fix描述为过滤器。 引理3.4意味着每一个“高阶”空间都可以通过定 义 经 由 F Q 和 G Q 的 标 准 适 当 映 射 ， 以 规 范 的 方 式 嵌 入 F Q。例 如 ，为了 加 快 fix 的速度 ， 在[[F Q→F Q]→FQ]中，我们考虑映射HQ：F Q→[[F Q→F Q ] → F Q]和KQ：[[F Q→F Q]→Fq ]的p空气，定义如下：HQ（X）=FQ（X）<$GQ，KQ（H）= GQ<$λX. （H<$FQ）（X）.很容易检查，（q）HQ ◦ KQ=id[[FQ→FQ]→FQ]→[[FQ→FQ]→FQ]。我们认为有一个算子H∈[[FQ→FQ]→FQ]，如果HQ（X）= H.等式（q）保证每个H都由KQ（H）表示。给定任意的EITT_Q，我们现在研究一个特殊的滤波器，称为_Q，它首先在[1]中引入，其中_Q被证明是表示fix算子的Q-滤波器（见定理3.7）。F. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）317nn00nn0n定义3.5[过滤器]LetQanEITT. 对于所有itegersn，setsΦQ而滤波器则由互感定义如下：Q={}QΦ Q={C→A| <$B. C→B∈ <$Q&C≤QB → A}<$Q=↑QΦQ;= ↑QΦ Q。n+1个nn+1n+1个我们定义了Q=我的天例如A→A ∈ΦQ，（A→A）→A∈ΦQ，（A→A0）<$（A0→A1）→1 2A1∈ΦQ，且（φ →A0）φ（A0→ A1）φ. <$（An−1→An）→ An∈ΦQ为所有3A，A0，.，An.n+2的现在我们给出一个关于ΦQ，φQ的有用引理，它刻画了箭头n n类型在ZEROQ。引理3.6（i）对于所有n > 0，我们有C→A∈ΦQ⇔C→ A∈ <$Q。(ii)对于所有n≥0，我们有C → A∈Q惠B，.，B . C≤（B→B）n0nQ0≤i≤n−1i一期+1& B0q&BnA。证据 （1）在[1]中证明。 （ii）的证明是通过对n的归纳。对于n= 0，我们有：C→A∈Q惠≤QC→A通过定义Q0 0用公理（θ）和（θ-η）证明惠θ →θ≤QC→A由定理2.4和规则（η）得到的惠A≤QA由公理（axiom）表示的惠益定理。这正是基本的情况，考虑到空的交叉点等同于，并选择B0A。Φn18F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21n+1个n+1个nn+1个ρρρρρ我们证明了n+1的命题。C→A∈H惠C→A∈ΦQ（一）优惠券B. C→B∈Q&C≤QB→ A根据ΦQ的惠誉B，B0，.，Bn.C≤Q0≤i≤n−1（Bi→Bi+1）&B0<$Q<$Bn<$BC≤QB→A通过感应⇔ B0，.，Bn. B0 q&C≤Q（0≤i≤n−1（Bi→Bi+1））<$（Bn→A）规则（mon），（transs）和公理（idem），（inclL），（inclR）。证据是如此完整。Q在[1]中证明的最重要的性质是：定理3.7滤波器φ Q表示最小不动点算子，即Q= HQ（fix）。通过滤波器fixq刻画fix是证明下一个结果的基础定理3.8[[t]]Q={A∈Q|∃Γ|=ρ。 {\displaystyle{\frac{A}。证据通过对λrec项的归纳，使用生成定理2.9。除rec-项的情形外，所有情形都在[1]中得到了证明当考虑到这一点时，t，通过特征化[recx. t]]Q=Q·[[λ x. 我们有一个问题：λ x. t]]Q={A∈Q|∃Γ|=ρ。 rQrecx. t：A}。首先我们证明（b） Q·[[λ x. t]]Q={A|B0. . . . Bn，Γ|=ρ。B0qBnA& Γ， x：Bi<$Qt：Bi+1（0≤i≤n−1）}。F. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）319ρ事实上我们是λ x. t]]Q={A|[λ x. t]]Q. C→A∈<$Q}ρ ρ根据应用={A|C，Γ|= ρ。 Γ<$Qλ x. t：CC→A∈<$Q}通过感应={A|C，Γ|= ρ。 Γ<$Qλ x. t：C&n，B0. . . Bn.C≤Q0≤i≤n−1（Bi→Bi+1）B0<$Q<$Bn<$A}通过定义Lemma 3.6（ii）和Lemma3.6（ii），={A |B0... Bn，Γ |= ρ。 B0<$Q<$&Bn<$A&Γ<$Qλ x。t：Bi→Bi+1（0≤i≤n−1）}按规则（≤Q）={A |B0... Bn，Γ |= ρ。 B0q&BnA&Γ， x：Bi<$Qt：Bi+1（0≤i≤n−1）}根据生成定理（定理2.9（iv））。我们现在检查双重包含。定理：我们用i上的归纳法证明了Γ≠Q∈Cx。t：Bi，0≤i≤n。基本步骤是微不足道的，因为B0Q。对于归纳步骤，它可以应用规则（rec）：Γ， x：BiQt：Bi+1ΓQrecx. t：BirQrecx. t：Bi+1我们得出了r_（？）r_（？）t：AsinceBnA.证明：这个证明是通过对ν（D）的归纳，其中D是Γ<$Qrecx的导子。t：A.基础条件p ν（D）=0是理想的。对于归纳步骤，我们从生成定理（定理2.9（v））得到，存在J，Dj，Ej，Dj，使得：(i) 对任意yi∈J，Dj是D在Γ_（？）q-反应c_x上的带闭集的次导数。t：Dj;(ii) j∈J. r， x：Dj<$Qt：Ej;(iii)j∈JEj≤qA;(iv)j∈Jν（Dj）+|J|= ν（D）.From（i）和d（iv）可由归纳Dj∈λQ·[[λ x. t]]Q对所有i∈J. 这20F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21由（b）表示，存在n，B（j）. B（j）使得B（j）≠ D，B（j）≠ Dj0n j0Q njj且Γ， x：B（j）<$Qt：B（j）（0≤i≤nj−1）。再次使用（ii）和（b），i i+1Ej∈ <$q·[[λ x. t]]Q，s，则得到eA∈<$Q·[[λ x. t]]Q来自（iii）bei ng<$Q·[[λ x. t]]Qρ ρ ρaQ-过滤器。Q最后，我们展示了以下一致性结果：给定任何简单的项e，我们可以在微积分中加入可数的方程（e） t∈ Λ rec. e（λx. t）= rec x. 不并且所得的理论λrec+（εe）仍然是相容的。我们回顾一下在[2]中首次给出的简单易行术语的定义。如果我们能强迫一个项的解释被任意的主滤波器精确地扩展，那么这个项就是简单的。更准确地说，如果给定一个EITTq，和一个类型Z∈Q，我们可以用保守的方式将<$Q推广到EITT<$QJ，soth a t[e]]QJ=（↑QJZ）H [[e]]Q.首先介绍了EITT映射：将EITT映射应用于易交型理论，并应用于一个型，建立了一个新的易交型理论，它是原易交型理论的保守推广。定义3.9[EITT图](i) 设Q和q为两个EITT。 我们说，QJ是保守扩张，（记作<$Q±<$QJ）当且仅当Q<$QJ且对所有A，B∈Q，A≤QB当且仅当A≤QJB;(ii) 一个点EITT是一个对（Q，Z），其中Z∈Q;(iii) 一个EITT映射是一个映射M：PEITT›→EITT，使得对于所有的（n，Q，Z）Q±M（其中EITT和PEITT分别表示EITT和pointed的类，埃特山定义3.10[简单易项]一个不可解项e是简单易项，如果存在一个EITT映射Me，使得对于所有的点EITT（EITT，Z），►QJe：B如果且o如果<$C∈Q.C<$Z≤QJB<$Qe：C，其中，N=Me（N，Z）。将I<$λx.x、W2<$λx.xx、W3<$λx.xxx和Rn归纳定义为：R0=W2W2，Rn+1=RnRn. 简单易词的例子有W2W2，F. Alessi，M.Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）321W3W3I，且Rn对所有n [2]。Lusin [14]给出了简单易行项的进一步例子这里有用的简单易项的性质是（证明见[1]）：定理3.11设e为简单易项。则存在一个非平凡的滤波器模型FQ，使得e的解释是最小不动点算子。我们可以得出结论：定理3.12设e为简单易项。则存在一个非平凡的滤波器模型FQ，使得e（λx. t）和recx. 对于所有t∈ Λ rec，t重合。推论3.13设e为简单易项。则理论λrec+（εe）是相容的。4结论最后，我们证明了明确引入术语rec x的决定。不并且不解释mby[Y（λ x. t）]]Q用于somedpo intcombinatorY. 第一个原因是类型分配系统的平滑性：rec x的类型。t对于将类型派生到Y（λx）的规则的繁琐应用是非常简单的。t）。作为第二个，也是更重要的原因，rec x的可能解释。t是λx的最小不动点。t不能被一个年轻人抓住了。事实上，这是一个无法修复的问题，使得[[Y]]Q表示用于在eachflmodelF Q中操作算子FIX 的最小固定点。事实上，考虑滤波器模型FPark同构于Parkλ-模型DParkλ-演算（见例2.3）。如[11]中所证明的，对于所有闭λ-项t，[[t]]Park在与底部元素不同的某个紧元素c之上特别地，对于所有固定点组合子Y，[[YI]]Park在c之上，其中I是单位组合子。由于fix（λX.X）显然是底部元素，我们知道HPark（[[Y]]Park）不可能表示fix，因为HPark（[[Y]]Park）（λX.X）=（FPark（[[Y]]Park）<$GPark）（λX.X）=FPark（[[Y]]Park）（GPark（λX.X））=[[Y]]Park·[[I]]Park= [[YI]]Park±c其中利用了如下公式：[I]Q=GQ（λX. X）对于所有的 DQ。22F. Alessi，M. Dezani-Ciancaglini/理论计算机科学中的电子笔记136（2005）3-21致谢作者感谢Furio Honsell就本论文的主题进行了富有启发性的讨论，并感谢裁判仔细阅读和提出有用的建议，这些建议大大改善了论文的介绍。引用[1] Fabio Alessi，Mariangiola Dezani-Ciancaglini和Stefania Lusin。交集类型和域运算符。理论计算。Sci. ，316（1[2] 法比奥·阿莱西和斯特凡尼亚·卢辛。简单的条款。在Ste Escheren van Bakel，编辑，IntersectionTypes and Related Systems ， 第 70 卷 Electronic Lecture Notes in Theoretical ComputerScience。Elsevier，2002年。[3] Henk Barendregt，Mario Coppo，and Mariangiola Dezani-Ciancaglini. 一个过滤器lambda模型和类型赋值的完备性。J. Symbolic Logic，48（4）：931[4] 马里奥·科波应用语言的扩展多态类型系统。在Piotr Dembinski，编辑，MFCS史普林格出版社[5] Mario Coppo和Mariangiola Dezani-Ciancaglini λ-演算的基本泛函理论的一个推广。Notre DameJ. Formal Logic，21（4）：685[6] Mario Coppo，Mariangiola Dezani-Ciancaglini，and Bet
我的内容管理
展开
