Generalisert algebraisk spesifikasjon med en anvendelse på indirekte semantikk

anvendelse på indirekte semantikk

Jo Erskine Hannay

[email protected]

29. september 1995

Abstrakte datatyper har lenge representert et paradigme innen program-design og program-verikasjon. Abstrakt representasjon og spesikasjon av program- mer tillater matematisk resonnering om vesentlige egenskaper ved programmer uten brysomme implementatoriske detaljer. Det har blitt sett at algebraiske me- toder kan tas ibruk for abstrakt representasjon og spesikasjon av programmer, ogalgebraisk spesikasjonvedligningertilbyr en abstrakt men konstruktiv måte å spesisere funksjoner på: Ligninger kan sees på som abstrakte programmer.

Denne hovedoppgaven er bygget rundt følgende to punkter: 1) Vi skal ge- neralisere algebraisk spesikasjon på en måte som åpner for en spesiell type modulær spesikasjon. 2) Vi skal innføre en spesikasjonsmåte som vi skal kalle indirekte spesikasjon, som en variant av algebraisk spesikasjon. Vi skal se at indirekte spesikasjon innfører eninhomogenspesikasjonssituasjon i forhold til vanlig algebraisk spesikasjon. Den modulære egenskapen ved vår generaliserte spesikasjonsmåte kan så brukes for å fange opp denne inhomogene spesika- sjonssituasjon.Konsistenser et gjennomgangstema i diskusjonen.

Innhold

1 Innledning 1

2 Abstrakte og formelle datatyper 9

2.1 Grunnleggende begreper : : : : : : : : : : : : : : : : : : : : : : : 9 2.2 Algebra : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 12 2.2.1 Formelt språk : : : : : : : : : : : : : : : : : : : : : : : : : 12 2.2.2 Tolking av formelt språk: : : : : : : : : : : : : : : : : : : 13 2.2.3 Homomorer og term-algebraer : : : : : : : : : : : : : : : 14 2.2.4 Full uttrykkbarhet : : : : : : : : : : : : : : : : : : : : : : 15 2.2.5 Formulering av matematiske påstander: : : : : : : : : : : 16 2.2.6 Omskrivningssystemer og ligningslogikk : : : : : : : : : : 17 2.2.7 Termunivers: : : : : : : : : : : : : : : : : : : : : : : : : : 19 2.2.8 Algebraisk spesikasjon : : : : : : : : : : : : : : : : : : : 19 2.2.9 Formell resonnering : : : : : : : : : : : : : : : : : : : : : 21 2.3 Semantikk : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 22 2.3.1 Implementasjon: : : : : : : : : : : : : : : : : : : : : : : : 22 2.3.2 Initialsemantikk : : : : : : : : : : : : : : : : : : : : : : : 24 2.3.3 Finalsemantikk : : : : : : : : : : : : : : : : : : : : : : : : 26 2.3.4 Alternativ denisjon av nalsemantikk : : : : : : : : : : : 30 2.3.5 Initialsemantikk generalisert: : : : : : : : : : : : : : : : : 31 2.3.6 Konsistens : : : : : : : : : : : : : : : : : : : : : : : : : : 32 2.3.7 Sammenheng mellom initial- og nalsemantikk : : : : : : 33 2.3.8 Inkonsistens og tolkninger : : : : : : : : : : : : : : : : : : 44 2.3.9 Inkonsistens sett som inkongruens : : : : : : : : : : : : : 44 2.3.10 Modulær oppbygging av semantikk : : : : : : : : : : : : : 46 2.4 Mot mekanisk resonnering : : : : : : : : : : : : : : : : : : : : : : 47 2.4.1 Induktive vs. logiske konsekvenser : : : : : : : : : : : : : 47 2.4.2 Konvergente omskrivningssystemer : : : : : : : : : : : : : 49 2.4.3 Resolusjonsmetoder for basis-semantikker : : : : : : : : : 50 2.4.4 Knuth&Bendix-komplettering : : : : : : : : : : : : : : : : 51 2.4.5 Induktiv komplettering : : : : : : : : : : : : : : : : : : : 56 2.4.6 Metoder som søker generell resolusjon : : : : : : : : : : : 57 2.4.7 Algoritmisk oppdagbarhet av inkonsistens : : : : : : : : : 58 2.5 Oppsummering : : : : : : : : : : : : : : : : : : : : : : : : : : : : 61 3 Semantikkgivende syntaktiske funksjoner 63 3.1 Syntaktiske funksjoner : : : : : : : : : : : : : : : : : : : : : : : : 63 3.2 Funksjonsspesikasjon over kanoniske representanter : : : : : : : 68 3.2.1 Mekanisk generering av kanoniske representanter : : : : : 69 3.2.2 Eksempler på funksjonsspesikasjon : : : : : : : : : : : : 71 3.2.3 Utledning og resolusjon : : : : : : : : : : : : : : : : : : : 73 3.3 Algebraiske spesikasjoner av syntaktiske funksjoner : : : : : : : 74

ii

3.4.2 Formell omgivelse... : : : : : : : : : : : : : : : : : : : : : 84 3.4.3 ...og formelle datatyper : : : : : : : : : : : : : : : : : : : 87 3.4.4 Reduksjon til basis-nalsemantikk : : : : : : : : : : : : : 88 3.4.5 Reduksjon til basis-initialsemantikk : : : : : : : : : : : : 90 3.5 Inkonsistens i tilknytning til indirekte algebraisk spesikasjon : : 107 3.6 Komplettering avid-utvidelser. : : : : : : : : : : : : : : : : : : : 111 3.6.1 id-utvidelser og mangel på kjernebevaring : : : : : : : : : 115 3.6.2 Synliggjøring av kjernebevaring : : : : : : : : : : : : : : : 120 3.6.3 Kjernebevaring avid-utvidelser og inkonsistens : : : : : : 121 3.6.4 Synliggjøring av kjernesemantikk : : : : : : : : : : : : : : 122 3.6.5 id-utvidelser og inkongruens: : : : : : : : : : : : : : : : : 123 3.6.6 Nytten av id-utvidelser som basis-initialsemantikk spesi-

katorer : : : : : : : : : : : : : : : : : : : : : : : : : : : : 124 3.7 Skjuling av hjelpefunksjoner : : : : : : : : : : : : : : : : : : : : : 125 3.7.1 Operasjonell skjuling : : : : : : : : : : : : : : : : : : : : : 126 3.7.2 Operasjonell skjuling i resolusjonsmetoder : : : : : : : : : 131 3.7.3 Skjuling på spesikasjonsnivå : : : : : : : : : : : : : : : : 133 3.7.4 Skjulingpåspesikasjonsnivåogreduksjontilbasis-initial-

semantikk : : : : : : : : : : : : : : : : : : : : : : : : : : : 135 3.7.5 Skjuling ved innføring av typer : : : : : : : : : : : : : : : 136 3.8 Alternativ tilid-utvidelser under konsistens : : : : : : : : : : : : 138 3.9 Verikasjon av indirekte algebraiske spesikasjoner : : : : : : : : 139 3.9.1 Program-analyse : : : : : : : : : : : : : : : : : : : : : : : 139 3.9.2 Verikasjon relativt til en direkte algebraisk spesikasjon 140 3.10 Andre temaer : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 141 3.10.1 Generaliserteid-utvidelser: : : : : : : : : : : : : : : : : : 141 3.10.2 id-utvidelser og nalsemantikk : : : : : : : : : : : : : : : 142 3.10.3 Fikspunkt-semantikk : : : : : : : : : : : : : : : : : : : : : 143 3.11 Oppsummering : : : : : : : : : : : : : : : : : : : : : : : : : : : : 144 4 Sekvens-utvidet Knuth&Bendix-komplettering 147 4.1 Denisjon av sekvens-utvidet Knuth&Bendix-komplettering : : : 147 4.1.1 Utledningssekvenser : : : : : : : : : : : : : : : : : : : : : 148 4.1.2 Utvidelsen: : : : : : : : : : : : : : : : : : : : : : : : : : : 151 4.1.3 Godtgjørelse for sekvens-utvidet Knuth&Bendix-kom-

