基于最大不动点语义的自然语义证明演算

理论计算机科学电子笔记132（2005）73-93www.elsevier.com/locate/entcs基于最大不动点语义的自然语义证明演算萨宾·格莱斯纳卡尔斯鲁厄大学程序结构和数据组织研究所，76128Karlsruhe，Germany http：//www. info. uni-karlsruhe。德格莱斯纳摘要编程语言的形式语义需要对潜在的无限状态转换进行建模， 程序的行为以及最终结果的计算。这个要求在编译器的正确性证明中是必不可少的。我们表明，自然语义的最大不动点解释能够同样好地模拟这两个方面。 从技术上讲，我们基于对归纳和共归纳的对偶定义和证明原则的简单介绍，推断出对自然语义的这种解释。此外，我们开发了一个基于它的证明演算，并展示了它的应用程序的两个典型问题。关键词：形式语义，形式编译器正确性，自然语义，共归纳/最大不动点解释，证明演算。1对最大不动点语义的需求编程语言语义包含两个双重方面：程序的执行触发一个潜在的无限状态转换序列。如果这个过渡序列终止，那么它就定义了程序执行的最终结果。编程语言语义的形式化体系应该同时对这两个方面进行建模。如果一个程序的执行终止，那么它的最终结果应该根据有限状态转换序列来定义。此外，语义形式主义应该为非终止程序指定一个更有意义的语义，而不仅仅是“unfined”。这一要求在实际应用中是必不可少的。许多程序（例如操作系统、数据库、嵌入式系统或反应式系统中的控制软件）在仍然具有非常特殊的语义时不打算终止1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.01174S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）73p--···我们证明了自然语义的最大不动点解释能够同时对这两个方面进行建模。这个最大的不动点解释产生了一个由归纳和共归纳证明规则组成的证明演算。它可用于程序设计语言的形式化推理。作为示例，我们考虑两个应用。第一个是翻译的正确性证明，例如在编译器中。因此，需要证明翻译程序的可观察行为被保留。这是一个比仅仅保存最终结果更强的要求。第二个例子是关于编程语言属性的证明，例如类型安全。他们需要考虑终止和非终止程序。我们的证明演算是基于一种成熟的趋势，即代数和共代数方法的组合可以成功地用于编程语言的规范和推理，特别是对于潜在的非终止过程。我们以一种简单的形式重申归纳和共归纳的相应证明原理，这种形式足够强大，可以在有限计算中模拟确定性。我们描述的两个双重定义和证明原则，在一个纯粹的集合论和易于理解的方式，在使用范畴论的共同文学相反。我们证明了程序的状态转换行为必须是共归纳的，而最终结果是在其上归纳定义的。虽然自动定理证明器，例如Isabelle [13]，有可能进行共归纳推理，但标准实践并不使用它。所有基于自然语义的自动和“纸笔”证明都利用归纳，因此只适用于终止计算。本文的结果表明，这是不够的，可以很容易被共归纳推理取代。归纳证明让我们从一个动机开始，为什么归纳法不是无限计算的适当证明原理。P过程···{P}{Q}结束过程{Q}考虑Hoare calculus [6]的一个著名的证明规则。如果要证明一个递归过程p是正确的，wrt。一个前提条件P和一个后置条件Q，那么假设对于p的主体内的p的所有递归调用，前提条件P和后置条件Q成立。如果p总是终止，则这是归纳证明。内部调用的递归深度总是小于p的深度如果过程p没有终止，它就不再是有效的归纳证明内部过程体中的状态转换序列和外部过程的状态转换序列一样，都是无限长的。因此，我们没有关于严格较小的归纳前提，S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）7375状态转换序列两个状态转移序列具有相同的集合论大小。尽管如此，它仍然是一个有效的共归纳证明，表明在每个过程入口处，前提条件都是满足的。因此，我们假设该前提条件在初始状态下成立，并证明当进入内部过程时也成立。 在这种情况下，我们不能说任何关于 后置条件，因为它应该保持的程序点从未到达。证明霍尔演算规则在非终止情况下的有效性这个推理是共同归纳的基础。一个归纳论证表明，对于潜在无限状态转移序列的所有有限前置条件，前置条件P在过程p的每个入口处都有效。然后它得出结论，这个性质（P在p的每个入口都有效）也适用于无限状态转移序列。如果不是这样的话，那么就会有一个不完全填充P的有限前缀，从而与归纳证明的结果相过程的霍尔演算规则本质上是两个规则的叠加。第一个考虑的终止情况与后置条件。第二个模型的非终止的情况下，在每个过程入口的前提我们将看到自然语义的规则的相同覆盖。2自然语义自然语义学[9]是一种用于定义程序语义的演绎方法。公理和推理规则规定了wrt的语义属性。ab-mandrel语法。抽象语法树的语义被定义为从初始状态到最终状态的状态转换。这种状态转换是根据抽象语法树的直接子树的状态转换来定义的。考虑例如while循环的规则Eval（cond，σ）= true，→ σJ，Eval（cond，σ）=false<当S结束时，σ >→σ<当S结束时，σJ>→σJJ<当S结束时，σ >→σJJ这两条规则表示循环体S的执行取决于 条件cond的值。如果它被执行，那么整个循环将再次递归执行。在传统的计算环境中，这种语义描述只用于终止计算，本文对此进行了修正。在这种情况下，第二条规则说，如果条件cond的评估为真，如果主体S由从σ到σJ的状态转换执行，并且如果存在描述循环的递归执行的从σJ到σJJ的状态转换，则存在从σ到σJJ的76S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）73≤≤···→→一般地，给定抽象syn- tax的产生式X0：：=X1···Xn，相应的推理规则具有以下形式，其中Xlk∈{X1，.，X n}，1 ≤k≤m和X ij ∈ {X0，X1，.，X n}，1 ≤j≤ r：Eval（Xl1，σ0）=值1，.，Eval（Xlm，σ0）=值m，→σ1，···，→σr→σr推理规则的假设由两部分组成，求值条件Eval（X lk，σ0）和直接子程序→ σ j的状态转移。评价条件决定了该规则在给定状态σ0下的适用性。 在while循环示例中，它们表示条件cond的值Eval（cond，σ0）。假设中的状态转换描述了子程序的语义循环的整个状态转换在结论中表示公理是一种推理规则，在其假设中只有评估条件，但没有状态转换，即。r=0。需要数据结构来定义求值条件的值这些数据结构通常由一组固定的构造函数上的代数项归纳定义。额外的（定义的）函数由递归定义这些函数在构造函数项上的结果的自然语义规范描述了派生树。它们的根节点标记有要执行的程序以及计算的初始和最终状态。根的后继者要么用程序的直接子树来标记，要么用程序本身来标记（递归定义）。此外，后继者被标记有由推理规则定义的状态转换：从初始状态σ到根节点的最终状态σJ被分解为序列σ=σ0→σ1→σ r=状态转换的σ j。每个状态跃迁σi−1σi，1r，由派生树的子树中的恰好一个描述这些子树上的顺序由状态σ0→σ1···→σr的线性顺序隐式地指定。传统上，自然语义规范是用有限的派生树来解释的，因为只有这样，才存在唯一的最终状态。这种传统观点对应于归纳或最小固定点解释。在本文中，我们讨论为什么最大不动点或共归纳解释更合适。它还允许非终止程序的语义，同时不改变终止程序的通常归纳语义。S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）7377DDD≤ ≤ ≤≤3归纳和共归纳设D是一个抽象数据类型，S是一个固定集合，dl∈ D，其中l∈ {1，. ，j∈{1， . ，q}和sk∈ S，其中k∈{1， . ，w， j}，j∈{1， . ，q}或k∈{1， . ，ti}，i∈ {1，.，p}定义为：d∈D id：：= Base1（s1，. （一）|···|Basep（s1，. （s tp）|Con1（d1，...， d r1，s1，. （一）|···|Conq（d1，.， d rq，s1，.（s wq）这个定义指定了树的全域D，其节点用基或构造器符号之一标记Basei，i∈{1，.，p}或Conj，j∈ {1，.，q}，并且具有值s1， . . sti或s1， . . swj。对于小的y，这个标记树的集合D由两个递归条件定义：• 如果d = Basei（s1，. s ti），1 ≤i≤p，则根（d）没有后继结点。在这种情况下，根（d）的标记被定义为mark（root（d））=（Basei，s1，... s ti）。• 如果d=Conj（d1， . ，drj，s1， . . . swj），1≤j≤q，则当root（d）有srj个直接子树 d1 ， . ，drjsuch c hthatd1， . ， drj∈D. 在这种情况下，root（d）的标记被定义为mark（root（d））=（Conj，s1， . . swj）。这个定义不仅指定了有限高度的树，而且还指定了无限高度的树。 由于空间的原因，我们不证明集合 存在. 这样的证明可以在例如[2]中找到，表明的闭包序数是ω。 为了可读性，作为缩写，我们将给定树d的mark（d）写成mark（root（d）），而不是mark（root（d）），其中root（d）表示树d的根节点。1标记树的论域D诱导出完备格（P（D），n），其中P（D）表示D的幂集，P（D）表示集合上的包含关系定义3.1[SpecificationSpec] SpecificationSpec定义了抽象数据类型D的论域上的一元预测Spec，通过为每个基Basei，1≤i≤p和每个构造函数Conj，1≤j≤q精确地陈述一个方程：S pec（Bas ei（s1， . ，sti））真实的数据块Bas ei（s1， . . . ，sti）Spec（Conj（d1， . ，drj，s1， . . . swj）Spec（d1）· ··Spec（drj）· · · BjcokCo nj（s1， . ，swj，mark（d1）， . ，mark（drj））因此，谓词okBasei和okConj，1i p和1jq，定义了对元素中的已标记节点的标记的允许组合的限制，. okBase的定义是 和okConj 取决于具体规格。例如在自然语义学的上下文中，它们是1注意mark（d）不是表示树中所有节点的标记的递归函数D. mark（d）仅指定d的根节点的标记。78S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）73DD由自然语义学的公理和推理规则隐含地指定第4.1节，我们陈述了相应的细节。目前，我们只要求它们是可判定的。谓词Spec隐含地定义了一个函数spec：P（D）→ P（D）：s pec（X）={x∈X|i∈{1， . ，p}.x=Basei（s1， . . sti）SlokBas ei（s1， . ，sti）{1， . ，q}。x=Conj（d1， . ，drj，s1， . ，swj）<$d1∈X< $··< $drj∈X<$okCo nj（s1， . ，swj，mark（d1）， . ，mark（drj）}定理3.2（spec的单调性）指定函数spec：P（D）→ P（D）在格（P（D），n）上是单调的，即， 如果X<$Y对于X，Y∈ P（D），则spec（X）<$spec（Y）.证据通过矛盾：假设存在z∈spec（X），z/∈spec（Y）。则存在x∈X使得spec（{x}）={z}。由于X<$Y，因此x∈Y且spec（{x}）={z}<$spec（Y），这与假设相矛盾。Q塔斯基因此，我们得出结论，lfp（spec）和gfp（spec）存在。最小不动点称为初始代数，最大不动点称为最终余代数。规范Spec限制了全域中树的节点的有效标记抽象数据类型。最小不动点lfp（spec）是所有有限树的集合，其标记是有效的wrt。规格。（简短的证明大纲：这显然是一个固定的点。考虑一个严格较小的集合：那么“缺失元素”总是可以由有限的构造序列构造。最大固定点gfp（spec）是所有具有有限高度和无限高度的树的集合，其标记是有效的wrt。规格。（一个证明的简短大纲：不包含在这个集合中的每棵树至少有两个标记无效的节点。它的前代节点或后继节点的标记）。先验地，在具体化中没有方向。 尚未确定是否标记是根据其继承者或其前身的标记来定义的。 原则上，有两种可能的定义图式：定义模式，我们为基地指定然后，我们通过定义节点的标记如何从其子节点的标记中导出来说明它们如何在整个树中传播。相反的方向也是可能的，并给出了共归纳定义原理。..................归纳定义流上归纳定义流S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）7379∈∈···≡ ∧···∧D请。从树的根节点开始，我们指定它的标记如何通过树传播。因此，我们定义一个节点的标记是如何从其前身的标记中派生出来的。第一个原则是结构归纳，并定义了有限树上的唯一标记。第二个原则也适用于无限树。即使一棵树可能不是有限的，硬币的定义也指明了一个可能的无限标记过程，在每一步都有明确的定义。归纳定义原理直接对应于归纳证明原理。它指出某个谓词Q对最小固定点lfp（spec）中的所有元素都成立。归纳证明完全是构造性的。Q只能对可以构造的元素进行验证还有一个与共归纳定义原理直接对应的共归纳证明原理它可以用来证明元素在最大不动点上的性质。我们需要这两个版本：定理3.3（一元共归纳原理）设dgfp（spec），Q是关于d的节点标记的谓词. Q（mark（k））对所有节点k∈d成立，如果• Q（mark（root（d）和• 如果{1， . ，q}。 （d=Conj（d1， . . . ，drj，s1， . ，swj）n（Q（mark（Conj（d1，. . . ，drj，s1， . ，swj）Q（mark（d1）） · ··Q（mark（drj）定理3.3中的两个条件为我们提供了一个证明原则，以证明树dgfp（spec）中的所有标记都能填充给定的谓词Q。因此，我们需要证明Q对于d的根节点的标记（第一个条件）以及对于从这个根节点可能到达的所有节点（第二个条件）都成立。这是通过证明，只要Q对内部节点的标记成立，那么它也对它的直接后继节点的标记成立。与定义3.1相反，没有重新定义。cursiveproofobligationslikekeSpec （ Conj（） 的 情 况 ）Spec （ d1 ）Spec（drj）. . . .这里我们只需要证明一个关于有限个构造函数Con1，...，和他们可能的继任者。作为定理3.3的一个结果，我们得到一个关于最大不动点gfp（spec）中的无穷多棵树（其中许多树的高度是无限的）及其标记的陈述在实际应用中，我们利用谓词的具体化规范及其定义来验证- orem3.3的两个okBasei 对于1 ≤i≤p和okConj 对于1≤j≤q，参见 第四节和第五节。证据定理3.3的证明通过矛盾：假设存在一个节点k∈d使得<$Q（mark（k））。W.l.o.g.设k是到d的根节点具有最小距离的节点，使得<$Q（mark（k））。 设pos为该节点k的位置，即k = d|POS. (Each树中的节点可以是spec-80S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）73∈由一系列导航号标识，表示从根到它可以到达的路径。）因为我们假设Q（mark（root（d）））成立，所以列表pos至少包含一个元素：pos=[l|位置J]。 由于我们假设k是最小节点，使得<$Q（mark（k）），Q（mark（d|位置J）） 但d|posJ=Co nj（d1， . ，drj，s1， . ，swj），对于somej∈{1， . ，q}和d|p〇s∈{d1， . ，drj}。 由定理3.3中的第三个假设，我们推出对所有l∈ {1，.，rj}，特别是Q（mark（k））， 假设为<$Q（mark（k））。 因此，对于所有k∈d，Q（mark（k））。Q定理3.4（二元共归纳原理）设d，DJ绿色荧光蛋白（质量标准）。 D=dJ如果• 对于某个i∈ {1，...，p}：d=Basei（s1，...，s ti）和dJ=Basei（s1，...，sti），或者如果对于某个j∈{1， . ，q}：d=C0 nj（d1， . ，drj，s1， . ，swj）和dJ=Conj（dJ1， . ，dJrj，s1， . ，swj）和• 如果对于所有项t1，t2∈gfp（spec）并且对于所有j ∈ {1，.， q}：如果t1=Co nj（d1， . ，drj，s1， . ，swj）和t2=Co nj（dJ1， . ，dJrj，s1， . ，swj）这意味着对于所有l∈ {1，...，r j}：mark（d l）= mark（dJl）。证据类似于定理3.3的证明：通过矛盾：假设d/=dJ. 则存在位置pos =[l|位置J]的最小长度，该标记（d |pos）mark（dJ|pos）和mark（d|posJ）= mark（dJ|位置J）。但后来定理3.4中第二个条件意味着标记（d |pos）= mark（dJ|pos）这与假设DDJ相矛盾。因此d=dJ。Q与定理3.3一样，定理3.4陈述了两个非递归的条件，这两个条件允许我们推理递归的，可能是有限结构的。在推理编程语言的语义时，我们使用一元共归纳原理来证明关于程序执行的可能有限状态转换序列的陈述此外，我们使用二进制共归纳原理比较程序的状态转移序列。4自然语义学我们从观察每个自然语义定义一个抽象数据类型开始。然后我们证明，每一个自然语义都是定义3.1意义上的一个具体化。我们证明了这样一个规范的最小不动点描述了所有终止程序的执行，而最大不动点也定义了所有非终止计算的语义S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）7381S{|∃∈∨}4.1自然语义的派生树一个大的步骤语义定义程序的执行是自上而下的：整个抽象语法树的状态转换是由它的直接子树的状态转换组成的，在递归定义中，也是由它自己的状态转换组成的。重要的是要注意，大步骤语义只在抽象语法树的叶子上定义单个状态转换。对于所有内部节点，推理规则指定如何从假设的状态转换组成结论中的总体状态转换序列。因此，我们可以把每一个推理规则看作是一个递归过程，如果它的求值条件被满足，那么它是可应用的，并且递归地调用进一步的公理或推理规则。程序的执行定义了一个可能无限的其内部节点对应于推理规则的应用，其叶子表示公理的应用我们正式定义这个概念：首先，我们定义派生树中节点的标记。假设Prog是所有抽象语法树。 设Prog = progprogJProg. prog=progJprog是progJ的子树 都是抽象语法树及其子树。让可以是在自然语义中用于表示状态的数据结构（CP.第2条）。在派生树中，每个节点标记为（P，prog，s，sJ），其中P是其基或构造器，prog∈Prog是程序，s∈ S是初始状态，sJ∈S为最终状态。令A1，...，A p是公理和R1，...，R q是自然语义规范的推理规则，每个推理规则唯一地属于抽象语法的一个产生式X0：：= X1···Xn，并且每个推理规则的形式Eval（Xl1，σ0）=值1，.，Eval（Xlmi，σ0）=value mi→σ1Eval（Xl1，σ0）=值1， . ，Eval（Xlmj，σ0）=valuemj，→σ1，· · ·， Xirj，σrj−1>→σrj→σrj派生树的抽象数据类型D定义如下：prog∈Prog和s，SJ∈ S：d∈Di ∈d：：= A1（prog，s，sJ）|···|A p（prog，s，sJ）|R1（d1，.，（d r1，prog，s，sJ）|···|R q（d1，.， d rq，prog，s，sJ）谓词Spec通过为每个公理和每个推理规则陈述一个等式来定义。这是Ai，1≤i≤p的版本：规范（Ai（prog，s，sJ））root（prog）= X0root（prog|[1]）= X1···root（prog|[n]）= X n替代τ。（τ（σ0）=s<$τ（σ1）=sJ<$82S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）73≤≤联系我们D ∈ D联系我们∈ ∈ S评估（前/后）|[l1]， τ（σ0））=value 1· ··Eval（p rog|[lmi]， τ（σ0））=值mi）第一行说明公理Ai属于产生式X0：：=X1··Xn，并且只能应用于那种形式的程序。prog|[i]表示prog的第i个直接子树。第二行描述了可以包含变量作为占位符的一般状态σ0和σ1可以通过应用替换τ映射到具体状态s和SJ。最后一行指定求值条件必须满足状态s=τ（σ0）。推理规则Rj，1jq的Spec版本需要递归正确性要求的附加条件。第一行是递归约束，要求所有子树都满足指定。最后三行要求每个直接子树用同一程序或该程序的直接子树标记此外，指定第k个子树的最终状态是第k+ 1个子树的初始状态，1≤k≤j− 1。 其余的要求与公理相同：Spec（Rj（d1， . ，drj，prog，s，sJ））Spec（d1）· ··Spec（drj）root（prog）= X0root（prog|[1]）= X1···root（prog|[n]）= X n替代τ。 （τ（σ0）= s <$τ（σ rj）= sJ<$评估（前/后）|[l1]， τ（σ0））=value 1· ··Eval（p rog|[lmi]， τ（σ0））=valuemil ∈ {1，.， r j}。 （mark（d l）=（progJ，s1，s2））（i l= 0 prog = progJi l> 0 prog |[il]= progJ）root（progJ）=Xil<$τ（σl−1）=s1<$τ（σl）=s2））Spec是一个Specification Wrt。定义3.1.因此，在集合上存在具有最小和最大不动点的单调指定函数spec，lfp（spec）和gfp（spec）标记的派生树。 如果d标有（P，prog，s，sJ）对于PA1，...，A p，R1，...，R q，那么我们说d是一个导数，这是一棵树，S是D的初始状态，S是D的最终状态。先验地，标记的定义没有方向。无论如何，在所有现有的规范中，都存在这样一个方向。对于导出树的每个标记（P，prog，s，s，J），A p，R1，...，Rq、程序prog和初始状态s被共归纳地定义，而最终状态sJ 是归纳性定义的。即使执行没有终止，并且最终状态没有唯一定义，在执行期间执行的状态转换仍然是唯一确定的。定义4.1自然语义规范是确定性的，如果• 对于所有progProg，s，存在一个公理或推理规则，其求值条件在状态s中被满足，并且适用于prog（即，如果公理或推理规则属于产生式X0：：=X1···Xn，则根（prog）= X0，并且对于l∈ {1，.，n}，root（prog|[1]）= X1）。• 对于每个公理和推理规则，如果prog和初始状态s已知，则S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）7383prog prog，[]，[i=5]>i：=1while i 2 doi：=i+1 odi：=5<而i 2做i：=i+1 od，[i=1]，[i=2]>Fig. 1. 终止程序所有评估条件都可以通过终止计算来计算• 对于每个公理，如果给定prog和初始状态s，则最终状态也可以通过终止计算来唯一地计算SJ我们还可以考虑这样的情况，即存在指定，使得无法计算最终状态，因为，例如，可能没有适用的规则。这种情况被称为卡住的计算。 为了使演示简单，我们不在此讨论这些情况4.2经典归纳解释自然语义学的经典解释只为终止程序定义语义。我们给出了一个终止计算的例子。然后我们证明了对于所有的终止程序，最终状态是唯一的。例4.2[终止执行]假设执行期间的状态是一个变量对及其当前值的列表。进一步假设在图1中的左手侧给出的程序prog将在状态[]中执行，即，还没有变量被赋值。然后，程序的语义由图1右侧的派生树d表示。这个例子演示了程序语义中共归纳和归纳结构的两级层次：程序prog和初始状态s被定义为共归纳。它们的定义从派生树的根开始，并通过树传播，直到到达它的叶子。在叶子上，语义学的共归纳部分，即状态转移行为，与归纳部分，即最终状态的计算相联系。最终状态的定义是归纳的，因为它从叶子开始，沿着派生树结构一直到根。定理4.3设Spec是一个确定性自然语义，指定相应的指定函数，lfp（spec）是它在标记导树集合D上的最小不动点. 设S为状态集，Prog为状态集抽象语法树或其子树。对于每个程序prog∈ Prog，s0∈ S，如果在s0开始的prog的执行终止，则存在84S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）73→∈ D∈ S→一棵派生树D对于prog和s0。 d的最终状态是 唯一确定的。证据 通过对d的（有限）结构的归纳：归纳基：如果存在一个公理A i，使得它的求值条件满足s0，并且它适用于prog，则存在唯一的最终状态sJ使得sJ。因为Spec是确定性的，没有其他公理或推理规则适用，因此d是唯一确定的。归纳步骤：设Rj，1 ≤ j ≤ q，是适用于其评估条件满足的prog的唯一推理规则。 如果这个规则有r j个假设，那么prog和s 0的派生树d有r j个直接子树。第一个子树是唯一确定的，因为它是某个程序progJ和s0的派生树，其中progJ= prog或progJ是prog的直接子树，由R j指定。由于归纳假设，存在唯一的状态s1，它是d的第一个直接子树的最终状态， s1。S1也是d的第二子树的初始状态。通过重复这个推理，我们得出结论，d的所有直接子树都有唯一的初始和最终状态。d的最后一个子树的唯一最终状态也是d的最终状态。因此，我们认为，PROG和SO的导出树D是唯一确定的。Q4.3共归纳解释如果程序prog在初始状态s0下启动时没有终止，那么prog和s0的派生树具有无限高。这意味着语义学的共归纳和归纳定义流不能连接，因为没有叶子。因此，prog和s0没有唯一的派生树。作为说明，考虑以下示例：例4.4[非终止执行]和例4.2一样，每个状态都是一个变量对及其当前值的列表。左边有一个非终止while循环的程序的语义注释“.”这意味着各个初始或最终状态的值不是唯一确定的。因此，对于prog和s0=[]有几个派生树，所有这些都是为了父节点和子节点的标记之间的关系是有效的WRT。规格。即使不是所有的状态都是唯一定义的，这些派生树也定义了一个唯一的无限状态转换序列，正如我们下面证明的那样定义4.5[状态转换序列]设Spec是一个确定性的自然语义规范，指定相应的规范函数，prog是一个程序，s0是计算的初始状态设d∈gfp（spec）为aprog和s0的派生树。则d，prog的状态转移序列而s0的定义如下：S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）7385prog prog，[ ]，.>i：=1while true doi：=i+1 odi：=5非终止计算导致未定义的初始和最终状态状态s e quen ce（Rj（d1， . ，drj，prog，s0，s））=append（[s0]，state sequence（d1），.，状态序列（dn））状态序列（A i（prog，s0，s））= [s0，s]其中s是唯一确定的最终状态（参见第三种情况，定义4.1）。引理4.6设Spec是一个确定性的自然语义规范，指定相应的规范函数，prog是一个程序，s0是计算的初始状态。设d∈gfp（spec）是prog和s0的一棵导子树.然后，唯一地定义d，prog和s 0的状态转移序列state sequence（d，prog，s0）。证据如果d有有限高，则由定理4.3得出。如果d有无限高和直接子树d1，. . .，dr，则设di，1≤i≤r是无限高的第一个子树。所有的子树d1，...，d i-1有有限的高度和唯一的初始和最终状态。D1具有唯一的初始状态。 通过使用一元余归纳原理（在定理3.3中，设Q是所有有限子树的根以及第一个具有无限高的子树的根具有唯一确定的初始状态的性质），我们得出di具有唯一的状态转移序列。由于该序列是无限的，因此其与子树di+1，.，D R没有任何效果。(The一个无限列表l与任何其他列表lJ的连接再次是列表 （l.） 因此，d有一个定义良好的状态转移序列。Q当程序不终止时，它们通常有不止一个派生树，如例4.4所述。然而，它们的状态转换序列总是相同的。为了证明这一点，我们首先定义了一个派生树的有效部分e_part（d），它只包括那些在计算过程中花费足够时间可以到达定义4.7[导出树的有效部分]导出树d的有效部分，e_part（d），是如下定义的树：如果d具有有限的高度，则e = part（d）= d，e_part（Rj（d1， . ，drj，prog，s，sJ））=86S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）73∈--L∈⊥⊥≤ ≤ −∈Rj（d1， . ，dl−1，e part（dl），prog，s，n）其中l∈ {1，.，rj}，以及d1，.，d l-1有有限高。定理4.8（唯一有效部分）设Spec是一个确定性的自然语义规范，程序是程序执行的初始状态。设spec为相应的指定函数，d，dJ为prog和s的gfp（spec）导出树。 则e part（d）= e part（dJ）。证据如果d和DJ都有有限高，则它直接由定理4.3得出。因此，假设d或dJ具有无限高，并使用二元共归纳原理证明e part（d）=e part（dJ）。因此，我们证明了定理3.4中关于e part（d）和e part（DJ）的两个条件。第一条件：d = Ai（prog，s，sJ）或dJ= Ai（prog，s，sJ），i 1，.， p不存在，因为d和dJ都等于A i（prog，s，sJ）（和有限）b e，因为spec是确定性的。因此，d=Rj（d1， . ，drj，p rog，s，sJ）和dJ=Rl（dJ1， . ，dJrl，p rog，s，sjJ），j，l∈{1， . ，q}。 因为Spec是决定性的，所以Rj=Rl。因此，wlog.， dJ=Rj（dJ1， . ，dJr，p rog，s，sJ J）。因此，我们得出结论，e part（d）= R j（e part（d1），.，e_p（d_r_l），prog，s，）和e_p_r_t（d_J） =R_j（e_p_r_t（d_J_l）， . ，e ∈part（dJrl），p rog，s，），其中表明定理3.4的第一个条件被满足。第二个条件：我们需要证明，e part（d）和e part（dJ）的直接子树的那些不表示树的标记是相同的。这些标记是构造器符号（即所应用的推理规则）、程序注释（Prog的元素）以及e_（d）和e_（J）的直接子树的标记d至少有一个无限子树dl，1≤l≤rj。子树d1，…，d l-1有有限高。d1与DJ1具有相同的初始状态，因此d1=DJ1。(For一个反证，假设d1dJ1. 然后假设，是以从左到右的顺序遍历d1和dJ1时的第一个位置，d1和dj1型二聚体。但这与Spec是确定性的相矛盾）。特别地，我们得出结论：mark（d1）=mark（d1J）。 基于同样的理由重复，我们证明了dk=DJK，对于2 KL1. dl和dJl的标记不需要等于非终止计算的最终状态 不是唯一确定的。尽管如此，它们的标记的部分，在其有效部分是相同的：dl-1和dJl-1的最终状态是相同的，因此dl和dJl的初始状态也是相等的;程序d1和dJ1的标记中的Prog是相同的，因为在d和dJ处应用了相同的推理规则（Spec是确定性的）;并且因为Spec是确定性的，所以恰好有一个推理规则R1适用于d1和dJ1。因此，我们有d1=（R1（. . ），prog，sl，SJl）和dl= Rl（. . ）、prog、s l、sJlJ）。 由此得出，e_（d_l）=（R_l（. . . ），p rog，sl，n）和depart（dJl）=（R l（. . ），prog，s l，prog），完成了第二个条件的证明-S. Glesner/Electronic Notes in Theoretical Computer Science 132（2005）7387orem3.4. 因此，我们得出结论，e part（d）=e part（dJ）。Q推论4.9（唯一状态转换序列）设Spec是一个决定性的自然语义，prog是一个程序，s 是程序执行的初始状态.设spec是相应的规范函数，d， DJ∈gfp（spec）是prog和s 0的导出树。 则状态序列（d，prog，s0）=状态序列（dJ，prog，s0）。证据这直接从定理4.8和引理4.6的证明中使用的结构得出。Q定义4.10[程序的语义]设Spec是一个自然语义，指定相应的指定函数，prog是一个程序。prog的语义Sem（prog）定义为gfp（spec）中所有根标记为prog的派生树的集合：Sem（prog）={d∈gfp（spec）|s，sJ∈ S，P∈ {A1，.，A p，R1，...，R q}。mark（root（d））=（P，prog，s，sJ）}prog对于初始状态s的语义是集合Sem（prog，s0）={d∈Sem（prog）|sJ∈ S，P∈ {A1，.，A p，R1，...，Rq}。mark（root（d））=（P，prog，s0，sJ）}集合Sem（prog，s0）可能包含多个派生树。在这种情况下，计算不会终止。派生树的子树在（wrt.从左到右的深度第一顺序），非终止子树对无限状态转换序列没有贡献，因为它们永远不会被到达。然而，所有派生树的有效部分，Sem（prog，s0）是相同的，并且精确地包含那些对程序的状态转移序列有贡献的5证明演算的应用自然语义学，如果被共归纳地解释，以一种非常优雅