lambda演算中的Λ-幺半群：分析与抽象克隆

可在www.sciencedirect.com在线获取理论计算机科学电子笔记303（2014）59-77www.elsevier.com/locate/entcs关于Lambda幺半群的一个概念Martin Hyland马丁·海兰1，2剑桥大学纯数学与数理统计系英国剑桥摘要lambda演算的任何解释都确定了一个复合幺半群，这个幺半群可以被赋予一个结构，从这个结构中可以恢复解释。 这就是Dana Scott关于lambda演算的收缩范畴的解释的本质。本文提出了一种新的方法，所需的结构上的幺半群来自最近的分析lambda演算的代数理论。关键词：代数理论，抽象克隆，λ-演算，反应对象，Λ-幺半群。1介绍我们把lambda演算的解释可以用carlavian封闭范畴中的自相关对象来理解这一见解归功于达纳·这个想法在他身边的圈子里得到了很好的认可，最终在他为CurryFestschrift撰写的论文中得到了概述。斯科特这促使其他人（Karst Koymans在[7]和Jim Lambek和Phil Scott在[8]）分析什么是复合幺半群上的结构，它确保了收缩范畴是carnival闭的。他们得出的答案可能非常接近，尽管从文献中可以找到的结果来看，这一点并不明显。在本文中，我概述了一种不同的方法。Lambek和Scott [8]专注于C-幺半群的一个非常强的概念：它对应于有一个（也许应该说）carte的非平凡对象U1我感谢约翰·鲍尔在巴斯组织了代数、余代数和拓扑研讨会，他是威塞克斯理论研讨会的主席，并鼓励他写一篇论文。我感谢德累斯顿工业大学的Mike Behrsich、Sebastian Kerkho和Martin Schneider在毕业典礼和毕业典礼后对抽象克隆的建议和讨论了那次会议2电子邮件：M. dpmms.cam.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2014.02.0041571-0661/© 2014 Elsevier B. V.保留所有权利。60M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59具有s-限制同构U× U=U=U U的s-闭范畴。由于存在这种情况，Lambek和Scott利用了Dana Scott对该问题的一种优雅的分类(In我顺便说一下，[8]中的知识史是误导性的。Dana Scott在保罗·泰勒的论文[ 11 ]的2.5.11中描述的直接域理论结构我仍然认为它有独立的利益。）Lambek和Scott这接近于Koymans在他的详细分析[7]中所称的carnival闭幺半群。科伊曼斯意识到，幺半群与结构和λ演算的解释之间的联系并不简单，[7]的大部分内容都是为了将其联系起来。在加紧联系，他来到他的最终概念，他所谓的λ幺半群或λ-幺半群。HLambek和Scott以及Koy- mans的方法的想法非常粗略地是编码什么将是产品，然后给出一个适当相关的lambda抽象操作。有一组方程，其意义也许并不完全清楚。在本文中，我提出了一种新的方法，避免明确的治疗lambda抽象，但类似的产品编码仍然存在。乘积的编码的选择甚至对C-幺半群的情况也提出了问题：这个问题在[8]的练习中得到了处理。Koymans在[7]中进一步讨论了这个问题他的分析似乎没有得到广泛的重视。在本文中，我提出了一个新的结构上的组成单子。我希望通过它使科伊曼斯所处理的考虑更加透明。为了束缚他的λ-幺半群的概念，柯伊曼斯不得不写下许多方程。在提出另一种方法时，我并不想减少方程的数量：我肯定会有更多的方程。相反，我在寻求一个公式，它的意义在一般意义上是显而易见的，并且特别地使我所谓的λ演算基本定理有意义。我在最近的一篇论文[5]中解释了这一点。在那里我提出了一个阅读的解释λ演算作为代数理论的结构。打破了既定的用法，我把这些称为λ理论。更标准的解释思想，如[2]中的λ-代数的旧概念，是相当技术性的。在我的设定中，它对应于初始λ-理论Λ的更表层更易理解的代数概念，即对应于一个Λ-代数。[5]中的关键论点从Λ-代数传递到相应的幺半群，然后传递到该幺半群上的预层范畴。预层范畴配备了一个反射对象，为了建立基本定理，人们需要一些详细的信息。在[5]中，所有需要的计算都是直接在lambda演算中完成的：我没有空间来开发对幺半群的更抽象的处理本文从文[5]的观点出发，说明幺半群的本质结构是什么。我并不试图提出一个定义性的Λ幺半群概念我会M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）5961相反，这样做的同时，使一个严重的遗漏，从[5]，即与组合逻辑的联系。这可能不会立即显而易见，但实际上Λ-幺半群的结构与组合子的代数理解密切相关，并且Koymans发现的问题在那里得到了反映。正如我希望在另一个场合表明，所有这一切都可以理解的角度来看，代数理论和一种方法的结构上的幺半群自然产生的角度抽象克隆[12]。在本文中，我仅限于解释这一观点，并根据这一观点对[7]中的分析给出一些提示。2代数理论根据[5]中给出的说明，λ-演算的解释是λ-理论，也就是说，通过定义，一个具有附加结构的代数理论。对于这篇论文来说，通过回顾代数理论的三个概念，似乎值得把它放在上下文中。我从一个定义开始，它包含了在[6]中解释的一般观点，即各种代数理论是由某些Kleisli双范畴[3]中的单子给出的然后，我将对这个定义进行一点分解，以达到一个更熟悉的表述，最后，我将澄清与抽象克隆概念的联系。这种材料基本上是民俗在习惯意义上，它是相当明显的，虽然没有明确讨论的文献。在这里给出一个账户的原因是这样的。λ-理论的概念是用代数理论的范畴概念来表达的。另一方面，我想概述的Λ-幺半群的概念最好理解为来自一个代数理论的片段，后者最好被认为是一个抽象的克隆。2.1笛卡尔运算我首先给出一个与运算或对称运算完全平行的代数理论的定义。与操作的定义一样，有很多结构需要布局。当然，这是一个支持[6]的抽象方法的论点写集合为集合范畴，写F为有限集合范畴的标准骨架，如果你愿意，它的对象是有限基数。运算方法主要关注函子F2→F;（n，m）<$→n+m在这种特殊情况下是副产物。运算符方法是符号沉重，它是以及设置它的一些提前我们需要一些表示多重余积的符号。的序列m=（m1，···，mn）对于F的对象，设m=m1+···+mn62M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59是F的一个对象的和。同样对于一个序列g=（g1：m1→p1，···，gn：mn→pn）F中的映射，设g：是由+的函性产生的明显映射我们还需要一些符号来处理重新索引。 假设我们有p=（p1，···pm）F的m元对象序列和F中的映射f：n→m。然后我们得到诱导的n元序列f∈p =（pf（1），···pf（n））.+是余积的事实给出了一个明显的诱导映射f：f p → p。现在来定义一个代数理论。我担心在此过程中会引入更多的符号。定义2.1（运算式）一个carbohydrate operadT由以下数据给出：• 一个函子T：F →Sets;• 选择单位元id∈T（1）;• 对于每个n和m1，···mn是一个合成映射，T（n）×（T（m1）×···×T（mn））−→ T（m1+···+mn），记作（f，g1，···，gn）<$→f[g1，···，gn].这些数据需要满足一定的单位律和结合律以及自然性条件。• 单位定律是简单的方程id [t] = t;t[id，···，id]。• 要给出结合律，还需要进一步的符号。设m=（m1，···mn）为F的对象序列T（m）= T（m1）×· · ·×T（mn）。注意，composition现在可以写成T（n）×T（m）−→ T（m）。M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）5963ˆ我我我我我假 设 我 们 有 一 个 对 象 n ， 一 个 对 象 序 列 m = （ m1 ， ··· ， mn ） ， 对 于each1≤i≤n，一个序列pi=（pi1，· · ·，pimi）。有一个明显的nt平行组成T（m）×T（pi）−→（T（mi）×T（pi））−→T（α p i）。这涉及到一些明显的重新排序，我没有详细说明。比如说，这些pipi本身形成一个和为pipi（pipi）的序列。那么结合律就是要求图T（n）×T（m）×T（p i））T（m）×T（p i）VVT（n）× T（pi））T（ipi）我上下班 在这里，上面介绍的平行组合出现在左边。结合性的结果是，t[s1[r11，···，r1m1]，···，sn[rn1，···，rnmn]]是明确的。• 第一个和直接的自然条件是这样的。假设我们有一个对象n，映射g1：m1→p1，.，gn：mn→pn.然后，T（n）×T（m））T（m）T（n）×T（g）vT（微克）vT（n）×T（p））T（P）上下班上面解释了符号T（g），并且T（g）的含义与上面的T（m）• 第二个自然条件稍微复杂一些 假设我们有一个映射f：n→m和一个对象序列p= p1，···pm。乘积的基本性质给出了一个明显的映射T（p）→T（f<$p）.自然性条件也包括在定义之前引入的符号f。这张图T（n）×T（p））T（n）×T（f<$p））T（f<$p）T（f）×T（p）vTfvT（m）×T（p））T（p）64M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59上下班这就结束了操作定义。这是线性逻辑的精神。基本操作是线性的，在这个意义上，没有弱化或重复，但这些结构规则是在函数性F→集内处理的。2.2代数理论假设我们有一个carbohydrate operadT。我们可以得到一些进一步的结构如下。首先，对于对象n∈F的n个点k：1→n中的每一个，我们有一个元素prk=kid∈T（n），即单位元id∈T（1）的像。其次，对于每个n和m，我们可以定义一个同时复合，其中变量T（n）×T（m）n→T（m）对应于传统的替代概念：我们有一个明显的投影映射snd：n×m→m，我们可以取复合T（n）× T（m）n）T（n×m）snd）T（m）.这就引出了一个更为熟悉的公式，我希望它能被视为典范。定义2.2（范畴论版本）代数理论T由以下数据给出：• 一个函子T：F →Sets;• 对每个n∈F，有投影pr1，···，prn∈T（n）;• 复合映射T（n）×T（m）n→T（m）;（f，g1，···，gn）→f（g1，···，gn）.这些数据需要满足以下法律。• 单位定律恒等式id=pr1∈T（1）是T（1）中的特殊投影，其他投影定义为prk=kid∈ T（n）。恒等式充当恒等式，因为id（f）=f;此外，在另一边f（pr1，···，prn）=f上，与合成投影存在相容性。• 结合律对于所有的n，m和p，T（n）×T（m）n×T（p）m）T（m）×T（p）mV VT（n）×（T（m）×T（p）m）n）T（n）×T（p）n ）T（p），上下班，其中左手箭头是明显的重复论点。• 合成T（n）×T（m）n→T（m）在m和n中是自然的，M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）5965对于h：m→p和f：n→k，T（n）×T（m）n）T（m）T（n）×T（m）k）T（n）×T（m）nv vvvT（n）×T（p）n）T（p）T（k）×T（m）k）T（m）通勤。（有时右手边的图被称为非凡的自然。）这就结束了我对代数理论的范畴论定义。很容易看出，有了上面概述的定义，每一个卡氏运算都产生一个代数理论。相反，给定一个代数理论T，人们可以用一种简单的方式恢复相应的卡氏运算。为了定义操作成分T（n）×（T（m1）×· ··T（mn））−→ T（m1+···+mn），设i：mi→mm为标准品进样到联产物中然后f[g1，···，g n]= f（in1 <$g1，···，inn<$g n）.这样就可以直接建立一个carniveroperad的公理，尽管可能有点乏味。代数理论的范畴论定义具有比运算定义更简洁的优点，同时保持了函数性的重要方面因此，我把它简单地称为代数理论。然而，如果我们把范畴论的观点放在一边，那么我们就可以用一个简单而基本的公式来做。2.3抽象克隆在刚才给出的代数论的范畴论定义中，有某种接近冗余的东西，值得更仔细地研究一下。假设f：n→m。使用组合来定义f∈：T（n）→T（m）; t <$→ t（prf（1），···，prf（n））.以t和pr1，···，prm为例，在非常自然图T（n）×T（m）m）T（m）×T（m）mV VT（n）×T（m）n ）T（m）66M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59n证明了T（f）（t）=f<$t，所以（希望是函子的）作用可以用复合来定义。现在，代数理论定义的一个稍微古怪的特征也许是，我们不要求投影在prk（c1，···，cn）=ck的意义上投影。但是假设我们有这个。则对于f：n→m和g：m→pg（ft）=t（prf（1），···，prf（n））（prg（1），···，prg（m））=t（prf（1）（prg（1），···，prg（m）），···，prf（n）（prg（1），···，prg（m）=t（prgf（1），···，prgf（n））=（gf）由于我们已经有了id=t（id）=t，我们得到了根据合成定义的动作的函性。有了这个定义，简单的自然性条件是微不足道的，而非凡的自然性则由一个与刚才给出的论证相平行的明显论证所遵循。为什么我们不需要这个预测项目？好吧，相反的方向，很容易看出，投影方程是从非常自然的。取平方T（1）×T（m）n）T（1）×T（m）V VT（n）×T（m）n）T（m）对于映射k：1→n。从T（1）×T（m）n中的id和（c1，···cn）开始。绕到顶部，我们首先得到id和ck，然后得到ck。另一方面，绕着底部走，我们首先得到k_id=pr_k和（c_1，···c_n），因此，prk（c1，···cn）.因此，prk（c1，···cn）=ck，投影确实起投影的作用。从这一讨论可以得出，我们可以给出代数理论概念的另一种更具体的表述，如下所示。定义2.3（通用代数版本）抽象克隆由以下数据给出。• 对于每个自然数n，一个集合T（n）。• 对于每个n，元素prk∈T（n），1≤k≤n.• 对于每个n和m，T（n）×T（m）→T（m）;（f，g1，···，gn）→ f（g1，···，gn）.这些数据需要满足以下方程。• 单位定律prk（a1，···，a n）= a k;a（pr1，···，prk）= a.M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）5967.- 是的Σ• 结合律ab1（c1，···cm），···，bn（c1，···cm）= a（b1，···，bn）（c1，···cm）.这是代数理论的一个基本的、直接的定义，其句法精神来自于泛代数。它通常与菲利普·霍尔有关。这种归因是合理的，但通常的参考文献实际上并不支持这种联系，我认为这是基于个人的知识。这个术语很可能是由于泰勒[12]。在泛代数中，人们经常在抽象克隆中省略显式常数T（0）。对于一般概念的克隆问题的零操作讨论了一份文件的迈克Behrisch。省略零元运算感觉像是一个疏忽，但奇怪的是，从Λ-代数导出的幺半群最好被看作是没有（显式）零元运算的抽象克隆的一个片段2.4关于等价性的我相信，我已经说得足够清楚了，代数理论概念的三种表述，如代数运算、代数理论和抽象克隆，是等价的。在每一个公式中，我们都有一个代数理论的映射F：S →T的自然直观的概念，它是由一个（自然）变换给出的，其中的分量Fn：S（n）→T（n）保持投影和合成。因此，在每种情况下，我们都得到一个代数理论范畴，而上面概述的平移给出了这些范畴之间的同构。3Lambda演算我将本文的其余部分置于上下文中，简要回顾了[5]中给出的λ-演算的语义方法。在那篇论文中，我尽可能地保留了传统术语，但我觉得在一个方面与传统分道扬镳是不可避免的。我建议把我对lambda演算的解释的基本语义概念称为lambda理论或λ-理论。这个术语的既定用法是用于纯λ-演算语言中的理论：这样的理论对应于我所赞成的意义上的初始λ-理论的商。我把这种改变变成一种更具包容性的意义，作为一种坚持改变观点的方式，远离过去主要是句法上的关注3.1Lambda理论与代数在[5]中，我提出了这样一种情况，即在λ演算的任何干净处理中需要显式地处理变量绑定，这意味着演算的基本语义分析应该根据代数理论。为了解释λ-演算，我提出λ-理论，这是一种具有进一步数据的代数理论。这就是定义。定义3.1λ-理论是一个具有半封闭结构的代数理论L。给一个代数理论L配备半闭结构就是给出68M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59Mma retractionL（n+1）aL（n），其中映射ρ：L（n）→ L（n+1）和λ：L（n+ 1）→ L（n）在n中是自然的，并且与作用相容L（m）× L（n）→L（n）和 L（m + 1）× L（n）→L（n +1）。语义学的传统方法[2]使用λ-代数的困难技术概念。在我的方法中，有一些更容易接近的东西，这正是与之相对应的。 如果L和M是λ-理论，则λ-理论的映射L →M是与收缩ρ和截面λ交换的代数理论的映射。这给出了一个λ-理论的范畴。λ-演算模β-等式的语法给出了这一范畴的初始对象Λ，初始λ-理论，它足够自然地导致下面的内容。定义3.2Λ-代数是初始λ-理论Λ的代数。这个定义比λ-代数的传统定义更简洁，因为它避免了对抽象的明确解释。然而，为了避免误解，我应该强调它并不实用：直接证明一个人有一个Λ-代数和证明一个人有一个λ-代数一样困难。而不是集中在代数应该考虑一般情况下，在以下方式。任何λ-理论L的初始代数L（0）都可以通过唯一映射Λ→ L而被看作是一个Λ-代数。在大多数情况下，通过找到λ-理论L并用L（0）确定假定的Λ-代数来找到Λ-我所推荐的观点可以用我称之为λ-演算的基本定理来解释。定理3.3（λ-演算的基本定理）λ-理论范畴与Λ-代数范畴之间存在等价性，其中λ-理论L对应于Λ-代数L（0）。在[5]中，我给出了这个定理的一个更精细的公式，但在这里我不想涉及它在本文的其余部分，我将概述那些依赖于诱导幺半群的证明部分，并将它们用一个临时的Λ-幺半群的新概念来表示。3.2动机我对Λ-幺半群的新概念的研究是出于清理[5]中λ演算基本定理的徒手证明的愿望。基本定理的实质是把λ-理论L的整体作为一个Λ-代数编码在L（0）中。也许对[5]中的证明的欣赏点是，沿着这条路，人们首先看到L的结构是如何编码在L（n）中的结构中的，对于其他小的n，特别是对于n等于1和2。我解释这是怎么回事。M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）596922我们所关心的[5]的主要论点如下。我们从Λ-代数A开始。我们最终将用λ-理论UA的初始代数UA（0）来标识A。对于从A导出的么半群 MA，我们从预层范畴PA=PMA中的泛对象U得到λ-理论UA。最终的识别将给出MA与λ-理论的幺半群UA（1）的主要的一点是，我们有关于幺半群MA的数据，它把U表示为预层范畴PA中的自反对象。[5]中的证明主要依赖于用一个预层来标识函数空间UU，该预层的底层子集MA最终将被标识为UA（2）。仔细观察就会发现，所有的数据实际上都被λ理论UA对F的两个对象1和2的截断所控制。3.3截短克隆让我们退后一步，考虑一下将代数理论T截断为对象1和对象2。我们想要的最好是在抽象的克隆公式中处理。所以我们有两个集合T（1）和T（2）。我们有恒等式I∈T（1）和第一和第二投影T，F∈ T（2），其中为了简单起见，我已经使用了来自λ-演算的符号。最后我们有四个组成部分T（1）×T（1）−→T（1）;T（1）×T（2）−→ T（2）;T（2）×T（1）−→ T（1）：T（2）×T（2）−→ T（2）。所有这些数据都将满足这个有限数据集合的单位和结合律的抽象克隆版本。我希望指出这些是什么习惯语法会有所帮助。单位定律有两种。我们有左规则I（a（x））=a（x）I（c（x，y））=c（x，y）T（a（x），b（x））=a（x）T（c（x，y），d（x，y））=c（x，y）F（a（x），b（x））=b（x）F（c（x，y），d（x，y））=d（x，y）和正确的规则a（I（x）= a（x） c（T（x，y），F（x，y））= c（x，y）.结合律在某种意义上被吸收到句法中。有四个这样的，这非常简单地意味着，a（b（c（x），a（b（c（x），d（x）），a（b（c（x，y）），a（b（c（x，y），d（x，y）是明确的。其中有四个是关于a（b（d（x）），c（d（x），a（b（d（x，y）），c（d（x，y），a（b（d（x），e（x）），c（d（x），e（x），a（b（d（x，y），e（x，y）），c（d（x，y），e（x，y）其中有重复的子项，关键是这些子项可能是由重复变量的项替换而产生的。我希望这完全70M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59直观的，但如果不是，它可能有助于看到所有这些方程改写为编码形式的Λ-幺半群。我在第3.5节的结尾提出了这一点。3.4λ理论的截断现在考虑将λ-理论L截断为对象1和2。然后，我们自然会得到上面的数据，但也有一些额外的功能是显而易见的。首先通过λ理论的定义，我们将得到一个收缩L（2）aL（1）。 此外，这种收缩的图像被确定为幺半群L（1）的子集。 如果我们将L（1）上的基本复合记为λ，将λ项的关键解释记为1，λx，y.xy则我们可以将图像识别为{a∈ L（1）|1a = a}。这有一些简单的后果。首先，显然我们可以把T和F看作是L（2）的元素，从而也是L（1）的元素。其次，通过按需要与收缩复合，我们可以将上述所有复合视为对所有L（1）的适当元的运算。结果，单位定律得到了一点点修改，但结合律仍然保持不变。到目前为止，我们看到，对于λ-理论L，它的截断可以编码为幺半群L（1）。λ-理论给出了更多，一个特殊的方程，它反映了λ-演算处理多变量函数的方式，以及一些额外的数据（在弱意义上）编码产品。为了准备定义，我在这里给出额外的数据。在句法形式中，我们将有p，q∈ L（1）和m∈ L（2），使得方程p（m（x，y））=x=T（x，y）q（m（x，y））=y=F（x，y）稍等从某种意义上说，这可以用来束缚λ理论L，尽管我在本文中不会给出全部的故事3.5λ幺半群：代数理论λ-幺半群的定义背后的思想是，它是一个幺半群M，其结构用于表示关于一元运算集合M（1）和二元运算集合M受前几节讨论的启发，我们从幺半群M=M（1）开始，给出一个恒等式I∈M和复合式<$：M2→M以及我们马上得到的方程。然后在M内，我们取一个幂等元1，我们设置M（2）={a∈M|1a = a}。 所以我们进一步取元素T和F来表示投影。它们应该在M（2）中。再加上1的等元数，我们就得到了1 1= 11T = T1 F = F。我们已经提到了幺半群的复合，我们还需要三个复合。我介绍这些符号及其语法解释。首先，为了一致性，幺半群复合本身是n：M×M→M;（a，b）<$→a<$b，M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59712语法解释为a（b（x））。 然后有一个组成型号：M×M→M;（a，（b，c））<$→a（b，c），具有句法解释a（b（x），c（x））。当然，原则上这是一个组合M（2）×M2→M，如上所述扩展。我在这里使用相同的符号，因为合成的输出不受限制。还有一种成分*：M×M→M;（a，b）›→a*b，具有句法解释a（b（x，y））。原则上，这里的复合是M×M（2）→M（2）的形式，符号*引起了对受限余域的注意。最后还有一个组成部分*：M×M2→M;（a，（b，c））›→a*（b，c），具有句法解释a（b（x，y），c（x，y））。现在，复合原则上是M（2）×M（2）2→M（2）的形式，在符号中，配对（b，c）引起对第一个M（2）的注意，而*再次表示受限的余域。我们应该避免愚蠢的区别，所以我们需要一些卫生的法律，就像上面的T和F，确保我们的非标准组合物的良好行为我列出这些。共域约束只涉及*组合：它们是1（a* b）= a*b;1（a*（b，c））= a*（b，c）。涉及配对的组合要求对应用的内容进行限制：这些限制是（1 a）（b，c）= a（b，c）;（1 a）*（b，c）= a*（b，c）。最后，我们可以预期域约束：a*b = a*（1 <$b）; a*（b，c）= a*（1 <$b，1 <$c）。给出这些没有什么坏处，但事实上，它们将从方程中得出。在这份文件中，我将不再进一步关注冗余问题我们有自己的身份，投影和组成，我们需要单位和作为社会性的法律.我不想把这些给幺半群，以便把它们放在一起处理。让我先给出单位律来扩充么半群的单位律。这些涉及到偶尔的调整，以考虑到收回。我提出它们，使它们与3.3节中出现的定律平行。左定律是I*a=1aT（a，b）=a T*（c，d）=1cF<$（a，b）=bF*（c，d）=1<$d正确的法律是a I = ac *（T，F）= 1c。72M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）5922当然，在这些单位定律中，有关于幺半群的。我现在转向结合律。回想一下2.2节中的结合性条件，对于所有的n，m和p，T（n）×T（m）n×T（p）m）T（m）×T（p）mV VT（n）×（T（m）×T（p）m）n）T（n）×T（p）n ）T（p），上下班在Λ-幺半群的设置中，我们可以设置n，m和p为1或2，所以我们得到了对应于3.3节中八种句法形式的八个结合律。我按照与上面类似的顺序列出这些，在每种情况下，都从图的左上角开始T（1）×T（1）×T（1）（a<$b）<$c=a<$（b<$c）2T（1）×T（2）×T（1）（a* b）<$（c，d）=a<$（b<$（c，d））T（1）×T（1）×T（2）（a<$b）*c=a*（b* c）2T（2）×T（1）×T（1）（a<$（b，c））<$d=a<$（b<$d，c<$d）2T（1）×T（2）×T（2）2（a* b）*（c，d）=a*（b*（c，d））T（2）×T（1） 2×T（2）（a∈（b，c））*d=a*（b* d，c* d）2T（2）×T（2）×T（1）a*（b，c））<$（d，e）=a<$（b<$（d，e），c<$（d，e））T（2）× T（2）×T（2）（a*（b，c））*（d，e）=a*（b*（d，e），c *（d，e））当然，列出的第一个结合性只是关于幺半群的。3.6Λ-幺半群：λ-演算方面到目前为止，在我们所整理的内容中，还没有太多关于λ演算的迹象事实上，我们很可能有I=1，在这种情况下M=M（2），然后我们可以编码任何截断代数理论与T（1）和T（2）之间的同构λ演算的第一个方面包含了我们将要看到的函数空间的关键表示。我们的成分不是完全独立的，特别是我们需要下面的特殊方程来联系其中的两a<$（b <$c，d）=（a <$b）<$（c，d）.这个等式应该是一种解脱。到目前为止，关于参数对的一切都是完全对称的。但该特殊方程是不对称的，它在对称条件下的孪生方程不成立。最后，我们有一个在某种意义上使投射内在化的特征。我们在方程中附加常数p，q∈M和m∈M（直观地在M（2）中），M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59731m = mp * m = Tq* m = F。74M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59这些常数在基本定理的证明中起着至关重要的作用。理解它们的方法是把m看作是M（2）中的m，因此是一个二元函数。它是一种弱形式的配对，M=M（1）中的p，正是这些功能，我们开始看到的微妙之处所考虑的Koymans [7]为他的概念的λ-幺半群。3.7Λ-幺半群的Λ -设A是[5]意义上的Λ-代数，或者（两者的意义相同）是传统意义上的λ-代数[2]。然后，可以给出一组A（1）={a ∈ A|1a = a|}一个λ-幺半群的结构如下。 常量为I=λx.x，1=λxy.xyT=λxy.x，F=λxy.y，p=λx.xT，q=λx.xF，m=λyzx.x（yz）二进制运算是a*b=λx.a（bx），a * b=λxy.a（bxy），c∈（a，b）= λx.c（ax）（bx），c *（a，b）= λxy.c（ax）（bxy）.命题3.4假设A是一个Λ-代数。 则A（1）={a∈A|1a = a}具有上述结构的是Λ-幺半群。证据有很多方程需要检查，但这都是用λ项进行简单计算的问题。我举几个例子来说明。关键的特殊方程如下所示a<$（b<$c，d）=λx.a（（b<$c）x）（dx）=λx.a（b（cx））（dx）=λx。（a<$b）（cx）（dx）=（a<$b）<$（c，d）p的基本方程由计算p*m = λxy.p（mxy）= λxy. （λz.zT）mxy= λxy.mxyT = λxy. （λuvw.wuv）xyT=λxy。Txy=λxy.x=Tq* m的计算非常相似。Q3.8Rexexive对象M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）5975设M是幺半群，考虑集合X的预层范畴PM，其右作用X×M→XbyM.泛对象U是可表示的函子，76M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）59U也就是说，M本身具有明显的成分作用。现在假设M具有λ-幺半群的结构。第一个目标是使用这些数据来展示U作为一个反射对象。设M（2）={a∈M|1a = a}，其组成的明显正确的行动。由于1∈M是幂等的，这显然是U在下午.然后，我们的想法是Λ-幺半群结构给出了与函数空间UU的一个恒等式。对于任意X，Y∈PM，标准范畴论用M-等变映射φ：M×X→Y的集合来标识函数空间YX，其中右M-作用由φ.c（a，x）=φ（ca，x）给出。评估图是Y X×X→ Y;（φ，x）<$→ φ（I，x）.现在考虑当M是Λ-幺半群时UU的特殊情况。给定c∈M（2），我们有一个显映射φc：M×M→M;（a，b）<$→c<$（a，b）.目的是证明这提供了M（2）与U的一个恒等式。引理3.5任何等变φ：M×M→M具有以下形式（a，b）›→c（a，b）对于唯一的c ∈ M（2）.证据 首先注意，对于任何c，映射M×M→M;（a，b）<$→c<$（a，b）确实是M-等变的，（c<$（a，b））d=c<$（a<$d，b<$d）由结合律之一。相反，如果任何φ：M×M→M，我们定义c φ= φ（p，q）*m。我们的一个卫生定律表明cφ∈M（2）。使用结合律的简单计算给出（c（p，q））*m=c（p * m，q * m）=c（T，F）=1c=c，最后一个等式假设c∈M（2）。因此，一个相关的复合物是身份。为了证明另一个，我们假设φ是等变的，并使用另一个分配律几次，我们得到以下计算M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）5977（φ（p，q）* m）<$（a，b）=（φ（p，q）<$（m<$（a，b））=φ（p<$（m<$（a，b），q<$（m<$（a，b）=φ（（p* m）<$（a，b），（q* m）<$（a，b））=φ（T（a，b），F（a，b））=φ（a，b）.（等方差用于第二行。）这些计算一起给出了M（2）和等变φ之间的集合的同构。Q当然，我们不想要集合的同构。相反，我们想要PM中的同构，即M-集的同构.因为这就是需要表明我们在PM中有一个反射对象的东西。命题3.6如果M是Λ-幺半群，则泛对象U ∈ PM获得自反对象的结构。证据 我们表明，同构M（2）→PM（U×U，U）;（a，b）<$→c<$（a，b）是M-集的同构。d∈M的作用在第一种情况下是c<$→c<$d，在第二种情况下是φ<$→φ.d，其中φ.d（a，b）=φ（d<$a，b）。但我们最后一个对称破缺方程是（c<$d）<$（a，b）=c<$（d<$a，b），这正是我们所需要的但由于M-集M（2）是M的收缩集，所以命题如下.Q3.9恢复一个Λ-代数让我们退后一步。在3.7节中我们看到，一个Λ-代数A给出一个Λ-幺半群MA。然后在3.8节中我们看到，一个Λ-幺半群M给出一个预层范畴PM，它有一个泛对象U，具有显自反结构UU a U。这本质上是[5]中一个关键论点的文明版本在任意范畴C中，一个自反的UU aU给出一个λ-理论U，这或多或少是一件小事其中U（n）=C（Un，U）。最后从任意λ-理论L得到一个Λ-代数L（0）。所以在我们的例子是一个Λ-代数U（0）=C（1，U）。 我们可以很容易地确定Λ-代数由任何Λ幺半群产生。为PM（1，U）= C M={c∈M|ca = a for all a∈M}是么半群中的常数集。有以下直观合理的特征。命题3.7 F∈CM和c∈CM当且仅当c = c<$F。这个证明并不十分简单，我省略了细节。我希望在另一个场合对这个Λ-代数作更多的讨论。78M. Hyland/Electronic Notes in Theoretical Computer Science 303（2014）593.10什么是Λ-幺半群？在最后一节中，我用本文或[5]中所涉及的材料来设置场景。通过后者的论证，我们知道，如果我们从一个Λ-代数开始，绕着这个圈走，我们会得到一个Λ-代数，它与原来的代数具有一个特定的自然同构。如果我们从一个λ-理论出发，然后再去寻找另一个λ-理论，情况也是如此。这里又有一个特殊的自然同构。但是，坐在中间的Λ-幺半群是什么？此时自然的问题是，我们是否可以将从诱导Λ-代数CM得到的Λ-幺半群与原Λ-代数M等同起来。在这里，为了满足读者的胃口，我只是粗略地描述一下将Λ-代数CM的合成幺半群与幺半群PM（U，U）等同起来是很简单的，并且将其等同起来是范畴论的常规方法。M.识别实际上是微不足道的。每个a∈M诱导一个由b<$→a<$b给出的映射U→U;每个α：U→U由α（I）诱导。所以很明显，我们的工作是研究Λ幺半群的附加结构似乎有一个自然的发展顺序。首先检查关键的幂等元1在标识下保持不变。然后，我们来考虑一下组成部分。最棘手的是组成a（b，c），但直接计算表明它是保留的。其他成分a*b和a*（b，c）保持不变的事实可以从分配律中得到解释。(As我注意到，在第一种情况下，它是我们已经使用的法律，而在第二种情况下，法律是新的。这可能会让人停顿