plettering : : : : : : : : : : : : : : : : : : : : : : : : : : : 151 4.2 Anvendelser av sekvens-utvidet Knuth&Bendix-komplettering : : 154 4.2.1 id-utvidelser og kjernebevaring igjen : : : : : : : : : : : : 154 4.2.2 Skjuling av hjelpefunksjoner: : : : : : : : : : : : : : : : : 158 4.2.3 Basis-initialsemantikk og induktive konsekvenser : : : : : 161 4.2.4 Basis-initialsemantikk og konsistens : : : : : : : : : : : : 162

5 Konklusjon og videre arbeid 163

A Surjektivitet og grunnterm-algebraer 167 A.1 Mer om formelle datatyper og semantikk: : : : : : : : : : : : : : 167 A.1.1 Bevis av (2.2) side 17 : : : : : : : : : : : : : : : : : : : : 167 A.1.2 Semantikk, initialalgebra og nalalgebra : : : : : : : : : : 167 A.1.3 Elementær ekvivalens og isomor : : : : : : : : : : : : : : 169 A.1.4 Semantikk på termer med variable : : : : : : : : : : : : : 172 A.2 Induktive konsekvenser og surjektivitet: : : : : : : : : : : : : : : 173 A.3 Omskrivningssystemer og konvergens : : : : : : : : : : : : : : : : 175 A.3.1 Bevis for (2.16) side 49: : : : : : : : : : : : : : : : : : : : 175 A.3.2 Delvis konvergens vs. full konvergens : : : : : : : : : : : : 175

Figurer

1.1 Implementasjon via formelle datatyper : : : : : : : : : : : : : : : 2 1.2 Svak simulering og implementasjon av abstrakt datatype ved mo-

duldeklarasjon : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 2.1 Sammenhenger mellom initial- og nal-semantikk : : : : : : : : : 34 2.2 Del-bevisskisse for sats 2.7 : : : : : : : : : : : : : : : : : : : : : 36 2.3 Inkonsistens sett på to måter. Inversjon : : : : : : : : : : : : : : 37 2.4 Inferensregler i Knuth&Bendix-komplettering : : : : : : : : : : : 54 3.1 Syntaktiske funksjoner : : : : : : : : : : : : : : : : : : : : : : : : 67 3.2 ^<Uprogrammert^> og^<pre-programmert^>maskin : : : : : : : : : 70 3.3 Illustrasjon til eksempel 42 : : : : : : : : : : : : : : : : : : : : : 75 3.4 Möbius-bånd. Sammenbrudd av skillet mellom syntaks og seman-

tikk : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 77 3.5 Semantikkspesikasjon på to nivåer: : : : : : : : : : : : : : : : : 82 3.6 Semantikkspesikasjon på ett nivå og sammenslåtte funksjons-

spesikasjoner/beskrivelser : : : : : : : : : : : : : : : : : : : : : 83 3.7 Formell omgivelse for reduksjon til basis-semantikker : : : : : : : 85 4.1 Inferensregler i sekvens-utvidet Knuth&Bendix-komplettering : : 152 4.2 Figur til eksempel 87 : : : : : : : : : : : : : : : : : : : : : : : : : 159

Forord

Dette er en hovedfagsrapport for graden Cand. Scient. i informatikk, studie- retning databehandling ved Universitet i Oslo. Her er det på sin plass å rette en stor takk til min veileder Olav Lysne for tålmodig, samvittighetsfull og god veiledning. Takk også til Henrik Linnestad og Peter Ølveczky som har funnet tid til å kommentere denne rapporten.

Takk til Marit med sitt nesten uknekkelige humør og morsomme lyder som har holdt ut en frustrert og irritabel Jo, og som har vært 3550 m.o.h. og på mange fjelltopper. Takk til Kjetil og Rune; poeten Kjetil med hans underfundige mentale bilder og Rune med sin morsomme absurde fantasi og sitt forsøk på teselskap på Dyrehaugsryggen. Takk til Peter og hans dyktighet som guide i Egypt. Hadde det ikke vært for at Peter kk meg til å ta 200-kurs, hadde jeg sikkert aldri tatt sikte på informatikk hovedfag (jeg hadde bare pause fra Musikkhøgskolen). Men takk til de ovenstående først og fremst sommine venner og takk til alle de venner jeg ikke har nevnt. En takk til Skiforeningen og til skogene rundt Oslo som gir mulighet for rask oppladning og gjenoppbygging av fragmenterte hovedfagsstudentsjeler. Jeg vil også få lov til å uttrykke stor takknemlighet for Jotunheimen.

Hva er min presentasjon av kjent sto og hva er nye tanker? Jeg har ikke skrevet med tanke på å få dette skillet klart frem, fordi jeg nner det distrahe- rende (og faglig uinteressant) å måtte tenke på å fremheve eget åndsverk. Men grovt sett kan man regne at alt fra og med avsnitt 2.3.3 side 26 er (til mitt kjennskap) nytt sto. Ting som etter dette ikke er nytt sto er da eksplisitt fremstilt som presentasjon av kjent sto. I det stoet som erfør avsnitt 2.3.3 presenteres stort sett kjente begreper, men jeg nevner at presentasjonen til ti- der, på både godt og vondt, er sterkt preget av min følelse for stoet og den vinkling jeg synes er hensiktsmessig for diskusjonen. Det nnes her også mindre resonnementer og observasjoner som er egne, men som muligens ikke står frem som sådane.

Tilleggskapitlene er egenhendig utført. Noen av resultatene er her kjent sto, selv om måten jeg har vist disse på muligens er ny. Andre resultater ersann- synligvis kjent sto, men for å spare tid har jeg vist slike resultater selv.

Jeg har i referanselisten tatt med referanser til to arbeidsnotater som jeg har skrevet til veileder underveis. De er tatt med fordi de inneholder ting jeg har tenkt på i forbindelse med stoet i denne rapporten, og fordi en av dem omhandler noen tanker som tar for seg et morsomt sidetema til diskusjonen.

På side 177 nnes en symboltabell, i tilfelle symbolbruken blir for voldsom.

Det er ingen dårlig idé å rive den ut. Bakerst nnes også et stikkordsregister.

God lesing!

Oslo, mai 1995 Jo Erskine Hannay

Innledning

Vi er, selvsagt, interessert i at de datamaskinprogrammer vi skriver er ^<rik- tige^>. Desverre kan det være svært vanskelig å gå god for at et program av vesentlig størrelse eller kompleksitet er korrekt; i den forstand at det eksekverte programmet alltid gir det output man tilsiktet for ethvert input.

Her er det to viktige sider. For det første kan det meget godt tenkes at man ikke har en presis forestilling om hva man ønsker at et program skal gjøre. For det andre overlates ofte verikasjon av programmer mht. eventuelle slike presise forestillinger til synsing; eller utelates helt og overlates til testing og debugging (som gjerne varer ut et programs levetid).

Slik^<intuitiv^>programmering er ofte tilstrekkelig. I kritiske situasjoner kan derimot et programs uforutsette oppførsel være katastrofal.¹ Metoder for presis spesisering av hva et program gjør eller skal gjøre, samt metoder for på en strukturert måte å resonnere om hvorvidt programmer er korrekte mht. slike spesikasjoner, er derfor svært viktige. Dette sier ikke at metoder som garante- rer^<riktigheten^>av programmer nnes eller engang er mulige. Ved forskjellige metoder kan imidlertidvisse egenskaper ved programmer spesiseres og vises å holde. Presis spesikasjon er også essensiell for modularisering av programmer og for gjenbruk av moduler; trekk som begge kan lette oversikten i programme- ringen og således også bidra til^<riktige^>programmer.

