2466 女 算 学 报 2016年 缩节点展开成两种情况，其一与ptr！=NULL矛 形状图等价规则限制为单向后得到的蕴涵规则 盾被略去，另一种情况就是图8(2)的形状图.把语 就是一条形状图重写规则.一组形状图重写规则构 句ptrl=ptr当作语句序列dummy=ptr;ptrl= 成一个形状图重写系统.不能用该系统的规则再进 NULL:ptrl=dummy:dummy=NULL,按图6和 行归约的形状图称为最简形状图.不存在无穷归约 图7的规则逐步修改图8(2)，其中dummy是初值 序列的系统称为具有终止性的系统.可以参照项重 为NULL的虚拟局部指针变量.引入dummy主要 写系统继续定义系统的临界对(critical pair)、局部 是为了避免为某些特殊的指针赋值情况设计复杂的 合流性和合流性， 专用规则，见文献[10]的3.1节.对ptr=ptr--next 仿照Knuth-Bendix完备化过程)，可以把文 也继续用类似的方法修改形状图，再把得到的形状 献[10]中2.3节的等价规则集变换成一个与之等价 图用类似图3(3)的规则，把ptr1原先指向的结构节 并且终止与合流的形状图重写系统R 点逆向折叠进左边的浓缩节点，得到图8(1). 下面先以一个简单的项重写系统为例来熟悉项 重写系统的一些概念，然后说明项重写和形状图重 写之间的主要异同.例如，代数等式 x十0=x,x十（一x)=0,(x十y)十之=x十(y十） nex 是属于包含0、加和一元减的自然数等式系统中的 等式，把它们从左到右定向，得到3条重写规则 x+0→x,x+(-x)→0，(x+y)+2→x+(y+之) 项x+(y+(一y)的子项y+(一y)与第2条规则 的左部匹配，因此x十(y+(一y)可用第2条规则 重写成x十0，再依据第1条规则重写为x.不难证 (2) 明这3条规则构成的重写系统是终止的. 图8形状图的两个例子 要证明合流性，需要考察临界对.第3条规则左 部的子项x十y和该规则左部(x'+y)+之'（加撇号 3形状图理论的判定方法 以便区别)合一，得到临界对 ((x'+y')+(+),(x'+(y+之'))+》 形状图的等价推理规则集由文献[10]中2.3节的 该临界对中的两个项都能归约到x'十(y'十(z'十z)) 形状图等价规则（不包括那些推导形状图析取G1VG2 可以类似地计算该重写系统的其它临界对并证明每 的规则，例如本文图3(3))和任何等价推理系统都 一临界对中的两个项都能归约到同一个项，所以该 有的自反、对称和传递规则组成.该规则集可用来证 系统具有局部合流性，再由终止性可得该系统具有 明形状图之间的等价性， 合流性。 若等价形状图的集合E是封闭于可证明的，即 在上述项重写系统中，规则的左部和右部都是 项，被重写的也是项.而形状图系统与项重写系统相 G1台G2蕴涵G台G2∈￡，则把￡叫做形状图的一 比，最大的区别是：规则的左部和右部都是窗口，被 个语法等价理论.类似地可以定义形状图相应的语 重写的是形状图.产生该区别的根源在于形状图是 义等价理论，即=G台G2蕴涵G1台G2∈C.由文献 二维的.基于同样的原因，合一和匹配的描述也有区 [10]中2.4节关于等价规则的性质定理，不难证明 别.但是两个系统的本质概念和方法是一致的， ￡G1台G2当且仅当￡=G,台G2.类似地根据形状图 下面先给出节点相同和形状图相同的定义 的蕴涵规则，可以定义形状图的语法蕴涵理论和语义 定义1.节点1和2若满足下面两个条件，则 蕴涵理论及证明G1→G2当且仅当卡G,→G2: 称m1和n2相同： 本节介绍形状图的重写系统和这两种理论的判 (1)1和2是同类节点，并且若都是声明节点、 定方法。 结构节点或浓缩节点，则有同样的出边及其标记；若 3.1形状图的等价重写系统 都是谓词节点，则谓词名相同. 形状图的等价重写系统可比照代数项的重写系 (2)若1和2是同类浓缩节点或谓词节点，且 统[]来讨论.它用于形状分析和验证过程中对形状 分别带e1与a1和e2与a2,则必须满足(e1==e2A 图进行等价化简. a1)→a2并且(e1==e2∧a2)→a1.其中，无约束浓缩缩节点展开成两种情况，其一与ｐｔｒ！＝ＮＵＬＬ矛 盾被略去，另一种情况就是图８（２）的形状图．把语 句ｐｔｒ１＝ｐｔｒ当作语句序列ｄｕｍｍｙ＝ｐｔｒ；ｐｔｒ１＝ ＮＵＬＬ；ｐｔｒ１＝ｄｕｍｍｙ；ｄｕｍｍｙ＝ＮＵＬＬ，按图６和 图７的规则逐步修改图８（２），其中ｄｕｍｍｙ是初值 为ＮＵＬＬ的虚拟局部指针变量．引入ｄｕｍｍｙ主要 是为了避免为某些特殊的指针赋值情况设计复杂的 专用规则，见文献［１０］的３．１节．对ｐｔｒ＝ｐｔｒ→ｎｅｘｔ 也继续用类似的方法修改形状图，再把得到的形状 图用类似图３（３）的规则，把ｐｔｒ１原先指向的结构节 点逆向折叠进左边的浓缩节点，得到图８（１）． 图８形状图的两个例子 ３形状图理论的判定方法 形状图的等价推理规则集由文献［１０］中２．３节的 形状图等价规则（不包括那些推导形状图析取犌１∨犌２ 的规则，例如本文图３（３））和任何等价推理系统都 有的自反、对称和传递规则组成．该规则集可用来证 明形状图之间的等价性． 若等价形状图的集合犈是封闭于可证明的，即 ! "犌１犌２蕴涵犌１犌２∈!，则把!叫做形状图的一 个语法等价理论．类似地可以定义形状图相应的语 义等价理论，即! #犌１犌２蕴涵犌１犌２∈!．由文献 ［１０］中２．４节关于等价规则的性质定理，不难证明 ! "犌１犌２当且仅当! #犌１犌２．类似地根据形状图 的蕴涵规则，可以定义形状图的语法蕴涵理论和语义 蕴涵理论及证明! "犌１犌２当且仅当! #犌１犌２． 本节介绍形状图的重写系统和这两种理论的判 定方法． ３１形状图的等价重写系统 形状图的等价重写系统可比照代数项的重写系 统［１２］来讨论．它用于形状分析和验证过程中对形状 图进行等价化简． 形状图等价规则限制为单向后得到的蕴涵规则 就是一条形状图重写规则．一组形状图重写规则构 成一个形状图重写系统．不能用该系统的规则再进 行归约的形状图称为最简形状图．不存在无穷归约 序列的系统称为具有终止性的系统．可以参照项重 写系统继续定义系统的临界对（ｃｒｉｔｉｃａｌｐａｉｒ）、局部 合流性和合流性． 仿照ＫｎｕｔｈＢｅｎｄｉｘ完备化过程［１３］，可以把文 献［１０］中２．３节的等价规则集变换成一个与之等价 并且终止与合流的形状图重写系统$． 下面先以一个简单的项重写系统为例来熟悉项 重写系统的一些概念，然后说明项重写和形状图重 写之间的主要异同．例如，代数等式 狓＋０＝狓，狓＋（－狓）＝０，（狓＋狔）＋狕＝狓＋（狔＋狕） 是属于包含０、加和一元减的自然数等式系统中的 等式，把它们从左到右定向，得到３条重写规则 狓＋０→狓，狓＋（－狓）→０，（狓＋狔）＋狕→狓＋（狔＋狕） 项狓＋（狔＋（－狔））的子项狔＋（－狔）与第２条规则 的左部匹配，因此狓＋（狔＋（－狔））可用第２条规则 重写成狓＋０，再依据第１条规则重写为狓．不难证 明这３条规则构成的重写系统是终止的． 要证明合流性，需要考察临界对．第３条规则左 部的子项狓＋狔和该规则左部（狓′＋狔′）＋狕′（加撇号 以便区别）合一，得到临界对 〈（狓′＋狔′）＋（狕′＋狕），（狓′＋（狔′＋狕′））＋狕〉 该临界对中的两个项都能归约到狓′＋（狔′＋（狕′＋狕））． 可以类似地计算该重写系统的其它临界对并证明每 一临界对中的两个项都能归约到同一个项，所以该 系统具有局部合流性．再由终止性可得该系统具有 合流性．在上述项重写系统中，规则的左部和右部都是 项，被重写的也是项．而形状图系统与项重写系统相 比，最大的区别是：规则的左部和右部都是窗口，被 重写的是形状图．产生该区别的根源在于形状图是 二维的．基于同样的原因，合一和匹配的描述也有区 别．但是两个系统的本质概念和方法是一致的． 下面先给出节点相同和形状图相同的定义． 定义１．节点狀１和狀２若满足下面两个条件，则 称狀１和狀２相同： （１）狀１和狀２是同类节点，并且若都是声明节点、 结构节点或浓缩节点，则有同样的出边及其标记；若 都是谓词节点，则谓词名相同． （２）若狀１和狀２是同类浓缩节点或谓词节点，且 分别带ｅ１与ａ１和ｅ２与ａ２，则必须满足（ｅ１＝＝ｅ２∧ ａ１）ａ２并且（ｅ１＝＝ｅ２∧ａ２）ａ１．其中，无约束浓缩 ２４６６ 计 算 机 学 报 ２０１６年