Kuten edellä totesimme, symmetria voidaan ymmärtää automorfismin käsitteen avulla. Rajoitan tarkastelun tässä käytännössä graafien automorfismeihin, ja vielä spesifimmin, invarianssiryhmiin. Kertauksena, jos meillä on Kripke-rakenne (S,R,L), jossa (S,R) on graafi ja L on "lätkäfunktio", joka antaa siis jokaiselle S:n alkiolle joukon propositioita, invarianssiryhmä on automorfismiryhmä, jonka mielivaltaiselle alkiolle &sigma pätee, että kaikille s &isin S, L(&sigma(s)) = L(s).
Intuitiviivisesti esitettynä invarianssiryhmä koostuu sellaisista S:n alkioiden permutaatioista, jotka takaavat, että kun on annettu jokin lähtösolmu, niin sekä alkuperäisessä graafissa että sen kuvassa tästä solmusta lähtien voidaan kohdata vain samalla tavalla merkittyjä polkuja, so. kaikilla poluilla on samat ominaisuudet. Jos ollaan aivan tarkkoja, vielä vahvemmat ominaisuudet pätevät, koska eivät ainoastaan polut, vaan kaikki puut (joiden ominaisuudet voidaan karakterisoida CTL-logiikalla) säilyvät.
Symmetrioiden matematiikka on tavallaan hyvin "vaikeaa", vaikka itse asia on intuitiviisesti "helppo": järjestelmää voidaan tutkia vaihtelemalla sen osia keskenään jollakin tavalla, ja sen käyttäytyminen ei tässä tarkastelussa muutu. Vaikka näitä käyttäytymistapoja on samalla järjestelmällä useita, kaikkien ominaisuuksien selvittämiseksi riittää tehdä vain yksi näistä tarkasteluista. Invarianssi takaa, että kaikki muut tarkastelut antaisivat tarkalleen saman tuloksen. Yksinkertainen esimerkki on vaikkapa järjestelmä, jossa on tulostuspalvelin ja n identtistä asiakaskonetta. Järjestelmän mallinnoksessa asiakaskoneilla on rotaatiosymmetria. Jokaisessa järjestelmän tilassa voidaan aina pyörittää n asiakaskonetta niin, että niistä "pisimmälle" edennyt (jossakin merkityksessä) on numero 1, tasatilanteessa pyritään saamaan kolmanneksi pisimmälle edennyt mahdollisimman pieneen indeksiin jne, eli "aakkosjärjestyksessä" pienin permutaatio edustaa kaikkia sen rotatoituja versioita.
Abstrahoinnin ja symmetrian yhdistäminen on hieman hankala tehtävä. Käsittelen tässä vain hyvin kapeaa osaa siitä. Oletetaan, että Kripke-rakenne M=(S,R,L) on peräisin järjestelmäkuvauksen X operationaalisesta semantiikasta. X voi sisältää mitä hyvänsä operaatioita, mutta oletan yksinkertaisuuden vuoksi, että kuvauksessa on joukko muuttujia ja joukko tapahtumia muotoa (g,a), missä g on predikaatti muuttujien yli ja a on funktio, joka kuvaa muuttujien vanhat arvot uusiksi. Semantiikka on sellainen, että S koostuu kaikista mahdollisista muuttujien arvoista ja (s,s') &isin R jos ja vain jos tapahtumien joukosta löytyy sellainen tapahtuma (g,a), että g(s) pätee ja a(s) = s'. Oletamme, että propositiot ovat joitain tutkijaa kiinnostavia väittämiä muuttujista, ja että kykenemme jokaisessa tilassa nämä ilmaisemaan L:n avulla.
Abstraktiolla viittaan tässä nyt sellaiseen kuvaukseen, joka muuttaa järjestelmän semantiikkaa niin, että jotain hävitetään. Esimerkiksi voimme ajatella, että korvaamme kokonaislukumuuttujan x
(äärettömän) arvodomainen kolmelle arvolla, eli "negatiivinen", 0, ja "positiivinen". Jokainen tilanne, jossa x esiintyy jossakin roolissa missä sen arvoa kysytään tai muutetaan, noudattaa tätä abstraktiota. Abstraktio tuottaa epädeterminismiä, koska kun esimerkiksi vähennämme positiivisesta arvosta jotakin, tulos voi olla joko nolla tai positiivinen. Ideana abstraktiossa on viimekädessä se, että mallin tilojen joukko pienenee.
M:llä on omat symmetriansa, mitä ikinä ne ovatkaan. Niiden laskeminen on hankala laskennallinen ongelma, ja usein käytännössä nojataan oletukseen, että järjestelmäkuvauksen laatija antaa jonkun lähtökohdan, esimerkiksi ilmoittaa mitkä prosessit ovat keskenään isomorfisia tms, ja symmetrian tunnistamisen ongelma oletetaan ratkaistuksi. Jos nyt käytämme alkuperäisen semantiikan sijaan abstraktimpaa semantiikkaa, niin joudumme kysymään, mitä symmetrioille tapahtuu. Tämä ongelma on ei-triviaali. Periaatteessa voimme rajoittua käyttämään abstraktiota, joka lupaa säilyttää symmetriat, esimerkiksi niin, että sovellamme abstraktiota symmetrian jälkeen. Tämä on kuitenkin epämielenkiintoinen ratkaisu, koska jos sovellamme abstraktiota etukäteen, saatamme kyetä tuottamaan uusia symmetrioita. Esimerkiksi, jos meillä on kaksi laskuria, joista toinen laskee viiteen ja toinen seitsemään, yllä mainittu arvoabstraktio tekee näistä laskureista symmetrisiä.
Yleensä abstraktio valitaan niin, että se ei koskaan hävitä virheitä, mutta voi synnyttää niitä. Tämä takaa virheiden löytymisen, jos niitä on alkuperäisessä, mutta mahdollistaa toki väärien (spurious) virhejälkien löytymisen. Väärä virhejälki voidaan kuitenkin käydä läpi automaattisesti ja tunnistaa kohdat, joissa abstraktio mahdollisti askeleen, jota alkuperäisessä mallissa ei tosiasiassa esiinny. Jos tällaista askelta ei ole, virhejälki on tietysti todellinen virhe. Muussa tapauksessa abstraktiota pitää tehdä hienojakoisemmaksi, eli poistaa ainakin jokin sellainen abstraktio, joka mahdollisti virheen. Symmetrian kanssa tulee taas tässä kohtaa eteen sama kysymys, eli miten se suhtautuu tähän nimenomaiseen abstraktioon. Yleensä tämä prosessi (symmetriaa lukuunottamatta) tunnetaan nimelle CEGAR, eli counterexample guided abstraction refinement.
Tässä kohtaa on syytä ottaa etäisyyttä ja ymmärtää tämän prosessin luonne filosofisemmin. Pyrin yleensäkin kirjoituksissani abstraktiosta käsittelemään sitä syvällisempää kognitiivista ja metakognitiivista ulottuvuutta, joka mielestäni tutkimusalallani on. Tässä kohtaa voimme ajatella minkä tahansa yrityksen ymmärtää ilmiötä tai muodostaa teoriaa eräänlaisena CEGAR-prosessina. Ongelmana on toimiva abstraktio; jos ihminen uskoo, että käytetty abstraktio säilyttää (operationaaliset) virheet, hän luottaa abstraktiin käsitykseensä ilmiöstä. Lisäksi ongelmana on tietenkin se, että kun todellisessa maailmassa tapahtuva tapahtumasarja sotii käsitystä vastaan, ei abstraktion hienojakoisemmaksi tekemiseen ole oikein mitään erityisempää keinoa, ja sosiaalinen paine hylätä koko malli "vääränä" on suuri. Esimerkkejä (kummastakin) ongelmasta löytyy vaikkapa taloustieteestä.
Ei kommentteja:
Lähetä kommentti