Matematisk terminologi kan være svært presis, og ere spesikasjons- og ve- rikasjonsstrategier bruker matematiske vendinger for å beskrive presist hva et program gjør eller skal gjøre. Felles for mange slike strategier, er å avbilde prog- ramtekst (syntaks) til en form for meningsfull (semantisk) matematisk størrelse som på en eller annen måte sier noe om hva programmet gjør. Å beskrive et program veddenotasjonell semantikk (se f.eks. [Mos90]) går eksempelvis ut på å avbilde programmer til matematiske funksjoner. Beskrivelse vedaksiomatisk semantikk (ved f.eks. såkalt^<Hoare-analyse^> [Hoa69]) avbilder predikatlogiske utsagn og programtekst til matematiske påstander om programmet. Vår disku- sjon utover er først og fremst tilknyttet aksiomatisk semantikk.

Sentralt for oss er begrepet datatype. Programmering innbefatter generelt datastrukturer som variable, lister, trær, grafer, databaser osv. og operasjoner på disse som sortering av lister eller trær, pruning av grafer m.m. For resonner- ingsformål er det hensiktsmessig å betrakte datastrukturer og deres tilhørende operasjoner på et abstrakt nivå, uten tanke på implementasjonsdetaljer. Dette kan gjøres ved å innse at en programmerer sannsynligvis forestiller seg at data- strukturer lagrer matematiske verdier; i en vid forstand. Vi kan da betrakte en

1`Uforutsett oppførsel' har her ingenting med maskiner som <sup><</sup>tenker på egenhånd<sup>></sup>, ei heller med ikke-determinisme å gjøre. `Uforutsett oppførsel' er snarere en detalj i programmet programmereren ikke visste han programmerte.

mengde matematiske verdier tenkt lagret i datastrukturen og en mengde mate- matiske funksjoner svarende til operasjonene på strukturen. En samling av en slik matematisk verdimengde, tilhørende funksjonsmengde samt denisjoner av funksjonene, utgjør grovt sett hva vi kaller enabstrakt datatype.

