可在www.sciencedirect.com在线获取理论计算机科学电子笔记352（2020）5-27www.elsevier.com/locate/entcs纤维化中的最弱前提Alejandro Aguirre亚历杭德罗·阿吉雷1，2IMDEA软件研究所UniversidadPolit'ecnicadeMadridCampusdeMontegancedo，28223PozuelodeAlarc'on，Madrid，S painShin-ya Katsumata胜也1，3国立信息学2-1-2 Hitotsubashi，Chiyodaku，东京都，日本摘要最弱前提转换器是程序验证中的有用工具。它们的关键特性之一是组合性，也就是说，与程序f;g相关联的最弱前提谓词Transformer（简称wppt）应该等于与f和g相关联的wppts的组合。 在本文中，我们从虚构的角度研究了wppts背后的范畴结构。 我们描述了wppts满足组合性的，如从单子的笛卡尔提升构造的。此外，我们表明，笛卡尔提升单子沿宽松片范畴双射对应于Eilenberg-Moore单调代数。然后，我们实例化我们的技术，通过推导常见的事件，如可能单子，非空幂集单子，计数器单子或分布单子的wppts。我们还展示了如何将它们结合起来，推导出出现在概率程序验证文献中的wppts。关键词：最弱前提谓词Transformer，单子，计算效应，纤维范畴理论，霍尔逻辑。1介绍Dijkstra当强制程序f总是终止并且只确定性地更新存储器时，f的最优值可以被建模为存储器集合M上的内函数[f]1本研究得到了ERATO HASUO Metamathematics for Systems Design Project（No.JPMJER1603），JST的资助。这项研究是在第一作者访问国家研究所期间进行的信息学。作者感谢Satoshi Kura对本文的详细评论，并感谢匿名评论者仔细阅读我们的手稿和建设性的反馈。2电子邮件：alejandro. imdea.org3电子邮件：s-katsumata@nii.ac.jphttps://doi.org/10.1016/j.entcs.2020.09.0021571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。6A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）5→→⇒ −×最弱谓词P被定义为使得[P]]<$M（满足P的存储器配置）对应于[Q]<$M的逆像，[[f]]。谓词转换器的一个关键属性使其适合于程序验证：组合程序f;g的最弱前提条件wp（f;g，Q）等于其组件的最弱前提条件的组合，即wp（f，wp（g，Q））。这允许谓词转换器被定义并归纳应用于程序的结构在Dijkstra的开创性工作之后本文的动机是确定这些类似wppt的语义变体背后的数学结构为了实现这一目标，在本文中，我们着手研究wppts及其在纤维中的可合成性。 粗略地说，纤维化是一个函子p：P→C，谓词范畴P与底层范畴C建模计算之间的关系-当pP=X成立时，我们将P∈P视为X∈C上的谓词;这一观点与精化类型的范畴研究相同[30]。纤维化特别适合于解释谓词变换及其可组合性，这要归功于笛卡尔提升属性，它允许我们沿着C中的态射f：X → pQ取Q ∈ P的f<$Q∈P使得p（f<$Q）=X.这是逆图像操作的分类抽象。我们现在考虑扩展命令式编程语言（其程序被建模为M M类型的函数）及其Hoare逻辑。 4以一元风格给出两个系统的指称语义[32] ，我们使用C上的一对单子T和T子P，使得p严格预-服务于单子结构-后者被称为T沿着p的提升。然后我们把PTstecas中的态射看作Hoare三元组的解释。这会引起一种自然的wppt描述了Hoare三元组的特征，但它不满足可组合性，总的来说。这就提出了一元计算何时会导致组合谓词转换器的问题。在本文中，我们通过引入单子提升的Cartesian-ness属性来回答这个问题，并对它的理解做出如下贡献：(i) 我们证明了使用单子提升定义的wppt是可组合的当且仅当单子提升是笛卡尔的。这一结果建立了一元环境下wppts的可组合性与提升的笛卡尔性(ii) 我们研究笛卡尔提升单子沿域纤维从宽松切片类别。对于这类映射，单子T的笛卡尔提升与Eilenberg-Moore单调代数4这里的副效应是指那些不能被M M类型的存储器更新函数建模的副效应，例如输入、输出、非确定性选择、概率性选择以及操纵外部存储器设备。最后一个可以由状态单子S（S）建模，该状态单子S（S）采用独立于M取得的状态集合S。A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）57这是通过切片对象上的代数范畴（具有变化的内函子）与域纤维化之间的纤维函子范畴之间的么半群同构表现出来的这一结果简化了探索单子沿着这样的纤维化的笛卡尔提升的任务。我们还将最强后置条件谓词转换器作为wppts的左伴随，并讨论它们何时在域fibrations中可用(iii) 计算效应通常由复合单子通过分配律来建模。我们将（ii）中给出的对应推广到复合单子和满足[4，27]中给出的一个额外相干律的Eilenberg-Moore单调代数对的笛卡尔提升。这种对应提供了一个模块化的方法来计算复合单子的笛卡尔提升(iv) 为了计算包含有效命令（如概率选择和计数）的程序的wppts，我们研究了Plotkin和 Power(v) 除了域纤维化之外，我们还举例说明了单子沿着关系纤维化的笛卡尔提升。他们在[11]和[13]中提出的框架之外。这些研究使我们能够从它们的代数中定义单子的提升（因此，wppts），以及通过组合单个代数来定义复合单子的变换我们通过在文献中定义monad的谓词变换来说明这一点：maybe monad，非空幂集monad，计数monad，分布monad和索引分布monad。然后，我们将展示如何结合这些来恢复文献中的谓词变换器，例如Kaminski等人的预期运行时变换器[16]和高阶矩Transformer由Kura等人。[21]第20段。2预赛函子的合成、函子的whiskering[42]和自然变换用并置表示。自然变换的垂直和水平组合分别用*和*我们省略了单子的定义，单子的Eilenberg-Moore（简称EM）代数和单子的Kleisli范畴;见例如。[24，第六节]。 设（T，ηT，μT）是范畴C上的单子. f：X→TY的Kleisli提升为f#T=ΔμTY<$T. WHEN从上下文来看，T是显而易见的，我们简单地写f#来表示f#T。Kleisli类别T的表示为CT，其中的组合表示为·。C和CT之间的邻接称为T的Kleisli分解。继[32]之后，我们把CT中的态射看作是引起计算效应的程序的抽象表示。设（S，ηS，μS）是C上的另一个单子. 一个分配律[4]SoverT是一个自然变换α：ST → T S，使得ηTS= αSηTαSμT= μTST α αTηS= αηSTα μST = T μSαSSα8A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）5分配律产生复合函子上的单子（T S，ηT<$ηS，（μT<$μS）*（TαS））。 We用T∈αS表示这个单子。2.1纤维化Dijkstra然而，在谓词变换的抽象研究中，扩展谓词的概念是很方便的，这样它们就可以定义在范畴上的任意对象上。对于谓词的这种抽象和一般的处理，我们利用纤维范畴理论的概念（参见例如[14]）。在介绍这些概念之前，我们对它们作一个非正式的说明给定一个范畴C（其对象用字母X、Y、Z表示），我们的目标是通过引入一个范畴P（其对象用P、Q、R表示）和一个函子p：P→C来定义其对象上的谓词。我们对这一一般情况的理解如下：• P中的一个宾语是C中某个宾语之上的一个谓词，它由函子p记录：P→C。也就是说，pP=X意味着P∈P是X∈C上的谓词。• P中的态射f：P→Q证明了C中的基本态射pf：pP→pQ 特别是如果f：P→Q满足pf= idX，则f证明P蕴涵Q。对于一个对象X∈C，在函子p：P→C下的逆象形成一个用PX表示的范畴，称为X上的纤维范畴。 形式上，一个P X的对象是P-对象P∈P使得pP=X，从P到Q的PX-态射是P-态射f：P→Q使得pf=idX. 本分类的对象 是X上的谓词，态射见证了它们之间的含义在最弱前提谓词变换器的基础上，谓词的强度通过一个顺序关系进行比较，因此我们将注意力集中在定值上。回想一下，最弱的前置条件谓词Transformer收集了所有需要后置条件的内存配置。从集合理论上讲，这种操作称为逆像，而纤维化则是对逆像的更一般和更灵活的处理。粗略地说，纤维化是一个函子p：P→C，使得对于任何f∈C（X，Y）和P∈PY，我们可以找到P沿f的逆像f<$P∈PX。后文给出了定态纤维化的正式定义• 对于对象P，Q ∈ P和一个态射f ∈ C（pP，pQ），我们定义f上P -态射的集合Pf（P，Q）为Pf（P，Q）={k∈P（P，Q）|pk = f}。• 一个态射k∈P（P，Q）是笛卡尔的，如果对任意R∈P和h∈C（pR，pP），k的后复合被看作是Ph（R，P）→Ppk<$h（R，Q）型函数，双射这是笛卡尔态射的普适性质。笛卡尔态射k：P→Q抽象地表示P是Q沿pk的逆像的情形。• 一个函子p：P→C是一个纤维化，如果对任何f∈C（X，Y）和Q∈PY，存在一个对象P∈PX和一个称为笛卡尔态射的笛卡尔态射k∈Pf（P，Q）A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）59∗→f与Q的提升• 一个纤维化p：P→C是posetal的，如果每个纤维范畴PX是偏序集。在任意的定态纤维化中，f∈C（X，Y）的笛卡尔提升（其中Q∈PY）唯一存在;因此我们用fQ表示它，用fQ表示它的定义域。我们注意到，姿态化是忠实的。 由此，P中的态射f：P Q是笛卡尔的当且仅当P =（pf）<$Q。• 对于f∈C（X，Y），赋值Q∈PYf<$Q∈PP扩张到函子类型PY→PX，我们称之为重索引函子。 赋值f<$→f<$进一步满足（idX）= idPX和（g<$f）=f<$$>g<$。一个介于定值泛函p：P→C和q：Q→D之间的泛函是一对F：C→D和Fstec：P→Q的函子，使得q<$Fstec=F<$p，且Fstec保持笛卡尔态射这等价于：对任意对象P∈P和C中的态射f：X→pP，Fstec（f<$P）=（Ff）<$（FstecP）。从p：P→C到q：Q→D的G iventwoffered函子（F，Fstec），（G，Gstec）对自然变换α：F→G和αstec：Fstec→Gstec，qαstec=αp. THE2-由这些数据确定的类别由Pos-Fib表示。我们说一个2胞腔（α，αstec）是笛卡尔的，如果FstecP=αpP（GstecP）. Pos-Fib（p，q）的子范畴记为Pos-Fibc（p，q）.进一步的限制posetalfibrations是可能的。设K是偏序集和单调函数范畴Pos的一个子范畴K纤维化p：P→C是一个定态纤维化，使得每个纤维范畴PX和每个重索引函子f都属于K。从K纤维化p：P → C到另一个P纤维化的K纤维函子（F，Fstec）一个q：Q→D是从p到q的一个纤维函子，使得F的极限为每个纤维PX成为K中PX→QFX型的态射。 我们将K-Fib写为Pos-Fib的子2-类别（分别为。Pos-Fibc）其中0-cell是K-纤维化，1-cell是K-纤维函子。2细胞保持不变。3Dijkstra结构和最弱预条件Pred-icate变压器在前一节中，我们已经看到了如何定义范畴C上的谓词范畴P。接下来，我们将由一些单子T建模的计算效应添加到这种情况中。我们的目标是对一元计算f：X→ TY尊重前置条件和后置条件的陈述进行建模，前置条件和后置条件分别作为X和Y上的谓词给出为此，第一步是定义T提升为单子T转移在P.定义3.1设p：P→C是定态纤维化，（T，η，μ）是上的单子C. 一个满足pTtec=Tp，pηtec =ηp和pμtec=μp的monad（Ttec，ηtec，μtec）onP称为a提升T （沿p）。 我们说，解除是：• 如果（T，Tstec）是从p到p的纤维函子，且• 笛卡尔坐标系，如果它是纤维化的和μTstecTstecP= μπιpPTstecP。和ηstecare笛卡尔，即P=ηp<$P（TstecP）和nd单子提升的概念并不新鲜;它是作为语义对应物出现的10A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）5的逻辑关系单子[7，8，10，17，18]; Hermida认为comonadic情况下早于这些作品[12，第5章]。当p是非定态纤维化时，单子的笛卡尔提升的定义是有意义的。当C是一个具有拉回的范畴时，C上的单子T是笛卡尔的（例如参见[23，4.1节]）当且仅当T到箭头范畴C→的沿余域纤维化代码：C→→C的明显提升T→：C→ →C→是笛卡尔的。由一个定态纤维化p，一个单子T和它的提升T形p为我们提供了一个背景，在这里我们定义了Hoare三元组的抽象概念以及与之相关的wppt。定义3.2[Dijkstra结构] A（分别 Dijkstra结构是一个元组（p，T，Tstec）的一个定态纤维化p：P→C，一个单子T在C和a（resp.（纤维的，笛卡尔的）沿p提升T定义3.3设（p：P→C，T，Tstec）是一个Dijkstra结构。低于X，Y范围超过C-对象。(i) 对C中的任意f：X→ TY，P∈PX，Q∈PY，我们定义了Hoare三元组P{f}Q，P{f}Q <$Δffstec∈P（P，TstecQ）. pfstec=f.（一）因为忠诚，所以它是独一无二的。(ii) 我们定义最弱的前提谓词Transformer（简称wppt）wp：C（X，TY）×PY→PXwp（f，Q）=Δf（TstecQ）。（二）这两个概念由等价P≤wp（f，Q）P{f}Q联系起来。 Hoare三元组和wppt在我们的范畴设置是更一般的比标准的，因为我们可以提供任何P-对象和C-态射的wppt。这种解放使我们能够将wppt的可组合性和Cartesian-ness联系起来的Tstec。由于wp以Kleisli态射作为参数，因此可组合性应该针对Kleisli复合来讨论定理3.4设（p，T，Tstec）是Dijkstra结构.对任意适当类型的f，g，P，我们得到不等式wp（ηpP，P）≥P和wp（f·g，P）≥ wp（g，wp（f，P））.此外，它们成为等式当且仅当Dijkstra结构是笛卡尔的。是的。单位ηstecP：P→TstecP高于ηpP。因此wp（ηpP， P）=ηp<$P（TstecP）≥P。如果ηstecP是笛卡尔的，则这个不等式y变成n等于y。其次，乘法μstecP：TstecTstecP→TstecP，Tstecis大于μpP。因此，TstecTstecP≤μmpPTstecP;这是一个等于笛卡尔坐标。 更进一步地，对任意yX∈C， P∈P，f：X→pP，h aveTstecP（fP）≤（Tf）P（TstecP）;如果Tstecf化，则这是相等的。从这些，A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）511不不T T我们得到了如下不等式y，当μ是笛卡尔坐标时，Tstecisfibered.（f·g）（TstecP）=（μTfg）（TstecP）=g（（Tf）（μ（TstecP）≥g（（Tf）（TstecTstecP））≥g（Tstec（f（TstecP））=wp（g，wp（f，P））.从而证明了关于一般Dijkstra结构的wp不等式（p，T，Tstec），如果它是笛卡尔的，这些不等式就变成等式。相反，设（p，T，Tstec）是Dijkstra结构，并假设P=wp（ηpP， P）=ηpP（TstecP），（3）gTstecP（fTstecP）=wp（g，wp（f，P））=wp（f·g，P）=f（T g）<$μpPTstecP。（4）设X=pP。（3）表示ηstecP是笛卡尔的。 通过令g=idTT P，在（4）中f=id T P，我们得到TstecTstecP=μstecP（TstecX），因此μstecP是笛卡尔的. 通过让g=idTX和f=ηXh：Y→X→TX，对于（4）中的某个h：Y→X，我们得到Tstec（hP）=Tstec（hηXTstecP）=（Th）（TstecP），因此Tstecis化。Q因此，在笛卡尔Dijkstra结构（p：P→C，T，Tstec）中，wppt成为（CT）op→Pos类型的函子。相应的纤维化（通过Grothendieck构造）与p到Kleisli范畴的扩张一致推论3.5设（p，T，Tstec）是一个 Cartesian Dijkstra结构. 我们带走克莱斯里ResolutionsLER：CT→CofT和LstecERstec：PTstec→PofTstec。我们定义函子pT，Tstec：PTstec→CT由pT，TstecP=pP和p，Tstecf = pf. 然后(i) pstec 是一个pullback与wppt一致的posetalfibration： fP=、wp（f，P）.(ii) 对于X∈C，我们有一个同构：（Pstec）LX∈C=P X.(iii) （L，Lstec）和（R，Rstec）形成一个灵活的附加函数（see[14，Exercise1.8.10]）p和pstec。T， T最近的一项工作[2]提出了关系预期望算子（简称RPEO）的可组合性的失败。我们把他们的问题和我们的背景联系起来。它们的rpeo与我们在Dijkstra结构（p，D，K）中的范畴wppt一致，其中p：EPMet→Set是来自扩展伪距离空间范畴（它是偏序纤维化）的遗忘函子，D是有限概率分布单子（例5.6），K是Kantorovich度量构造，称为有限概率分布单子D沿p的提升。由于它不满足可组合性，我们得出结论，K不是笛卡尔。12A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）54Lax切片范畴在任意纤维化的情况下，我们不知道构造单子的笛卡尔提升的任何一般方法。然而，在来自松散切片范畴的域纤维化的特定情况下，有一个构造笛卡尔提升的方法A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）513C⊗ ◦◦在本节中，我们将抽象地研究这个配方，然后实例化通过构造沿着定义域纤维化的单子的各种笛卡尔提升，它用于第5-7为了让纤维具有偏序集的结构，我们考虑有序对象上的切片，定义为：定义4.1范畴C中的序对象是一对对象Ω∈C和偏序≤X对母集C（X，Ω）的一个赋值，对于每个X∈C。这些偏序应满足：对任何h：Y→X，i≤XiJ蕴涵i<$h ≤YiJ <$h。例4.2在Set中给出有序对象的一个典型方法是取一个偏序集（Ω，≤），并将集合（X，Ω）上的偏序≤X定义第5-7节中的例子都使用了从这种有序对象中产生的域纤维化从C中的一个有序对象（Ω，≤），我们定义了松弛片范畴C/Ω。它的对象是到Ω的C-态射.从i到j的态射是态射h∈C（X，Y）使得i≤dom（i）j <$h。定义为dC，Ωi=Δdom（i）anddC，Ω（f）=Δf的域函子dC，Ω：C / Ω → C是偏序集，在X ∈ C处的纤维范畴（C/Ω）X是偏序集（C（X，Ω），≤X）. i：X→ Ω沿h：Y→X的拉回由h<$i = i<$h给出。对于本节的剩余部分，设C是一个范畴，（Ω，≤）是C中的一个有序对象。我们对（dC，Ω，T，Tstec）形式的纤维/笛卡尔Dijkstra结构特别感兴趣。事实上，构成三纤维/笛卡尔Dijkstra结构的对（T，Tstec）只不过是严格么半群范畴（Pos-Fib（dC，Ω，dC，Ω），Id，Id）/（Pos-Fibc（dC，Ω，dC，Ω），Id，Id）中的么半群对象。为了研究这些幺半群范畴和其中的幺半群，我们引入了与之密切相关的Ω上单调代数的概念。在余代数社区中，它已被用于确定余代数函子的谓词提升[19，38，5]。定义4.3设F：C→C是函子。Ω上的单调F-代数是指F-代数o：FΩ→ Ω使得蕴涵i≤XiJ=oFi≤FXoFiJ对任意i，IJ∈C（X，Ω）成立.从这个定义出发，单调F-代数o：FΩ→ Ω确定函子F沿dC，Ω：C/Ω→C的提升Fo：C/Ω →C/Ω。 它由Fo（i）oFi给出。为了更好地理解赋值o<$→Fo，我们将Ω上的单调代数的范畴MAlgC，Ω构造 一个对象是一对（F，f）函子F：C→C和Ω上的单调F-代数o.从（F，o）到（G，oJ）的态射是一个自然变换α：F→G使得o≤FΩoJ<$αΩ。单位和张量乘积定义为yI=Δ（IdC，idΩ）andd（F，o）（G，oJ）（FG，OFoJ）。我们定义MAlgC，Ω为MAlgC，Ω的宽子范畴，其中从（F，o）到（G，oJ）的态射是一个自然变换，使得o=oJ<$αΩ.下面的结果展示了纤维函子和单调代数之间的关系。14A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）5CCCCC定理4.4有么半群同构的范畴（MAlgC，Ω，I，Ω）（Pos-Fib（dC，Ω，dC，Ω），Id，Id），（MAlgC，Ω，I，Id）（Pos-Fibc（dC，Ω，dC，Ω），Id，Id）。这个同构的对象部分已经显示为[5，命题12]。通过展开定义，MAlgC，Ω中的幺半群对象由一个单子（T，η，μ）和一个单调T-代数o：TΩ→ Ω组成，满足idΩ≤o<$ηΩ和o <$To≤o<$μΩ。我们称O为Ω上的松弛EM单调T-代数。MAlgC，Ω中的幺半群对象恰是Ω上的一个单子T和一个EM单调T-代数对从定理4.4，我们得到以下对应关系：推论4.5对于C上的任何单子T，a（resp.）lax）Ω上EM单调T-代数和一个笛卡尔（分别为 纤维）T沿dC，Ω的提升。最后，我们总结了由EM单调代数产生的笛卡尔Dijkstra结构的wppts。推论4.6设T是C上的单子，o是Ω上的EM单调T-代数，To是T沿dC，Ω的相应笛卡尔提升. Dijkstra结构（dC，Ω，T，To）中的wppt满足wp（f，i）= o<$Ti<$f.当o是一个松弛EM单调T-代数，To是T的相应的纤维提升时，同样成立.4.1域纤维化我们考虑对给定给homsetC（P，Ω）的偏序施加进一步的条件。设K是Pos的一个子范畴。我们说，一个有序对象（Ω，≤）如果1）对任意X∈C，偏序集（C（X，Ω），≤X）属于K，2)对任何C-态射h：Y→X，函数−H：C（X，Ω）→C（Y，Ω）是K中的（C（X，Ω），≤X）→（C（Y，Ω），≤Y）型态射。引理4.7设K是Pos.对任意一个C-序对象（Ω，≤），若dC，Ω：C/Ω → C是K-纤维化.接下来，固定C中属于K的有序对象（Ω，≤）。 对于闭函子F：C→C，我们说o：FΩ→ Ω是K-代数，如果对任意X∈C，函数o<$F−：C（X，Ω）→C（FX，Ω）是（C（X，Ω），≤X）型的K-态射）→（C（FX，Ω），≤FX）。 我们记K-AlgC，Ω为的全（monoidal）子范畴MAlgC，Ω由K-代数构成.定理4.8设K是Pos的一个子范畴，（Ω，≤）是属于K的一个序C-对象.存在范畴（K-AlgC，Ω，I，Ω）的么半群同构（K-Fibc（dC，Ω，dC，Ω），Id，Ω）。A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）515例4.9对于完备格和保持所有交的单调函数的范畴，我们写CLat [1]。这是Pos的一个子类别。 当我们把两点偏序集2 ={X≤ X}看作Set中的有序对象时（如例4.2所示），它属于CLatX。因此，dSet，2：Set/2→Set是一个CLat纤维化。进一步地，对任意（T，Tstec）∈ CLat ∈ Fibc（dSet，2，dSet，2），相关的wppt保持满足，即wp（f，iPi）=iwp（f，Pi）. 在程序验证的上下文中，这样的wppt被称为合取。最强后置条件谓词变换我们将注意力转向最强后置条件谓词转换器。 在霍尔逻辑中，关于程序f和预条件φ的最强后置条件是一个公式，使得1）φ{f}成立，2）当φ{f}成立时，在霍尔逻辑中包含本文给出了Dijkstra结构（p：P→C，T，Tstec）中最强后置条件的概念。关于C中的态射f：X→ TstecY和对象P∈PX的最强后置条件是对象S∈PY使得对任何Q∈PY，S≤Q当且仅当P{f}Q。如果这样的S存在，它是由f和P唯一确定的，因此我们将其记为sp（f，P）。总而言之，我们得到了三向等价：sp（f，P）≤ Q P {f}Q P ≤ wp（f，Q）.因此，如果对任何f，P都存在sp（f，P），我们得到一个函数sp：C（X，TY）×PX→PY，称为最强后置谓词Transformer，且sp（f，−）被刻画为wp（f，−）的左伴随。当程序被简单地建模为内存配置集上的内函数时，sppts对应于直接图像。这种操作的分类抽象是在操作中向前推进[31，示例6]，我们在下面简要回顾一下。一个函子p：P→C是一个函数化，如果pop：Pop→Cop是一个函数化。给定P∈P，Y∈C，f：pP→Y在C中，f沿op-fibration的op-Cartesian提升记为fP，其目标记为fP，称为P沿f的推进。既是纤维化又是操作化的函子称为双纤维化。Posetal双振动可以由以下引理表征引理4.10（[14]）设Pos r是Pos的子范畴，其中态射限制在偏序集之间的右伴随上.一个位置纤维化是一个双纤维化当且仅当它是一个位置纤维化。例4.11考虑CLat标定的情况。 由于重索引函子保持任意交，因此它们具有左伴随，我们可以计算为f<$P={Q∈Pcod f|P≤f<$Q}。由于CLat是Posr的一个（全）子范畴，所以CLat双标化是posetal双标化。左伴随的存在允许我们定义sppt's，如以下结果所述：命题4.12设（p：P→C，T，Tstec）是一个Dijkstra结构，其中p是a设T_stec：P_X→P_T_X的约束T_stec为16A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）5SS纤维是一个右伴随。 则对C中的任意f：X→ TY，wp（f，−）：PY→PX有一个左伴随sp（f，−）：P X→P Y。如果Dijkstra结构是笛卡尔的，则sp是可合成的：sp（ηpP，P）= P和sp（f，sp（g，P））= sp（f·g，P）。4.2复合单子到Lax切片范畴在许多情况下，用于建模计算效应的单子是通过分配律的简单单子的组合。我们推广我们的提升理论的单子复合单子。设T，S是C上的单子，α：ST → TS是分配律（见第2节）. 我们对T_∞αS的EM单调代数感兴趣，它给出了T_∞αS的笛卡尔提升. 在[4，第2节]，[27，定理2.4.3]中研究了这类EM下面，我们将这些结果进行适当的扩展。定理4.13设T，S是C上的单子，α：ST → TS是分配律.在以下每两个之间存在双射对应(i) EM单调T∈αS-代数a.(ii) 一对EM单调代数t：TΩ→ Ω和s：SΩ→ Ω满足s<$St=t<$Ts<$αΩ;（5）(iii) 沿dC，Ω的笛卡儿提升的三元组TstecofT和SstecofS和一个分配的αstec定律：SstecTstec→TstecSsteca大于α，其分量是笛卡尔的。我们注意到条件（5）出现在[4，第2节]中。这个定理说，要确定T∈αS的提升，就必须确定满足（5）的所有EM单调T-和S这是自然的，以寻求一个宽松的版本上述对应关系。 然而，在这方面，它不能完全推广到有序设置。问题来自不能比较涉及代数合成的某些态射。S p ecicall y，o：TSΩ→ΩandoT（ηΩSoηTΩ）一般不具有可比性。S但是当o是合成tt时，TΩ→ Ωs的lax EM单调代数t：且s：SΩ→Ω，则有o≤o<$T（ηΩS<$o<$ηTΩ）. 因此，我们可以找到一个同构时，我们限制到这些定理4.14设T，S是C上的单子，α：ST → TS是分配律. 则一个松弛EM单调T<$αS-代数ao使得o≤o <$T（ηΩS<$o <$ηTΩ）是双有效的对应于一对松弛EM单调代数t：TΩ→SΩ和s：SΩ→ Ω使得s<$St≤t<$Ts <$αΩ， t =t<$Ts<$TηΩS和s=t<$Ts <$ηTΩ。4.3代数运算与最弱前提谓词Transformer导致计算效应的各种程序构造可以通过Plotkin和Power的代数运算自然它们经常出现在有效程序的一元语义中。在本节中，我们给出了代数运算的wppt语义。我们假设C是笛卡尔闭的，T具有强度A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）517M MM+θX，Y：X× TY→ T（X×Y）。对于指数对象、currying、uncurrying和evaluation，我们使用符号、λ、λ−1、ev任何态射g：A→ TB（称为类射）都具有一个EMT-代数o：TX→X，运算op（o，g）：A×（B<$X）→X：op（o，g）=Δo<$T（ev）<$θBJ，B<$X<$（g×idB<$X）;这里θXJ，Y：TX×Y→T（X×Y）是θ的对称变换。Sp eci fcally，the定义为α（g）X=op（μX，g）的自由代数{α（g）X}X∈C上的运算族形成对应于g的代数运算。下面的定理帮助我们（在6.2节）计算涉及代数运算的程序的wppt定理4.15Leto：TΩC→Ω是EM单调T-代数a，To是T沿着d，Ω被o的笛卡尔提升。 对任意态射g：A → T B，a：Y→ A，b：Y→BC <$TX和i：X→Ω，以下等式在Dijkstra结构（d，Ω，T，To）：wp（α（g）X<$a，b<$，i）=op（o，g）<$a，λ（wp（λ−1（b），i））<$.5d集上的Dijkstra结构我们将在前面几节中开发的技术应用于具体的设置。我们首先考虑偏序集2={X ≤ X}的松弛切片范畴，它被看作是Set中的有序对象（例4.2）。 我们在Set / 2中识别一个对象i：X→2作为集合对（X，P），使得P<$X。纤维化dSet，2：Set/2→Set同构于子对象纤维化（参见例如：[14]第0章（一）例5.1[11，2.3节]作为热身练习，我们考虑maymonad（a.k.a. Monad）MalongdSet，2.它的函子部分定义为yMX=ΔX+{x}，其中{x}表示单例集。有两个EM单调M-代数tot，par超过2：tot（x）= x=，par（x）=（x = x =）。它们分别诱导了沿 dSet ， 2 的 两 个笛卡尔提升 tot， par。 与这些笛卡尔提升相关联的Dijkstra结构使得Hoare三元组的全部和部分EM单细胞。 M-Algo提升Mo，对象部分（X，P）{ f}（ Y，Q）in（ dSet，2，M，MO）totMtot（X，P）=（M X，P）x∈X 。x∈P=f（x）=/f（x）∈QparMpar（X，P）=（MX，P<${n}）x∈X。x ∈ P <$f（x）/=<$ = f（ x）∈Q例5.2[13，例3.3]接下来我们考虑非空幂集单子P+沿dSet，2的笛卡尔提升。它的函子部分定义为P+X{UX|U}。恰好有两个单调EMP-代数可以，必须超过2：may（U）=∈U，must（U）=/∈U18A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）5可以，PPΣD dd它们诱导出两个笛卡尔提升P++必须 P+沿d集，2。 的Dijkstra这些笛卡尔升力的结构+沿着d集，2或可能和必须Hoare三元组的正确性解释EM单细胞。P+-Algo提升P+，物体部分O（X，P）{ f}（ Y，Q）in（ dSet，2，P+，P+）O可以P+ （X，P）=（P+X，{U|U =/}）可以x∈X。x∈ P= f（x）的值。u ∈Q必须正+ +P必须（X，P）=（PX，{U |U P}）x∈X。x∈ P= f（x）的值。u ∈Q例5.3我们再次考虑前一个例子中的P+单子，但现在我们把dSet，2看作一个CLat分解。则必是唯一的2上EMCL代数。因此必须正确解释Hoare三元组中具有最强后置条件的谓词Transformer。例5.4我们考虑状态单子S，其函子部分定义为：SX=S<$X×S;这里S是状态的集合。但是，两点集2太小，无法记住存储值，|S|≥ 2。的确，定理5.5当|S| ≥ 2，则不存在2上的EM单调S-代数。证明思想很简单，每次计算都需要与2的元素相关联，以满足查找和更新的代数理论Plotkin和Power在[35]中进行了研究。 如果|S|≥ 2则存在s1s2在S中，我们无法区分查找状态、存储S1和存储S2，因此可能会产生矛盾。当我们把切片对象2替换为S2（具有逐点顺序）时，我们发现它携带EM单调S-代数o（k）λs。π1（ks）（π2（ks））;参见[25，4.4节]。S沿dSet，（S <$2）：Set/（S<$2）→Set的相应笛卡尔提升及导出的wppt满足So（i）（c）= λs. i（π1（cs））（π2（cs）），wp（f，i）（x）= λs . i（π1（f（x）（s）（π2（f（x）（s）.通过分别使用i和f的解卷积iJ和f J，wppt可以简化为：wp（f，i）（x）= λs。iJ（f J（x，s））。例5.6最后，我们考虑有限概率分布单子D。集合X上的有限概率分布是一个函数μ：X→ [0，1]，使得μ在X中的有限个元素处不为零，且 i∈Xμ（i）= 1。单子D的函子部分由DX={μ是X上的有限概率分布}给出。定理5.7存在两个2上的EM单调D-代数，由下式给出：pmay（μ）=μ（μ）>0，pmust（μ）=μ（μ）= 1它们诱导出两个笛卡尔提升Pmay，pmustof沿dSet，2. 预- 与它们相关的计算转换器将非确定性程序的可能和必须正确性推广到概率设置。EM单细胞。 D-Algo提升Do，物体部分（X，P）{ f}（ Y，Q）in（ dSet，2，D，Do）PMAYD p可以（X，P）=（D X，{μ |x ∈ P。μ（ x）>0}），x∈X。x ∈P=<$Pry<$f（x）[y∈Q]>0普穆特D p必须（X，P）=（D X，{μ |x ∈ P。μ（ x）>0}）x∈X。x ∈P=<$Pry<$f（x）[y∈ Q] = 1A. Aguirre，S.y. Katsumata/理论计算机科学电子笔记352（2020）519P准备，2+这里的符号Pry∈f（x）[y∈Q]表示当采样时y∈Q的概率f（x）中的y我们注意到，笛卡尔提升是相当罕见的，相比任意提升。我们看一下幂集单子P沿着dSet，2的情况。对于每个正则基数λ，Pλ（P<$X）={U<$P||U|<λ}给出幂集单子P沿D. 另一方面，（对）例5.2的修改表明，只有两个笛卡尔提升，沿着d集，2。 例5.4还表明， 没有笛卡尔提升（非平凡）状态单子沿d集，2。6d集[0，∞]上的Dijkstra结构接下来，我们用非负扩展实数的偏序集[0，∞]替换2，具有通常的数字顺序。它是一个完全分配格，并且定义域纤维化dSet，[0，∞]：Set/[0，∞]→Set具有丰富的结构（实际上它是一个tripos [33，例2.2]）。Set/[0，∞]的一个对象是函数i：X→[0，∞]，它可以以许多不同的方式看到：随机变量，成本分配，鲁棒性，
我的内容管理
展开
