无类型λ-演算的Engeller型模型的范畴论表述

理论计算机科学电子笔记161（2006）43-57www.elsevier.com/locate/entcs非类型λ-演算的Engeller型模型的范畴论表述Martin Hylanda，4Misao Nagayamab，1，5，John Powerc，2，6和Giuseppe Rosolinid，3，7a剑桥大学纯数学和数理统计系，Wilberforce路，Cambridge CB3 0WB，ENGLANDb日本科学技术公司，CREST，验证和语义研究中心，国家先进工业科学技术研究所，3-11-46Nakoji，日本兵库县尼崎市，邮编661-0974c爱丁堡大学计算机科学基础实验室，国王Edinburgh EH9 3JZ，苏格兰dDISI，Univ. di Genova，via Dodecaneso 35，16146 Genova，ITALY摘要我们给出了无类型λ-演算的Engeller式模型的范畴理论公式。 为了做到这一点，我们表现出一个单子的Kleisli范畴的另一个分配律和扩展之间的等价性，并探讨了一个任意交换单子的例子与交换单子。在Set作为基范畴时，后者是有限多集单子。我们利用范畴Rel的自对偶性，即，幂集单子的Kleisli范畴，以及它的范畴理论结构，允许我们构建无类型λ演算的模型，产生Engeler模型的变体。我们用幂等交换幺半群的单子代替交换幺半群的单子，幂等交换幺半群在集合上是有限幂集单子。这并不完全产生一个分配律，所以需要更微妙一点，但是，在这种微妙的情况下，它完全产生了最初的恩格尔结构。关键词：Engeler模型，无类型λ-演算，Carnival闭范畴，分配律，交换幺半群，有限多集，有限幂集，Kleisli构造1 这项工作得到了CREST项目的支持。2这项工作得到了EPSRC基金GR/586372/01：A Theory of Exections for Programming Languages的支持3这项工作得到了MIUR项目McTati的支持4电子邮件：M. dpmms.cam.ac.uk5 电子邮件地址：m-nagayama@aist.go.jp6 电子邮件地址：ajp@inf.ed.ac.uk7电子邮件地址：rosolini@disi.unige.it1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.02444M. Hyland等人/理论计算机科学电子笔记161（2006）431引言Dana Scott证明了无类型λ-演算的任何模型，或者更直接地说，任何λ-代数，都生成一个carnival闭范畴，其中模型可以被看作是一个自反对象，即，对象D以及将指数DD展示为D的收缩的数据[20]。我们通过取柯西完备化得到这样一个范畴，等价于由模型生成的回缩范畴虽然从范畴论的角度来看是一个精细完备性的结果，但这个结果并不意味着任何λ-代数都是一个自然范畴闭范畴的对象，例如范畴ωCpo或从Rel构建的某个范畴。因此，从范畴论的角度来看，将无类型λ-演算的各种模型视为自然范畴闭范畴中的自反对象是一个正在进行的自然问题。在本文中，我们研究的特殊情况下的模型的精神提出的恩格尔在[8]，也研究了在[17]。Engeler集合PfD×D充当D对自身的一种指数。每个子集都是一个收缩的分裂，因此PfD×D是D的一个收缩。如果人们能通过一个自然的构造来理解PfD×D是一种指数精度，我们就能回答我们的问题了。考虑下面的启发式论证：如果在幂集单子P上有单子Pf的分配律，我们将把单子Pf提升到Rel。后一类是自对偶的，所以提升可以被看作是Rel上的一个comonad。范畴Rel是对称的么半群闭的，有乘积和余积，提升把乘积送到Rel的对称么半群结构，从而使得余积范畴的Kleisli范畴是闭的。根据Rel的结构，Kleisli范畴中的闭结构可以由下式给出：PfX×Y。 通过一点计算，人们可以将恩格尔结构看作是一个Kleisli范畴的相关对象。然而，这个论证失败了：自然构造并不产生Pfquamonad在P上的分配律。但我们可以退一步。假设我们用有限多集单子Mf代替Pf。这是交换幺半群的单子。 我们可以证明，在任何基余完全对称monoidal闭范畴C上的任何交换monadT上的交换monod的monad总存在分配律：见第2节。 公理化地得出Mf扩张到Kleisli范畴上的单子T的Kl（T）：见第3节。Kleisli范畴Kl（T）有一个典范对称幺半群，M的M上的六个元素是Kl（T）中的交换幺半群的M和K的交换幺半群：见第4节. 如果我们限制Set为base，范畴并取T为幂集单子P，则Kl（T）是自对偶的，并且必然存在一个使Kl（M_（ref））为p闭的外推定理：我们可以对其中的一部分给出更一般的分析只需要一点计算-因此，这提供了Engeler模型的温和变体关于Engeler模型的一系列其他变体Mf与Pf的区别是有意义的：Mf是交换的单子M. Hyland等人/理论计算机科学电子笔记161（2006）4345f是幂等交换幺半群的单子。后者涉及到一个卡氏方程，即x+x=x。正是x在方程左侧的重复，使得这里的差别至关重要。(How这个问题本身将在例2.4中描述。）我们上面给出的关于单子扩张的论证在更一般的情况下没有大惊小怪，只要我们只考虑对称运算结构而不是一般的代数结构：我们在第2节给出背景。但如果没有进一步的扩张，它不会扩展到Pf然而，回到恩格尔我们可以很容易地找到Pf作为P上的闭函子的分配律：见第3节。我们就可以解除它的乘法自然变换。唯一的困难是单子Pf的单位不能从Set提升到Rel，即，它在集合中是自然的，但在关系中不是。但这并不坏：内函子和乘法允许我们建立一个克莱斯利构造，但它是一个半范畴而不是范畴。Hayashi在[9]中对与半范畴密切相关的半函子进行了精确的研究，以建立无类型λ-演算的模型语义范畴在范畴论中已经研究很久了，例如参见[11]。单位的数据仍然存在，它提供逐点幂等元。这就足以让我们模仿上面的论证，模的温和额外微妙涉及采取和分裂幂等，返回恩格尔对这个更精细的论证的完全公理化的处理将出现在随后的论文中。这项工作留下了一个我们热衷于追求的突出的开放问题：Engeler模型是无类型λ演算的滤波器模型的简单情况。因此，随着在Engeler模型的范畴理论公式中，作为未来的工作，我们打算扩展我们的范畴理论分析来解释过滤器模型。由于至少有一些滤波器模型是自然域，这可能需要重建域理论。这可能是一项艰巨的工作，因此我们推迟了这项工作。2分配律与提升给定范畴C上的一对单子S和T，下面的结果在文献中广泛出现，例如，在[1]中。定理2.1给出单子的一个分配律λ：ST段抬高等价于把单子T提升到范畴S-Alg。在本文中，我们将集中讨论这类分配律的一类例子，我们将描述，其中S是对称monoidal范畴C中交换monoid的monad，当这样的monad存在时，T是C上的任意交换monad。我们简单回顾一下相关的定义。给定一个对称monoidal范畴C，C上的单子（T，η，μ）的强度是一个自然变换，其分量形式为tX，Y：X<$TY−→T（X<$Y），满足四个公理，表示关于以下单子结构的一致性：46M. Hyland等人/理论计算机科学电子笔记161（2006）43T和C的对称幺半群结构[15]。一个具有强度的单子称为交换的，如果图TXT YtTX，）YT（TXY）TtX，）YT2（X和Y）∗X，T YvμXμYvT（XY））T2（XY））T（XY）TtX，Yμ X Y对所有的X和Y都是对易的，其中t是使用C的对称性从t定义的[15]。给定一个任意对称幺半群范畴C，我们可以很容易地定义C中的交换幺半群范畴CMon（C）。它天生就有一个健忘的函子U ：CMon（C）−→C。 总的来说，健忘函子不需要有左伴随。但它在一个很宽的这类情况，包括我们主要感兴趣的所有情况：参见[14]，了解一些这样的一般条件。对于一个比必要的更严格的类，但包括我们的主要例子，如果C是闭的且上完备的，则左伴随存在。在C是集合的情况下，C中交换幺半群的单子是Mf，有限多集单子。扩展该符号，我们将用Mf表示任何对称幺半群范畴中的交换幺半群的单子，其中左伴随和因此单子存在。例行检查U ：CMon（C）−→C总是满足另Beck单子性定理的条件把这些放在一起，我们有以下几点。定理2.2若C是上完全对称幺半群闭范畴，则C中的交换幺半群范畴CMon（C）是C上的一元范畴。这个定理允许我们把我们的主要一类分配律的例子表示如下，参见[15]。例2.3设C是一个上完全对称monoidal闭范畴，T是C上的一个交换monad。证明T提升到C中的交换幺半群范畴CMon（C）是常规的。因此，定理2.1给出了Mf在T上的一个分配律。特别地，设C为集合，这就导出了任意交换单子T上有限多集的单子Mf的典范分配律。这个例子显然是扩展的，从C中交换幺半群的范畴CMon（C）推广到C中任何对称操作数的模型范畴我们将不在此进一步阐述这一点，但我们打算在今后的工作中这样做。对于单子分配律的一类非例子，但本着与例2.3相同的精神，且其结构我们将在后面详细讨论，考虑以下内容。不M. Hyland等人/理论计算机科学电子笔记161（2006）4347例2.4设C是一个有限积范畴，T是其上的一个交换幺半群。试图将例2.3限制为C中幂等交换幺半群（半格）范畴ICMon（C），失败了：例2.3中描述的提升将一个幂等交换幺半群发送到一个不必是幂等的交换幺半群。对于与本文相关的特定示例，设C为Set，T=P为通常的幂集单子。 现在，从实施例2.3得出的结果如下。如果（A，·）是交换幺半群，则P（A）继承了X·Y ={a·b |a ∈ X，b ∈ Y}。但对于A幂等元，P（A）一般不是幂等元（乘法）.幂等交换的单子幺半群是Pf，即有限幂集单子，我们看到例2.3的分配律不能商给出单子Pf在单子P上的分配律。(It是直接检查起重故障的例行程序）。从[21]中的思想可以得出，人们可以将定理2.1和其中的定义推广到在温和的公理条件下发生在2-范畴内不是有一个范畴C，而是有一个2-范畴的对象;对于函子和自然变换也是如此;人们可以很容易地将范畴S-Alg的构造推广到具有某些有限2-范畴极限的2-范畴内的构造。下一节的工作，我们研究Kleisli构造Kl（S）而不是S-Alg，也可以在Street的设置中完成3分配律与Kleisli扩张给定一个范畴C上的单子（T，η，μ），我们用Kl（T）表示（T，η，μ）的Kleisli范畴，用J：C−→Kl（T）表示从C到Kl（T注意函子J不需要是忠实的，所以不需要一种包容性。然而，它通常是一种夹杂物，并且通常对人体无害。就这么想吧事实上，函子J是忠实的当且仅当η是逐点单态。定义3.1给定范畴C上的一个单子（T，η，μ）和范畴C上的一个闭函子H，C是H在Kl（T）上的一种扩张，它是H在Kl（T）上的一种有趣的扩张，使得H∈J=JH.注意，在定义中，我们要求函子相等，而不仅仅是同构。这不仅便于避免相干条件，而且对于提供精确和合理的结果也是必要定义3.2范畴C上单子T上的内函子H的分配律是自然变换λ：HTλ服从于明显的两个图的交换性，这两个图表示关于T的单位和乘法的一致性。命题3.3给出单子T上闭函子H等价于给出H到Kl（T）的扩张。48M. Hyland等人/理论计算机科学电子笔记161（2006）43证据 从一个分配律到一个推广是很 平常的事。而且，一个人的生活到由C中的idTX给出的从TX到X的K1（T）中的映射，也就是说，对典型的附加物的计数，产生一个分配律。验证这两种构造是相互逆的是常规的。Q给定一个分配律λ：HTλTH，我们将诱导扩张表示为：Hλ第二项的组成。1，Example2。3和Proposin3。3分钟为我们提供了一类扩展的例子。例3.4设C是上完全对称monoidal闭范畴，T是C上的交换monad。如例2.3所述，T提升到C中交换幺半群范畴CMon（C）上的一个单子。通过定理2.1，这种提升产生了T上交换幺半群的单子Mf的一个典范分配律。更进一步，这是Mf作为闭函子在T上的一个分配律.因此，应用命题3.3得到函子Mf到Kl（T）的典范扩张例3.5设C为集合，P为幂集单子，例3.4的分配律意味着给出了P上的有限幂集函子Pf的分配律，从而给出了Pf到Rel的推广，即，到Kl（P）。这个结果似乎不适用于任意交换单子T代替P。分布式law将P（X）的有限子集A发送到PfX的子集Y，该子集Y由X的有限子集B确定，对于这些子集B，b∈Ba∈A.b∈a和a∈Ax∈a.x∈B。简单地说，一个闭函子H到Kl（T）的扩张会导致复合HH到Kl（T）的扩张：需要注意的是，H到Kl（T）的扩张可能不止一个。证明一个分布律λ：HTλTH导出HH在T上的分配律，由下式给出：HHTHλ）HT HλH）T H我们用λ2表示。 证明下面的结果很简单。命题3.6给定单子T上的闭函子H的分配律λ，H<$λ2的扩张等于H <$λH<$λ的共点。我们将内函子的扩张的概念推广到Kl（T），并将分配律的等价性推广到内函子之间的自然变换的情形，如下所示。定义3.7给定范畴C上的单子T，给定范畴C上的闭函子H和K，将H和K的H和K表示为Kl（T），并给定一个最小值α：H∈K，α对Kl（T）的一种扩展是一种新的形式，即α∈：H∈满足α∈J=Jα.⇒K˜一个新的结构函数的所有元素都是唯一的元素：结构函数的数据由J：C−→Kl（T）是对象上的恒等式这一事实决定，因此唯一我们的做法是，我们的数据基本上符合H.R.P.的要求和K. OBSERVETATM. Hyland等人/理论计算机科学电子笔记161（2006）4349Kl（T），而它的扩展实际上依赖于一个预先存在的扩展选择，H和K到Kl（T），其中可能有许多。定义3.8给定范畴C上的内函子H和K，C上的自然变换α：H<$K和单子T，以及给定分配律λH：HT<$TH和λK：KT<$TK，如果图HTλH）THαT TαV VKT） TKλK上下班命题3.9给定分配律λ H：HT<$TH和λ K：KT <$TK，以及自然变换α：H <$K，自然变换α在T上分布当且仅当存在α到Kl（T）的扩张（必然唯一）。证明是例行公事。我们可以把上述命题结合起来，得到几个结果的简单证明。我们并不详细说明在单子上的每一个点端点函子、共端点内函子、单子和共单子的分配律的定义：这四个定义是上述定义和命题的常规结果（关于涉及共单子的情况，见[16]但是，写下我们主要感兴趣的结果，从上面的分析中得出，我们有以下几点定义3.10给定范畴C上的单子（S，η，μ）和T，S到Kl（T）的扩张是amonad（S，η，μ）到Kl（T），使得S，η，μ分别xt endS，η和dμ。定理3.11给定范畴C上的单子S和T，给出S在T上的分配律等价于给出单子S到Kl（T）的扩张。这使我们能够立即开发例3.4。例3.12设C是一个上完全对称monoidal闭范畴，T是C上的一个交换monad。则C中交换幺半群的单子Mf扩张到Kl（T）.例3.13借助于定理2.1和例2.4，例3.12并没有导出单子Pf从Set到Rel的扩张：后者是Kl（P），我们知道Mfqua monad在P上的分配律并不商于Pf在P上的分配律，因为否则P到CMon（C）的提升将限于ICMon（C），如例2.4所讨论的。然而，通过例3.5，存在Pf作为闭函子在P上的分配律。此外，验证由Pf的乘法所给出的自然变换也分布在P上也是常规的。因此函子Pf及其乘法自然变换推广到Rel.50M. Hyland等人/理论计算机科学电子笔记161（2006）43我们在这一节的发展很容易扩展到2-范畴和伪单子的情况。这里需要更多的注意，因为连贯性是--我们将在以后的工作中回到二维情况，因为它与Winskel及其同事在并发域理论上的工作相一致，其中Set被Cat取代，幂集单子被预层构造取代，预层构造在任何方面都是伪单子，除了大小，交换幺半群被对称幺半群范畴取代[4]。交换单子的概念一般化为伪交换2-单子的概念，并且我们对交换单子及其与交换幺半群的关系的公理化发展扩展到伪交换2-单子和对称幺半群范畴[12]。有关伪分配律的定义和构造的细节将在[22]中出现，但也可参见[5]的大纲。4对称么半群的伴随与交换么半群到目前为止，我们的注意力集中在对称幺半群闭范畴C上的交换单子T上，我们考虑了C上交换幺半群的单子Mf与T之间的关系，等价地说，Mf到Kl（T）的扩张。后者是关于Mf的单子结构的一个陈述。在本节中，我们将讨论更具体地涉及Mf的交换幺半群结构的问题：但以下内容仍然适用于更一般的对称运算。Mf的交换幺半群结构更直接地涉及到C的对称幺半群结构，以及C和Kl（T）中的交换幺半群的概念。我们从[7]中回顾一些基本的定义。给定对称monoidal范畴C和D，从A到B的对称monoidal函子是函子H：A−→B以及具有分量HX <$HY的自然变换 −→H（X<$Y）和I−→HI服从四个相干性的结合性，左和右单位，和对称同构的效果的条件。一个对称幺半群函子称为强函子，如果其结构自然变换是可逆的。对称monoidal函子H和K之间的对称monoidal自然变换是一个自然变换，形成α：HK，它尊重对称结构的其余部分，monoidal函子小的对称monoidal范畴、对称monoidal函数和对称monoidal自然变换构成2-范畴SymMon。对称么半群的附加是2-范畴SymMon中的附加。下面的结果很容易证明，并且隐含在[7]中。定理4.1从A到B的每一个对称幺半群的加法提升为从CMon（A）到CMon（B）的一个加法.这就是我们需要的结果，条件是我们可以得到基范畴C与C上交换单子的Kl（T）之间的对称幺半群伴随。M. Hyland等人/理论计算机科学电子笔记161（2006）4351事实上，我们可以通过下面的论证来做到这一点。下面的结果不是它的最一般形式（见[3]），而是我们在这里需要的形式[13]。定理4.2给定对称monoidal范畴A和B，并给定一个普通的伴随FEG：A-→B，将该伴随推广到对称monoidal范畴的伴随等价于在普通函子F：B-→ A上给出一个强对称monoidal结构。我们可以把对称monoidal算子的特征与[19]中的下列结果结合起来。定理4.3给定一个对称monoidal范畴C和其上的monad T，给出T的交换强度等价于给出K1（T）上的一个对称monoidal结构，使得Kleisli伴随是一个对称monoidal伴随。这对我们的意义在于，给定一个上完全对称monoidal闭范畴C上的交换单子T，它给出了Mf到范畴Kl（T）的扩展M f的特征。推论4.4对任何上完备的对称么半群闭范畴C和对一个在C上的任意可换么半群T，Mf的外项Mf是在对称么半群范畴Kl（T）中的自由可换么半群。证据通过定理4.2和定理4.3，Kleisli附加正则地扩张为C和K1（T）之间的对称么半群附加.通过定理4.1，该附加提升到CMon（C）和CMon（Kl（T））之间的附加。特别是，分类CMon（KI（T）CMon（C）VVKl（T））C交换，带有明显的函子标签。合数的左伴随是JMf=M.J，以及系统中所有未执行的操作的集合从Kl（T）到CMn（Kl（T））。SoMfmustatheecmutivemonodinKl（T）.Q这里我们有一个最终的公理化结果在某些具有有限积和有限余积的范畴中，特别是Set，单子Mf具有这样的性质：Mf（X+Y）−→MfX×MfY总是同构的。对于那些范畴C，如果这是真的，我们寻求的是一个符合条件的，给定一个条件T，它的作用是Mf，通过我们知道它的自同构性和来自Mf（X+Y）的自同构性，52M. Hyland等人/理论计算机科学电子笔记161（2006）43对于M∈X∈M∈Y，利用K∈ I（T）的可压缩性和定理4.3导出的K∈I（T）上的对称幺半群结构. 唯一的问题是关于Kl（T）的比较图的自然性命题4.5对余完备carbohydrate闭集C上的任意交换单子T，M的交换单子T在Kl（T）中的交换单子是Kl（T）的对称单子结构，如果图Mf（TX+TY））MfTX×MfTY）TMfX×TMfYV VMfT（X+Y））TMf（X+Y））T（M fX × M fY）所有的地图都是由标准选择给出的，通勤。显然，这一结果延伸到Mf以外的任何对称运算和一些非运算单子，如阿贝尔群。为了分析无类型λ-演算的恩格尔风格模型，我们将在下一节中，我们要找到公理化条件，在这些条件下，对于一个共同体和T n S et i s的范畴Kl（Mf）op可以是封闭的：我们现在没有一个有限的概念，因为Kl（Mf）有一个有限的概念。在这两个问题上，一个问题是在Kl（Mf）op中有一个简单的预处理过程，即：在Kl（M_f）中的一个双线性映射，可以看作是在Kl（T）中的一个映射，但从这一点来看，目前，我们看不出如何在不使用自对偶性和封闭性，其中T是P，因此Kl（T）是Rel。然而，我们可以以一种非平凡的方式推广到2-范畴：小范畴和原函子的双范畴Prof在我们这里使用的意义上并不完全是自对偶的，但它有足够的自对偶结构，允许我们模仿我们的论证。5Engeler模型在本节中，我们最终将前面几节的公理化发展与恩格尔的构造联系起来我们首先考虑有限多重集给出的变体，因为它提供了无类型λ-演算的更简单和更优雅的范畴理论模型。然后我们继续讨论恩格尔最初考虑的Pf。这涉及到更复杂的范畴理论，但也使我们能够对这种关系作出更精确的陈述。下面这个简单的结果多年来一直是线性逻辑语义学的基础[2]。定理5.1设C是一个具有有限积的对称monoidal闭范畴，G是C上的一个把有限积送到对称monoidal结构的余单子。 则Kleisli范畴K1（G）是Carnes-closed的，其指数由C中的线性指数[GX，Y]给出.M. Hyland等人/理论计算机科学电子笔记161（2006）4353例5.2范畴Rel是对称monoidal闭的，实际上是紧闭的，具有由集合的乘积给出的对称monoidal结构，并且它具有由集合的余积给出的乘积和余积。此外，它是自对偶的，最不寻常的是，线性指数由集合的乘积给出我们从前面的章节中知道Mf扩张到Rel上的单子，因此等价地扩张到Rel上的余单子，并且扩张将余积发送给张量。如果我们如果Mf不考虑M f的计算结果，则它满足Kl（Mf），公式如下Kl（Mf）op，它可以被关闭。闭合的结构由MfX×Y给出。例5.2给出了一个carbohydrate闭范畴。 给一个反射物体给出一个集合D，并给出数据，使MfD×D表示为D在Kl（M_f）中的一个集合。所有功能都提供了备份功能，这些功能是一个通用的组件，用于备份S et to Kl（Metf）。 因此，在设置中允许任何回缩，即，任何集合D连同M fD×D到D中的包含，都可将该包含的一个应用归结为Kl（Mf）的一个可积性。ONECAN通过求解显域得到满足D所需条件的集合方程因此，用Mf代替Pf给出的Engeler模型的变体可以看作是在封闭类别Kl（Mf）中的严格对象。现在我们通过用有限子集代替有限多集来精确地考虑恩格尔原则上，我们希望在我们的发展中尽可能合理地保持公理化但是，如例3.13所讨论的，单子Pf到Rel的自然扩张不满足Rel上单子的公理，因此不产生Rel上单子的Kleisli范畴。这使我们放松范畴的定义，考虑半范畴：半范畴由一个范畴的数据组成，除了存在恒等映射，唯一的公理是组合是结合的。半函子是保持复合的图态射，例如参见[11]。我们并不断言下面的定义是有定义的，但它便于我们表达本节的结果。定义5.3范畴C上的近单子由C上的内函子S，满足结合性条件的自然变换μ：S2<$S组成S3μS）S2Sμ μVVS2）Sμ和一个ObC-指标映射族ηX：X−→SX，使得下列dia-54M. Hyland等人/理论计算机科学电子笔记161（2006）43克通勤：SXSηX）S2XSXηSX）S2XμX μXV VSX SX例5.4我们的主要例子是通过在闭函子Pf的集合上的Rel=Kl（P）的推广和例3.13中的乘法自然变换给出的，同时给出了Pf的单位的数据。定义5.5设S是C上的近单子。用Kl（S）表示其对象是C的对象的半范畴，其中母集Kl（S）（X，Y）被定义为C（X，SY），复合被定义为Xf）SYSg）S2Z μZ ）SZ构造Kl（S）被限制为Kleisli构造的推广：观察到从C到Kl（S）的正则图态射甚至不需要满足半函子的公理，因为它不需要保持合成。因此，为了取得任何公理化的进展，我们需要做如下的辅助构造。定义5.6给定C上的一个近单子S，用Cη表示C的子范畴具有与C相同的对象，C的映射f：X−→Y位于Cη中，如果图X（f）YηXηYV VSX） SYSF上下班定义5.7给定C上的一个近单子S，用Kl（S）η表示由Kl（S）的所有对象连同那些映射f确定的Kl（S）的子半代数：X−→Y，对于X − →Y，下图中的Kl（S）是可交换的：X（f）YˆηXη YvX） YFM. Hyland等人/理论计算机科学电子笔记161（2006）4355上述两个定义之间的关键区别在于右手垂直箭头的方向：在前一个定义中，它指向下，而在后者中，它指向上。在前者中，箭头只能指向下，因为没有向上的自然箭头.但在后者中，箭头的方向正好是使Kl（S）η成为由Kl（S）中的幂等元（X，ηX）确定的Kl（S幂等分裂是半范畴Kl（S）上的余自由范畴。注意，映射ηX不一定在范畴Cη中：它们不形成自然变换，因此没有理由相信它们相对于自身是自然的。但它们确实存在于Kl（S）η中，在那里它们充当恒等映射。它们确实存在于C中，这使得我们可以证明下面的结果。命题5.8给定C上的一个近单子S，C到Kl（S）限制于函子J：C η−→ Kl（S）η。我们可以把这个命题扩展到处理C中的余积：在我们的主要例子类中，C是Kl（T）的形式，如果基范畴有余积，则它总是有余积，我们试图在Kl（T）上做一个进一步的类Kleisli构造，它是函子的，因此保持收缩，并保持余积：后者在存在自对偶的情况下成为积。事实上，副产品的保存是常规的。命题5.9假设C有有限个余积。设S是C上的近单子，其余投影Xi −→ X0+ X1位于C η中。 则C η有且J：C η−→Kl（S）η保持有限余积。因此，Kl（S）η有有限个余积。从这一点来看，公理化的发展似乎是被迫的。因此，我们将仅限于我们主要感兴趣的特定示例，其中C是Rel，S由下式给出：P_（？），他在格勒顿，映射X−→PfX。由Proposition5. 9，范畴Kl（P∈f）η有一个严格的正则函子，并且η在Set上是自然的，利用Rel的自对偶性，我们有一个正则函子，Setin o Kl（P）op. 后面的类别不需要关闭，fη但是，如在[9]中，它的幂等分裂是，集合X和Y的指数YX通过分裂PfX×Y上的一个明显幂等给出，完全类似于例5.2中有限多集的情况。因此，类似于例5.2，但更进一步，任何具有PfD×D的集合D被表示为D的子集，产生使D成为carbohydrate闭范畴的自反对象的结构通过Kl（P）op的iidement-splittingg来确定：对于六个元素DDisafηPfD×D的收缩核，它又是D的收缩核。同样，与有限多重集的情况一样，为了获得特定的自相关对象D，只需在Set中求解域方程D=A+PfD×D，适用于表格A/=0。该算法是一个简单的表格，Pf（D）上的二元运算由关系RfromPf（D）×Pf（D）给出。D定义如下：（u，v）Rb如果（u={（u1，b），···，（un，b）}）<$（v=iui）。56M. Hyland等人/理论计算机科学电子笔记161（2006）43这在任何具有余域D的homset上生成了一个集合论λ模型，并且考虑到0到D的hom，正好产生了Engeler通过结论，我们说一些关于我们的观点之间的联系恩格尔的模型和目前的文献。（Plotkin [18]从这个领域理论的角度对构式进行了很好的考察。）最简单的故事从半函子理论开始（Hayashi [9]）。如Hoofman [10]所示（但也可参见[11]），该理论允许使用与有限子集相关联的完全不同的结构来构造幂集和连续映射的范畴POWHoofman观察到Engeler对我们Engeler的模型位于K l（P n）op中。这是一个很好的例子，fη一个域的类别;特别是它没有足够的点。我们希望因此，强调Engeler的模型适用于独立于历史的组合原因。如何将POW称为KI（POW）操作的一种方法，fη是点上的双射通过这种方式，人们可以恢复域理论的观点。最后，我们解释一下我们在此提出的工作计划。过滤器lambda模型由都灵学派引入（例如，参见[6]）通常被 当然，它们是lambda模型，因为它们似乎来自具有足够点的类别。但我们对恩格尔模型的分析是，它自然产生于一个没有足够点数的范畴。因此，在我们的公式中，它自然是一个既定术语中的lambda代数。现在，恩格尔模型被认为是一般滤波器模型家族的一部分。因此，这就提出了（至少对我们来说）以下几个问题。哪些过滤器模型真正是域模型（毕竟没有人怀疑斯科特 似乎有很多更多地了解lambda演算模型的具体构造（也就是一般的lambda代数）。引用[1] M. Barr和C. Wells，Toposes，Triples，and Theories，Grundlehren der math. Wissenschaften 278，Springer-Verlag，1985。[2] N.本顿湾Bierman，V. de Paiva，and M.李文，线性λ-演算与范畴模型，计算机科学与逻辑学报，1992，计算机科学讲义，第702期，第61[3] R. Blackwell，G.M.陈文辉，二维单子理论，国立台湾大学数学研究所硕士论文，（1989）[4] Gian Luca Cattani和G. Winskel，Profunctors，Open Maps and Bisimulation，Mathematical Structuresin Computer Science（即将出版）。[5] E. Cheng，M.中国植物志刘文，“非线性分布的理论与应用”，国立台湾大学计算机科学研究所硕士论文，2003年。[6] M. Coppo，F. Honsell，M. Dezani-Ciancaglini和G. Longo，Extended type structures and filter lambdamodels，Logic Colloquium[7] S. Eilenberg和G.M. Kelly，Closed Categories，Proc. Conference on Categorical Algebra La Jolla 1965，（1966）421M. Hyland等人/理论计算机科学电子笔记161（2006）4357[8] E. Engeler，Algebras and Combinators，Algebra Universalis 13（1981）389[9] S. Hayashi，半函子的伴随：非延拓λ-演算中的范畴结构，理论计算机科学41（1985）95[10] R. Hoofman，半函子理论，计算机科学中的数学结构3（1993）93-128。[11]R. 霍 夫 曼 和 我 Moerdijk ， A Remark on the Theory of Semi-Functors ， Mathematical Structures inComputer Science 5（1995）1[12] M. Hyland和A. J. Power，伪交换Monads和伪闭2-范畴，J. Pure Appl. Algebra 175（2002）141[13] 通 用 汽 车 Kelly ， Doctrinal Adjunction ， Category Seminar Sydney 1972/73 ， Lecture Notes inMathematics 420，Springer-Verlag，1974，257[14] 通用汽车Kelly，A Unified Treatment of Trans finite Constructions for Free Algebras，Free Monoid，Colimits，Associated Sheave，and so on，Bull. Austral. Math. Soc. 22（1980）1[15] A. Kock，由交换单子生成的闭范畴，J. Austral. Math. Soc. 12（1971）405- 424。[16] M. Lenisa，A.J. Power，and H.孙文，“点内函子与共点内函子的分布性”，中国科学院学报，2000年，第33卷，2000年。[17] G. Longo，λ-演算的集合理论模型：理论，扩展，同构。Pure Appl. Logic 24（1983）153[18] G.D. Plotkin ， Set-Theoretical and Other Elementary Models of theλ ， -Calculus ， TheoreticalComputer Science 121（1993）351[19] A.J. Power 和 E.Robinson ， Premonoidal Categories and Notions of Computation ， Proc.LDPL1996，Mathematical Structures in Computer Science 7（1997）453[20] D.S. Scott，Relating Theories of theλ-Calculus，To H. B. Curry：Essays in Combinatory Logic，λ-Calculus and Formalism，Academic Press，1980，403[21] R. Street，Monads的形式理论，J. Pure Appl. Algebra 2（1972）149[22] M.田中，伪分布律和变量绑定的统一框架。爱丁堡博士论文（提交）。