Inleiding Theoretische Informatica Deel II: Equationele specificatie van datatypen

Inleiding Theoretische Informatica Deel II: Equationele specificatie van datatypen Roel de Vrijer najaar 2008

Inhoudsopgave 1 Inleiding

2

2 Algebra¨ısche specificaties

3

3 Afleidbaarheid

10

4 Algebra’s

13

5 Syntax en semantiek

15

6 Initi¨ ele modellen

21

7 Homomorfismes en isomorfie

27

8 Termmodellen

33

1

1 Inleiding/ 2

1

Inleiding

Deze syllabus bestrijkt de collegestof van het tweede gedeelte van het tweedejaarscollege Inleiding Theoretische Informatica, voorjaar 2008. Er wordt in behandeld hoe met behulp van een eenvoudig stelsel vergelijkingen een datatype kan worden gespecificeerd. Deze methode van specificatie is tegelijk de eenvoudigste als ook de meest aansprekende, en waarschijnlijk de meest gebruikte. Het is ´e´en van de belangrijke specificatie-formalismen in de moderne informatica. Voor eenvoudige datatypes is het vaak niet moeilijk om een intu¨ıtief overtuigende specificatie op te schrijven. Dit is ook leuk en instructief. Moeilijker is het om te begrijpen hoe een gevonden specificatie het beoogde datatype ook werkelijk vastlegt, en om in te zien wanneer dat inderdaad gelukt is en wanneer niet. Het stukje algebra¨ısche theorie dat daarvoor nodig is is elegant en vormt een niet te omvangrijk afgerond geheel. Daarover gaat dit onderdeel van Inleiding Theoretische Informatica. De hier behandelde theorie en het gebruikte formalisme komt uit het gebied van de zogenaamde universele algebra. Het gebruikte specificatieformalisme vindt zijn oorsprong in ASF. Dit is een afkorting voor Algebra¨ısch Specificatie Formalisme. Het is ontwikkeld door Bergstra, Heering en Klint, op het Centrum voor Wiskunde en Informatica (CWI) in Amsterdam. De huidige tekst is gebaseerd op de syllabus Algebra¨ısche specificaties uit 1994, van de hand van Yde Venema en Roel de Vrijer en is voor een deel gebaseerd op het boek Algebra¨ısche Specificaties van Wiet Bouma.

2 Algebra¨ısche specificaties/ 3

2

Algebra¨ısche specificaties

In deze paragraaf geven we een formele definitie van het begrip ‘algebra¨ısche specificatie’. Daartoe bespreken we eerst meersoortige verzamelingen en functies. Het is een belangrijke maar bepaald niet opzienbarende observatie dat data altijd van een bepaalde soort zijn, denkt u maar eens aan het voorbeeld van het datum 0: het is van belang te weten of we het over een getal (natuurlijk, geheel, re¨eel) danwel over een waarheidswaarde hebben. Een ander voorbeeld is dat van een verzameling: u hebt ooit eens geleerd onderscheid te maken tussen een object en de singleton verzameling waarvan dat object het enige element is. Nu is het zo dat in vrijwel alle niet-triviale situaties verschillende datasoorten naast elkaar voorkomen. Als voorbeeld bekijken we de soort N van de natuurlijke getallen en de soort van de waarheidswaarden (T en F ). Beide soorten hebben een algebra¨ısche structuur, wat niets anders wil zeggen dan dat er functies zijn gedefinieerd op de verzameling N en de verzameling {T, F }. Op de natuurlijke getallen bijvoorbeeld kennen wij de optelling, de vermenigvuldiging en de opvolgerfunctie, en op de waarheidswaarden de boolese functies. Op dit moment interessanter is het feit dat er ook functies bestaan tussen de beide soorten, bijvoorbeeld de functies even en odd die aangeven of een getal even is (deelbaar door 2) danwel oneven. Een ander voorbeeld van een meersoortige datastructuur wordt gegeven door het datatype van een lijst. Hier zien we dat er twee soorten van data zijn: de soort van de data zelf, en de soort van de lijsten (merk op dat we ook hier weer onderscheid moeten maken tussen een object en de lijst bestaande uit alleen dat object). Voorbeelden van operaties op de soort lijst worden gevormd door het samenvoegen van twee lijsten, bijvoorbeeld door ze achter elkaar te plakken en dan (alfabetisch) te ordenen. Ook bij dit datatype spelen meersoortige functies een rol: neem als voorbeeld de functie die van een object en een lijst een nieuwe lijst maakt door het object achter aan de lijst te zetten. Om zulke voorbeelden wat meer wiskundig cachet te geven, introduceren we de notie van een meersoortige verzameling en een meersoortige functie. Definitie 2.1 (meersoortige verzameling) Laat S een verzameling zijn van elementen die we soortnamen zullen noemen, en stel dat er bij elke s ∈ S een verzameling As is gegeven van waarden van soort s. (Voor verschillende soortnamen s en s0 zijn de verzamelingen As en As0 disjunct, oftewel, As ∩ As0 is leeg.) Gegeven deze indeling in soorten, vormt de vereniging S s∈S As van al deze verzamelingen, meestal genoteerd als (As )s∈S , een S-soortige verzameling. Definitie 2.2 (meersoortige functies) Laat (As )s∈S een S-soortige verzameling zijn; een S-soortige functie is een afbeelding f : As1 × . . . × Asn → As , waarbij s, s1 , . . . , sn soortnamen in S zijn. We noemen het n-tupel (s1 , . . . , sn ) het input-type van f en s het output-type van f . Het paar ((s1 , . . . , sn ), s) heet het (functie-)type van f , en wordt meestal genoteerd als (s1 , . . . , sn ) → s. De verzameling functietypes van S wordt genoteerd als Tp S . Het is eenvoudig na te gaan dat de voorbeelden boven Definitie 2.1 inderdaad bestaan uit meersoortige verzamelingen en functies; de functie even is bijvoorbeeld een functie met als

2 Algebra¨ısche specificaties/ 4 input-type de soort van de natuurlijke getallen, en als output-type de soort van de boolese waarheidswaarden. Nu treden in een programmeertaal natuurlijk niet de verzamelingen en functies zelf op, maar symbolen die er naar verwijzen, oftewel: namen. Om precies vast te leggen wat de namen zijn van de verschillende datasoorten en de functies daartussen, is het begrip signatuur ontwikkeld. Definitie 2.3 (signatuur) Een signatuur is een paar (S, Σ), waarbij S een eindige verzameling soortnamen is, en Σ een eindige verzameling functiesymbolen. We nemen hierbij aan dat elk functiesymbool van een bepaald type is. Een bijzonder geval ontstaat wanneer het input-type van een functiesymbool het lege rijtje is; dergelijke functiesymbolen noemen we constantes. Voorbeeld 2.4 Laten we eerst het voorbeeld bekijken van de natuurlijke getallen met als functies: de opvolgerfunctie succ (met succ(n) ≡ n + 1)1 , de optelling add en de vermenigvuldiging mul. Het is duidelijk dat we hier te maken hebben met een ´e´ensoortig datatype; de verzameling soortnamen S is het singleton {nat}. Als we nu voor de hand liggende namen kiezen voor de functies, bijvoorbeeld succ, add en mul, dan krijgen we dus succ : nat → nat add : nat × nat → nat mul : nat × nat → nat. Voorbeeld 2.5 We veronderstellen dat u het begrip stack al eens ergens bent tegengekomen. Omdat we op dit moment niet ge¨ınteresseerd zijn in de vraag of de stack nu natuurlijke getallen bevat of objecten van een andere soort, nemen we aan dat de objecten van de stack van een verder niet gespecificeerde soort data zijn. We krijgen dus een datatype S met twee soorten: {data, stack}. Als naam voor de lege stack hebben we een constante nodig: empty : → stack. Als naam voor de operatie die het bovenste object van de stack pakt, kiezen we top: Σstack→data is {top}. Verder hebben we nog namen nodig voor de pop-operatie (die de resterende stack oplevert als we het bovenste object van de stack afnemen) en de push-operatie (waarmee een nieuwe stack wordt gevormd door een object op een stack te plaatsen): push : data × stack → stack pop : stack → stack. Tenslotte zal de naam error dienen om aan te geven dat een top-actie is mislukt, omdat men deze op de lege stack toepaste. Om de typeringen consistent te houden, moeten we 1

≡ noteert syntactische gelijkheid.

2 Algebra¨ısche specificaties/ 5 van error dus een constante van soort data maken. Als we nu vervolgens aannemen dat we voor de soort data nog n constanten nodig hebben, vinden we dus: d1 : → data ··· dn : → data error : → data. We merken op dat het in principe niet de bedoeling is dat de constante error als element van stacks wordt gebruikt. Maar de typering van de functie push laat dit wel toe. Voorbeeld 2.6 Als tweede voorbeeld van een tweesoortige signatuur bekijken we het datatype bestaande uit de natuurlijke getallen, de boolese waarheidswaarden en de meersoortige functies op deze beide soorten, zoals we die eerder zijn tegengekomen. De notatie die we hier gebruiken is ontleend aan de specificatietaal ASF en spreekt hopelijk voor zich: module NatBool sorts nat, bool functions 0 : true : false : succ : add : mul : and : or : not : even : odd :

nat nat # nat nat # nat bool # bool bool # bool bool nat nat

-> -> -> -> -> -> -> -> -> -> ->

nat bool bool nat nat nat bool bool bool bool bool

end NatBool Naast de constantes, waarvan de betekenis in een gegeven model vast ligt, hebben we nog symbolen nodig die naar wisselende objecten van het model kunnen verwijzen. We veronderstellen dat we een S-soortige verzameling (Xs )s∈S van variabelen tot onze beschikking hebben. Hierbij is Xs de collectie van variabelen van soort s. (Voor verschillende soortnamen s en s0 zijn de verzamelingen Xs en Xs0 disjunct.) Definitie 2.7 (termen) De verzameling termen van een gegeven signatuur (S, Σ) wordt inductief gedefinieerd, evenals de soort van een term: • De constanten en variabelen van soort s zijn de basistermen van soort s. • Als t1 , . . . , tn termen zijn van de respectievelijke soorten s1 , . . . , sn , en f is een functiesymbool is van soort (s1 , . . . , sn ) → s, dan is f (t1 , . . . , tn ) een term van soort s.

