替代和粘合剂：理论计算机科学电子笔记中的替代monoidal结构与粘合剂的比较和对比

理论计算机科学电子笔记173（2007）3-16www.elsevier.com/locate/entcs摘要：替代和粘合剂邀请地址John Power约翰·鲍尔1，2爱丁堡大学信息学院摘要我们总结了Fiore等人 对于自由余补，给定S在（部分）伪单子Tcoc−= [（−）op，Set]上的伪分配律，我们可以定义一个典范置换monoidal结构，范畴[（S1）op，Set]，概括了Fiore等人的用于carbohydrate上下文的替换monoidal结构：这为上面的例子提供了一个自然的替换结构。我们给出了一个具体的描述，这种替代monoidal结构在充分的一般性。然后给出绑定签名的一个公理化定义，并给出了绑定签名的一个初始代数语义定理，再次推广了Fiore等人的定义和定理研究的一个微妙的延伸包括Gabbay和Pitts在他们对粘合剂的非常不同的分析中研究的P b（Injop，Set）范畴，我们将其与Fiore等人的分析进行比较和对比。保留字：替换，绑定签名，初始代数语义，伪分配律。1引言我很荣幸也很高兴能在庆祝戈登·普洛特金60岁生日的MFPS特别会议上为了纪念这一时刻，我将发表我认为是他最有趣的论文之一，抽象约束和变量绑定，由他的两个门徒MarceloFiore和Daniele Turi共同撰写[4]，后来由我和他以前的学生MikiTanaka公理化[22，23，26，27，28，29]。在我看来，Fiore等人论文的标题是用词不当：这篇论文主要不是关于变量绑定，而是关于变量替换。即1这项工作是在EPSRC基金GR/586372/01的支持下完成的，A Theory of EECtions for Programming Languages和访问AIST，Senri-Chuo，Japan。2电子邮件：ajp@inf.ed.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.0244J. Power/Electronic Notes in Theoretical Computer Science 173（2007）3最清楚地看到，也许是通过比较它与另一篇论文，也表面上是关于变量绑定，出现在同一个会议，LICS 99，另一篇论文是Gabbay和Pitts的菲奥雷等人的论文是错综复杂的，但人们可以很容易地通过它线程路径如下。作者首先定义范畴F是有限集合和所有函数范畴的骨架。然后他们考虑函子范畴[F，Set]并在其上定义一个代换么半群结构·，这样做之后，利用[F，Set]的有限积结构和代换么半群结构，他们定义了绑定签名幺半群和幺半群的概念，其中幺半群部分的幺半群定义本身就使用了·。最后，他们陈述并证明了一个初始的代数语义定理，该定理的陈述又内在地涉及·。因此，他们论文的核心是描述和分析范畴[F，Set ]上的置换么半群结构·。我们在第2节中更详细地总结了他们的论文。与Gabbay和Pitts的论文相比。从范畴论的角度来看，他们的论文也是令人费解的，但原因有些不同。此后，他们以一种更便于我们理解的方式修改了他们的阐述，所以这就是我将在这里使用的表述[7，19]。而不是研究[F，Set]，他们研究的是一个到Pb（Inj，Set）的分类方程，其中Inj是有限集合和所有整数集合的分类的集合，而Pb（Inj，Set）是由那些保持回调的函子确定的[Inj，Set]这有时被称为Schanuel topos ， 它 对 应 于 Fraenkel-Mostowski 集 [7] 和 标 称 集 [19] 的 范 畴 NomGabbay和Pitts根本没有考虑范畴上的替换么半群结构，这样的结构在他们的分析中没有任何作用。相反，他们的分析重点是在重命名下的约束项的不变性和引入一个新名字的可能他们对约束本身的分析比Fiore等人的分析更微妙，因为回调的保留使他们能够给出一个有意义的约束项支持的概念，这是一个在Fiore等人的设置中无法类似地研究的概念所以Fiore等人这两篇论文中的研究自撰写以来已经经历了多年的实质性发展。但这一发展几乎完全是分开的。Gabbay和Pitts研究的显著发展与此同时，Miki Tanaka和我对Fiore等人的论文进行了公理化工作如下。 首先选择一个伪单子S，J. Power/Electronic Notes in Theoretical Computer Science 173（2007）35Cat生成上下文。例如，Fiore等人然后，我们观察到，将小范畴C发送到预层范畴[Cop，Set]的构造可以被表征为C的自由余限完成。所以，除了大小，它相当于在Cat上给出了另一个伪单子Tcoc，一个用于余完备范畴的伪单子。将Tfp应用于范畴1，然后应用Tcoc，得到Fiore等人研究的[F，Set]。从公理上讲，Fiore等人使用的所有结构都来自于他们对Cat上的伪单子S=Tfp的选择，以及S在Tcoc上的规范伪分配律，模大小[28，29]：这样的结构使得在Tcoc S上产生一个伪单子结构，从而在TcocS（1）上产生一个替换单子结构，并定义了绑定签名M和M-单子，以及一个初始代数语义定理的陈述和证明，该定理公理化了Fiore等人的命题。分析也可以被丰富和扩展，以纳入类型[23]。我们在第3节中总结了公理化。马克斯·凯利在俱乐部上的工作值得一提[11，12]。在20世纪60年代后期这个想法是给一个范畴理论的替代说明。在这方面，他没有像菲奥雷等人那样走得那么远，确切地说，他没有公式化或证明初始代数语义定理。但他们的一般设置是他的变体：在他们考虑[F，Set]，或等价地考虑Fop上的离散纤维化范畴时，他考虑Cat/Fop：前者是后者的一个完全子范畴，凯利但是，如上所述，菲奥雷等人进一步发展了他们的帐户。先验地，不清楚如何将Fiore等人两组使用不同的类别。典范代换幺半群结构是第一个的核心，而第二个则根本没有研究。但是我们可以做以下的事情：取上面的替换公理化，修改它以允许保持单态的拉回，并考虑特殊情况，其中S是小对称monoidal范畴的伪单子Tsm1，其中单位是终端对象[28，29]。由此得出（S1）op是Inj，并且对于重新推pimorphisms的ut的自由余补，用（部分）伪单子Tp o cc代替Tcc，TpoccS（1）是Pb（Inj，Set），这是由Gabbay和Pitts确定的。因此，我们有一个典型的替代monoidal结构的Gabbay和皮茨断言单态回撤保持的条件在Fiore等人的设置中也是有意义的我们的希望是，这种新的公理化将提供一个数学基础上，人们可以作出精确的比较两种方法之间我们在第4节中概述了这个新的公理化。6J. Power/Electronic Notes in Theoretical Computer Science 173（2007）3ρi最后，我们应该提到，虽然Gabbay和Pitts2Fiore等人对变量取代和结合的解释在本节中，我们简要概述了Fiore等人的论文[ 4 ]中的主要论点设F表示有限集合范畴的骨架以及它们之间的所有函数。Fiore等人考虑了函子范畴[F，Set]。其思想是，对于[F，Set]的任何对象X，集合X（n）被理解为模α-转换的项的集合，包含至多n个变量。Fiore等人然后通过Fiat，描述了[F，Set]上的替换monoidal结构如下。定理2.1给定[F，Set]中的X和Y，以及给定 F中的m，定义（X·Y）m为成为平等者（1）A=（n∈NXn×（Y m）n）/μ其中等价关系由（t; u1，. ，un）n（tJ; uJ，. ，uJJ）如果1N且仅当存在一个箭头ρ：n → NJ使得X（ρ）（t）= TJ和ui= UJ.然后，集合族（X·Y）m通过它的定义的普适性而正则地扩展，以给出范畴[F，Set]上的monoidal结构。在描述了替换么元结构之后，Fiore等人定义了绑定签名的概念。在没有绑定器的情况下，签名将由一组操作O和一个函数ar：O−→N组成，该函数将每个操作发送到一个由自然数给出的arity。但是，如果一个人想允许绑定器，他需要在arities中更复杂，因为他不仅想要一个自然数，而且要考虑每个参数中绑定的变量的数量。所以一个arity应该由一个有限的自然数序列组成Fiore等人因此做出了以下定义。定义2.2绑定签名由一组操作O和一个函数ar组成：O−→N。例2.3考虑无类型λ-演算M：：= x| λx.M |MM它有两个操作符，一个用于lambda，一个用于应用程序，其中arities为1，分别为：λ-abstraction有一个参数，绑定一个变量，application有两个参数，不绑定任何变量。给定一个绑定签名，Fiore等人在[F，Set]上生成了他们所谓的签名内函子，如下所示。J. Power/Electronic Notes in Theoretical Computer Science 173（2007）37定义2.4给定一个绑定签名，由签名生成的签名内函子发送一个[F，Set]的对象X到（δn1X）× ··· ×（δnkX）联系我们|ar（o）=（ni）1≤i≤k}其中δX定义为X（1 + −）。例2.3显示了在实践中如何理解这一点：δX = X（1 + −）给出了绑定在一个变量上的思想的数学公式。更一般地说，合数δnX，也就是X（n+ −），允许在n个变量上绑定的概念。 为了构造λ-项，λ-抽象是一个一元运算，需要使用一个额外的变量，因此它的arity是1，而应用是一个二元运算，两个参数都不需要任何额外的变量，因此它的arity是0，0。Fiore等人他们称这个定理为初始代数语义定理，因为T（1）描述了由T生成的项。初始代数语义定理的支持结果和定义，模一个微小的修正，可以表示如下。定理2.5对于任何绑定签名，存在诱导内函子的正则强度为X·Y−→对于指向的对象Y.推论2.6对于任何绑定签名，如果T是由在[F，Set]上生成的自由单子，则T在点对象上关于·具有典范强度。回想一下，对于monoidal闭范畴上的任何monad，对尖对象的强度都会在1上的自由代数上产生一个标准monoid结构[27]。因此，我们立即有以下内容。推论2.7对于任何绑定签名，[F，Set ]的对象T（1）具有关于替换幺半群结构·的规范幺半群结构。Fiore等人不可避免地需要一个相干条件来将T（1）的幺半群这就引出了下面的定义。定义2.8设F是monoidal闭范畴（C，·，I）上的强（在点对象上）内函子F-幺半群（X，μ，m，h）由幺半群（X，μ，m）组成，8J. Power/Electronic Notes in Theoretical Computer Science 173（2007）3C和F-代数（X，h）使得图F（X）·XtX），X F（X·X）Fμ）FXh·X hV VX· X） Xμ上下班F-幺半群形成了一个范畴，其映射由C中的映射给出，既保持F-代数结构又保持幺半群结构。定理2.9（初始代数语义）对于任意的绑定签名φ，范畴[F，Set ]的对象Tφ（1）与它的规范φ-代数结构和关于φ的么半群结构一起构成初始φ-么半群。证据根据推论2.6和2.7，对象T（1）必然存在，并且在它上面有一个标准幺半群结构。由于自由性的一般原因，T（1）上的幺半群结构和-代数形成一个-幺半群。T（1）是1上的自由π-代数的事实，以及幺半群映射必须保持幺半群的单位的事实，确定了从T（1）到任何π-幺半群的唯一映射。断言它是么半群映射，则等价于定义么半群时的相干条件。Q这是Fiore等人3Fiore等人关于变量取代和约束的解释在第2节中，我们总结了Fiore等人的论文的发展主线在本节中，我们总结了田中三木和我自己对菲奥雷等人的论文进行公理化的工作这项工作已经发表，特别是在[28，29]，所以我们不拼出进一步的例子在这里，而只是解释如何公理化的发展扩展菲奥雷等人。关于伪单子、伪代数等的精确定义，参见[27]。这些概念比2-monad的概念复杂一点，2-monad的概念又比普通monad的概念复杂一点，但也仅仅是一点点。我们的两个主要例子如下。例3.1设Tfp表示Cat上的伪单子，它是有限乘积的小范畴。2-范畴Ps-Tfp-Alg具有由具有有限积的小范畴给出的对象，由在通常意义上保持有限积的函子给出的映射，即，直到相干同构，以及由所有自然变换给出的2-胞腔所以Ps-Tfp-Alg是2-范畴FP，范畴Tfp（C）是自由的J. Power/Electronic Notes in Theoretical Computer Science 173（2007）39）C上的有限产品类别。设C= 1，范畴Tfp（C）在等价的情况下由Fop给出。例3.2由于规模的原因，Cat上没有有趣的伪单子用于共同完成范畴：小的上完全范畴必然是前序范畴，小范畴上的自由大的上完全范畴不存在于Cat中。但是有一些经过充分研究的技术来处理这种担忧[27]，让我们可以安全地忽略它。假设我们这样做，有一个伪单子Tcoc的共同完成范畴。对于任何小范畴C，范畴Tcoc（C）由预层范畴[Cop，Set]给出。关于伪单子之间伪分配律的精确定义，参见[27]。同样，它们比普通的分配律稍微复杂一点，但也只是稍微复杂一点，唯一的实质性复杂性在于相干细节，即，一个关于哪些二维图必须彼此一致的声明。先把这一点放在一边，我们的主要例子如下[27，28，29]。例3.3存在Tfp对Tcoc的正则伪分配律。Ob- serveTcoc Tfp（1）等价于[F，Set]。伪分配律定义的直接结果如下[27，28，29]。定理3.4给定Cat上伪单子的伪分配律δ：ST −→ TS，伪函子TS支持一个标准伪单子结构，并且范畴TS（1）在其上既有标准伪S-代数又有伪T-代数结构。对于Cat上的任意伪单子T，设tC，D是复合的unCurryingD）[C，C×D]T[TC，T（C×D）]我们称t为由伪单子T诱导的伪强度。定理3.5给定Cat上的一个伪单子T，范畴T1有一个正则单子结构，其乘法由T诱导的伪强度定义• ：T1×T1t1，T）1T（1×T1）=）T21μ1）T1单位为η1：1）T 1结合性和单位同构是由T的乘法和单位的结合性和单位同构与伪强度的结合性和单位同构共同生成的。此外，乘法·：T1 × T1 → T1是T-代数在其第一个变量上的伪映射，10J. Power/Electronic Notes in Theoretical Computer Science 173（2007）3）T1也就是说，有一个连贯的同构2tT1，T1T1 ×T1T（T1×T1）T·）2μ×idv=μvT1×T 1）T 1·例3.6考虑Cat上的伪单子Tcoc Tfp。通过例3.3，范畴Tcoc Tfp（1）等价于[F，Set]。因此，通过定理3.5，[F，Set]获得了一个标准的monoidal结构。根据定理的最后一行，对于[F，Set]的每个对象Y，函子−·Y：[F，Set]−→[F，Set]是Tcoc Tfp-代数的伪映射由于每个函子X：F−→Set都是可表示的余极限，并且Fop的每个对象都是生成对象1的副本的有限积，而生成对象1又是张量·的单位，因此我们可以将X·Y计算为以下形式的正则余均衡器：（X·Y）m=（Xn×（Y m）n）/nn∈ N精确地产生Fiore等人的稍加注意，例3.6中的论证可以扩展到如下的完全公理化的一般性[28，29]。对于Cat上的任意伪单子S，如果（A，a）是任意伪S-代数（的一部分），例如，S1或[（S1）op，Set]，且α是范畴Sk的对象，对任何小范畴k，特别是对任何自然数，我们可以定义函子αA：Ak→A如下：Ak=Ak×1S×）α（SA）Sk×Skev）αSAa）A这种构造是集合上（无穷）单子的每个代数都支持与单子对应的Lawvere理论的每个操作的语义的想法的常规扩展，这在[21]中的计算效应建模中得到了利用。定理3.7给定Cat上的伪单子S和S除以Tcoc，给定X，Y在[（S1）op，Set]中，可以计算X·Y的值在c∈S1时，（X·Y）c=n∈S1XcJ×（cJ[（S1）op，Set]（Y））c（1）我们现在从替代转向约束。在Fiore等人的绑定签名定义（定义2.2）中，arity（n1，···，nk）产生两个数据：对于每个i，每个n i告诉你应用X（1 +−）的次数，k告诉你需要乘以多少个这样的X（n i + −）。但在更复杂的设置中，需要更具体的说明，因为自然数的有限序列并不指定要使用哪种粘合剂，以及要使用的粘合剂的组合：Fiore等人使用J. Power/Electronic Notes in Theoretical Computer Science 173（2007）311Carriage binders和采取产品; Tanaka使用线性binders和采取张量积;但在BunchedImplications中，人们可以选择binders和产品或张量。这些考虑导致以下一般定义：定义3.8对于Cat上的伪单子S，绑定签名S =（O，a）是一组操作O和一个元函数a：O→ArS其中ArS的元素（k，α，（ni，βi）1≤i≤k）由自然数k和范畴Sk的对象α组成，当1≤i≤k时，由自然数ni和范畴S（ni+1）的对象βi组成这里的k和ni有了绑定签名的定义，我们就可以像菲奥雷等人那样导出一个签名内函子，然后讨论内函子的代数。我们将重载1的使用：它将引用类别1的唯一对象1，并通过S单位引用其在S1中的图像。当我们写1时，我们的意思是列表1，.，1的长度由我们写作的上下文决定。我们进一步证明了f（x1，.，xn）到f（x），并且f（x1，.，xn，−）到f（x，−）。使用这些符号缩写，我们定义诱导签名内函子如下。定义3.9给定一个绑定签名，[（S1）op，Set]上的签名内函子将X发送给X=α[（S 1）op，Set]（X（β1S1（1，−）），. ，X（βkS1（1，−）o∈ Oa（o）=（k，α，（ni，βi））定义3.9中构造的函子与Fiore等人的定义2.4一致在Fiore等人之后，我们通过表示签名和它由签名生成的函子例3.10设S为Tfp，即， 考虑Fiore等人的骨水泥粘合剂。我们的k是他们的王。 我们的α是Tfp k的对象1，它生成函子[F，集合]k−→[F，集合]定义k-fold乘积。 我们的ni就是他们的ni。 我们的βi是Tfp（ni+1），生成函子βiF：Fni+1−→F将（a1，···，ani，b）发送到a1 +. +ani+b。因此，Fiore等人的每一个对于一个具体的例子，回想一下例2.3，无类型λ演算M：：= x| λx.M|app（M，M）12J. Power/Electronic Notes in Theoretical Computer Science 173（2007）3用它的两个运算符λ和app，用Fiore等人设2被定义为具有元素x和y。然后，在我们的术语中，对于第一个算子λ，arity由k= 1给出，α∈Tfp（1）是1，n1是1，β1是Tfp（2）的元素x×y对于应用app，k= 2，α是Tfp（2）的元素x×y，n0=n1=0，两个βi我们应该提到的是，不仅是我们的绑定签名先验更一般比菲奥雷等人，但似乎有一个我们的绑定签名，没有菲奥雷等人例3.11考虑我们意义上的签名由一个元组成，k= 1，α是Tfp1的生成对象1，β1由例3.10中的符号对y×y给出。一个代数将由一个预层X和一个自然变换X（2× −）−→X（−）它似乎不能被构造成任何签名的代数，在Fiore等人的意义上：注意y×y生成X（2×−）而不是X（2 + −）。例3.11中的签名似乎没有计算意义。这并没有过分地困扰我们：我们关于签名的主要定理是一个肯定的定理，断言任何签名都会产生初始代数语义，因此在该结果中包含不感兴趣的例子并不会困扰我们。从这一点出发，我们可以逐字扩展Fiore等人在推广证明中，唯一的难点是推广定理2.5的证明，即。e，构造关于指向对象的Rollover·的强度：证明出现在[29]中。总结起来，我们有以下几点。定理3.12（初始代数语义）给定Cat上的任意伪单子S，以及S在（部分）伪单子T coc−=[（−）op，Set]上的伪分配律，并且给定任意绑定签名，范畴[（S1）op，Set]的对象T（1），以及它的关于·的规范的n-代数结构和么半群结构，形成初始n-么半群。例子包括Fiore等人此外，分析扩展到包括类型和丰富，从而允许递归[23]。4扩展到包括Gabbay和Pitts正如在引言中提到的，Gabbay和Pitts在[6，7]中研究了重命名下约束项的不变性，而不是研究替代，J. Power/Electronic Notes in Theoretical Computer Science 173（2007）313具体地说，他们从[Inj，Set]到那些保持回调的函子的完整子范畴的限制使他们能够明智地谈论绑定项的支持。人们可以根据第3节的公理化来分析这个思想。例4.1令S=Tsym1是Cat上的伪单子，对于具有终结对象的小对称monoidal范畴。因此（S1）op=Inj.在[29]中证明了Tsym1在Tcoc上存在一个典型的伪分配律，因此定理3.12适用。因此，给定任何绑定签名，我们可以考虑从Inj到Set的函子T（1）。注意这个函子保持拉回：T（1）n的一个元素相当于一个至多n个变量的项，拉回条件断言，如果给定变量在x1，···，xn，y1，···，ym 之 间 的项s和变量在y1，···，ym，z1，···，zk之间的项t，并且x因此，拉回条件允许Gabbay和Pitts公理化地谈论一个项的支持，这相当于表达该项所需的最小变量集例4.1表明，如果我们可以修改第3节的公理化，对于小范畴S1具有推出的那些例子，用Pb（（S1）op，Set）代替[（S1）op，Set]，那么就有可能为Fiore等人以及Gabbay和Pitts的思想找到一个共同的数学基础这样的修改似乎是可能的。但存在如下问题：例4.2令S=Tfp，即，考虑一下菲奥雷等人的设定。给定一个绑定签名，一般情况下，T（1）不会保持回调。因为范畴F有一个终端对象1，而映射在F中沿着自身从2到1的拉回是4。保留这种回撤意味着，给出一个最多有四个变量的项就是给出一对最多有两个变量的项，每个项都服从一个相干条件，即使在非常简单的例子中，这也是错误的。困难在于F有太多的回调，所以要求保留F的所有回调基本上排除了所有有趣的绑定签名的例子。因此，人们需要考虑一些回调，但不是所有的回调。一个自然的解决方案是要求保留单态对的拉回：这与Gabbay和Pitts一致，因为Inj中的所有映射都是单态的，在[F，Set]中，Fiore等人的T也是如此在[P，Set]中，即，对于Tanaka束的情况更复杂但类似。因此，我们建议修改第3节的分析如下。定义4.3设P Oe表示2-范畴的小范畴，它具有满态的推出和保持这种推出从而保持所有满态的函子。给定P Oe的对象C，设P bm（Cop，Set）表示由保持单式拉回的函子确定的[Cop，Set]14J. Power/Electronic Notes in Theoretical Computer Science 173（2007）3phisms。命题4.4 2-范畴P Oe是一个Carnival伪闭2-范畴[10]，因此支持P Oe-富集范畴的概念，参见[23]。命题4.5我们可以将[28，29]的各种伪单子，特别是T fp，从Cat提升到P Oe，并且提升具有典型的P Oe-富集或等价的伪强度。注意到构造Tpoecoc将一个具有满态推出的小范畴C发送到一个尊重C中满态推出的自由余完备化，即Pbm（C，Set）[14]，规范地扩展到P Oe上的一个P Oe-丰富的伪单子.定理4.6具有满态推出的范畴T PoecocS（1）在满足定理3.5的凝聚条件的情况下具有一个正则替换幺半群结构。定理4.7给出了约束签名半群和约束签名幺半群的定义，以及定理3.12的陈述和证明，将初代数语义定理推广到P O e的情形。上面的细节依赖于一些微妙但直接的2-范畴定义，这些定义尚未在文献中出现。对于各种构造的显式描述，对于任何具有满态的推出的小范畴C，和过滤的上极限在P bm（C，Set）中是逐点的，这对于所考虑的特定极限类是非常特殊的。因此，上述结构的明确描述并不困难。现在的结果使我们能够精确地比较菲奥雷等人这种比较可能与Gabbay及其同事[5，8]最近关于替代的非范畴理论研究有关。5进一步工作最明显的进一步工作项目是本文件的重点，因此我将不在此重复。但除此之外，本文还专门针对替代和约束给出了一个范畴论解释。虽然替代和绑定的概念是句法的，在本文中，我们没有解决的问题，给出一个一般的语法。因此，一个明显的问题，为进一步的工作是提供这样一种语法，其包括Fiore等人这似乎是最不可能的，有一个自然的语法被发现，符合本文件的全部一般性。然而，一个一般的语法肯定应该存在与范畴理论模型在这里给出。伪交换单子的概念[10]可能是相关的。J. Power/Electronic Notes in Theoretical Computer Science 173（2007）315Hofmann还在[9]中研究了绑定结构的逻辑原理，这是在LICS 99上发表的第三篇关于绑定的论文。因此，人们希望将逻辑原理，如高阶项归纳法，纳入这里的公理化引用[1] S.安布勒河L.克罗尔和阿尔贝托·莫米利亚诺。 高阶抽象代数上本原递归的定义方法Merlin 2003，ACM数字图书馆，2003年。[2] 詹姆斯·切尼走向名称、约束和范围的一般理论。 Merlin 2005，ACM数字图书馆，2005年。[3] M. Fiore，Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus。 Proc. PPDP02，ACM出版社，第26-37页，2002年[4] M.菲奥雷湾，澳-地Plotkin和D.图里抽象变量和变量绑定。见Proc. LICS 99，第193-202页。IEEEPress，1999.[5] M. Gabbay和A.马蒂森作为一个名义代数的避免捕获替换。InProc. ICTAC 2006，LNCS 4281，pages 198[6] M. Gabbay和A. M.皮茨一种新的涉及绑定的抽象排序方法。 见Proc. LICS 99，第214-224页。IEEEPress，1999.[7] M. Gabbay和A. M.皮茨一种新的变量绑定抽象查询方法。Formal Aspects of Computing13：341[8] M. Gabbay，S. RotaBul'o，andA. MARIN。 订阅内容是一个Fraenkel-Mostowskisets的p p p e r y。已提交。[9] M. Hofmann，Semantical Analysis of Higher-Order Abstract，2004。在Proc. LICS 99，IEEE出版社，第204-213页[10] M. Hyland和A. J. Power。伪交换单子和伪闭2-范畴J. Pure and Applied Algebra175：141[11]G. M.凯利连贯性的抽象方法。在Coherence in categories中，LNM 281，第106-147页，1972年。[12] G. M. 凯利关于俱乐部和教义。在类别研讨会悉尼1972/73，LNM 420，第181[13] G. M. 凯利自由代数、自由幺半群、上极限、相关层等的超越有限构造的统一处理。Bull. Austral.Math. Soc，22：1[14] G. M. 凯利 丰富范畴理论的基本概念，伦敦数学。Soc. 讲义系列64，剑桥大学出版社，1982年。[15] M. Lenisa，A. J. Power和H.渡边操作语义学的范畴理论。理论计算机科学327：135[16] M.米库兰和我。Scagnetto，一个有类型的HOAS和语义框架。PPDP 2003，ACM出版社，第184-194页，2003年[17] M.诺里什带有绑定器的类型的递归函数定义。在Theorem Proving in Higher Order Logics 2004中，LNCS 3223，第241-256页[18] P.[19] A. M. 皮茨 名词逻辑：名称与约束的一阶理论信息和计算183：165[20] A. M. 皮茨Alpha-Structural Recursion and InductionJournal of the ACM 53：459[21] G. D. Plotkin和A. J. Power。代数运算与类属效应。在Proc. MFCSIT 2000，Applied CategoricalStructures11：69[22] A. J. Power。变量绑定的统一范畴理论方法。Merlin 2003，ACM数字图书馆，2003年。16J. Power/Electronic Notes in Theoretical Computer Science 173（2007）3[23] A. J. Power和M. 田中递归类型绑定签名的范畴理论语义。已提交。[24] D. 皮姆《逻辑的语义学与证明理论》，应用逻辑丛书。Kluwer，2002年。[25] M. R. Shinwell，A. M. Pitts和M.贾贝 Fresh ML：Programming with Binders Made Simple. 在Proc.ICFP 2003，ACM Press，第263[26] M.田中线性绑定器的抽象变量和变量绑定。 在Proc. MFCS 2000，LNCS 1893，第670-679页[27] M. 田中伪分布律和变量绑定的统一框架爱丁堡博士论文，2004年。[28] M. Tanaka和A. J. Power。变量绑定的伪分布律和公理化。高阶与符号计算19：305[29] M. Tanaka和A. J. Power。子结构逻辑中绑定签名的统一范畴理论语义。Journal of Logic andComputation，16：5[30] C. 城市 和S.伯格韦尔Isabelle/HOL中实现的一个名义型数据集递归组合器。在Proc. IJCAR2006，LNCS 4130，第498-512页