初始代数和最终余代数的构成

可在www.sciencedirect.com在线获取理论计算机科学电子笔记341（2018）23-44www.elsevier.com/locate/entcs由非确定有限迹策略构成的初始代数和最终余代数内森·鲍勒1德国汉堡大学数学系保罗·布莱恩·利维2英国伯明翰大学计算机科学学院戈登·普洛特金3英国爱丁堡大学LFCS摘要我们研究执行I/O和有限或可数不确定性选择的程序，直到有限迹等价。对于有根据的程序，我们描述哪些策略（迹集）是可定义的，利用I/O与非确定性之间的交换性公理化迹等价。 这给出了作为半格上多项式内函子的初始代数的策略集。对应于非良基程序的策略构成了这个函子的最终余代数关键词：最终余代数，不确定策略，迹，代数项，半格1引言这篇文章是关于执行I/O的非确定性程序的。为了说明这些想法，让我们考虑以下（无限）命令式语言：1电子邮件：Nathan. uni-hamburg.de2电子邮件：P.B. cs.bham.ac.uk3电子邮件：gdp@inf.ed.ac.ukhttps://doi.org/10.1016/j.entcs.2018.11.0031571-0661/© 2018作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。24N. Bowler等人/理论计算机科学电子笔记341（2018）23defdefM，N：：=年龄？（Mn）n∈N| Happy?（男、女）|是否继续？（百万） | Byen| M或N其意义如下。• 命令年龄？（Mn）n∈N打印年龄？ 和停顿。 如果用户输入n，则执行Mn。• 快乐的命令？（M，N）打印快乐吗 和停顿。如果用户输入是或否，它分别执行M或N。• 命令Continue？（M）打印继续？和停顿。如果用户输入Yes，则执行M。• 命令Byen打印Byen并暂停。 无法进一步输入。• 命令M或N非确定性地选择执行M或N。一个游戏是一个输出和输入的交替序列，例如，快乐？Yes.Age? 93.Age? 27.Continue? Yes.Happy?一个命令比如让M0=快乐？再见，继续。（再见6））它有以下被动结束跟踪（即以执行暂停结束的跟踪）：开心了吗开心了吗是的再见3快乐？No. 再见5快乐？No. 是否继续？开心了吗No. 是否继续？是的再见6以及随后的活动结束轨迹（即，以程序执行结束的那些空场（Empty Play）开心了吗是的开心了吗No.开心了吗No. 是否继续？是的以下命令M1=快乐？（再见3，再见5）或快乐？3、继续？（再见6））具有与M0相同的轨迹，即这些命令是轨迹等价的（尽管不是双相似的）。自然会产生以下问题：N. Bowler等人/理论计算机科学电子笔记341（2018）2325∈(i) 给定一个对策集σ，在什么条件下σ是某个命令的迹集？(ii) 我们能给出迹等价的公理化理论吗？（参见[1，25]中过程等价的公理化分析。本文问题（ii）的答案出奇地简单：我们采用普通的或理论（交换性、结合性和幂等性），以及每个I/O操作与或交换的事实。举例来说Age（Mn）n∈N或Age（MnJ）n∈N为 年龄（Mn或MNJ）n∈N我们不仅给出了上述语言的结果，而且给出了一些变体的结果，我们现在将解释。该语言有两个部分-I/O和不确定性-并且每个部分都可以变化。(i) I/O部分由签名确定，每个操作都有一个指定的arity-一组参数索引。 上面的语言有四个I/O操作-Age，Happy，Continue和Bye-各自的arityN，{是，否}，{是}和。无论I/O签名是什么，我们的结果都是适用的用于生成语言。(ii) 我们可以包括形式为nNMn的命令。该命令非决定性地选择n∈N，然后执行Mn。在本文的第二部分（第6节）中，我们考虑了非良基程序行为，直到（有限）迹等价。我们看到，熟悉的对偶--有良基行为的初始代数与无良基行为的最终余代数--也出现在有限迹的设置这些结果的重要性通过它们与语义学的几个领域的联系而得以体现。集合和单子。I/O操作和不确定性选择是计算效应的例子。 一个集合的效应通常由集合[20]上的单子来描述，有时可以用一个简单的理论[21]来表示。我们的每一个效应组合都会在Set上产生这样一个单子，对应于模迹等价的程序，它也是I/O和非确定性单子的张量[3，6，7，13]。游戏语义学上述语言中的程序可以被看作是在玩一个游戏（图1），其中有一个主动位置（表示程序正在执行）和几个被动位置（表示执行暂停）。在游戏语义中出现的游戏可能有几个主动和几个被动的位置[19]。使用不同的术语：输出称为“P移动”，输入称为“O移动”。尽管如此，在研究有限迹的地方，可以使用相同的非确定性策略概念[8，9]，我们的结果描述了这些更一般的博弈的策略。余代数迹 的几个余代数解释 迹线 有 出现[10，15，16]。我们的叙述（尽管它没有对这些进行补充）具有包括输出和输入动作的新颖性。 我们在第7节中进行了简要的比较。26N. Bowler等人/理论计算机科学电子笔记341（2018）23FC正+ +活性输出（P移动）z被动t，位置输入（O型移动）位置年龄？开心了吗t，，n是的z轴等待年龄z_程序运行，等待幸福， 继续？是的再见没有等待决定是否继续完成nFig. 1. 程序与用户之间的博弈。确认我们感谢V.Vignudelli解释了分布之间互模拟的概念，并提出了与迹等价的联系2预赛2.1半格给定一个集合X，我们写PX为子集的集合，PfX为有限子集的集合，PcX为可数子集的集合。我们写X，我们写P+X为居住的（非空的）子集的集合，同样地写PX和PX。一个半格是一个偏序集（A，≤），所有的二元连接。 它是有界的，最小元，可数子集有上确界时的ω-半格，居住子集有上确界时的几乎完全半格，子集有上确界时的完全半格地图A半格的二分B是一个保持二元并的单调映射。有界半格的映射必须保持最小元素，ω-半格的映射必须保持可数连接，几乎完全半格的映射必须保持居住子集的上确界，完全半格的映射必须保持任意上确界。我们也可以描述一个半格，而不是像上面那样有势地描述它。 它在等式上是：一个集合A，它的二元运算是交换的、结合的和幂等的。一个正半格（A，≤）通过设置x∈y是x和y的连接。反之，一个方程半格（A，A）通过设x≤y，当x≠y =y时，给出一个适定性的半格。这些结构是相反的。半格之间的一个函数是方程半格的映射（即保持π），如果它是posetal半格的映射（即保持π），则它是半格的映射。是单调的并且保持二元连接）。继续方程式风格：• 有界半格是具有中立元的半格（A，N. Bowler等人/理论计算机科学电子笔记341（2018）2327n∈NFC克n∈Nn∈Nn∈Nn∈N• 一个ω-半格是一个半格（A，A），其中Aω<$A满足X轴yn=（x<$yn）x=xx n= x mx n（m ∈ N）一个更抽象的观点：半格的范畴是Eilenberg-Moore范畴对于集合上的单子P+。同样地，P+的ω-半格范畴，几乎完备半格范畴等2.2语言定义2.1(i) 一个签名由一个操作集合K组成，对于每个操作k∈K，一个参数索引集合Ar（k）。(ii) 签名（Ar（k））k∈K上的转移系由集合X和函数X组成：CUPk∈Ki∈Ar（k）X. 当（k，（yi）i∈Ar（k））∈ Ax时，我们构造了x ∈ Ar（yi）i∈Ar（k）.非正式的xk（yi）i∈Ar（k）意味着thatx输出k并暂停，如果用户随后输入i，则执行yi。对于续集，我们固定签名S=（Ar（k））k∈K。命令集由语法M，N：：=要求k？（M i）i∈Ar（k） | M or N这组命令构成了一个转换系统。 转换关系Mk（Ni）i∈Ar（k）归纳定义如下。Mk（N）MJk（N）ii∈Ar（k）要求？（Mi）i∈Ar（k）k（Mi）i∈Ar（k）M或Mjk（N）M或MJk（N）i∈Ar（k）i∈Ar（k）对于可数非决定性，我们扩展语法如下：M：：= ···|M nn∈N并包括操作规则MKn≠（Ni）i∈Ar（k） n∈NMnn∈NKn（Ni）i∈Ar（k）28N. Bowler等人/理论计算机科学电子笔记341（2018）23i∈in∈Nn∈Nn∈Nn∈Nn∈N定义2.2迁移系统（X，X）是• total当对所有x∈X，集合x∈ x是居住的• 确定性的，当对所有x∈X，集合x至多有一个元素• 有限不确定的，当对所有x∈X，集合x是有限的• 可数不确定的，当对所有x∈X，集合x是可数的• 当没有无限序列的跃迁时，xk0 00k1 1提议2.30<$（yi）i∈Ar（k0）yi0=x1<$（yi）i∈Ar（k1）· · ·(i) 作为一个过渡系统，这组有限不确定的命令是完全的、有限不确定的和有根据的。(ii) 可数不确定命令集作为一个转移系统，是完全的、可数不确定的、有根据的。证据我们通过M上的归纳证明了M是有限的/可数的和居住的，并且不存在从M的无限转移序列。Q2.3互模拟虽然在续篇中没有用到，但我们还是简单地看一下互模拟。定义2.4迁移系统（X，X）上的互模拟是一个关系R，Xsuc h，则xRxJ意味着，如果x=k，（yi）i∈Ar（k）则存在（yiJ）i∈Ar（k）suchxJ=k∈（yJ）Ar（k）且i∈Ar（k）. 你是我的，我是你的，我是你的。最伟大的互模拟被称为双相似性。例如，第1节中的命令M0和M1不是双向相似的。我们将双相似性公理化如下。定义2.5基本等价，记作“基本等价”，是满足半格定律的命令的最小同余：M或NN或M（1）（M或N）或PM或（N或P）（2）M或MM（3）此外，对于可数非确定性语言，ω-半格定律：M或Mn（M或Mn）（4）（5）M nMm或Mn（m∈N）（6）N. Bowler等人/理论计算机科学电子笔记341（2018）2329[4]参见良基余代数的概念[2，24]。30N. Bowler等人/理论计算机科学电子笔记341（2018）23==Σ命题2.6对于有限和可数非确定性语言，基本等价性是双相似性。证据关于双相似性的归纳表明，双相似性蕴涵着双相似性，并且它是一个双模拟。Q2.4痕迹与策略我们关于交互作用的基本概念如下。定义2.7博弈是一个序列k0，i0，k1，i1，. 其中kr∈K，ir∈Ar（kr）. 它是主动结尾、被动结尾或无限结尾，根据它的长度是偶数、奇数或无限。如第1节中的M0和M1所示，如果两个命令具有相同的被动结束跟踪，则它们是跟踪等效的;主动结束跟踪是冗余的。这激发了以下动机。定义2.8(i) 一个非确定性的有限迹策略是一个被动结局策略的集合σ，使得sik∈σ蕴涵s∈σ。(ii) 当σ为ε（空局）或si对于s∈σ。Henceforth定义2.9设（X，λ）是一个转移系统，x∈X。 A play k0，i0，. 是一有序列时x的迹x=xk000k1 10<$（yi）i∈Ar（k0）yi0=x1<$（yi）i∈Ar（k1）· · ·由x的被动结尾迹组成的策略记为迹x。显然，x的主动结尾轨迹是轨迹x所实现的播放。相比之下，无限迹一般不能从迹x导出。例如，在语言的非良基扩展中，def0def1是否继续？n（再见3）或继续ωn∈N是否继续？n（再见3）n∈N“行，行。是的ω是N0的迹，而不是N1的迹。这不可能发生在一个有根据的系统中，因为没有无限的痕迹。它也不可能发生在一个有限的非确定性系统中，因为下面是柯尼希引理的翼形变化。命题2.10对于一个有限的非确定性系统：XCUPk∈Ki∈Ar（k）X且x∈X，是一个无限对策k0，i0， . . 是x的一个trace，则它的所有被动结尾前缀都在迹x中。NNN. Bowler等人/理论计算机科学电子笔记341（2018）2331defdefn∈Nn∈Nn∈Nn∈Nn∈Nn∈N让我们来看看一些有用的操作策略。首先，我们把策略放在一起如下。定义2.11对于k∈K和一族策略（σi）i∈Ar（k），我们定义策略要求？（σ i）i∈I={（k）}<${k.i.s |i ∈ Ar（k），s ∈ σ i}命题2.12在命令上，我们可以按组成给出迹：要求跟踪？（M i）i∈Ar（k）=要求？（迹M i）i∈Ar（k）痕量（M或N）=TracesM TracesN迹线M n=迹线M n其次，我们分解策略如下。定义2.13设σ是一个策略。 对于k∈K的集合，我们写Initσ，使得（k）∈σ。对于每个这样的k和每个i∈Ar（k），我们定义策略σ/ki={s| k.i.s∈ σ}。3有理有据的行为3.1通勤等值我们从公理化迹等价开始。正如我们将看到的，适当的公理化如下。定义3.1交换等价，写为等价，是满足半格定律（1）和或：要求？（M i aorN i）i∈Ar（k） =要求k？（M i）i∈Ar（k） 或要求？（N i）i∈Ar（k）（k∈K）（7）对于可数非确定语言，证明了ω-半格律（4）-（6）和Req k？以及：要求？（一）M i，n）i∈Ar（k）= 要求？（M i，n）i∈Ar（k）（k ∈K）（8）例如，第1节中的命令M0和M1是交换等价的。命题3.2（合理性）如果M ≠cN，则迹线M =迹线N。证据这是证明归纳法;健全的法律如下命题2.12。举例来说要求？（一）σ i，n）i∈Ar（k）={k}<${k.i.s|i∈Ar（k），s∈σ i，n}要求？（σi，n）i∈Ar（k）=（{k}{k.i.s|i∈Ar（k），s∈ σ i，n}）n∈Nn∈N32N. Bowler等人/理论计算机科学电子笔记341（2018）23FC∈n∈N+因为N是有人居住的所以它们是相等的 所以（8）是正确的。Q现在我们将证明完备性，即命题3.2的逆命题。我们使用以下内容。引理3.3对于每个命令M，McReq k？（Nk，i）i∈Ar（k）k∈L对某些L∈PK和命令族（Nk，i）k∈L，i∈Ar（k）.对于可数不确定语言，L∈ P+K。证据诱导M。如果M=Reqk？（Nk，i）i∈Ar（k）是明显的.在M =n∈NMn的情况下，我们有Mn <$ck∈LnReqk？（N n，k，i）i∈Ar（k）. 然后Mnc要求？（Nn，k，i）i∈Ar（k）n∈Nn∈N，k∈Ln布拉奇要求？（Nn，k，i）i∈Ar（k）是否需要？（一）k∈n∈NLnNn，k，i）i∈Ar（k）对于M=M0或M1的情况也是如此。Q我们的完备性证明通过刻画迹包含来进行，当迹M<$迹N时，将M与N联系起来的预序。命题3.4当M或N <$cN时，写作M ≤ c N。(i) C是一个前序。(ii) M或N是M和N的最小上界(iii)是（Mn）n N的最小上界。(iv) 或者n∈N和Reqk？对k∈K，都是单调的，即≤c是一个预收敛。证据第（i）-2.1节中的半格。最小上界性质证明了或和 n∈N的单调性。Reqk的单调性如下（7），因为后者可能被视为说，要求k？是方程半格的映射，因此也是posetal半格的映射。Q命题3.5 M ≤cN i Traces M Traces N.证据（1）由命题3.2引出。我们在M上用归纳法证明了（？）当M=M0或M1和M=n∈ NMn时，由最小上界性质可得.假设M=Reqk？（Mi）i∈Ar（k）.引理3.3给出Nck∈LReqk？（Nk，i）i∈Ar（k），所以k∈n∈NLnn∈N：k∈Lnn∈N：k∈LnN. Bowler等人/理论计算机科学电子笔记341（2018）2333要求跟踪？（M i）i∈Ar（k）<$TracesReq k？（Nk，i）i∈Ar（k）k∈L即要求k？（迹Mi）i∈Ar（k）<$Reqk？（迹Nk，i）i∈Ar（k）k∈L因此k∈L，对于每个i∈Ar（k），我们有迹Mi<$迹Nk，i意味着通过归纳假设得到Mi≤cNk，i因此M=要求k？（Mi）i∈Ar（k）≤c要求k？（Nk，i）i∈Ar（k）≤ck∈LReqk？（Nk，i）i∈Ar（k） NQ推论3.6 M cN i Traces M = Traces N。3.2有限非决定论现在我们将描述对于一个有限的非确定性命令M，哪些策略具有迹M的形式。我们还给出了第二个完整性的证明，直接在这个意义上，不涉及跟踪包含（但它似乎不适应设置可数非决定论）。我们考虑以下关于策略的条件定义3.7设σ是一个策略。(i) 对于使能的策略s，对s的响应是操作k∈K，使得sk∈σ。(ii) σ是一棵树，当每个被启用的策略都有唯一的响应时。(iii) 当每个启用的播放至少有一个响应时，σ是总计(iv) σ是确定性的，或部分树，当每个启用的播放最多有一个响应。(v) σ是有限不确定的，当每一个被允许的策略只有有限多个响应时。(vi) σ是有限成立的，当它是有限不确定的，没有无限游戏在σ中有所有被动结尾的前缀。具有后一种性质的树或部分树也称为良基树。让我们用例子来说明这些条件。• 以下战略是完全建立的：开心吗？开心吗？是的再见3，快乐？是的再见它不是总的，因为启用播放快乐？No. 没 有反应。34N. Bowler等人/理论计算机科学电子笔记341（2018）23我• 以下是总体战略：开心吗？开心吗？是的再见3，快乐？是的Bye5}开心吗？No. 再见|n∈ N}它不是绝对不确定的，因为启用的游戏快乐吗？No. 有很多答案。• 下面的策略是完全和有限不确定的：开心吗？开心吗？是的再见3，快乐？是的再见开心吗？No. （继续？是的）n继续吗？ | n ∈ N}它不是无限的，因为无限的游戏快乐吗？No. （继续？是的）ω具有 所有的被动结尾前缀命题3.8设（X，λ）是一个转移系统，且x∈ X。(i) 如果m是total，那么轨迹x也是total。(ii) 如果x是确定性的，那么迹线x也是确定性的。(iii) 如果x是无限不确定的，那么迹x也是无限不确定的。(iv) 如果x是有限不确定的和有根据的，那么迹x是有限有根据的。证据轨迹x启用的播放是x的活动结束轨迹。对于（i），我们证明了每个这样的迹s都有一个响应，通过s上的归纳。 s=ε的情况是eas y，且如果s=k。I. 则有zsuc h使得s=k<$（yi）∈Ar（k）且z=yi和sJ在轨迹z中有响应，所以k.i.sJ在轨迹x中有响应。（2）（3）（4）（5）（6）（7）（8）（9）（10）（11）（12）（13）（14）（15）（16）（17）（19）（10）（11）（12）（11 第（四）部分来自命题2.10。Q让我们来谈谈决定论碎片。命题3.9确定性命令，由文法M：：=Reqk？（M i）i∈Ar（k），通过M<$→迹M对应于良基树。3.10对于每一个被建立的， 总策略σ我们有σ=轨迹M，对于某个命令M，直到100c都是唯一的。证据对于一个有限成立的全策略σ，令P（σ）断言σ =迹M，对于某个命令M，直到σc是唯一的。我们将证明，k∈Initσ。P（σ/ki）蕴涵P（σ）。这暗示了我们的结果，因为否则相依选择给出了一个无限迹，它的被动结尾前缀都在σ中。对于每个k∈Initσ和i∈Ar（k），假设P（σ/ki），所以我们选择一个命令Nk，i使得迹Nk，i=σ/ki.然后我们有迹线k∈Initσ要求？（Nk，i）i∈Ar（k）=k∈Initσ要求？σ/ki=σN. Bowler等人/理论计算机科学电子笔记341（2018）2335nn对于唯一性，假设σ=迹M。引理3.3给出McReqk？（NkJ，i）i∈Ar（k）k∈L因此，σ=迹线M=T种族要求k？（NkJ，i）i∈Ar（k）k∈L=要求k？（T族NkJ，i）i∈Ar（k）k∈L因此，L = Init σ，对于每个k ∈ Init σ和i ∈ Ar（k），我们有迹NJ= σ/ki，给出Nkj，i∈cNk，ibyyh p。所以McReqk？（NkJ，i）i∈Ar（k）k∈L是否需要？（Nk，i）i∈Ar（k）k∈LQ推论3.11一个策略的形式为迹M，对于一个有限不确定的命令M，如果它是完全的和有限成立的。最后，我们得到了完备性的第二个证明：如果迹M=迹N=σ，则M<$cN。3.3可数不确定性对于可数非确定性语言，我们再次想刻画那些形式为迹M的策略σ。正如我们经常观察到的那样，情况与定义3.7（vi）不同：我们不能排除一个无限游戏在σ中具有所有被动结尾前缀。例如，命令n∈NContinuen（Bye3）具有跟踪集{（继续？是的）继续？ |n ∈ N}<${（继续？是的）再见|n ∈ N}（9）每一个人，都有自己的故事，都有自己的故事，都有自己的故事。是）ω。正如我们将要看到的，适当的条件如下。定义3.12设σ是一个策略。(i) σ是可数不确定的，当每一个使能的策略都有可数多个响应时。(ii) 对于使能策略s，对s的响应树是树τ，使得对于所有t∈τ，s和t的级联在σ中。(iii) 当每个使能的策略都有一个有理有据的响应树时，σ是有理有据的总体。（参见[18][19]我们举例说明这些条件。36N. Bowler等人/理论计算机科学电子笔记341（2018）23n⇒∈∈我0我0⇒我1in−1• 在我们的签名示例中，K是可数的，因此每个策略都是可数的。• 策略（9）是完全有根据的。• 以下是总体战略：{Bye3}{（继续？是的）是否继续？ | n ∈ N}这是没有充分的总，因为启用播放继续？是的没有良好的响应树。命题3.8的对应部分如下。命题3.13设（X，λ）是一个转移系统，且x∈ X。(i) 如果x是可数不确定的，那么迹x也是可数不确定的。(ii) 如果X是可数不确定的、完全的和有根据的，则迹x是有根据的完全的。证据第（i）部分类似于命题3.8（iii）。为了证明部分（ii），我们首先选择，对于每个z∈X，一些R（z）∈π z。任何策略k0，i0，. k n-1，i n-1由迹线x启用是x的迹线，即有一个序列x=x0k0（y0）i∈Ar（k）y0 =x1k1（y1）i∈Ar（k）···yn−1 =xn良基全确定系统（X，z→ {R（z）}）中的xn的迹集是k0，i0，...的良基响应树， kn-1，i n-1.Q定理3.14一个策略σ的形式为迹M，对于某个命令M，i，它是可数不确定的和完全的。证据 （1）由命题3.13引出。 对于（1），我们如下进行。 对于n∈N，我们将策略k0，i0，.，k m m< n。σ的一个n-逼近是一个命令M，使得σPlaynTracesMσ通过对n的归纳，我们证明了对所有n∈N，每个可数不确定的完全良基策略σ都有一个n-逼近.• 为了证明它对0是真的，设τ是对ε的树响应，那么相应的确定性命令（命题3.9）是σ的0-近似。• 假设n为真。对任意k∈Initσ和i∈Ar（k），设Mk，i是σ/ki的n-逼近.集合Initσ是可数的，是对ε的响应的集合。所以k初始化σ要求k？（Mk，i）iAr（k）是σ的（n + 1）-逼近。对于每个n∈N，设Mn是σ的n-逼近.则迹n∈NMn=σ.QN. Bowler等人/理论计算机科学电子笔记341（2018）23374初始代数4.1签名的初始代数本节的目的是以一种不提及语言的方式重新构建我们的结果回想一下，S是我们的签名（Ar（k））k∈K。以下是众所周知的。定义4.1(i) 一个 S-代数 组成 的 一 设置 X并且，在本发明中， 为 每个 K∈K，的函数θk：i∈Ar（k）X第十章(ii) S-代数同态（X，（θk）k∈K）<$（Y，（φk）k∈K）是一个函数f：X<$Y满足f（θ k（xi）i∈Ar（k））= φ k（fxi）i∈Ar（k），对所有k∈K.这导致了一个标准的结果：命题4.2具有（Reqk？）k∈K是初始S-代数。我们的目标是以类似的方式将非确定性和I/O结合起来。我们将定义4.1推广如下。定义4.3设C是一个有乘积的范畴。(i) C中的S-代数由X∈ C和对每个k∈K的一个态射θk：i∈Ar（k）X第十章(ii) S-代数同态（X，（θk）k∈K）<$（Y，（φk）k∈K）是一个态射f：XYsuc hthati∈Ar（k）θkXi∈Ar（k）fi∈Ar（k）Yφk为所有人k∈K。XCYcF我们现在用公式表示有限非决定论的结果，不提语言。定理4.4(i) 对于一个策略σ，以下是等价的：• σ=迹x，对于一个有根据的、有限不确定的全系统的某个元素x。• σ是有限成立的和完全的。(ii) SL（半格范畴）上的初始S-代数是由有限成立的全策略集给出的，全策略集按包含序，（Reqk？）k∈K。证据(i) （1）命题3.8。 （1）由命题3.10引出。38N. Bowler等人/理论计算机科学电子笔记341（2018）23(ii) 半格中的S-代数由半格（X，X）和族函数θk：i∈Ar（k）X的（θk）k∈K半格：X是（equa-）的同态θk（xi<$yi）i∈Ar（k）=θk（xi）i∈Ar（k）<$θk（yi）i∈Ar（k）一个同态是一个函数保持θk和θk对所有k∈K。因此，半格中的初始S-代数是由有限不定命令的类给出的.根据命题3.10，这些策略对应于有确定基础的总体策略。Q同样，我们有以下内容。定理4.5(i) 对于一个策略σ，以下是等价的：• σ =迹x，对于一个良基的可数非决定的全系统的某个元素x。• σ是可数的不确定性的和有充分根据的总和。(ii) ωSL（ω-半格范畴）上的初始S-代数由可数不确定的、有充分基础的全策略集给出，按包含序，（Reqk？）k∈K。几乎完全半格的概念（2.1节）给出了另一个变体：定理4.6(i) 对于一个策略σ，以下是等价的：• σ=迹x，对于一个良基全系的某个元素x。• σ是完全有根据的。(ii) 几乎完全半格范畴上的初始S-代数是由包含序下的完备全策略集给出的，其中（Reqk？）k∈K。证据设C是良基全策略的集合。设λ为λ0的最大值，C和K的基数。因此，对于任何策略σ，每个使能策略都有≤λ的反应。将可数不确定语言推广为λ元不确定选择i<λMi，得到了与定理4.5类似的结果. 因此，每个策略都是针对某个命令M的迹M，给出部分（i）。假设一个λ-半格是一个半格，其中每个大小≤λ的居住子集都有一个上确界，而同态是一个保持这些上确界的函数则C构成λ-半格中的初始S-代数 设A是几乎完备半格中的S-代数，f：Cλ-半格中S -代数的唯一同态。任何居住的RC有基数≤λ，所以它的上确界被f保持。因此f是几乎完备半格的同态。QN. Bowler等人/理论计算机科学电子笔记341（2018）2339Σj∈JFj∈Jj∈JΣ（U，（aj）j∈U）到j∈Ufjk∈K(i)函数Φ：φL∈PKk∈Li∈Ar（k）StratStrat发送4.2闭函子的初始代数回想一下，定义4.3适用于任何C类产品。若C也有余积，则C中的S-代数是闭函子k∈Ki∈Ar（k）的代数.我们的每一个范畴-半格、ω-半格和几乎完全半格-有允许简单显式描述的余积。命题4.7设（Aj）j∈J是一族半格。(i) SL中的交路fAj是对（U，（aj）j∈U）的集合，其中U∈P+J且每个aj∈Aj。当U≠V时，则（U，（aj）j∈U）≤（V，（bj）j∈V且aj≤bj，其中allj∈U. 对于j∈J，则ej满足ej：Ajsends是a›→（{j}，（a）j）。j∈JAj(ii) 对于有限居住集L，fAj中的L-指标上确界由下式给出：（Ul，（al，j）j∈Ul） =（V，（bj）j∈V）l∈L其中reV=l∈LUl，bj=l∈L：j∈Ulal，j.(iii) F或一族半分ce同态（fj：Aj<$B）j∈J，二元组s结束我们同样描述一个副产物cωSL中的一个j，和一个余积j∈J 在ACSL。让我们用这些术语重新表述定理4.4我们将使用下列结构。定义4.8让Strat是所有策略的集合。（L，（（σk，i）i∈Ar（k））k∈L），(ii)函数名：Stratk∈LReq k？（σk，i）i∈Ar（k）.<$L∈PKk∈L i∈Ar（k）Strat发送σ到（Initσ，（（σ/ki）i∈Ar（k））k∈Initσ）.注意，Φ和Φ是相反的。还记得Lambek定理4.9(i) 初始fi∈Ar（k）《易经》云：“君子之道，焉可诬也？有始有终。全策略，按包含排序，具有结构u<$→Φu，其逆为σ→ σ。(ii) 对于ω-半格也是如此，使用可数不确定的、有充分根据的全策略。(iii) 几乎完全半格，使用well-foundedly全策略。证据第一部分是定理4.4（ii）的重述。通过命题4.7（iii），（Reqk？）k∈K是u<$→Φu。第二至第三部分也是如此。Q40N. Bowler等人/理论计算机科学电子笔记341（2018）23j∈J∈¸Bj∈Jk∈Kk∈Kj∈Jk∈K对于所有的j∈J. 显式地，g发送（U，（aj）j∈U）tooj∈Ufj（aj）。我们已经有了这类代数的范畴就是我们理论的模型范畴Q5中性元素假设我们在我们的语言中添加一个没有转换的命令骰子• 为了刻画可定义性，我们放弃了总体性和有根据的总体性的条件。因此，一个策略是可以由一个无限不确定的命令来定义的，如果它是无限成立的。它可以由一个可数不确定性命令来定义，如果它是可数不确定性的。• 为了表征迹等价，我们在迹等价的定义中增加了以下等式：M或模具这是唯一需要的改变Reqk？和死亡，即要求？（die）i∈Ar（k）=die，必须省略，因为它是不合理的。我们希望将有限有界策略集视为上的初始代数，BSL（有界半格范畴我们这样做使用以下的骗局-结构。 对一族半格（Aj）j∈J，有界半格fA j与命题4.7相同，但包含空集;因此它由对（U，（aj）j∈L）组成，其中ithU∈PfJ。它满足了以下通用特性：有界半格B和半格映射族（fj：Aj<$B）j∈J，存在一个唯一有界半格映射g：njJAjBsuchthatAjejj∈JG表示“共同”之义FJzC函子j∈J ：BSLJSLandf：SLJBSL定理5.1初始fi∈Ar（k）BSL上的-代数由以下集合给出：有限成立策略，按包含排序，结构为u<$→Φu，其内部是的，是的。证据 一fi∈Ar（k）- 代数可以描述为有界半格Ai∈A r（k）A <$A）k∈K。THE同样地，对于有界ω-半格范畴，记为BωSL，我们定义函子j∈J ：BωSLJ <$ ωSL和c <$：ωSLJ<$BωSL.则该组可数不确定性策略形成了一个初始条件，i∈Ar（k）- 代数上BωSL。同样，对于完备半格范畴，我们定义了函数CSL函数j∈J：CSLJ<$ACSL和函数j∈J：ACSLJ<$CSL。然后，所有策略在CSL上形成一个n个初始的Kk∈Ki∈Ar（k）-代数。与一族（单纯）半格映射（fk：N. Bowler等人/理论计算机科学电子笔记341（2018）2341ΣΣk我所有树的集合都是一个最终集合，i∈Ar（k）-余代数。我们将看到k∈K6无充分根据 行为6.1最终余代数到目前为止，我们已经刻画了良基系统中某些元素x的迹x形式的策略我们现在转向非良好基础的系统。回想一下，只要as，fwell-founded树的集合就形成了n初始k∈Ki∈Ar（k）-非确定性系统也会出现类似的现象我们只处理不受限制的情况。如果需要的话，强制执行有限或可数的非决定论和/或强制执行总体性命题6.1每个策略σ都是转移系统（X，λ）中某个元素x的迹x的形式。证据 考虑系统：StratP k∈Ki∈Ar（k）Strat，其中： σ<$→ {（k，（σ/ki）i∈Ar（k））|k∈Init σ}然后，通过归纳法将迹σ=σ覆盖，分离情况（k）和k.i.sJ。Q我们的第一个目标是证明斯特拉特形成了一个最终的目标，完全半格范畴CSL∈Ki∈Ar（k）-余代数定义6.2设（A，λ）是CSL上的一个λk∈Ki∈Ar（k）-余代数. 对于a∈A， ar的迹是策略k0，i0，. 使得a= a0 n（a0）=（L0，（（b0b0=a1 n（a1）=（L1，（（b1）i∈Ar（k））k∈L0）k0∈ L0）i∈Ar（k））k∈L） k1∈ L1k0，i0···k，i1由a的被动结尾迹构成的策略记为迹a。定理6.3CSL上的代数A的最终结果k∈ Ki ∈Ar（k）-co代数a由Strat，orderd给出结构为σ <$→ φ σ，其逆结构为u <$→ Φ u。独特的煤-从（A，λ）到最终余代数的bra态射是a→迹a。证据归纳超过播放，分离的情况下（k）和k.i.sJ。Q42N. Bowler等人/理论计算机科学电子笔记341（2018）23∈j∈J定理6.3缺少的是映射x→迹x的特征一个过渡系统。 接下来我们使用以下概念给出这个。定义6.4给定一个函数族（Xj<$Aj）j∈J，其中Xj是一个集合，Aj对于几乎完全半格，我们记为：j∈J XjJAj代表