参数多态性的双泛函语义及其性质验证-斯特拉斯克莱德大学和阿巴拉契亚州立大学的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记319（2015）165-181www.elsevier.com/locate/entcs参数多态性的双泛函语义尼尔·加尼，帕特里夏·约翰，Fredrik Nordvall Forsberg，Federico Orsanigoa和Tim Revellaa英国斯特拉斯克莱德大学b美国阿巴拉契亚州立大学摘要Reynolds在语义上，自相关图范畴和纤维化都被认为是对参数多态性的分类理解。本文通过展示双标的相关性，进一步促进了这一范畴视角。我们为参数化的系统F的模型开发了一个双虚构框架，因为它们验证了恒等扩展引理和雷诺兹抽象定理。我们还证明了我们的模型满足预期的性质，如初始代数和最终余代数的存在性，以及参数性意味着非自然性。关键词：参数化，逻辑关系，系统F，固定范畴理论。1介绍Strachey [30]称多态函数为参数函数，如果它的行为在所有类型实例中是一致的。Reynolds [25]通过公式化关系参数化的概念使其在数学上精确，其中参数多态函数的一致性通过要求它们保留实例化类型之间的所有逻辑关系来捕获。关系参数性已被证明是正式建立软件系统属性的关键技术，例如表示独立性[1，6]，程序之间的等价性[15]，以及关于程序的有用（在本文中，我们处理多态λ-演算系统F [10]的关系参数 性， 它构 成了 许多 现代 编程 语言 和验 证系 统的 核心Hermida 、Reddy 和Robinson [14]很好地介绍了关系参数性。由于范畴论支持并告知了现代编程语言的许多关键思想，因此很自然地会问它是否也可以提供关于参数化的有用观点马和雷诺兹[19]开发了第一个http://dx.doi.org/10.1016/j.entcs.2015.12.0111571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。166N. Ghani等人/理论计算机科学电子笔记319（2015）165它们的模型复杂，难以理解。此外，Birkedal和Rosolini发现，并非所有参数性的预期后果都必然在他们的模型中成立（见[4]）。另一种工作是由O'Hearn和Tennent[ 21 ]以及Robinson和Rosolini [ 28 ]开始的这是参数多态的函子语义的最新技术。将类型解释为函子在概念上是优雅的，Dunphy和Reddy表明这个框架足够强大，可以证明预期的结果，例如严格正类型表达式的初始代数的存在性[5]。然而，由于自反图范畴是相对未知的数学结构，这种发展的大部分不得不从头开始相反，我们建议从一开始就采用更成熟的逻辑虚构观点，从而分析参数通过范畴类型理论的强大镜头[16]。在这样做时，我们遵循Hermida [12，13]和Birkedal和Møgelberg [4]的广泛工作，他们使用纤维化来构建复杂的范畴模型，不仅是参数性，而且是其逻辑结构的Abadi-Plotkin逻辑[24]。Abadi-Plotkin逻辑是参数多态的形式逻辑，包括谓词逻辑和多态lambda演算，因此需要大量的机器来处理。使用这种机制，Birkedal和Møgelberg能够超越邓菲和雷迪的结果，例如，证明所有积极的类型表达式-而不仅仅是严格积极的邓菲和雷迪-有初始代数。然而，这些令人印象深刻的结果是以所涉及的概念的复杂性为代价的。我们的目标是在一个更简单的设置1中实现相同的结果，更接近Dunphy和Reddy的函子语义。我们最终得到了模型的概念，其中每个类型都被解释为一个保持相等的函数，每个项都被解释为一个函数自然变换。这与Robinson和Rosolini [28]的参数完备过程产生的模型（也参见Birkedal和Møgelberg[4，第8节]）以及Mitchell和Scedrov因此，我们将Birkedal和Møgelberg的虚构模型的一般性与Dunphy和Reddy的函子语义的简单性结合起来我们的核心创新是使用双振动来实现参数性研究中的“最佳点”。这对于我们的框架的定义来说是不必要的，因为Lawvere等式[17]（即，opreindexing沿对角线只）表面，但它有助于显着的具体解释的类型[9]和图形关系的处理。在技术层面上，我们最强的结果是使用我们更简单的框架来恢复Birkedal和Møgelberg [4]使用Abadi-Plotkin逻辑证明的参数性的所有预期后果。特别是，我们超越Dunphy和Reddy然而，本文绝不是要作为虚构的最后一句话。[1]我们再次强调，我们并不是试图对所有的Abadi-Plotkin逻辑建模，而是只对涉及参数多态的类型系统建模。事实上，关于阿巴迪-普洛特金逻辑，我们不可能希望改进Birkedal和Møgelberg [4]的结果，他们给出了一个声音和完整的语义。N. Ghani等人/理论计算机科学电子笔记319（2015）165167§参数性相反，我们希望我们在这里所做的参数性的简单重新概念化-将类型作为函子和术语作为自然变换的通常分类解释替换为它们的对应物-将为在更丰富的环境中研究参数性开辟道路，例如，相关证据论文的结构：在第2节中，我们简要介绍了双振动。我们回顾第3节中Reynolds然后，我们在第4节中提取这些的双对数概化，并构建我们的参数模型。在第5节中，我们通过导出所有可定义函子的初始代数并证明参数性蕴涵（di）自然性，证明了我们的模型表现出预期的行为。最后，我们在第6节中实例化我们的框架，以导出第7节总结并讨论了未来的工作。2关系参数性我们简要介绍了纤维化;更多细节可以在，例如，[16 ]第10段。定 义2.1设U ：E → B 是函子。 一个态射g：Q→P在 E中是在f ：X→Y在B中 的carrierover，如果Ug=f，并且对于每个gJ：QJ→P在E中满足UgJ=f<$v，对于某个v：UQJ→X，存在唯一的h：QJ→Q满足Uh=v和gJ=g<$h。 一个态射g：P→Q在E中是在f ： X→Y 在 B 中 的 opcarnival ， 如 果 Ug=f ， 并 且 对 于 每 个 gJ ： P→QJ 在 E 中 满 足UgJ=v<$f，对于某个v：Y→U QJ，存在唯一的h：Q→QJ满足Uh=v和gJ=h<$g。我们写的是P§对于f上具有余域P的Carnival态射，且fP§ 为域P上f上的opcarnumerical态射这样的态射是唯一的，直到同构如果P是E的一个对象，那么我们把fP的定义域写成f P，对于f P的余域，§和定义2.2函子U：E → B是纤维化，如果对于E的每个对象P和B中的每个无向态射f：X→UP，存在一个无向态射fP§ ：Q→P在E上除以f。 类似地，U是一个运算，如果对于E的每个对象P和每个态射，f：UP→Y在B中，有一个opcarnumerical态射fP：P→Q在E中在f上。一函子U是双纤维化，如果它既是纤维化又是操作纤维化。如果U：E → B是一个纤维化、opfibration或bifibration，那么E是它的总范畴，B是它的基范畴。E中的对象P在它的像UP上，对于态射也是如此。一个态射是垂直的，如果它在id上。我们将B中的对象X上的纤维写为EX，即，E的子范畴的对象在X和态射在IDX。对于B中的f：X→Y，将E的每个对象P映射到fP的函数扩展到a函子f∈：E§Y→§EX映射each态射k：P→§ PJ在EY中到态射其中kfP=fP′fk。fP′的普适性保证了fk的存在唯一性。我们称f为沿着f的重索引函子。类似的情况对于运算也成立;将E的每个对象P映射到f的函子f：EX→ EY是沿着f的运算索引函子。168N. Ghani等人/理论计算机科学电子笔记319（2015）165∗我们写|C|对于离散范畴C.如果U：E → B是一个函子，则离散函子|U|：|E| → |B|由U的限制引起，|E|. 若n∈N，则En表示E在Cat中的n重积.U的n重积，记为U n：E n→ Bn，是由U n（X1，...， X n）=（UX1，...， UX n）。引理2.3如果U：E → B是函子，则|U|：|E| → |B|是一种双纤维化。 如果U是一个（双）纤维化，那么U n也是：对于任何自然数n，E n → Bn。Q为了明确地表述雷诺兹集合上的关系的关系和集合上的关系纤维化[16]。定义2.4范畴Rel有三元组（A，B ，R）作为对象，其中A，B，R是集合，R<$A×B。一个态射（A，B，R）→（AJ，BJ，RJ）是一个对（f，g），其中f：A→AJ，g：B→BJ，使得如果（a，b）∈R则（fa，gb）∈RJ。当A和B不重要或从上下文中清楚时，我们写（A，B，R）为R。注意，Rel不是对象是集合且态射是关系，有时也出现在文学作品中。每个集合A都有一个相关的等式关系，由等式A ={（a，a）|a∈ A}。例2.5将（A，B，R）发送到（A，B）的函子U：Rel → Set × Set称为Set上的关系纤维化。为了证明U确实是一个纤维化，令（f，g）：（X1，X2）→（Y1，Y2）是Set × Set中的态射，其中UR =（Y1，Y2），对于Rel中的某个R。若定义（f，g）<$R<$X1×X2为（x1，x2）∈（f，g）<$R i <$（fx1，gx2）∈R，则（f，g）是（f，g）上从（f，g）R到R的一个同态.也很容易看出U是一个opfibration，opreindexing由forward image给出。所以，U是一个双纤维化。我们用Rel（A，B）表示Set上的关系Fibration中的（A，B）上的Fibre。定义2.6设U：E → B和UJ：EJ→ BJ是泛函。一个有限函子F：U→UJ由两个函子F0：B →BJ和F1：E →EJ组成，使得UJF1= F0U，并且保持carnival态射，即， 如果f在E中的平方超过g在B中的平方，那么F1f在EJ中 的 平 方超过F0g在BJ中的平方。如果FJ：U→UJ是另一个有限函子，则有限自然变换η：F→FJ包含两个自然变换η0：F0→F0J和η1：F1→F1J，使得UJη1=η0U。在本文中，我们使用fibred函子和fibred变换来解释系统F的类型和项，并表明在温和的条件下，这给出了参数模型。3Reynolds我们现在描述雷诺正如雷诺兹发现的那样，如果元理论是经典逻辑[26]，那么实际上就没有集合论模型，但是下面的内容在topos的（直觉主义的）内部语言中是有意义的[22]，或者在具有非谓词集合的构造演算中是有意义的。在本文中，我们假设系统F的标准语法N. Ghani等人/理论计算机科学电子笔记319（2015）165169C3.1类型的语义Reynolds为System F提出了两种给定类型，其中类型上下文Γ包含|Γ |= n型变量，Reynolds定义解释[[T]] o：|设置|n→Set和[T]] r：|Rel|n（A，B）→Rel（[[T]] oA，[[T]] oB），通过结构归纳法进行类型判断，如下所示：• Typevai ables：[Xi]]oA=Aiand[Xi]]rR=Ri• 箭头类型：[[T1→T2]]oA=[[T1]]oA→[[T2]]oA[[T1→ T2]] rR ={（f，g）|（a，b）∈ [[T1]] rR <$（fa，gb）∈ [[T2]] rR}• 对于所有类型：[[X.T]] oA ={f：[[T]] o（A，S）|<$RJ∈ Rel（AJ，BJ）. （f AJ，f BJ）∈ [[T]]r（Eq A，RJ）}S：设置[[X.T]] rR ={（f，g）|<$RJ∈ Rel（AJ，BJ）. （f AJ，gBJ）∈ [[T]] r（R，RJ）}[[X.T]]o和[X.T]]r的定义相互依赖因此，我们实际上并没有两个语义--一个基于Set，一个基于Rel--而是一个基于关系纤维化U：Rel→Set×Set的单一语义。在其他方面，Reynolds定理3.1（类型的纤维化语义）设U是集合上的关系纤维化。每 一个判断Γ T诱导一个有限函子[[T]]：|U ||→ U。|→ U.|Γ|| Γ|[[T]]r¸Rel|Γ||Γ|C|设置|Γ|U||Γ|¸Set|×|设置[[T]]o×[[T]]o×设置Q由于[T]]r的定义域是一个离散范畴，要求[T]是一个有限函子就等于要求上面的图是可交换的。特别地，不需要通过[T]]r来 雷诺兹不给类型对态射的函子作用。这反映在定理3.1中离散范畴的出现上。因此，Reynolds对函数空间的逐点解释是函子范畴中的指数解释|U|| → U [ 27 ]。|→ U [27].参数性如何处理对态射的作用将在5.1节中变得清楚;类型的解释作用于由态射诱导的图关系，而不是作用于态射。现在，我们简单地注意到，离散域的使用并没有使我们脱离纤维化框架;引理2.3确保[T]]是纤维化之间恒等式扩展引理（IEL）是许多170N. Ghani等人/理论计算机科学电子笔记319（2015）165˛参数化的应用它说，每个关系解释都保持相等关系2：引理3.2（IEL）如果Γ <$T那么[[T]] r <$|EQ|| = Eq [[ T ]] o .|= Eq ◦ [[T]] o.Q3.2术语的语义雷诺兹 Reynolds首先给出了术语上下文的集值和关系解释Δ= x1：T1，. xn：Tn通过定义[[Δ]] o= [[T1]] o×···× [[Tn]] o和[[Δ]] r=[[T1]] r×···× [[Tn]] r。 这就定义了一个函数[Δ]：|U ||→ U。|→ U. Reynolds然后将每个判断Γ; Δ t：T解释为函数族[ t ]]o：[[Δ ] o S → [[ T ]] o S，对于每个环境S ∈|设置||.|. 我们在这里省略[t]]o的标准定义最后，雷诺兹证明：定理3.3（抽象定理）设A，B∈集合 |Γ|，R∈Rel| Γ|（A，B），a∈ [[Δ]oA，b∈[[Δ]oB。对于每一项Γ; Δt：T，如果（a，b）∈ [[Δ]rR，则（[[t]] oA a，[[t]] oB b）∈ [[T]] rR。 或者，更简洁地说，用虚构的方式：每一个判断Γ; Δ t：T都被解释为一个固定的自然变换（[[t]] o，[[t]] r）：[[Δ] → [[T]]。[[Δ]]r|Γ||Γ|z[[t]]r[[T]]r|Γ||Γ|zRelUc[[Δ]]o×[[Δ]]ozc|设置|| × |设置|Γ||Γ|z[[t]]o×[[t]]o集合×集合[[T]]o×[[T]]oQ这是值得解开定理的虚构陈述：由于函子[[Δ]]o和[T]]o的域是离散的，解释[t]]o实际上定义了一个（空自然的）变换[t]]o：[[Δ]o→ [[T]]o。由范畴Rel中态射的定义，在[t]]o×[[t]]o上的变换[t]]r的存在性（又是空的自然的）恰好是这样的陈述：如果（a，b）∈[[Δ]] rR，则（[[t]]oA a，[[t]]oB b）∈[[T]]rR--定理的冗长结论雷诺兹然而，令人惊讶的是，我们的虚构版本清楚地表明，抽象定理实际上陈述了由[t]]r给出的额外代数结构的存在，并且更一般地，将术语解释为自然变换。采取这种观点并揭示这种迄今为止隐藏的结构为我们对雷诺模型的双指数概括开辟了道路[2] Reynolds 在本文中，像许多其他文献[2，4，13，24]一样，我们只处理等式关系。 今后工作，我们希望给一个公理化的帐户N. Ghani等人/理论计算机科学电子笔记319（2015）165171¸4双指数关系参数性到目前为止，我们只展示了如何根据具体化U：Rel → Set × Set来看待雷诺我们现在将其推广到其他纤维。这要求我们将[-]]o和[-]]r推广为IEL和抽象定理成立的形式，这反过来又要求我们为这些其他的纤维化定义相等函子。等式函子的构造在任何具有必要基础设施的纤维化中都是标准的[16]，但为了完整性，我们在这里简要描述它。第一步是注意到例2.5中的关系纤维化是由Set上的子对象纤维化通过所谓的基的变化（或拉回）产生的，并推广该构造。定义4.1设U：E → B是一个纤维化，并假设B有乘积。纤维化Rel（U）：Rel（E）→B× B由以下基的变化定义：qRel（E）E相对（U）UCcB×B×B我们称Rel（U）为U的关系纤维化，称Rel（E）的对象为关系在B上，强调这种构造推广了Set上的关系。我们说一个纤维化U：E → B有纤维化终末对象，如果E的每个纤维EX都有终末对象，并且如果重索引保留了这些终末对象。将B的每个对象X发送到EX中的终端对象的映射扩展到一个函子 K：B → E称为U的真值函子。我们可以从U的真值函子构造Rel（U）的等式函子，如下所示：定义4.2设U：E → B是一个具有纤维终端对象的双纤维化。 如果B有积，则映射X<$→<$δXKX，其中δX是对角态射δX：X→X×X，对于Rel（U），扩展到等式函子Eq：B →Rel（E）对于这个定义，只要求沿着对角线δX的操作重索引就足够了（这就是Birkedal和Møgelberg [4]对等式建模的方法）。 打交道时 然而，对于5.1节中的图关系，我们将使用所有的操作结构来沿着任意态射操作索引。 我们的定义专门针对等式关系EqA，当实例化为Set上的关系Fibration时。等式函子是忠实的，但并不总是完整的;一个反例是恒等式双标度Id：Set→Set的等式函子，它给出了一个具有特殊而非参数的多态函数的模型。 因此，我们在本文的其余部分假设等式函子是满的。这让人想起Birkedal和Møgelberg内部相等意味着外部相等，在以下意义上：丰满说，如果（f，g，α）：1→EqY（即， α表示f=g（内部），那么，由于1=Eq1B，对于某个h，（f，g，α）=（h，h，Eqh）：1B→Y（即，f=g外部）。 我们在下面的第5节中的几个地方使用了Eq172N. Ghani等人/理论计算机科学电子笔记319（2015）165我们现在展示如何将箭头类型和forall类型解释为具有离散域的有限函子。然后，我们证明了一类特殊的函子形成了一个λ2纤维化，从而形成了一个实际上是参数化的系统F的模型4.1解释箭头类型第3.1节中[T→U]]o和[T→U]]r的定义分别由Set和Rel 此外，纤维化U：Rel→Set×Set保持了carbohydrate封闭结构，使得[t]]r在[[t]]o×[[t]]o上，正如抽象定理所要求的从这种纤维化中概括，我们可以“参数化”地对箭头类型进行在满足抽象定理的方式下-在任何纤维化U：E → B中，其中E和B是Carnival闭范畴（CCC），U保持Carnival闭性。定义4.3纤维化U：E → B是一个箭头纤维化，如果E和B都是CCC，并且U保持了Carnival闭结构。一个关系纤维化Rel（U）是一个保持相等的箭头纤维化，如果它是一个箭头纤维化，并且等式：B →Rel（E）保持指数。研究像纤维化这样的数学结构的一个好处是，它们的许多性质都可以在文献中找到。这有助于确定关系纤维化何时是保持相等的箭头纤维化：引理4.4设U：E → B是一个有纤维终端对象的双纤维化，B是一个CCC。(i) 如果Eq ：B → Rel（E）有一个左伴随Q，则Eq保持指数i <$Q满足Frobenius性质。如果U：E → B具有完全理解，Eq：B → Rel（E）是完全的，并且B具有推出，则这样的Q存在。(ii) 如果U：E → B是一个 固定的CCC，并且有简单的 乘积（即，如果，对于每个proje<$πB：A×B→AinB，reindex函子πB<$ 有右伴随（1）A是A，B是A，C是A，D是A，C是A，D是A。腕骨闭合结构Q基的变化保持了简单乘积和纤维结构，所以如果U是，则Rel（U）是具有简单乘积的此外，如果B是，则B × B是CCC。 引理4.4因此从U中的结构导出Rel（U）中的结构。4.2解释所有类型我们必须将Reynolds的f[ − ] ] o和[ − ] ] r的定义推广 规则对于类型抽象和类型应用程序，建议我们应该将类型变量的弱化解释为右伴随。 我们可以首先尝试寻找这样的一个伴随在基本范畴上，然后另一个伴随在总范畴上，然后试着把这些伴随词连起来。 但这是一个错误的想法;因为关系纤维化在例2.5中，这给出了所有的多态函数，而不仅仅是参数多态函数。相反，我们需要一个伴随的组合firebred语义。N. Ghani等人/理论计算机科学电子笔记319（2015）165173让|相对值（U）|n→EqRel（U）是其对象是来自于其中的保持相等的函数的范畴|相对值（U）|n到Rel（U），它们的态射是它们之间的自然变换。然后又道：定义4.5 Rel（U）是一个平衡，如果对于每个投影π n：|相对值（U）|n+1 →|n，函子<$π n：（|相对值（U）|（1）（1）（|相对值（U）|n+1 → Eq Rel（U））有一个右伴随算子n，并且这个算子族在n中是自然的。|n+1 →EqRel (U )) has a rightadjoint ∀nand this family of adjunctions is natural in n.当n可以被推断时，我们把n写成n这个定义如下，例如， Dunphy和Reddy [7]通过如果U是忠实的，那么定义4.5就可以用它的运算结构用更基本的概念来重新表述。而这一点，也是一个必然的结果，而不是一个必然的结果。对于本文的目的，这种抽象的规范就足够了。4.3具有离散域的纤维函子形成参数模型λ2-纤维化，即，一个纤维化p：G → S，有纤维有限积、S中的有限积、纤维指数、类属对象Ω和简单Ω-积，是系统F的范畴模型。Seely [29]给出了在这样的纤维化中的微积分的合理解释。我们用下面的定理来总结这一节定理4.6如果Rel（U）是一个保持相等的箭头纤维化和一个双纤维化，则存在一个λ2纤维化，其中类型ΓT被解释为保持相等的纤维函子[[T]]：|相对值（U）||→Eq Rel（U）和项Γ; Δ t：T被解释为离散自然变换[[ t ]]：[[Δ ] → [[ T ]]。|→EqRel(U ) and terms Γ; Δ ►t : T are interpreted as fibred natural transformations [[t]]:[[Δ] → [[T]].Q注意，引理4.4给出了Rel（U）是箭头纤维化的条件，我们的另一篇论文[9]类似地给出了Rel（U）是箭头纤维化的条件。展开λ2-纤维化中的系统F的解释[29]，我们看到对于满足定理假设的每个纤维化U：E → B，我们得到以下结果：对于每个系统F类型ΓT和项Γ;Δt：T，我们得到(i) 一个标准的解释，Γ T作为一个函子[T]] o：|B|| → B ;|→ B;(ii) 将ΓT作为函子[T]] r的关系解释：|Rel（E）||→ Rel（E）;|→ Rel (E);(iii) 以引理3.2的形式证明恒等式扩展引理，即，一个证明，[T]是平等的维护;(iv) 将T;Δt：T作为自然变换[t]]o：[[Δ]o→ [[T]]o的标准解释;以及(v) 以定理3.3的形式证明抽象定理，即，一个证明，即Γ;Δt：T有一个关系解释为自然变换[[t]]r：[[Δ]r→ [[T]]r over[t]]o×[[t]]o。定理4.6还给出了一种强大的内部语言[16]，其中类型上下文Γ中的基类型由fired函子给出|相对值（U）||→ Eq Rel（U），和基项|→EqRel (U), and base term174N. Ghani等人/理论计算机科学电子笔记319（2015）165§在术语上下文Δ中的常数由有限自然变换[[Δ]]→[[T]]给出因此，我们可以使用这种语言来推理使用System F的模型。这将用于下面定理5.7和5.11的证明5参数化的后果我们使用我们的新框架，以获得预期的后果参数。这是对我们新的双虚构概念化的“健全性检查”，并表明我们的框架足够强大，可以得出相同的结果，例如，Birkedal和Møgelberg [4].在高层次上，我们的证明策略通常与文献中发现的相似，而单个事实的证明必然是特定于我们的设置的，并且通常是虚构的。5.1图关系在纤维化U：Rel→Set×Set中，每个函数f：X→Y定义一个图关系f ={（x，y）|fx= y} X × Y。这推广到虚构的设置，其中f：A→B的图是通过重新索引B上的等式关系获得的。定义5.1设U：E → B是一个纤维化，纤维化的终对象和乘积在B中。B中h：X→Y的图是Rel（E）中的<$h<$=（h，idY）<$（EqY）在集合论中，对集合上的关系纤维化，给出了一个一致的定义。由于重索引保留了恒等式，所以对于B的任何对象A，都有Eq_idA_i =（idA，idA）_i（EqA）= EqA。在一个双标中，我们也可以用另一种同构的方式定义f：A→B的图，通过使用运算结构来操作A上的等式：引理5.2（Lawvere [17]）如果U：E → B是一个双纤维化，其纤维化终端对象满足Beck-Chevalley条件[16，1.8.11节]，并且如果B有乘积，则h：X→Y的图也可以由下式描述：Q能够在任何双标中用重索引或操作重索引来描述图关系，使我们在证明关于它们的定理时可以使用两者的普适性质。 图关系是将B中的态射转换为Rel（E）中的对象的关键结构，并且更一般地，介导标准语义和关系语义。Rel（U）：Rel（E）→ B×B的图函子是函子：B → →Rel（E）将B中的f：X→Y映射到Rel（E）中的f。为了了解态射如何作用于态射，回想一下，如果f：X→Y和fJ：XJ→YJ是B →的对象，那么从f到fJ的态射是一对态射g：X→XJ和h：Y→YJ，使得fJ<$g= h<$f。Rel（U）中重索引的普适性保证了在（g，h）上存在唯一的态射g，h：f → f j，使得下图可以f快！布雷格湖 C公式hC<$fJ<$（f′，id）<$EqYJN. Ghani等人/理论计算机科学电子笔记319（2015）165175引理5.3如果基本双振动满足Beck-Chevalley条件，则如果Eq：B→Rel（E）是，则Eq：B → Rel（E）是完全的和忠实的。Q证明使用引理5.2中的图函子的运算特征。导出参数性结果的主要工具是图引理，它将函子在态射上的作用图与其在态射图上的关系作用联系起来有趣的是，虽然我们的设置可能是证明相关的（即，可以有多个证明两个元素是相关的），下面的图引理的“逻辑等价”版本对于我们的如果U：E→B和UJ：EJ→BJ是有理数，我们写（Fo，Fr）：Rel（U）→EqRel（UJ）来表示函子（不一定是有理数）Fo：B → BJ和Fr：Rel（E）→Rel（EJ）使得Rel（UJ）<$Fr=（Fo×Fo）<$Rel（U），并且（Fo，Fr）是保相等的，即，Fr<$Eq=Eq<$Fo.定理5.4（图引理）假设下面的双纤维满足Beck-Chevalley条件，令（Fo，Fr）：Rel（U）→EqRel（U）。对于B中的任意h：X→Y，在Rel（E）中存在垂直态射φh：F o h→F rh和φh：F rh→F o h.Q我们对图引理的证明是完全独立于特定函子（Fo，Fr）的，因此特别是不通过类型结构的归纳来进行。这就是为什么我们可以超越Dunphy和Reddy [7]，证明正型表达式的初始代数的存在性，而不仅仅是严格正型表达式的初始代数的存在性的关键原因。5.2初始代数设F：C → C是闭函子。 一个F-代数是一个对（A，kA），其中A是对象C和kA的：FA→Aa态射。 我们称A为F-代数的载体，kA其结构图。 C中的态射h：A→B是F-代数同态h：（A，kA）→（B，kB），如果kB<$（Fh）=h<$kA.一个F-代数（Z，in）是弱初始的，如果对任何F-代数（A，kA），存在一个中介F-代数同态折叠[A，kA]：（Z，in）→（A，kA）.如果fold[A，kA]是唯一的，则它是初始F-代数文献包含初始代数存在于参数模型中的其他证明（例如，[4，24]）。与我们的背景最接近的是Dunphy和Reddy [7]，他们证明了严格正类型有初始代数。在不强于他们的假设下，我们将这个结果锐化为所有正类型，或者更一般地，我们的参数模型上的所有函子都是强的（见下文）和等式保持的。设F=（Fo，Fr）：Rel（U）→EqRel（U）是一个函子（注意F的定义域不是离散的，F不需要保持carnomorphisms），其强度为t=（to，tr），即，一族态射（to）A，B：A<$B→FoA<$FoB和（tr）R，S：R<$S→FrR <$FrS，其中（tr）R，S在（（to）A，B，（to）C，D）上，如果R在（A，B）上，S在（C，D）上，使得t保持恒等和复合。具有强度的函子称为强函子。 由于离散域的存在，t是一个自然的变换，|相对值（U）|2→EqRel（U），因此α，β;·Rel：（α → β）→（F[α] →F[β]）表示F对以下态射的作用：176N. Ghani等人/理论计算机科学电子笔记319（2015）165内部语言。所有具有一个自由类型变量的类型表达式都只出现在正数上，这就产生了强函子，但是还有更多这样的函子的例子，例如，如果模型包含具有自然函子（和关系）解释的非系统F类型构造-例如，那些在Set中的依赖类型。我们将证明一个初始Fo-代数存在.为此，我们首先构造了一个弱初始Fo-代数，它可以在任何λ2-纤维化中完成。使用内部语言，我们定义Z为（Z o，Z r）=[[X。（FX→X）→X]]。引理5.5Zo是弱初始Fo-代数（Zo，ino）具有中介态射折叠o [A，k]的载体，Zr是弱初始Fr-代数（Zr，inr）具有中介态射折叠r [A，k]的载体.Q为了证明折叠o是唯一的，我们使用5.1节中的图形关系。回想一下，一个具有终结对象1的范畴是良点的，如果对任何f，g：A→B，我们有f=g ife =ge对所有e：1→A。像Dunphy和Reddy [7]一样，我们只考虑指向良好的基本范畴;指向良好用于将非空上下文中的内部语言推理转换为封闭上下文，以便我们可以应用定理5.4等语义技术。引理5.6假设基本双振动满足贝克-谢瓦利条件，并且方程是满的。(i) 如果B是良点的，则foldo[Z o，ino] =idZ。(ii) 对于每个Fo-代数同态h：（Zo，ino）→（A，kA），我们有hfoldo [Z o，ino] = fold o [A，k A]。Q引理5.6的两个部分的证明是相似的：都使用图函子将B中的交换图映射到Rel（E）中的态射，然后使用图引理看到这些态射是Fr-代数。引理5.5和引理5.6合在一起，现在直接隐含了主要结果。定理5.7如果基本双振动满足Beck-Chevalley条件，Eq是满的，B是良点的，则（Zo，ino）是初始Fo-代数.Q我们在第6节中表明，这些假设不能被削弱。人们可能会问，上述结果是否可以加强，不仅得到一个初始的Fo-代数，而且还得到一个初始的Fr-代数。当然，这对于纤维化关系Rel→Set×Set是可能的，因为Rel中的关系是证明无关的：映射要么保持相关性，要么不保持相关性。这在公理化的双虚构设置中转化为要求纤维化Rel（E）→ B× B是忠实的。 当它是时，弱初始Fr-代数实际上是初始的：忠实性意味着所需的唯一性。5.3最终余代数我们也可以对上一节的证明进行对偶，以证明[11]《易经》中的阴阳五行。像往常一样，这需要我们首先在系统F中编码乘积和存在类型。我们将乘积编码为A×B=很好。（A→B→Y）→Y。这支持通常的配对和投影操作，N. Ghani等人/理论计算机科学电子笔记319（2015）165177以及使用参数性的满射配对我们通过以下方式编码存在类型：X.T=Y. （注十）（T→Y））→Y。 我们可以支持引进和淘汰规则T[A/X] Γ;Δu：TΓ;Δ A，u：X.T（X）T;Δt：TTT，Z; Δ，y：T[Z/X]Δs：SΓ;Δ（打开t作为Z，y在s中）：S通过定义ΔA，t=ΛY.λf.f A t和s =tV（ΛZ.λy.s）中的开t，将转换开ΔA，t转换为s=s[X/A，y/t]中的Z，y使用参数性，我们可以证明存在类型的以下交换性质和η-规则引理5.8假设基本双振动满足贝克-谢瓦利条件，并且方程是满的。(i) 令Γ;Δμt：μX.T，令 Γ，Z; Δ，u：T[Z/X]μs：S，令Γ;Δμf：S→SJ对于闭型SJ。 然后[[f（open t asZ，u in s）]] o=[[open t asZ，uin f（s）]] o。(ii) 如果Δ; r t：<$X.T，则[[open t as <$Z，u<$in <$Z，u<$]]o=[[t]] o。Q如果F：C → C是一个闭函子，则F-余代数是一个对（A，kA），其中A是C的对象，kA：A→FA是态射. 我们称A为F-余代数的载体， kA其结构图。 C中的态射h：A→B是F-余代数同态h：（A，kA）→（B，kB），如果kB<$h=Fh<$kA.一个F-余代数（W，out）是弱最终的，如果对任意F-余代数（A，kA），存在一个中介F-余代数同态展开[A，kA]：（A，kA）→（W，out）.它是一个最终的F-余代数，如果unfold[A，kA]是唯一的。设F=（Fo，Fr）：Rel（U）→EqRel（U）是一个强度为t的函子. 我们证明了最终的Fo-余代数存在.同样，我们首先构造一个弱最终余代数，通过定义W =（W o，W r）= [[X. （X→F（X））×X]]。引理5.9 W o是弱最终F o-余代数（W o，out o）具有中介态射展开o [A，k]的载体，W r是弱最终F r-余代数（W r，out r）具有中介态射展开r [A，k]的载体.Q我们继续类似于引理5.6。这一次，我们使用图引理的运算部分来构造Fr-余代数。引理5.10假设基本双纤维满足贝克-谢瓦利条件，并且方程是满的。(i) F或任意Fo-co代数的态射h：（A，kA）→（B，kB）有展开o[B，kB]h=展开o [A，k A]。(ii) 展开o [W o，out o]= idWo.Q把这些东西放在一起，我们构造了一个final coalgebra。定理5.11如果下面的双振动满足Beck-Chevalley条件，并且如果Eq是满的，则（W o，out o）是最终的F o-余代数。Q5.4参数化意味着二元性我们表明，我们的公理基础可以用来证明，可以推导出参数的非自然性。这在其他设置中是众所周知的（参见，例如，[4，178N. Ghani等人/理论计算机科学电子笔记319（2015）165、R一R但我们这样做是因为：i）它表明我们的基础通过了这个检验; ii）它再次强调了双振动的使用，以给出函数图的两个定义，这两个定义都用于证明。第一，非自然性的定义定义5.12如果F，G：Bop×B → B是混合变函子，则二自然变换t：F→G是tX：FXX→GXX索引的态射的集合 通过B的对象X，使得对于B的每个g：X→Y，以下交换：F X XtXGX XF Y XF（idY，g）G（idX，g）zG，XYzG（g，idY）FYYtYG YY我们注意到，我们的证明适用于所有具有相等保持提升的混合变函子，而不仅仅是强函子。定理5.13设（Fo，Fr），（Go，Gr）：Rel（U）op× Rel（U）→EqRel（U）. 此外，让0：FoAA→GoAA是由B的对象A所索引的族，t1：FrRR→GrRR是由Rel（E）的对象R索引的族，使得如果R在（A，B）上，则t1是over（t0A，t0B）. 则t0是从Fo到Go的一个双自然变换.Q定理5.13特别适用于对项t的解释：<$X.FXX→GXX，其中F和G由具有两个自由类型变量的类型表