第十章代数语义学-ppt课件

1、第十章第十章 代数语义学代数语义学代数语义学是用代数的方法来处置满足一计算逻辑的各种模型。把模型的集合看作是代数构造。代数语义学公理规定算子的组合规那么和约束。算子集和域上值集的关系正好是代数系统研讨的范畴。代数规格阐明成为语法、语义一体化描画的方式根底。10.1 代数根底定义10.1 代数是形如(A，OP)的对偶，其中A是承载子(carrier)集合，OP代表了操作符的有限集。 OPi(a1，a2，an) = as: AA(ai，as A，i = 1n)详细代数 (true，false， ) /布尔代数 (N，+，*) /整数代数 (S，gcd，lcm) /S-代数笼统代数 只给出一笼统的A

2、集合和(组合)算子o，以及在构造中某些必需满足的公理、定理。 笼统代数从更高的层次上研讨构造子和承载子之间的关系，它不规定详细的值集和操作集，只给出一笼统的A集合和(组合)算子o，以及在构造中某些必需满足的公理、定理。中对构造子不同的商定(即应满足的性质)得到不同的笼统代数: 群: (A，o) /o不满足任何定理 半群: (A，o) / o必需满足结合律: x o (y o z) = (x o y) o z 独导半群满足恒等定律: x o (i(a) = x = (i(a) o x /其中(A，o)是一个半群, i是恒等操作(函数) i(a)为A的单位元。假设o是+，A是整数集，i(a) =

3、0。同样假设o是*，i(a) = 1。单位元是相对o而言的。 每一群(A，o , i )中都有一逆操作i-1的独异(A，o，i-1)满足逆定律: x o i-1 = i(a) = i-1 o x 更为笼统的是泛代数(universal algebra) 它把详细代数看作是具有某种操作性质的“对象去研讨各“对象的“关系。 这些“关系被笼统为态射(morphism)。 定义10-2(子代数) 设(A，OP)是一个代数 ，(B，OP)也是一代数且(A，OP)，那么称(B，OP)是(A，OP)的子代数，写为(B，OP)(A，OP)。 定义10-3 (范畴category) 范畴C是(ob(C)，mor

4、p(C)的二元组。其中ob(C)为集合对象X，Y，Z，等的象元集合，morp(C)为C(X,Y)，C(Y,Z)，C(X,Z)，组成的态射集合。C(X,Y)为X到Y的态射(morphism)集合，也可以写作f:XY，fC(X,Y)。X为态射函子ffunction的域(domain)，Y为f的协域(codomain)。公理保证这种映射总是有效。 对于每个态射函数的对偶(f，g)，假设一态射函数的域是另一态射函数的协域，即f:XY; g: YZ，那么可利用组合算子o构成新的态射f o g: XZ。组合算子服从结合律。假设f: XY，g:YZ，h:ZW，那么有: (h o g) o f = h o (

5、g o f): XW对于范畴每一对象X均存在着恒等(identity)态射idx: XX。因此，对任何态射有: idx o f : (XX) o (XY) = XY: f g o idy f : (YZ) o (YY) = YZ: g态射是表达两代数的构造类似性的有力工具。定义定义10-4 (单射，满射，双射单射，满射，双射) 假设有态射函子假设有态射函子f: AB，对于恣意两对象，对于恣意两对象a1，a2A，且，且a1a2，都有，都有f(a1)f(a2)，(f(a1)，f(a2)B)，那么，那么f称为单射称为单射(injective)函子。函子。 对于恣意对于恣意bB都可以找到一个都可以找到

6、一个aA，使得，使得b| =| f (a)，那么，那么f称为满射称为满射(surjective) 函子。函子。 假设假设f:AB的的f既是单射又是满射，那么既是单射又是满射，那么f是可逆的，即存在是可逆的，即存在 f -1 :BA。f称为双称为双射射(bijective) 函子。函子。定义定义10-5(同态映射同态映射homomorphism)假设态射函子假设态射函子f: AB是从代数是从代数(A，OP)到到(B，OP，)的映射。假设对恣意的映射。假设对恣意opOP，a1，a2，anA有有: f (op (a1，a2，an) = op (f(a1)，f(a2)，f(an) (10-1) 其中其

7、中opOP，f(a1)，f(a2)，f(an)B，n = 0，1 k。意即代数。意即代数A中某中某k目操目操作作op，假设将其，假设将其k个变元先映射到代数个变元先映射到代数B中，总可以找到同目的操作中，总可以找到同目的操作op，以映射后，以映射后的变元作变元，其结果和的变元作变元，其结果和op运算后再映射的结果一致。运算后再映射的结果一致。(A，OP)，(B，OP，)是同是同态的。态的。 同理。假设同理。假设f: AB中中f是单射的且满足是单射的且满足(10-1)，那么称单同态，那么称单同态(monomorphism)。 假设假设f是满射的且满足式是满射的且满足式(10-1)，那么称满同态，

8、那么称满同态(epimorphism)。 假设假设f是双射的且满足式是双射的且满足式(10-1)，那么称同构，那么称同构(isomorphism)。 同态坚持两代数构造的类似性，同构即两代数构造相等，仅管其中值集不一样。同态坚持两代数构造的类似性，同构即两代数构造相等，仅管其中值集不一样。 BOOLEAN = (true，false，not) not(true) = false not(false) = true A = (0,1，flip) flip(0) = 1 flip(1) = 0 B(yes,no, maybe，change) change(yes) = no change(no)

9、= yes change(maybe) = maybe C(any，same) same(any) = any 假设有态射函子假设有态射函子h: BOOLEANA。详细定义是。详细定义是: h(true) = 1，h(false) = 0 我们验证我们验证(10-1)式，先看右侧式，先看右侧: h(not(true) = h(flase) = 0 再看右侧再看右侧: flip(h(true) = flip(1) = 0 因此，代数因此，代数BOOLEAN和代数和代数A是同态的，且对于是同态的，且对于0，1均有映射均有映射(满射且直射满射且直射)，故，故BOOLEAN和和A同构。同构。h -1(

10、1) = true，h-1(0) = false成立。成立。 假设有态射函子h:BOOLEANB。同样有: h(true) = yes，h(false) = no 验证(10-1)式可知BOOLEAN，B是同态的。但由于非满射(maybe无对应)，故非同构。 同样，假设有h: BOOLEANC。同样有: h(true) = any，h(false) = any验证(10-1)式: h(not(true) = h(flase) = any same(h(true) = same(any) = any它们依然同态，但由于非直射(非一对一),故非同构。以上仅仅是为阐明概念的非常简单的例子。为了明晰阐

11、明代数间映射关系，常用交换图(commuting diagram)。 h BOOLEAN A h-1 id(BOOLEAN) id(A) 同构 h BOOLEAN A id(BOOLEAN) id(B) h BOOLEAN B 同态 其中id为恒等函数，其值是单位元操作。 图10-1 态射的交换图 程序员在设计程序时如能构造笼统代数，把它写成规格阐明，即Sp代数，再经过中间方式变为实现，可以看作是同态映射变成不同的代数。这就成为公理化自动程序设计的模型。为此，我们还要调查Sp-代数的详细模型。先看-代数。定义10-6(型构Singnature) 型构是表示操作的符号(有限或无限)集。例如，我们

12、在自然数集上指定四个函数符zero，succ，pred，plus，我们就指明了一个代数构造(N，n)。n是这四个函数符的统称叫型构。定义10-7(目Arity) 目是每一函数符所要求的参数个数。对一于中的每一函数符，均有一求目的函数: arity(): N arity(zero) = 0 / 不带参数zero为常(函)数，零目算子。 arity(succ) = 1 arity(pred) = 1 arity(plus) = 2定义定义10-8(-代数代数) 假设一代数其承载子集合假设一代数其承载子集合A仅由仅由操作，那么称操作，那么称(A，A)为为_代数。代数。 我们将同一我们将同一施加于三种

13、承载子集合上，分别得到施加于三种承载子集合上，分别得到(N，N)，(Z，E)，(E，E)三个三个_代数。然而，我们最感兴趣的是承载子元素均可由代数。然而，我们最感兴趣的是承载子元素均可由生成的项生成的项代数。代数。定义定义10-9 (_项，项，_项集，项项集，项_代数代数) 假设假设_代数代数(A，A)中承载子集合中承载子集合A中的每一元素中的每一元素a iA(i=1，n)均可用均可用中的函数符及其复合表示，那么每一用函数符号串表示的项称为中的函数符及其复合表示，那么每一用函数符号串表示的项称为_项。项。 1 假设假设，且为，且为0目函数符，那么目函数符，那么即为即为_项。记为项。记为0 =

14、C。2 假设假设，且为，且为k0目的函数符，那么形如目的函数符，那么形如(t1，t k)的串是的串是_项，项，其中其中t 1，t k也是也是_项。项。记记_项的集合为项的集合为T ，为满足上述规那么的最小项集。，为满足上述规那么的最小项集。3 假设假设T中没有中没有0目目，那么，那么T = 。4 假设假设T那么那么(T，)即为项即为项_代数。代数。 zero，succ(zero)，succ(succ(zero)， pred(zero)，pred(pred(zero)， succ(pred(zero)，pred(succ(zero)， plus(zero，zero)，plus(succ(zero

15、)，zero)，显然，项代数成了承载子集生成语法规那么。按上述项代数定义的承载子集合T是归纳性的，即归纳出常量符号和中每个对这些符号返复操作的最小串的集合。T的归纳性质为导出项的各种特性提供了强有力的证明方法。 1 证明中一切常量符号均具有性质P。2 假定项t1,t k 具有性质P，对于中一切k0目的，证明项(t1,t k)也具有性质P。 这就是所谓构造归纳法。如欲在T上定义函数g，满足以下两个条件就是充分的:1 定义将g运用于常量函数符的结果。2 对于中每个k0目的，经过g(t1),g(tk)来定义g运用于(t1,t k)的结果。定义10-10 (_同态_同构) 设(A，A )，(B，B)是

16、两_代数，h: AB为映射函数，仅当中每个k目的，有: h(A (a 1 ,a k) = B (h(a 1),h(a k) (10-2)那么两代数_同态，h为同态映射。 假设h为双射的那么_同态h: AB即为同构。同构那么阐明中任何函数符假设作用于A的承载子集上为真，作用于B的承载子上亦为真。反之亦然。同样，两代数值集可以不一样。如A = true，false，(，)，B = 1，0，(+*)。定理定理10-1(_同态的独一性、存在性同态的独一性、存在性)对于每个对于每个_代数代数(A，A)都存在独一的都存在独一的_同态映射同态映射 i A: TA (10-3)1 先证同态存在性。先证同态存在

17、性。 对于对于中某个中某个k0目的目的，形如，形如(t1，tk)的项是的项是T的项。按构造归纳法。常量的项。按构造归纳法。常量T项项的的 iA (t1) ，iA(tk)曾经定义。那么曾经定义。那么iA(t1，tk)可定义为可定义为A (iA (t1) ，iA(tk)。这样，。这样，T中的每一元素都作了中的每一元素都作了iA定义。再检查定义。再检查iA能否同态的能否同态的:iA(T (t1，tk ) = iA (A(t1,tk ) /按按T定义定义 = A (iA (t1), ,iA(tk) /按按i A定义定义其中其中T: TT，即将项元组，即将项元组映射为项映射为项(t1，tk)。此证同态。

18、此证同态。2 再证独一性再证独一性 设设h是从是从T 到到A的某个同态映射，只需证明的某个同态映射，只需证明T中的每个中的每个t都有都有iA(t) = h(t)，即，即iA，h重合。重合。iA (t1，tk) = (iA(t1)，iA(tk) /按按i定义定义 = A(h(t1)，h(tk) /按构造归纳按构造归纳 = h (T(t1，tk) / 由于由于h是是同态同态 = h (t1，tk) / 按按T定义定义 iA = h /此证独一此证独一假设我们把T看作程序设计言语的语法，_代数(A，A)看作是语义域或解释。那么本定理阐明言语中的每一表达式或项，在(A，A)中都对应独一的含义，即在语义

19、域中只需一个解释。本定理的另一层意图是试图阐明T是“最小的_代数。10.1.3 全等类定义10-11(-代数类) 具有操作的代数集合称_代数类，记为C。定义10-12(初始代数Initial algebra) 假设代数类C中_代数I是初始代数，仅当对C中每一_代数J都存在着从I到J的独一_同态。 由定理10-1，项代数T在一切_代数的类中是初始的。这就意味着T到任何_代数的值都存在着独一的项映射。这是很强的概念。人们只需标识出某个有“意义的_代数，即可将项映射到该代数的元素上。以此定义项的语义。定理定理10-2 假设假设_代数类代数类C中代数中代数A，B均为初始代数，那么它们必为同构的。均为初

20、始代数，那么它们必为同构的。 证证: 假设假设A为初始的，为初始的，B为普通为普通_代数，按定义代数，按定义10-12它们必存在独一它们必存在独一_同态同态i1: AB。同样，假设。同样，假设B为初始的，为初始的，A为普通为普通_代数，也存在独一代数，也存在独一同态同态i2: BA。它们的复合它们的复合 i1 o i2 = AA = idA同理，同理，i2 o i1 = BB = idB所以，它们是同构的。所以，它们是同构的。 初始代数只在符号方式上区别初始项，只需符号不同就是不同的值。例如，有初始代数只在符号方式上区别初始项，只需符号不同就是不同的值。例如，有_项代数项代数 Bool = t

21、rue，flase，not 其项集是其项集是: T = true，not(true)，not(not(true)， false，not(flase)，not(not(flase)，现实上我们知道现实上我们知道(true，not(false)，not(not(true)，和，和false，not(true)，not(not(false)， 是语义等价的两个类我们记为是语义等价的两个类我们记为true，false。定义定义10-13 (_全等全等congruence) 在在_代数代数(A，A)中，中，A上的关系上的关系R是是_全等关系，假设有全等关系，假设有R(0ik，ai，aiA)成立，仅当对成

22、立，仅当对中每个中每个k目的目的，A(a1，ak)，A (a1，ak) R也成立。也成立。 按上例，按上例，(ture，not(flase)R，那么有，那么有(not(true)，not(not(false)R。全。全等关系假设以等关系假设以符号直接表示两个项是全等的。以上定义是符号直接表示两个项是全等的。以上定义是: 假设假设ture not(false)那么有那么有 not(ture) not(not(false)定义定义10-14 (商代数商代数Quotient Algebra) 对于对于_代数代数(A，A)中的承载子中的承载子aA，按全等关系，按全等关系R归于归于a R那么称商化那么称

23、商化(quotienting)。商化的结果得到全等类集合。商化的结果得到全等类集合A/R = a RaA，且在，且在A/R上上对对中的每个中的每个可定义以下映射可定义以下映射:A/R(a1 R, ,a k R = A(a1，ak) R其中其中A/R A/R，表示表示的全等类。那么称的全等类。那么称(A/R，A/R)为商代数。为商代数。 可以推论可以推论: 1 (A/R，A/R)是是_代数。代数。 2 由于存在由于存在AA/R直射，直射，h(a) = a R也是也是_同态。同态。我们最感兴趣的是在项集我们最感兴趣的是在项集T上的上的_全等。假设一切项对偶全等。假设一切项对偶 R ，根据，根据T的

24、初始性有的初始性有iA: TA，那么，那么iA(t) = iA(t)即即_代数代数A也具有等价关系也具有等价关系R。设设C(R)是一切具有是一切具有R性质的性质的_代数类。代数类。定理定理10-3 (全等的初始性全等的初始性) 在具有性质在具有性质R的代数类中的代数类中_代数代数T/R是初始代数。是初始代数。10.1.4 泛同构映射泛同构映射 给定一操作集，我们可构造一切能够的表达式，也就是对应于给定一操作集，我们可构造一切能够的表达式，也就是对应于的一切的一切能够值集的外延。在这个值集上操作的代数那么称字代数。能够值集的外延。在这个值集上操作的代数那么称字代数。 3+5按前述自然数集上代数按

25、前述自然数集上代数(N，N)是是_代数，但不是字代数代数，但不是字代数.定义定义10-15(泛同构泛同构Universal Isomorphism) 给定一代数，从它的商代数出发可以找到许多同态映射，直到找出同构。给定一代数，从它的商代数出发可以找到许多同态映射，直到找出同构。那么称为泛同构。那么称为泛同构。定义定义10-16(自在字代数自在字代数Free word algebra) 自在字代数是每个项均可为变量的字代数。由于按泛同构实际，从商代数自在字代数是每个项均可为变量的字代数。由于按泛同构实际，从商代数寻觅同构，把字代数要素化要更方便。寻觅同构，把字代数要素化要更方便。E(Y)是有变量

26、并以表达式方式表达的是有变量并以表达式方式表达的承载子集合。承载子集合。例例10-4 _字代数的项集字代数的项集 设设Y = x，y，z， = +，*对于对于_字代数字代数(E(Y)，)能够的项集是能够的项集是: x , y , z , x*y，z+x，x*(y+x*z)，定义定义10-10(Sp-代数代数) 我们称我们称(0，E)为为Sp-代数，其中代数，其中0为常量算子集，为常量算子集，为算子集，为算子集，E为公为公理集。理集。 公理集公理集E是由是由_项表达的全等关系。项表达的全等关系。10.2 代数规格阐明代数规格阐明 数据类型可以以下述等价方式描画数据类型可以以下述等价方式描画: 字

27、代数上的某个全等关系。字代数上的某个全等关系。 字代数的某个商代数。字代数的某个商代数。 代数规格阐明中以代数公理给出全等关系。代数规格阐明中以代数公理给出全等关系。 代数公理是表征两个代数项全等的等式集合代数公理是表征两个代数项全等的等式集合 x = R y(上下文明晰时略去下标上下文明晰时略去下标R) 即为一简单公理。根据公理置换型构中的操作符，即可生成全等类。置换中遵即为一简单公理。根据公理置换型构中的操作符，即可生成全等类。置换中遵照全等性质照全等性质: 自反性自反性 x = y，y = x或或xy(x,y是同一项是同一项) 对称性对称性 y = R x 传送性传送性 x = R y，

28、y = R z 那么那么x = R z 全等性全等性 假设假设xi = R yi，有某操作，有某操作那么那么 xi(x1，xm); yi(y1，ym) 0in假设有一最简单型构: 0: N S: NN和以下公理集: R0 = R1 = 0 = 0 R2 = 0 = S0 R3 = 0 = SS0 R4 = S0 = SS0由这五个公理生成的全等类是: C/R0，R1: 0，S0， SS0，假设S的语义是“后继那么C/R0，R1为自然数集。 C/R2: 0，S0，SS0，为一切项均全等的小代数。 C/R3: 0，SS0，SSSS0， S0，SSS0，SSSSS0，可以看做布尔代数值集(true，

29、false。C/R4: 0，S0，SS0，SSS0，以上(C/Ri，)都是_字代数，由于_全等的关系不同，同态映射为自然数、小代数、布尔代数、二值代数。也阐明_字代数的初始性。每一代数都是一简单数据类型的模型。10.2.1 Sp代数公理代数公理10-10(Sp-代数公理代数公理)公理带有项变量的等式。形如公理带有项变量的等式。形如: r(v1，vn) = s(v1，vn)当变量当变量vi以项以项ti置换后置换后 r(t1，tn) = s(t1，tn)就是全等项。当变量个数为零时即简单公理。就是全等项。当变量个数为零时即简单公理。带变量的公理带变量的公理 设有简单型构设有简单型构 0: N S:

30、 N N +: N N N R5: x + 0 = x; x + Sy = S(x + y) R6: SSx = x; x + 0 = 0; x + S9 = y10.3 数据类型的代数规格阐明数据类型的代数规格阐明 specification TURTH-VALUES sort Truth_Value operations ture: Truth_Value false: Truth_Value not_: Truth_ValueTruth_Value _: Truth_Value , Truth_ValueTruth_Value _: Truth_Value , Truth_ValueTr

31、uth_Value _ = _: Truth_Value , Truth_ValueTruth_Value variablest , u: Truth_Value equations not true = false (10.5-a) not flase = true (10.5-b) ttrue = t (10.5-c) tfalse = false (10.5-d) tu = ut (10.5-e) t true = true (10.5-f) tfalse = t (10.5-g) tu = ut (10.5-h) t=u = (not t )u (10.5-i)end specific

32、ation10.3.1 简单类型的代数规格阐明简单类型的代数规格阐明specification NATURALS include TRUTH_VALUSE sort Natural operations 0 : Natural succ : Natural Natural pred : Natural Natural _ : Natural , Natural Truth_Value _is_ : Natural , Natural Truth_Value _+_ : Natural , Natural Natural _*_ : Natural , Natural Natural varia

33、bles n , m: Natural equations pred succ n = n (10.6.-a) pred0 = 0 (10.6.-b) 00 = flase (10.6.-c) 0succ n = true (10.6.-d) succ n 0 = false (10.6.-e) succ n succ m = nm = mn (10.6.-g) 0 is 0 = true (10.6.-h) 0 is succ n = false (10.6.-i) succ n is succ m = n is m (10.6.-j) n is m = m is n (10.6.-k) 0

34、+n = n (10.6.-l) (succ n)+m (succ (n+m) (10.6.-m) n+m = m+n (10.6.-n) 0*n = 0 (10.6.-o) (succ n)* m = m+(n*m) (10.6.-p) n*m = m*n (10.6.-q)end specification 公理等式描画的是操作符的代数性质，而不是对左边表达式的定义。例如: n+m = m+n /指出+算子的可交换性。 0*n = 0 /指出等式两边表表达式的等价性。 本规格阐明并未显式给出自然数集0，1，2，3，但已给出同构的项集0，succ0，succ succ0，它与以阿拉伯数字表示

35、的自然数集具有完全一致的代数性质。例如，pred(3) = 2，我们有: pred succ succ succ0 = succ succ 0 按公理(10.6-a) 再如，1*n = n，我们有: (succ 0)*n n+(0*n) 按公理(10.6-p) n+0 按公理(10.6-n) 0+n 按公理(10.6-o) n10.3.2 参数化规格阐明参数化规格阐明specification NATURALS_LIST include NATURALSsort Listoperations empty_list: List conr(_,_): Natural , ListList head

36、_of_: ListList tail_of_: ListList length_of: ListNaturalvariables c: Natural l: Listequations head_of_cons(c,l) = c tail_of_cons(c,l) = l tail_ofempty_list = empty_list length_of_empty_list = 0 lenght_of_cons(c,1) = succ(length_of)end specificationspecification LISTS include NATURALS formal sort Com

37、ponent sort Listoperators empty_list: List cons(_,_) : Component , ListList nead_of_ : ListComponent tail_of : ListList length_of : ListNaturalvaribles c: Component l: Listequations head_of_cons(c , l) = c 10.7-a tail_of_cons(cl , l) = l (10.7-b tail_of_empty_list = empty_list 10.7-c length_of_empty

38、_list = 0 10.7-d length_of_cons(c , l) = succ(length_of l )10.7-e end specificaionspecification TRUTH_VALUE_LISTS include instantiation of LISTS by TRUTH_VALUES using Truth_Value for Component renamed using Truth_Value_List for Listend specification(2) 操作参数化操作参数化specification ARRAYS include NATURALS

39、 formal sort Component formal operation maxsize: Natural sort Array operations empty_array : Array modify(_,_,_): Natural , Component , ArrayArray component_of: Natural , ArrayComponent variables c : Component j , j : Natural a : Array equations component i of modify(j , c , a) = c if i is j i maxsi

40、ze (10.8-a) component i of modify(j , c , a) = component i of a if not (i is j) (10.8-b) modify(i , c , a) = a if not (imaxsize) (10.8-c)end specification 作为实例化的一个例子，请看以下的最大长度为6的真假值数组的规格阐明:specification TRUTH_VALUE ARRAYS include instantiation of ARRAYS by TRUTH_VALUES using Truth_Value of Component

41、 succ succ succ succ succ succ 0 for maxsize renamed using Truth_Value_Array for Arrayend specification10.4 演算的代数规格阐明演算的代数规格阐明 演算的演算的，三种归约。假设我们定义一个置换函数三种归约。假设我们定义一个置换函数sub(M , a , b)表示表示a在表达式在表达式M中一切自在出现均以中一切自在出现均以b置换，那么三种归约描画为置换，那么三种归约描画为: if w is not free in M then (u . M) = (w . sub(M , u , w) (x

42、 . M)N) = sub (M , x , N) if x is not free in M then (x . (Mx) = Mspecification LAMBDA_CLACULUS include TRUTH_VALUESsorts Expr , 1doperations firstid: 1d nextid_ : 1d 1d equals(_,_): 1d , 1d Truth_Value var_ : 1d Expr ap(_,_): Expr , ExprExpr abs(_,_): 1d , Expr Expr * sub (_,_,_): Expr , 1d , ExprExpr * notfree(_,_): 1d , ExprTruth_Valuevariables v , w , x , y: 1d M , N , E: Exprequations equals(x , x) = true equals(firstid , next(x) = false equals(nextid(x) , firstid) = false equals(nextid(x) , nextid(y) = equals(x,y) notfree(x,va