En abstrakt datatype er da en ^<utkrystallisering^> av et lettfattelig mate- matisk objekt som formodentlig søkes implementert i et program. Den virkelige fortreelighet av abstrakte datatyper vises likevel først når et programmerings- språk har mekanismer som tilbyr en måte å^<implementere^> abstrakte dataty- per. Eksempelvis tillater modul-konstruksjonene i f.eks. SIMULA [DMN70] og Smalltalk [GR83] (modulkonstruksjonene kalles i disse språkene `klasser'), blant mye annet, at datastrukturer og tilhørende operasjoner kan deklareres og brukes som en enhet i programteksten. Abstrakte datatyper sammen med slike meka- nismer oppfordrer da til enmodulær tankegang ved utvikling av programmer.

Et ideelt scenario for datatype-tankegangen, ville være om enhver program- meringsoppgave kunne resonneres om og uttrykkes utelukkende ved hjelp av abstrakte datatyper. Dette ville gi presis matematisk spesikasjon på et nivå hvor forstyrrende implementasjonsdetaljer er abstrahert vekk. Siden implemen- teres de abstrakte datatyper i et (imperativt) programmeringsspråk ved f.eks.

modulkonstruksjoner. Programmeringsoppgaven er da korrekt løst i den grad implementasjonene av de abstrakte datatyper er korrekt. I hvilken grad og hvor- dan det er mulig å ^<høy^>-programmere utelukkende ved abstrakte datatyper skal ikke være vårt tema. Vår diskusjon hører til under problemstillingen korrekt implementasjon av abstrakte datatyper.

Anta vi vil vise at en moduldeklarasjon i et (imperativt) programmerings- språk er en `korrekt implementasjon' av en gitt abstrakt datatype. Dette burde kunne gjøres ved strategien å avbilde programtekst på semantiske matematiske objekter; dvs. her fortrinnsvis å avbilde moduldeklarasjoner på abstrakte data- typer. Vi skal gjøre dette, men avbildningen skal gå via noe vi skal kalleformelle datatyper. Formelle datatyper fungerer i to roller: Som syntaktiske formelle ut- trykk for abstrakte datatyper men også som abstrakte uttrykk for (imperative) moduldeklararsjoner. Formelle datatyper utgjør således et (toveis) grensesnitt mellom moduldeklarasjoner og abstrakte datatyper. Formelle datatyper er syn- taktiske objekter, så detsemantiske spranget fra syntaks til semantikk benner seg her mellom formelle og abstrakte datatyper. Dette spranget er trivielt sam- menlignet med et direkte semantisk sprang fra moduldeklarasjon til abstrakt datatype. Se ellers gur 1.1.

Moduldeklarasjon

SYN TAKS SEMAN TIKK

Abstrakt datatype

IM PL EM EN TA S JO N

Formell datatype

Figur 1.1:Implementasjon av abstrakt datatype ved moduldeklarasjon. Implementa- sjonen går via en formell datatype.

formelle datatyper. Termene er bl.a. ment å være symbolske representasjoner av elementer i verdimengden til en abstrakt datatype. Ligningene sammen med ligningslogikk gir en formell beskrivelse av funksjonene i en abstrakt dataty- pe. Implementasjonsdetaljer er, som i abstrakte datatyper, abstrahert vekk i formelle datatyper.

Det er stor interesse for å mekanisere deler av programverikasjon. Ved siden avå fungere somgrensesnittmellommoduldeklarasjoner ogabstrakte datatyper, benner i den forbindelse formelle datatyper seg på et abstraksjonsnivå som egner seg forformell resonnering.

Ved matematisk resonnering kan man tidvis ta seg i å bedrive^<bevisstløs^>

symbolmanipulasjon etter mer eller mindre implisitte regler.^<Bevisstløs^>i den forstand at både betydningen til de matematiske symboler som manipuleres og opphavet til reglene de manipuleres etter, er glemt. Formell resonnering er rendyrket symbolmanipulasjon utfra eksplisitt gitte regler for hvordan symbo- lene kan manipuleres. Formelle systemer som predikatkalkyler, ligningslogikk, -kalkyle m.m. er beskrivelser av forskjellige typer formell resonnering.

Symboler er i formell resonnering ment å representere matematiske objekter, og for å få noe nytte ut av formell resonnering må resultater av symbolmani- pulasjonen (f.eks. et bevistre med aksiomer som blader eller en omskrivning i -kalkyle) også tolkes. Men gitt regler og symboler kan selve symbolmanipula- sjonen eller^<resonneringen^>skje uten annen viten om de matematiske objekter symbolene representerer, enn den viten som er nedfelt i reglene. Det er ikke vanskelig å forestille seg mekaniserbare aspekter ved formell resonnering.

Abstrakte maskiner som endelige automater, Pushdown-automater og i yt- terste instans Turing maskiner, er matematiske beskrivelser av hva man fore- stiller seg at `mekaniske prosesser' er. Abstrakte maskiner egner seg for å bli resonnert matematisk om, og gir da en mulighet for å resonnere matematisk om mekaniske prosesser. (Abstrakte maskiner er på den annen side ofte lite egnet for programmering i praksis.) Også abstrakte maskiner er symbolmanipulator- er, og symboler sett som^<maskindeler^> er helt strippet for mening: Maskiner kan kun skjelne syntaks eller^<form^>og ikke semantikk eller^<mening^>. Mange formelle systemer kan naturlig betraktes og beskrives som abstrakte maskiner, noe vi kommer til å gjøre i diskusjonen fremover, siden vi skal være interessert i åresonnere matematisk om mekaniserbare aspekter ved formell resonnering.² I forbindelse med formelle datatyper, kreves symbolsk representasjon av ele- menter i muligens uendelige verdimengder. Vi kunne ha et symbol for hvert element i aktuell verdimengde, men vi skal insistere på å ha abstrakte maskiner med endelig mange ^<deler^>. Verdimengder skal derfor betraktes som generert av endelig mangegeneratorfunksjoner. F.eks. kan de naturlige tall genereres av konstanten 0 og etterfølgerfunksjonensucc. Dersom symbolene0ogsuccrepre- senterer 0 ogsucc hhv., kan ethvert naturlig tall representeres av en term på formensucc(succ( (0) )). Vi betrakter således kun abstrakte datatyper med

2At en oppgave kan mekaniseres betyr i praktisk forstand at et datamaskinprogram kan skrives for å utføre oppgaven. Tilsynelatende er vi tilbake i programmeringsverdenen igjen, snarere enn i den matematiske. I siste instans er det jo ønskelig å implementere et formelt system på en datamaskin. Men vårt fokus her på formelle systemer og abstrakte maskiner er primært å demonstrere at en gitt resonneringsprosess er mekaniserbar. Derfor holder vi oss (eller benner oss fortsatt) på det matematiske nivå med abstrakte matematiske beskrivelser i form av formelle systemer og abstrakte maskiner.

rekursivt tellbare (mekanisk beregnbare) verdimengder. Vi skal også kun be- trakte abstrakte datatyper med endelige funksjonsmengder. Termuniverset mengden av alle representasjoner av funksjonsapplikasjonersikres da også å være rekursivt tellbart. Mengden avgeneratortermer i en formell datatype ut- gjør generatoruniverset som representerer verdimengden i en gitt abstrakt da- tatype. I eksemplet med de naturlige tall er generatoruniverset i et en-til-en forhold med den korresponderende verdimengden. Dette er ikke alltid tilfellet.

En naturlig måte å generere f.eks. de hele tall på, er med generatorfunksjonene 0, succ og forgjengerfunksjonenpred. Da vil f.eks. termene succ(pred(0))og 0 representere samme element i verdimengden.

Den type formelle resonnering vi skal befatte oss med er avleding av ligning- er fra gitte initialligninger eller aksiomer. Det grunnleggende formelle systemet skal være det som er forbundet med formelle datatyper; nemlig ligningslogikk.

Ligningslogikk kan gis en spesielt enkel og intuitiv beskrivelse som direkte for- maliserer den velkjente matematiske resonneringen vi gjør når vi resonnerer utfra ligninger. Eksempelvis kan vi fra Peano-aksiomene

x+0 = x og x+succ(y) = succ(x+y) for addisjon i de naturlige tall, avlede ligningen

succ(0)+succ(succ(0)) = succ(succ(0))+succ(0)

ved å starte på hhv. venstre og høyre side i ligningen og erstatte ^<like for like^>

til vi får syntaktisk like termer på følgende måte:

succ(0)+succ(succ(0)) succ(succ(0))+succ(0)

;succ(succ(0)+succ(0))

;succ(succ(succ(0)+0)) succ(succ(succ(0)+0)) ^;

En formell spesikasjon av en funksjon kan utrykke en egenskap ved funksjo- nen; f.eks. kommutativitetx+y=y+x. Vårt mål er imidlertid implementasjon av abstrakte datatyper, så vi skal være interessert i å nnekonstruktive spesi- kasjoner av funksjoner som forteller hvordan verdien av en funksjonsapplikasjon evalueres. Aksiomene over for addisjon i naturlige tall er konstruktive i så måte.

F.eks. kan man^<regne ut^>2+ 1 ved å avlede:

succ(succ(0))+succ(0)^;succ(succ(succ(0)+0))^; succ(succ(succ(0))) I tillegg til å implementere funksjoner i en abstrakt datatype, er det svært relevant å implementere likhets-/identitetsrelasjonen for datatypen. (Dette er relevant for betingede kontrollstrukturer i programmeringsspråket, men også for formellresonnering.) I den forbindelse kandet gis ligningersomgir likhet mellom generatortermer i tilfellet mange-til-en generatorunivers. For generatoruniverset for de hele tall som over kan vi eksempelvis gi ligningene

succ(pred(x)) = x og pred(succ(x)) = x for å utrykke hvilke generatortermer som skal forstås som like.

Formelle datatyper har altså et formelt språk og et formelt system knyttet til seg. Dette språket kan sies å være et abstrakt programmeringsspråk i hvil- ket abstrakte programmer kan skrives. Slik kan formelle datatyper abstrahere moduldeklarasjoner skrevet i et mer konkret programmeringsspråk.

Alle somhar drevet med formelle systemer eller matematisk bevisføring over- hodet vet at det ofte er forbundet strategiske vanskeligheter med hvordan man skal gå frem underveis. Ligningslogikk har dette iboende i og med at det ofte

er imidlertid slik at de kan orienteres og alltid brukes én vei og likevel beholde den samme bevisstyrken. Videre kan de ha egenskapen at enhver utledning er endelig og forskjellige valg av anvendte ligninger alltid fører til samme resultat.

Slike ligninger utgjør det vi kaller etkonvergent omskrivningssystemog er essen- sielle for mekaniserbarheten av ligningslogikk; og derved for mekaniserbarheten av vår formelle resonnering i formelle datatyper. Ligningenesucc(pred(x)) = x ogpred(succ(x)) = xorientert mot høyre utgjør et konvergent omskrivningssys- tem. I lys av atikke-determinismeer latent i ligningslogikk, utgjør konvergente omskrivningssystemer endeterministisk del av ligningslogikk; i den forstand at konvergente omskrivningssystemer sett på som abstrakte deterministiske prog- rammer gir samme output for et gitt input.

Formelle datatyper representerer et ^<minste steg^> fra abstrakte datatyper inn i den syntaktiske formelle verden. Ved programutvikling tilbyr således for- melle datatyper en meget presis uttrykksform for matematiske idéer som søkes implementert, uten forstyrrende og på dette nivå uvesentlige detaljer. Det nnes programmeringsspråk som søker å forene slik høynivå spesikasjon ved formelle datatyper og mer implementatoriske mekanismer. Eksempler på slike formelle spesikasjons- og programmeringsspråk er ABEL [DO91] og OBJ [GW88]. Merk også atapplikative programmeringsspråk kan sies å ligge nær opp til abstrak- sjonsnivået til formelle datatyper.

Verikasjonen av at en moduldeklarasjon implementerer en abstrakt dataty- pe består nå av to hoveddeler. For det første må et samsvar mellom den (impe- rative) moduldeklarasjonen og den korresponderende formelle datatypen vises.

Dette er beskrevet utfyllende i [Dah92]. (En modul kan vises åimperativt simu- lere en formell datatype. Dette gjøres ved å identisere en såkalttypeekvivalent til modulen, som så vises åsimulere den formelle datatypen. Sentralt er å nne eektfunksjonersom beskriver (funksjons-)prosedyrers eekt på datastrukturen i modulen. `Hoare-logikk' [Hoa69] kan brukes til å vise korrespondanse mellom eektfunksjon og (funksjons-)prosedyre.) Dette samsvaret kallessvak simuler- ing og tar bl.a. i betraktning motsetningen mellom fysiske begrensninger på en fysisk datamaskin og den abstraherte og idealiserte situasjon forbundet med teoretiske abstrakte maskiner.

Gitt at en moduldeklarasjon således simulerer en formell datatype, tilbyr den formelle datatypen muligheten å resonnere formelt om modulen: En modul som tenkes å implementere naturlige tall og addisjon, har kanskje en prosedyre pluss(x nat, y nat) somvises å ha de abstrakte egenskaper beskrevet ved Peano- aksiomene over. Ved formell resonnering (ved f.eks. såkaltgeneratorinduksjon; ren ligningslogikk er her for^<svak^>) kan vi avledex+y = y+x, som da gir i en passende forstand at pluss(m,n) = pluss(n,m), for alle aktualparametre m,n av typenat; under forutsetning av at evaluering av applikajonene av pluss ikke fører til run-time feil.

Slike resultater om en modul kan brukes i Hoare-analyse av progamtekst der instanser av modulen blir brukt; det være i et evt. hovedprogram eller f.eks. i deklarasjonen av en annen modul.³

Den andre delen av verikasjonsoppgaven består i å vise at den formelle

3De este programmeringsspråk tilbyr jo datatypen `naturlige tall med addisjon' ferdig implementert med korrekt semantikk. Med mekanismer for implementasjon av abstrakte datatyper, kan imidlertid programmereren implementere egne datatyper, og det er da nødvendig å etablere^<oppførselen^>, eller semantikken, til disse.

endmodulemodule<>; C;

F:^hG;Eⁱ -syntaktisk formelt uttrykk forA -abstrakt uttrykk for C

-formell resonnering om C

SY NTAKS SEMAN TIKK

A:^hV;Fi

SVAK SIMULERING IMPLEMENTASJON

Figur 1.2: Svak simulering og implementasjon av abstrakt datatype ^A ved moduldeklarasjon^Cog formell datatype^F.

datatypen ien presis forstand er enimplementasjonav den abstrakte datatypen.

Kriteriet vi skal bruke utrykkes i begrepetinduktiv ekvivalens, og ligningslogikk er sentral for dette. I tilnærmelser til induktiv ekvivalens, vil formell resonnering være sentral. Figur 1.2 oppsummerer litt av fremstillingen så langt.

Vi skal ikke snakke mer om samsvar mellom moduldeklarasjoner og formelle datatyper (nedre del av gur 1.2). Vår diskusjon skal dreie seg om formelle datatyper og formell resonnering og om samsvar mellom formell- og abstrakt datatype (øvre del av gur 1.2).

Ligninger deler termuniverset opp i klasser; hver klasse bestående av termer som kan vises ^<like^> ved ligningslogisk utledning. En slik klasseinndeling kan vi kalle ågi semantikk til termer. Det at en formell datatype implementerer en abstrakt datatype, hviler da i essens på en riktig klasseinndeling av termuniver- set. For formell resonnering er det sentralt at semantikk spesiseres på en måte somer tilnærmbar for formelle systemer. Ligninger og ligningslogikk er som sagt våre midler her.

Ligningslogisk omskrivning til syntaktisk like termer er én måte å gi seman- tikk på. Det nnes andre måter å gi semantikk på enn ved slik direkte om- skrivning. Især for semantikkgiving av generatortermer fra mange-til-en genera- torunivers, nnes det en rekke teknikker foruten den direkte metoden. Eksem- pelvis kan man denere semantikk på basis avobservatorfunksjoner ved å spesi- sere at to generatortermerg;g⁰er semantisk like hvis og bare hvish(g) = h(g⁰) for gitte observatorsymbolerh, er utledbart fra gitte ligninger.

En av de større diskusjonene i denne hovedoppgaven tar for seg nok en meto- de: En utledning fra en termgi et konvergent omskrivningssystem gir alltid en unik normalform. Et konvergent omskrivningssystem kan således sies åberegne en syntaktisk funksjonsyntsom gitt en termg, gir dennes normalform. En slik funksjon gir for hver termg en unik representant for klassen tilg ifølge seman- tikken gitt av ligningene i omskrivningssystemet. Vi kan derfor gi semantikk til termer ved å bestemme at to termerg;g⁰skal forstås som like hvis og bare hvis

synt(g) =synt(g⁰) ()

terer synt. Imidlertid kan semantikkgiving etter prinsipp () generaliseres til semantikkgivende syntaktiske funksjoner som ikke er beregnbare ved konver- gente omskrivningssystemer i den forstand som over.

En syntaktisk funksjon som implementeres av et konvergent omskrivnings- system, gir altså for hver termg en unik representant for klassen til g. Denne representanten er selv et medlemav klassen;en egenskap viessensielt skal la kva- lisere til navnetkanonisk representant for klassen. Alle syntaktiske funksjon- er implementert av konvergente omskrivningssystemer i ovenstående forstand, er slike kanonisk-representant funksjoner. Men ikke alle kanonisk-representant funksjoner kan implementeres på den måten: En vanlig symbolsk representa- sjon for mengder av naturlige tall, er sekvenser induktivt bygget opp av sym- bolene 0, succ, Ø og add. Mengden ^f0;1^g kan f.eks. representeres av termen add(add(add(Ø,succ(0)),0),succ(0)). Det er klart at vi her har et mange-til-en generatorunivers, og den ønskete semantikk (klasse-inndeling) til disse termer gis av ligningene

add(add(s,x),x) = add(s,x) og add(add(s,x),y) = add(add(s,y),x) For en klasse, kunne en naturlig kanonisk representant være den sorterte term- en uten repetisjon; for klassen til termen over:add(add(Ø,0),succ(0)). Det nnes imidlertid intet konvergent omskrivningssystem som implementerer en syntak- tisk funksjon som gitt en^<mengde^>-term, gir den kanoniske representanten til termens klasse. Grunnen til dette ligger i at ligningen

add(add(s,x),y) = add(add(s,y),x)

ikke kan orienteres uten at beviskraft mistes. Utbygginger av ligningslogikk som f.eks. betingete og ordnede omskrivningssystemer kan dog bøte på orienterbar- hetsproblemet i akkurat dette tilfellet.

Syntaktiske funksjoner som ikke er kanonisk-representant funksjoner, kan også gi semantikk til termer ved prinsipp (). Også slike syntaktiske funksjoner går ut over det som er implementerbart av konvergente omskrivningssystemer i ovennevnte forstand.

Generelle semantikkgivende syntaktiske funksjoner løfter idéen omsemantik- kgiving ved omskriving til syntaktisk like termerut avdet begrensende domenet til ren ligningslogikk. I lys av orienterbarhetsproblemet over, kan styrken til be- tingete og ordnede omskrivningssystemer også sies å være innlemmet i generelle semantikkgivende syntaktiske funksjoner.

Som andre funksjoner, kan semantikkgivende syntaktiske funksjoner spesi- seres ved ligninger og ligningslogikk. Ligninger som spesiserer semantikkgiven- de syntaktiske funksjoner giropphavtildetviskalkalleindirekte spesikasjonav semantikk. Indirekte spesikasjon spesiserer semantikk på en måte avledet fra vanlige måter ligninger gir semantikk på. Via indirekte spesikasjon innplantes dermed ligningslogikk med kraften til generelle semantikkgivende syntaktiske funksjoner.

Klassen av semantikkgivende syntaktiske funksjoner er altså større enn klas- sen av funksjoner implementerbare av konvergente omskrivningssystemer. Indi- rekte spesikasjon har derfor et potensiale for å utvide området av semantikk- spesisering som det er mulig å få mekanisk grep på ved konvergente omskriv- ningssystemer (i sin enkleste versjon).

Vi skal se at spesikasjon av semantikkgivende syntaktiske funksjoner be- grepsmessig kan forestilles å være på et^<meta^>-nivå forskjellig fra den abstrakte datatypen om hvilken det i utgangspunktet skal resonneres. Vi må i prinsipp da

behandle indirekte spesikasjon separat fra ligninger som denerer funksjoner (i den opprinnelige abstrakte datatypen). Vanlige måter å spesisere semantikk på er ikke tilstrekkelige for å uttrykke slik sammensatt semantikk. Vi utvikler derfor nyegeneralisertesemantikker. Dette er en annen hoveddiskusjon i denne oppgaven. Vår generaliserte semantikk har en modulær oppbygning, og åpner for en modulær oppbygging av formelle datatyper. Denne modularitet er for oss essensiell når indirekte spesikasjon skal sees som del av en større spesikasjons- omgivelse.

En stor del av diskusjonen skal også gå til å vise at indirekte spesikasjon, under visse interessante forutsetninger faktiskkan integreres med ligninger for vanlige funksjoner.

Indirekte spesikasjon skal vise seg å være et interessant supplement til al- gebraisk spesikasjon. Ett særtrekk ved indirekte spesikasjon er enoperasjonell spesikasjonsstil som faktisk gjør spesikasjoner tilgjengelige for programveri- kasjons-metoder.

Konsistens er et gjennomgangstema. Konsistens er relatert til grunnleggen- de oppfatninger om den semantiske verden som nedfelles somforutfatninger i semantikkspesikasjon og som ikke ønskes rørt ved. Eksempelvis nedfelles vår oppfatning om at en matematisk påstand ikke både kan være sann og gal i predikatlogikk ved predenerte (forutfattede) tolkninger av symbolene trueog false, samt ved å kalle en aksiommengde for inkonsistent dersomtrue = false er utledbart fra mengden. (In)konsistens må således alltid sees relativttil slike forutfatninger.

Vi skal sammen med utviklingen av generaliserte semantikker, utvikle til- hørende konsistensbegreper. Vi skal se hvordan inkonsistens kan oppdages og hvordan konsistens kan etableres.

Vi skal dessuten innføre begrepetkunstiginkonsistens. Dette er inkonsistens med opphav i hjelpefunksjoner; funksjoner som er nyttige hjelpemidler under implementasjon men som begrepsmessig kan sees ikke å høre hjemme på det semantiske plan. Vi skal søke å skjule hjelpefunksjoner og dermed kunstig in- konsistens fra den formelle resonnering, slik at de implementatoriske fordeler ved bruken av hjelpefunksjoner likevel kan utnyttes.

Universell algebrafanger inn mange begreper relatert til formelle og abstrak-* te datatyper. I kapittel 2 presenteres noen for oss vesentligere deler av universell algebra, innledet av en kort oppsummering av grunnleggende matematiske be- greper. Presentasjonen av algebra går så over i et avsnitt om semantikk. Vi utvikler generaliserte måter å spesisere semantikk på vha. ligningslogikk vårt grunnleggende formelle system. Vi utvikler også konsistens-begreper knyt- tet til disse spesikasjonsmåtene. Kapitlet avsluttes med mekanisering av lig- ningslogikk og relevante formelle systemer bygget på ligningslogikk for formell resonnering i formelle datatyper.

I kapittel 3 tar vi så for oss semantikkgivende syntaktiske funksjoner. Vi lar slike funksjoner motiveres som en eksplisittgjøring av konvergente omskriv- ningssystemer. Vi generaliserer den semantikkgivende egenskapen og anerkjen- ner kanonisk-representant funksjoner som et viktig spesialtilfelle. Vi studererer så spesikasjoner av semantikkgivende syntaktiske funksjoner og bruker disse i indirekte spesikasjon. Disse benyttes i anvendelser av semantikkbegrepene ut- viklet i kapittel 2. I dette kapitlet utvikles også begrepet kunstig inkonsistens, og vi utvikler teori og antyder metoder for skjuling av kunstig inkonsistens.

I kapittel 4 denerer vi en utvidelse avKnuth&Bendix-komplettering. Denne utvidelsen er interessant i sammenheng med konstruktive bevis. Vi relaterer dessuten denne utvidelsen til temaer i kapittel 2 og kapittel 3.

Abstrakte og formelle datatyper

I dette kapitlet deneres begrepene abstrakt datatype og formell datatype. Vi etablerer hva vi mener med at en formell datatype er enkorrekt implementasjon av en abstrakt datatype.

Vi presenterer forskjellige måter å denere formelle datatyper på ved hjelp av ligningslogikk. Slike ulike måter fremkommer ved ulike metoder for å dele opp et termunivers i klasser, slik at hver klasse består av termer vi ønsker skal representere samme matematiske objekt i en abstrakt datatype.

Kjente måter sominitialsemantikk og nalsemantikk presenteres. Vi innfører generaliseringerav initialsemantikk og nalsemantikk. Disse generaliseringer gir oss et begrepsapparat som gjør oss istand til å uttrykke vesentlige egenskaper ved spesikasjonen av formelle datatyper.

Konsistens er her en sentral egenskap. Ved hjelp av generalisert initial- og nalsemantikk, knytter vi konsistens til enintensjon bak måtene å spesisere forskjellige formelle datatyper på.

Våre generaliseringer av initial- og nalsemantikk er også en forberedelse til diskusjonen i kapittel 3.

Vi er interessert i formell men ogsåmekanisk resonnering. Kapitlet avsluttes med en presentasjon av sentrale begreper for mekanisk resonnering.

2.1 Grunnleggende begreper

Vi oppfrisker her noen grunnleggende matematiske begreper som brukes utover i den videre diskusjon. Vi bygger det hele opp ved begrepetmengde.

Mengder

Vi antar en intuitiv forståelse av begrepet mengde. Vi antar også en grunnlegg- ende kjennskap til notasjoner og begreper knyttet tilmengder. Vi skal her likevel gi noen avledninger og konvensjoner som vi kommer til å bruke i det følgende.

Vi skal alltid (implisitt eller eksplisitt) se matematiske objekter som elemen- ter i mengder. Dersoma;a⁰ betegner samme element i en mengde, skal vi si de eridentiske. Vi skriver da a = a⁰. Vi bruker denne notasjon kun for slik elementidentitet. Vi skrivera6=a⁰nåraoga⁰ ikke er identiske.

n-tupler

Et n-tuppel ^ha¹;:::;anⁱ for et naturlig talln, er en ordnetmengde¹. Et m- tuppel ^hb¹;:::;bmⁱ og et n-tuppel^ha¹;:::;anⁱ er identiske hvis og bare hvis m=noga_i=b_ifor 1in. Vi kallera_i fori-te komponenti^ha¹;:::;a_ni. En sekvens q er et n-tuppel for en uspesisert n og der n er lengden av q. En sekvens kan dessuten ha uendelig lengde. Vi betegner sekvenser av lengde 0 med". Vi betegner lengden av en sekvenssmedlens.

For vilkårlige mengderA¹;:::;An, er mengden betegnetA¹ An det n-foldige kartesiske produkt av A¹;:::;An mengden av n-tupler

ha¹;:::;anⁱ slik at a^{1 2} A¹;:::;an ² An. Dersom alle A¹;:::;An er identis- ke med en mengdeA, betegner vi ofteA¹ AnmedAⁿ, derA⁰=^;. Relasjoner

En n-ær relasjon^<påA¹;:::;A_nfor et naturlig talln, er en delmengde av A¹ A_n for gitte mengder A¹;:::;A_n. Dersom A¹;:::;A_n alle er iden- tiske med en mengde A, sier vi bare at ^< er en relasjon påA og kaller daA relasjonsdomenet(eller baredomenet) til^<.Restriksjonen av en relasjon

< A¹ An tilA⁰¹ A⁰_n (eller tilA⁰for A⁰¹ = =A⁰_n=A⁰) for A⁰¹A¹;:::;A⁰_nAn, er relasjonen^{< \}A⁰¹ A⁰_nog betegnes^<_A⁰¹_A⁰_n (eller ^<A⁰ forA⁰¹= =A⁰_n=A⁰).

Vi skal i vår diskusjon fremover snakke mye om binære (2-ære) relasjoner. La

< ABog^<0BCvære vilkårlige binære relasjoner for vilkårlige mengder A;B;C.^< sininvers^<;1, er relasjonen slik at^hb;a^{i 2 <;1} hvis og bare hvis

ha;b^{i 2 <}. Enhver binær relasjon har en entydig invers.Sammensetningen

<<⁰ av ^<og^<0 er relasjonen^fha;ci j 9b2B j ha;bi 2 <og^hb;ci 2 <⁰g. For

< AAkan videnere^<0 =^fha;ai ja2Ag,^<1=^<og^<n=^<n;1<;n >1.

(Denne notasjonen skal ikke forveksles med den for kartesiske produkt.) La ^< være en vilkårlig binær relasjon på A for en eller annen mengde A (altså^< AA). ^<kalles

reeksivdersom^ha;a^{i 2 <}, for allea²A.

symmetriskdersom^ha;bi 2 < ) hb;a^{i 2 <}. (Dvs.^<=^<;1.) transitivdersom^ha;b^{i 2 <}og^hb;ci 2 < ) ha;c^{i 2 <}.

En ekvivalens-relasjon er en (binær) relasjon som er reeksiv, symmetrisk og transitiv.

For en vilkårlig binær relasjon ^<på en eller annen mengde A, denerer vi forskjelligetillukningerav^<slik:

<⁺ =^{<0[ <}, denreeksive tillukningav ^<.

<⁺=^S_n>^0<n, dentransitive tillukningav^<.

M.a.o.^ha;c^{i 2 <+ , h}a;c^{i 2 <}eller det nnes enbslik at^ha;b^{i 2}

<og^hb;c^{i 2 <+}.

<=^{<0[ <+}, denreeksiv-transitive tillukningav^<.

<=< [ <^;1, densymmetriske tillukningav^<.

< ervelfundertdersom det ikke nnes noen uendelig sekvens ^ha;b;c;:::i

fora;b;c;::: 2Aslik at^ha;bi 2 <;hb;ci 2 <;:::.

Denuniversellerelasjon på enA¹ A_ner mengden^fha¹;:::;a_ni ja_i2

A_i;1 i ng. Vi skal ofte skrive a < b og a 6< b i stedet for ^ha;bi 2 < og

ha;bi 62 <hhv.

1En ordnet mengde er mengde-teoretisk ikke en ny type objekt, men deneres utfra (vanlige) mengder. Paret^ha;bideneres i mengde-teori som mengden^ffag;fa;bgg. Et vilkårlig

n-tuppel^ha1;:::;ani;^n>2 deneres som paret^{hha1;:::;an ;1i;ani}.

Funksjoner

Enfunksjonf fraAtilB for vilkårlige mengderAogB, er en binær relasjon

<f ABslik at det nnes nøyaktig ett tuppel (2-tuppel) i^<f slik ata²A er første komponent, for allea²A. For hvera²Akan vi da identisere en unik b²Bverdienavaunderfslik ata^<f bog som vi skal betegnef(a). Vi kaller Aog B hhv.funksjonsdomenet (eller bare domenet) ogkodomenet til f. Vi skal tidvis forestille oss funksjoner somoperatorer på sitt domene.

For en vilkårlig funksjonf fraAtilB for mengderAogB, sier vi da atf tar elementer fraA oggir elementer fraB. Vi skal da kalle f(a) enapplikasjon avf påafor ena²A. Vi betegner mengden av alle funksjoner med domeneA og kodomeneB med (A!B).

La f ² (A ^! B) være en vilkårlig funksjon for mengder A og B. For en A⁰Asier vi atf(A⁰) =^ff(a)^ja²A^0gerbildetavA⁰under f. En funksjon f ²(A^!B) erinjektivdersom for allea;a⁰²A:a⁶=a^{0 )} f(a)⁶=f(a⁰). En funksjonf ²(A^!B) er surjektivdersom det for alleb²B nnes ena²A slik at f(a) = b; dvs. at B er identisk med bildet av A under f. En bijektiv funksjon er en funksjon som er både injektiv og surjektiv. Alle binære relasjoner har som sagt en invers. Bijektive funksjoner (spesielle binære relasjoner) har dessuten alltid en invers som selv er en bijektiv funksjon. Sammensetningen av funksjoner er en funksjon. Sammensetninger av bijektive funksjoner er en bijektiv funksjon.

Etkspunkttilen funksjonfer etelementaidomenet tilfslikatf(a) =a. Enkonstantfunksjon fa er en funksjon slik at for en a så er fa(x) =a for alle x i domenet til fa. En mengdeA erlukket under en funksjon f, dersom f(a)²A for allea²A.

Laf ²(A¹ An^!B);n >0. Vi sier atf ern-ær.Laa¹²A¹;:::;an²

An. Vi skal lette skrivemåten forf(^ha¹;:::;anⁱ) ved å skrivef(a¹;:::;an).

Funksjoner er relasjoner, så relasjon-språkbruken `enn-ær funksjonf på A' for en mengdeA, henspeiler på en delmengde avA<sup>n+1</sup>. Funksjonsdomenet tilf er daA<sup>n</sup>. Videre er begrepene `restriksjon', `sammensetning' samt notasjonen fⁿfor funksjoner denert ved relasjoner.

Vi kommer til å bruke ordenefunksjon ogavbildning om hverandre.

*

Vi har denert relasjoner som en spesiell type mengde og funksjoner som en spesiell type relasjon. Dette denisjonshierarkiet skal vi ha nytte av å snu på hodet som følger: Vi kan betrakte enn-ær relasjon ^< på mengder A¹;:::;An

som en n-ær funksjon f^<funksjonsvarianten til ^<fra domenet A¹

A_ntil kodomenetBool =^f?;>ghvorf^<(a¹;:::a_n) =^>hvis og bare hvis

ha¹;:::;an^{i 2 <}, fora¹2A¹;:::;an²An. (Men merk atf^<jo selvfølgelig igjen er en (spesiell)n+ 1-ær relasjon^<f^< påA¹;:::;An;Bool.)

Vi skal også tidvis se på elementer som konstantfunksjoner; dvs. et vilkårlig elementa²Asees på som en konstantfunksjon med kodomene ^fa^g.

Store mengder

Vi betegner mengden av alle mengder med^S. Mengden av alle delmengder av en mengdeA betegnes med^P(A) . Mengden av alle funksjoner betegnes med

F.²

2`Mengden av alle mengder' er ikke et uproblematisk begrep (jf. `Russels paradoks'), men for vår diskusjon lar vi dette ligge.

