多类余代数模态逻辑及其应用

54网址：http://www.elsevier.nl/locate/entcs/volume65.html17页多类余代数模态逻辑的CorinaC^rstea1;2英国牛津大学计算机摘要[4]描述了集合上某些多项式内函子的余代数的模态逻辑。这种逻辑在这里推广到endofunctors类别的排序集。的结构考虑endofunctors然后利用，以DENE的方式移动（余代数）一个endofunctor（余代数）另一个，并配备它们与相关的模态语言之间的翻译。此外，所得到的翻译是保持和反映的余代数的模态公式的满足。1引言在基于状态的动态系统建模中使用共代数[9]，将转移系统用作过程的操作模型[8]，互模拟的概念在共代数方法中发挥着重要作用各种模态逻辑可以用来推理共代数结构[6，5，7，4]，就像标准模态逻辑可以用来推理变迁系统结构一样（见例[3]）。这些逻辑捕获互模拟，因为状态的逻辑等价与互模拟关系一致。然而，这些逻辑依赖于特定的endofunctors用于定义感兴趣的共代数结构，不同的，但相关的endo- functors产生不同的，但尚未正式相关的模态逻辑。本文的目的是提供一个（制度）框架，将模态逻辑与特定的一类内函子（即[4]中考虑的那些）联系起来。（类似的，但更抽象的这样的框架在[1，第2节]中描述。这里介绍的框架符合[1]中的框架。）1牛津大学圣约翰学院支持的研究2电子邮件：corina. comlab.ox.ac.ukc2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。55[4]（也见[7]）描述了（nite）Kripke多项式内函子的余代数的模态逻辑，即，集合上的内函子由常数和单位函子使用乘积、余积、具有常数指数的指数和（nite）幂集构造而成。[4]中的方法在这里被进一步采用，一方面通过将其推广到有序集范畴上的内函子，另一方面通过提供对模规范的前面提到的概括在存在不止一种感兴趣的类型的情况下是有用的在定义了Kripke多项式内函子及其相关逻辑之后，利用由这种内函子结构引起的自然变换，定义了从一个Kripke多项式内函子到另一个Kripke多项式内函子的新方法.这样的自然转换导致函子之间的范畴的余代数相关联的域和各自的余域，以及翻译之间的模态语言相关联的余域和各自的域。此外，沿着这些自然变换，余代数对模态公式的满足被保持和反映。也就是说，由此产生的框架具有作为一个机构的属性[2]。这个机构的态射捕获了余代数类型之间的关系和封装关系，如几个例子所示前面提到的满足关系的性质允许规范及其逻辑后果在余代数类型之间沿着态射进行。本文件的结构如下。第2节将[4]中的方法推广到有序集范畴上的内函子。第三节定义了从一个内函子转移到另一个内函子的方法，这些方法保持和反映了余代数对模态公式的满足。第4节总结了结果。2排序集范畴上Kripke多项式尾函子的余代数模态逻辑本节将[4]中介绍的共代数模态逻辑推广到有序集范畴上的内函子。为了便于在下一节中定义模化规范框架，这种内函子的组成部分被视为一个范畴的对象，该范畴的箭头自然地从函子的结构中产生，捕获共代数类型之间的语义依赖。定义2.1设S表示一个集合（类）3.集S上的Kripke多项式函子范畴记为KPS，是KPS的最小子范畴。3给定一个集合S，S-序集和S-序映射的范畴Set S有对象由族A=（As）s2S给出，其中As2jSetjfors2S，而从A到B的映射由族（fs）s2S给出，其中（fs：As！ Bs）2k设k为s2S。5621我12我[SetS; Sett]表示：KPS包括[SetS;Set]的子范畴，其子范畴是常数函数，第十章D对于X2j集合Sj，其中D2j集合j是有限的且非空的，并且他们的箭头是自然变化D=0，则（D！D0）2k集合k，并且具有D和 D0 nite和非空;j KP S j包含投影函子s：Set S！集合（将S-排序的集合/函数带到它们的S-分量），对于s2S;KPS在二元积和余积下是闭的;KPS在FD型指数下是闭的，其中D2jKPSj是常数函子;KPS在幂集下是封闭的;包含形式d的所有自然变换：F）D（其每个分量是产生d作为结果的常数函数），其中F;D2jKPSj，D是常数函子，d2D4.注2.2将定义2.1中幂集下的闭包替换为nite幂集下的闭包，得到集合S上的nite Kripke多项式函数的概念。本文的所有结果都是针对Kripke多项式函子的，然而，它们也适用于nite Kripke多项式函子。注2.3KPS定义的直接结果是在这一范畴中存在以下形式的箭头：i：F1F2）Fi，其中i2f1;2g，其中verFi2jKPSj，i=1;2h 1; 2i：F）F 1F 2，当（i：F）F i）2k KP Sk，i = 1;2i：Fi）F1+F2，其中i2f1;2g，当i=1;2时，v erFi2jKPSj[1;2]：F1+F2）F，当（i：Fi）F）2kKPSk， i=1;2：F0）FDwhenever（：F0D）F）2k KPSk其中 D是常数函子evalF;D： FDD） F，当 F;D2 j KPSj，其中 D是常数函子时P（）：P（F））P（F0）当（：F）F0）2kKPSk满足下列等式时：（一）ih1;2i= i=1;2（二）[1; 2] i=1;2（iii）eval F;D（1 D）=特别地，KPS包含以下形式的箭头：1第二名：F1F2） F0F0（由h1<$1;2<$2i给出）每当（i：Fi）F0）2kKPSk，对于i= 1;21+2：F1+ F2） F0+F0 （由[1<$1;2<$2]给出）无论何时（i：Fi）F0）2kKPSk，对于i= 1;24在处理指数时，需要这些自然变换。D//57F;D当D为常数函子时，D：F 0 D）F D（由（k-eval 0）给出）为（：F 0）F）2kKP k和D 2 jKP S jF：FD）FD（givenbyy（evalF;D0 （1FD 0） 当verF2jKPSj和（：D）D 0）2kKPSk，其中D; D 0为常数函子.Kripke多项式内函子的概念（见[4]）现在推广到排序集的范畴如下。定义2.4设S表示一个集合（类）。集合S上的Kripke多项式内函子是一个内函子T：集合S！设置S使得对于每个s 2 S，范畴KP1的对象，其中1表示一个单元素集合，正是[4]中定义的Kripke多项式内函子（也见[7]）。[4]还定义了一个范畴，记为KPF，其对象是集合上的Kripke多项式内函子，其箭头是这些内函子之间的路径，从F到F0的路径对应于F0用于F的定义（或作为F的成分）。虽然范畴KPF中的箭头捕获Set上的Kripke多项式内函子之间的结构依赖性，但范畴KP1（并且实际上，对于任意S，KPS）中的箭头捕获Kripke多项式内函子（的分量）之间的语义依赖性，因为可以从对应于它们的域5的余代数中提取对应于它们的余域的余代数。 前一类用于[4]在Kripke多项式内函子上定义了一些模态公式（通过结构归纳）。下一个定义将[4]中引入的模态公式的概念推广到排序集上的Kripke多项式内函子将其实例化为Set上的Kripke多项式内函子，得到与[4]中的定义等价的定义，但它没有使用成分函子的概念。定 义 2.5 设 T ： 设 S！ 集 合 S 表 示 Kripke 多 项 式 内 函 子 。 对 于F2jKPSj，T上F型模态公式的集合Form T（F）（根据F的结构）归纳地定义如下：什么？2表格T（F）（'！如果2FmT（F）和2FmT（F）d2表格T（D）如果 d2 Dnexts'2 FormT（s）if'2 FormT（ Ts），with s2 S[i]'2FormT（F1F2）if'2FormT（Fi），其中i2f1;2g[i]'2FormT（F1+F2）if'2FormT（Fi），其中i2f1;2g[ev（d）]'2FormT（FD）ifd2Dand'2FormT（F）[P]'2For mT（P（F））if' 2For mT（F）.5这一观察将在第3节中加以利用，以获得一个多排序余代数模态逻辑的机构。058FJKFFFFDFDFP（F）FFFF对于s2 S，T上s型状态公式的集合SForm（T）s由Form T（s）给出.注2.6如果T是集合上的闭函子，F是T的成分（见[4]），则T上F型的模态公式与[4]中定义的F类模态公式本质上相同（w.r.t.T）6.我们感兴趣的公式是状态公式，上面定义为投影类型的公式（即s与s2S）。这些公式涉及余代数的状态，并且被解释为余代数的载体这些解释的定义遵循相应组成部分的结构（即：Ts）。定义2.7设T：设S！ 集合S表示Kripke多项式内函子，设h C; i表示T-余代数.对于F 2 j KP Sj， 的解释JK2模态公式的P（（F）在余代数hC中， i是归纳地定义（在'和F的结构上）如下：J？J？K=;J'！K=[J K（其中，对于X2 P（ FC）， X由 FCn X给出）JdK= fdg for d2 DJnext'K=1（J'K）与s2 SsssT sJ[]'K=1（J'K），其中i2f1;2giF1 F2i FiJ[]'K=（J'K）[（FC），其中i2f1;2g且fjg=f1;2g nfigiF1+F2iFij jJ[e v（d）]'K =ff：D！FCjf（d）2J'Kg ford2DJ[P]'K=P（J'K）一个元素c2 FC被称为满足一个模态公式“2FormT（ F）”（写作cj='）当且仅当c2J'K. 此外，余代数hC;i被称为满足mula'（记为hC;ij='）的模当且仅当J'K=FC。 在特别地，给定s2S，称元素c2Cs满足状态公式'2形式（）当且仅当c2J'K，而余代数hC; i被称为T SS当且仅当J'K'=C s.注2.8上述定义将[4]中的一个类似定义推广到排序集上的Kripke多项式内函子。注2.9定义2.7的结果如下：J>K=C，J：“K= ，J”_K=J“K[J K]和J”_K=J“K\JK，其中，F F F F F：'、'_和'^是由y给出的吗？ ！什么？、、怎么样？ ！'，：'！并保留：（'！ ：）的情况。定义2.10设T：设S！集合S表示一个Kripke多项式内函子，设F2jKPSj。模态公式';2形式T（F）称为：6在[4]中定义的模态逻辑也被定性为多排序的。然而，在[4]中，排序用于指代集合上的内函子的成分，而在这里，多排序是基础类别的一个特征，其中排序用于表示感兴趣的类型。JKF59F1+F2F1F1F1+F2语义等价nt（写为“）当且仅当J'K=JK，对于nybe说ab出对[i]'和hii'，分别是[P]'和hPi'，如，F FT-余代数h C; i.注2.11对于Kripke多项式闭函子T：集合S！集合S，也可以定义ne：hnextsi'：：=： nexts：'2FormT（s）for'2FormT（Ts）withs2Shii'：：=：[i]：'2FormT（F1F2）for'2FormT（Fi）withi2f1;2ghii'：：=：[i]：'2FormT（F1+F2）对于'2FormT（Fi），其中hi2f1;2ghev（d）i'：：=：[ev（d）]：'2FormT（FD）对于d2D和'2FormT（F）hPi'：：=：[P]：'2FormT（P（F））for'2FormT（F）（上述算子是[7]中算子到有序集范畴的推广。然后，定义2.7的直接结果是，用于mulaenexts'和hnextsi'、[i]'和hii'以及分别地[ev（d）]'和hev（d）i'的模态对是语义上等价的。同样的，但是，不能例如，J[1]′K=1（J′K）[2（F2C）%1（J′K）=Jh1i′K，而J[P]′K=P（J′K）6=fXFCj X|J′K6=; g=Jh Pi′K。P（F）F FP（F）例 2.12使用内函子 T TS： Set指定未标记的跃迁系统！由T TS= P（Id）给出。例2.13给定A 2 j Set j，A-标号迁移系统用闭函子T LTS：Set！由TLTS= P（A Id）给出。例2.14用闭函子T FTS：Set指定nite深度的未标记跃迁系统！由TFTS= P（ Id）N以及模态公式给出下一页[2]0$下一页[1][P]？next[2]（ n+ 1）$ next[1]（hPi next[2] n^[P] next[2]（0_：_n））; n2N将next[1][P]重命名为[succ]，将next[1][P]重命名为，将next[2]重命名为[depth]，并使用next [1]在^w.r. t上的分布性。语义等价7，我们得到了nite深度的未标号转移系统的以下等价说明：[depth] 0 $[succ]？[depth]（n+ 1）$[depth] n^[succ][depth]（0_：_ n）;n2N其中：cj=[succ]'，（8c0）（c02<$cC（c））c0j='）cj='，（9c0）（c02<$cC（c）andc0j='）cj=[深度]'N ，（8n）（depthC（c）=n）nj='N）7next和[1]在^上的分配性是[4，引理3.3和4.3]的结果，但也直接从定义2.7和注释2.9得出。60对任意的T-FTS-余代数C=hC; hsuccC;深度Cii和任意的c2C.因此，上面的公式形式化了这样的陈述，即当有根转移系统的根没有后继时，有根转移系统精确地具有深度0，并且当有根转移系统的根具有深度n的后继时，有根转移系统精确地具有深度n+1，并且它的任何后继的深度不超过n。例2.15元素属于集合E的列表使用内函子T LIST：Set！由TLIST=（1+E）（1 + Id）给出的集合（其中1表示一个元素集），连同模态公式：下一页[1]h1i>$下一页[2]h1i>在将next[1]h1i和 next[2]h1i分别重命名为和之后，，上述模态公式变为：>$ tailF>>其中：cj=1，（9s）（headC（c）=1（s）andsj=“1”）cj=1，（9s）（tailC（c）=1（s）andsj=“1”）对任意T_LIST-余代数C= hC; h头C;尾C_ii和任意c~ 2C.因此，列表的指定形式化了列表没有头的观察，当且仅当它没有尾。第三章共代数模态逻辑的范畴KPS的箭头捕获了克里普克多项式内函子（的分量）之间的语义依赖性。在下文中，这样的箭头将被用来定义从一个Kripke多项式内函子移动到另一个内函子的新方法，这些内函子保持并反映了余代数对模态公式的满足。这种方法提供了对模块化规范的支持，因为它允许规范及其（全局）语义结果从不太复杂的共代数类型转移到更复杂的类型。例如，这将使我们能够得到一个标记的过渡系统的规范，通过简单地转换未标记跃迁例2.14中的nite深度系统沿着一个自然的转换，给类型结构添加标签。此外，以前证明的关于未标记的夜晚深度转换系统的任何内容在转换为标记的夜晚深度转换系统时仍然是正确的。（相关的）余代数类型的集合使用多排序的余签名来指定，而从一个这样的集合移动到另一个（更大或更多的集合）的方式使用多排序的余签名态射来指定定义3.1多排序的共同签名是一个元组（S; T），其中S是一个集合，T：Set S！设S为Kripke多项式闭函子。 一个多分类的61f（s）0 080op0从（S;T）到（S0;T0）的余签名态射是上图e（f;），其中hf：S！S0和：UT0）TU，例如，S2kKPS0 k为ea chs2S。（这里U：SetS0 ！ Se tS表示将S 0-排序集/函数带到S-排序集/函数的函子，S-排序集/函数的s-分量由所讨论的S 0-排序集/函数的f（s）-分量给出，对于s 2 S。多排序余签名和多排序余签名态射的范畴记为Cosign。注3.2闭函子U：SetS0 ！SetSsatis esU=为每个sf（ s）s2S。因此，自然变换s的形式为s：T0）TsU，对于每个s2S。任意排序的余签名态射（f;）：（S;T）！ （S 0;T0）引入函子U：Coal g（T0）！ Coalg（T），其中U取一个T0-余代数hC 0;0i到T-余代数hUC;C0<$Ui. 这将产生一个函子Coalg：Cosign！ Cat，取一个多排序余签名为其余代数范畴，取一个多排序余签名态射为其诱导约化函子。我们将在下文中证明，多排序余签名态射也诱导其定义域上的状态公式到其余域上的状态公式的平移这种平移的定义反映了Kripke多项式内函子上的状态公式的定义：与定义Kripke多项式内函子T上的状态公式一样，首先定义T上任意类型F的模态公式，然后用s来表示F，定义T上状态公式沿着许多排序的余签名态射：（S;T）的平移！（S 0;T0）将需要定义翻译（w.r.t. T上任意类型F的模态公式沿任意自然变换：F 0）FU的），然后实例化其中1f（s）：f（s））sU。 一般来说，所产生的翻译不仅取决于自然转换， 同时也影响了转型因此，随着身份的自然转换，不会让模态公式保持不变，除非基础本身就是一种身份的自然转换。此外，形式=1f（s）的恒等自然变换 将在确定上述翻译中发挥至关重要的作用;正是这些自然的转换，将最终确保从T上的模态公式转移到T 0上的模态公式。对于一个特定的自然转换，翻译的定义沿（w.r.t.）a xed）是由确保公式的解释在翻译过程中被保留的需要驱动的。翻译的这一性质将使我们能够证明，在我们的框架中，约束的确定条件成立。定义3.3设（f;）：（S;T）！ （S0;T0）表示一个多序余符号态射. F或F2jKPSj、F2jKPS0j和（：F）FU）2kK PS0k，8注意F2jKPSj意味着FU2jKPS0j. 这从sU=f（s）得出，对于s2S（参见注3.2）。62/打开/关闭（1DU）/打开/关闭（1个后续行动）/打开/关闭（1个P（FU））（1个后续行动）/打开/关闭/打开/关闭（一）/打开/关闭f（s）（1FiU）/打开/关闭我我我我W？ 如果d06=d沿w.r.t.平移本文归纳地定义了F型T上的模态公式'到F型F0上的T0上的模态公式'的结构，）如下：(i) （a）？//？（b）（'！）的方式（'0！0）如果'0和0(ii) 如果由恒等自然变换给出，则可以区分以下子情况：(a) 如果由1 DU给出：D = DU）DU：D d(b) 如果由1f（s）给出：f（s）=s U和s 2 S：下一个s'，其中s：T0//nextf（s）'0if'）T s U。//'0(c) 如果由1F1UF2U给出：F1UF2U）F1UF2U=（F1F2）U：[]'（1F1UF2U）//[]'0if''0，其中i2f1;2g(d) 如果由1F1U+F2U给出：F1U+F2U）F1U+F2U=（F1+F2）U：[]'（1F1U+F2U）//[]'0if''0，其中i2f1;2g(e) 如果由1（FU）D：（FU）D）（FU）D=FDU：[ev（d）]'（1（FU）D）//[ev（d）]'0if' '0(f)如果由1P（FU）：P（FU））P（FU）=（P（F））U给出：[P]'//[P]'0if''0(iii) （a）如果由下式给出：D0）D= DU：Dd（d0）=d(b) 如果由d：F）D = DU给出：（> 如果d0=d(c) 如果由yi：F0F0）FiU给出，其中i2f1;2g且F0=Fi U：12i“[i]”0，如果“ ”0(d) 如果由h1;2i：F）F1 U F2 U=（ F1 F2） U给出，其中i：F）Fi U，其中 i= 1;2：/打开/关闭/打开/关闭（1名女）（个）（1FiU）/打开/关闭（1FiU）/打开/关闭D/打开/关闭0d063[1;2]/打开/关闭（一）（）下一页/打开/关闭/打开/关闭h1F0;di1的t0（评估随访;D）/打开/关闭（1个后续行动）/打开/关闭（1页2）（一）/打开/关闭（二）1的t09020D2D21[i]“//“0if”'0，i2f1;2g(e) 如果由yi给出：FiU）F1U+F2U=（F1+F2）U，其中i2f1;2g：[j]“（一）'0ifj=iand'>如果j6= i'0，j2f1;2g（f）如果由[1;2]给出：F1+ F2）FU，其中i：Fi）FU，对于 i= 1;2：“[1]”%1^[2]“%2if”//“% i 对于i=1;2(g) 如果由下式给出：F 0）（FU）D = F D U，：F 0D）后续：[ev（d）]“0if”“1”0(h) 如果由eval FU给出;D：（FU）DD）后续：'V（[]d！ [][e v（d）]"）if“”0(Note这里，集合D必须是nite。）(i) 如果由P（）：P（F 0））P（FU）=（P（F））U给出，其中：F 0）FU：[P]“[P]'0if'//'0(iv) 如果由12：F0）FU给出，其中1：F1）FU和2：F0）F1在kKPS0k中，并且如果尚未定义：“//”0如果"1和“1”0对于s2 S，T上s型的状态公式到typef（s）的T 0上的状态模（记为s：SForm（T）s！ S For m（T0）f （s），由y（1f（s ））给 出 ：For mT（s）！ F或mT0（f（s））（其中1f（s）：f（s）sU）。（i）定义3.3中的复数公式沿着任意自然变换的变换，是根据它们的子公式沿着相同的自然变换的变换来定义的。(ii)定义3.3将用于T上的模转换为用于T0 上 的 模，但是是类似的类型。这是通过取=1F0来完成 并对F. 这里的第二种情况是F0= f（s）。(iii)定义3.3中的公式将T上的模态公式沿着任意自然变换转换为T0上的模态，考虑到这些公式可以根据的形式采取各种形状。例如，将F1类型的模态公式沿1：F 1 UF0）F1 U要求满足它的满足给定的公式沿1F1U的平移。 另一方面，沿着1：F1 U）（F1+ F2）U的F1 + F2型模态公式的平移取决于给 定 公 式 所 指 的 是 哪个余积分量。如果9这一条件确保， 只有一次定义，通过防止定义 基于形式=1<$h;i或=[;]<$1的等式。h1;2i（一）/打开/关闭（1FiU）/打开/关闭P（）/打开/关闭（64（一）/打开/关闭/打开/关闭（1个后续行动）/打开/关闭不TT不0TT不公式是指第一个余积分量，它的翻译需要的是来自第一个余积分量的状态的原始公式所需要的，但是沿着1F1U进 行 翻 译。 如果for mula指的是第二个余积成分，那么它的翻译就不需要任何东西。形式为[ev（d）]'的模沿：F0）FDU的翻译是通过首 先将'along：F0D）FU翻译为'say'0，然后从'0'中“提取”恰好在' 0 '时保持在状态 f0 的type F0的模来获得的保持在状态hf0;di。此外，沿着eval FU;D：（FU）DD）FU的用于mula的模态的翻译需要满足它的任何状态h f;di使得f（d）满足沿着1 FU的翻译。（四）定义3.3根据沿着被合成的自然变换的平移，定义沿着自然变换的合成的平移下面的结果证明了定义3.3的正确性建议3.4Let（f;）：（S;T）！ （S 0;T0）表示一个多类共轭态射，设（：F0）F）2kKPSk（因此（U：F0 U）FU）2kKPS0k）. 那么，（U）10（1F U）=（U）=（1F0U）表格T（F）（1个后续行动）//F或T0（FU）TTTT （U）1TTTTTTT（U）10FormT（F0）（1F0U）//FormT0（F0U）证据 这一陈述之后是关于的结构归纳。2推论3.5Let（f;）：（S;T）！（S0;T0）表示一个多类共符号态射，设（ 1： F1）F）2kKPSk（henCe（ 1U： F1U）FU） 2kKPS0k）和（2：F ）F1U）2kKPS0 k是这样的，使得（1U=2）是根据（1U）和（2）10使用定义3.3的（iv）来定义的。那么，（2）10<$（1U）=（1U<$2）=（2）<$（1）1T：表格T（F）（1U）//FormT0（F1U）TTTT（1U/2）（1）1吨TTTTTTTT（二）十表格T（F1）（二）//FormT0（F0）证据 使用定义3.3和命题3.42注3.6以下是定义3.3和更正3.5的结果：[i]“[i]“0if”“0[i]“（[i]'0^[j]>）[i]'0if''0，j=f1;2g nfig[e v（d）]'[e v（d）]'/打开/关闭[e v（d）]“0if”“0/打开/关闭[e v（（d））]'0if''0（一）（二）（1+2）（一）/打开/关闭（D）（（FU））65//FormT（F1F2）////FormT0（F1+F2）//1不 //FormT（F D）D121不不0（自然转换）12：F0F0）F 1 UF2U，1+2：F0+F0）FU+FU、D：F0D）（FU）D和（FU）：（FU）D0 ）（FU）D如在21 2注2.3.）公式沿着余签名态射的平移与注2.3中的等式（i）{（iii）相容，在某种意义上，下面将更精确建议3.7Let（f;）：（S;T）！ （S 0;T0）表示一个多类余符号态射.那么，下面的内容就可以达到语义等价10：（i）h1;2ih（i）1T =（i）for（i：F）FiU）2kK PS0k，i=1;2：形式T （Fi）㈠1吨（一）h1;2i形式 T0（女）（ii）（i）10 [1;2]=（i）对于（i：Fi）FU）2kK PS0k，i=1;2：形式T （女）[1;2]（一）（i）10形式 T0（Fi）（iii）（1D）（e valF; D）1T =for（：FD）FU）2kK PS0k：F（F）（评价F;D）1（1 D）T0前（F0 D）证据 该声明直接从定义3.3中得出。2定义3.3产生一个函子SForm：Cosign！集合，对它的状态公式集取一个多排序的余签名，对导出的平移取一个多排序的余签名态射。例3.8给定A2 j Set j，用闭函子T LFTS：Set！由TLFTS= P（A Id）N给出的集合，连同定义nite深度的未标记转移系统的模态公式（见例2.14）沿着由自然变换：：= P（2）N：P（A Id）N）P（Id）N定义的连署态射的平移。具体而言，这些模态公式为：下一页[1][P][2]next[2]（n+1）$next[1]（hPi[2]next[2]n^[P][2]next[2]（0_： _n））;n2N或者，将next[1][P][2]重命名为[succ]，将next[1]h Pi[2]重命名为，将next [2]重命名为[depth]，并使用next [1]在^w.r.t.上的分布性。语义等价：[depth] 0 $[succ]？[depth]（n+ 1）$[depth] n^[succ][depth]（0_：_ n）; n2N10请注意，推论3.5在这里不适用。66（1Id）/打开/关闭P（2）（十一）（十一）/打开/关闭（1Id）/打开/关闭（1Id）/打开/关闭（11+））E（1Id）/打开/关闭P（A）Id）Nhi>/ hi>？什么？例如，事实上，翻译的模式为穆拉下一步[1][P]？沿着由y定义的余签名态射，由ynext[1][P][2]给出？可以推断如下：？P？[1][P]？下一个[1][P]？//[2]？//[P][2]？//[1][P][2]？//next [1][P][2]？还值得注意的是，T LFTS可以通过在P（2）的余弦中取推出来获得：TTS！T LTS和1：T TS！T FTS。对于，以下是KP 1中的回调图：1 JJTTP（2）1NqyjjjP（A）Id）TTTTP（2）TTTTT-%P（Id）Njjjjjyqjjjj1P（Id）例3.9元素属于集合E且大小不超过m2N的列表用内函子T mLIST：Set！设置givenbyTmLIST=TLISTf0; ：;mg（TLIST的定义与例2.15相同），以及定义E上列表的模态公式（见例2.15）沿着由：：=1：TmLIST）TLIST定义的连署态射的转换，以及以下模态公式：下一页[2]0$下一页[1][2]h1i>下一个[2]（n+1）$下一个[1][2]h2i下一个[2]n;n2f0; ：; m1g（一）特别地，模态公式de ning lists沿着由定义的连署态射在E上的平移如下获得：>联系我们>>>h1i>//h1i>（11+Id）1/1（1（1+E）（1+Id））[1]h1i>//[1]h1i>（一）[2]h1i>（1+E）（1+Id））//[2]h1i>[1]h1i>下一页[1]h1i>[1][1]h1i>下一页[1][1]h1i>[2]h1i>下一页[2]h1i>[1][2]h1i>下一个[1][2]h1i>下一页[1]h1i>$下一页[2]h1i>下一页[1][1]h1i>$下一页[1][2]h1i>在将next[1][1]h1i、 next[1][1]h2i、 next[1][2]h1i、 next[1][2]h2i和 next[2]分别重命名为、、、和[size]之后，（二）（1Id）/打开/关闭/打开/关闭67大小最多为m的列表的规范变为：>$ tailF>>[size]0$>[size]（n+1）$[size]n;n2f0; ：; m1g（二）例3.10通过适当地扩展例3.9中给出的不超过m的列表的规范，可以得到m大小的数组的规范。 当调用y时，可以考虑共同签名（Se tfmLis t;Arrayg;T），其中内函子T的分量由T mList= T mLIST1（1 +E）f1;：;mg和相应地TArray=1Ef1; ：;mg 给 出。（第二个 comppone ofTmLists peciesalistobser verwhichtakesan数组p2f1; ：;m g andreturn the p th element of the list in casethis element exists，or？否则，请执行以下操作。此外，TArray的第二个组件指定了一个数组观察器，它接受一个数组p2f1; ：;m g并返回数组y的第p个元素。大小为m的数组的规范则由以下公式组成：>$ tailF>>[size]0$>[size]（n+1）$[size]n; n2f0; ：; m1g> $> e$ e; e2 E>$> _>; p2f1; ：; m1ge$e; p2f1; ：; m1g;e2EmList类型的函数，以及以下公式：[get（p）]e$[list]e; p2f1; ：;mg;e2E（3）o类型Array，使用以下缩写：：：=nextmList[1][1][1]h1i：：=nextmList[1][1][1]h2i：：=nextmList[1][1][2]h1i：：=nextmList[1][1][2]h2i[size]：：=nextmList[1][2]：：=nextmList[2][ev（ p）]h1i：：=nextmList[2][ev（ p）]h2i[list]：：= nextArray[1][get（p）]：：=nextArray[2][ev（ p）]68特别地，（3）中的公式指出，对于nypos i t i onp2f1; ：;m g，数组的第p个元素由相关联的列表的第p个元素给出。它69的t0SW12我值得注意的是，这个公式实际上将用于表示数组的列表限制为大小正好为m的列表。然后，将大小至多为m的共同签名指定列表包含到大小为m的（二排序的）共同签名指定数组中由共同签名态射（f;）捕获，其中f：f mList g！fmList;Arrayg是包含函数，其中：UT）TmLISTUbeing给出1：TmList ）TmLIST1（其中U：Se tfmL is t;Arra yg！Setisgivevenbyy①的人。定义大小至多为m的列表的模态公式沿着这个连号态射的平移使（2）中的公式保持不变。然而，注意，、、...当从TmLIST移动到T时改变，所以例如（1）中的公式实际上当从TmLIST移动到T时改变。如前所述，沿着连署态射的公式翻译保留了公式的解释。建议3.11Let（f;）：（S;T）！（S0;T0）表示一个多类ed坐标，0 0 0 0自然态射，设hC;i表示T-co代数a，设=C0 你好，0 0100UC！ TUC. 然后，C 0 （J'KF）=J（'）KF0 对任意F2jKPSj，F02jKPS0j，（：F）FU）2kKPS0k和'2FormT（F）.证据这个陈述之后是关于“和”的结构归纳。这里只考虑其余的（见定义3.3）也作类似处理。如果由1f（s）给出：f（s）=s U和s 2 S：Jnext 'K=1（J'K）=（0）1（1（J'K ））=sssTsf（s）s;C0 Ts0f（s）1（J（s））（'）K0f（s））=Jnextf（s）（个）（'）K0 =f（s）J（1）（f（s））（下一个s'）K0f（s）= J（下一个s'）K0f（s）如果由下式给出：D0）D= DU：1 10 0 0 0了c0 （JdKD）=C 0 （fdg）=fd2Dj（d）=dg =fdg =（d0）=d00000 0（dS0）=dJdKD0 =J（d0）=dD0 =J（d）KD0 =J（d）KD0如果由下式给出i：F0F0FiU，i2f1;2g，F0=Fi U：01（J'K）=1（J'K）=1（J（1）（'）K）=了c0J[]（1FII）（'）K0Fi= J（）我（'）K0FiU= JFiU（'）K0iFiUF0F0iF0 F0F0 F01 2 1 2 1 2如果由yi给出：FiU）F1U+F2U=（F1+F2）U，其中i2f1;2g：（70如果j=i且flg=f1;2g nfj g：71不f（s）f（s）表明上述持有可以减少到表明，鉴于 和1（J[]'K）=1（（J'K）[（FUC 0））=J'K=C0jF1+F2jjFjl lFjJ（1））（'）K00=J（）（[]'）K= J（[]'）K0如果j6=i：FjUFjUj jFjUjFjU1（J[]'K）=1（（J'K）[（FUC 0））=FUC 0=C0jF1+F2ijFji i i iJ>K00=J（）（[]'）K= J（[]'）K0Fi UijFiUjFiU如果由下式给出：F 0）（FU）D = F D U，：F 0D）后续：1（J[e v（d）]'K）=（）1（ff：D！FUC 0jf（d）2J'Kg）=C0FDC00000F0000ff2FCjC 0（f）（d）2J'KFg=ff2FCjC0（f;d）2J'KFg=1 10 0h1F0;diC 0（C 0（J'KF））=Jh1F0;di10（（'））KF0 =J（[e v（d）]'）KF02特别地，T0-余代数的T-约简中的模的状态的解释与原T0-余代数中的模的平移的解释是一致的在S2S。我们现在准备好了我们的主要结果。定理3.12（Cosign; Coalg; SForm; j=）是一个机构。证据作为一个机构的性质相当于以下等价物，对于一个任意排序的连署态射成立：（S;T）！（S0;T0），一个nyT0-余代数hC 0;0i和一个nyT，对于模2SForm（T）：hC 0;0i