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