Avgjørbarhet

En egenskap^P sies å være(eektivt) avgjørbar, dersom det nnes en deter- ministisk mekanisk prosess (deterministisk abstrakt maskin) som i endelig tid (i et endelig antall diskrete steg) gir en bestemt symbolkongurasjon^S(^P) hvis og bare hvis ^P holder.

En mengde sies å være avgjørbar, dersom medlemskap i mengden er avgjør- bar.En oppgave^Oeralgoritmisk, dersomdet nnes en deterministisk mekanisk prosess som i endelig tid i en passende forstand utfører^O.

2.2 Algebra

Fra det grunnleggende begrep `mengde' har vi denert^<høyere-nivå^> begreper somn-tupler, relasjoner og funksjoner som spesielle typer mengder. Vi denerer nå et begrep på et enda høyere nivå.

En algebra er essensielt et tuppel ^hA;Fi, der A er en mengde ogF er en mengde funksjoner påA. En algebra kan således avgrense et interesse-område.

Ønsker man f.eks. å studere trigonometriske funksjoner på de reelle tall, vil man kanskje betrakte algebraen ^hR;f+;;sin;cos^gi. Vi skal med begrepet algebra presisere begrepet abstrakt datatype og også begrepet formell datatype.

Vi søker å implementere abstrakte datatyper ved formelle datatyper. Ved å implementere en abstrakt datatype menes her 1) å representere verdimeng- den i datatypen symbolsk, og 2) å modellere funksjonene i datatypen formelt.

Implementasjon kan altså sees som bestående av en representasjonell del og en operasjonell del. Vi ønsker også å resonnere formelt og i siste instans også mekanisk ved hjelp av formelle datatyper. Til dette trengs også symbolske re- presentasjoner og/eller et formelt språk.

Vi gir her først det formelle språket. Deretter deneres avbildninger som

<tolker^>språket til semantiske størrelser.

2.2.1 Formelt språk

Det formelle språket skal være typet. Typeuniverset er imidlertid svært enkelt og en delmengde av f.eks. typeuniverset i typet-kalkyle.

La^GTypevære en gitt symbolmengde avgrunntyper. Vi denerer en meng- de^Typeavtyperfra^GType og symbolmengden^f;^!gsom den minste meng- den av symbolsekvenser (skrives tettløpende) som tilfredstiller:

GType Type

T¹;:::;Tn;T ^{2 GT}ype;n1 ⁾ T¹ Tn^!T ^{2 T}ype

(Merk at denne denisjonen av typerikke er induktiv. De typer vi her befatter oss med, kan derfor ikke være av vilkårlig kompleksitet.)

Enfunksjonsproler en symbolsekvens på formen f :T

der f er etfunksjonsymbol og T er en type. Vi sier at f her er av type T. DersomT =T¹ T_n^!T_C;n1,sier viatf hararitetn.HvisT 2 GType, kallesf enkonstant.

En (funksjons)signatur er en endelig mengde funksjonsproler³. Et funksjonsymbol kan høyst forekomme én gang i en signatur. Dersom det kun

3Vi lar informasjon om ariteter og om hvilke grunntyper som er involvert fremgå implisitt gjennom prolene i signaturen.

forekommer én grunntype i en signatur, skal vi tidvis forkorte skrivemåten av signaturen ved å bare angi funksjonsymbolene (og deres ariteter) uten fullsten- dig prol. Denne skrivemåten inspirerer til å kalle en slik en-typet situasjon for utypet. Vi skal også bruke denne forkortede skrivemåten ellers, hvis typeinfor- masjon er overødig for diskusjonen.

Envariabelproler en symbolsekvens på formen x:T

derxer etvariabel(symbol)ogT er en grunntype. Visier atxer av typeT.En variabelsignatur^V er en endelig mengde variabelproler. Et variabelsymbol kan kun forekomme én gang i en variabelsignatur. Dersom det kun forekommer én grunntype i en variabelsignatur, eller hvis det ellers er hensiktsmessig, skal vi tidvis angi bare variabelsymbolene, uten fullstendig prol.

La og ^V være en vilkårlig funksjonssignatur og variabelsignatur hhv. Vi denerer mengden^T(^V) av termerover og^V som den minste mengden av symbolsekvenser induktivt bygget overog^V (samt noen skillesymboler) som tilfredstiller følgende:

V T(^V)

Hvisk :T ²ogT ^{2 GT}ype, så erk^{2 T}(^V).

Hvis f :T¹ Tn^!T ² og ti ^{2 T}(^V) og ti er av type Ti for 0< in, så erf(t¹,:::,tn)2 T(^V). Vi sier atf(t¹,:::,tn)er av typeT. Vi betegner mengden avgrunntermer^T(^;) med^G.

2.2.2 Tolking av formelt språk

En typetolk er en avbildning ^{T 2} (^Type ^{! Sn ;}), slik at for vilkårlige T⁰;T¹;:::;Tn;T ^{2 GT}ype;n1:

^T(T⁰)^{2Sn ;}.

^T(T¹ Tn^!T) = (^T(T¹) ^T(Tn)^!T(T)).

For en vilkårligT ^{2 T}ype, sier vi at^T(T) er entolkningav T.

En funksjonsproltolk er en avbildning ^F slik at for en vilkårlig prol f :T:

F(f :T)^2T(T)

for en (forutbestemt) tolk av typer^T. Vi sier at^F(f :T) er entolkningavf, for et vilkårlig funksjonssymbolf; underforstått en tilhørende funksjonsprol.

Vi sier at^T herinngåri (denisjonen av)^F.

*

En-algebraAfor en signaturer etr+1-tuppel^hD¹;:::;Dr;F^{i 2SrP}(^F), slik atDi=^AT(Ti);1irfor entypetolk^AT og der^fT¹;:::;Tr^ger mengden av alle grunntyper som forekommer i. For 1 i r kalles Di tolkningen av Ti iA. Videre erF en mengde funksjoner (også konstanter) slik: For hver funksjonsprolf :T iskal det være en tolkning fA =^AF(f :T) iF for en funksjonsproltolk^AF hvori ^AT inngår. Vi sier atfA ertolkningenavf iA. AlgebraenAer entolkningavog er entydig bestemt av^AT og^AF. Somregel skal vi ikke eksplisitt nevne tolkene som inngår i denisjonen av en-algebra.

Dersom vi snakker om en-algebra for en eller annen ikke nærmere spesi- sert signatur, skal vi bare bruke benevnelsenalgebra. Vi kallerDi;1ir, bæremengdertilA,ogFkallesfunksjonsmengdentilA.Viskaloftebetrakte bæremengdene til en algebra under ett og da som unionen av alle bæremengd- ene. Denne unionen refereres da til som algebraens domene. Vi betegner ofte en algebra og dens domene med det samme; altsåA=^hA;Fⁱ. Vi betegner da bæremengdenDiAfor en 1irtidvis medATi.

Eksempel 1 Betrakt den (utypete) signaturenInt=^f0,succ,pred^g. Ariteter er hhv. 0, 1 og 1. En mulig tolkning avInter algebraen^Int =^hZ;^f0;succ;pred^gi dersuccogpreder hhv. etterfølger- og forgjengerfunksjonen for hele tall. Disse er tolkningene i^Int av hhv.succogpred. Konstantfunksjonen 0 er tolkningen i

Int av0.

d

Etredukt av en-algebraA = ^hD_A;F_Aier en⁰-algebraB = ^hD_B;F_Bi for en ⁰slik atD_B D_A;F_BF_A⁰, der F_A⁰ er restriksjonene av funksjonene iF_A tilD_B. Spesialtilfellet forF_B=F_A⁰ kalles ensubalgebraavA. Et redukt av Asom ikke er en subalgebra avAer etekte reduktavA.

Eksempel 2 For signaturen Int⁺ = ^f0;succ;pred;+^g med ariteter 0;1;1;2 hhv., betrakt Int⁺-algebraen ^Int⁺ = ^hZ;^f0;succ;pred;+^Zgi for +^Zaddisjon på hele tall. For Nat⁺ = ^f0;succ;+^g Int⁺, er Nat⁺-algebraen ^Nat⁺ =

h^N;^f0;succ;+^Ngi for +^Naddisjon på hele tall, et ekte redukt av^Int⁺.

d

Med en `abstrakt datatype' skal vi nå mene en `algebra'tolkningen av en funksjonssignatur; altså en tolkning av et syntaktisk objekt. Vi har nå etablert et grunnlag for vårt semantiske sprang mellom syntaks og semantikk.