2 Algebra¨ısche specificaties/ 6 Een term heet gesloten als hij geen variabelen bevat (dus alleen constanten en functiesymbolen); termen die niet gesloten zijn heten open. Bij een gegeven S-soortige verzameling X van variabelen, defini¨eren we Ter Σ (X) als de S-soortige verzameling termen waarin alleen variabelen uit X voorkomen. De verzameling Ter Σ (∅) van gesloten termen wordt meestal weergegeven als Ter Σ . De strings x, add(succ(x), y) en mul(0, add(0, y)) zijn voorbeelden van open termen van soort nat in de signatuur NatBool uit Voorbeeld 2.6. Daarentegen zijn 0 en add(0, 0) gesloten termen van soort nat. Het zal duidelijk zijn dat een signatuur vaak verschillende termen bevat die we naar het zelfde object willen laten verwijzen. Beschouw bijvoorbeeld de termen true, not(false), or(true, not(false)) in de signatuur NatBool. We zullen in de volgende paragraaf een formeel afleidingssysteem geven om zulke termen met elkaar te identificeren.2 Om straks de identificatie van twee termen mogelijk te maken, voeren we nu het begrip vergelijking in. Definitie 2.8 (vergelijking) Een vergelijking in een signatuur (S, Σ) is een syntactische string van de vorm t1 = t2 , waarbij t1 en t2 termen van de zelfde soort zijn. Een equationele specificatie is nu niets anders dan een signatuur, waaraan we een verzameling vergelijkingen hebben toegevoegd. Het idee is dat we gelijksoortige termen van de signatuur zullen identificeren op grond van de vergelijkingen. Definitie 2.9 (equationele specificatie) Een (equationele) specificatie is een paar ((S, Σ), E) waarbij (S, Σ) een signatuur is en E een verzameling vergelijkingen over (S, Σ). Voorbeeld 2.10 Als eerste voorbeeld geven de (´e´ensoortige) specificatie Naturals van de natuurlijke getallen, door vergelijkingen toe te voegen aan de signatuur van Voorbeeld 2.4. In de gebruikte ASF-achtige notatie worden de vergelijkingen opgeschreven na de declaratie van de soorten, constanten en functiesymbolen: module Naturals sorts nat functions 0 : succ : nat add : nat # nat mul : nat # nat equations [N1] [N2] [N3] [N4]

-> -> -> ->

add(x,0) add(x,succ(y)) mul(x,0) mul(x,succ(y))

nat nat nat nat

= = = =

x succ(add(x,y)) 0 add(mul(x,y),x)

end Naturals 2 Merk echter op dat we het op dit moment nog maar over de syntax hebben. Termen zijn striktgenomen niet meer dan betekenisloze strings van symbolen.

