广义共归纳与最终F-余代数模式的扩展性证明技术

67《理论计算机科学电子札记》44卷第1期（2001）网址：http://www.elsevier.nl/locate/entcs/volume44.html21页广义共归纳F. Bartels1CWI，P.O.Box 94079，1090 GB Amsterdam，荷兰http://www.cwi.nl/~bartels摘要本文引入了环上函子T的分配律λ的λ-余迭代模式一个函子F.在某些条件下，它可以证明唯一地将函数分解为最终F-余代数的载体，推广了由最终性给出的基本余迭代模式。原始递归和价值过程迭代的迭代，这是已知的共同迭代的扩展，出现作为我们的框架的实例。人们还可以获得证明递归规范的模式，这些规范涉及诸如幂级数加法、语言上的正则运算符或进程的并行和顺序组合接下来，相同类型的分配律λ被用于推广共归纳证明技术。为此，我们引入了λ-互模拟关系的概念。它专门研究从上面提到的类型的操作符构建的上下文的互模拟直到相等或互模拟直到上下文。 我们指出，每一个这样的关系包含在一些较大的传统互模拟，并证明这一原则导致更简单的双相似性证明使用不太复杂的关系。1介绍大约在90年代初，人们发现范畴C上函子F的最终F-余代数的范畴概念对于抽象描述是有用的在计算机科学中可能是无限的对象。例子是数据流，如无限流或动态系统，如过程或自动机（例如，参见Jacobs和Rutten的介绍[JR 96，Rut00b]）。将这些不同的实体统一地视为某种类型F的行为系统，允许对定义和证明原则进行抽象的表述，这些原则之前已经为各种应用分别进行了研究。一个最终余代数的状态可以用一个由最终性直接我们在这里称之为重叠，[1]这里报告的研究是NWO项目ProMACS的一部分2000年1月，出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-ND许可证。巴特尔斯68衍生变体。证明状态相等的主要工具是F-互模拟 [AM 89]，这是用于不同具体系统的互模拟概念的分类概括。但这些基本原则往往过于严格，无法很好地涵盖给定的例子。许多函数到一个最终余代数的载体可以证明是不是coiterative和许多声明是-economical等价需要互模拟这是很难展示和检查。因此，几个特定的设置扩展进行了研究。更一般类型的例子是作为原始递归和值过程迭代的基础而产生的定义原则。用递归方程组对过程的具体化形成了另一种形式。为了证明的目的，人们经常使用这样的关系，它们本身不是互模拟，而是满足包含在某种互模拟中的充分条件。这些通常被称为互模拟（参见例如，Milner [Mil89]）。Sangiorgi[San98]介绍了一个框架，用于在标记过渡系统的背景下导出这些原则形成原始递归和价值过程迭代的模式的范畴公式是已知的，参见例如Vene和Uustalu [UV99]。按照惯例，我们将第一个原始核心称为cursion。一个步骤，以更一般的描述扩展原则在这一水平上已作出了Lenisa在她 的 比 较 过 程 中 的 集 合 论 和 coalgebraic （ 范 畴 ） 配 方 coinduction[Len99a]。她已经证明了她的框架捕捉到了通过原始上递归可获得的箭头，并且对于值过程迭代的对偶也可以证明这一点，但是在这两种情况下，她的理论都通过修改莱尼萨简单地说，传统的迭代模式通过为每个元素指定一个直接观测和后继状态来为集合X的状态指定无限个条件。由于这些后继者又是从X中取出来的，所以应用于它们的相同的规范揭示了行为的第二层，依此类推。我们引入的λ-共迭代模式采用了一种不同的方法，它由另一个函子T和T在F上的一个分配律λ来参数化：它允许从TX中X的，这可以增加格式的表现力，如果前者可以被认为比后者“更丰富”。为了使观测值与这些后继观测值继续下去，分配律λ将X的具体化提升到TX。在本文的主要定理中，我们证明了两个额外的假设，它们中的每一个都足以使λ-余迭代模式唯一地定义到最终F-余代数的箭头。类似地利用T和λ，我们定义了λ-互模拟的概念，并证明了与λ-共迭代模式有效性相同的条件巴特尔斯69→→⟨⟩⟨ ⟩→⟨ ⟩ ⟨⟩足以表明，在这种关系中的所有状态都是双相似的。一个小的例子表明，该技术可以实现更简单的证明，涉及不太复杂的关系。对于T和λ的适当的实例化，可以从λ-余迭代模式中得到上述本原上递归和过程值迭代的对偶的范畴式，尽管我们没有解释详情在这里。相反，我们简要地概述了如何使用它来证明涉及某种类型的运算符的规范。这些是Turi和Plotkin [TP97]已经证明与GSOS格式[BIM95]中的结构化转换规则定义的操作符密切相关的操作符。同时将这些模式作为我们框架的实例，产生了λ-互模拟证明技术的相应变体。对于通过运算符定义的情况，人们获得了从上述类型的运算符构建的多变量上下文（即具有几个“洞”的上下文）的互模拟到上下文的概念[San98]。这为这些运算符的可用性提供了一个抽象的理由。所提出的理论是针对某个范畴C而陈述的，但为了便于阅读，我们的解释和例子都涉及集合和全函数的范畴Set。本文是CWI同名技术报告的简短版本[Bar00]。长版本包含了这里给出的大多数陈述的详细证明和进一步的例子。2（Co）代数与（Co）迭代在这一节中，我们将简要地介绍代数和代数的范畴观点更详细的论述可以在例如Jacobs和Rutten的论文中找到[JR 96，Rut00b]。我们取C和T，F：C C表示一个范畴和它上面的两个函子.定义2.1[T-代数，F-余代数] T-代数是一对X，β，其中X是C的一个对象，β：T X X是C中的一个箭头。 我们有时会称X和β为代数的载体和运算对偶地，F-余代数是一个对X，α，其中运算α：XFX是一个指向相反方向的箭头。一般来说，代数运算可以看作是构造其载体元素的一种手段余代数的运算在第一种情况下，我们将讨论一个状态允许的观测，在第二种情况下，我们将讨论它的动力学。定义2.2[同态]一个箭头h：X→Y是从一个T-代数X，β X到另一个T-代数Y，β Y的T-代数同态，如果它使下面的左图可交换。类似地，从一个F-余代数<$X，αX<$到另一个F-余代数<$Y，αY$的F-余代数同态是一个箭头h：X→Y，使得右图可交换：巴特尔斯70F⟨⟩⟨⟩ ⟨ ⟩→⟨ ⟩ ⟨⟩⟨ ⟨ ⟩⟩ →→→×∈Fh⊕ ×→TXTh TYβXβYJ JXhYαXαY J JXhYFXFhFY我们经常只讨论同态，当它们的类型从上下文中很清楚的时候。代数和余代数与相应的同态一起分别形成范畴AlgT和Coalg。定义2.3[final F-余代数]final F-余代数是F-余代数范畴CoalgF中的一个final对象，即一个余代数F-余代数例2.4我们后面的一些例子将涉及实数σ的无限流IR ω。 这些作为函子的最终余代数的状态出现S：设置设置，其中S X：=IRX. 这个函子的余代数具有形状X，o，s对于集合X和两个函数o：XIR和S：XX. 也就是说，对于每个状态，我们可以观察到一个实数，并移动到一个后 继 状 态 。 实 数 的 无 限 流 形 成 最 终 的 S- 余 代 数 <$IR ω ， <$head ，tail<$R，其中对于每个流σ=<$σ0，σ1，.. . ∈IR ω，观察值由其第一个元素头（σ）：= σ0和后继元素尾（σ）：= σJ：=σ1，σ2，. . .下面我们将S-余代数称为流系统一个F-余代数<$F，ωF的final y产生一个函数wh：X对X上的每一个F-余代数运算α，通过假设它是X，α到<$F，ωF的唯一同态，得到了<$F. 于是，Suchannw被称为由α的同向相对箭头：X__！h__FαωFJJFX_FF例2.5[流的重叠迭代]例2.4中流系统的重叠迭代模式表明，对于每对函数o：X→IR和s：X→X，存在唯一函数f：X→IRω，满足f（x）=0，tail（f（x））= f（s（x））.作为一个例子，我们来看看两个流的元素加法。通过共迭代模式，存在唯一函数：IRω IRω IRω满足以下两个等式：头（στ）=头（σ）+头（τ）tail（στ）=tail（σ）tail（τ）巴特尔斯71→⟨ ⟩ ≤ ⟨ ⟩→S⟨ ⟩ ⟨ ⟩ B ⟨⟩..⟨ ⟩ ⊆×⟨ ⟩ ⊆ ×≤作为原理的一个证明，对于一个最终的F-余代数<$F，ωF<$，通过在X上提供一个F-余代数运算，使得两个箭头h1，h2：X <$F是相等的，其中两个箭头都是同态.大多数情况下，人们利用这个性质来证明两个状态表现出相同的行为，即它们通过余迭代态射映射到最终余代数的相同状态上。从技术上讲，人们使用基于互模拟概念的派生原理。我们在跨度方面有一个定义：定义2.6[span]在范畴C中，两个C对象X和Y之间的跨距R=R，r1，r2由一个对象R和两个箭头r1：R→X和r2：R→Y组成。X和它自身之间的跨度称为X上的跨度。在对象X和Y之间有一个的<$Y，αY<$，其中互模拟性质由γ：B→FB证明。设hX和hY表示从αX，α X，αX到αX的余迭代箭头，FXFB巴特尔斯72⟨⟩→→⟨⟩ω∞⊕⊕⊗⊗和αY，α Y，αF到最终余代数ωF，ωF，则得到图b-下在CoalgF中，通过最终交换。这就得到了所需的hX（x）=hX（π1（πx，yπ））=hY（π2（πx，yπ））=hY（y）γR，γ Rπ1SJX，αX、、π2，，vzαY，α Y高X ，vzsJhYF，ωF3定义：λ-Coiteration最终F-余代数<$F，ωF的状态可以用来表示F型的抽象行为，正如我们在上面的解释中已经做过的那样。箭头f：X<$F将这些行为分配给X的元素。coiterationschema允许我们定义这个函数，使得它将X的每个元素映射到它在给定的F-余代数<$X，α<$中表现为状态的行为。不幸的是，对于许多想要指定的函数f：X<$F，X本身上没有F-余代数运算α使f成为余迭代态射，或者从f的给定指定中可能不明显。在本节中，我们将首先介绍这种规格。然后，我们将更抽象地表达遇到的模式，本文的主要定理这就产生了一个定义模式，我们称之为λ-coiteration。3.1示例：形式幂级数的乘法例如Rutten[Rut00a]，我们将考虑有限个随机数流σ=σ0，σ1，.. . 形式幂级数的表示i=0时σ i X i. 的操作从例2.5中可以看出，τ代表由σ和τ表示的两个级数之和。类似地，我们想在IRω上定义一个二元运算，使得σ τ表示由σ和τ表示的两个级数的卷积积。经过一些计算（cf。[Rut00a]）得到以下规范，其中常数级数r∈IR表示为[r] =r，0，0，. . ε∈IR ω：2头（στ）=头（σ）·头（τ），tail（σ <$τ）=（[head（σ）]<$tail（τ））<$（tail（σ）<$τ）。这两个方程并不像例2.5那样形成一个共同迭代的定义，因为在表示尾部的表达式中使用了“尾”。为了更好地理解我们这里的定义类型，我们设置X：=IRω×IRω和o：X→IR，s1，s2：X→X，2共迭代：head（[r]）=r和tail（[r]）=[0]。巴特尔斯73⊗→|◦→→β⟨⟩→ ⟨⟩⟨ ⟩→⟨⟩⊕⟨ ⟨ ⟨ ⟩⟩⟩ ⟨ ⟨⟩⟩×⊗o（σ，τ）：=head（σ）·head（τ），s1（σ，τ）：=[头（σ）]，尾（τ），s2（σ，τ）：=尾（σ），τ.使用这个，上面的等式可以通过要求拟合到下面的图表中来替代地陈述X_IRω_________________________1991年，第1，第2次世界大战期间，IR×（JX）JωX×IdIR×（λ（λ ×λ））IR×IR下面要更一般地讨论的问题在这里等于问这个条件是否唯一地定义了箭头。3.2一般模式为了更抽象地描述上述规范的格式，我们做了以下两个定义：定义3.1[T-扩张]设β：T Y Y是T-代数. 对于给定的箭头f：XY，我们称fβ：=βT f：T Xf的T-扩张沿β：TXTfTY、、、F|、、、β，zJXfY定义3.2[同态上β]设X，φ是FT-余代数，Y，α是F-余代数，其上有T-代数运算β：TY Y 一个箭头f：XY称为从X，φ到Y，α的上至β的同态，如果它使下面的图可交换（注意，在图中 我们为β添加了一个箭头，以可视化其类型，尽管它没有贡献表示的交换性TYβFJX YφαJ JFTXFf|βFY通过取函子T：= Id Id Id，成为从ST-余代数X，o，s1，s2到IRω，head，tail，最终S-余代数的同态，因为我们可以将图底部的箭头重写为如下：IdIR×（（×））= S（（×））= S（T）= S|- 是的巴特尔斯74→⊗⇒→α⟨⟩α→→3.3分配律我们在寻找一个框架，在这个框架中，对于给定的T-代数算子β，到最终F-余代数<$F，ωF的同态唯一存在。由于很容易看出这不是所有β的情况，因此需要限制允许的操作类别。直到β的同态的唯一存在性意味着对象X上的FT-运算指定一个箭头h：X<$F，即抽象F-行为对X中元素的赋值。这表明β计算T <$F的元素的方式可以通过T和F的相互作用的具体化来更全局地描述。在我们的方法中，我们假设这是由下面定义的T在F上的分配律λ给出的在我们的例子中，可以看出运算是由这样一个分配律λ产生的。定义3.3[分配律]设T，F：C C是两个函子.自然变换λ：TF FT称为T在F上的分配律。我们有时会交替使用短语T通过λ分布在 F上。Turi和Plotkin [TP 97]给出了分配律概念在计算机科学中的一个主要应用，其中两个函子分别作为单子和共单子出现，并考虑了涉及额外结构的额外相干轴（参见Power和Watanabe [PW 99]的工作，以了解这种设置的结构化说明）。随后，分布律也被用于对函子假设较少结构的情况，并且相应的相干公理被丢弃（参见[LPW00]）。现在我们只处理普通函子而不处理相干公理，但我们稍后会遇到需要更多结构的情况将来自TX的元素视为包含来自X的元素作为参数的结构化实体，分配律告诉我们如何在给定参数可以执行的步骤的情况下将F步骤分配给这样的实体。有了这些信息，我们可以从F-余代数<$X，α<$导出TX的F-余代数运算定义3.4[λ-提升]给定函子T在函子F上的分配律λ，我们可以通过设置将T：C C提升到F-余代数上的函子Tλ：CoalgFCoalgFTλ<$X，α<$：=<$TX，升力λ<$和Tλh：= Th，对于F-余代数<$X，α<$和F-余代数同态h，其中升力λ：= λ X<$T α：T X→ FT X。为了使这个定义有意义，我们需要以下引理，使用λ是自然的假设很容易证明引理3.5（也见[Rut 00 b，定理15.3]）设h是从λX，α Xλ到λY，α Yλ的F -余代数同态，则Th是从T λX，α Xλ到T λY，α Yλ的同态.巴特尔斯75×F⟨ ⟩ ⟨⟩、、⟨ ⟩ ⟨ ⟩ ⟨⟩XF在我们的例子中，T：= Id Id在S上的分配律λ应该给出两个态相加的整体描述对于集合X，我们定义λX：（IR×X）×（IR×X）→IR×（X×X）为(1)λ X（λo x，s xλ，λo y，s yλ）：= λo x+ o y，λs x，syλ。很容易证明我们确实得到了一个自然的转变。给定一个流系统，结果系统Tλ具有来自X的状态对作为状态。展开这样一对x，y，得到两个观测值o（x）+o（y）和后继观测值对s（x），s（y）的和，即X，y在Tλ中的行为x，y，o，s是x和y在T λ中的行为的（流）和。我想找你。通过上面的提升，给定X中元素的行为，分配律λ将F-行为分配给集合TX。我们将要陈述和证明的广义共归纳图式涉及T-代数运算β，它保持了这些行为。更精确地说，对于给定的F-余代数X，α，我们考虑从TλX，α到X，α的同态β.事实证明，这种情况在文献中被λ-双代数发生环的概念所捕获，因此我们在这里回忆它的定义定义3.6[T，F-双代数，T，F-双代数同态，λ-双代数] A T，F-双代数是一个对象X和两个箭头β的三元组λX，β，αλ：TX→X和α：X→ FX，即一个T-代数和一个F-余代数运算在一个共同的载体上。给定两个T，F-双代数<$X，β X，α X<$0和<$Y，β Y，α Y<$0，从<$X，β X，αX<$0到<$Y，β Y，α Y<$0的T，F -双代数同态是一个箭头h：X → Y，它既是从<$X，β X <$0到<$Y，β Y<$0的T-代数同态，又是从X，α X到Y，α Y的F-余代数同态。与T-代数和F-余代数一样，T，F-双代数和它们的同态构成一个范畴，记为BialgT。给定T在F上的一个分配律λ， λ-双代数是T，F-双代数<$X，β，α<$，使得下图可互换：Tα、TX，oTFXβJλXλ-bialg XJFTX，αFβ，zF<$J记BialgT的包含所有λ-双代数的满子范畴为λ-Bialg。请注意，实际上，将T λ <$X，β，α<$定义为λ-双代数等价于说β是从Tλ <$X，α<$到T λ <$X的F-余代数同态。αX、αX和α X的平均值分别为0. 利用这一注记，对于最终F-余代数<$$>F，ωF<$对于T-代数运算βλ：T <$F→<$F，存在一个选择，使得<$$>F，βλ，ωF<$是λ-双代数，即Tλ <$$>F，ωF<$的迭代态射到ωF，ωF，分配律的双代数在本文中起着重要的作用，巴特尔斯76⟨⟩⟨⟩⟨⊕ ⟨⟩⟩⟨⟩⟨⟩⟨ ⟩ ⟨⟩i=0时Turi和Plotkin [TP97]也是。与分配律的定义一样，我们的λ-双代数概念不同于他们的概念，因为我们没有假设T和F是单子和余单子：在它们的集合X中，β和X，α被假设分别是单子的代数和余单子的余代数。在我们的例子中，所考虑的双代数是IR ω，，head，tail。很容易证明它是λ的λ-双代数，如（1）。3.4λ-重叠迭代定义模式现在我们准备定义一个新的模式，称为F上函子T的分布律λ的λ-coiteration定义3.7[λ-Coiterative Arrow]假设给定一个函子F，它有一个最终余代数ωF，ωF，和另一个函子T的一个分布函数wλF.对于FT-余代数<$X，φ<$，我们称箭头f：X→<$F为φ诱导的λ-余迭代箭头，如果它是从<$X，φ<$到<$F，ωF<$的直至- β λ的同态对于唯一的ωwβλ，使得ΩF，βλ，ωF是λ-双代数（c.f. 注：定义3.6）：FXφJTFβλJFωFJFTX_β_FFf |λ我们想使用上面的图作为f的定义，称之为λ- coiteration模式。为了能够做到这一点，我们需要证明对于任何给定的FT-余代数X，φ，λ-余迭代箭头的唯一存在性。这两个问题的解答是通过建立λ-余迭代箭头与由X，φ构造的F-余代数LX，α φ的余迭代箭头之间的一一对应来给出的。前者的独特存在是由后者的独特存在而来的。这些构造分别需要对C或T和λ进行额外的假设：定理3.8（λ-余迭代（1））设范畴C有可数余导，且给定一个函子F：C→C，其最终的余代数为ω F∈F，ωF∈ F，另一个函子T：C → C通过λ分布在F上. 然后，对每个FT-余代数<$X，φ<$X，存在唯一的由φ诱导的λ-余迭代箭.利用这种方法，我们构造了一个关于countable的F-余代数，ut∞i=0TiX. 该运算是求解φi：TiX→FTi+1X的一个实例分析和适当的联产品注射，其中φi作为以下的提升获得：φ通过λ。关于βλf：X→λF上的同态与同态h：∞i=0TiX→<$F由f <$→[fi]∞i=0和h<$→h<$inn0给出其中f0：=f，f i+1：= f i|βλ，ini是第i个副产物注入，并且[. ]∞是_巴特尔斯77⊗⟨ ⟩ ⟨⟩ıııı、、∈⟨⟩⟨⟩⇒可数案例分析。 详细的证明可以在[Bar00]中找到。利用这个定理，我们可以最终回答3.1节中的具体化是否唯一地正定义了函数的问题：这个例子是在集合范畴中，它当然有可数的余积。定理3.9（λ-余迭代（2））设函子F：C →C有一个最终的c~ o代数ra∈F，ωF，C中的一个单子T，η，μ，以及这个单子在F上的一个分配律λ，即T在F上的一个分配律，使得下面的图可交换，我们将其称为λ的单位和乘法律：FT FλzFTc、..、、、ηFcccccCcc，Fη、、、电子邮件ıııı，Fµ、、、、，ccunit λ z2个月。 λ2TFλzFTTF，，，F，TTλ，，z，λ，TTFT然后，对每个FT-余代数X，φ存在唯一的由φ诱导的λ-余迭代箭.在T作为单子出现的情况下，对于每个i IN，来自TiX的元素可以在TX内表示，可以使用η或（可能几次）μ。关于λ的附加假设确保这些映射havioursbe代替∞i=0TiX构造为bove。对同性恋的正确认识给出了直到βλ f的态射：X→<$F和同态h：TX→< $F由f → f |βλ和h <$→ h <$η X。作为一个注释，上面的论证将定理3.9得到的λ-余迭代箭头标记为在Lenisa [Len 99 a]的框架中余迭代到T，η。实际上，她用来推理这些态射的设置对应于位于这里给出的两个定理之间的假设的另一种变体：它假设范畴C具有ω-链的共极限，并且函子T被假定为一个点函子，λ满足单位律。3.5属性和扩展作为一个有趣但微不足道的观察，注意到共同迭代模式本身是通过自然变换FId：IdF FId在F上分布的恒等函子的λ在这个方向上的另一个观察是，当存在单位自然变换η：Id T时，λ满足单位律（无论如何，这在定理3.9中是假定的），则λ-共迭代模式的相应实例单独地推广了共迭代模式：人们可以获得由任何F-共代数运算α：X→FX诱导的共迭代箭头，作为由FηXα：X→FTX诱导的λ-共迭代箭头（关键的观察巴特尔斯78→→- -我是◦→∈∈×⇒，，×拉 斯关于λ的假设使β λ成为指向函子π T，ηπ的代数运算，它产生f |βλ η X=f）。一个简单的共迭代模式的扩展是作为递归的对偶出现的，因此有时称为原始共递归（参见例如[UV99]）。 它指出，在一个具有二元余积的范畴中，每个箭头φ：X F（X +<$F）唯一地确定一个态射f：X使下面的图表通勤。X_∀φ__！h_--ωFJF（X+F）_JF FF[h，Id]这一特征可以作为函子TX ：=X+<$F的λ-迭代模式和分配律λ ：TF<$FT （ 定 义 为 λX ： =[Finl ， FinrωF] ： FX+<$F ） 得 到F（X+<$F）。 在l oc。前引书作为值过程迭代的对偶而产生的S Chema也被明确地给出。它也可以作为λ-余迭代的一个例子得到。我们在此不作说明，因为这需要相当多的技术细节。我们仍然想提到的是，对于第二个例子，与“手工”证明相比，λ-coiteration大大简化了模式的证明最后，我们要提到的是，如果C类有两个-nary产品上述结果可以扩展到一个设置，分配律λ被以下类型的自然变换所代替：λ：T（IdF） 英尺 这增加了表现力，两个，F步骤，一些x X出现在tx可以做x对于T的行为的具体化。定理3.8和3.9可以通过小的修改推广到这个新的设置：在第一种情况下，构造进一步要求在范畴C中存在二元余积，在第二种情况下，λ的单位律和乘法律必须 修改如下：3Id×Fπ2zFT（Id×F）λzFTηId×F单位λFηµ（Id×F），、、、、、czcz2 ，2T（Id×F）λ zFTT（Id F）......穆特λT，T、、、T<$Tπ1，λ，λ，TT（T ×FT）3 根据Lenisa、Power和Watanabe的建议[LPW00]，这是通过从函子F移动到由F生成的余自由余点函子，即Id×F，π 1、、巴特尔斯79⟨ ⟩ ⟨⟩⊕ω4用λ-余归纳法在本节中，我们将考虑双相似性的广义证明原则。我们给出了一个例子的陈述，其中的直接关系未能成为互模拟。 但它满足了一个条件，足以得出结论，它包含在一些更大的互模拟中。这个条件再次通过关系上的FT-余代数运算而不是F-余代数结构的存在来表示，我们将这种关系称为λ-互模拟。相应的证明原则允许更简单的双相似性证明涉及不太复杂的关系。4.1示例：平均值对平均值的分布我们想证明例2.5中定义的实数流的加法分布在3.1节中考虑的乘法上：<$σ，τ，ρ∈IR：σ<$（τ<$ρ）=（σ<$τ）<$（σ<$ρ）由于在最终余代数上双相似包含在等式中，因此可以证明这两个项都表示双相似流。要找到的互模拟需要包含ω ω ω(2)B：={|σ，τ，ρ ∈ IR} IR × IR我们可以很容易地检验出所有与B相关的对都有相等的头。此外，要找到的互模拟必须将由B相关的每两个流的尾部相关联。计算得出4tail（σ<$（τ<$ρ））=（[σ0]<$（τJ<$ρJ））<$（σJ<$（τ<$ρ））``=：x1=：x2tail（（σ <$τ）<$（σ <$ρ））=（（[σ0]<$τ J）<$（[σ0]<$ρJ））<$（（σ j<$τ）<$（σJ <$ρ））。``=：y1=：y2我们得到与B相关的流的和，即x1，y1和x2，y2。 因此，互模拟还应该包含T（B）：={x1x2，y1y2 |<$x1，y1<$，<$x2，y2<$$> ∈ B}<$IR ω× IRω。但是，我们还需要检查T（B）中包含的对这种程序的继续将导致关系B_i：=∞T_i（B）。i=0时为了证明这是一个互模拟，我们可以通过对i∈IN的归纳来证明，对于x，y∈Ti（B），我们发现hea d（x）=hea d（y）andtai l（x），tai l（y）<$∈Ti+1（B）.4第二个问题涉及到的交换性和结合性。两者都可以很容易地证明使用标准的互模拟。巴特尔斯80⊆×2上述计算构成了这种归纳法的基本情况，归纳步骤简单且与B无关。5证明了如下原理：给定一个关系B<$IRω×IRω，使得对于<$x，y<$∈B，有那么B：=head（x）=head（y）andtail（x），tail（y）<$∈T（B）∞i=0Ti（B）是一个包含B的二进制数.有了这个原理，我们就可以像（2）中那样直接处理关系B，它只包含在陈述本身中使用的对。没有必要找到一个描述，涵盖所有的尾巴遇到，而走下来的流，因为它是这样做的，例如。”[10]“凡所有相，皆是虚妄。卢恩⟨i=0时（σi<$（τi<$ρi）），卢恩i=0时（（σi<$τi）<$（σi<$ρi））<$对n∈IN，σi，τi，ρi∈IRω（0≤i≤n）.4.2λ-共诱导我们现在要从上面明确地捕捉情况。对于通过λ分布在F上的函子T，它对应于要求在关系B X Y上的FT-余代数运算χ，使得对于所考虑的F-余代数上的合适的T-代数运算，投影同态达到-β我们引入以下概念：定义4.1[λ-互模拟]设F， T：C→C是函子。 A跨度B=如果B上存在FT运算χ，X和Y上存在T代数运算β X和βY，则B1，B2是F-余代数B1X，αX与B1Y，αY之间的λ-互模拟，使得B1X，βX ，αX与B1Y，βY，αY是λ-双代数，B1和B2分别是到-βX和-βY的同态：T X。T.YβX。Jbb.βYX，，1αXB.. ∃ χJY αYJ.JJFX，，βFb1|X FTB Fb2|βYFY如果我们想使T-代数运算βX和βY显式化，我们讨论关于βX和βY的λ-互模拟。一个λ-互模拟在λX，αX和它自身之间将被称为λ-互模拟在λX，αX上。结果表明，在定理3.8（3.9）中关于C（T和λ）的假设下，λ-互模拟只涉及双相似态。这可以通过给出一个构造来证明，该构造扩大了λ-互模拟，使得遇到常规的互模拟，类似于我们在示例中所做的的[5]归纳步骤基本上表明T是Sangiorgi [San98]术语中的一个尊重函数（将这个概念从标记的过渡系统翻译为流系统）。巴特尔斯81→⟨⟩⟨ ⟩ ⟨⟩⟨⟩⟨ ⟩ ⟨ ⟩›→›→×⊗⊗⊆ ×⊆×ω参数不假设最终F-余代数存在，因此可以使用在任何通过互模拟定义行为等价的情况下。定理4.2（λ-余归纳法）设两个函子T， F：C，C，使得T在 F上经由λ分布，并假定(i) C类有可数余积，或(ii) T取自一个单子T，η，μ，使得λ满足定理3.9的单位乘法律。设B是两个给定的F-余代数<$X，αX<$X和<$Y，αY<$X之间的λ-互模拟则它们之间存在一个（传统的）互模拟B，其中B≤B。该证明使用由B，χ构造的F-余代数LB，αχ，分别如定理3.8或3.9以同样的方式，直到-βX和-βY的同态产生F-余代数同态，LB，αχ至X，αX和Y，αY，sayb1B1和B22. （注意：此方向仅需要假设所涉及的双代数是λ-双代数，不需要finality。 这产生了二进制计算公式，其中，所要求的跨距的顺序由（i）中的0和（ii）中的η B证明。4.3重新审视的例子再次考虑4.1节中的例子，其中我们有T：= IdID和λ，如第9页上的等式（1）中给出的。在这种情况下，λ-互模拟的定义如下：设λX，λX，sX λ和λY，λY，sY λ是两个流系统，它们的载体上都有二元运算λX和λY，使它们成为λ-双代数。关系B<$X×Y是<$X，<$oX，sX<$$>和<$Y，<$oY，sY<$$>之间关于<$X和<$Y的λ-互模拟的条件可以很容易地看出等价于以下条件：对于所有<$x，y<$∈B，我们有oX（x）=oY（y）和<$sX（x），sY（y）<$∈T（B），其中T（B）：={x1|<$xi，yi <$∈ B; i = 1，2}.通过取λX，λo X，s Xλ= λY，λo Y，s Yλ= λIR，λ头，λ尾，λX=Y=，我们发现在第4.1节给出的原理中关于关系B的假设只是关于最终流系统的λ-互模拟。定理4.2告诉我们，这足以得出结论：存在与BB<$的互模拟B<$IRωIRω。根据定理构造的跨距4.2对应于第4.1节中的B节。5λ-余迭代与算子在本节中，我们将再次考虑在状态动力学定义中涉及算子的规范，但这次是以更灵活的方式。在前面的部分中处理的形式幂级数的卷积积的定义只能由简单的函子T：= Id Id处理，因为辅助运算在巴特尔斯82⊗∈×⟨ ⟩ ⟨ ⟩ ∈ ∗ ∗→联系我们∗2 ∗⟨⟩→ ⟨⟩⟨⟩具体说明：σ τ的尾部总是可以表征为两个流的乘积之和。在这里，我们将给出一个模式，允许任意条款建立可能属于某个类的几个运营商。我们再从一个具体的例子开始。5.1Hamming数从Dijkstra的[Dij81]（也由Sijtsma [Sij89]处理）中取一个例子这些数通常被称为汉明数（诚然，为了简单起见，我们省略了素数因子5）。类似于前面的例子，最终的SNI-余代数的载体，其中SNIX：=INX，是指自然数的无限流。我们将专注于使用辅助运算符merge（二元）和mapg（一元）对g：IN→IN进行以下指定：头，尾（火腿）= 1，合并（地图2（火腿），地图3（火腿））如果σ0<τ0，则合并（σJ，τ）如果σ0=τ0，则头，尾σ0，merge（σJ，τJ）如果σ0> τ0，则合并（σ，τJ）头，尾对于σ=σ0：σJ，τ=τ0：τJINω和函数2， 3：IN IN，使其参数加倍和三倍。将流ham视为函数ham：1INω，其中1 =是 一个单元素集合，可以尝试用λ-coiteration来定义它。其思想是使用函子T将集合X映射到由以下项自由生成的项集合：对应的运算符符号合并和映射G （g：IN→IN）对X和a分配律λ使这些项具有根据上面的merge和mapg的定义。然后，汉明数流应该作为由下式诱导的λ-迭代箭头出现：φ：= →1，merge（map （）、地图∗3（10）δ：1→SNIT1。我们将在余下的部分中在更一般的环境中研究这个模式这一节。5.2关于项的λ-重叠模式假设我们被赋予一个签名r，ar，即一组带有arity赋值ar：arityIN的运算符符号。设T，η，μ表示由该签名生成的项单子。 也就是说，TX是由X上的x，ar自由生成的项的集合（在这种情况下，我们有时称集合X为变量的集合），Tf通过应用f来重命名项中的所有变量，ηX将变量x∈X转换为项（我们通常将其应用隐式地保留），而μX：T2X→TX表示两级项。巴特尔斯83×⇒⇒→◦|◦∗∈∈为了在λ-余迭代中使用函子T，我们需要指定它与F的相互作用，即分配律λ：TF FT，或者使用3.4节末尾提到的推广，λ：T（IdF）英尺 我们将集中讨论后一种类型，因为这种方法的许多示例需要它所提供的更强的表达能力。假设我们被给定为一个分布的wλ。 L∈F，ωF∈F是一个最终的F-余代数，令[. ]表示从Tλ<$$>F，ωF<$到F，ωF 通过应用定理3.8，我们得到对于每个操作φ：X→FTX存在唯一的ωf：X<$F满足ωFf=Ff[[. ]]φ。在上面的例子中，这意味着火腿是一个独特的箭头，满足head（ham）= 1和tail（ham）=[[merge（map∗2（）、地图∗3（注）]]。 这是一个对于上述问题，我们需要[]。]根据以下条件评估术语对于（语义）运算符merge和mapg。具体而言，[. ]应该是合成的，即对于所有的σ∈T <$F，ti∈T <$F，我们问[[σ]]=σ和[o p（t1， . ，tn）]]=[o p（[[t1]]， . ，[[tn]]）]。可以证明，在λ自身是合成的情况下，我们得到了一个合成T-代数运算，这意味着它满足3.5节中所示的修改单位和乘法定律。这相当于说λ是从自然变换中(3)ρop：（Id× F）nπFT，对于每个算子符号op，ar（op）=n。然后[。]可以被独特地描述为是合成的和令人满意的ωF（[[o p（σ1， . . . ，σn）]]）=（F[. ]]）（ρo p（ωσ1，ωF（σ1）ω， . ，<$σn，ωF（σn）<$））。在我们的具体示例中，可以直接提出转换ρmerge和ρmapg，这样使用merge和图G满足这个特征。利用这一点，我们可以很容易地计算出上面的λ-coiterative箭头是满足原始规范的唯一箭头一般来说，该方法会产生唯一的解决方案的规格，涉及一组辅助运营商，可以捕获的自然变换如（3）中所示。这归结为说，对于每个算子op，op（σ1，.，σ n）可以通过只查看σ i <$F的直接观测值来确定，并且所包含的后继状态是在σ i、它们的直接后继状态或通过应用算子本身可以从这些状态到达的任何状态之中（这些限制是由于（3）中的自然性条件）。Turi和Plotkin [TP97]表明，这种类型的操作符指定与GSOS格式[BIM95]中的转换规则密切相关事实上，[。]通过应用相应的语义运算符来评估术语，也可以用于简化最终F-余代数：设B为表示给定关系的同余闭包B在所有算子下均为F×F，即包含B的最小关系对于所有运算符opwehav h a ttt p（σ1， . ，σn），op（τ1， . ，τn）<$∈B<$如果当1 ≤ i ≤ n时，<$σi，τi<$