理论计算机科学：Martin-Léofe概念理论的一个版本及其应用于名称抽象的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）19-50www.elsevier.com/locate/entcs具有抽象名称Andrew M.皮茨a，1，2，贾斯特斯·马蒂森a，3，4和贾斯珀·德里克斯b，5a计算机实验室，剑桥大学，剑桥CB3 0FD，英国bRadboud University，6500 GL Nijmegen，Netherlands摘要本文描述了Martin-Léofe的概念理论的一个版本，它扩展了名称和结构，用于新鲜性和名称抽象，它们来自于名称集合理论。我们的目标是一个类型理论用于计算和证明（通过Curry-Howard对应关系）语法结构，这些结构在处理绑定器时捕获了熟悉但非正式的保留字：绑定，依赖类型，名称，名义集1介绍我们的目标是发展一个作为依赖类型理论的名词逻辑[15]的构造性版本。从编程的角度来看，我们希望将Agda/Coq风格的定理证明（特别是归纳定义的索引类型族和依赖模式匹配）与FreshML [21]风格的元编程结合起来，用于绑定操作的语法。实现这些目标需要建设性地对待名义集合的新鲜性概念[16，第3章]。这里我们给出一个这样的处理方法，它是Martin-Lüof型理论的一个推广。函数式编程语言FreshML是不纯的：它通过生成性来确保名称的新鲜性，（因此）避免检查本地作用域名称是否1部分由英国EPSRC计划资助EP/K 008528/1，主流系统（REMS）的严格工程支持。2电子邮件：andrew. cl.cam.ac.uk3由英国EPSRC领导奖学金（Peter Sewell）资助EP/H 005633/1，真实世界系统的语义。4电子邮件：justus. cl.cam.ac.uk5电子邮件：jasperderikx@gmail.comhttp://dx.doi.org/10.1016/j.entcs.2015.04.0031571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。20上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19··∀··--并不支持使用该词的表达的含义。该语言的原始版本在名义集合[16]中，新鲜度关系的定义涉及对有限个名称集合的量化：n#f意味着存在支持f的有限个名称集合，该集合不包含名称n。在实践中，人们经常依赖于这样一个事实，即这种关系在置换名称下是不变的，并使用下面的声音方法，该方法反映了具体的元理论版本的新鲜度，即。未 发生：为了证明n #f，选择一个在当前上下文中没有出现的名称nj（即，一个元理论上新鲜的名称）并证明（n nJ）f = f，在函数可拓性存在的情况下，这等价于证明（x）（n nJ）（f x）=f（（n nJ）x）。（通常，（n nJ）x表示在名义集合的元素x中转置名称n和nJ的结果 由于nJ#f通过选择nJ而成立，应用交换n和nj的置换（n nJ），我们得到n =（n nJ）·nJ#（n nJ）·f=f，如所需。这个证明原则被名义代数[9]/名义方程逻辑[5]所采用T#t：T等价于形式r [nJ：N] n（n nJ）. t=t：T（1）其中（n nJ）。是（对象级）名称交换操作，上下文Γ包含关于自由变量的名称的新鲜度的假设，并且Γ[n：N]6向Γ添加针对某种N的（元理论上）新名称n的额外新鲜度假设。平等判断，如（1），将公理化的类型理论介绍了节。二、我们把这种赋予定义上的平等的新鲜感称为定义上的新鲜感。 这意味着平等判断与打字判断交织在一起以一种不同于依赖类型系统的额外方式。这种方法的优点是，我们可以给出下一节将描述这样一个具有抽象名称的依赖类型理论。由于它是Martin-LéofTy pe理论的扩展，第3节描述了FreshMLTT的预期模型;我们[6]我们没有使用“非注意的”上下文n 1 # x 1：T 1，n 2 # x 2：T 2，. . 从[24，9，5，4，7]中，这里我们将使用上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1921将名词集合组织成Dybjer的带族范畴概念（CwF）[ 8 ]的实例在本CwF中，FreshMLTT的解释及其合理性（定理4.2）在第4节中给出。第5节调查了以前的工作结合名义集与依赖类型和节。6概述了需要做些什么来进一步开发FreshMLTT。特别是，关于FreshMLTT是否具有可判定的类型检查的问题是开放的。2FreshMLTT本文考虑Martin-LüofTyp e理论[14]的一个扩展，它包含可以交换、相等比较、局部作用域和抽象的变量。我们称之为FreshMLTT。其表达式的语法在图中给出1.一、 有两种可绑定的标识符，变量（x）和名称（n），表达式被标识到α等价：绑定形式是ν [n：N]，[n：N]，（x：T），α [n：N]和λ（x：T）。我们写fv（e）为表达式e的自由变量的有限集合，fn（e）为它的自由名称的有限集合。避免捕获的替换e的所有自由出现的变量x在eJ表示eJ（e/x）;名称不受替换（见节。2.1）。我们将dom（Γ）写为在上下文Γ中声明的变量和名称的有限集合例如，我们采用Agda风格的符号表示多个上下文扩展，并写为Γ[n nJ：N]而不是Γ[n：N][nJ：N]。FreshMLTT的判断形式如图所示二、得出这些判决的有效实例的规则列于附录A。我们将在下面的章节（2.12.1名字FreshMLTT旨在用作描述和计算各种语言的语法和语义的元语言。这些“对象语言”通常涉及各种名称（例如，变量名称、通信通道等）。因此，FreshMLTT具有可数无限集合N，NJ，. ∈Nsort的区别类型7，称为名称排序Γok（N-形式）ΓNwhi ch的术语代表对象语言名称。Martin-L？ofType Theory扩展上下文的一般规则Γ<$Tx∈/dom（Γ）（cTX-EXT-v）Γ（x：T）Γok（x：T）∈Γ（v-INTRO）rx：T[7]允许名称排序被其他类型的元素参数化是很自然的，但为了简单起见，我们在这里不这样做22上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19namesn∈Name（可数的有限集合）名称排序N∈Nsort（可数有限集）变量x ∈ Var（可数无限集）表达式e∈Exp：：= Γ|不|不context Γ∈Ctx：：= ⬦空|Γ（x：T）用变量|Γ[n：N]用新名称typeT∈Type：：=||N（n n）。 不ν[n：N]T名字交换局部作用域名|[n：N]T名称抽象类型|T（x：T）T相依函数型...（MLTT的其他结构）termst∈Term：：=x变量| nname|（n n）。 测试名称交换| if t = n then t else t branch on name equality|v[n：N]t本地作用域名称|α[n：N]t名称抽象|t@n固结|λ（x：T）t λ-抽象| ttapplication...（MLTT的其他结构）Fig. 1. 关于FreshMLTT允许假设某种类型的变量（即未知元素）因此当T=N时，我们假设一个未知的对象级名称N.然而，在FreshMLTT中，除了变量x、y、. . . ∈Var，存在一种不相交的可绑定标识符，元级别名称n，m，. 名字，一起上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1923⎬判断采用形式ΓJ，其中J：：= OK格式良好的上下文|不合式类型|t：T类型关系|（n：N）#T类型的定义新鲜度|（n：N）#t：T术语的定义新鲜度|T= T定义相等类型|t=t：T定义上相等的条件图二. FreshMLTT的判决具有关联的上下文扩展和引入规则：Γ∈kn∈/dom（Γ）（CTX-EXT-N）Γ[n：N] N-OkΓok [n：N]∈Γ（N-INTRO）中文（简体）类型N的变量和类型N的名称之间的区别在于后者具有固定的、上下文无关的身份：如果n和nJ是不同的名称，则布尔表达式n=nJ可转换为false;而如果x和xJ是不同的变量，则布尔表达式x=xJ是中性的。为了简单起见，我们没有显式地引入布尔类型，而是在每个类型上使用测试和分支Tt：Nn：Nt1：Tt2：Trift=nthent1elset2：T与定义等式（IFEq）如果n=n，则telsetJ=t（如果n=nJ则telsetJ=tjIF-cOMP）（其中ni=nJ）。由于这些等式，FreshMLTT的判断的有效性在用项替换名称的操作下不被保留，而用项替换变量的操作像往常一样保留有效性。相反，名称遵守一个较弱的替代纪律熟悉的工作名义逻辑：有效性的判断是保留下置换的名称，特别是在操作交换两个名称。2.2定义新鲜度在用涉及名称的对象语言进行计算时，语言表达式中的非自由发生关系是至关重要的。特别是人们经常不得不引入在当前上下文中不自由的名称这24上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19►►►在FreshMLTT中由上面提到的上下文扩展规则（cTX-EXT-N）支持：在上下文r [n：N]中，意图是将在r中声明的任何变量限制为在名称n不自由出现的对象级实体上的范围新鲜度的名义集合关系（a#x）[16，第3章]为“不自由出现”提供了一种语法独立的含义为此，有一些表达式用于交换类型或术语中的两个名称rn：NrnJ：NTΓ（n nJ）. 不和定义的等式ΓTΓΔokrn：NrnJ：Nt：TΓ（n nJ）. t：（n nJ）. 不t：T[n：N]，[nJ：N]∈Δ（FRESH-HYP-TYPE）r Δ n（n nJ）. T=T[n：N]，[nJ：N]∈Δr Δn（n nJ）. t=t：T（新鲜-HYPP-TERM）它形式化了新鲜度的基本属性：a#xaJ#x（a aJ）·x=x[16，命题3.1]。 新鲜度的另一个关键属性是给定任何元素x在一个名义集合中，有一个原子a带有一个#x。这样做的结果是消除未使用的新鲜名称假设的结构规则，这些规则来自名义方程逻辑[5]和代数[9]的工作：ΓΔTΓΔTJΓ[n：N]ΔT=TJT=TJ（N-ELIM-TYPE）ΓΔt：TΓΔtJ：TΓ[n：N]Δt=tJ：TΓΔt=tJ：T（N-ELIM-TERM）正如在引言中所解释的，FreshMLTT可以通过定义等式来判断一个名称对于一个表达式是否是新鲜的，定义等式涉及与上下文中已知为新鲜的名称进行交换Γn：NΓTr [nJ：N] n（n nJ）. T=TT（n：N）（新鲜-典型）r（n：N）#Tr [nJ：N] n（n nJ）. t=t：TT（n：N）#t：T（新鲜----足月）这种定义性的新鲜度判断是表达名称抽象的属性所必需的，我们将在下一节讨论注2.1注意，即使名称n对于表达式e不是元理论上新鲜的，也就是说，即使n在e中自由出现，定义新鲜性也可以保持。例如，n在项中是自由的，如果n=nJ，则n，否则nJ，但是[nnJ：N]是FreshMLTT中的有效判断，因为上面提到的定义平等（IF-cOMP）。（交换-类型）（掉期-期限）上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1925►►⭢2.3抽象和局部作用域名称相关函数Γ（x：T）<$TJT j（x：T）TJ（表格）Γ（x：T）tJ：TJΓ<$λ（x：T）tJ：<$（x：T）TJ（-介绍）从上下文中释放变量。在FreshMLTT中，有一些名称抽象的形成和引入规则，包括从上下文中删除一个新名称：Γ[n：N] 不（[n：N]T-表格 ）Γ[n：N]t：T（Γα [n：N]t：[n：N]T-介绍 ）名称抽象类型可用于指示某些对象语言中的语法构造是绑定器。例如，假设FreshMLTT增加了有限列表的数据类型[14，第10章]，可以为自由变量在列表l中的λ-terms引入一个依赖类型Term（l）：List（N）（使用名称sortN来表示λ-terms中的变量）。那么形成λ-抽象的操作可以被给定为类型（l：List（N））（ [n：N]Term（cons n l））Term（l）.选择名称抽象类型的符号[n：N]T是为了表明它与名义逻辑的新鲜度量化器的Curry-Howard关系[16，Sect.3.2];参见注释3.7。同时，它形式化了名称抽象的名义集合概念的依赖版本[16，第4章];见3.6节。特别是名称抽象的排除规则使用一种特殊的应用形式，称为具体化，写作t@n。我们从名义集合理论中知道，要使这种具体化有意义，就要求名称n对于要具体化的抽象t：[nJ：N]T是新鲜的;由于类型可以依赖于名称，我们也应该要求n对于类型T是新鲜的。因此，消除规则的假设将是定义的新鲜度判断Γ[nJ：N]n（n：N）#T和Γn（n：N）#t：[nJ：N]T。结论中的具体化t@n的类型应该是什么？对于依赖函数，消隐涉及进行替换以获得函数应用程序的结果类型Γt：τ（xJ：TJ）TΓtJ：TJ（τ-ELIM ）rt tJ：T（tJ/xJ）我们不能对具体化做同样的事情，并把它的结果类型取为T（n/nJ），因为正如我们在2.1节末尾所提到的，FreshMLTT判断的有效性一般不通过名称替换而仅通过名称置换来保持。8这[8]Cheney的DNTT[3]确实使用了名字替换（见该论文中的图9），但限制了具体化的名字n对于T是元理论上新鲜的，因此T（n/n′）等于在T中对n和n′进行替换的结果。定义的新鲜性是一个较弱的，因此更具有表现力的约束具体的名称。26上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19►►►►我们建议使用结果类型（n nJ）。 T和以下消除规则：T [nJ：N]T（n：N）r [nJ：N] t@n：（n nJ）. 不（二）注意，结论中的上下文必须是Γ[nJ：N]而不仅仅是Γ，因为[nJ：N] T中的绑定名n j在（n n j）中变成了自由名。T.然而，从（2）的假设（连同名称交换直到定义相等的性质）可以推导出Γ[nJ：N]（nJ：N）#（n nJ）。T和（因此）Γ[nJnJJ：N] （n个nJ）。T=（nnJJ）。T.也就是说，结果类型（n nJ）。（2）中具体化的T是独立的，直到在[nJ：N]T中选择的约束名nJ的定义相等。从系统的表达能力的角度来看，从语言学的角度来捕捉这一事实是很重要的。我们可以通过对表达式中的名称使用某种形式的局部作用域来做到这一点，我们将其写为ν[n：N]e。这样的表述可以由规则引入Γ[n：N]（n：N）#T[n：N]T（LOcAL-TYP）Γ[n：N]（n：N）#t：TΓν [n：N]t：ν[n：N]T（长期）并被计算规则Γ[n：N]（n：N）#T（LOcAL-TYP-cOMP）Γ[n：N]πν[n：N]T=TΓ[n：N]（n：N）#t：T（LOcAL-TERM-cOMP）Γ[n：N] πν[n：N]t=t：T我们将在后面看到（命题3.5和定理4.2），这些规则在名义集合方面有一个合理的解释。他们形式化的形式，当地新鲜的名字通常使用的语法操纵结构，其中的意义取决于一些新鲜的名字是一个结构（可证明）独立于哪些特定的新鲜的名字被选中;见[16，节。3.3]。当构造涉及第一类函数时，为这种名称作用域提供一种语言形式是很重要的，因为像λ（x：T）v[n：N]t这样的表达式在定义上一般不等于v[n：N]λ（x：T）t，因此局部作用域不能直接到达顶层，在上下文中变得隐式。使用局部作用域名称，我们加强（2）以获得FreshMLTT- 消除：[001 pdf 1st-31files][001pdf 1st- 31files][001 pdf 1st-31files]（rt@n：v [nJ：N]（n nJ）. 不-ELIM ）上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1927►⟨⟨⟩⟩中文（简体）中文（简体）（ABS-FORM）Γn：NΓt：TΓn：Nt：n：NT（ABS-INTRO）r（n：N）#t：nJ：NTr_t @ n：（n nJ）. 不（ABS-ELIM）rn：Nr（nJ：N）#t：Tr_n（n_n：N_t）@ n_J=（n_n_J）.t：（n nJ）. 不（绝对值-总平均值）Γ（n：N）#t： n：NT（绝对值-单位q）Γn：N（t@n）=t：n：NT图3.第三章。非绑定名称抽象的可接受规则相关的计算和唯一性（η）规则是：2019 - 05 -25 01：0102：02：0302：02：r ∈（α [nJ：N] t）@n= v [nJ：N]（n nJ）. t：v [nJ：N]（n nJ）.不-cOMP）Γt：[n：N]Tn∈/fn（t）Γt=α[n：N]（t@n）：[n：N]T-UNI q）我们将在第4节中看到，它们对于第4节中发展的名词集合语义是合理的。3 .第三章。2.4非绑定名称抽象FreshML [21]使用一种非绑定形式的名称抽象，在FreshMLTT中定义如下：（其中nJ∈/⟨⟨n: N ⟩⟩T[nJ: N](n nJ). T（3）中文（简体）α [nJ：N]（n nJ）. （四）fn（n，T，t））。 注意，n在n：NT和n：NT中是自由的，而它在[n：N]T和α[n：N]t中是有约束力的。 这种形式的可接受规则名称抽象如图所示。3 .第三章。如果Γ[n nJ：N]不等于T，则它是（FRESH-hyp-type）和交换操作（n nJ）的转换性（28上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19质的结果。 [n nJ：N] n（n nJ）。T = TJ和Γ[nnj：N]<$（nnj）。 t = tJ：T J，其中tJ和T J是从t得到的表达式上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1929⭢⭢和T通过转置n和n j的出现。它遵循Γ[n：N]πTΓ[n：N]T=ν[n：N]n：NTΓ[n：N]t：TΓα [n：N]t=ν[n：N]n：Nt：[n：N]T（五）（六）是可接受的规则。相反，我们可以将名称抽象的非绑定形式作为原语，使用图3中的规则，然后使用局部作用域名称定义绑定形式，如（5）和（6）所示当必须在多个文本位置引用对象级绑定名称时，使用FreshMLTT元语言中的非绑定名称抽象这里有一个例子。例2.2像往常一样，我们写T TJ为非依赖函数类型，当x∈/fv（TJ）时，对T j ∈ f（x：T）T j，我们将编写非专有名称抽象其中n∈/fn（T）（7）（当n∈/fn（T）（7）时，其中h定义为非约束性抽象<$n：N<$<$Tfn（T））。 在下面给出的名义集合语义中，类型NT由下式建模：名称抽象的名义集合[16，第4章]。已知这些在名义集合的范畴中与幂运算直到同构交换（参见[16，命题4.14]）;并且我们确实可以表示同构N（T TJ）=在FreshMLTT中，请选择[编辑]事实上，我们可以给出这个同构[n：N]（x：T）TJ=（y：[n：N]T）[n：N]TJ（y@n/x）（8）如下。德费恩T1[n：N]n（x：T）TJT2（y： [n：N] T）[n：N] T J（y @ n/x）我λ（z：T1）λ（y：[n：N] T）α [n：N]（z @ n）（y @ n）jλ（f：T2）α[n：N]λ（x：T）f（n：N<$x）@n使用图中的派生规则3.可以证明，如果Γ[n：N]πTΓ[n：N]（x：T）<$TJ30上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19时间：TT21⟨⟩∈在FreshMLTT中是可证明的，那么Γ►i:T1⭢T2Γ（z：T1）<$j（iz）=z：T1Γ（f：T2））i（jf）=f：T2注意，在j的子表达式f（n=n：Nnx）@n中，我们使用非绑定名称抽象n：N x，而不是α[n：N]x（对于任何nJ，α[nJ：N]x都等于α-等价），因为在应用函数f之后，我们必须在相同的名称n处具体化，以便进行类型化。3名义集我们将使用具有排序原子的名义集合来为FreshMLTT提供语义因此，我们假设有一个固定的原子集合A，被划分为可数的无限多个子集A=N N sortAN，在FreshMLTT中由名称N∈N sort的每个子集AN都是可数无限的。 我们写a，b，... 典型的A.设G是A的排列群π，它们尊重排序（πa∈AN，如果a∈AN）并且是有限的（在这个意义上，πa=a，除了有限多个a∈A）。一个名义集合是一个集合X，它配备了一个G-作用，关于这个作用，每个元素都有一个有限支集。 这意味着对于每 个 x ∈ X ， 存 在 有 限 子集A ∈f inA 满 足 （ nπ∈GA ） π·x = x ， 其 中 GA{π∈G|（α∈A）πa = a}.名义集合是我们将用Nom表示的范畴的对象，其态射是等变函数（f（π·x）=π·（fx）），具有集合范畴中的组成和恒等式我们请读者参考[16]，以了解对名义集合的介绍，特别是第16节。4.7的那本书的许多排序的版本，我们在这里使用。3.1名作为族范畴为了对FreshMLTT建模，我们将赋予Nom一个带有家族的类别（CwF）的结构[8]。一般来说，CwF由具有终端对象1的范畴C指定，以及以下结构：• 对于每个对象X∈C，一个集合C（X），其元素称为族除以X• 对于每个对象X∈C和族E∈C（X），元素的集合C（X<$E）E除以X• C语言中族和元素沿态射的重索引操作E∈C（X）f∈C（Y，X）E[f]∈C（Y）e∈C（X<$E）f∈C（Y，X）e[f]∈C（Y<$E[f]）上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1931∈∈∈∈⭢满足E[idX]=E（A∈C（X））（9）E[f<$g]=E[f][g]（E∈C（X），f∈C（Y，X）， g∈C（Z，Y））（10）e[idX]=e（e∈C（X<$E）（11）e[f<$g]=e[f][g]（e∈C（X<$E）， f∈C（Y，X）， g∈C（Z，Y））（12）• 对每个族E∈C（X），一个理解对象X.E∈C，它具有一个投影态射p∈C（X.E，X），一个类元v∈C（X.E<$E[p]）和一个配对运算f∈C（Y，X） E∈C（X）e∈C（Y<$E[f]）f，e∈C（Y，X，E）满足pf，e=f（13）v[f，e，f]=e（14）f，ep，v定义3.1我们将由名义集合和等变函数组成的范畴Nom化为CwF，如下所示：• 在一个标称集合X∈Nom上的标称集合族E的集合Nom（X）由X-指标集合族（E x）组成|x∈X）的一个依赖G作用actE∈x∈Xπ∈GExEπ·x（17）满足下面给出的有限支持性质我们将把动作E应用于x∈X，π∈G，e∈Ex，把E和x作为隐式变元，写成π·e要有资格作为作用（17），必须满足对所有x∈X，π，πJ∈G和e∈ExπJ·（π·e）=πJπ·eEπ′·（π·x）=Eπ′π·x和i·e=eEi·x=Ex（十八）（其中，i表示单位置换）。此外，还需要act满足以下有限支撑性质：对于每个x∈X和e∈Ex，存在原子的有限集合A，满足32上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19（<$π∈GA）π·x=x<$π·e=e(so特别地，A在X中支持x，因此Eπ·x=Ex，对于任何π∈GA）。在这种情况下，我们可以说A是e依赖于x的有限支集。上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1933⭢Σ（x，e）∈Σx∈XEx到π·（x，e）=（π·x，π·e），由X在• 族E ∈ Nom （X）的元素的集合Nom（X<$E）由依赖等变的依赖函数e∈x∈XEx组成，在π·（ex）= e（π·x）∈Eπ·x的意义下，对所有x∈X和π∈ G。• E ∈ Nom （ X ） 沿 f ∈ Nom （ Y ， X ） 的 重 指 标 化 是 Y 指 标 集 族 E[f]（Ef y|y∈Y） ，且G-αt∈E ：若e∈E[f]y=Efy，则新的wge∈Eπ· （ fy ） =Ef （ π·y ）=E[f]π·y（利用f是Nom中的态射，是等变的）. 类似地，e∈Nom（X<$E ）alongf∈Nom（Y ，X ）的重索引是e[f]λ（y∈Y）e（fy），其中f在Nom（Y∈E[f]）中，因为e是完全等方差的，而f也是等方差的.• 对于每个E∈Nom（X），理解对象X.E∈Nom是由集合的不相交并给出的名义集合x∈XEx配备G-作用映射第一个分量和E在第二个分量中的依赖G作用注意，通过Nom（X）的定义，每个（x，e）∈x∈XEx关于这个G-作用是有限支撑的，因此X.E确实是一个名义集。投影态射p∈Nom（X，E，X）由第一个投影p（x，e）x给出。类属元素v∈Nom（X.E<$E[p]）由第二投影给出：v（x，e）e∈Ex= E [p]（x，e）。给定E∈Nom（X），f∈Nom（Y，X）和e∈Nom（Y∈E[f]）的对是等变函数通过将每个y∈Y映射到f ∈f，e∈y（fy，ey）∈X.E给出了f ∈ f，e∈Nom（Y，X. E）.很容易检查这些定义是否满足（9）注3.2对于CwF的每个对象X ∈ C，我们可以通过对每个E，EJ∈C（X）取态射C（X）（E，E j）为C（X.E <$E j [p]），使C（X）成为范畴，态射C（X）（E，E j）具有由类属元素给出的恒等式和由eJ<$eeJ[p，e<$]给出的复合。则映射E∈C（X）<$→ p ∈C（X.E，X）扩张为片范畴的一个完全忠实函子C（X）→C/X（19）E→eEJX. 好吧，好吧，好吧。EJpzX重新索引操作被映射到切片之间的回调函子，因为对于每个E∈C（X）和f∈C（Y，X），Y. E[f]fp，v 第十章E（二十）pYcFpXc是C语言中的回调;参见[11，命题3.9]。当C=Nom时，函子（19）不仅是完全的和忠实的，而且本质上是满射的，因此是等价的。这p34上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19X-指标集族（e∈ExF（x，e））上的G -作用 | x ∈ X)by mappingE∈C（X）F∈C（X.E）<$EF∈C（X）f∈C（X.EEF）f∈C（X<$F）e∈C（X<$E）appfe∈C（X<$F[X <$idX，e<$]）（EEF）[g] = EEF（E[g]）（F[EEF，v]）(lamf）[g]= lamf[g p，v]（appfe）[g]= app（f [g]）（e[g]）app（lamf）e=f[xidX，e]lam（app（f[p]）v）=f见图4。 CwF中的类型是因为，给定Nom /X中的p：E→X，X-指标集族（p−1{x}|x∈X）从E的G -作用继承了一个依赖G-作用（因为p是等变的）;并且对于每个x∈X，如果A在E中支撑e并且pe = x，那么在定义3.1的意义下，它是e∈p−1{x}依赖于x的支撑。所以（p−1{x}|x∈X）是Nom（X）的一个对象。它由函子（19）发送到π1：<$x∈X p−1{x}={（x，e）|pe = x} → X它在Nom/X中通过第二投影函数同构于p：E→Xπ2：（x，e）<$→e，其逆是e<$→（pe，e）。3.2Nom中的类型马丁-勒维的类型理论的上下文、上下文中的类型、上下文中的项和项替换分别用词、族、元素和态射在CwF中解释;见[11，Sect.3.5]。CwF以无名（de Bruijn索引）风格提供了类型理论语法的基本代数公式，因此可以将每个类型形成构造转换为CwF内的等效结构。例如，图4中给出了对应于多类型的额外结构（cnt，lam，app）。由于Nom是一个topos，因此特别是局部carbohydrate闭的，从注3.2可以得出，作为CwF，Nom具有这种结构。在这种情况下，我们可以这样描述（numb， lam， app）• E：给定E∈Nom（X）和F∈Nom（X.E），首先注意，我们得到一个相关的f∈e∈ExF（x，e）到π·fλ（e ∈ Eπ·x）<$π·（f（π−1·e））。为了得到一个家庭，e∈ExF（x，e）由那些f组成，它们有一个依赖于x的有限支集，上述行动。Nom（X），对于每个x∈X，我们取（NomEF）x为上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1935⭢.• lam：如果f ∈ Nom（X.E <$F），则对于每个x ∈ X，可以检查lam f xλ（e ∈ Ex）f（x，e）∈e∈ExF（x，e）是支持（依赖于x）的任何有限子集A，x在X中;因此lamf x∈（λEF）x。此外，xEF）。• app：如果f∈Nom（X<$EF）和e∈Nom（X<$E），则对于每个x∈X，我们有f x∈（<$EF）x<$e∈ExF（x，e）和ex∈Ex;因此appfex（fx）（ex）∈F（x，e x）=F[xid，ex]x并且可以检查x<$→appfex是依赖等变的，因为f和e是。 所以我们得到app f e ∈ Nom（X <$F [id，e<$]）。很容易看出，这些操作满足图1中的性质四、3.3在Nom中命名对象对于每种名称N∈Nsort，该种原子的集合AN一个名义集，一旦我们赋予它由函数应用π·aπ a给出的G -作用，关于它，每个a∈AN都由{a}支持。由注3.2我们得到：终结对象1上的族范畴Nom（1）等价于Nom。对于每一个X∈Nom，我们不会在一个名义集合Y和Nom（X）中的对应族之间做记号上的区分，Nom（X）中的族是常数，值为Y。特别地，对于每一种名称N∈Nsort，我们只写AN∈Nom（X）作为X上的常数族的名称对象。这个族的元素a∈Nom（X<$AN）就是等变函数a∈Nom（X，AN）.为了解释名称相等的分支，我们将在CwFNom中使用以下操作：哪里a，b∈Nom（X<$AN）e，f∈Nom（X<$E）ifeq（a，b，e，f）∈Nom（X<$E）（二十一）ifeq（a，b，e，f）xexifax=bxf x否则（x∈X）（22）3.4在上下文如果a，b∈AN是相同种类的原子N，我们通常写（ab）为G中交换a与b的置换，使所有其他原子固定。我们将动作x<$→（a b）·x从名义集合的元素提升到CwFNom中的族及其元素，如下所示36上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）19操作定义为：a，b∈Nom（X<$AN）E∈Nom（X）（a b）·E∈Nom（X）（二十三）（（ab）·E）xE（bx ax）·x（x∈X）具有相依G作用act（a b）·Exπ e作用E（（bx ax）·x）πe（x∈X，π∈G，e∈（（a b）·E）x）∈Eπ·（bx a x）·x=E（b（π·x） a（π·x））·π·x（使用a和b的等方差）=（（ab）·E）π·x换句话说，π在e∈（（ab）·E）x上的作用是π在e∈E（bx ax）·x上的作用由家庭E。同样，操作定义为：a，b∈Nom（X<$AN）e∈Nom（X<$E）（a b）·e∈Nom（X<$（a b）·E）（二十四）（（a b）·e）xe（（bx a x）·x）（x∈X）∈E（bx a x）·x=（（a b）·E）x由于（（a b）·e）（π·x）e（（b（π·x）a（π·x））·（π·x））= π·e（（bxax）·x）= π·（（ab）·e）x，使用a，b的等方差和e的相关等方差。3.5背景中的新鲜感如果X∈Nom，x∈X和a∈A，我们为通常的名义集新鲜关系写一个#x：通过定义，它意味着有一个有限子集A∈A支持X中的x，a∈/A;见[16，Sect. 3.1]。 如果E∈Nom（X），则标称集合X的新鲜度关系。E对应于新鲜度的依赖版本：如果x∈ X且e ∈ Ex，则根据定义3.1，存在某个有限子集A ∈A −{a}支持e依赖于x i ∈ a#（x，e）对标称集合X成立。在这种情况下，写一个# e是很有诱惑力的，[9]我们在上面写（bxa x）·x，而不是（axb x）·x，以表明当使用以一般置换而不仅仅是转置取值的等变函数时，我们应该将（π·E）x定义为E（πx）−1·x。当然，（bxa x）·x =（axb x）·x，因为转置是自逆的。9上午Pitts et al. /Electronic Notes in Theoretical Computer Science 312（2015）1937除了家庭元素的新鲜感，我们还需要一个家庭本身的新鲜感概念。给定E∈Nom（X）和x∈X，写“a # E x”是没有意义的， 相反，我们使用的事实是，新鲜度关系可以用等式来描述：a#x保持i（a b）·x=x对某个（或实际上任何）新鲜b保持。在CwF标称中，我们可以用分离产物的使用来代替3.4]：XAN{（x，a）∈X×AN|a #x}（25）这是乘积的一个名义子集：X上的G-作用是由下式定义的：π·（x，a）=（π·x，πa）（因为新鲜度关系是等变的）;并且关于这个动作（x，a）被A{a}有限地支持，如果A{A}在X中支持x。这个分离的产品将用于使用新名称对类型化上下文的扩展进行建模。第一次和第二次投影产量p∈Nom（X<$AN，X）p（x，a）（ 26）ν∈Nom（X<$AN<$AN）ν（x，a）a （27）第一个将被用来模拟从一个类型上下文到一个扩展为一个新名称的判断，第二个将模拟新名称本身。定义3.3给定a∈Nom（X<$AN），使用（26）和（27）中的运算，我们得到a[p]，ν∈Nom（X<$AN<$AN）。然后，对于任何族E∈Nom（X）和任何元素e∈Nom（X<$E），使用3.4节中的交换运算，我们定义a#XE（a[p]v）·E[p] =E[p]∈Nom（X<$AN）（28）a#Xea #XE<$（a [p] v）·e [p] = e [p] ∈Nom（X<$AN<$E[p]）（29）注意（28）中的集合族的相等性不仅意味着对所有（x，b）∈X<$AN，集合E（axb）·x和Ex相等，而且意味着这两个集合族上的依赖G-作用相等。从定义3.3可以很容易地得出以下结果：命题3.4假设a，AJ∈Nom（X<$AN）且e∈Nom（X<$E）。然后a #XEX（a）aJ）·E（30）a#XeaJ#X（a aJ）·e38上午Pitts et al. /Electr