2 Algebra¨ısche specificaties/ 7 Het idee achter de twee vergelijkingen voor add is dat allereerst iedere gesloten term van de soort nat in de vorm succ(· · · (succ(0) · · ·) gebracht kan worden. Dankzij [N2] kunnen succ-symbolen over het add-symbool getild kunnen worden, zodat het tweede argument van add kan worden afgepeld tot het gelijk is aan 0. Uiteindelijk maakt dan [N1] het mogelijk om het add-symbool te elimineren. Hetzelfde idee ligt ten grondslag aan de twee vergelijkingen voor mul. We geven twee voorbeelden van afleidingen op de basis van deze specificatie. De formele onderbouwing van deze afleidingen zal in de volgende paragraaf gegeven worden. add(S(0), S(0)) = S(add(S(0), 0)) = S(S(0)) mul(S(0), S(0)) = add(mul(S(0), 0), S(0)) = add(0, S(0)) = S(add(0, 0)) = S(0). Voorbeeld 2.11 Als tweede voorbeeld geven we de specificatie Booleans. module Booleans sorts bool functions true : false : and : bool # bool or : bool # bool not : bool equations [B1] [B2] [B3] [B4] [B5]

-> -> -> -> ->

and(true,x) and(false,x) not(true) not(false) or(x,y)

bool bool bool bool bool

= = = = =

x false false true not(and(not(x),not(y)))

end NatBool Voorbeeld 2.12 Als voorbeeld van een tweesoortige specificatie beschouwen we NatBool. module NatBool sorts nat, bool functions 0 : true : false : succ : nat add : nat # nat

-> -> -> -> ->

nat bool bool nat nat

2 Algebra¨ısche specificaties/ 8 mul and or not even odd

: : : : : :

equations [N1] [N2] [N3] [N4] [B1] [B2] [B3] [B4] [B5] [E1] [E2] [E3] [E4]

nat # nat bool # bool bool # bool bool nat nat

-> -> -> -> -> ->

add(x,0) add(x,succ(y)) mul(x,0) mul(x,succ(y)) and(true,x) and(false,x) not(true) not(false) or(x,y) even(0) even(succ(x)) odd(0) odd(succ(x))

nat bool bool bool bool bool

= = = = = = = = = = = = =

x succ(add(x,y)) 0 add(mul(x,y),x) x false false true not(and(not(x),not(y))) true odd(x) false even(x)

end NatBool Als laatste voorbeeld in deze paragraaf geven we de volgende specificatie van het datatype van een stack, gebruikmakend van de signatuur uit Voorbeeld 2.5. Voorbeeld 2.13 module Stack-Of-Data sorts data, stack functions d1: -> data ... dn: -> data error : -> data empty : -> stack push : data # stack -> stack pop : stack -> stack top : stack -> data equations [1] pop(empty) [2] top(empty) [3] pop(push(x,s)) [4] top(push(x,s)) end Stack-Of-Data

= = = =

empty error s x

2 Algebra¨ısche specificaties/ 9 Opgave 2.1 (a) Geef een eindige signatuur voor de verzameling gehele getallen. (b) Vul deze signatuur aan met een geschikt stelsel vergelijkingen.

Opgave 2.2 (a) Geef een signatuur voor een FIFO-queue. (b) Breid deze signatuur uit tot een specificatie door geschikte vergelijkingen toe te voegen (Hint: varieer een beetje op de specificatie Stack-Of-Data uit Voorbeeld 2.13.)

Opgave 2.3 In Voorbeeld 2.12 zijn de specificaties Naturals en Booleans samengevoegd tot ´e´en tweesoortige specificatie NatBool, waarin functiesymbolen zijn bevat die (ge¨ınterpreteerd) aangeven of een getal even is dan wel oneven. Doe nu hetzelfde voor het geval waarin het deelbaarheidspredicaat (dat aangeeft of van twee gegeven getallen het eerste getal een deler is van het tweede) in de specificatie opgenomen wordt.

Opgave 2.4 Beschouw de specificatie voor stacks in Voorbeeld 2.13. 1. Geef vergelijkingen voor de functie concatenate : stack # stack -> stack die twee stacks aan elkaar plakt. Bijvoorbeeld: concatenate(push(d,push(e,empty)),push(f,push(g,empty))) = push(d,push(e,push(f,push(g,empty)))) 2. Geef vergelijkingen voor de functie reverse : stack -> stack die een stack omdraait. Bijvoorbeeld: reverse(push(d,push(e,push(f,empty)))) = push(f,push(e,push(d,empty)))

3 Afleidbaarheid/ 10

3

Afleidbaarheid

Zoals we al in de vorige paragraaf hebben opgemerkt, zijn termen op dit moment nog betekenisloze strings van symbolen. In deze paragraaf defini¨eren voor een specificatie een formeel afeidingssysteem, op grond waarvan we termen zullen identificeren. Daartoe geven we eerst de definitie van het begrip substitutie. Definitie 3.1 (substitutie) Laat (S, Σ) een signatuur zijn en X een verzameling variabelen. Een substitutie is een functie θ : X → Ter Σ (X), waarbij θ(x) steeds een term van dezelfde soort als de variabele x is. Zo’n functie kan inductief worden uitgebreid tot een functie θ¯ : Ter Σ (X) → Ter Σ (X): ¯ θ(x) = θ(x) ¯ θ(c) = c ¯ (t1 , . . . , tn )) = (f (θ(t ¯ 1 ), . . . , θ(t ¯ n )). θ(f θ en θ¯ horen eenduidig bij elkaar, we duiden ze beide aan als substitutie. Merk op dat substituties voorbeelden zijn van meersoortige functies op de verzameling termen. Nu kunnen we algebra¨ısche afleidingssystemen of equationele logica’s defini¨eren: Definitie 3.2 (equationele logica) Laat ((S, Σ), E) een specificatie zijn. De verzameling uit E afleidbare vergelijkingen wordt recursief gedefinieerd als volgt: • (axioma’s) De vergelijkingen in E heten axioma’s en zijn afleidbaar uit E. • (reflexiviteit) Elke vergelijking t = t is afleidbaar uit E. • (symmetrie) Als t1 = t2 afleidbaar is uit E, dan is t2 = t1 dat ook. • (transitiviteit) Als t1 = t2 en t2 = t3 afleidbaar zijn uit E, dan is t1 = t3 dat ook. • (congruentie) Laat de termen t1 , . . . , tn van soort s1 , . . . , sn zijn, en het functiesymbool f van het type (s1 , . . . , sn ) → s. Als alle vergelijkingen ti = ui afleidbaar zijn uit E, dan is de vergelijking f (t1 , . . . , tn ) = f (u1 , . . . , un ) ook afleidbaar uit E. • (substitutie) Laat θ een substitutie zijn. Als t1 = t2 afleidbaar is uit E, dan is ¯ 1 ) = θ(t ¯ 2 ) ook afleidbaar uit E. θ(t Om weer te geven dat de vergelijking t1 = t2 afleidbaar is uit E, gebruiken we de notatie: E ` t1 = t2 . Een afleiding is een rijtje vergelijkingen waarvan elk element `of een axioma is, `of van de vorm t = t, ` of op grond van ´e´en van de afleidingsregels (symmetrie), (transitiviteit), (congruentie) of (substitutie) kan worden verkregen uit eerdere elementen van het rijtje. Als voorbeeld geven we een afleiding in de specificatie NatBool (zie Voorbeeld 2.12) van de identiteit even(add(succ(succ(0)), succ(0))) = false. Daartoe leiden we eerst af dat add(succ(succ(0)), succ(0)) = succ(succ(succ(0))):

3 Afleidbaarheid/ 11 (1) (2) (3) (4) (5) (6)

add(x, succ(y)) = succ(add(x, y)) ([N2]) add(succ(succ(0)), succ(0)) = succ(add(succ(succ(0)), 0)) (1, subst) add(x, 0) = x ([N1]) add(succ(succ(0)), 0) = succ(succ(0)) (3, subst) succ(add(succ(succ(0)), 0)) = succ(succ(succ(0))) (4, cong) add(succ(succ(0)), succ(0)) = succ(succ(succ(0))) (2, 5, trans)

Nu laten we zien dat het rechter lid van vergelijking 6 ‘afleidbaar niet even’ is: (7) (8) (9) (10) (11) (12) (13) (14) (15)

even(succ(x)) = odd(x) ([E2]) even(succ(succ(succ(0)))) = odd(succ(succ(0))) (7, subst) odd(succ(x)) = even(x) ([E4]) odd(succ(succ(0))) = even(succ(0)) (9, subst) even(succ(succ(succ(0)))) = even(succ(0)) (8, 10, trans) even(succ(0)) = odd(0) (7, subst) even(succ(succ(succ(0)))) = odd(0) (11, 12, trans) odd(0) = false ([E3]) even(succ(succ(succ(0)))) = false (13, 14, trans)

We kunnen nu de afleiding afmaken: (16) even(add(succ(succ(0)), succ(0))) = even(succ(succ(succ(0)))) (6, cong) (17) even(add(succ(succ(0)), succ(0))) = false (16, 15, trans) Misschien maken exercities als bovenstaande afleiding een wat formalistische en omslachtige indruk. Toch is hier een waarschuwing op zijn plaats: kijken we bijvoorbeeld naar de specificatie Naturals, dan ligt het misschien voor de hand te geloven dat de vergelijking add(x, y) = add(y, x) afleidbaar zal zijn. Dit is echter niet het geval — we komen hier in Voorbeeld 5.9 op terug. Om nu te laten zien dat bepaalde vergelijkingen niet afleidbaar zijn, kan de algebra¨ısche modeltheorie een nuttig hulpmiddel zijn. Deze theorie wordt in de volgende twee paragrafen behandeld. Opgave 3.1 Geef afleidingen in de specificatie van stacks uit voorbeeld 2.13 van de volgende vergelijkingen: (a) pop(pop(pop(empty))) = empty, (b) pop(push(x, pop(push(x, empty)))) = empty.

Opgave 3.2 (a) Geef in de specificatie Booleans een formele afleiding van de vergelijking and(not(x), not(y)) = not(or(x, y)). Geef bij iedere stap een motivering (zoals in het voorbeeld in de tekst). (b) Geef in de specificatie Naturals een formele afleiding van de vergelijking mul(succ(0), add(0, succ(0))) = succ(0). Geef bij iedere stap weer een motivering.

3 Afleidbaarheid/ 12 Opgave 3.3 In deze opgave gebruiken we de afkorting succn (t) (voor een natuurlijk getal n en een term t) als volgt: succ0 (t) = t succn+1 (t) = succn (succ(t)) Laat zien dat elke gesloten term t in de specificatie Naturals afleidbaar gelijk is aan een term van de vorm succn (0).

Opgave 3.4 Definieer de volgende relatie ∼ op Ter Σ (X): t ∼ u als E ` t = u. Laat zien dat ∼ een equivalentierelatie is.

4 Algebra’s/ 13

4

Algebra’s

Specificaties zijn bedoeld als syntactische representaties van structuren, bijvoorbeeld Naturals voor de natuurlijke getallen met de gebruikelijke operaties. In de volgende paragraaf zullen we zien hoe de koppeling tussen syntax en semantiek formeel kan worden uitgewerkt (deze koppeling kent u overigens al uit inleidende colleges logica). Daartoe ontwikkelen we eerst de nodige terminologie om over de structuren te praten waarin we specificaties zullen interpreteren. Definitie 4.1 (Σ-algebra’s) Laat (S, Σ) een signatuur zijn. Een Σ-algebra Ais een paar (A, IA ) waarbij A een S-soortige verzameling (As )s∈S is, en IA een interpretatie, dat wil zeggen een functie die aan elk functiesymbool uit Σ een S-soortige functie toekent van het juiste type. Met andere woorden: als f een functiesymbool is van type (s1 , . . . , sn ) → s, dan geldt: IA (f ) : As1 × . . . × Asn → As . De verzameling A heet wel de drager van deze algebra. Conventie: In plaats van IA (f ) schrijven we vaak fA . Merk op dat in de definitie van een Σ-algebra niets wordt gezegd over vergelijkingen: elke meersoortige verzameling met meersoortige functies is een Σ-algebra, mits de soorten en types overeenstemmen met de signatuur. Dat betekent bijvoorbeeld dat er algebra’s bestaan van de signatuur Naturals, die niets met de natuurlijke getallen uit hebben te staan. Pas in de volgende paragraaf, wanneer we het begrip ‘waarheid’ defini¨eren, kunnen we dan een eerste selectie maken tussen de schapen (algebra’s waar de vergelijkingen van de specificatie waar zijn) en de bokken (algebra’s waar dit niet het geval is). Voorbeeld 4.2 Laten we eerst de signatuur van de specificatie Naturals kijken. De voor de hand liggende Naturals-algebra is natuurlijk die der natuurlijke getallen. In de notatie van Definitie 4.1 hebben we het over de structuur N = hN, 0N , succN , addN , mulN i, waarbij N de verzameling {0, 1, 2, . . .} van natuurlijke getallen is, 0N het getal 0, en de functies gegeven worden door: succN (n) ≡ n+1 addN (m, n) ≡ m + n mulN (m, n) ≡ m ∗ n. Een Naturals-algebra die hier nog een beetje op lijkt, is die der gehele getallen, namelijk de structuur Z = hZ, 0Z , succZ , addZ , mulZ i; hier is Z de verzameling {. . . , −2, −1, 0, 1, 2, . . .}, en de interpretatie van de constante- en functiesymbolen zijn als boven. Een totaal andere structuur is de volgende: A = hA, 0A , succA , addA , mulA i, waarbij A = {a, b, c} en 0A ≡ a; de interpretaties van de functiesymbolen worden gegeven door de volgende tabellen: a b c

succA a a a

addA a b c

a b c a

b c a b

c a b c

mulA a b c

a c b a

b c b a

c c b a

In dit laatste voorbeeld zien we dat A voldoet aan de enige voorwaarde om een Naturalsalgebra te zijn: de functies succA , addA en mulA zijn alledrie van het juiste type.

4 Algebra’s/ 14 Voorbeeld 4.3 Geschikte algebra’s voor de signatuur van de specificatie Booleans worden gevormd door de verzamelingsalgebra’s. Laat Q een verzameling zijn; we defini¨eren de verzamelingsalgebra over Q als de structuur P(Q) = hP(Q), Ii, waarvan de drager P(Q) de deelverzamelingen van Q als elementen heeft, en de functiesymbolen true, false, not, and en or met behulp van I worden ge¨ınterpreteerd als respectievelijk Q zelf, de lege verzameling, complement, doorsnede en vereniging. Het eenvoudigste voorbeeld van een geschikte boolese algebra is de structuur B2 met als drager de verzameling {T, F }. De constanten true en false worden ge¨ınterpreteerd als respectievelijk T en F , en functiesymbolen not, and en or als respectievelijk de functies ¬, ∧ en ∨, gegeven door de gebruikelijke waarheidstafels:

T F

¬ F T

∧ T T T F F

∨ T T T F T

F F F

F T F

Ook hier vinden we overigens weer ‘absurde’ algebra’s: beschouw bijvoorbeeld de structuur A = hA, trueA , falseA , notA , andA , orA i, gegeven door: A trueA falseA notA (n) andA (m, n) orA (m, n)

= ≡ ≡ ≡ ≡ ≡

{0, 1, 2, . . .} 0 1083 n3 m∗n min(m, n)

5 Syntax en semantiek/ 15

5

Syntax en semantiek

In de vorige paragraaf hebben we gezien dat er bij een gegeven signatuur Σ zeer verschillende Σ-algebra’s bestaan. In de meeste gevallen hebben we echter slechts ´e´en bijzondere Σ-algebra op het oog, het datatype dat we met behulp van vergelijkingen proberen vast te leggen (te specificeren). Denk bijvoorbeeld aan de algebra N van de natuurlijke getallen in het geval van de specificatie Naturals. Van een geslaagde specificatie verwacht je dan natuurlijk dat deze je in staat stelt de oorspronkelijke algebra als zodanig te herkennen. In de eerste plaats zal de gespecificeerde algebra moeten voldoen aan de vergelijkingen van de specificatie. Wat dat precies betekent zullen we in deze paragraaf hard maken. De behandeling sluit nauw aan bij het modelbegrip uit het college Inleiding Logica. Daarmee zijn we er echter nog niet: in het algemeen zullen er meerdere modellen bestaan voor een specificatie. De uiteindelijke selectie van het beoogde model vergt dan ook nog een extra stap, die we zullen behandelen in de volgende paragraaf. Het is waarschijnlijk wel duidelijk wat we bedoelen als we zeggen dat een algebra aan een vergelijking voldoet, of dat de vergelijking waar is in de algebra: het zogenaamde waarheidsbegrip is in de inleidende colleges logica al uitvoerig aan de orde gekomen. Bijvoorbeeld, in de algebra A van Voorbeeld 4.2 is de vergelijking succ(succ(0)) = 0 waar, terwijl A niet voldoet aan de vergelijking mul(x, y) = mul(y, x). In deze paragraaf zullen we dit waarheidsbegrip formeel defini¨eren. Als we nader onderzoeken wat we zoal ondernemen bij het evalueren van de waarheid van een vergelijking in een algebra A, dan blijkt dat we allereerst de linker- en rechter term interpreteren als elementen van (de drager van) A. Met andere woorden: we geven de syntax een semantiek. Van de inleidende college’s logica herinnert u zich wellicht, dat dit interpretatieproces inductief gedefinieerd werd, met clausules als ι(f (t1 , . . . , tn )) ≡ fA (ι(t1 ), . . . , ι(tn )). (Hierbij staat ι(t) voor de interpretatie van term t in de algebra A, en is f een n-plaatsig (´e´ensoortig) functiesymbool). Als we uit willen rekenen wat de interpretatie is van een open term, dan moeten we natuurlijk eerst weten wat de interpretatie van de variabelen is. Daartoe wordt het begrip ‘assignment’ ge¨ıntroduceerd: Definitie 5.1 (assignment) Laat X een (meersoortige) verzameling variabelen zijn van een signatuur Σ, en A een Σ-algebra met drager A. Een (S-soortige) functie θ : X → A heet een assignment (van elementen van A aan variabelen uit X). Als ook de betekenis van de variabelen bekend is doordat we een assignment gedefinieerd hebben, dan ligt de interpretatie van alle termen vast. Definitie 5.2 Laat A een Σ-algebra zijn, en θ een assignment van variabelen uit de verzameling X aan elementen van A. Definieer de volgende functie θ¯ : Ter Σ (X) → A: ¯ θ(x) ≡ θ(x) ¯ θ(c) ≡ cA ¯ ¯ 1 ), . . . , θ(t ¯ n )) θ(f (t1 , . . . , tn )) ≡ fA (θ(t

voor variabelen x, voor constantes c, voor complexe termen.

5 Syntax en semantiek/ 16

Op de verzameling TerΣ van gesloten termen hangt θ¯ niet af van θ. In dat geval wordt θ¯ ook weergegeven als eval A . We kunnen nu een precieze definitie geven van het begrip waarheid: Definitie 5.3 (waarheid) Laat (S, Σ) een signatuur zijn en A een Σ-algebra. Een vergelijking t1 = t2 is waar in A, notatie: A |= t1 = t2 , als voor elke assignment θ van de variabelen ¯ 1 ) en θ(t ¯ 2 ) identiek zijn. t1 en t2 , de interpretaties θ(t Een verzameling vergelijkingen E is waar in een algebra A, notatie: A |= E, als elke vergelijking uit E waar is in A. Voorbeeld 5.4 Laten we twee eerder genoemde voorbeelden nu eens nader en formeler bekijken. Om te beginnen onderzoeken we de waarheid van de vergelijking succ(succ(0)) = 0 in de algebra A van Voorbeeld 4.2. Omdat de vergelijking geen variabelen bevat, hoeven we alleen naar de functie eval A te kijken; voor het rechterlid van de vergelijking geldt: eval A (0) ≡ 0A ≡ a. Voor het linkerlid van de vergelijking moeten we weten hoe het symbool succ wordt ge¨ınterpreteerd. Met behulp van de tabel vinden we: eval A (succ(succ(0))) ≡ ≡ ≡ ≡

succA (succA (0A )) succA (succA (a)) succA (a) a.

Uit de bovenstaande gelijkheden volgt dus dat eval A (succ(succ(0))) ≡ eval A (0). Met andere woorden: de termen succ(succ(0)) en 0 worden door het zelfde element (namelijk: a) ge¨ınterpreteerd; dat betekent dat de vergelijking succ(succ(0)) = 0 inderdaad waar is in de algebra A. Om te laten zien dat de vergelijking mul(x, y) = mul(y, x) niet waar is in A, moeten we iets meer werk verrichten: deze vergelijking bevat immers variabelen. We zoeken twee elementen van de drager A van de algebra, waarvoor de functie mulA niet commutatief is, bijvoorbeeld a en b. Vervolgens defini¨eren we de assignment θ als volgt: θ(x) ≡ a, θ(y) ≡ b. Dan geldt: ¯ ¯ ¯ θ(mul(x, y)) ≡ mulA (θ(x), θ(y)) ≡ mulA (θ(x), θ(y)) ≡ mulA (a, b) ≡ b, terwijl ¯ θ(mul(y, x)) ≡ mulA (b, a) ≡ c. We hebben dus een voorbeeld van een assignment θ waarbij het linker- en het rechterlid van de vergelijking op verschillende elementen van A worden worden afgebeeld; er geldt A 6|= mul(x, y) = mul(y, x).

5 Syntax en semantiek/ 17 Met behulp van dit waarheidsbegrip kunnen we nu voor een specificatie ((S, Σ), E) de eerste schifting maken in de klasse van Σ-algebra’s: Definitie 5.5 (model) Een Σ-algebra A is een model voor een specificatie ((S, Σ), E) als A |= E. In de praktijk zullen we vaak gewoon zeggen dat A een model is voor E in plaats van voor ((S, Σ), E). Voorbeeld 5.6 Het is niet zo moeilijk om in te zien dat de algebra N van de natuurlijke getallen (Voorbeeld 4.2) een model is voor de specificatie Naturals. De algebra A uit hetzelfde Voorbeeld is geen model voor deze specificatie; de reden hiervoor is niet dat A 6|= mul(x, y) = mul(y, x), immers deze vergelijking behoort niet tot de verzameling E. We moeten dus een ander tegenvoorbeeld zoeken. We laten het over aan de lezer om te laten zien dat bijvoorbeeld de vergelijking add(x, succ(y)) = succ(add(x, y)) niet waar is in A. Het is overigens niet zo dat we nu alle onintu¨ıtieve algebra’s hebben gediskwalificeerd, getuige het volgende voorbeeld van de Naturals-algebra O. De drager O van O is de singleton {∗} — merk op dat dit de interpretatie van alle constante- en functiesymbolen vastlegt (hoe?). Er geldt zelfs voor elke interpretatie θ en elke term t dat ¯ ≡ ∗. θ(t) Maar dit betekent dat elke vergelijking t1 = t2 waar is in O. In het bijzonder is O dus een model voor de vergelijkingen van de specificatie Naturals. In Voorbeeld 5.9 en in Opgave 5.2 zullen we nog weer andere modellen voor de specificatie Naturals tegenkomen. Uit bovenstaande voorbeelden blijkt dat een specificatie nog steeds meerdere (en soms onverwachte) modellen kan hebben. In de volgende paragrafen zullen we een nadere schifting maken binnen de klasse van modellen voor een specificatie. Als belangrijke toepassing van het waarheidsbegrip behandelen we nu een semantisch hulpmiddel om aan te tonen dat een vergelijking niet afleidbaar is uit een specificatie. Daartoe introduceren we eerst de notie ‘semantisch gevolg’. Definitie 5.7 (semantisch gevolg) Laat ((S, Σ), E) een specificatie zijn. Een vergelijking t1 = t2 volgt semantisch uit E, notatie: E |= t1 = t2 , als t1 = t2 waar is in elk model voor E. Het belang van de semantische gevolg-relatie ligt in het feit dat ze equivalent is met de afleidbaarheidsrelatie. Dit betekent bijvoorbeeld dat als we willen laten zien dat de vergelijking t1 = t2 niet afleidbaar is uit een specificatie E, dat we dan kunnen volstaan met te laten zien dat er een model is voor E waar t1 = t2 niet waar is. We maken dan gebruik van de de Correctheidsstelling, die we hier vermelden zonder bewijs.

5 Syntax en semantiek/ 18 Stelling 5.8 (correctheid) Laat (S, Σ) een signatuur zijn, en E een verzameling vergelijkingen; dan geldt voor elke vergelijking t = u: E ` t = u ⇒ E |= t = u. Dit is ´e´en richting van de genoemde equivalentie van semantisch gevolg en afleidbaarheid. De andere richting is de Volledigheidsstelling, beter bekend als de Stelling van Birkhoff. Een belangrijke toepassing van de Correctheidsstelling is, dat we nu een manier hebben om te bewijzen dat een vergelijking niet afleidbaar is uit een specificatie. Voorbeeld 5.9 We zullen laten zien dat we niet uit de specificatie Naturals van de natuurlijke getallen kunnen bewijzen dat de optelling commutatief is, oftewel dat de vergelijking add(x, y) = add(y, x) niet afleidbaar is. Daartoe bekijken we het volgende niet-standaard model voor de specificatie Naturals3 : C = hN × N, 0C , succC , addC , mulC i, waarbij ≡ (0, 0) ≡ hz,  b + 1i hz1 , b1 + b2 i als z2 ≡ 0 addC (hz1 , b1 i, hz2 , b2 i) ≡ hz1 + z2 , b2 i als z2 6≡ 0 0C succC (hz, bi)

Deze ingewikkeld ogende structuur wordt misschien iets eenvoudiger met behulp van het volgende ezelsbruggetje: we beschouwen een element hz, bi van de algebra als een stapel bestaande uit z zware dozen, met daar bovenop geplaatst b breekbare dozen. De ‘optelling’ addC (hz1 , b1 i, hz2 , b2 i) bestaat dan uit het plaatsen van de stapel hz2 , b2 i op de stapel hz1 , b1 i. Als de bovenste stapel zware dozen bevat (dat wil zeggen, als z2 6≡ 0), dan worden alle breekbare dozen uit de onderste stapel vernietigd; er blijven dus z1 + z2 zware dozen en b2 breekbare dozen over. De ‘successor’ succ C (hz, bi) bestaat uit het plaatsen van een lichte doos bovenop de stapel hz, bi. We zullen nu aantonen dat C een model is voor de specificatie Naturals. Daartoe moeten we laten zien dat [N1] en [N2] waar zijn in C. We bewijzen eerst dat C |= [N1]. Laat θ een assignment zijn van elementen uit N × N aan de variabele x; stel dat θ(x) ≡ hz, bi. ¯ θ(add(x, 0)) ≡ ≡ ≡ ≡ ≡ ≡

¯ ¯ addC (θ(x), θ(0)) addC (θ(x), 0C ) addC (hz, bi, h0, 0i) hz, bi θ(x) ¯ θ(x)

We bewijzen nu dat C |= [N2]. Laat θ een assignment zijn van elementen uit N × N aan de variabelen x en y; stel dat θ(x) ≡ hz1 , b1 i en θ(y) ≡ hz2 , b2 i. Het is eenvoudig in te zien dat het voldoende is om aan te tonen dat addC (hz1 , b1 i, succC (hz2 , b2 i)) ≡ succC (addC (hz1 , b1 i, hz2 , b2 i)). Onderscheid de volgende gevallen: 3

Om de definitie begrijpelijk te houden, laten we de interpretatie van het functiesymbool mul weg.

5 Syntax en semantiek/ 19 geval z2 ≡ 0 ; dan geldt addC (hz1 , b1 i, succC (hz2 , b2 i)) ≡ ≡ ≡ ≡

addC (hz1 , b1 i, hz2 , b2 + 1i) hz1 , b1 + b2 + 1i succC (hz1 , b1 + b2 i) succC (addC (hz1 , b1 i, hz2 , b2 i)).

geval z2 6≡ 0 ; nu geldt addC (hz1 , b1 i, succC (hz2 , b2 i)) ≡ ≡ ≡ ≡

addC (hz1 , b1 i, hz2 , b2 + 1i) hz1 + z2 , b2 + 1i succC (hz1 + z2 , b2 i)) succC (addC (hz1 , b1 i, hz2 , b2 i)).

Aan de andere kant geldt niet dat de vergelijking add(x, y) = add(y, x) waar is in C. Beschouw bijvoorbeeld de assignment θ met θ(x) ≡ h1, 0i (‘´ e´en zware doos’) en θ(y) ≡ h0, 1i (‘´e´en breekbare doos’). Er geldt ¯ θ(add(x, y)) ≡ addC (θ(x), θ(y)) ≡ addC (h1, 0i, h0, 1i) ≡ h1, 1i, terwijl ¯ θ(add(y, x)) ≡ addC (θ(y), θ(x)) ≡ addC (h0, 1i, h1, 0i) ≡ h1, 0i. In woorden: het maakt verschil of je een zware doos op een breekbare zet, of andersom. We hebben dus laten zien dat commutativiteit van de optelling niet een semantisch gevolg is van de vergelijkingen [N1] en [N2]. Maar dan volgt met behulp van de Correctheidsstelling dat de vergelijking add(x, y) = add(y, x) ook niet afleidbaar kan zijn uit de specificatie Naturals. Opgave 5.1 Beschouw de algebra P(V ) van deelverzamelingen van een verzameling V , als in Voorbeeld 4.3. Laat zien dat P(V ) een model is voor Booleans.

Opgave 5.2 Beschouw de algebra B = hB, Ii voor de specificatie Naturals. Hierbij is B de verzameling {T, F }, en worden de functiesymbolen als volgt ge¨ınterpreteerd: I(0) ≡

T

I(succ) ≡

¬

I(add) ≡

xor

I(mul) ≡

∨.

Deze functies worden vervolgens gegeven door de volgende tabellen: T F

¬ F T

xor T T T F F

Laat zien dat B een model is voor Naturals.

F F T

∨ T F

T T T

F T F

5 Syntax en semantiek/ 20 Opgave 5.3 Laat zien dat voor elke algebra A, elke assignment θ en elke gesloten term t geldt: ¯ ≡ eval A (t). θ(t)

Opgave 5.4 Laat zien dat de vergelijking even(x) = not(odd(x)) niet afleidbaar is in de specificatie NatBool. (Hint: beschouw een model voor Naturals met als drager de verzameling N ∪ {ω}, dat wil zeggen voeg het ‘getal’ ω toe aan de verzameling der natuurlijke getallen. Er dient nog wel enig puzzelwerk te worden verricht om de interpretatie zodanig te kiezen, dat de verkregen algebra inderdaad een model is voor de specificatie Naturals.)

6 Initi¨ele modellen/ 21

6

Initi¨ ele modellen

In de vorige paragraaf hebben we gezien, dat we een aantal ongewenste algebra’s voor een specificatie ((S, Σ), E) konden afwijzen door ons te beperken tot de klasse van modellen voor de vergelijkingen in E. We hebben echter ook gezien dat er binnen de klasse van modellen voor een specificatie nog steeds een grote verscheidenheid aan structuren kan bestaan. De vraag is dan of we niet verder kunnen gaan met het uitzonderen van die modellen voor de specificatie die onze voorkeur hebben. We merkten overigens al eerder op dat we in de praktijk meestal met de omgekeerde situatie te maken hebben, namelijk waarin we uitgaan van een specifieke algebra (bijvoorbeeld die van de natuurlijke getallen met de gebruikelijke operaties). Het doel van het opstellen van een specificatie is dan juist om deze ene algebra zo nauwkeurig en zo bondig mogelijk te beschrijven. We kunnen onszelf dan de vraag stellen, hoe ‘goed’ een gegeven specificatie is. Een specificatie is ‘goed’ als de bedoelde structuur een unieke plaats inneemt binnen de klasse van modellen voor de specificatie. In Definitie 6.5 zullen we dit idee preciseren. Laten we eerst eens kijken naar twee modellen voor de specificatie Naturals die een aantal onprettige eigenschappen hebben. Om te beginnen beschouwen we het model C uit Voorbeeld 5.9. Bij een nadere analyse van deze algebra blijkt dat het ‘natuurlijke’ gedeelte van dit model (dat wil zeggen, de paren h0, bi) zich goed gedraagt, maar dat de paren van de vorm hz, bi met z > 0 de problemen veroorzaken. Merk nu op dat elk ‘natuurlijk’ element de interpretatie is van een gesloten term, terwijl dit voor geen enkel ‘onnatuurlijk’ element het geval is. Elementen van een algebra die niet de interpretatie zijn van een gesloten term noemen we ‘junk’ (rotzooi). Ons tweede voorbeeld is het Naturals-model B uit Opgave 5.2. Waar C te groot is, in de zin dat het junk bevat, is het model B te klein: er worden bijvoorbeeld veel meer verschillende termen hetzelfde ge¨ınterpreteerd als de constante 0 dan noodzakelijk is op grond van de vergelijkingen in Naturals. Merk op dat we bij een gegeven specificatie kunnen bepalen welke termen noodzakelijkerwijs door hetzelfde element moeten worden ge¨ınterpreteerd: de termen die afleidbaar gelijk zijn. Laten we zeggen dat een element van een algebra voor confusion zorgt, als het de interpretatie is van twee gesloten termen s en t waarvoor de vergelijking s = t niet afleidbaar is uit de specificatie. In het model B zorgt het element T dus voor confusion, omdat geldt dat eval B (0) ≡ eval B (succ(succ(0))) ≡ T , terwijl de vergelijking 0 = succ(succ(0)) niet afleidbaar is in de specificatie Naturals (waarom niet?). Modellen, die geen junk en geen confusion bevatten, noemen we initi¨ele modellen. Definitie 6.1 (initieel model) Laat A een model zijn voor een specificatie ((S, Σ), E). A bevat junk als A elementen bevat die niet de interpretatie zijn van een gesloten term, A bevat confusion als A gesloten termen t en u identificeert, zonder dat t = u afleidbaar is uit E. Formeel: ”no junk”: ∀a ∈ A ∃t ∈ Ter Σ eval A (t) ≡ a, ”no confusion”: ∀t, u ∈ Ter Σ (eval A (t) ≡ eval A (u) ⇒ E ` t = u). A heet een initieel model voor E als A geen junk en geen confusion bevat.

Voorbeeld 6.2 Als standaardvoorbeeld van een initieel model nemen we de algebra N van de natuurlijke getallen voor de specificatie Naturals. We bewijzen eerst dat N geen junk bevat; daartoe moeten we dus laten zien dat elk natuurlijk getal de interpretatie is

6 Initi¨ele modellen/ 22 in N van een gesloten term. Intu¨ıtief zal duidelijk zijn dat we elk getal n kunnen lezen als de n-de opvolger van het getal 0. Wat formeler kunnen we laten zien dat voor elke n ∈ N: n ≡ eval N (succ( . . . (succ( 0)) . . . ) (1) | {z } n maal Het bewijs van (1) verloopt met natuurlijke inductie. Het is iets lastiger om te laten zien dat N geen confusion bevat. Dit bewijs verloopt in twee stappen: eerst bewijzen we dat elke gesloten term in Naturals is afleidbaar gelijk aan een term van de vorm succn (0).

(2)

Het bewijs van (2) is gegeven in Opgave 3.3. Met behulp van (2) kunnen we vervolgens als tweede stap direkt aantonen: N bevat geen confusion.

Stel immers dat 6` t = t0 . We moeten laten zien dat t en t0 dan ook door verschillende getallen worden ge¨ınterpreteerd, oftewel dat eval (t) 6≡ eval (t0 ). 0

Wegens (2) bestaan er getallen n en n0 z´o dat ` t = succn (0) en ` t0 = succn (0). Omdat N een model is voor Naturals, geldt dan (met (1)): eval N (t) ≡ eval N (succn (0)) ≡ n 0 eval N (t0 ) ≡ eval N (succn (0)) ≡ n0 . Stel nu dat eval N (t) ≡ eval N (t0 ). Dan geldt dat n ≡ n0 , zodat de termen succn (0) 0 en succn (0) identiek zijn. Met behulp van de afleidingsregels (reflexiviteit) en (transitiviteit) is dan eenvoudig een afleiding van de vergelijking t = t0 te vinden. Dat geeft een tegenspraak met de aanname 6` t = t0 . Er moet dus wel gelden dat eval (t) 6≡ eval (t0 ).

Voorbeeld 6.3 Voor de specificatie Booleans is de algebra B2 uit Voorbeeld 4.3 een initieel model. Het bewijs dat B2 een model is voor Booleans laten we achterwege (dit volgt overigens uit de Opgaves 5.1 en 7.9). Aangezien T ≡ eval B2 (true) en F ≡ eval B2 (false), bevat B2 geen junk. Om te laten zien dat B2 geen confusion bevat, bewijzen we eerst dat voor elke gesloten term t geldt: ` t = true of ` t = false.

(3)

We bewijzen (3) met inductie naar de complexiteit van t. Voor het basisgeval hebben we te maken met de termen true en false en volgt de bewering uit de regel (reflexiviteit). Voor de inductiestap behandelen we alleen het ingewikkeldste geval, namelijk waar t van de vorm or(t0 , t00 ) is. De inductiehypothese stelt nu dat ` t0 = true of ` t0 = false en ` t00 = true of ` t00 = false.

6 Initi¨ele modellen/ 23 Er zijn dus vier mogelijkheden, waarvan we alleen de volgende onderzoeken: ` t0 = true en ` t00 = false.

(†)

Beschouw nu de volgende afleiding: (1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12)

not(true) = false (B3) and(not(true), x) = and(false, x) (1, congr) and(false, x) = false (B2) and(not(true), x) = false (2, 3, trans) not(and(not(true), x)) = not(false) (4, congr) not(false) = true (B4) not(and(not(true), x)) = true (5, 6, trans) not(and(not(true), not(false))) = true (7, subst) or(y, z) = not(and(not(y), not(z))) (B5) or(true, false) = not(and(not(true), not(false))) (9, subst) or(true, false) = true (8, 10, trans) 0 00 or(t , t ) = true (11, †, cong)

Het volgt onmiddellijk dat in dit geval de vergelijking t = true afleidbaar is. Dit bewijst (een geval van) (3). Stel nu dat s en t gesloten term zijn en dat de vergelijking s = t niet afleidbaar is uit de specificatie. Wegens (3) zijn er dan twee mogelijkheden: ` s = true en ` t = false of ` t = true en ` s = false. In beide gevallen zullen s en t als verschillende elementen van de algebra B2 worden ge¨ınterpreteerd. Dat betekent dat B2 geen confusion bevat. We geven nu ter lering en vermaak een heel eenvoudig voorbeeld van een specificatie en nodigen de lezer uit er zelf een initieel model voor te construeren. Voorbeeld 6.4 Beschouw we de specificatie Toy, gegeven door: module Toy sorts thing functions c : d : nxt : thing

-> thing -> thing -> thing

equations [T1] nxt(nxt(c)) = d [T2] nxt(nxt(nxt(x))) = x end Toy

6 Initi¨ele modellen/ 24 In veel gevallen (zoals dat van de specificatie Naturals) hebben we bij het opstellen van een specificatie ´e´en speciaal model in ons achterhoofd (bijvoorbeeld de structuur der natuurlijke getallen), en vragen we ons af, in hoeverre de gegeven specificatie dat ene model karakteriseert. Laten we proberen hiervoor een formeel criterium op te stellen: Definitie 6.5 (initieel correcte specificatie) Laat A een Σ-algebra zijn voor een zekere signatuur (S, Σ). Een specificatie ((S, Σ), E) heet een initieel correcte specificatie als A een initieel model is voor ((S, Σ), E). Uit de Voorbeelden 6.2 en 6.3 blijkt, dat Naturals een initieel correcte specificatie is van het model N der natuurlijke getallen, en Booleans voor het model B2 van de waarheidswaarden. Kun je nu zeggen dat een initieel correcte specificatie het bijbehorend initieel model karakteriseert? Ja en nee. Er kunnen weliswaar meerdere initi¨ele modellen bestaan voor ´e´en en dezelfde specificatie, maar als dat zo is, dan zijn die modellen toch weer zo verwant dat je ze kunt zien als verschillende versies van hetzelfde. Die verwantschap heet isomorfie: alle initi¨ele modellen voor een gegeven specificatie zijn isomorf. Daarom kunnen we toch spreken van het initi¨ele model voor een specificatie. Om dit allemaal goed te kunnen begrijpen en precies te maken hebben een definitie nodig van het begrip isomorfie, en daarvoor moeten we eerst homomorfismes bestuderen tussen algebra’s. Dat gebeurt in de volgende paragraaf. Opgave 6.1 Geef voor de specificatie Booleans een model dat (a) junk bevat, maar geen confusion, (b) geen junk bevat, maar wel confusion, (c) zowel junk als confusion bevat.

Opgave 6.2 (a) Geef een initieel model voor de specificatie Toy uit Voorbeeld 6.4. (b) Bewijs dat het gevonden model geen junk bevat. (c) Bewijs dat het geen confusion bevat.

Opgave 6.3 Beschouw de algebra¨ısche specificatie Get = ((S, Σ), E) met: S: Σ:

soort constanten functies

E:

vergelijkingen

I n: S: P:

→I I→I I→I

[1] [2]

S(P(x)) P(S(x))

= =

x x

Verder zijn de volgende vier Σ-algebra’s K, N, Z en R gegeven: K:

IK = {0, 1}

nK ≡ 0

N: R: Z:

IN = N IR = R IZ = Z

nN ≡ 0 nR ≡ 0 nZ ≡ 0

SK (0) ≡ SK (1) ≡ SN (x) ≡ SR (x) ≡ SZ (x) ≡

1 0 x+1 x+1 x+1

PK (0) PK (1) PN (x) PR (x) PZ (x)

≡ ≡ ≡ ≡ ≡

1 0 max(x − 1, 0) x−1 x−1

6 Initi¨ele modellen/ 25 (a) Onderzoek voor deze algebra’s of het modellen zijn van Get. (b) Onderzoek of ´e´en (of meerdere) van deze modellen een initieel model is van Get. Geef in de niet-initi¨ele modellen eventuele junk en/of confusion aan.

Opgave 6.4 Gegeven is de volgende specificatie Spec: module Spec sorts object functions a : h : s :

-> -> ->

object object

equations [E1] h(h(x)) [E2] s(h(x))

= =

object object object

x s(x)

end Spec

Voor deze specificatie beschouwen we de volgende Σ-algebra’s K, L, M en N. K: L: M: N:

K = N, aK ≡ 0, hK (n) ≡ n + 1, sK (n) ≡ n2 . L = Z, aL ≡ 0, hL (z) ≡ −z, sL (z) ≡ z 2 . M = Z, aM ≡ 0, hM (z) ≡ −z, sM (z) ≡ |z| + 1. N = {2, 4, 16, . . .}, aN ≡ 2, hN (x) ≡ x, sN (x) ≡ x2 .

(a) Geef een afleiding voor de volgende vergelijking: s(s(h(a))) = s(h(s((a))). (b) Precies ´e´en van de algebra’s K, L, M, N is geen model voor de specificatie Spec. Geef aan welke dat is en waarom. (c) Ga voor elk van de drie algebra’s van K, L, M, N die een model zijn voor Spec na of het een initieel model is voor Spec. Alleen negatieve antwoorden moeten worden gemotiveerd door het aangeven van junk en/of confusion. Opgave 6.5 Geef een initieel correcte specificatie voor de Naturals-algebra B van Opgave 5.2.

Opgave 6.6 Geef een initeel correcte specificatie (inclusief een declaratie van alle functiesymbolen) voor de algebra Z van gehele getallen, met optelling en aftrekking.

Opgave 6.7

6 Initi¨ele modellen/ 26 (a) Gegeven is de algebra Z = (Z, 0, succ, pred) waarbij zero ≡ 0, en succ en pred) gegeven worden door succ(z) ≡ z + 1 pred(z) ≡ z − 1. Geef een initieel correcte specificatie voor Z. (b) Breid deze specificatie uit tot een initieel correcte specificatie voor de algebra Z+ = (Z, 0, succ, pred, neg) waarbij neg de functie is met neg(z) ≡ −z.

7 Homomorfismes en isomorfie/ 27

7

Homomorfismes en isomorfie

In deze paragraaf laten we zien dat elke algebra¨ısche specificatie in feite maar ´e´en initieel model heeft. Dat is niet echt zo, maar als er meer zijn, dan hebben die precies dezelfde struktuur, waardoor je eigenlijk kunt beschouwen als verschillende “uitvoeringen” van hetzelfde model. Technisch drukken we dat uit door te zeggen dat zulke modellen isomorf zijn. Om het begrip isomorfie te begrijpen moeten we kijken naar afbeeldingen tussen algebra’s. In het bijzonder gaat het dan om speciale afbeeldingen: homomorfismes en isomorfismes. Definitie 7.1 (homomorfismes en isomorfismes) Laat A en B Σ-algebra’s zijn voor een zekere signatuur (S, Σ). Een S-soortige afbeelding φ: A→B heet een homomorfisme van A naar B als geldt 1. φ(cA ) ≡ cB voor constanten uit Σ. 2. Als f een functiesymbool is van type (s1 , . . . , sn ) → s, dan geldt voor alle n-tupels a1 , . . . , an uit A dat φ(fA (a1 , . . . , an )) ≡ fB (φ(a1 ), . . . , φ(an )). Het kan verhelderend zijn om een homomorfisme van een algebra A naar een algebra B te zien als een afbeelding die mogelijk bepaalde gegevens over de onderliggende structuur van A ‘vergeet’. Voorbeeld 7.2 Beschouw de signatuur met ´e´en constante 0 en ´e´en ´e´enplaatsig functiesymbool succ). Laten A en B de algebra’s A = (A, 0A , succA ) resp. B = (B, 0B , succB ) zijn met A = {0, 1, 2, . . .} B = {e, o} 0A ≡ 0 0B ≡ e succA (n) ≡ n + 1 succB (e) ≡ o succB (o) ≡ e Het zal duidelijk zijn dat de afbeelding φ : A → B gegeven door  e als n even is φ(n) ≡ o als n oneven is, een homomorfisme is (ga dit na). De functie φ vergeet dus als het ware hoe groot een getal is, de enige informatie die bewaard blijft is het volgende: 1. 0 is een even getal 2. de opvolger van een even getal is oneven, en andersom. Als er een surjectief homomorfisme4 bestaat van A naar B, dan heet B een homomorf beeld van A. Een bijectief homomorfisme5 noemen we een isomorfisme. Als er een isomorfisme bestaat van A naar B, dan noemen we A en B isomorfe algebra’s; notatie: A ∼ = B. 4

Een functie f : A → B is surjectief als ∀b ∈ B∃a ∈ A f (a) ≡ b. Een functie f : A → B is injectief als ∀a, a0 ∈ A f (a) ≡ f (a0 ) ⇒ a ≡ a0 . Een functie f : A → B is bijectief als f zowel surjectief als injectief is. 5

7 Homomorfismes en isomorfie/ 28 Isomorfe algebra’s zijn ‘eigenlijk gelijk’, dat wil zeggen: twee isomorfe algebra’s mogen dan verschillende dragers hebben, de onderliggende structuur van de algebra’s is dezelfde. We merken op dat twee algebra’s niet isomorf hoeven te zijn als de eerste een homomorf beeld is van de tweede, en andersom (in dat geval zijn beide homomorfismen geen bijecties). In Opgave 7.8 wordt hiervan een (tegen)voorbeeld gegeven. Voorbeeld 7.3 Als voorbeeld bekijken we de algebra’s P(Q) en B2 voor de signatuur Booleans uit Voorbeeld 4.3. Laat a een element zijn van Q. Definieer de volgende functie φ : P(Q) → B2 :  T als a ∈ X φ(X) ≡ F als a 6∈ X We beweren dat φ een homomorfisme is van P(Q) naar B2 . We beschouwen eerst de constante true. Omdat trueP(Q) ≡ Q, geldt a ∈ trueP(Q) . De functie φ beeldt trueP(Q) dus af op T , en omdat T ≡ trueB2 , geldt dus inderdaad φ(trueP(Q) ) ≡ trueB2 . Van de functiesymbolen behandelen we alleen and. Stel dat X en Y deelverzamelingen zijn van Q; we onderscheiden vier gevallen, al naar gelang a al dan niet een element van X of Y is. We behandelen alleen het geval waarin a ∈ X, a 6∈ Y : φ(andP(Q) (X, Y )) ≡ ≡ ≡ ≡ ≡

φ(X ∩ Y ) F T ∧F andB2 (T, F ) andB2 (φ(X), φ(Y )).

Stel nu dat Q de singleton {a} is. Dan geldt P(Q) = {Q, ∅}, φ(Q) ≡ T φ(∅) ≡ F, zodat φ een bijectie is. De algebra’s P({a}) en B2 zijn dus isomorf. Uit de volgende stelling kunnen we afleiden dat de beperking tot initi¨ele modellen en de notie van initieel correcte specificatie juiste keuzes zijn geweest, aangezien er temidden van alle modellen voor een specificatie, hooguit ´e´en initieel model bestaat (op isomorfie na). Stelling 7.4 (isomorfie) Alle initi¨ele modellen voor een specificatie ((S, Σ), E) zijn isomorf. Bewijs. Laten A en B initi¨ele modellen zijn voor ((S, Σ), E). Beschouw een willekeurig element a in A. Aangezien A geen junk bevat, is er een t ∈ Ter Σ z´o dat a ≡ eval A (t). Stel nu dat er nog een gesloten term bestaat, bijv. u, waarvan a de interpretatie is. Omdat A geen confusion bevat, geldt dan dat t = u afleidbaar is uit E. Met behulp van de Correctheidsstelling 5.8 volgt dan dat t en u niet alleen in A, maar ook in B door ´e´en en hetzelfde element worden ge¨ınterpreteerd.

7 Homomorfismes en isomorfie/ 29 Het bovenstaande toont aan dat de volgende afbeelding φ gegeven door φ(eval A (t)) ≡ eval B (t), een correct gedefinieerde functie: A → B is. We zullen nu laten zien dat φ een isomorfisme is. Daartoe moeten we aantonen dat φ (1) injectief, (2) surjectief en (3) een homomorfisme is. We laten de onderdelen (1) en (2) over aan de lezer (opgave) en bewijzen hier alleen (3). Voor de interpretatie van de constanten is het bewijs zeer eenvoudig: φ(cA ) ≡ φ(eval A (c)) ≡ eval B (c) ≡ cB . Laat nu f een functiesymbool zijn van type (s1 , . . . , sn ) → s, en a1 , . . . , an elementen van A van de juiste soort. Omdat A geen junk bevat, zijn er gesloten termen t1 , . . . , tn z´odat eval A (ti ) ≡ ai , voor alle i. Nu rekenen: φ(fA (a1 , . . . , an )) ≡ ≡ ≡ ≡ ≡

φ(fA (eval A (t1 ), . . . , eval A (tn ))) φ(eval A (f (t1 , . . . , tn )) eval B (f (t1 , . . . , tn )) fB (eval B (t1 ), . . . , eval B (tn )) fB (φ(a1 ), . . . , φ(an )) 

Opgave 7.1 (a) Laat zien dat de inclusie-functie (φ(x) ≡ x) van N naar Z uit Voorbeeld 4.2 een homomorfisme is. (b) Bestaan er meer homomorfismes van N naar Z? (c) Laat zien dat er geen homomorfismes bestaan van Z naar N.

Opgave 7.2 Is de algebra B uit Opgave 5.2 een homomorf beeld van de structuur van de natuurlijke getallen?

Opgave 7.3 We werken in de signatuur (S, Σ) met ´e´en soort: nat; en alleen de constante 0 en het binaire functiesymbool add. N + is de Σ-algebra met als domein de natuurlijke getallen en de voor de hand liggende interpretaties: 0 als het getal 0 en add als de gewone optelling. Welke van de volgende twee afbeeldingen zijn homomorfismes? (a) φ gegeven door φ(n) ≡ n + 3. (b) φ gegeven door φ(n) ≡ 2n.

Opgave 7.4 Onderzoek tussen welke algebra’s uit Opgave 6.3 er homomorfismes bestaan.

Opgave 7.5 In Voorbeeld 7.3 is een begin gegeven van een bewijs dat de algebra B2 een homomorf beeld is van een willekeurige algebra P(Q). Maak dit bewijs af.

7 Homomorfismes en isomorfie/ 30 Opgave 7.6 We defini¨eren twee algebra’s voor de signatuur van stacks uit Voorbeeld 2.5. Om te beginnen beschouwen we de verzameling Ad = {a1 , . . . , an , ⊥}; Ad ∗ is de verzameling van strings over Ad . Daarbij introduceren we de volgende functies: conc tail

: Ad × Ad ∗ → Ad ∗ : Ad ∗ → Ad ∗

head : Ad ∗

→ Ad

conc(a, ai1 . . . aim ) tail() tail(ai1 . . . aim ) head() head(ai1 . . . aim )

≡ ≡ ≡ ≡ ≡

aai1 . . . aim  ai2 . . . aim ⊥ ai1

(m > 0) (m > 0)

We maken hier als volgt een algebra A van: Adata Astack diA errorA pushA popA topA

= = ≡ ≡ ≡ ≡ ≡

Ad Ad ∗ ai ⊥ conc tail head

De tweede algebra B wordt als volgt gedefinieerd: Bdata Bstack diB errorB pushB (, n) popB (n) topB (n)

= = ≡ ≡ ≡ ≡ ≡

{} {0, 1, 2, . . .}   n+1 max(n − 1, 0) 

Laat zien dat er een homomorfisme bestaat van A naar B.

Opgave 7.7 (a) Laat zien dat de compositie van twee homomorfismes weer een homomorfisme is. (b) Laat zien dat de converse van een isomorfisme weer een isomorfisme is. (c) Laat zien dat de relatie ∼ = (er bestaat een isomorfisme) tussen algebra’s een equivalentierelatie is.

Opgave 7.8 Gegeven is een ´e´ensoortige signatuur (S, Σ) waarvan Σ alleen ´e´en ´e´enplaatsig functiesymbool f bevat. (a) Beschouw de volgende algebra’s C, D en gegeven door C = D = E =

E, met als dragers respectievelijk C, D en E {an | n ∈ N } {de , do } {a}.

fC , fD en fE worden gegeven door de volgende plaatjes, waaruit u dient af te lezen dat f (x) ≡ y als er een pijl loopt van x naar y:

7 Homomorfismes en isomorfie/ 31 ' q

C

$ -q a1

a0

-q a2

-q a3

-q

-q

a4

-

a5

...

&

%

' de q 

D

'

$ - qd o

&

q a 

E %

$

&

%

Laat zien dat D een homomorf beeld is van C, en dat E een homomorf beeld is van D. (b) Gegeven zijn nu de volgende algebra’s A en B. De dragers A en B worden gegeven door A B

= {amn | m, n ∈ N } ∪ {bn | n ∈ N } = {cmn | m, n ∈ N } ∪ {en | n ∈ N } ∪ {de , do },

en fA en fB kunnen worden afgelezen uit de volgende plaatjes: A

'

B

$'

.. .

$

.. .

q a20

-q

q a10

-q

q a00

-q

a21 a11 a01

-q -q -q

a22 a12 a02

...

q c20

-q

...

q c10

-q

...

q c00

-q

q b0  q b1  q b2 

de q 

c21 c11 c01

-q -q -q

c22 c12 c02

... ... ...

- qdo

q e0  q e1  q e2 

.. .

.. . &

%&

(i) Laat zien dat B een homomorf beeld is van A. (ii) Laat zien dat A een homomorf beeld is van B. (iii) Laat zien dat A en B niet isomorf zijn.

%

7 Homomorfismes en isomorfie/ 32 Opgave 7.9 Laat A en B twee Σ-algebra’s zijn, en neem aan dat φ een een surjectief homomorfisme is van A naar B. (a) Stel dat θ een assignment is van elementen van B aan variabelen uit een verzameling X. Laat zien dat er een functie η : X → A bestaat z´o dat voor alle variabelen x geldt θ(x) ≡ φ(η(x)). Bewijs vervolgens dat voor elke term t geldt: ¯ ≡ φ(¯ θ(t) η (t)). (b) Laat met behulp van onderdeel (a) zien dat voor elke vergelijking t = u geldt: A |= t = u ⇒ B |= t = u. (c) Laat zien dat geldt, als A en B isomorfe algebra’s zijn: A |= t = u ⇔ B |= t = u. Merk op dat dit laatste feit inderdaad overeenstemt met het idee, dat twee isomorfe algebra’s ‘eigenlijk gelijk’ zijn.

8 Termmodellen/ 33

8

Termmodellen

In de vorige paragraaf hebben we gezien hoe de voorwaarden ‘no junk’ en ‘no confusion’ in principe een geschikt criterium opleverden voor een keuze binnen de klasse van alle modellen van een specificatie. Immers, de Isomorfiestelling 7.4 drukt uit dat alle initi¨ele modellen van een specificatie (op isomorfie na) identiek zijn. De vraag is nu nog, of er voor iedere specificatie eigenlijk wel een initieel model bestaat. Een heel bijzonder, en ook heel belangrijk voorbeeld van een Σ-algebra is het termmodel van de signatuur. Deze algebra zal blijken een initieel model te zijn. We behandelen eerst een voorbeeld van een termmodel, en geven dan de algemene definitie. Voorbeeld 8.1 We defini¨eren de volgende relatie ∼ op de verzameling gesloten termen van de specificatie Toy uit Voorbeeld 6.4: s ∼ t ⇐⇒ E ` s = t. Bijvoorbeeld, d ∼ nxt(nxt(c)). In Opgave 3.4 is aangetoond dat ∼ een equivalentierelatie is. Als we nu termen in equivalentieklassen groeperen, krijgen we het volgende plaatje: '

$

'

$ '

$ '

$

c

nxt(c)

d

nxt(d)

nxt(nxt(d))

nxt(nxt(nxt(c)))

nxt(nxt(nxt(nxt(c)))) .. .

nxt(nxt(c)) .. .

nxt(nxt(nxt(nxt(d)))) .. . &

% &

% &

%

&

%

We kunnen nu een model van de specificatie Toy defini¨eren dat we het termmodel zullen noemen en dat we om redenen die aanstonds duidelijk zijn noteren als TerΣ /∼. Het basisidee achter de constructie is dat we als drager de verzameling equivalentieklassen van termen onder de relatie ∼ kunnen nemen. De constanten c en d worden ge¨ınterpreteerd als de equivalentieklassen [c] en [d] van de termen c respectievelijk d. Om het functiesymbool nxt te interpreteren, maken we eerst de volgende observatie: voor alle termen s, t geldt: als s ∼ t, dan nxt(s) ∼ nxt(t).

(4)

Het bewijs van deze bewering is heel eenvoudig: als s ∼ t, dan is de vergelijking s = t afleidbaar; volgens de afleidingsregel (congruentie) is dan ook de vergelijking nxt(s) = nxt(t) afleidbaar, en dat betekent weer dat nxt(s) ∼ nxt(t). Het belang van observatie (4) is dat het de correctheid van de volgende definitie impliceert: nxtTerΣ /∼ ([t]) ≡ [nxt(t)].

8 Termmodellen/ 34 Met andere woorden, we hebben nxtTerΣ /∼ ([c]) ≡ [nxt(c)] nxtTerΣ /∼ ([nxt(c)]) ≡ [d] nxtTerΣ /∼ ([d]) ≡ [c]. Het termmodel van de specificatie Toy is nu de algebra TerΣ /∼ = hTer Σ /∼, Ii, waarbij Ter Σ /∼ I(c) I(d) I(nxt)

= ≡ ≡ ≡

{[c], [nxt(c)], [d]} [c] [d] nxtTerΣ /∼

We laten nu zien dat de vergelijkingen van Toy waar zijn in deze algebra; we behandelen alleen [T2]. Stel dat θ een bedeling is van de variabele x aan een element van Ter Σ /∼. Er zijn drie mogelijkheden, waarvan we alleen het geval θ(x) ≡ [nxt(c)] beschouwen. ¯ Het zal duidelijk zijn dat θ(nxt(nxt(nxt(x)))) ≡ [nxt(nxt(nxt(nxt(c))))]. Omdat de vergelijking nxt(c) = nxt(nxt(nxt(nxt(c)))) aleidbaar is in de specificatie Toy, geldt ¯ ¯ [nxt(c)] ≡ [nxt(nxt(nxt(nxt(c))))] en dus θ(x) ≡ θ(nxt(nxt(nxt(x)))). Aangezien de andere bedelingen van de variabele x ook identieke interpretaties opleveren voor de termen x en nxt(nxt(nxt(x))), is de vergelijking [T2] dus waar in TerΣ . Tenslotte moeten we nog aantonen dat TerΣ /∼ een initieel model is voor Toy. Om te beginnen is elk element van Ter Σ /∼ de interpretatie van een gesloten term: [c] ≡ eval TerΣ /∼ (c) [nxt(c)] ≡ eval TerΣ /∼ (nxt(c)) [d] ≡ eval TerΣ /∼ (d), zodat TerΣ /∼ geen junk bevat. Meer in het algemeen kunnen we bewijzen dat voor alle gesloten termen t geldt: eval TerΣ /∼ (t) ≡ [t]. (5) Uit (5) volgt nu dat voor termen s en t met eval TerΣ /∼ (s) ≡ eval TerΣ /∼ (t) moet gelden dat [s] ≡ [t], oftewel s ∼ t. Per definitie van ∼ volgt dan dat de vergelijking s = t afleidbaar is. Maar dit betekent dat TerΣ /∼ geen confusion kan bevatten. In bovenstaand Voorbeeld 6.4 hebben we voor de specificatie Toy een initieel model geconstrueerd. We zullen nu zien dat deze constructie werkt voor elke specificatie. Laat ((S, Σ), E) een specificatie zijn, en beschouw de verzameling gesloten termen Ter Σ . In Opgave 3.4 is aangetoond dat de relatie ∼ gedefinieerd door t ∼ u als E ` t = u een equivalentierelatie is op Ter Σ . Voor een gesloten term t defini¨eren we [t] als de equivalentieklasse van t onder ∼, oftewel [t] is {u ∈ Ter Σ | E ` t = u}.

8 Termmodellen/ 35 De verzameling equivalentieklassen noteren we als Ter Σ /∼. Deze verzameling zal de drager worden van de Σ-algebra TerΣ /∼. (Als S meersoortig is, zal de soort van [t] natuurlijk die van t zijn.) Voor een constante c defini¨eren we cTerΣ /∼ ≡ [c].

(6)

Nu moeten we alleen nog aangeven wat de interpretatie van de functiesymbolen wordt. Laat f een functiesymbool zijn van type (s1 , . . . , sn ) → s. Neem aan dat t1 , . . . , tn en u1 , . . . , un gesloten termen zijn (van het juiste type) z´o dat ti ∼ ui voor alle i. Per definitie van ∼ geldt dan dat E ` ti = ui voor alle i. Maar dan volgt met behulp van de afleidingsregel (congruentie) dat E ` f (t1 , . . . , tn ) = f (u1 , . . . , un ). We hebben dus bewezen dat ti ∼ ui (voor alle i) ⇒ f (t1 , . . . , tn ) ∼ f (u1 , . . . , un ).

(7)

Maar dit betekent dat we nu ook een mooie interpretatie kunnen vinden voor het functiesymbool f : uit (7) volgt dat de onderstaande definitie op een correcte wijze een afbeelding definieert: fTerΣ /∼ ([t1 ], . . . , [tn ]) ≡ [f (t1 , . . . , tn )]. (8) Definitie 8.2 Laat ((S, Σ), E) een specificatie zijn; het termmodel TerΣ /∼ van ((S, Σ), E) is de algebra die als drager de verzameling Ter Σ /∼ heeft, en waarbij de interpretaties voor de constanten en functiesymbolen worden gedefinieerd als in (6) resp. (8). Het belangrijke resultaat over deze algebra’s is dat ze altijd initi¨ele modellen van hun specificaties zijn: Stelling 8.3 Laat ((S, Σ), E) een specificatie zijn; dan is het termmodel TerΣ /∼ een initieel model van ((S, Σ), E). Uit Stelling 8.3 volgt dus dat inderdaad elke specificatie een initieel model heeft: het voorbeeld in 6.4 van het termmodel voor de specificatie Toy was dus geen uitzondering. Merk verder op dat uit Stelling 8.3, de Isomorfiestelling 7.4 en Voorbeeld 6.2 volgt, dat het termmodel van de specificatie Naturals isomorf is met het model van de natuurlijke getallen (zie ook Opgave 8.2). Opgave 8.1 (a) Construeer het termmodel als een initieel model voor de specificatie Booleans (naar analogie van Voorbeeld 6.4). (b) Laat zien dat dit model isomorf is met het model B2 .

Opgave 8.2 (a) Construeer het termmodel als een initieel model voor de specificatie Naturals. (b) Laat zien dat dit model isomorf is met het model N.

Opgave 8.3 Gegeven een signatuur met soort S en functiesymbolen a :→ S, b :→ S en f : S → S. De bijbehorende equationele specificatie bestaat uit ´e´en vergelijking: f(f(b)) = a Construeer het termmodel als een initieel model voor deze specificatie.

8 Termmodellen/ 36 Opgave 8.4 Beschouw de algebra¨ısche specificatie Abc = ((S, Σ), E) met: S: Σ:

soorten constanten

E:

functie vergelijkingen

I, V a: b: c: e: in: [1] [2]

→I →I →I →V I#V → V in(x, in(y, z)) in(x, in(x, y))

= =

in(y, in(x, z)) in(x, y)

Voor in(x, y) mag ook de infix-notatie x · y worden gebruikt. (a) Laat zien dat de volgende vergelijking afleidbaar is uit E: in(a, in(b, in(a, e))) = in(a, in(b, e)) (Een volledig geformaliseerde afleiding is niet nodig.) Nu worden de volgende drie Σ-algebra’s K, L, en M gedefinieerd: K:

IK = VK = {0, 1}

aK ≡ 0 bK ≡ 0 cK ≡ 1

eK ≡ 1

inK (x, y) ≡ x ∗ y

L:

IL = VL = {−1, 0, 1}

aL ≡ 0 bL ≡ 0 cL ≡ 1

eL ≡ 1

inL (x, y) ≡ x ∗ y

M:

IM = {1, 2, 3} VM = P({1, 2, 3})

aM ≡ 1 bM ≡ 2 cM ≡ 3

eM ≡ ∅

inM (x, y) ≡ {x} ∪ y

(Nota bene: ∗ staat voor vermenigvuldiging, P voor machtsverzameling.) (b) Onderzoek voor deze algebra’s of het modellen zijn van Abc. (c) Onderzoek of ´e´en (of meerdere) van deze modellen een initieel model is van Abc. Geef eventuele junk of confusion concreet aan. (d) Beschrijf een initieel model voor Abc door uit elke equivalentieklasse van het termmodel ´e´en representerend element te kiezen.