Lähdetään siitä, että malli on struktuuri (S,i,&tau), jossa S on jokin joukko, &tau on kokoelma relaatiosymboleita, ja i on kuvaus &tau &rarr P(S*), missä P on potenssijoukko, ja "*" on operaatio, joka ottaa unionin kaikista sen argumentin n-tupleista, kun n = 0,1,... i siis antaa tulkinnan jokaiselle relaatiolle.
Ensimmäisen kertaluvun predikaattilogiikan (FOL) tunnettekin jo. Jos M = (S,i,&tau) on malli ja &phi on FOL-lause, kirjoitamme M |= &phi, kun M on &phi:n malli. Tämä ilmaistaan myös niin, että &phi pätee M:ssä. Tulkinta on ilmeinen: Atomilauseke (eli yksittäinen relaatio) R(x) on tosi, jos annetulla x:n (käytän lihavointia osoittamaan, että kyse on vektorista, jätän ariteetin spesifioimatta kun sillä ei ole väliä) tulkinnalla ja i:n osoittamalla R:n tulkinnalla R(x) on voimassa. (Propositiot saadaan 0-ariteettisilla relaatioilla, jotka siis ovat vakioarvoisia tosiasioita) Jokainen lause on itsessään myös Teoria, eli se karakterisoi ne mallit, joissa teoria on tosi.
Kun olen esittänyt, että ei ole olemassa mitään "objektiivista todellisuutta", tätä ei tule ymmärtää makkaratukkien "kaikki on niinq sillee suhteellista"- läppänä, vaan ainoastaan niin, että teorioita muodostaessamme emme postuloi sitä, että on olemassa "yksi ja ainoa malli", vaan ainoastaan pyrimme karsimaan joitakin malleja pois. Sivuutan tässä operationalisoinnin problematiikan (joka liittyy tulkinnan kiinnittämiseen). En kirjoita filosofiasta tässä enempää, koska se ei ole nyt tässä aiheena.
FOL on siis logiikka, jossa on relaatioita, vakiosymboleja, muuttujasymboleita, ja kvantifiointi ainoastaan kiinteiden muuttujien kokoelmien yli, eli esimerkiksi ettemme implisiittisesti kvantifioi relaatioiden ariteettia. Matemaatikot tekevät näitä aika liberaalisti, mutta tietojenkäsittelyteoriaan ne eivät sovi, eivätkä yleensäkään silloin, kun semantiikan kanssa tulee olla erityisen tarkkana.
FOL:ia voidaan laajentaa mielenkiintoisella tavalla, ottamalla mukaan kiintopisteoperaatio. Kiintopisteoperaatio viittaa siihen, että voimme karakterisoida lauseen niin, että jos &phi(R) on lauseke, jossa R esiintyy tulkitsemattomana relaationa, jolla on kiinteä ariteetti (sanotaan vaikka n), voimme siirtyä juuri sen verran toisen kertaluokan puolelle, että sallimme kaavan lfp(&phi(R(x)). Tämän tulkinta toimii seuraavasti: R tulee tämän myötä määritellyksi sellaisen relaatiosekvenssin pienimmäksi (osajoukkomielessä) kiintopisteeksi, jossa sekvenssi määritellään niin, että R(0) on tyhjä joukko ja R(k) = R(k-1) U {x | &phi(R(k-1)(x)) on tosi}. Tämän sekvenssin pienin kiintopiste on siis se relaatio, jonka lfp(&phi(R(x)) määrittelee. Lauseissa voi laajennoksen jälkeen siis tällöin esiintyä paitsi muuttujia kvantifioituina, myös "vapaita" relaatioita karakterisoituna kiintopistemääritelmillä. Klassinen esimerkki on (graafeille) määritelty kaava:
&forall x &forall y: [lfp(&phi(R(u,v)): u = u &or &exist z: (u,z) &isin E &and R(z,v)](x,y)
Harjoitustehtäväksi jätetään selvittää, mitä tämä sanoo graafeista.
FOL + lfp on siitä mielenkiintoinen logiikka, että sen kaavoilla on erikoinen ominaisuus: Kun mallien joukoiksi rajoitetaan formaalit kielet tietyllä koodauksella, niin näiden mallien luokka on tarkalleen niiden kielten joukko, joihin liittyvät päätöstehtävät ovat ratkaistavissa polynomisessa ajassa. Kuuluisa P=NP- kysymys tulisi siis kertaheitolla ratkaistuksi, jos jollekin NP-täydelliselle kielelle löytyisi Lfp-karakterisointi. Jos esimerkiksi voisimme antaa hamiltonin polulle lfp-karakterisoinnin, se olisi siinä: P = NP pätisi. Toinen mahdollisuus olisi, että löytäisimme mallin NP:stä, josta voisimme osoittaa jollakin keinoin, ettei sille ole Lfp-karakterisointia.
tiistai 17. toukokuuta 2011
keskiviikko 11. toukokuuta 2011
Symmetria ja Abstraktio.
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ä.
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ä.
Tilaa:
Blogitekstit (Atom)