二元方法余代数扩展多项式函子及其应用

317理论计算机科学电子笔记65第1期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 65. html20页s二元方法Hendrik Tews1TUD resden，Institutfur？TheoretischeInformatik，D-01062 Dresden，Germany.摘要在以前的工作[14]中，我介绍了一个广义的余代数概念，它能够在面向对象编程中对二元方法进行建模。这种推广的一个重要问题是，互模拟在联合下不是封闭的，并且一般不存在最大的互模拟。 有两种可能的方法来改善这种情况：第一，加强互模拟的定义，第二，对余代数施加约束（即，二进制方法的行为）。在本文中，我结合这两种方法表明，（在合理的假设下）最大的互模拟确实存在于所有的余代数的扩展多项式函子。1介绍术语二进制方法源于面向对象编程。如果一个典型的例子是equal：Self×Selfbool在这里，Self代表当前类的类型在典型的面向对象语言中，Self类型的第一个参数是隐式的，不会出现在equal方法的接口中。二进制方法以在面向对象的理论描述中提出问题而闻名，参见[2]。给出面向对象语义的一种有前途的方法是基于余代数[11]。一个余代数是一个简单的函数，它有一个结构化的余域，如下一个状态：SelfSelf ×N+1余代数的余域描述了可能的观测和后继状态。它通常用一个内函子来描述。上一1电邮地址： tews@tcs.inf.tu-dresden.de·2002年由ElsevierSc ie nceB出版。 V. 操作访问根据C CB Y-NC-N D许可证进行。特维斯318×我我示例一将使用K（X）=（XN）+1。面向对象的coalge方法的优点是它直接处理了行为、行为不可否认性（互模拟）和信息隐藏等术语。它通过不变量的概念进一步支持共同归纳作为定义和证明原则以及模态逻辑，例如参见[7，12]。然而，使用内函子的余代数来建模类（如[11]中所建议的）并不涵盖二元方法。问题是内函子不足以用二进制方法来建模类签名。解决这个问题的最简单的方法是将二元方法视为定义扩展[6]。 这样，二进制方法就不被认为是签名的一部分，而是作为外部函数，根据签名中的操作统一定义。Hennicker和Kurz在[3]中建议将二元方法形式化为共代数签名的代数扩展这种方法适用于那些具有Self的余域（因此排除了典型的例子equal）并且其行为完全由余代数签名中的操作确定的二元方法 。在[14]中，我提出了一个严格的解决方案，允许对任意类型的方法进行建模，包括二进制方法。这个想法是使用双变函子Setop×Set Set来建模签名，并使用适当的gen-余代数和互模拟的一般概念如果H是这样的双变函子则H这允许对像2这样的外来方法类型进行建模Self×（N<$Self+1）这里我们可以使用函子H（Y，X）=（N<$（Y+1））<$···。（）[14]方法的一个问题是广义余代数是不像弱拉回保持内函子的余代数那样表现良好。[14]中的仔细研究产生了扩展多项式函子类（见第6页的定义），作为表达性和一般结构性质之间的合理折衷 扩张多项式函子覆盖前一个例子（）。对于扩张多项式函子的余代数，可以证明互模拟和不变量在交下是封闭的，余代数态射是泛函互模拟，以及许多其他标准结果（再次，我参考[14]）。[14]中一个重要的问题是在什么条件下广义余代数存在最大互模拟的互相似性这一疏忽激发了波尔和茨瓦嫩堡的兴趣。在[10]中，他们将双代数定义为集合（FI（X）FO（X）），其中X是状态双代数空间与FI我FO我are functorsSetSet描述双代数中第i个Poll和Zwanenburg将可能出现在其对偶代数中的函子限制为2我用X<$Y表示X和Y之间的函数空间（指数）。···自我···特维斯319这些函子可以从常量、恒等式、乘积和余积中构建出来在这些假设下，他们在[10]中证明了对于双代数，最大互模拟等价总是存在的。这一结果意味着，对于某些（真）扩张多项式函子，所有余代数都存在最大互模拟然而，Poll和Zwanenburg的结果并不适用于所有的扩张多项式函子，因为不是每个扩张多项式函子都可以表示为双代数。Poll和Zwanenburg的工作激励了我，基于他们的思想，本文做出了以下贡献：第4节对Poll和Zwanenburg的引用结果进行了简单的概括，并将其适用于我的框架。第4节的主要结果是定理4.6。它说，对于扩展的Caribbean函子（扩展的多项式函子的真子类），那些部分等价关系的互模拟形成了一个完整的格。例4.7表明定理4.6是尖锐的：它包含一个扩张多项式函子的余代数，该函子具有无限上升的互模拟链，没有上限。例4.7基于一个不可判定的函数.这就提出了一个问题，定理4.6是否可以通过对余代数施加某些限制来第5节给出了这样一个限制：有限基余代数。它使定理5.7的证明成为可能，定理5.7（粗略地）说，对于那些有限基的扩展多项式函子的余代数，确实存在最大互模拟其他部分的内容如下：下面的第2节介绍了一些非标准的符号。第3节复制了[14]中的重要特别地，第3节定义了各种函子类以及余代数和双模拟的概念与[14]相比，有一个很小但很重要的区别：本文中所有函子都可以包含函子List：Set Set作为成分函子。(The函子List在其参数上构建（finite）列表集。本文的一个特点是，所有的结果和例子已经-在可行的范围内-形式化并在定理证明器PVS[9]中证明源代码可在万维网上的URLwwwtcs.inf.tu-dresden.de/publictews/binary/.在介绍的其余部分，我讨论了为什么要关心上面的（）方法。为此目的，考虑具有两个运算的一个位置缓冲器store： FREEfetch： SelfI+1一种方法是添加一个公理fetch（store（x，i））=k1i，并允许fetch返回如果之前没有存储任何内容，则∈1现在让我们用指针对一个位置的缓冲器建模，如图1所示。除了它的当前内容之外，每个buffer都包含一个next字段，该字段（潜在地）保存其他一个buffer的引用。在图1中，botthb1和特维斯320内容：7下一篇：·B1B3图1.一、具有以下关键点的电子应用程序数据库的特性：数据库数据库1和数据库2均为数据 库3。B1和B2可以在B3的基础上使用。b2holdarefe erencefb3.这将引用buffer的b1c在b3上创建方法。特别地，在b1上创建方法可以在b3中产生状态变化。这一结构在所有具有可靠性b3的缓冲器中均可见。使用下一个引用的方法的一个例子是方法push。当在bubber1上执行此操作时，通过调用（通过引用）b3上的存储器，将b1的内容存储在bubber3中。3如前所述，当在b1中推动时，b3的变化在b2中可见。 在纯函数环境（如定理证明器）中执行此操作的一种新方法如下：下一个字段仅包含索引（或地址），而不是对缓冲器的引用想要访问下一个字段的方法获得一个缓冲器环境作为额外的参数。存储在下一个字段中的索引可以通过环境解析。的环境可以从一个方法调用传递到下一个方法调用，反映系统全局状态的变化有不同的可能性来模拟这样一个商业环境。一种可能性是取函数NSelf+1（假设索引是自然数）。在这种情况下，方法push的类型如下。push：Self×（N <$Self +1）（N （1）对环境建模的第二种可能性是使用关联列表（即，在N ×Self上列出）。那么方法push将具有以下类型。push：Self×List（N×Self）List（N ×Self）显然，在这两种情况下，多项式函子都不成立。3.为了使示例保持在合理的大小内，我在这里只考虑push方法。在一个更现实的例子中，应该有更多的方法，例如改变一个缓冲器的下内容：3下一篇：·B2内容：5下一篇：·特维斯321×⇒列表×2预赛本节介绍了本文的一些标准和一些非标准符号。在整个论文中，我工作的范畴集的集合和total函数。我用×来表示笛卡尔积和投影Xπ1X ×Yπ2Y. 不相交的并集（上积）由+表示以及注射Xκ1X+ Yκ2Y。我把X和Y之间的函数空间（指数）写成XY。两个函数f：XY和g：YZ的合成为g<$f：YZ。X和Y之间的二元关系写为R<$X×Y={（x：X，y：Y）|R（x，y）}。 在任意集合A上的等式关系是Eq（A）={（a，a）|a∈A}。给出了关系（Ri）i ∈ Ii的统一非线性指数集当iR i={（x，y）|xR i y}。 对于关系R<$X×X，其定义域是predicateonX，definedasdo m（R）={x|x×. x Rx ×关系是部分自同构，如果它在其定义域上自同构，即如果xRy蕴涵xR x和yR y。关系R是部分等价关系，如果它是对称和传递的。包含R的最小部分等价关系记为R。取最小部分等价关系是一个闭包运算，特别是R=R，如果S是部分等价，则R<$S蕴涵R<$S关系。 关系R中的Z字形是一个有限序列x1，...，xn，使得x i R x i+1或x i+1R x i对所有i< n成立。闭包R可以描述如下：x Ry成立当且仅当存在Z字形x，...，y在R.Set中的carbohydrate封闭结构可以提升到如下关系设S<$U×V和R<$X×Y是关系：S×RR（U×X）×（V×Y）=S+RR（U+X）×（V+Y）=.Σ（（u，x），（v，y））|S（u，v）<$R（x，y）（κ1u，κ1v）|S（u，v）.Σ（κ2x，κ2y）|R（x，y）S<$RR < $（U<$X）×（V<$Y）=（f、g）|u：U，v：V. S（u，v）蕴含R（f（u），g（v））在 适 当 的 设 置 中 （ 见 [8] ） ， 运 算 R 、 +R 和 R 可 以 扩 展 到 Set 的carbohydrate闭结构上的firebred函子。这种结构对本文来说并不重要。然而，我确实使用了×R和+R在两个参数中都是单调的（相对于包含），并且在第一个参数中，R是反单调的，在第二个参数中是单调下面我使用函子List：SetSet将集合A映射到A上的有限列表集合。 从形式上讲，清单（A）是作为（的载体）获得的。函子FA（X）=A×X+1的初始代数。 态射部分List（f）是熟悉的映射函数：它将f应用于名单 我使用nil：List（A）和cons：A List（A）List（A）来表示List（A）上的初始代数。函子List也可以提升为关系。一般的理论是Σ..特维斯322⊆ × ⊆×⊆ × ⊆×112在[4]中描述。对于关系R X Y，提升RelList（R）List（X）List（Y）的特征如下：如果l1=nil，则为true;如果l2=nil，则RelList（R）（l1，l2）=R（x，y）<$RelList（R）（l×，l×）如果L1=cons（x，l1×）12l2= cons（y，l2×）我不知道你在说什么下面的引理描述了提升操作和取关系并之间的相互作用。Lemma2. 1Let（SiUV）i∈I和（RiXY）i∈I是关系的任意I-指数集。然后iRelList（Ri）RelList.ΣiRii（Si×RRi）i（Si+RRi）=iSi×RiSi+RiRiiRii（Eq（A）<$Ri）<$ Eq（A）<$RiR1很容易找到前面的子集关系的例子我艾玛很严格。此外，一般指数的两个表达式i（Si <$RR i）和i S1<$RiR1一般不相关。3广义多项式函子本文考虑集合的集合范畴和全函数范畴上的不同多项式函子类 这些函子被称为多项式，因为它们是由恒等式、常数、（余）积和指数归纳建立的。我区分了五类多项式函子。这些类之间唯一的区别是允许的指数类型。在下文中，A代表任意常数集。笛卡尔函数：K（X）=一|X|列表（K1（X）） |K1（X）×K2（X） | K1 (X)+ K2(X)多项式函子：F（X） = 一|X| List (F1 (X)) | F1 (X) × F2 (X)|F1（X）+F2（X） |1（X）扩展笛卡尔函子：H K（Y，X） = 一|X| List (H K (Y, X)) | H K (Y, X) × H K (Y, X)|特维斯323121H K（Y，X）+H K（Y，X） | K (Y ) ⇒ H K (Y, X)特维斯324112121函数类财产例如笛卡尔没有参数自我···多项式常数变元自我×A···扩展卡耳无函数参数Self×Self ×Self（Self+A）······扩张多项式功能常域变元自我×（A）自我···高阶多项式任意参数Self×（SelfA）自我×（自我×自我）······表1本文中的函子类扩展多项式函数：H F（Y，X）= A|X|列表（H F（Y，X））|H F（Y，X）×H F（Y，X）|H F（Y，X）+H F（Y，X）|F（Y）H F（Y，X）高阶多项式函数：H（Y，X）= 一|X|列表（H1（Y，X）） | H1 (Y, X) × H2 (Y, X)|H1（Y，X）+H2（Y，X） |H1（X，Y）→H2（Y，X）笛卡尔函子和多项式函子是内函子Set Set，所以它们只有一个参数。其他类描述了具有第一个逆变和第二个协变参数的双变当用于对共代数签名进行建模时，上述类对可以建模的方法类型有不同的限制示例见表1高阶多项式函子是上面定义的最一般的类本文不研究高阶多项式函子。然而，我用它们来给出适用于所有考虑的函子类的定义扩展多项式函子将子句中的表达式的域限制为多项式函子。扩展的Carnival函子需要域的Carnival函子对于多项式函子，指数的定义域必须是常数。与[14]相比，本文明确地允许函子List作为成分函子.文[14]的所有结果也适用于本文中更一般的函子类必要的证据在PVS里形式化。特维斯325×D为了与Poll和Zwanenburg在[10]中的结果相比较，我们注意到，每个给定X的dialga都对应于一个pairc，a≤，其中rc是某个扩张的Carnival函子的余代数，a是某个多项式函子F在F（X）中的常数. 有一些扩张的Carnival函子的余代数不能表示为双代数。例如函子G（Y，X）=（Y<$A）+（X× A）的余代数。定义3.1设H：SetopSet Set是一个高阶多项式函子。一个H-余代数是一个函数c：XH（X，X）.令d：YH（Y，Y）是另一个H -余代数.函数f：XY是一个H- 余 代 数 态 射 f ： c d ， 如 果 下 面 的 图 交 换 ：XcH（X，X）H（X，f）fH（X，Y）H（f，Y）YH（Y，Y）由于函子H保持合成和恒等式，因此上面定义了每个高阶多项式函子H的H-余代数（在集合中）的范畴CoAlg（H对于多项式和笛卡尔函子，前面的五边形坍缩为熟悉的正方形。例3.2要用引言中的指针来模拟缓冲器的签名，需要扩展多项式函子G缓冲（Y，X）=（I<$X）×（I +1）×. （NY+1）NX+1代替函数，可以使用N×Self上的（关联）列表来建模环境。然后，推送的类型发生变化，为了对签名进行建模，需要扩展的Carnival函子G×Buf（Y，X）=（I<$X）×（I+1）×. List（N×Y）List（N×X）文献中有两种方法来定义互模拟：要么是Aczel/Mendler风格[1]，要么是Hermida和Jacobs建议的关系提升[5]。对于本文的范围，定义互模拟的选择主要是一个品味问题，因为对于扩展多项式函子，两种方法都产生相同的互模拟概念[14]。 我更喜欢Hermida/Jacobs的方法。定义3.3设S<$V×Y和R<$U×X是两个关系，H是一个高阶多项式函子。它的关系提升Rel（H）（S，R）<$H（V，U）×特维斯3261221H（Y，X）是通过归纳H的结构而定义的（关于运算符×R、+R、R +R和RelList的描述，请参见第6H=A：Rel（H）（S，R） =Eq（A） ={（a，a）|a ∈ A}H=ID：Rel（H）（S，R）=RH=列表（H1）：Rel（H）（S，R）=RelList（Rel（H1）（S，R））H=H1×H2：Rel（H）（S，R）=Rel（H1）（S，R）×RRel（H2）（S，R）H=H1+H2：Rel（H）（S，R）=Rel（H1）（S，R）+RRel（H2）（S，R）H=H1H2：Rel（H）（S，R）=Rel（H1）（R，S）<$RRel（H2）（S，R）在前面的定义中，高阶多项式函子的关系提升需要一个逆变和协变的自变量关系。对于卡方函子和多项式函子，从不使用逆变参数。对于这些函子，我放弃了逆变参数，并将它们的关系提升写为Rel（F）（R）定义3.4设c：XH（X，X）和d：YH（Y，Y）是高阶多项式函子H的两个共轭环。关系R<$X×Y是c和d的HR（x，y）蕴涵Rel（H）（R，R）（c（x），d（y））注意，R是Rel（H×）（R，R）对于c和d的二次近似计算，H×（Y，X）=Y<$H（Y，X）.本文只考虑一个余代数上的互模拟R<$X×X。这样的互模拟R称为（部分）互模拟等价如果R是（部分）等价关系。请注意，前面的定义并不要求这种互模拟是自反的或传递的（正如人们对行为平等的体面概念所期望的那样 对于多项式函子的余代数，这不是一个问题，因为可以证明每个互模拟都包含在某个互模拟等价中[13]。然而，一旦存在二进制方法，这就失败了。例3.5这个例子显示了两个互模拟，使得它们的并集不是互模拟。考虑扩展的Caribbean函子G（Y，X）=Ybool，它对应于只有一种方法相等的余代数签名。取集合A={a1，a2}作为状态空间，定义一个G-余代数c如下。c（x）（y） =if x=ythen true else false endifRd=ef{（a， a），（a， a）}的第n个关系是对c和s的一个二次模拟等式（A）。然而，它们的结合不是互模拟。这里的问题是对于互模拟R，沿着“如果a1在行为上与a2不可区分，则c（a1）（a1）与c（a1）（a2）不可区分”的非正式推理✷特维斯327⊆×⊆ × ⊆×. Σ∈×4最大互模拟等价例3.5表明，定义3.4中的直接推广产生了一个太弱的互模拟概念。一个明显的解决方案是只考虑具有附加属性的互模拟。例如，[14]中的命题4.4证明了自反互模拟形成了扩张多项式函子的余代数的（不完全）格。在本节中，我考虑部分互模拟等价。它们使得Poll和Zwanenburg在[10]中关于存在最大互模拟等价的结果成为可能。下面所有的引理都指向定理4.6. 它们之间的相互作用在引理4.5的证明中变得很清楚。我从三个简单的观察开始开发，这些观察处理下面的副作用引理4.1(i) 多项式函子的关系提升保持部分自反关系。 也就是说，如果R XX是部分反应的，那么Rel（F）（R）也是部分反应的。 对于所有多项式函子F.(ii) 高阶多项式函子的关系提升保持部分等价关系。 也就是说，如果 SYY和RXX是部分等价关系，那么Rel（H）（S，R）对任意高阶多项式函子H也是部分等价关系.(iii) 多项式函子的关系提升保持了“具有相同域”的性质。精确地说，设R1，R2<$X×X是满足dom（R1）=dom（R2）的关系.如果R1和R2是部分反应性的，则dom（Rel（F）（R1））=dom（Rel（F）（R2））对于所有多项式函子F.证据用归纳法对函子的结构进行了研究。诱导步骤已在PVS中正式化。✷引理4.2设S<$Y×Y和R<$X×X是部分自反关系。S+RR=S+RR（1）S×RR=S×RR（2）RelList（R）= RelListR（3）证据 这个引理已经在pvs中得到了证明。从左到右的包含在所有情况下都是微不足道的对于另一个方向，必须构造合适的标记。对于整数，对于（2），let（（y，x），（y×，x×））SRR，soy， . . . ，y×和x， . . ，x×在S和R中是Z形的，是对称的。 n（y，x）， . . ，（y×，x）， . . . ，（y×，x×）是S×RR中的Z字形，因为R和S是部分自反的.✷对于指数的情况，可以导出S<$RR<$S<$RR成立，如果S特维斯328⇒ ⊆⇒⊆ × ⊆×部分自反，R是对称的。 而SRRSRR要求R是部分等价关系。然而，这些更强的假设并没有在我使用前面引理的上下文中给出引理4.3设Si YY和Ri X X是任意指标集I的两个部分自反关系的指标族。假设所有的R i和所有的S i都有两两相等的域。然后i（Si+Ri）=（iSi）+R（iRi）（1）i（S i×R i）=（iSi）×R（iRi）（2）iRelList（Ri）= RelList（iRi）（3）证据 等式（1）以及等式（2）和（3）中从左到右的包含，将等式（1）和等式（2）中从左到右的包含从等式（2）和等式（3）中的从左到右的包含。1 .一、 对于（2），它仍然是一个问题，（iSi）×R（iRi）<$i（Si×RRi）. SoassumeySiy×andxRjx×forsomei，j∈I，序列e（y，x），（y×，x），（y×，x×）在i（Si×RRi）中 是azigzag（3）一个是（iRi）i RelList（R i）通过列表上的归纳。✷4.我的朋友4LetK是一个广义函数，（Ri）i∈I是一个具有两两相等定义域的部分等价关系的集合. 然后Rel（K）（iRi）=iRel（K）（Ri）证据 通过对K的结构的归纳来进行证明。让我们来演示一下K=List（K1）的情况：.- 是的ΣRel（列表（K1））iRi10） A = 0（.iRi）= RelListΣiRel（K1）（Ri）在Ind. 嗨.Σ=RelListiRel（K1）（Ri）4.2（3）=i RelList（Rel（K1）（Ri））乘以4.3（3）=iRel（List（K1））（Ri）边条件与前面的引理一起解除。✷前一命题的重要部分是来自左为右：假设一个新的向量为pair（t， t×）∈Rel（K）（iRi），则新的向量为这是一个非常有趣的事情，这是一个ZIG ZAGT， . . ， t×iniRel（K）（Ri）.引理4.5设G是一个扩张的Carnival函子，（Si）<$Y×Y和（Ri）<$X×X是两个由任意集合I指标的部分等价关系族.假设所有的Si和所有的Ri都有两两相等的整环。设（s，r）∈ Rel（G）（Sj，Rj），其中j∈I.如果对所有的i∈Ib，h（r，r）∈R el（G）（Si，Ri）和（s，s）∈R el（G）（Si，Ri），我们有另外的（s，r）∈ Rel（G）（i Si，i Ri）.特维斯329证据通过对G. 所有诱导步骤已在PVS中正式确定。让我们演示一下G（Y，X）=特维斯330K（Y）<$G1（Y，X）.从假设可以得出，s和r是函数，使得存在j∈I，a，b ∈ K（Y）.Rel（K）（Sj）（a，b）蕴涵Rel（G1）（Sj，Rj）（sa，rb）（1），且对所有i∈ Ia，b ∈ K（Y）.Rel（K）（Si）（a，b）蕴含Rel（G1）（Si，Ri）（sa，Sb）（2）a，b ∈ K（Y）.Rel（K）（Si）（a，b）蕴含Rel（G1）（Si，Ri）（r a，r b）（3）它仍然表明，对于所有的a，b∈K（Y）：Rel（K）（iSi）（a，b）蕴涵Rel（G1）（iSi，iRi）（s a，r b）（1）A（1）A（2）A（iS i），根据命题4.4，有一个Z字形a，.，bini Rel（K）（Si）. 现在我们可以建立一个序列，... 、s b、r b和invokeG1在每两个相邻元素上的归纳假设表明，在Rel（G1）中，它是一个Z字形（iSi，iRi）。 这就完成了证明，因为后者是由引理4.1（ii）的部分等价关系。的假设归纳假设需要一些注意，但它们可以用前面的引理和假设（1）-（3）来排除。✷定理4.6设c：XG（X，X）是扩张Carnival函子G的余代数. c在固定区域上的部分互模拟等价构成了一个完备的格. 在这个格中，互模拟族（Ri）的连接是由iR i给出。特 别 地，iR i是对任意族（R i）的互模拟，互模拟等价证据 证明了对于任意的指数族（R i），在同一域上的部分互模拟等价关系iRi是a互模拟 若Ri是c的互模拟，则（c，c）∈Rel（X<$G）（Ri，Ri）.我不想让他们知道。5.在C_i（R_i）和P_ir（c，c）中，要求（c，c）∈ Rel（X<$G）（i R i，i R i）.✷前面的结果应用于Ex示例3.2中的函数G × B u f。 因此，如果一个模型的环境中的关联列表，那么最大互模拟等价的所有模型都存在。最大的互模拟等价可以用来，例如，在像CCSL[12]这样的规范语言中定义行为平等。例4.7这个例子给出了一个扩张多项式函子的余代数，对于这个扩张多项式函子，存在一个无限上升的互模拟等价链，没有上限。 因此，如果不作进一步的假设，前面的定理就不能推广。 考虑扩展多项式函子G（Y，X）d=ef（NY）阿博布尔特维斯331∈×⊆×∈×对于关系R<$U×V，两个函数a：NU和b：NV是RG的关系提升是.ΣRel（G）（R，S）=（f、g）|对于所有R相关函数a和b：fa = gb下面我定义一个G所以c的第二个参数是函数NN.关系RN N是c的互模拟，如果对所有x，yN，其中xRy和所有R相关函数f和g，我称一个函数N为有界的，如果存在一个自然数n，使得对所有i，N，<主要的一点是，对于全关系N N，存在函数对f，g：N N，使得f和g是N-相关的，并且f是有界的，而g是无界的。余代数c现在被定义为.c（x）（f）=真f有界否则为falsec的构造确保了全关系N×N不是c的互模拟。现在考虑由下式定义的部分等价关系族（Sn）n∈Ni Snj当且仅当i=j或 （injn）对于任何一个Sn和两个函数f和g，以下成立：如果f和g是Sn相关的，那么当g是时，f是精确有界的。因此所有Sn都是互模拟等价。此外，任何有限的关系集Sn都有一个上界，这是c的互模拟（参见[14]中的命题4.4）。所有Sn的最小上界是全关系，因此不存在最大互模拟等价。✷5基于代数的余代数本节通过排除例4.7中的余代数改进了定理4.6。主要思想并不十分困难。然而，为所有扩展多项式函子设置东西有点因此，让我首先讨论定理4.6和例4.7的证明。 这将（希望）给一些直觉，有助于保持在以下方向。定理4.6被限制到扩展的Carnival函子，原因如下：在引理4.5的证明中，指数的归纳步骤需要命题4.4，它只对Carnival函子成立。反过来，命题4.4被限制为Carnival函子，因为存在以下子集关系是严格的情况Eq（A）<$RiRi <$i（Eq（A）<$RRi）（†）例4.7的余代数利用了这样一种情况（假设A=N在（t））中：对于两个函数f，g：N N，其中f是有界的，而g是非有界的。有界我们有（f，g）∈Eq（N）<$RnSnbut（f，g）∈/n（Eq（N）<$RSn）。特维斯332{1}|}†{|}例4.7中的余代数c足够复杂，可以在输入f和g上给出不同的观测值。推广定理4.6的主要思想是给出一个条件，排除那些利用（†）中子集关系的余代数，其方法与例4相同。7. 由于下面将变得清楚的原因，我说满足这个条件的余代数是有限基的。发展的第一步是更好地理解（†）中的子集关系引理5.1设（Ri）X×X是部分自反关系的I -指标集.假设I是非空的，并且所有的R i都有两两相等的整环。考虑两个函数f，g：A X。如果f和g仅对有许多论点（即，如果a fa= g a是有限的），则它成立，.Σ（f，g）∈ Eq（A）<$RiRi蕴涵（f，g）∈i（Eq（A）<$Ri）证据 这个证明是在pvs中完成的。 它通过对集合{a|fa=g a}。 在基本情况下（其中f=g），e必须证明在i∈I的条件下，证明了（fa）Ri（fa）.这是因为所有的Ri都是上的部分自反关系。相同的域。对于归纳步骤，假设集合{a|fa_n =g_a}有n +1个元素。从这一点和等式fa0（ag0）中可以看出，一个零表示hg（a0）在一个零处的函数更新日期。 函数fa0（ag0）和g方向的位置由感应产生，从fa0（ag0）到gini（Eq（A）<$Ri）.从这些假设中，我们可以得到一个从fa0到g a0。 这两个双标记可以连接在一起，形成一个从f到g的之字形，i（Eq（A）<$R i）。✷前面的结果表明，对于例4.7，应用c（x）（f）的结果依赖于f的无穷多个映射是必不可少的。为了便于讨论，假设在例4.7的上下文中，我们给出一个可计算的G-余代数d：N（NN）布尔。如果d是可计算的，那么在应用程序d（x）（f）中，余代数d可以它的函数参数f只对有限个参数有效。回顾临界子集关系（†），假设我们有一对函数（f，g）包含在左边。因为假设余代数d有了前面的引理，我们现在可以得出结论，对（d（x）（f），d（x）（g））也包含在（）的右边。因此，对于假设的余代数d，存在最大互模拟等价。为了形式化前一段的思想，对于所有扩张多项式函子的余代数d传递给f的参数集（对于特定的x和特定的f）是特维斯333∈∈称为参数描述符。这样一个描述符D告诉我们如何在余代数d不能检测到变化的情况下改变自变量f。余代数d不能与f区分的所有自变量f×的集合是f关于描述子D的环境。余代数d具有这样的性质，即对于每个x和每个f都存在一个有限的参数描述符，它被称为是有限基的。在下文中，我将这些概念形式化为任意扩展的多项式函子。在这些定义中，有趣的情况总是关于指数的情况（余）积和列表的情况 在发展的最后，我证明了有限基的扩张多项式函子的余代数的最大互模拟等价确实存在。定理4.6将作为一个推论再次出现：Carnival函子的描述子集将是平凡的，并且所有扩展Carnival函子的余代数都是有限基的。定义5.2[参数描述符]设F是多项式函子。F的参数描述符集合，用descF表示，通过对F的结构的归纳来定义：descA=1={}描述ID=1descList（F1） =List（descF1）descF1+F2=descF1×descF2descF1×F2=descF1×descF2descA<$F1={R<$A×descF1|a Rb1<$a Rb2隐含sb1=b2}描述符DdescF是描述可以传递到F（X）的元素中的可能参数的结构。如果F是一个Carnival函子，那么因此，descK对于Carnival函子K是平凡的。实际上，集合descK对于不包含List作为成分函子的Cars函子同构于1如果F（X）=List（F1（X））a描述符D∈descF包含列表l∈F（X）中每个元素的描述符如果与列表l结合使用的描述符D为至少和我一样长。然而，技术上更容易让下面的定义适应D比l短的情况。在F（X）=A<$F1（X）的情况下，描述符D∈descF包含一组可以传递给fF（X）的参数。 对于每个这样的参数a，描述符D精确地包含f（x）的一个（子集合descA×B<$F和descA<$B<$F并不像人们所期望的那样同构然而，如果将descA<$B<$F限制为R∈descB<$F非空的那些对（a，R），则它们是同构的一个参数描述符D是遗传有限的，如果D本身是有限的，如果D的所有元素都是遗传有限的。所有的Carnival函子的描述符都是遗传有限的。特维斯334∈∈⊆∈∈我我F一IDenvD（x） F（X）F1×F2F1+F2{x}{x}envπ1D（π1x）如果x=κ1x1：×envπ2D（π2x）{κ1x×1|envπ1D（x×1）}{κ x |env（x）2×π D×222 }如果x=nil：.{nil}列表（F1）如果x=cons（a，x×）Σ1D=cons（A，D×）{cons（a2，yx）|a2∈envA（a1）如果D=零：{y|长度x =长度y}n∈env（x）×D×J}A组F1{y|n（a，D×）∈D . ya∈envDJ（xa）}对于一个固定的多项式函子F，一个参数描述符DdescF会对每个元素x F（X）产生一个环境4envD（x）F（X这个环境包含所有那些元素y F（X），当评估被限制在参数描述符D中包含的内容时，这些元素不能与x区分开。定义5.3[关于参数描述符的环境]设F是多项式函子，D是descF中的参数描述符。对于元素x F（X），x相对于D的环境用envD（x）表示，并通过对F的结构的归纳来定义：对于每个x和D，我们有x∈envD（x）。进一步地，对于所有的Cars函子K和所有的元素x∈K（X），存在一个（遗传有限的）描述子D∈descK使得envD（x）={x}。现在可以对多项式函子用公式表示命题4.4的特殊推广。命题5.4设（Ri）<$X×X是一个非空指标集I的I-指标部分自同构关系族.假设所有的R i都有两两相等的域。则对x，y∈F（X）和所有遗传有限描述子D∈descFthe reexist tsx×∈envD（x）使得.Σ（x，y）∈Rel（F）iR蕴涵（x×，y）∈Rel（F）（Ri）证据通过对F的结构的归纳来进行证明。乘积、副积和列表的归纳步骤类似于命题的证明4这里没有拓扑学的联系。特维斯335∈第4.4节。指数的归纳步骤依赖于引理5.1。所有诱导步骤已在PVS中正式确定。✷定义5.5设G是一个扩展多项式函子。有限基的性质是G（Y，X）上的谓词。它是由G的结构上的归纳法定义的。一个元素x G（Y，X）是无限基的，当且仅当：• G（Y，X）=X：所有x∈G（Y，X）都是有限基的。• G（Y，X）=A：所有x∈G（Y，X）都是有限基的。• G（Y，X）=List（G1（Y，X））：列表x的所有元素都是无限基的。• G（Y，X）=G1（Y，X）×G2（Y，X）：如果π1x和π2x都是有限基的。• G（Y，X）=G1（Y，X）+G2（Y，X）：如果x=κ1x1，则x1必须是无限基的;第二次注入也是如此。• G（Y，X）=F（Y）<$G1（Y，X）：对所有的a∈F（Y），结果x（a）是有限基的，进而存在一个遗传有限数D∈descF，使得a×∈envD（a）. xa=xa×。一个G 如果对于每个可以传递到c的可能参数a，存在一个遗传有限参数描述符D，使得c无法区分a和来自a的环境的元素，那么情况就是这样。基本上，这意味着，c只检查对于类型对应于Carnival函子的参数没有限制，因为对于Carnival函子，每个参数描述符都是遗传有限的。 因此，扩张Carnival函子的余代数总是有限基的。一般来说，如果一个给定的余代数是有限基的，则它是不可判定的。下面的结果是引理4.5的推广。引理5.6设G是扩张多项式函子，（Si）<$Y×Y和（Ri）<$X×X是两个I-指标的部分等价关系族.假设I是非空的，并且所有的Si和所有的Ri都有两两相等的整环。设（s，r）∈ Rel（G）（Sj，Rj），其中j∈I，并假定s是有限基的.如果我们另外有，对于所有i∈I，（r，r）∈ Rel（G）（Si，Ri）和（s，s）∈ Rel（G）（Si，Ri），那么我们也有（s，r）∈ Rel（G）（i Si， i Ri）.证据 这个证明几乎与引理4.5的证明相同，只是在指数的归纳步骤上有一点变化。对于所有的a，b∈F（Y），必须证明以下含义Rel（F）（iSi）（a，b）蕴涵Rel（G1）（iSi，iRi）（sa，r b）（1）A（1）A（2）B（3）A（iSi）。 因为s是基于那里的存在一个遗传有限描述子D∈descF。 提案5.4特维斯336其中x是tsa×∈envD（a），其中hs a=sa×suchat（a×，b）∈Rel（F）（S）。没有我这个论证在引理4.5的证明中继续进行。✷定理5.7设c：XG（X，X）是扩张多项式函子G的余代数.如果c是有限基的，则c在固定域上的部分互模拟等价形式a 完全晶格 一个家庭（R i）的加入在这个格子中的互模拟是iRi。证据应用引理5.6，如定理4.6的证明。✷例5.8考虑一个余代数c：X GBuf（X，X）作为带指针的缓冲器的例