Grunntermer er delen av det formelle språk som skal representere elementer og funksjonsapplikasjoner i en algebra. Gitt en -algebra A, følger en grunn- termtolk naturlig utfra typetolken og funksjonsproltolken i denisjonen avA. Vi skal imidlertid generelt ha bruk for mer ^<abstrakte^> termtolker. Til det trengs et par begreper til.

2.2.3 Homomorer og term-algebraer

LaA;B være to vilkårlige-algebraer for en signatur. Enhomomorfra A til B er en avbildning fra A sitt domene til B sitt domene slik at for alle f :T¹ T_n^!T 2;n1

(f_A(a¹;:::;a_n)) =f_B((a¹);:::;(a_n))

for alle^ha¹;:::;a_ni 2A¹ A_n, derA_i er tolkningen avT_i;1in, iA, ogf_Aogf_Ber tolkningene avf iAogBhhv. Vi krever at^h(a¹);:::;(a_n)^{i 2} B¹ BnderBi er tolkningen avTi;1in, iB.

Vi skriver av og til _BA for en homomor fra en algebra A til en algebra B. Mengden av homomorer fra A til B betegnes med ^Hom_BA. Dersom det nnes en surjektiv homomor fraAtilB, kallesB ethomomorft bildeavA. Sammensetningen av homomorer er en homomor.

La^Kvære enklasse(mengde) algebraer. En algebraA^{2 K}kallesinitielli

Khvis det for alle algebraerB^{2 K}ns nøyaktig én homomor fraA tilB. På den annen side kallesAnali^Khvis det for alle algebraerB^{2 K}ns nøyaktig én homomor fraB tilA.

For en gitt og variabelsignatur^V denerer vi enterm-algebra fraog

V som-algebraen med bæremengde^T(^V) og med den minste funksjonsmeng- de slik at det for hver funksjonsprol f :T¹ Tn^!T 2 ;n 1, nnes