参数代数规范与关系提升的多项式函子研究

理论计算机科学电子笔记106（2004）335-353www.elsevier.com/locate/entcs参数代数规范Hendrik Tews1TUDresden，Institutfur？Theoretisch eInformatik，D-01062 Dresden，Germany.摘要关系提升[6]将内函子F：CC推广到函子Rel（F）：Rel（C）Rel（C），其中Rel（C）是C上的 一个合适的关系范畴。函子F的关系提升可以可用于定义余代数X F（X）的互模拟概念。 谓词提升的相关概念可以用来定义F -余代数的不变量。谓词和关系提升可以直接定义为丰富的多项式函子[5，6，19]。在本文中，我调查函子F被定义为（单排序）参数代数规范的初始语义的情况。关键词：内函子，关系提升，互模拟，余代数，多项式函子，代数规范。1介绍互模拟的概念抓住了行为等价的概念。对于一个被描述为余代数X F（X）的系统，双模拟的定义通常或多或少地直接从描述系统接口的函子F在本文中，我调查的问题，如何定义的概念的双模拟函子，产生于（单排序）参数代数规格与初始语义。这样的函子对于CCSL [20]或CoCASL [10]等特定环境很重要。在这些规范语言中，人们可以通过嵌套代数和1电子邮件地址：tews@tcs.inf.tu-dresden.de1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.040336H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335一BSSScoalgebraic specifications.例如，我们可以首先定义一个集合A上的序列作为函子FSeq（X）= A×X+1的最终余代数，并得到一个函子Seq：SetSet，它将任何集合A映射到A上的可能非终止序列。然后，可以定义具有有限深度和无限宽度的树， 其标签从B 绘制为FTree（X）= Seq（X×B）的初始代数[5]。这定义了一个函子树：Set Set。考虑一个函子F，它是通过迭代具有初始语义的代数规范和具有最终语义的余代数规范而构造的。在[5]中，Hensel和Jacobs研究了迭代数据类型的情况，也就是说，所有这些规范都不包含任何公理。他们的方法也扩展到F的构造的最后一步是一个适当的共代数规范的情况（即，包含公理）。现在假设F的构造的最后一步是一个适当的参数代数规范。 为了简单起见，我假设在下面只有一个参数。如果这个形参是一个类型形参，也就是说，如果在形参上没有使用任何操作（甚至没有相等），那么F可以被认为是一个函子Set Set。在这种情况下，可以使用以下方法：Aczel和Mendler [1]的方法来定义F-余代数上的互模拟本文集中讨论规范在其参数上使用ad-parameter操作（例如相等）的情况。在这种情况下，参数代表参数指定T的模型（通常具有松散的语义）。 因此，F则只是一个函子Mod（T）集，其中Mod（T）表示T的模型范畴。我在续集中表明，一般来说，对于这样的函子，已知的定义互模拟的方法失败了。考虑例如图1。它包含了有限集合的代数规范。有两个要点：首先，规范FSet在T中是参数的，它代表规范Elem的任意模型。其次，FSet通过额外的删除操作指定有限集合。这个删除操作的具体化依赖于Elem的每个模型附带的操作equal。诚然，首选的方法是指定不带删除操作的有限集合，并将其定义为定义扩展。这样就可以使指定仅在类型中是参数化的（也就是说，没有相等操作），并避免使用参数T的相等关系所导致的所有问题。然而，正如图1所示的FSet规范，它代表了一个有趣的边界情况。这很有趣，因为谓词和关系提升的语义和相关概念是众所周知的-即有限幂集函子及其提升[7]。然而，由于技术原因，人们不能使用熟悉的方法来定义（FSet）-余代数的互模拟的H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335337××⇒（Ⅲ）⟨ ⟩⇒×Elem：松散规范操作equal：Elem Elembool结束元素FSet[T：Elem]：初始指定操作空：FSetadd：FSet×TFSetdel：FSetTFSet变量x：FSet; t，t1，t2：T公理add函数：add（add（x，t1），t2）= add（add（x，t2），t1）add idem：add（add（x，t），t）= add（x，t）del empty：del（empty，t）= emptydel addeq：equal（t1，t2）= truedel（add（x，t1），t2）= del（x，t2）del add neq：equal（t1，t2）= false del（add（x，t1），t2）= add（del（x，t2），t1）结束FSetFig. 1. 有限集合的删除运算原因是投影π1和π2一般不反映参数上的等式关系。所以FSet（π1/2）甚至没有定义好！以下关于技术细节的部分介绍了一些更特殊的概念。在第二小节中，它描述了代数规范的语义本小节只包含标准材料，但介绍了本文其余部分所需的符号和假设。该等声明于第9页分节结尾处概述。第3节包含定义，第4节研究其属性。致谢。我感谢霍斯特·赖歇尔（Horst Reichel）的许多讨论和他对代数规范的微妙之处的2技术细节2.1范畴理论集合和全函数的范畴用Set表示。对于乘积（）和余积或不相交的并集（+），我使用标准的符号，投影为π1/2，元组为f，g，注入为κ1/2，余元组为[f，g]。我写X Y作为指数（X和Y之间的函数空间）。n元多项式338H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335⊆∀ ∈∈关于谓词PX是f（x）={f（x）|x ∈ P}。functor是一个从以下语法生成的functorSetnSetF（X1，.. . ，Xn）=一|Xi|F1（· · ·）×F2（· · ·）|F1（· · ·） +F2（· · ·）|A F1（· · ·）迭代多项式函子的文法[5，14]包含最小和最大不动点的附加子句：F（X1，. ，X n）=. |µ X。 F（. ，X，.. ）的方式|V X. F（. ，X，.. ）这里是µX。F（.，X，. . ）表示的初始代数为的functor F（.，−，.. . ）：Set Set（其中F的所有至多一个参数位置都是固定的）和νX。F（···）是它的最终余代数。当在迭代多项式函子μX中使用时。F（···）和νX. F（···）分别表示初始和最终余代数的载波集。态射上的映射定义如下（我只给出了n=2的情况）：设b：F（V，B）B为初始F（V，-）代数和f：UV是任意函数。 然后b<$F（f，id B）具有F（U，−）代数的形式，因此存在唯一的代数同态，a：F（U，A）A，初始F（U，−）代数，作为域。这个代数态射的基础函数给出μX。F（f，X）.定义νX。 F（f，X）1取F（f，id）<$c的唯一余代数态射，其中c是最终F（V，−）余代数。有几个概念是与本文相关的。我只是在这里将它们定义为集合或谓词上的运算，而忽略了它们的固有性质。[12]见《易经》中的《易经》。本文中使用的材料也在[4，第3章]或[20，第2章]中涉及集 合 X 上 的 谓 词 写 为 P<$X={x|x∈P} 。 关 于 X 的 真 值 谓 词 是TX=X<$X。 谓词构成范畴Pred（实际上它们是在Set上生成的）。 一个态射PXQ<$Y是一个函数f：XY使得fx∈Q对所有x∈P。 X和Y之间的二元关系写为R<$X×Y={（x：X，y：Y）|R（x，y）}。在任意集合A上的等式关系是Eq（A）={（a，a）|a∈A}。 关系形成了范畴Rel（它是在集合×集合上产生的）。态射是保持定义域关系（（x，y）R）的函数对。（f x，g y）S）。函数f：X Y关于谓词Q Y的逆像记为f<$（Q）<$X={x∈X|f（x）∈Q}. f的图像，对于任意关系R X×X，商X/R是X关于包含R的最小等价关系的等价类。存在一个商映射qR：X X/R，它将每个x发送到它的等价类[x]R。在适当的情况下，函子是函子[8，4.8节].商的态射分量在这里也很重要。对于两个关系R1<$X×X，R2<$Y×Y和函数f：XYsuchH. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335339P<$PQ<$X<$Y=. F|x ∈ P =<$（f x）∈Q<$- 是的（κ2x，κ2y）|xRy.Σ⊆⊆⊆×⊆×⊆×× P××。|∈∧∈Σx R1y<$（f x）R2（f y）商函子的态射分量记为Q（f）：X/R1Y/R2.它发送一个等价类[x] R1 到[f x]R2.方程Q（f）f一般成立（它由附加式Q E Eq得出）。对于谓词和关系，存在一个特殊的笛卡尔闭结构。对于谓词P<$X，Q<$Y和关系S<$U×V，R<$X×Y，它可以定义如下：P Q X Y=（x，y）x P y QP+ PQ<$X + Y={κ1x |x ∈ P} κ2y |y ∈QS×RR （U×X）×（V× Y）=. （（u，x），（v，y））|uS v xR yS+ RR （U+ X）×（V+ Y）=.（κ1u，κ1v）|uSv索尔河⊆（U<$X）×（V<$Y） =（f，g）|uSv =（fu）R（gy）谓词提升[6]将集合上的多项式函子F提升为函子Pred（F）对Pred，使得Pred（F）（P）F（X）对于P X。F的谓词提升可以用来定义F关系提升将F提升到Rel上的函子，其中Rel（F）（R）F（X）F（Y）对于R X Y。它可以用来定义F通过用谓词或关系的carless-closed结构代替F中Set的carless-closed结构，可以得到这些提升。更准确地说，对于多项式函子F：Set×Set集合和两个关系R1，R2关系提升Rel（F）（R1，R2）归纳定义如下：Rel（A）（R1，R2）=等式（A） Rel（Xi）（R1，R2）=RiRel（F1×F2）（R1，R2）=Rel（F1）（R1，R2）×RRel（F2）（R1，R2）Rel（F1+F2）（R1，R2）=Rel（F1）（R1，R2）+Rel（F2）（R1，R2）Rel（A<$F1）（R1，R2）=等式（A）<$RRel（F1）（R1，R2）谓词提升的精确定义非常相似：谓词提升使用谓词的carbohydrate封闭结构，并对F（···）=A的情况使用TA。Hensel和Jacobs将[5]中的谓词和关系提升推广到迭代多项式函子。提升为µX。F和νX。F被定义为最小和最大固定点，如下所示：考虑关系RX设α：F（X，A）A和β：F（Y，B）B为340H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335×α Pred（F）（P，Q）。类似地 对于νX。福：合适 最终煤-TS预测寿命预测值（µX. F（−， X））（P）的线性不动点定义为S的最小不动点α×βRel（F）（R，S）.为F（X，−）和F（Y，−）。 举升Rel（µX. F（−，X））（R）Qgebrasρ andγ the greatest fixed points ofQρPred（F）（P，Q）和S（ρ γ）Rel（F）（R，S）分别定义了谓词提升和关系提升，很好 这些不动点对所有迭代多项式函子都存在。以下两个技术结果已在PVS中得到证明[11]。引理2.1等价关系的关系提升是所有多项式函子的等价关系。引理2.2设F是多项式函子。存在F（X1，…，Xn）/Rel（F）（R1，.，Rn）和F（X1/R1，.，Xn/Rn）的所有关系Ri <$Xi× Xi。 同构由将[x]R el（F）（···）映射到F（qR1， . . ，qRn）（x）.2.2规范及其语义下面的部分依赖于几个关于代数规范的形式，特别是语义的假设。本节解释这些概念并介绍所需的概念。该等假设于第9页本分节结尾处概述。在本文中，我只考虑最多有一个参数的单个排序规范。对一种排序的限制有些必要，因为我使用态射F（X）X作为代数规范的语义。此外，针对规范提出的提升依赖于Hensel和Jacobs针对数据类型的提升[5]。对一种类型的限制也存在于他们的工作中。限制为一个参数只是为了方便。对于更多的参数，只需向所涉及的函子和提升添加更多的参数。在这篇论文中，我考虑了两个如图1所示的T和S。规格是参数规格。规格是具有初始语义的单个排序代数规范它是T中的参数。因此，签名、签名模型和S的模型的概念也被参数化。参数指定可以是具有松散语义的任意指定（不一定是代数的），如图1中的Elem指定。我忽略所有的语法问题，并假设参数指定T的语义被给定为T的模型的范畴Mod（T）。此类别中的对象是元组T =T|不|，（f i）由载体组组成的载体，|不|和一个函数族（f i）的操作声明在T.态射是函数H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335341∈不在与操作兼容的运营商之间。存在一个明显的遗忘函子U：Mod（T）Set。例2.3设bool为布尔值的集合{true，false}。图1中Elem规范的模型是对EqE，eqEq，其中E是一个集合，eq是一个函数E×E布 尔 。函数f：E1E2是一个态射如果它与运算equal兼容，即如果对于所有的e 1，e 2 E 1，eq 2（f e1，fe2）=eq1（e1，e2）。注意，f必须保持和反映equal的谓词。 这就形成了Mod（Elem）范畴Elem的模型对于代数规范S，我也想忽略语法问题。我假设S的签名被给出为迭代多项式函子Sig：Set×Set Set。这个函子将S的所有运算合并为一个。 第一个参数反映了对参数T的依赖性。Set的第一个参数（与Mod（）相反）是足够的，因为签名（的语义）只取决于参数的载体。签名模型是对S中所有操作的解释，它不一定满足S的公理。它可以作为代数Sig（U，X）X给出，其中U是任意集合，可能形成T的模型的载体。代数Sig（U，X）X（对于任意U）是范畴SigMod（S）的对象。代数a：Sig（U，X）X和代数b：Sig（V，Y）Y之间的这一范畴中的态射由一对函数（f：U V，g：X）组成Y）使得g<$a=b<$Sig（f，g）。存在明显的健忘函子U：SigMod（S）将代数a发送到U并将态射（f，g）发送到f的集合。 函子μX。Sig（−，X）映射对于函子Sig（T，-）的初始代数的集合T是U的左伴随。 还有第二个健忘函子，记为|− |，将每个代数Sig（U，X）X发送到其载波集X。为了处理规范S的公理，我假设对于T 的 每个模型T和每个签名模型a：Sig（|不|，X）X，则可以检验S的公理是否在a上成立。如果公理确实支持T，一个T被称为T的S模型。范畴Mod（S）有S的所有模型（对于所有可能的T）作为对象。态射是函数对（f，g），使得f是Mod（T）中的态射，并且（f，g）是SigMod（S）中的底层签名模型之间的态射。 对于T的每个模型T，都有Mod（S）的子范畴ModT（S），它只包含T的模型。模T（S）中的态射是具有形式（id）的态射|不|，g）。同样，有两个健忘函子U：Mod（S）Mod（T）和| − |：Mod（S）设置。关于规范S有两个重要的假设：第一，342H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335qRel（Sig）（Ⅲ）（Ⅲ）（Ⅲ）（2）（Ⅲ）−（Ⅲ）（Ⅲ）（Ⅲ）SS◦× ||健忘函子U必须有一个左伴随，记作S，使得US是Mod（T）上的恒等式。从符号中可以猜到，左伴随S称为S的语义。它将任何模型T映射到ModT（S）中的初始对象。U（S（T））=T的要求等于S的公理对参数指定没有限制第二个重要的假设是语义S可以被构造为初始代数μX的子代数。Sig（，X）.这个商结构的工作原理如下（也考虑下图）：设T是一个任意参数模型，α = μX。Sign（|不|，X）。S的公理确定了一个关于α的同余关系Q T<$A×A在α的载体上，使得商A/Q T是b= S（T）的载体。 因为Q T是同余关系，所以α是态射Rel（Sig）（Eq（|不|），QT）QT之间的关系，所以Q（α）是如下图所示。A/QT上的运算通过复合b= Q（α）<$i−1定义，其中i是引理2.2的同构。下图说明了这种结构（在图中，我将Rel（Sig）写为Rel（Sig）（Eq（|不|），Q T））：Sign（|不|，A）αAi−1qQTSign（|不|，A）/Rel（Sig）Q（α）A/QBSign（|不|、A/Q T）S的态射分量也必须构造为条件：考虑Mod（T）中的态射f：T V。然后是µX。Sig（f，X）是代数态射α μX。Sign（|V|，X），我们可以设置S（f）=Q（μX）。 Sig（f，X））。关于S的构造的假设没有太多限制：如果S的公理是方程Horn公式，则可以用所描述的方式获得S的初始模型[9]。关系QT的起源与本文无关（只有它的存在）。Meinke和Tucker构造Q-T作为从α到ModT（）的所有代数态射的核的交集。如果的公理是正的霍恩公式，则可以直接从公理构造Q，如下例所示。例2.4图1中FSet的特征函子为F（T，X）= 1+（X×T）+（X×T）。从签名模型γ：F（T，X）X，通过预组合注入来获得单个操作，例如addγ=γκ2。 bool的列表T形成初始签名模型，T. cons单元格中的附加布尔值用于区分add不H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335343S（Ⅲ）不不（Ⅲ）（Ⅲ）（2）（Ⅲ）不S| |（Ⅲ）（S）S德尔的。的方程具有简单的结构。 因此，我们可以将每个公理的语义定义为X上的关系。对于最后一个公理，例如：xdel add neqy删除t1，t2∈|不|，z∈X. <$eqT（t1，t2）x=delγ（addγ（z，t1），t2）n =addγ（delγ（z，t2），t1）我们得到语义QγX×X作为所有公理 如果Q γ ≠ Eq，则代数γ在Mod T（FSel）中，|不|）.可用于分解初始F-代数α的关系QT的最后两个公理是重写规则。对于任何加法和减法运算的列表，它们允许计算一个没有减法运算的等价列表关系QT关联两个列表，确切地说，如果有del-free等价物包含T的相同元素（忽略顺序和多次出现）。因此，QT的每一个等价类都描述了一个有限的集合，T的元素（关于等式T）。 最后，ModT（FSet）中的初始代数同构于有限集合，并具有对空、加和减运算的明显解释。概括而言，本文有以下假设：• 不 是具有松散语义• S是一个单一的排序代数规范，它在T中是参数化的，具有初始语义。• 语义S是函子Mod（T）M o d （S）从类别T的模型之一到S的模型之一。 特别地，S将与参数指定的操作兼容的任何函数f：U V映射到S的U和V的初始模型之间的函数。• 函子S与遗忘函子U左伴随，U∈ S= IdMod（T）。进一步地，S被构造为S的签名的初始代数的商。如果S的公理是等式Horn公式[9]，并且如果它们对参数T没有任何限制，则这些假设为真。2.3S一般来说，可以扩展多项式函子的定义，以允许具有初始语义的参数代数规范的成分函子（也可以用于具有初始语义的参数共代数规范）。344H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（S）最终语义）。然而，有两个技术上的复杂性：首先，将参数指定的模型作为参数。因此，在将S应用于集合X之前，必须为X配备适当的运算（fi）。当然，一般来说，S（fX，（f i）f）的结果取决于运算的选择。第二个问题是，|S（X，（f i）X）|提取S. 在本文中，我想忽略这些技术问题。我写S（X）来表示，根据上下文，S的模型和它的载波集。X上的操作将从上下文中清楚总之，余代数XS（X）的定义是一个四阶段的过程：必须定义载体集合X，为其配备适当的运算（fi），形成应用程序S（X），并最终定义余代数本身。注意，对于这样的余代数，余代数态射的概念仅对实际上是Mod（T）中的态射的函数g有意义（从而保持运算（fi）），因为否则应用S（g）不是良构的。 在本文中，我只考虑形式XS的余代数 （X），其中S的签名函子不包含源自代数规范2.4余代数的互模拟至少有三种方法可以定义两个余代数c：X F（X）和d：Y F（Y）之间的互模拟：(i) Aczel和Mendler提出了以下图表作为定义属性[1]：Xπ1Rπ2YCF（X）F（π1）F（R）F（π2）DF（Y）(ii) Hermida和Jacobs [6]建议对F使用关系提升Rel（F）并将互模拟定义为关系R，1996年， x R y= Rel（F）（R）（dy）(iii) 我们也可以将互模拟定义为那些元素被一对余代数态射所相等的关系。更精确地说，R是互模拟的，如果存在一个余代数z：ZF（Z）和余代数态射f：XZ，g：YZ使得xRy惠fx=gy。对于保持弱回调的函子，所有三种方法都是等价的[18]。H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335345∀（2）−Q现在考虑FSet注意，第一种和第二种方法都不能用来定义FSet第一种方法失败了，因为通常不可能将关系R转化为Elem的模型，使得投影在Mod（Elem）中是态射。第二种方法的问题是必须为每个函子显式定义关系提升。 将F的关系提升与F本身，即方程Rel（F）（R）=<$F（π1），F（π2）<$F（R），出现在[17，2]，不能用于FSet，再次因为投影。第三种方法可以用于FSet-余代数，但一般来说，它产生了一个不令人满意的互模拟概念，如下面的例子所例2.5考虑图1中有限集合的指定，并做以下修改：将新的操作color：Elem bool与公理t1，t2：Elem一起添加到参数指定Elem中。 color（t1）=color（t2）。这意味着一个模型的所有元素都具有相同的颜色。然而，Elem的模型可以用真或假来着色。现在考虑下面的两个余代数（我省略等于运算因为它不相关）：X={x}Y={y}颜色（x）为 真彩色（y）=falsec：XFSet（X）d：Y FSet（Y）c（x）=空 d（y）=空直觉上，状态x和y表现出相同的行为（关于余代数），所以应该有一个相互模拟将它们联系起来。然而，作为Elem的态射，每一个余代数态射都必须保持状态的颜色。没有两种不同颜色的变更Elem质量标准的模型。因此，不可能找到一对态射将x和y映射到同一个元素。3谓词的定义与关系提升本节给出了定义FSet -余代数的互模拟问题的解决方案：依赖于μX的提升的谓词和关系提升的定义。Hensel和Jacobs的Sig（，X）[5]。直接的方法，即通过同余关系T（它提供了公理的语义）分解迭代多项式签名函子的提升，不起作用，参见下面的示例3.2定义3.1设S是一个代数规范，其参数为346H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335T <$S）TS（Ⅲ）（Ⅲ）<$S）qQT。−∩Σ- − −（Ⅲ）一个规格。假设语义：Mod（）Mod（）的构造如第2.2节所述。(i) 一个标准形式的集合是一个索引集合（C T X）。 Sign（|不|，X））T∈|Mod（T）|对于所有的x∈μX。Sign（|不|，X）我们有[x]<$C T<$。(ii) 设T和V是T的模型。 假设标准型的集合C T和C V。对于谓词P，|不|关系R|不| × |V| S的谓词和关系提升被定义为Pred（）（P）=Pred（µX .Sig（，X））（P）C TRel（S）（R）= qQT×qQV。Rel（µX . Sig（−，X））（R）CT×C V）在这里，Sig是S的签名函子，µX。 Sig（-，X）表示将任何集合A映射到初始Sig（A，）- 代 数 的 函 子 ， Pred （ ） 和 Rel （ ） 是Hensel和Jacobs [ 5 ]描述的该函子的谓词和关系提升，q Q T是商的商映射，关于QT，在S（T）的构造中使用的关系规范形式上的条件确保在每个等价项类中至少有一个规范项。在进一步阐述规范形式之前，让我先展示一个例子例3.2再次考虑图1的说明（没有变化）。例2.4描述了签名函子F和FSet的语义。设T和V是Elem的模型，并考虑谓词P|不|关系R|不|×|V|. Hensel和Jacobs定义了μx的谓词和关系提升。F（−，X）为下列方程的最小不动点：Pred（µX. F（−，X））（P） ={空}{add（l，t）} |t∈P<$l∈ Pred（μX . F（−，X））（P）}{del（l，t）|t ∈ P <$l ∈ Pred（μX. F（−，X））（P）}Rel（µX . F（−，X））（R） ={（empty，empty）}{（add（l1，t1），add（l2，t2））|t1R t2<$（l1，l2）∈ Rel（μX. F（−，X））（R）}{（del（l1，t1），del（l2，t2））|t1R t2<$（l1，l2）∈ Rel（μX. F（−，X））（R）}提升的同品种器械Pred（µX . F（−，X））（P）对列表l成立，如果T中所有出现在l中的元素都在P中。 Rel（µX . F（-，X））（R）关联两个列表l1和l2，如果它们包含相同的add序列和del序列（以相同的顺序），使得T和V在相应位置的元素通过R关联。H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335347关于QT的等价类对应于348H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335（Ⅲ）（Ⅲ）| |（Ⅲ）（Ⅲ）（Ⅲ）S| |||T （关于等式T）。谓词提升Pred（FSet）（P）对于这样的集合s成立，确切地说，如果存在这个集合作为加和减运算的标准形式l∈C T的表示，使得l∈Pred（μX）。F（−，X））（P）.标准型主要是关系型，举重。 这里我们看到，如果CT包含足够的项（例如如果C T=|µX。Sign（|不|，X）|），则很容易导出s∈ Pred（FSet）（P）惠s∈P。现在转向关系提升。考虑T上的集合s和V上的集合p。它们通过Rel（FSet）（R）相关，如果存在正则表示ls∈CT和lp∈CV，使得ls和lp通过Rel（μX）相关。F（−，X））（R）.这里的问题是（这就是需要规范形式的地方）完全不同的集合可能具有通过Rel（μX. F（−，X））。例如考虑术语t1=del（add（empty，a），a）并且t2=del（add（empty，b），c）（对任意a∈T，b，c∈V）.从公理对于FSet，我们知道t1=空，t2=add（empty，b）。因此，t1是空集的表示，而t2表示集合{b}。然而，如果R同时包含（a，b）和（a，c），则（t1，t2）∈ Rel（μX . F（−，X））（R）.在两项都是正则项的情况下（t1∈CT和t2∈CV），FSet的关系提升将空集与集合{b}联系起来，这是非常不可取的。为了避免这个问题，我们将规范项的集合定义为那些不包含del运算的项。通过这种选择，很容易看出，FSet的关系提升精确地联系了两个集合s和p，如果对于每个t∈s都有一个v∈p使得tRv，反之亦然。注3.3规范型的集合必须在规范的定义过程中定义。提升在很大程度上取决于标准型。因此，他们应该谨慎选择。如果规范提供了规范形式，那么人们可以将规范形式的单例集作为规范形式。然而，前面的例子表明范式不是必需的。规范形式是必要的，因为规范的公理（当读作重写规则时）可能会引入或删除参数规范的元素（如规范FSet中的del empty）。如果没有这样的公理可以使用所有项的集合作为标准形式。从FSet-示例中产生的印象是，规范形式可以由子签名生成，这是误导性的。它只是表明FSet-示例有些人为：运算del应该被指定为定义扩展。注3.4前面定义的提升分别几乎是Pred和Rel上的函子。确切地说，提升是T的模型上的谓词和关系的范畴PredT和RelT上的内函子。H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335349不S P<$S）（S）P（Ⅲ）（Ⅲ）这些类别分别在Mod（T）和Mod（T）×Mod（T）上进行了定义Pred T的对象是对（P，T），其中T是T的模型，P是|不|.对于Rel也是如此。下面的命题表明定义3.1是合理的：该定义产生了指定FSet的期望提升。命题3.5定义3.1中描述的FSet的提升与[ 7 ]中定义的有限幂集函子的提升一致，如果我们把del -free项作为标准形式。更确切地说，设Pfin（T）表示Mod T（S）中的初始模型，该模型由以下的无穷幂集组成：|不|的三个操作的明显解释。 设i是finn（P）和（T）之间的代数同构。（1），（2），（3），）（P））= Pred（（P）对于所有合适的P，类似的等式，关系解除的条件成立证据显然，在考虑了示例3.2之后。然而，这个证明已经在PVS中正式化[11]。在PVS的证明是令人惊讶的困难，因为它的收益归纳，并涉及建设适当的集合和列表。4新提升在本节中，我将研究所提出的提升的一些性质。 在这些性质与双模拟和不变量的性质之间往往有着紧密的联系。例如，如果F的关系提升与交集互换，那么我们立即得到两个F显然，S的提升性质在很大程度上取决于迭代多项式函子μX的提升性质。 Sig（−，X）.不幸的是，只有少数结果可用于迭代多项式函子的提升。Hensel和Jacobs证明了这些提升是被固定的，并且保持了真理和平等[5]。令人惊讶的是，有许多结果与标准形式的选择无关。在这一节中，我假设S是一个具有参数指定T的代数指定，使得定义3.1。适用于S。引理4.1（单调性）S的提升 是单调的：假设对于适当的谓词P1，P2和关系R1，R2，P1 <$P2和R1<$R2.350H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335（2）（Ⅲ）（Ⅲ）（S）（S）（S）（Ⅲ）（1）（2）（3）（|不|））=Eq（<$S）（T））（Ⅲ）i−i−iii<$S）i<$S）我我然后又道：Pred（S）（P1）Pred（S）（P2）Rel（<$S））（R1）Rel（<$S））（R2）证据迭 代 多 项 式 函 子 的 谓词和关系提升是单调的[5].此外，沿着任意函数的余积f是纤维范畴之间的函子，因此它也是单调的。关于单调性的结果确保Pred（）和Rel（）分别是PredT和RelT上的函数。注4.2单调性也确保了人们可以应用亨泽尔和雅各布斯的定义来得到（常数）函子μX的提升。S（X）和νX。 S（X）。 这些不是迭代多项式函子，所以我们对这些函子和它们的提升几乎一无所知。命题4.3（真与等）在以下意义上，与真与等交换的谓词和关系提升：Pred（<$S））（T|不|）=T<$S）（T）证据 迭代多项式函子的提升与真值和等式交换[5]。定义3.1。i确保CT包含来自每个等价类的项，所以qQC T= T S（X）。关于真与等的上述结果保证了真谓词是余代数的不变量，而等关系是双模拟。下一个结果可以用来证明互模拟在并集下是封闭的。命题4.4（并集）考虑T的模型T和V，令（Pi）|）i ∈ I和（R i <$|不|× |V|）i ∈ I是任意指标集I上的谓词和关系的集合。|)i∈Ibe collections of predicates and relations over an arbitrary index set I.假设μX的提升。Sig（−，X）在以下意义上保持这些集合的并集：Pred（µX . Sig（，X））（P）Pred（µX . Sig（，X））（P）i Rel（µX. Sig（−，X））（R i）<$Rel（µX . Sig（−，X））（iR i）然后，S的提升也保持了任意集合的并集Pred（）（P）Pred（）（P）iRel（<$S））（Ri）SH. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335351××−T：松散规范操作k：T末端TS[T：T]：初始指定操作无：S缺点：STSm：STS变量l：S; t：T公理a：m（l，t）= cons（l，k）端S图二. 实施例4.5的质量标准关于µX的提升的假设。 Sig（，X）是必要的，因为（据我所知）没有通用的结果。此外，只有假设包含才有意义，因为平等并不普遍成立。证据 沿着每个函数f的余积与任意集合的并可交换：fiP i=if P i。作为下一个属性，我考虑纤维性。 函子的谓词提升如果方程F（f）<$Pred（F）（P）= Pred（F）（f<$P）对所有的适当的函数f和谓词P。类似地，F的关系提升是有限的，如果（F（f）×F（g））<$Rel（F）（R）=Rel（F）（（f×g）<$R）。第一纤维是确保Pred（F）和Rel（F）是有限函子的技术性质（即，F上的函子）。然而，关系提升的纤维性允许一个优雅的证明，证明一个函数f是一个余代数同态，如果它的图是一个互模拟。下面的例子表明，如果不仔细选择标准型，纤维性可能失败例4.5考虑图2中的参数S。它用一个额外的（无意义的）操作m来指定列表，使得m（l，t）等于cons（l，k），其中k是参数的已标识常数设T是参数T的模型，使得|不|={t1，t2}是一个二元集合，且kT= t1.那么把t1和t2都映射到t1的函数f是态射TT。S的初始语义是只包含t1或t2的有限列表，以及一个附加的操作m，该操作将t1转换为它的参数列表。352H. Tews/Electronic Notes in Theoretical Computer Science 106（2004）335<$<$）<$）（Ⅲ）（S）（）（）（）（Ⅲ）（S）{}−◦{}| | ||（Ⅲ）设标准形的集合CT是所有项的集合。现在考虑谓词P=t2.注意fP=.令[]Q表示关于用于分解初始µX的关系Q的等价类。SigS（T，X）代数我们有[cons（nil，t1）]Q∈（S（f）） Pred（S）（P） （因为m（nil，t2）∈Pred（µX . Sig S（−，X））（P）而Q（μX）SigS（f，X））将[cons（nil，t1）] Q映 射 到 [cons（nil，t1）]Q）。然而，Pred（S）（fP）={[nil] Q}。当考虑关系提升时，得到关系提升的纤维性的一个反例（t2，t2）不T. 谓词和关系提升都是有限的，如果一个人将规范形式的集合限制为不包含m的那些项。最后两个例子表明，取决于标准型，S的提升可能不会与关系的交集和组合交换。例4.6对于多项式函子，有Pred（F）（P）<$Pred（F）（Q）=