置换代数的特征结果及其在名义演算中的作用

理论计算机科学电子笔记104（2004）129-147www.elsevier.com/locate/entcs置换代数的一些特征结果法比奥·加杜奇a 马里诺·米库兰baDiparti medInformati ica，UiversitadiPisavia F. Buonarroti 2，56127 Pisa，Italy. {gadducci，ugo}@ di.unipi.itbDipartimentodiMatematicaeInform atica，Universit`adiUdineviadelle Scienze 206，33100 Udine，Italy.miculan@dimi.uniud.it摘要近年来，许多一般介绍（Meta模型）的结石与名称传递，无论是操作或指称的命名，已被提出。在本文中，我们研究了其中一些建议之间的联系，即置换代数，命名集和层范畴，目的是建立一个桥梁之间的不同方法抽象指定的名义演算。关键词：语义的编程语言;名称传递演算;分类和代数元模型的语言。介绍自从π演算的引入，名称的概念已被公认为中心的并发性，移动性，分级计算，元编程，内存区域分配等模型，近年来，已经提出了几种方法作为通用框架（元模型），简化这些模型的发展，具有名称传递和/或分配。最常见的方法之一是考虑有限集和内射函数的范畴I上的函子范畴，例如预层集I;参见例如Moggi，Stark，Hofmann，Fiore和Turi等[13，16，* 研究得到意大利MIUR项目COFIN 2001013518 C O M ETA和EU-FET项目IST 2001-33100 P ROFUNDIS的支持。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.08.022130F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-8、5]。预置层代表“分级计算”，由当前分配的名称（有限）集合索引。在这些范畴中，定义初始代数/最终余代数的经典结果可以扩展到处理名称，因此非常适合于解释多项式函子给出的规范。一个变体只考虑层的一个子类，导致支持经典逻辑的模型;见例如。Stark，Hofmann，and others [16，8，2].Gabbay和Pitts [6]提出了另一种方法，该方法基于原子集合论的Fraenkel-Mostowski置换模型（FM-集合）具有置换的集合的不同理论，命名为集合，已经被引入作为历史依赖自动机的操作模型的基础[14];而为了在该形式主义中发展结构化的共代数理论，置换代数也是合适的代数规范的模型。排列，已被法拉利，蒙塔纳里，Pistore考虑[4]。毫不奇怪，有这么多的方法：尽管所有最终处理相同的问题，他们受到不同的目标和观点的启发，导致不同的解决方案和选择。因此，研究这些元模型之间的关系非常重要。首先，这将指出元模型之间的相似性和差异性。可能的是，表面上奇特的特质要么被证明是正当的，要么被揭示为不重要的。此外，这些互连允许在元模型之间传输实际上，这种形式化的比较允许突出某些元模型的弱点，并可能提出改进建议然而，这些方法并不总是容易比较，也因为它们存在于不同的元逻辑环境中（范畴论，（非标准）集合论，代数规范，自动机理论......）。）.到目前为止，我们知道[6]中使用的有限支集的FM-集的模型等价于[8，2]中使用的层范畴，当然，它是[8，5]中使用的集I的完全对应子范畴。然而，大的图景仍然是不完整的，因为与其他方法的联系，特别是与那些植根于置换代数的方法，仍然不清楚。这确实是这项工作的目的：我们研究每突变代数，命名集和层范畴之间的联系。置换代数是置换签名上的代数。通常我们感兴趣的置换代数的元素是有限支持的-即，我们立即排除了具有无限自由名称的过程和术语。本文的一个结果是，具有有限支集的置换代数等价于拉回保持函子范畴I→Set，即，所谓的沙努尔·托波斯11一个更强的结果，说明了Schanuel topos与只包含有限核置换的签名上的置换代数范畴之间的等价性，F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-131--{∈|/}∈另一方面，命名集已经被引入作为历史依赖自动机的构建块，历史依赖自动机是一种操作模型，其状态配备有一组名称和名称双射。在某种程度上，命名集被认为是置换代数的一种实现在本文中，我们使这种联系变得精确：事实证明，命名集合形成一个范畴，它等价于具有有限支撑的有限核代数范畴这些结果证实了具有有限支集（和命名集）的置换代数是处理名称的形式化的一个很好的元模型，如就像Sh（Iop）和FM集一样。概要。在第1节中，我们回顾了（有限核）置换、置换代数和有限支撑的基本定义。在第2节中，我们证明置换代数可以看作是连续G-集，因此具有有限支集的置换代数最终对应于Schanuel topos。 在第3节中，我们考虑命名集，并且我们证明它们也形成一个范畴，该范畴等价于具有有限支撑的有限核置换代数范畴。最后，在第四节中得出了一些结论。1置换代数本节回顾置换代数的主要定义：它们主要来自[14]，并有一些额外的参考文献。定义1.1（置换群）给定一个集合A，A上的置换是A上的双射内函数。所有这些置换的集合记为Aut（A），它形成一个群，称为A的置换群，其中运算是函数复合：对于所有π1，π2∈ Aut（A），π1π2π1<$π2。在集合上，置换与自同构一致（因为没有结构要保持），因此符号表示置换群。然而，我们坚持使用排列，因为现在这几乎是理论计算机科学中的标准用法，并且它是我们主要参考文献中使用的术语：参见[14，第2.1节]和[6，第3节]的初始段落定义1.2（有限核置换）设πAut（A）是A上的置换。 π的核定义为ker（π）一一π（a）= a .有限核置换的集合Aut fk（A）形成Aut（A）的子群。现在让我们固定A为ω = 0，1，2，. . 自然数的集合。 在本文中，我们将把我们的注意力限制在ω上的排列，即，属于由于缺乏空间，本书中省略了这一部分;我们请读者参阅[7]。132F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-^ ^您的位置：^^^^^πππ^∈Aut（ω），即使我们的定义和评论可以完全普遍地适用。定义1.3（置换签名和代数）置换签名由一元运算符{π|π∈ Aut（ω）}，以及一对公理schemata id（x）= x和π1（π2（x））= π1π2（x）。 置换代数A =（A，{πA}）是一个关于π π的代数。置换态射σ：A → B是代数态射，即，函数σ：A→B使得σ（πA（x））= πB（σ（x））。最后，Alg（π）（通常简称为Algπ）表示置换代数及其态射的范畴例如，相同的置换集合Aut（ω）形成置换代数的载体。π演算的置换代数给出了一个有趣的例子：载体包含了所有的过程，直到结构上的一致性，而置换的解释是相关的名称替换（也见[14，定义15和第3节]）。我们现在给出一些关于有限核性质的额外定义，这些定义也是从[14，2.1节]中得出的。定义1.4（有限核的代数）有限核置换签名fk作为限制于有限核置换诱导的一元算子的π的子签名而获得。代数的相关范畴是Alg（Algfk），简称为Algfk。π π当然，有限核并不意味着有限载体，因为每个代数FK在Alg中，π也属于Alg，因此前者是后者的子范畴然而，Algfk有一组可数的算子和公理，因此它是更符合代数规范模型的标准结果。具有有限核和无限载体的代数的一个例子是具有有界并行性的π演算的置换代数，即，仅限于那些递归过程，其展开只能产生有限个[14]见“名”，见“名”。我们现在提供一个关于有限支持属性的定义的最终列表。他们根据[6，定义3.3]和我们在下面几节中的需要，重新表述了[14，2.1节]定义1.5（有限支撑代数）设A是置换代数，且a∈A。我们把a在A中的置换集合记为fixA（a），即，这些排列π使得πA（a）= a。此外，设X <$ω是一个集合。我们将f ix（X）表示为固定X的排列集合（即，这些排列π使得π（k）= k对于所有k X），我们说集合X支持元素a，如果所有固定X的排列也固定A中的元素a（即，如果fix（X）<$f ixA（a））。一个代数A是有限支集的，如果对于它的载体的每个元素，F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-133π.π存在一个有限集支撑它，所有有限支撑代数的范畴记为FSAlg（π），简称为FSAlgπ。值得注意的是，并非Algπ中的所有代数都是有限支持的（因此，Algfk中的代数也不是）。例如，让我们考虑代数（A，{π π ∈ Au t f k（ω）}），其中A c为i d，且满足以下条件|ρ（i）=i − 1if i = 2 k +1 =（1，0，3，2，5，4，7，6.. ）的方式i+1，如果i= 2k它在有限核置换的预合成下是封闭的。设ππ（ρ）πρ：这个代数在Algπ中，但它 不是无限可支的. 事实上，对 于任 何Xω 有 限， 我 们 可以 选 择π∈Autfk（ω），使得π（x）=x，x∈X，但满足maxx（X） +1和max x（X） +2;nπρ（ρ）=πρρ。一般来说，代数的载体的元素可以有不同的集合支持它。下面的命题，镜像[6，命题3.4]，确保最小支持确实存在。命题1.6设A是置换代数，且a∈A。如果a是有限支撑的，则存在ω的一个最小有限子集支撑它。给定一个代数A，和一个有限支撑元素a∈A，我们称a的支撑为支撑它的（必然唯一的）最小子集，记为suppA（a）。很容易看出，fixA（a）总是形成一个群。此外，固定一个元素的排列与它的支持有很强的联系 我们用一个与一个简单结果相关的技术引理来收紧这一节，这是必要的。关于保留支持的排列。引理1.7（保持支撑）设A是置换代数，a∈A是有限支撑元。此外，设spA（a）是保持a的支持的置换的集合（即，spA（a）{π|π（suppA（a））=suppA（a）}）。A（a）是一个群，且fixA（a）≠A（a）。2置换代数与连续G-集在这一节中，我们证明上面考虑的代数范畴Algπ和Algfk与代数拓扑的一个著名概念，即（连续）G-集的概念严格相关。这将允许利用一个庞大而完善的理论，这将在下一节中使用定义2.1（G-集）设G是一个群。一 个G-集是一个对（X，·X），其中X是一个集合，·X：X×G→X是一个右G-作用，即x·Xid=x（x·Xg1）·Xg2=x·X（g1g2）134F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-ππ^^ ^您的位置：πG-集之间的态射f：（X，·X）→（Y，·Y）是函数f：X→Y使得对所有x ∈ X，f（x·Xg）= f（x）·Yg。G-集和它们的态射构成一个范畴，记为BGδ。考虑当G是Aut（ω）或Autfk（ω）时的G-集.显然，每个Aut（ω）-集也是一个Autfk（ω）-集（仅仅通过限制有限核置换的作用），模仿Algπ和Algfk之间的对应。事实上，形式主义之间存在更强的等价性，正如下面证明的结果所证明的那样。命题2.2Algπδ=BAut（ω）δ和Al gfkδ=BAut fk（ω）δ。证据设A是置换代数.我们定义了一个相应的Aut（ω）-集G（A）=（A，·G（A）），其中a·G（A）π πA（a）对所有a∈A. 另一方面，如果（X，·X）是Aut（ω）-集，则定义相应的代数X=（X，{πX}）x·Xπ，其中π∈Aut（ω）.bytakingπ^X（x）设A，B是两个置换代数.一个函数f：A→B是Algπ i <$f（πA（a））=πB（f（a））中的一个态射f：A → B，它对所有排列π和a ∈ A都成立i<$f（a·G（A）π）= f（a）·G（B）π，等价地指出f：（A，·G（A））→（B，·G（B））是BAut（ω）δ中的态射。显然，这种对应关系是充分和忠实的，因此论文。使用相同的公式，我们有许多公式Algfk=BAut fk（ω）δ。Q此外，具有有限支撑的代数的子范畴（可能仅在有限核置换上）可以在更一般的G-集的设置中重新转换，但为此，我们需要回忆拓扑理论中的一些概念;见例如[10]为介绍这些概念的背景下，一般拓扑，[11，第五. 9]和[12，二]的背景下，范畴和拓扑理论。定义2.3（拓扑空间）拓扑空间是一pair（X，O（X）），X是一个集合，O（X）∈ O（X）.函数f：X→Y 是连续映射f：（X，O（X））→（Y，O（Y）），如果f−1（U）∈ O（X），对所有U∈ O（Y）。拓扑空间和连续映射形成一个范畴，记作top。O（X）的元素被称为拓扑的开集示例2.4最小值（即，时间复杂度为O（X）={x，X}。 另一方面，最精细的拓扑是离散拓扑，其中O（X）=（X）.很容易证明一个拓扑是离散的当且仅当对所有x∈X{x} ∈ O（X），即，如果每个点都与其他点分离（因此得名）。显然，每个函数相对于离散拓扑都是连续的F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-135∩∩逻辑空间，其空间为X=πi∈IXi，且拓扑最小那么O（X）=i∈IO（Xi）. 然而，这个属性对我来说并不成立注2.5（空间的积）范畴top是完备的和余完备的[11，V.9节]. 特别地，给定一族拓扑空间（Xi，O（Xi））∈top，索引为i∈I，乘积i∈I（Xi，O（Xi））是拓扑-拓扑使得投影πi：X→Xi是连续的。 如果我是有限的，现在我们回想一下最后一个标准定义，它是定义2.1的推广。定义2.6（拓扑群和连续G-集）群G是拓扑群，如果它的载体配备有拓扑，并且它的乘法和逆关于这个拓扑是连续的。一个G-集（X，·X）是连续的，如果G是拓扑的，且作用·X：X×G→ G关于X是连续的，且具有离散拓扑。连续G-集之间的态射f：（X，·X）→（Y，·Y）f：X→Y，表示动作。对于给定的拓扑群G，连续G-集和它们的态射形成一个范畴，记为BG。注意，对于任何群G，所有G-集的范畴是连续G-集的范畴，其中G具有离散拓扑注2.7（置换群作为拓扑空间）让我们考虑空间N，它是一个自然数集合ω，具有圆盘拓扑。 Baire space是一个存储空间，∞i=0N=Nω，配备了无限产品拓扑结构。该拓扑的基由下式给出：m∞i=0Ai的集合s，其中Aiω仅对有限多个索引i。现在让我们考虑群Aut（ω）和Aut fk（ω）。 所述 在[12，Section III.9]中，对于Aut（ω），这些群的载波可以被看作Baire空间的子空间，其中每个π对应于无限列表（π（0），π（1），π（2），. ）的。现在，Aut（ω）和Aut fk（ω）都从N ω继承了一个拓扑：它们的开集具有U Aut（ω）和UAut fk（ω）的形式，其中U openN ω的集合。 因此，我们可以分别考虑连续Aut（ω）-集和连 续 Aut fk（ω）-集的 范 畴 B Aut （ ω ） 和 B Aut fk（ω）。现在我们准备证明我们的第一个主要结果，即连续G-集与有限支撑置换代数之间的对应性。我们首先陈述一个技术引理[12，I，练习6]。引理2.8设（X，·X）是G-集，对于每个x∈X，设Ix{g∈G|x·Xg = x}记为x的各向同性群。 则（X，·X）是连续的，只要它的所有迷向群是G中的开集.定理2.9FSAlgπf=BAut（ω）和FS Al gfkf=BAut f k（ω）。136F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-ππ.- 是的我i=0时我π^.我我ω否则JJI支持x. 设π∈Autfk（ω）∈J. 对所有j∈ω，若j∈JX∞j=0Xi0j，且有π∈Ix，即 ππ（x）=x·Xπ=x，则此定理成立。π∈Iai=0时我我的律师。为了证明FSAlgfk=BAutfk（ω），我们表明，命题2.2的G将具有有限支撑和有限核的代数映射到连续Autfk（ω）-集，反之亦然。设tA=（A，{π<$A}）是FS Algf k中的一个代数，对应于Autf k（ω）-setis（A，·G（A）），其中a·G（A）π<$A（a）对所有a∈A. 对于Lemma2. 8，G（A）是连续的当且仅当对所有的a∈A，Ia是开的.事实上：∞Ia={π（i）}π∈Iai=0=∞Aπ<$Autfk（ω）其中Aπ{π（i）}如果i∈supp（a）=.∞AπAutfk（ω）（1）π∈Iai=0它在Autfk（ω）中是开的，因为每个∞Aπ在Nω中是开的，因为suppA（a）是有限个，因而只有有限个Aπ2另一方面，设（X，·X）是一个连续的Autfk（ω）-集，我们证明了X=（X，{πX}）在FSAlgfk中。显然X是有限核置换代数。根据引理2.8，对于任 意 x∈X ， Ix 是 Autfk （ ω ） 的 开 集 ， 因 此 对 于 Nω 的 某 个 U 开 集 ，Ix=U<$ Autfk（ω）。 更明确地说，Ix可以是写成如下I=∞Xi∈I j=0Autfk（ω）对于某个指数族I，并且其中对于每个i∈I，存在一个有限使得Xij/=ω仅对j∈Ji。因为id∈Ix（它是一个群），存在i0∈I使得id∈∞j=0Xi0j. 我们认为，0则π（j）=j∈Xi0j，否则Xi0j= ω. 在这两种情况下，π（j）∈Xi0j。所以π∈对于预处理FSAlgt=BAut（ω），我们可以使用上述参数，只需将Autfk（ω）替换为Aut（ω）。Q利用这个结果，我们可以利用一个关于连续G-集的成熟理论特别是，我们很容易建立联系，2我们也可以直接证明等价性（1）。很 明显，我是个骗子。π∈I我∞i=0Aπ我Autfk（ω）. 设π∈。∞i=0AπAutfk（ω）;则存在ρ∈Ia使得对所有i∈ suppA（a）：π（i）= ρ（i）. 因为ρ（a）= a，所以π（a）= a，所以π ∈ Ia。一π∈IaIJF. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-137π预层类别。回想一下，小范畴C上的预层范畴是函子集Cop的范畴，以及它们之间的自然变换。许多作者使用集合I范畴，其中I是有限的ω和内射映射的子集，用于对名称或位置的动态分配的计算概念进行建模;参见例如[13、16、8、5]。为了我们的目的，我们考虑集合I的一个特殊的子范畴，即关于原子拓扑的层范畴，记为Sh（Iop）。这个子类别方便地用下面的性质来表征[9，例2.1.11（h）]。命题2.10 Sh（Iop）是拉回仿射函子集I的全子范畴。范畴Sh（Iop）通常被称为Schanuel topos。它具有与上面的集合I相同的重要性质：它是一个拓扑（因此它是Carnival闭的），函子N=y（1）是一个层，多项式函子的初始代数和最终聚结是拉回保持的。因此，Sh（Iop）可以用来代替SetI来给出具有动态名称分配的语言的语义，如在[16，17，8，2]中以及最终也在[6]中（作为本质上等价于Sh（Iop）的Fraenkel-Mostowsky集合理论）。集合I和Sh（Iop）之间的主要区别在于后者是布尔拓扑[12，第III.8节，第150章不是，而是前者。因此，Sh（Iop）是经典逻辑的模型，而不是通常的直觉主义（扩展）高阶逻辑topoi。现在，对于[12，第II.9节，推论3]，我们不知道BAut（ω）n=SH（Iop）。因此，作为定理2.9的直接推论，我们有：置换代数与有限支集等价于Schanuel拓扑。Coroll ary2.11FS Algπ = Sh（Iop）。换句话说，具有有限支集的置换代数对应于拉回保持函子I→Set，因此它们形成了一个布尔拓扑，具有足够的结构来定义具有动态名称分配的语言的语义，例如π演算，移动环境等。3我们在图1的图表中总结了我们在置换代数和G-集之间建立的关系。有趣的是注意到包含函子BAut（ω）<$→BAut（ω） δ和BAutfk（ω）<$→BAutfk（ω）δ具有右伴随;后者例如在对象上定义如下：r：B Aut fk（ω）δ→ B Aut fk（ω） （X，·X）›→（{x∈X|Ixopen for Aut fk（ω）}，·X）3实际上，我们还可以提出一个应力方程FSAlgfk=Sh（Iop）。 这一事实的序言是相当技术性和冗长的，因此由于缺乏空间，我们请读者参考[7]。138F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-，，=，zz，zz，zzFK⊂ ∩⊆{∈|}ǁ ·ǁππAlgπ，Algfk，，，z，π，，， ，zBAut（ω）δ，BAutfk（ω）δ，r，、、，rFKFSAlgπ，，E，，，FSAlgπ，，E，，......，zJBAut（ω）=Sh（Iop）、，rBAut （ω）Fig. 1. 排列代数立方体，第一版。这就是对态射的限制。因此，r将每个BAutfk（ω）δ-集映射到其中包含的最大连续BAutfk（ω）-集。rJ：Algfk→FS Algfk（A，{πA}）›→（B，{π A}|B}）其中Ba一fixA（a）对于Aut fk（ω）是开的。现在，fixA（a）是开的，如果存在有限个Jω使得对于fix（J）Aut fk（ω）fixA（a）（见定理2.9的证明）。这正好对应于说a有有限支集，因此我们可以直接定义RJ（A）={a ∈ A|suppA（a）finite}.3置换代数与命名集命名集是HD-自动机的基本组成部分，是置换代数的实现部分。下面的定义是从[4，第3.1节]中提取的，并根据我们的需要进行了简化。定义3.1（命名集合）一个命名集合N是一个三元组N=<$QN，<$·<$N：QN→ω，GN：q∈QN<$（Aut（<$q<$N））<$其中QN是一个状态集;<$·<$N是枚举函数;对于所有q ∈ QN，集合GN（q）是Aut（<$q<$N）的子群（因此，关于逆和单位元是封闭的），它被称为q的置换群。在这个定义中，以及在下面的定义中，我们采用通常的“集合论”惯例，用自然数表示有限序数，因此0 = 0，n = { 0，...，n−1}。因此，Aut（qN）=Aut（{0，.，<$q<$N− 1}）。直觉上，QN中的一个状态表示一个过程，因此函数N给每个状态分配可能在其中自由出现的变量的数量;换句话说，它表示其自由变量的规范选择最后，GF. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-139ǁ ǁ ǁ ǁ22222π2∈ ⟨⟩222表示每个状态的重命名组，在该重命名组下保存该状态，即，这些名称的排列不会干扰其可能的行为。还注意，如果<$q<$N= 0，则GN（q）={id}定义3.2（命名集合的范畴）设N，M是命名集合。一命名函数H：N→M是一对H=<$h：QN→QM，Λh：q∈QN<$$>（I（<$h（q）<$M，<$q<$N））<$其中h是一个函数，Λh（q）是从h（q）M到qN的一组注入，满足附加条件GN（q）<$λ<$Λ h（q）=λ<$GM（h（q））<$λ ∈Λh（q）最后，NSet表示命名集合及其态射的范畴。因此，一个命名函数是一个状态函数，对于每个q∈QN，它配备了一组内射重命名，它们与GN（q）和GM（h（q））中的置换有些相容（并且使得λh（q）=<$如果<$h（q）<$M= 0）。换句话说，特别地，N上的恒等式是Aut（n·n·N）n，并且合成如预期地被定义例3.3让我们考虑几个简单的例子。由于1 ={ 0}是单例集，N1= 1，0= 1， Aut（1）={id}和Np= 1，0=2， Aut（2）={id，（1， 0）}是命名集合：相同的状态集合，不同的状态集合。功能。 相反，Ni= 1，0= 2，{id} Aut（2）是命名集具有相同的状态集和相同的枚举函数Np，但是一个不同的置换群。注意，从Np到N1没有命名函数，因为任何注入λ，当与Aut（2）后合成时，生成整个I（1， 2）。相反，对于j= 0， 1，通过Ij去注释包含注入映射0到j的集合，则id，Ij类似地，从Np到Ni没有命名函数，而Aut（2）是：Ni→Np（并且对于该组注入的任何其他选择都不存在Λ（1）≠Aut（2））。事实上，很容易看出，给定命名集合Q，·，G1和Q，·，G2（即， 相同的状态集和枚举函数，不同的每突变群），G1（q）是G2（q）的子群，对所有的qQ，则id，G2是从前者命名集到后者的定义良好的命名函数。在本节的其余部分，我们将FSAlgfk，有限支撑的有限核置换代数及其态射的范畴，以及NSet，140F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-^^ππ−1^ ^您的位置：πJ∈Aut f k（ω），对n∈ω，letusd.enoteby[π，πJ]∈Autfk（ω）满足^命名集合的范畴。我们计划使[14，第6节]中的一些结果总而言之，命题3.4和命题3.7（以及后者的3.1从命名集到置换代数从命名集合到置换代数的函子是通过自由构造得到的，（显然）类似于集合和代数之间的标准对应我们需要引入一些符号。对于π∈Aut（n），π与πJ，定义为[π，πJ]（i）π（i）ifi n πJ（i−n）+n否则命题3.4（从集合到代数）设FO是将每个命名集合N映射到由QN的元素（视为新常数）自由生成的有限核置换代数的函数，模等价由与GN中的置换相关联的公理集诱导的，即，[^π，πJ]F（N）（q）<$Nq（即， 当π∈GN（q）时，给出了π的一个适当的补集.此外，给定一个命名函数H：N→M，对于每个q∈QN，让我们选择一个内射λq∈Λ h（q）和一个置换λq∈Aut（<$q<$N）扩展λq。设Hλ：QN→QM表示函数Hλ（q）= [λq，id]（h（q）），对所有q∈Q.然后，设FA是将函数H λ的自由扩张与每个命名函数H相关联的函数。对F=<$FO，FA<$定义一个从NSet到FSAlgfk的函子。我的律师。 FO（N）的载波为s{π（q）|q∈QN， π∈Autfk（ω）}/<$N. 很容易看出，所得代数具有有限支集，证明了每个元素[π（q）] N都由集合π（{0，.，<$q<$N−1}）。为了证明因此，我们必须证明每个置换πJ∈ π（{0，. ，<$q<$N− 1}）也固定sπ<$F（N）（q）。现在我们有了<$kJ∈π（<$q<$N）：πJ（kJ）=kJ=<$k <$q<$N：πJ（π（k））=π（k）=kN：π−1（πJ（π（k）=k<==F（N）=（π^−1πJπ）F（N）（q）<$Nq（πFJ（N）（πF（N）（q）<$Nqπ^FJ（N）（π^F（N）（q））<$Nπ^F（N）（q）F. Gadducci et al. / Electronic Notes in Theoretical Computer Science 104（2004）129-141^ ^您的位置：π其中，h（q）等于[λ，id]（h（q）），从而得到了一个新的结果.a女（男）π^^ ^您的位置：π∈∈||一FK现在让我们考虑一个命名的集合函数H：N→M。 函数Hλ可以提升为从自由代数Tfk（QN）到自由代数Tfk（QM）的代数同态。此外，它保留了关于恒等式和复合的公理：然后我们必须证明，这也适用于加法，从置换群中产生的公理 这等价于证明Hλ（[π，πJ]F（N ）（q））<$MHλ（q）对所有π∈GN（q）.通过对比，我们得到Hλ（[π，πJ]F（N ）（q））[π，πJ]F （M ） （[λa，id]F （M ）（h（q）. 首先证明存在一个π∈GM（h（q））使得π<$λa=λa<$π，然后对一个合适的πJ我们有[π，πJ]<$[λa，id]=[λa，id]<$[π，πJ]：这意味着Hλ（[π，πJ]F（N）（q））与h[λ^a，id]F（M）（[π，πJ]F（M）（h（q）重合，其中hich是身份证，GN是明确保留。关于复合，只要证明函子的结果与注入的选择无关就足够了，即给定一个命名函数H：N→M，则对任意λ，λJ∈Λh（q），等式[λ，id]（h（q））<$M[λJ，id]（h（q））成立。为了证明后者，注意到关于Λ H（q）的条件确保存在一个p假设π∈GM（h（q）），使得λ∈π=λJ，从而满足以下条件。Q3.2从置换代数到命名集首先，我们定义一些关于支撑的附加结构。定义3.5（关于有限支集）设是置换代数，A是有限支集元素。然后，范数A（a）I（suppA（a），ω）表示覆盖该支撑的（必然唯一的）保序注入.形式上，normA（a）（i）

下载后可阅读完整内容，剩余1页未读，立即下载