关系参数性与计算效应：一种多态性的研究

理论计算机科学电子笔记173（2007）295-312www.elsevier.com/locate/entcs控制的关系参数性作为一种计算效应Rasmus Ejlers Møgelberg，亚历克斯·辛普森1爱丁堡大学摘要本文研究了控制算子存在时的参数多态性。我们的方法是专门的一般类型理论相结合的多态性和计算的effections，通过扩展它与额外的常数表示控制。通过定义这个扩展演算的关系参数模型，我们捕捉参数和控制之间的相互作用作为一个工作的例子，我们表明，最近的结果M。Hasegawa关于二阶（按名称调用）λμ-演算中的类型可定义性的研究是作为对任意计算结果有效的一般结果的特殊情况保留字：计算效应，控制，指称语义，参数多态1引言关系 参数性[19]为建 立多态 程序 的性质 提供了 一个强 有力的 证明 原则它 在Girard/Reynolds二阶λ-演算的背景下得到了广泛的研究，后者在其纯形式下是全函数的演算。试图将关系参数性的概念扩展到更丰富的演算会导致问题。甚至递归（以及随之而来的非终止性）也会产生困难，因为递归的定点性质与参数性的某些结果（有限余积的存在性这个问题导致Plotkin提倡采用线性类型理论，其中不会出现这种不一致[18]。这种方法已在[4]中详细研究，并具有许多良好的性质。例如，人们获得了广泛的多态类型可定义性结果，并从关系参数性中获得了所需的普适属性。不幸的是，使用线性类型理论的方法不适用于包含计算效应的不纯设置。 特别是，1这项工作得到了丹麦科学、技术和创新署以及EPSRC的支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.040296R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295线性逻辑的一个重要特征是，它的monoidal封闭结构，在计算对象的模型中不会自然出现，这些对象的相关计算单子（在Moggi [15]的意义上）不是可交换的。非交换单子的一个重要例子是用于对控制效应建模的连续对于这样的结果，长谷川[6，7]最近提出了关系参数性的语法解释，他利用这一点获得了Parigot二阶λμ-演算的按名称调用版本的类型可定义性结果他观察到的一个有趣的事实是，他关于多态类型可定义性的结果然而，开发这两类成果的技术框架似乎非常不同。本论文的目标，连同一个配套文件[14]，是开发一个统一的语义理论的关系参数，这是适用于任意计算的效果，并专门在交换效果的情况下，线性参数，并在控制的情况下，长谷川的参数的说明语义版本我们用于实现这一目标的一般框架在Companion文件[14]中详细介绍。它采用多态类型理论的形式，松散地基于Levy在本文中，我们重点关注控制。为此，我们扩展了[14]的一般类型理论，增加了一些常数，使其专门用于控制。该扩展允许基于控制的程序演算在类型理论中解释我们通过给出Parigot的二阶λμ -演算的一个逐名翻译来说明这一点本文的主要技术工作是构造了一个扩展类型论的关系参数模型。我们的目标是利用这个模型来证明长谷川事实上，我们表明，他们出现的特殊情况下，一般结果有效的任意计算ececks。这一事实不仅提供了长谷川结果的另一种（和指称）解释，而且解释了2多态性和控制的类型理论我们首先回顾[14]中提出的多态性和结果（PE）的一般类型理论，并将其专门用于延续的情况。多态和结果的类型理论基于Paul Levy 遵循[13]的约定，我们通过使用带下划线的元变量A，B，.. 对于计算类型，与A、B、. 对于值类型。类型理论PE允许对两种类型进行多态量化，因此类型可以包含值类型的类型变量，范围为X，Y，.. 或者对于计算类型，R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295297由X，Y，Z，. ...................... 值类型和计算类型由语法A，B：：=X|A→B|第十章一|X|一B|第十章A A，B：：= A→B|第十章一|X|第十章A.注意，与CBPV相反，我们的计算类型构成了值类型。关于这一点和其他CBPV偏离的讨论，请参见[14]。在这里，我们只评论那些在我们对控制的处理中起重要作用的特征函数类型有两种构造：和→，为了区分这两种类型，我们将前者称为线性函数类型。类型系统的一个语义在这种直觉下，→表示普通函数空间，是代数同态的空间，它一般不携带一个代数结构，所以是一个值类型。另一个有点不同的模式将是在第4节中介绍。 请注意，类型限制阻止构造函数被迭代。例如，（AB）BJ不是有效类型。术语由语法t，s：：= x| λx：A.t|s（t）|Λ X。不|t（A）|λmax：A.t|Λ X.t类型判断的形式为：|其中，r是变量的上下文，并且Δ是被称为stoup的第二变量上下文，该stoup或者是空的或者恰好由一个计算类型的变量组成，在这种情况下，A也必须是计算类型。这两种情况有时也被明确地写为Γ |−t：AΓ|x：B，t：A。stoup背后的语义直觉是，对于Γ中变量的所有实例化，项t表示从B到A的代数同态。这与Levy在CBPV [ 13 ]中的堆栈概念密切相关图1中给出了类型规则。我们将把关于类型论项的等式理论看作是由两种类型的项抽象和两种类型的类型抽象的通常β和η规则所导出的最小同余关系，见图2。当然，这些等式应被理解为在相关上下文中相同类型的术语之间。在[14]中，类型论PE被研究为结合多态和效应的一般演算。我们在这里的目的是将其专门化到控制事件的情况下，如由延续单子实现的那样。为了激励我们的方法，我们回顾一下，在[14]中，定义类型构造！A=def 第十章（A→X）→X，它将任何值类型A映射到计算类型！A，被证明是服务于莫吉的类型单子类型T A[ 15 ]的目的298R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295r，x：A| −Bx：Ar，x：A |Δ t：BΓ|Δ λ x：A.t：A → BΓ |Δεs：A → BΓ |−A：AΓ |Δεs（t）：BΓ |ΔΔt：AΓ|Δ ε Λ X。 t：X。一X/∈FTV（Γ，Δ）Γ |ΔΔt：ΔX。 一Γ |Δt（B）：A [B/X]Γ|x：A x：AΓ|x：A t：BΓ |−λx：A.t：ABΓ |ΔΔt：AX/∈FTV（Γ，Δ）Γ |−s：ABΓ |ΔΔt：AΓ |Δεs（t）：BΓ |ΔΔt：ΔX。 一Γ |Δτ Λ X.t：τX. AΓ |Δt（B）：A [B/X]Fig. 1. 体育课的打字规则（λx：A. t）（u）= t [u/X]λx：A. t（x）=tift：A→Bandx∈/FV（t）（λ∈x：A. t）（u）= t [u/X]λmax：A. t（x）=tift：ABanddx∈/FV（t）（ΛX. t）A=t[A/X]Λ Y.t Y= tif t：<$X. A和Y（ΛX. t）A=t[A/X]Λ Y. t Y= tif t：X. A和Y∈/FTV（t）∈/FTV（t）图二. PE的等式公理Levy在[14]中，关系参数化理论被用来证明这种编码。因此，我们得到一个Girard分解：类型A→B和！A B是同构的（作为值类型）。为了编码控制，我们希望专业化！A是一个延续单子。我们可以通过要求一个类型常量R来表达这一点，作为结果类型，并要求类型构造（A→R）→R的行为像！A.为此，类型表达式（A→R）→R必须是计算类型，因此类型常数R也必须是计算类型 。 那 么 （ A→R ） →R 的 所 需 性 质 可 以 通 过 要 求 标 准 线 性 映 射 来 实 现 ！ 一（A→R）→R有一个线性逆。 通过上面的Girard分解，这等价于要求正则映射！一（！一R）→R有一个线性逆。我们的实际控制方法是上述方法的自然概括。而不是将上面的最后一个同构限制为形式的类型！我们求正则映射A（A）R）→R是每个计算的同构型嗜当然，将这种同构添加到类型论的自然方法是添加一个多态常数。同构的一个方向是直接R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295299不需要对类型理论做任何补充就可以定义的：η = def Λ X。λmax：X. λf：XR. f（x）：f（X）X（XR）→R。因此，我们用一个常数： （（XR）→R）X，以及确保该常数与η成反比的方程。更准确地说，用符号A表示A，同样地用符号ηA表示ηA，我们将方程相加，Λ X。λmax：X. X（ηX（x））= Λ X。λx：X.xΛ X。λ_x：（XR）→R。ηX（λX（x））= Λ X。λx：（XR）→R. X.我们将把这个扩展称为多态和控制的类型理论，缩写为PE+C。在第3节中可以找到该理论公式化的进一步动机，其中它被用来模拟Parigot 我们还提到，我们使用线性函数空间AR相关 Levy在 我们将两者结合起来似乎是一种非常自然的方法，因为A和（AR）→R之间存在线性同构的要求导致了一个非常简单的方程理论。我们现在探索PE+C的一些简单的等式性质， βη定律和同构控制方程第一，常数在线性映射中自然的，在这个意义上，对于任何f：AB、图解（A）R）→R AA（f）R）→ Rf◦B（B）R）→ RB上下班这是从η的相应自然性得出的，η是β和η规则的简单推论。其次，我们证明了，仅仅从βη等式，人们就得到了函数空间的Girard分解，用（A→R）→R代替！A. (Note的多态性定义的相应结果！A取决于参数性属性。）为了可读性，我们引入符号<$A表示A →R。命题2.1对于PE+C中的任何类型A和计算类型B，在类型A → B的项和类型AB的项之间存在双射对应。对应在A中对所有映射是自然的，在B中对线性映射是自然的。300R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295证据对应关系取项t：AB到λx：A。t（λf：A。λf：BR. h（f u））。Q在类型论中增加常数η的一个重要结果是，成为分裂单声道，这意味着以下引理。引理2.2在PE+C中，下面的原理成立。 如果t，tJ：A使得f（t）=f（tJ），对于新变量f：AR，则t = tJ。我们用另一个引理来结束这一节，我们稍后会用到。引理2.3在PE+C中如果f：AR和x：（AR→R，则x（f）=f（Ax）证据n的自然性意味着f（nAx）= nR（fR）→R）（x））。现 在 ，通过同构的逆的唯一性，<$R（y）= y（id R），因此f（<$Ax）= x（f）如所期望的。3用PE+C语言解释二阶λμ-演算本节的目标是展示PE+C的控制原语如何支持Parigot的二阶λμ -演算的自然解释为此，我们给出了一个按名称调用的翻译，模拟[7]的等式理论我们首先回忆一下二阶λμ-演算λμ2。一般来说，我们遵循[7]中的表述，但通过引入一个虚假类型来稍微扩展语言，这允许我们将控制操作分解为名称应用和μ抽象。这并不是对微积分的一个严肃的修正。如[ 7 ]中所示，也参见第5节，在适当的关系参数化理论下，可以将X多态编码为X。X.λμ2的类型由文法给出σ，τ：：= X| ⊥ |σ→τ|第十章σ，并且术语由下式给出：M，N：：= x| MN| λxσ.M| Mσ|Λ X。M| μα。M|[α] M.我们用x，y，z来定义普通变量的范围，用α，β，γ来定义连续变量（有时也称为名称）的范围。打字判断被写为ΓM：σ|Δ，其中，Γ是普通变量的上下文，Δ是连续变量的上下文。图3给出了λμ2的类型规则。我们将把λμ2项上的等式关系看作包含图4公理的最小同余关系。图4中的最后两个规则使用所谓的混合规则。对于M[[β]（−N）/[α]（−）]m∈N，表示M的所有形式为[α]L的子项，其中[β]（L N）。R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295301Γ，x：σ，Γ J<$x：σ|Δr，x：σ，r J<$M：τ|Δr，r J<$λxσ.M：σ→τ|ΔΓM：σ→τ |ΔrN：σ| ΔrMN：τ|ΔΓM：σ|ΔX∈/FTV（Γ，Δ）X. M：是的。σ |ΔM：σ |ΔrMτ：σ[τ/X]|ΔΓM：σ|Δ，α：σ，ΔJΓ[α] M：|Δ，Δ JΓ►M: ⊥|Δ，α：σ，ΔJΓ<$μασ.M：σ|Δ，Δ J图三. λμ2的类型规则（λxσ.M）N=M[N/x]λxσ.M x=M（Λ X. M）σ = M[σ/X] Λ X。M X =M[α]（μβ. M）= M [α/β]μα。[α]M=M（α∈/FN（M））（μ ασ→τ。 M）N=μ πι。 M[[β]（−N）/[α]（−）]（μ α）X. σ。 M）τ=μβσ[τ /α]M[[β]（−τ）/[α]（−）]见图4。 按名称调用λμ2我们将λμ2解释为PE+C，表示为（−），如图5所示。λμ2的类型被解释为计算类型。λ μ 2类型化上下文Γ = x1：σ1，. xn：σn被解释为：x1：σ1，. xn：σn≠ 0。请求继续上下文，Δ = α1：σJ，.αm：σJ，我们对PE+C使用符号Δ ΔR1m上下文α1：σ1R，... αn：σ1R.下面的命题阐述了对打字判断的解释。X= X= R（σ→τ）= σ→τ （X. σ）=X。 σ<$x<$= x（λx：σ. M）= λx：σ.M（M N）= M <$N（Λ X. M）<$= Λ X.M <$（M σ）<$= M <$σ<$（[β]M）<$=β（M<$）（μασ.M）<$=<$σ<$（λα：σ<$R. M）302R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295图五. 将λμ2解释为PE+C。R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）29530312命题3.1（类型可靠性）如果Γ <$M：σ|Δ是λμ 2中的类型化项微积分，那么下面的判断在PE+C中很好地输入。Γ∗, Δ∗R|−M：σ定理3.2（合理性）若Γ <$M1 = M2：σ|Δ是可证明的，使用按名称调用λμ 2的等式规则，然后PE+C证明：Γ∗, Δ∗R| −M= M。1 2证据 证明是通过归纳的结构证明的M1= M2。 对于λμ 2公理的前半部分，这个解释显然是合理的，因为这个解释保留了简单类型结构和多态结构。考虑等式[β]（μγ）。M）= M [β/γ]。”[10]故，“以”为“以”。M））β（λσ）（λγ. 其中σ是γ的类型，根据引理2.3，它等于M [β/γ]=（M[β/γ]）规则μα。M=M是合理的，因为（μα。 [α] M）<$=<$σ<$（λα. α（M））= σ（ησ（M））= M我们给出了（μ ασ1 →σ2. M）N=μ sσ2。 M[[β]（−N）/[α]（−）]byusingg引理2.2.假设f：σ2<$R。则函数λ<$h：σ1<$→σ2<$.f（h（N<$））是线性的，因此根据引理2.3f（（μασ1→σ2.M）N）n=f（λσ1→σ2）n（λα：（σ1→σ2）n）R . （N））=（λα：（σ1α→σ2α）R. M<$）（λ<$h：σ1<$→σ2<$.f（h（N<$）=M<$[f（−N<$）/α（−）]=（λβ：σ2<$R. （M[[β]（−N）/[α]（−）]）<$）f=f（μ sσ2. M[[β]（−N）/[α]（−）]）<$。因此，定义了一个结构（μ α∈ X）。σ1。 M）σ2=μ Sσ1 [σ2/X]。 M[[β]（−σ2）/[α]（−）]的证明也是一样Q熟悉Reus和Streicher对λμ演算的“否定域”翻译[ 22 ]的读者这个问题也与长谷川的工作[ 7 ]相比较，因为他通过一个翻译来研究λμ 2演算，这个翻译本质上事实上，我们的翻译可以看作是对形式A的值类型的否定域翻译R. 对于每个λμ2类型σ，考虑PE+C值peσt=defσR。 Tenσt→Ren=σtndso，直到h为同构，任意λμ2项x1：σ1，.，xn：σn<$M：τ|α1：σJ，.，αm：σJ1m304R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295被翻译成一个术语x1：σ1→R，.，xn：σnt→R，α1：σJt，.，αm：σJ<$M：τ<$→R1m如果我们将乘积添加到值类型中（可以在parametricity的prence中进行多态编码），并且对于所有值，值类型X到PE+C，我们恢复了长谷川（σ→τ）<$=（（σ<$→R）→（τ<$→R））R<$=（（<$σ <$×τ<$）→R）R<$=<$σ<$×τ<$。4PE+C的相对参数模型本节的目的是为PE+C提供一系列相关参数模型。请注意，任何这样的模型都将包含一个通常意义上的标准二阶λ演算的关系参数模型，因为这是PE的值类型的子系统。因此，在这样的模型之上构建PE+C模型是很自然的。二阶λ演算的相对参数模型分为两种已知的类型：项模型[8]和PER模型。后者可以解释为PER模型[1]，分类为纤维化[3]，或在这里，与[14]一样，我们采用后一种方法，因为它允许我们在直觉主义集合论中公理化和直接地工作，执行简单的集合论构造，而不会受到具体模型的附带技术属性的阻碍因此，从现在起，我们研究直觉主义集合论（IZF）。对此不满意的读者，请耐心听我们的，并遵循经典的发展。在理论上，遵循Reynolds [20]，这样的读者将能够利用经典逻辑来推导不一致性。然而，这一尴尬的事实不太可能妨碍获得普遍的理解。我们首先回顾[14]中我们假定给定范畴Set的一个全子范畴C将用于解释值类型的集合。 这需要满足：（C1）若A∈C且A∈= Bin，则设B∈C.（C2）对于C中的任意集的集指标族{Ai}i∈I，i∈IAi又在C中。（C3）给定A，B∈ C和函数f，g：A→B，均衡器{x∈A|f（x）=g（x）{\displaystyle g（x）}在C中也是一样。（C4）存在C的对象的集合C，使得对于任意A∈ C，存在B∈C其中hB= A。通过项（C2）和（C3），类别C是完整的，具有从Set继承的限制。由于函数空间是幂，对任意集合A和任意B∈ C，函数空间BA在C中，即C是集合A的指数理想。特别地，C是闭的。R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295305最后一个公理指出C弱等价于一个小范畴。这允许一个显示C也是余完备的，通过应用Freyd的伴随函子定理，参见。[9]的文件。计算类型使用范畴A和满足以下公理的函子U：A → C来建模。目前，直觉将是A是C上单子的代数范畴，而U是遗忘函子。然而，当我们考虑控制的情况时，我们很快就会看到一个相当不同的模型例子。A和U所需的公理是：（A1）U对A中的任一图Δ和C中U（Δ）的极限锥limU（Δ），存在A中Δ的特定极限锥lim Δ，使得U（lim Δ）= limU（Δ）.（A2）U反映同构（即，如果Uf是同构，则f也是同构）。（A3）对于A的对象A，B，hom-setA（A，B）是C的对象。（A4）存在A的对象的集合A，使得对于A的每个对象A，存在xiss B∈A，其中A∈=BinA。虽然上述公理并不强制范畴A成为C上的单子的代数范畴，但为了方便和直观，我们还是将A的对象称为代数。由于公理暗示U是忠实的，我们可以将A（A，B）与从UA到UB的特殊函数的集合（我们称之为同态）等同起来，并且我们将写作f：AB表示f是同态从UA到UB。 如果A和B都是A的最小值，则A = B。对于C的一个对象A，我们写Sub C（A）for the set {B<$A |B∈ C}，其中给出了A的C-子代数集的一个典范表示。公理（A1）和（A2）表示U是从A∈ A的A-子代数到UA的C-子代数的内射映射.因此，我们可以定义Sub A（A）= def{B<$U A|BU A是A的A-子对象的像}作为A的A-子代数的集合的表示。对于参数模型的构造，我们将假设我们作为额外的数据被给予两个“可接受”关系的集合，我们将使用它们来更准确地说，对于C的每一对对象A，B，我们需要一组特定的容许C-关系RC（A，B）子C（A×B），对于A的每一对对象A，B，我们需要一个指定的容许A-关系RA（A，B）<$SubA（A×B）.此外，这些收藏关系需要满足一些闭包性质，我们现在定义。对于A∈ C，我们将SubC（A×A）中的对角（恒等）关系写成ΔA类似地，对于A∈ A，我们将UA上的对角关系写成ΔA，它确实在SubA（A×A）中。对于f：AJ→A，g：BJ→B in C和R∈ Sub C（A×B），我们写（f，g）−1R for {（x，y）|（f（x），g（y））∈ R}，它是SubC（AJ× BJ）中的一个元素. 注意，如果f：AJA，g：BJB和Q∈SubA（A×B）则（f，g）−1Q是SubA（AJ×BJ）的元素。我们对可容许关系施加以下要求306R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295（R1）对于C的每个对象A，对角线关系ΔA在RC（A，A）中，同样对于A的每个对象A，对角线ΔA在RA（A，A）中。（R2）容许关系在逆象下是封闭的，即，若R∈RC（A，B）且f：AJ→A，g：BJ→B，则（f，g）−1R∈RC（AJ，BJ）若Q∈RA（A，B）且f：AJA，g：BJB，则（f，g）−1Q∈RA（AJ，BJ）（R3）对于同一对对象上的任何容许C-（或A-）关系集，交集是容许C-（或A-）关系。（R4）RA（A，B）<$RC（UA，UB）.请注意，公理（R 1）和（R 2）意味着函数的图形是可容许的，特别是如果f：A→B则f = def{（x，y）|f（x）= y} ∈RC（A，B），若g：AB则<$g <$∈RA（A，B）.公理（C）、（A）和（R）有许多构造模型的方法。一个动机构造是将C取为弱小的可实现性topos的任何完全相对子范畴（关于如何产生这样的范畴，请参见[9，11]然后，对于C上的任何（内部）单子，取A为（Eilenberg-）的范畴。Moore）代数的单子。最后，将RC（A，B）和RA（A，B）分别简单地表示为SubC（A×B）和SubA（A×B下面是一个更复杂的例子，它利用了可容许关系中的可容许性我们简要地考虑了上述结构中PE的解释，给出了一个有助于理解本文的概述。详情请参阅[14]。值类型在类别C中解释，计算类型在类别A中解释为对象。我们将分别为这些解释写C[[−]]和A[[−]]。因为任何计算类型A也是值类型，所以给出了满足U（A[[A]]）= C [[A]]的两种解释。类型构造函数→被解释为集合论函数空间，并被解释为分配给计算类型的代数之间的同态集合。计算类型A→B使用弱极限创造被解释为代数A，其中UA是从C[[A]]到C[[B]]的函数的集合为了给出多态类型的关系参数解释，构造函数也被赋予关系解释。例如，如果R∈RC（A，B）且RJ∈RC（AJ，BJ），则R→RJ是关系式{（f，g）∈（A → AJ）×（B → BJ）|x：A，y：B. （x，y）∈R <$（f（x），g（y））∈ RJ}，若Q∈ RA（A，B）且QJ∈ RA（AJ，BJ）则QQJ是关系式{（f，g）∈（AAJ）×（BBJ）|X：U A，Y：U B. （x，y）∈Q<$（f（x），g（y））∈QJ}.多态类型通过分别在C和A上取乘积并限制到乘积的参数元素对参数元素的这种限制RC当量化超过值类型时，量化计算类型。作为一个说明性的例子，我们将在后面用到，对于封闭计算类型B，类型X。（（XB）→B）X是R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295307被解释为A的宾语，{（fA）A∈A∈A（（AA [[B]]）→ A [[B]]）A|A，B∈A。<$Q∈ RA（A，B）.（fA，fB）∈（（QΔA[[B]]）→ ΔA[[B]]）Q}。（一）最后，我们简要回顾一下术语的解释为了简单起见，我们仅限于类型是封闭的情况。一个类型良好的项Γ|Δ t：B被解释为C [[B]相对于环境γ的元素[ t ]] γ，其映射Γ中的每个变量x：A |Δ对一个元素γ（x）∈ C [[A].在Δ非空的情况下，映射d∈C[[A]]<$→[[t]]γ[d/x]是从A[[A]]到A[[B]的同态。对于涉及开放类型的术语的完整解释，参见[14]。现在已经介绍了为PE建模所需的语义结构，我们最后转向另外为控制建模我们的构造的问题。由于无法避免二阶λ-演算的参数模型，我们从满足上述（C）公理的任意范畴C开始设R是C中的任意对象，被选作结果类型。为了满足我们的公理，人们希望实现以下等式：UopR（−）A）C =defC）C，这与延续模型中的既定传统相适应，参见。[25、24、13]。实际上，在这样的结构中，可以解释计算类型常数RbyA[[R]]=def1anddC[[R]]=defR1=R. 对于任何一个A的B节点A，对于C，如果我们有A[[（AR）→R]]n=A，则C[[AR]]n=A（A，1）=C（1，A），则C[[（AR）→R]]n=RA=U（A），其中同构是一个同态.然而，虽然范畴Cop确实满足上面的公理（A3）和（A4），函子R（−）：Cop→ C不一定满足公理（A1）和（A2）。因此，我们修改了构造，使这些公理得到满足。首先我们讨论同构的反射。虽然R（−）：Cop→ C不需要在所有C上自同构，但存在C的最大满自同构子范畴。定义4.1[10，23]C中的集合C称为R-充满，如果对所有映射f：A→B在C，若映射Rf：RB→RA是同构，则Cf：CB→CA也是同构.我们用Crep表示C在满对象上的全子范畴。 这是标准的，cf。[10，23]，充满对象在Set中的极限下闭合，因此C表示（C1）它也满足（C4），因为我们可以取Crep =def{C∈C|C充满}。平凡地，对象R本身是充满的，因此任何幂RA也是充满的。作为构建模型的第二次尝试，我们将（4）替换为：UopR（−）A）Crep= defC rep）C rep，然而，在满足（A1）方面仍有一个技术问题。如前所述，公理（C1）-308R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295（完全。此外，函子R（−）保持极限，因为它有一个左伴随（也由R（−）给出）。仍然R（−）：Crepop→ Crep在（A1）的意义下并不弱地产生极限，因为形式为RΔ的图的Crep中的给定极限锥不需要在函子R（−）的像中直到相等。我们通过考虑而不是C这是我们对A的最终重新定义：对象：三元组（A，i，P），其中A，P是Crep中的对象，i：P→RA是同构。态射：从（A，i，P）到（B，j，Q）的态射是一个映射f：B→A。我们定义函子U：A →C来映射态射f：（A，i，P）→（B，j，Q）到j−1<$Rf<$i：P→Q。显然，C和C之间存在范畴的等价性A画出了图操作代表C代表）AC代表U：A → Crep在（A1）的意义下确实具有弱生成极限的性质命题4.2函子U：A → C表示（A1）-（A4）。在讨论该模型中的容许关系之前，我们先给出PE+C的非多态类型的解释。如果A[[A]] =（A，i，C[[A]]）且A[[B]] =（B，j，C[[B]]），则A[[R]]=（1， R=R1，R）C[[A→B]] =C[[B]]C[[A]]C[[AB]] = ABA[[A→B]]=（B×C[[A]]，h，C[[B]]C[[A]]）其中jC[[A]]与m（RB）C[[A]]的最小值相同，且C[[A]]=RB× C[[A]].最后，我们考虑如何定义容许关系。类型理论PE+C是由同构（XR）→R→=X→X →P→P第十章（（XR）→R）X与η成反比。 由（1），对于参数化的逆，我们必须有，对于任何Q∈RA（A×B），（ηA，ηB）−1（（QΔ R）→ Δ R）= Q。（二）这迫使我们考虑满足（2）的关系Q的集合作为我们的容许关系的概念。幸运的是，（ηA，ηB）−1（（QΔR）→ΔR）有一个熟悉的RepR.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295309另一种描述是QTT，定义为QT={（f，g）：（AR）×（B右）|X：U A，Y：U B. （x，y）∈ Q<$f（x）= g（y）}QTT={（x，y）∈ U A× U B|A：AR，g：BR. （f，g）∈ QT<$f（x）= g（y）}（-）TT构造定义了一个闭包算子，在这个意义上它是递增的（Q<$QTT），幂等的和关于包含序单调的，如果Q TT = Q，我们称一个关系为（-）TT-闭的。 （−）TT-闭包是参数性理论中一个常见的构造，Pitts 对此进行了广泛的研究在操作设置[17，2]。从指称的角度来看，这种技术似乎也是一种普遍而有力的技术，参见。[12 ]第10段。最后，我们定义：RC（A，B）= SubC（A×B）RA（A，B）={Q∈ Sub A（A×B）|Q = QTT}命题4.3可容许关系的公理（R1）-（R4）成立。证据有趣的是，对于任何A∈ A，恒等关系ΔA是（-）TT闭的。这很容易看出等价于下面的线性分离性质：对于所有x，y∈UA，如果f（x）=f（y）对于所有f：AR，则x=y;以及这又等价于正则函数ηA：A（AR）→R是单射的。然而，我们在上面证明了这个函数是同构的。Q定理4.4上面定义的结构是PE+C的模型。证据这个定理的大部分都是由命题4.2和4.3得出的。还有待证明的是，PE的这个模型也模拟了η的多态逆。由于每个ηA都有一个逆ηA，我们只需要证明这个集合构成了参数模型中的一个元素，即，对于代数之间的任何（-）TT闭关系Q，A，B，则对（A，B）将（QΔR）→ΔR中相关的元素映射到元素与Q有关。但这发生在i <$（ηA，ηB）−1（（QΔR）→ΔR）=Q，这对（−）TT闭关系Q成立，因为QTT=（ηA，ηB）−1（（QΔR）→ΔR）。Q5λμ2中的多态类型编码通过将从λμ2到PE+C的解释与PE+C到上一节定义的任何模型的解释组合在一起，我们得到λμ2的参数模型在本节中，我们研究了这类模型中的多态λμ复合翻译将λμ2的类型σ解释为A中的对象A[[σ]]，但λμ2的项t：σ→τ不被解释为同态，而是从U（A[[σ]]）到U（A[[τ]）的一般映射（回想U（A[[A]]）=C[[A]）。为以下310R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295因此，方便的是引入A类！，具有与A相同的对象，即，三元组（A，i，P）由满对象A，P和同构i组成：P→RA. 从（A，i，P）到（B，j，Q）的态射就是从P到Q的映射。请注意，类别A！等价于Set在形式为RAforA inCrep的对象上的全子范畴。Reus和Streicher [ 22 ]将这称为“否定域”范畴，实际上我们对A中λμ 2的解释也是如此！可以被看作是他们对（简单类型）λμ的解释的多态扩展。或者，人们可以将我们的解释视为Selinger [21]的多态扩展，因为A! 是一个控制范畴的意义上的操作。前引书类别A嵌入到A ！通过映射从（A，i，P）到（B，j，Q）的态射，由f：B→Atoj−1<$Rf<$i给出。我们称λμ2的项t：σ→τ为线性的，如果它在模型中被解释为同态。我们在本节中的目标是揭示λμ2中多态类型编码的普适属性，这些属性是由我们的关系参数模型导出的。我们考虑的所有例子都取自长谷川我们获得相同的我们要强调的主要一点是，我们的结果是对任何PE模型有效的一般可定义性结果的实例，因此是对任意计算结果有效的原理的实例[14]。例5.1 λμ 2型λX。 X被解释为A中的初始对象。实际上，对于任何类型的σ，项λx：<$X。X. x σ定义了从X到X的唯一线性映射。 X为σ。这是下列一般事实的直接后果，参见。[14 ]第10段。 在PE的任何参数化模型中，计算类型为X。X被解释为A中的初始对象，并以明显的方式给出唯一线性映射。注意，λμ 2类型也被解释为A中的初始对象（对象（1， R=R1，R）是初始的）。因此，相关性paricity产生phepolymor-在λμ2中的λ的phic可定义性这一事实可以用来证明省略λμ 2中的原始类型常量，并使用多态类型λ λX。X在其位置上，事实上，在[7]中完成。类似的观察适用于PE+C的制剂。在PE+C的任何参数模型中，类型常数R被解释为A.因此，常数R可以简单地从PE+C中省略，并且同构使用计算类型X来表示。X在其位置例5.2 λ μ2型λX。（σ→X）→X，其中X在σ中不是自由的，给出一个与σ的解释线性同构的解释。 在λμ 2中，σ→ λX型正则项。（σ→X）→X和（σ → X）。（σ→X）→X）→σ不是同构。相反，它们分别对应于控制范畴A中的双重否定单子和双重否定消去的单位！.上述性质来自一般事实[14]，即在PE的任何参数模型中，类型！A=X。（A→X）→X被解释为集合C [ [ A ]上的自由A-对象。在PE+C的许多模式中，它专门针对C[[！A]]=<$<$C[[A]]，cf.第2节中关于控制同构的激励性讨论。R.E. Møgelberg，A.Simpson/Electronic Notes in Theoretical Computer Science 173（2007）295311C[（X）]。X→X）]]=RRC[（X）]。（σ→X）→（τ→X）→X）]]=RC[[σ]]×RC[[τ]]（X/∈FTV（σ，τ））C[（X）]。（σ → τ → X）→ X）]]=C[[σ]]RC[[τ]]×R（X/∈FTV（σ，τ））C[[（C. （注十） （σ→Y））→Y）]=C[[X. σ]]（Y/∈FTV（σ））见图6。 模型中λμ2类型的解释例5.3假设σ是λμ2的一个类型表达式，类型变量X只出现在正态中。作为标准，此类型在A上导出一个内函子！.我们可以通过对σ的结构的归纳来检验，这个函子可缩减为作用于线性映射范畴A的函子。在纯二阶λ-演算中，型λX. （σ→X）→X是由σ诱导的函子的初始代数。然而，在我们的λμ2模型中，第十章（σ→X）→X是由型诱导的函子的初始代数<$<$σ在线性范畴A上。此外，所有必要的结构都可以在λμ2中定义，即，初始代数的结构映射可以定义为λμ2中的线性映射，同样，给出给定代数的唯一代数映射的项。详细定义见[7]。上述事实是以下PE模型一般性质的结果[14 ]第