Olen kirjoittanut aiemminkin invarianteista. Olen tutkinut jonkin verran ns. Craig:in interpolantteja ja niiden induktiivisia invariantteja, ja yksi julkaisuni käsittelee induktiivisten interpolanttien löytämistä.
Olen tehnyt jonkin verran käytännön ohjelmointityötä (sellaista josta joku muu jopa maksaa). Muutoin kokemukseni rajoittuu pitkälti akateemisiin ympyröihin ja melko simppeleihin pikkunäppäriin koodinpätkiin. Käytännön työssä havaitsin hyvin nopeasti hyödylliseksi ajattelutavan, jonka opin Ralph-Johan Backin luennolla. Tästä on aikaa liki 15 vuotta, joten en muista tilannetta tarkkaan; Olin Turussa konferenssissa jossa yksi workshop käsitteli ohjelmoinnin opettamista. Back kertoi heidän kokeilleen sellaista pedagogista tyyliä, jossa opiskelijoiden kehotettiin aina ennen minkäänlaisen silmukkarakenteen kirjoittamista ensin miettimään kyseisen silmukan silmukkainvariantin.
Ihmisen ajattelu on luonteeltaan abstraktia ja usein rekursiivista. Rekursiivisuus on kuitenkin yleensä tiedostamatonta, ja sen nouseminen tietoisuuteen synnyttää usein kokemattomalla ihmisellä hämmenystä. Merkittävä osa huumorista perustuu itse asiassa rekursiivisuuteen, ja rekursiovitsit ovat nörttivitsien aatelia. Klassinen vitsi on, että kun kysytään "Mikä on rekursiivinen määritelmä?", niin vastaus on "Perustapaus, jota seuraa rekursiivinen määritelmä".
Ihmisillä on voimakas tarve operationalisoida rekursio iteraatioksi, prosessilla jota kutsun usein aukikelaamiseksi. Esimerkiksi jos joku kysyy miten löydämme polun paikasta A paikkaan B, niin voimme vastata "Jos A = B, ollaan jo perillä. Muutoin otetaan A:sta yksi askel kohti B:tä, ja etsitään tästä uudesta paikasta polku B:hen". Tämä on rekursiivinen määritelmä, mutta se ei tietenkään aina toimi, koska termi "Kohti B:tä" on epämääräinen. Jos me kelaamme tämän implisiittisen prosessin auki, niin usein teemme sen niin, että samalla esimerkiksi kiellämme käymästä samassa paikassa kahdesti.
Jos lähdemme oletuksesta että polku aina löytyy, niin tässä aukikelauksessa voidaan ilmaista invariantti joka sanoo, että missä ikinä olemmekin, sieltä pääsee paikkaan B. Jotta se tapa jolla toteutamme tämän iteraation olisi oikea, sen täytyy säilyttää tämä invariantti. Näinollen, jos kiellämme esimerkiksi käymästä samassa paikassa kahdesti, voi invariantti helposti mennä rikki: Kuvitellaan että meillä on polku A-->C --> D ---> B, ja sen lisäksi polku C --> E ja E--> C. Jos me lähdemme C:stä tä E:hen, emmekä saa palata C:hen, on invariantti efektiivisesti rikki kun olemme E:ssä.
Tätä ongelmaa ei korjaa esimerkiksi se, että tarkennamme "askel kohti B:tä" siten, että sanomme että pisteen johon siirrymme pitää olla "lähempänä" B;tä. Jos esimerkiksi piste E esimerkissämme on aivan B:n vieressä, mutta näiden välillä vain on ylipääsemätön este, emme tiedä tätä ennen kuin tulemme pisteeseen E ja huomaamme että olisi palattava pisteeseen C, mikä puolestaan on kiellettyä.
Olen jumissa työssäni seuraavanlaisen ongelman kanssa. Meillä on graafi -- sivuutan ison läjän itse ongelman kannalta merkityksettömiä yksityiskohtia -- jossa on solmuja ja kaaria. Kaarilla on jonkinlainen pituus ja jokainen kaari yhdistää kaksi solmua, sillä on siis alku- ja loppupää. Teemme graafille kontraktiohierarkian. Tämä tarkoittaa että "poistamme" solmuja iteratiivisesti ja aina poistaessamme lisäämme oikopolun kahden sen naapurin välille, jos näiden välinen lyhin polku (jäljellä olevassa graafissa) kulki poistetun solmun kautta.
Invariantti tässä prosessissa on, että vielä poistamattomien solmujen väliset lyhimmät polut ovat saman pituisia kuin alkuperäisessä graafissa. Tämän invariantin voimassaolo on helppo todeta: Jos invariantti on voimassa ja poistamme solmun x, niin jokainen lyhin polku kahden solmun a ja b välillä joka ei kulkenut x:n kautta, säilyy sellaisenaan. Jos taas se kulki x:n kautta, niin se kulki ensin johonkin solmuun u, sieltä x:ään ja sieltä v:hen, missä u ja v jäävät graafiin. Jos u:n ja v:n välinen lyhin reitti kulkee u->x->v, niin jokainen polku joka kulkee siten että se käy ensin u:ssa ja sitten v:ssä, voidaan tehdä lyhyemmäksi vaihtamalla osareittu u:sta v:hen reitiksi u->x->v. Tässä tilanteessa lisäämme oikopolun u-->v, ja tämä reitti on yhtä pitkä kuin ennenkin. Toisaalta jos lyhin reitti ei kulje x:n kautta, niin x:n poistaminen ei vaikuta mitenkään.
Solmut muodostavat poistamisjärjestyksensä mukaisen hierarkian. Solmu, joka poistetaan aiemmin, on hierarkiassa alempana, ja myöhemmin poistettu solmu ylempänä. Kun estimme kahden solmun välistä lyhintä polkua, etsimme ns konkaavin polun. Tämä polku on sellainen, että sen alkuosa kulkee lähtösolmusta aina hierarkiassa ylöspäin, ja kun se saavuttaa polun "korkeimman" solmun, se tämän jälkeen kulkee aina alaspäin kunnes se saavuttaa maalisolmun.
Voimme todistaa että tällainen polku on olemassa ja se vastaa alkuperäisen graafin lyhintä polkua: olkoon lähtösolmu u ja maalisolmu v. Näiden välillä on alkuperäisessa graafissa jokin lyhin polku v1, v2, ... , vn, missä v1 = u ja vn =v. Olkoon vk näistä se, joka on hierarkiassa korkeimmalla. Voimme osoittaa, että meillä on oikopolkuja hierarkiassa ylöspäin kulkeva polku u:sta vk:hon (ja samalla tavalla voimme osoittaa että sellainen on alaspäin vk:stä v:hen) seuraavasti:
olkoon vi se solmu, joka on hierarkiassa korkeimmalla välillä v1..vk-1. Edellä mainitun invariantin nojalla, ennen vi:n poistamista, meillä oli jäjellä lyhin polku vi-->vk. Koska välissä ei voinut tuolloin olla muita solmuja, meillä on oltava oikokaari vi-->vk. Nyt voimme rekursiivisesti todeta taas, että saman argumentin nojalla meillä on jokin solmu välillä v1 ... vi-1 jne.
Kirjoitin tämän blogikirjoituksen, koska kaikesta tästä huolimatta, testiaineistossa on tapaus, jossa erään sillan yli kulkevaa lyhintä polkua ei hierarkia säilytä. Se on olemassa alla olevassa graafissa, mutta sitä ei löydy hierarkian avulla. Jossakin kohtaa koodia siis jokin näistä asioista tehdään siten, että invariantti rikkoutuu.
Kun kirjoitin koodin, mielestäni pidin koko ajan tämän invariantin mielessä ja pidin huolen ettei mikään operaatio riko sitä. Tyypillisesti tällaisissa tapauksissa on kyse joko abstraktiorikosta -- esimerkiksi jokin tieto viittaa johonkin mikä on muuttunut välissä -- tai ns reunatapauksesta. Olen mielestäni eliminoinut kummankin vaihtoehdon. Jäljelle jää muutama vaihtoehto. Kyseessä voi olla logiikkavirhe: Jokin ehto on kirjoitettu tavalla, jonka semantiikka on eri kuin se, mitä tarkoitin. Tämä on epätodennäköisen tuntuinen selitys siksi, että virhe on niin harvinainen. Kyseessä voi olla toki jonkin rakenteellinen poikkeama jostain tekemästäni oletuksesta, joka on riittävän harvinainen tuottamaan tällaisen ongelman.
Tämä on kiusallista.
EDIT: Vika liittyi tietorakenteeseen ja algoritmiin. Erässä kohtaa kun graafin kaaria järjesteltiin uudelleen, osa tiedosta jäi päivittämättä. Tietty invariantin kannalta olennainen informaatio ei ollut siellä missä pitää. Virhe myös "piilotti itsensä", sillä kun konstruktion jälkeen graafi luettiin, informaatio meni oikeaan paikkaan. Lopulta löysin sen ja sain korjattua tänä aamuna, useamman tunnin buginmetsästyksen jälkeen.
Huomenna lähden lomalle.
Näytetään tekstit, joissa on tunniste logiikka. Näytä kaikki tekstit
Näytetään tekstit, joissa on tunniste logiikka. Näytä kaikki tekstit
torstai 16. toukokuuta 2019
perjantai 24. maaliskuuta 2017
Deskriptiivinen kompleksisuus
Kompleksisuusteoria on tietojenkäsittelytieteen osa-alue, joka käsittelee sitä, miten tehokkaasti tietynlaiset ongelmat voidaan ratkaista, kun käytössä on jokin tietty formalismi jolla laskentaa tms suoritetaan. Esimerkiksi, meillä on taulukko (tai muu vastaava tietorakenne) A, jossa on lukuja. Emme nyt problematisoi lukujen esittämisen vaatimia resursseja (suuren luvun esittäminen vaatii paljon bittejä), vaan abstrahoimme tässä nyt sen osan pois. Oletetaan, että taulukon koko on n, ja me pääsemme käsiksi taulukon i:nteen alkioon vakioajassa. Viittaamme tähän alkioon A[i]. Oletamme että kaikki taulukon alkiot ovat erisuuria. (Tämä oletus ei ole olennainen tai välttämätön, mutta teen sen typografisista syistä...)
Tehtävämme on siirrellä taulukon alkioita siten, että siirtelyn jälkeen taulukko on järjestyksessä. Tämä tarkoittaa sitä, että jokaisella kokonaisluvulla i välillä 1 < i < n+1 pätee että A[i-1] < A[i]. Tämä ei siis päde alussa. Meillä on käytössämme kaksi operaatiota, V(i,j), joka vaihtaa taulukon alkiot i ja j keskenään, sekä vertailuoperaatio A[i] < A[j].
Emme nyt keskustele siitä, miten tarkalleenottaen toteutamme taulukon järjestämisen. Oletamme että taulukko on alussa täysin sekaisin, emmekä tiedä mitään esimerkiksi siitä, mitä arvoja taulukossa on ja miten ne ovat jakautuneet. Voimme ilmaista taulukon järjestämisen permutaation etsimisenä, ja tarkastelemme ongelman kompleksisuutta tästä näkökulmasta.
Koska alkiot ovat erisuuria, on keskenään erilaisia tapoja laittaa alkiot taulukkoon n! kappaletta, missä n! = 1*2*...*n. Tämä tulee siitä, että ensimmäinen alkio voi olla mikä hyvänsä n:stä alkiosta, tämän jälkeen toinen voi olla mikä hyvänsä jäljellä olevista, jne. Näistä n!-kappaleesta permutaatioita meidän tulee löytää se, joka vastaa taulkon järjestyksessä olemista.
Jokainen vertailu, jonka taulukolle teemme, paljastaa meille jotain siitä, minkälaisen permutaation tarvitsemme. Tarkalleenottaen, kaikkien vielä mahdollisten permutaatioiden joukosta yksi vertailu sulkee pois tarkalleen puolet. Nimittäin, vertaamalla A[i] < A[j], (missä i < j) tulos on "kyllä" tasan silloin kun nämä alkiot ovat oikeassa järjestyksesä ja "ei" silloin kun oikeassa permutaatiossa ne ovat eri järjestyksessä. Muuta informaatiota emme yksittäisestä vertailusta (yleisessä tapauksessa) saa. Yhden vertailun (ja mahdollisen vaihdon) jälkeen permutaatiota on jäljellä n!/2, ja jokainen vertailu vastaavasti puolittaa permutaatioiden määrän. Tätä puolittamista on pahimmassa tapauksessa jatkettava kunnes permutaatioita on enää yksi. Tiedämme, että tällöin olemme tehneet log(n!) puolitusta. log(n!) on suunnilleen n*log(n), mikä tarkoittaa, että pahimmassa tapauksessa taulukon järjestämiseksi täytyy tehdä (osapuilleen) tämän verran vertailuja ja vaihtoja.
Tämä on yksinkertaisimpia analyysejä joilla voidaan tarkastella miten kompleksinen jokin ongelma on; tämä paljasti siis, että taulukon järjestäminen ei onnistu (aivan) suoraan taulukon kokoon verrannollisessa ajassa.
Vaikeampien kysymysten analysoiminen on usein -- niin -- vaikeampaa. Deskriptiivinen kompleksisuusteoria on teoria, joka yksittäisten ongelmien kompleksisuuden sijaan pyrkii luokittelemaan ongelmia sen mukaan, millä tavoin ne ovat ilmaistavissa. Oletetaan, että meillä on syötteenä jokin struktuuri ja jollakin logiikalla ilmaistu ominaisuus, ja tehtävänä on selvittää, onko annetulla struktuurilla tämä ominaisuus. Ongelman vaikeus riippuu siitä, millaisia ilmaisutapoja logiikassa on käytössä.
Esimerkiksi, jos meillä on annettu syötteenä graafi (eli suomeksi "verkko", mutta käytän tätä termiä välttääkseni sekaannusta) ja jokin ensimmäisen kertaluvun predikaattilogiikan kaava ja annettu joukko predikaatteja, voimme itseasiassa hyvinkin helposti tarkastaa onko kaava tosi. Tässä siis oletamme, että nämä predikaatit todella on annettu, eli pystymme suoraan laskemaan niiden arvon mille tahansa alkioille. Esimerkiksi "Kaikille solmuille x,y, pätee että niiden välillä on kaari" Tai "on olemassa solmut x, y, z siten, että (x,y) on kaari ja (y,z) on kaari".
Tätä ei pidä sekoittaa siis sellaiseen tilanteeseen jossa on annettu kaava, ja pitää selvittää päteekö kyseinen kaava ylipäätään jollekin mallille, eikä myöskään tilanteeseen, jossa predikaattien arvoja ei tunneta, ja pitäisi tietää voidaanko predikaateille antaa sellainen tulkinta, jolla kaava pätee annetulle struktuurille.
Ongelmat, jotka on ilmaistavissa tällä tavalla, ovat luokassa FO (sanoista First Order), ja deskriptiivisen kompleksisuusteorian yksi tulos on, että tämä luokka on sama kuin AC0, joka puolestaan tarkoittaa ongelmia jotka voidaan ratkaista hyvin tehokkaasti; Jokaiselle tällaiselle ominaisuudelle on olemassa hierarkia ongelman ratkaisevia logiikkapiirejä, joiden syvyys (perättäisten porttien määrä) on rajoitettu. On huomattava, että tämän luokan yksittäisen ongelman karakterisoi nimenomaan yksittäinen predikaattilogiikan kaava (joka kullekin ongelmalle on kiinteä), ja mahdollisten struktuurien joukko.
FO ongelmat eivät ole esimerkiksi graafeille kovin mielenkiintoisia, koska vaikkapa kysymystä "Onko kahden annetun solmun välillä polku" ei voidan ilmaista ensimmäisen kertaluvun predikaattilogiikalla.
Jos haluamme nimittäin karakterisoida jälkimmäisen tapauksen, niin tarvitsemme toisen kertaluvun logiikkaa. Täysi toisen kertaluvun logiikka antaa meille mahdollisuuden ilmaista esimerkiksi sen, että "on olemassa predikaatti P(x,y) siten, että...". Aivan vielä emme kuitenkaan ota näin vahvaa ilmaisuvoimaa mukaan.
Transitiivinen sulkeuma on operaatio, jonka lisääminen FO:iin tuo sopivasti ilmaisuvoimaa. Esimerkiksi, jos syötteenä on suunnattu graafi, niin meillä on automaattisesti käytössämme predikaatti p(x,y), joka sanoo että solmusta x on solmuun y vievä kaari. Lisäämme logiikkaamme operaattorin TC, joka toimii siten, että jos Q(x,y) on osakaava jossa on kaksi vapaata muuttujaa, niin TC(Q)(x,y) määrittelee tämän osakaavan Transitiivisen sulkeuman. Sen totuusarvo käyttäytyy seuraavalla tavalla: TC(Q(x,y)) tulkitaan itseasiassa siten, että joko Q(x,y) pätee, tai pitää löytyä jokin ei-tyhjä jono alkioita z1, z2, ..., zk siten, että Q(x,z1) pätee, Q(z1,z2) pätee, jne, ja Q(zk, y) pätee.
FO[TC] on niiden ongelmien joukko, jotka voidaan ilmaista käyttäen ensimmäisen kertaluvun logiikkaa ja transitiivista sulkeumaa. Esimerkiksi "Graafissa on polku solmusta s solmuun t" on ilmaistavissa tällä; jos p(x,y) on (annettu) predikaatti, joka pätee kun on kaari solmusta x solmuun y, niin polku solmusta s solmuun t on olemassa, jos pätee TC(p)(s,t). Tämä kompleksisuusluokka on sama kuin luokka NL, joka on niiden ongelmien luokka, jotka voidaan ratkaista "arvaamalla" ratkaisu askel kerrallaan ilman että koko ratkaisua täytyy muistaa.
Least fixpoint, eli pienimmän kiintopisteen operaattori taas mahdollistaa yksinkertaisen rekursiivisen ilmaisun, jolla määritellään uusi predikaatti. Muistutan tässä kohtaa, että olemassaolevat predikaatit ovat kiinteitä ja tunnettuja; TC yllä mahdollisti "uuden" predikaatin luomisen vanhojen predikaattien avulla hyvin yksinkertaisesti. LFP-operaattori on jo selvästi monimutkaisempi. Luodaksemme "toisen kertaluvun" predikaatin P -- eli predikaatin jonka tulkinta ei ole kiinnitetty -- ilmaisemme sen muodossa LFP(Q(P,x)) Tässä siis LFP-operaattorin sisään tulee kaava Q, jossa käytetään predikaattia P, muuttujia x ja olemassaolevia predikaatteja. Tämä tulkitaan tarkoittavan "pienintä" sellaista predikaattia P, joka toteuttaa kaavan P(x) = Q(P(x),x) kaikilla x; Rajoituksena on, että P(x) ei saa esiintyä negatiivisena kaavassa Q (so. kun kaava Q kirjoitetaan konjunktiiviseen normaalimuotoon, P:n negaatio ei saa esiintyä kaavassa).
Esimerkiksi relaation p(x,y) transitiivinen sulkeuma voidaan ilmaista LFP-operaattorilla kaavasta LFP(p(x,y) || \exists z: P(x,z) && p(z,y)). Eli, P(x,y) on p:n transitiivinen sulkeuma, kun se on "pienin" relaatio joka toteuttaa em rekursiivisen määritelmän. Pienin tässä yhteydessä tarkoittaa, että se joukko pareja, joka yhtälön toteuttaa, on minimaalinen; mikään sen aito osajoukko ei voisi toteuttaa yhtälöä. FO[LFP] = P, eli polynomisessa ajassa ratkeavat ongelmat ovat karakterisoitavissa LFP-operaattorilla rikastetussa ensimmäisen kertaluvun predikaattilogiikassa. Tämä teoreema on hankalahko todistaa, joten en tässä ala sitä nyt käymään läpi.
Jos siirrymme toisen kertaluvun logiikkaan "aidosti", eli sallimme uusien predikaattimuuttujien esittelyn, mutta rajoitumme eksistentiaaliseen kvantifiointiin, saamme mielenkiintoisen luokan, SO[E]. Tässä siis on kyse ensimmäisen kertaluvun logiikasta, jossa saa luoda predikaattimuuttujia, kunhan ne on sidottu olemassaolokvanttorilla. Käytän tässä merkintää \E, koska en jaksa kaivaa symboleja.
Tällöin voidaan sanoa vaikkapa että \E(P(x,y): P(x,y) <=> (p(x,y) || (\Ez: P(x,z) && p(z,y) && \Ez: p(x,z) && O(z,y)). Tämä siis vain postuloi, että on olemassa predikaatti joka on tosi tasan silloin kun... jne. Tämä osakaava karakterisoi jälleen transitiivisen sulkeuman.
Tällä operaattorilla voidaan tehdä jo paljon muutakin. Esimerkiksi, voidaan karakterisoida graafissa ns. klikki. Jos p(x,y) on (suuntaamaton) kaarirelaatio, niin \E P(x): \Ax \Ay: (P(x) && P(y)) => p(x,y) && \Ay (\Ax: P(x) => p(x,y)) => P(y). Tämä on tosi predikaatille P(x), jos ja vain jos P(x) on tosi maksimaalisessa sellaisessa joukossa jonka kaikkien solmujen välillä on kaari. Tämän lisäksi täytyy voida jotenkin sanoa että P(x) pätee vähintään jollekin tietylle määrälle alkioita, sivuutan sen tässä teknisenä yksityiskohtana, toivon että lukija luottaa minuun tässä.
On siis mahdollista spesifioida tällä SO[E]-loogikalla se, että graafissa on tietyn kokoinen klikki. Tämä taas on tunnettu NP-täydellinen ongelma, joten SO[E] karakterisoi luokan joka on vähintään NP.
Pienen pohdinnan jälkeen oivalletaan, että jokainen SO[E]-luokan kaava joka on tosi annetulle struktuurille, voidaan osoittaa todeksi ensin arvaamalla tarkalleen milloin nämä uudet predikaatit ovat tosia. Koska jokaisen predikaatin määrittelyssä on jokin vakiomäärä parametrejä (esim k), ja koska syötteenä saadussa struktuurissa on alkioita joihin muuttuja voi viitata vain korkeintaan n kappaletta, on predikaatin totuusarvojoukko kooltaan korkeintaan n^k. Voimme siis arvaamalla nämä uudet predikaatit luoda polynomisessa ajassa FO-kaavan, jonka päteminen alkuperäiselle struktuurille on helppo todeta. Tiedämme siis, että SO[E] = NP.
Kompleksisuushierarkiassa on tästä kompleksisempiakin luokkia, ja lisäksi P-luokan sisällä on paljon alaluokkia. Mutta idea tulee ehkä jo tästä selväksi.
Tehtävämme on siirrellä taulukon alkioita siten, että siirtelyn jälkeen taulukko on järjestyksessä. Tämä tarkoittaa sitä, että jokaisella kokonaisluvulla i välillä 1 < i < n+1 pätee että A[i-1] < A[i]. Tämä ei siis päde alussa. Meillä on käytössämme kaksi operaatiota, V(i,j), joka vaihtaa taulukon alkiot i ja j keskenään, sekä vertailuoperaatio A[i] < A[j].
Emme nyt keskustele siitä, miten tarkalleenottaen toteutamme taulukon järjestämisen. Oletamme että taulukko on alussa täysin sekaisin, emmekä tiedä mitään esimerkiksi siitä, mitä arvoja taulukossa on ja miten ne ovat jakautuneet. Voimme ilmaista taulukon järjestämisen permutaation etsimisenä, ja tarkastelemme ongelman kompleksisuutta tästä näkökulmasta.
Koska alkiot ovat erisuuria, on keskenään erilaisia tapoja laittaa alkiot taulukkoon n! kappaletta, missä n! = 1*2*...*n. Tämä tulee siitä, että ensimmäinen alkio voi olla mikä hyvänsä n:stä alkiosta, tämän jälkeen toinen voi olla mikä hyvänsä jäljellä olevista, jne. Näistä n!-kappaleesta permutaatioita meidän tulee löytää se, joka vastaa taulkon järjestyksessä olemista.
Jokainen vertailu, jonka taulukolle teemme, paljastaa meille jotain siitä, minkälaisen permutaation tarvitsemme. Tarkalleenottaen, kaikkien vielä mahdollisten permutaatioiden joukosta yksi vertailu sulkee pois tarkalleen puolet. Nimittäin, vertaamalla A[i] < A[j], (missä i < j) tulos on "kyllä" tasan silloin kun nämä alkiot ovat oikeassa järjestyksesä ja "ei" silloin kun oikeassa permutaatiossa ne ovat eri järjestyksessä. Muuta informaatiota emme yksittäisestä vertailusta (yleisessä tapauksessa) saa. Yhden vertailun (ja mahdollisen vaihdon) jälkeen permutaatiota on jäljellä n!/2, ja jokainen vertailu vastaavasti puolittaa permutaatioiden määrän. Tätä puolittamista on pahimmassa tapauksessa jatkettava kunnes permutaatioita on enää yksi. Tiedämme, että tällöin olemme tehneet log(n!) puolitusta. log(n!) on suunnilleen n*log(n), mikä tarkoittaa, että pahimmassa tapauksessa taulukon järjestämiseksi täytyy tehdä (osapuilleen) tämän verran vertailuja ja vaihtoja.
Tämä on yksinkertaisimpia analyysejä joilla voidaan tarkastella miten kompleksinen jokin ongelma on; tämä paljasti siis, että taulukon järjestäminen ei onnistu (aivan) suoraan taulukon kokoon verrannollisessa ajassa.
Vaikeampien kysymysten analysoiminen on usein -- niin -- vaikeampaa. Deskriptiivinen kompleksisuusteoria on teoria, joka yksittäisten ongelmien kompleksisuuden sijaan pyrkii luokittelemaan ongelmia sen mukaan, millä tavoin ne ovat ilmaistavissa. Oletetaan, että meillä on syötteenä jokin struktuuri ja jollakin logiikalla ilmaistu ominaisuus, ja tehtävänä on selvittää, onko annetulla struktuurilla tämä ominaisuus. Ongelman vaikeus riippuu siitä, millaisia ilmaisutapoja logiikassa on käytössä.
Esimerkiksi, jos meillä on annettu syötteenä graafi (eli suomeksi "verkko", mutta käytän tätä termiä välttääkseni sekaannusta) ja jokin ensimmäisen kertaluvun predikaattilogiikan kaava ja annettu joukko predikaatteja, voimme itseasiassa hyvinkin helposti tarkastaa onko kaava tosi. Tässä siis oletamme, että nämä predikaatit todella on annettu, eli pystymme suoraan laskemaan niiden arvon mille tahansa alkioille. Esimerkiksi "Kaikille solmuille x,y, pätee että niiden välillä on kaari" Tai "on olemassa solmut x, y, z siten, että (x,y) on kaari ja (y,z) on kaari".
Tätä ei pidä sekoittaa siis sellaiseen tilanteeseen jossa on annettu kaava, ja pitää selvittää päteekö kyseinen kaava ylipäätään jollekin mallille, eikä myöskään tilanteeseen, jossa predikaattien arvoja ei tunneta, ja pitäisi tietää voidaanko predikaateille antaa sellainen tulkinta, jolla kaava pätee annetulle struktuurille.
Ongelmat, jotka on ilmaistavissa tällä tavalla, ovat luokassa FO (sanoista First Order), ja deskriptiivisen kompleksisuusteorian yksi tulos on, että tämä luokka on sama kuin AC0, joka puolestaan tarkoittaa ongelmia jotka voidaan ratkaista hyvin tehokkaasti; Jokaiselle tällaiselle ominaisuudelle on olemassa hierarkia ongelman ratkaisevia logiikkapiirejä, joiden syvyys (perättäisten porttien määrä) on rajoitettu. On huomattava, että tämän luokan yksittäisen ongelman karakterisoi nimenomaan yksittäinen predikaattilogiikan kaava (joka kullekin ongelmalle on kiinteä), ja mahdollisten struktuurien joukko.
FO ongelmat eivät ole esimerkiksi graafeille kovin mielenkiintoisia, koska vaikkapa kysymystä "Onko kahden annetun solmun välillä polku" ei voidan ilmaista ensimmäisen kertaluvun predikaattilogiikalla.
Jos haluamme nimittäin karakterisoida jälkimmäisen tapauksen, niin tarvitsemme toisen kertaluvun logiikkaa. Täysi toisen kertaluvun logiikka antaa meille mahdollisuuden ilmaista esimerkiksi sen, että "on olemassa predikaatti P(x,y) siten, että...". Aivan vielä emme kuitenkaan ota näin vahvaa ilmaisuvoimaa mukaan.
Transitiivinen sulkeuma on operaatio, jonka lisääminen FO:iin tuo sopivasti ilmaisuvoimaa. Esimerkiksi, jos syötteenä on suunnattu graafi, niin meillä on automaattisesti käytössämme predikaatti p(x,y), joka sanoo että solmusta x on solmuun y vievä kaari. Lisäämme logiikkaamme operaattorin TC, joka toimii siten, että jos Q(x,y) on osakaava jossa on kaksi vapaata muuttujaa, niin TC(Q)(x,y) määrittelee tämän osakaavan Transitiivisen sulkeuman. Sen totuusarvo käyttäytyy seuraavalla tavalla: TC(Q(x,y)) tulkitaan itseasiassa siten, että joko Q(x,y) pätee, tai pitää löytyä jokin ei-tyhjä jono alkioita z1, z2, ..., zk siten, että Q(x,z1) pätee, Q(z1,z2) pätee, jne, ja Q(zk, y) pätee.
FO[TC] on niiden ongelmien joukko, jotka voidaan ilmaista käyttäen ensimmäisen kertaluvun logiikkaa ja transitiivista sulkeumaa. Esimerkiksi "Graafissa on polku solmusta s solmuun t" on ilmaistavissa tällä; jos p(x,y) on (annettu) predikaatti, joka pätee kun on kaari solmusta x solmuun y, niin polku solmusta s solmuun t on olemassa, jos pätee TC(p)(s,t). Tämä kompleksisuusluokka on sama kuin luokka NL, joka on niiden ongelmien luokka, jotka voidaan ratkaista "arvaamalla" ratkaisu askel kerrallaan ilman että koko ratkaisua täytyy muistaa.
Least fixpoint, eli pienimmän kiintopisteen operaattori taas mahdollistaa yksinkertaisen rekursiivisen ilmaisun, jolla määritellään uusi predikaatti. Muistutan tässä kohtaa, että olemassaolevat predikaatit ovat kiinteitä ja tunnettuja; TC yllä mahdollisti "uuden" predikaatin luomisen vanhojen predikaattien avulla hyvin yksinkertaisesti. LFP-operaattori on jo selvästi monimutkaisempi. Luodaksemme "toisen kertaluvun" predikaatin P -- eli predikaatin jonka tulkinta ei ole kiinnitetty -- ilmaisemme sen muodossa LFP(Q(P,x)) Tässä siis LFP-operaattorin sisään tulee kaava Q, jossa käytetään predikaattia P, muuttujia x ja olemassaolevia predikaatteja. Tämä tulkitaan tarkoittavan "pienintä" sellaista predikaattia P, joka toteuttaa kaavan P(x) = Q(P(x),x) kaikilla x; Rajoituksena on, että P(x) ei saa esiintyä negatiivisena kaavassa Q (so. kun kaava Q kirjoitetaan konjunktiiviseen normaalimuotoon, P:n negaatio ei saa esiintyä kaavassa).
Esimerkiksi relaation p(x,y) transitiivinen sulkeuma voidaan ilmaista LFP-operaattorilla kaavasta LFP(p(x,y) || \exists z: P(x,z) && p(z,y)). Eli, P(x,y) on p:n transitiivinen sulkeuma, kun se on "pienin" relaatio joka toteuttaa em rekursiivisen määritelmän. Pienin tässä yhteydessä tarkoittaa, että se joukko pareja, joka yhtälön toteuttaa, on minimaalinen; mikään sen aito osajoukko ei voisi toteuttaa yhtälöä. FO[LFP] = P, eli polynomisessa ajassa ratkeavat ongelmat ovat karakterisoitavissa LFP-operaattorilla rikastetussa ensimmäisen kertaluvun predikaattilogiikassa. Tämä teoreema on hankalahko todistaa, joten en tässä ala sitä nyt käymään läpi.
Jos siirrymme toisen kertaluvun logiikkaan "aidosti", eli sallimme uusien predikaattimuuttujien esittelyn, mutta rajoitumme eksistentiaaliseen kvantifiointiin, saamme mielenkiintoisen luokan, SO[E]. Tässä siis on kyse ensimmäisen kertaluvun logiikasta, jossa saa luoda predikaattimuuttujia, kunhan ne on sidottu olemassaolokvanttorilla. Käytän tässä merkintää \E, koska en jaksa kaivaa symboleja.
Tällöin voidaan sanoa vaikkapa että \E(P(x,y): P(x,y) <=> (p(x,y) || (\Ez: P(x,z) && p(z,y) && \Ez: p(x,z) && O(z,y)). Tämä siis vain postuloi, että on olemassa predikaatti joka on tosi tasan silloin kun... jne. Tämä osakaava karakterisoi jälleen transitiivisen sulkeuman.
Tällä operaattorilla voidaan tehdä jo paljon muutakin. Esimerkiksi, voidaan karakterisoida graafissa ns. klikki. Jos p(x,y) on (suuntaamaton) kaarirelaatio, niin \E P(x): \Ax \Ay: (P(x) && P(y)) => p(x,y) && \Ay (\Ax: P(x) => p(x,y)) => P(y). Tämä on tosi predikaatille P(x), jos ja vain jos P(x) on tosi maksimaalisessa sellaisessa joukossa jonka kaikkien solmujen välillä on kaari. Tämän lisäksi täytyy voida jotenkin sanoa että P(x) pätee vähintään jollekin tietylle määrälle alkioita, sivuutan sen tässä teknisenä yksityiskohtana, toivon että lukija luottaa minuun tässä.
On siis mahdollista spesifioida tällä SO[E]-loogikalla se, että graafissa on tietyn kokoinen klikki. Tämä taas on tunnettu NP-täydellinen ongelma, joten SO[E] karakterisoi luokan joka on vähintään NP.
Pienen pohdinnan jälkeen oivalletaan, että jokainen SO[E]-luokan kaava joka on tosi annetulle struktuurille, voidaan osoittaa todeksi ensin arvaamalla tarkalleen milloin nämä uudet predikaatit ovat tosia. Koska jokaisen predikaatin määrittelyssä on jokin vakiomäärä parametrejä (esim k), ja koska syötteenä saadussa struktuurissa on alkioita joihin muuttuja voi viitata vain korkeintaan n kappaletta, on predikaatin totuusarvojoukko kooltaan korkeintaan n^k. Voimme siis arvaamalla nämä uudet predikaatit luoda polynomisessa ajassa FO-kaavan, jonka päteminen alkuperäiselle struktuurille on helppo todeta. Tiedämme siis, että SO[E] = NP.
Kompleksisuushierarkiassa on tästä kompleksisempiakin luokkia, ja lisäksi P-luokan sisällä on paljon alaluokkia. Mutta idea tulee ehkä jo tästä selväksi.
torstai 31. heinäkuuta 2014
Logiikka ja laskenta.
Olettakaamme että olemme tutkimassa jonkinlaisen systeemin S käyttäytymistä. Systeemissä on erilaisia muuttujia, joita voimme ehkä mitata, emme ehkä täydellisesti mutta voimme kuitenkin saada jotain tietoa. Oletetaan että nämä muuttujat ilmaistaan symbolilla x. Tämä on siis periaatteessa vektori kaikesta siitä, mikä systeemissä on olennaista. Oletan tässä että meillä on lisäksi käsite aika, joka on yksi muuttuja, mutta yksinkertaisuuden vuoksi oletan että se ei ole mukana mainitussa x:ssä.
Systeemin tila on jollakin ajanhetkellä muuttujan x arvo. Jos tunnemme systeemin tilan kahtena ajanhetkenä, niin oletamme että systeemi on siirtynyt ensimmäisestä tilasta toiseen; se, miten systeemi siirtyy tilasta toiseen, määrittää systeemin dynamiikan. Melko yleisiä systeemien dynamiikan kuvaamiseen käytettyjä formalismeja ovat esimerkiksi differentiaaliyhtälöt. Jos x koostuu komponenteista x1, x2, ..., xn, niin meillä on tyypillisesti useampia differentiaaliyhtälöitä jotka kuvaavat sitä miten muuttujien kehitys ajan suhteen riippuu toisistaan. Esimerkiksi voisi olla vaikkapa kahden muuttujan systeemi, jossa x1' = x2 ja x2' = -x1. Tämä on hyvin yksinkertainen systeemi, jossa siis x1 kasvaa sitä nopeammin mitä suurempi x2 on ja x2 taas pienenee sitä nopeammin mitä suurempi x1 on; tällainen systeemi on oskilloiva, mutta se ei nyt ole olennaista.
Differentiaaliyhtälöillä kuvataan järjestelmiä, jotka ovat jatkuvia. Jatkuvuus viittaa siis siihen, että aika etenee tasaista tahtia ja muuttujat ovat tyypillisesti reaali- tai kompleksilukuja. Differentiaaliyhtälöillä kuvataan lisäksi järjestelmiä jotka ovat deterministisiä, eli niiden toiminta on tarkalleen määrätty kun tila tunnetaan. Deterministisen sijaan järjestelmä voi olla esimerkiksi stokastinen, jolloin sen toimintaan liittyy jokin satunnainen komponentti, esimerkiksi differentiaaliyhtälössä voi esiintyä satunnaismuuttujia, jolloin saatu yhtälö ei kuvaakaan järjestelmän tilaa ajan funktiona vaan ainoastaan tilan jakaumaa. Kolmas vaihtoehto on, että järjestelmä on epädeterministinen, mikä tarkoittaa että sillä on aidosti useita eri polkuja; tätä käytetään erotuksena stokastisesta siten, että epädeterminismi tulee esimerkiksi mukaan malliin tuntemattomien vuorovaikutusten kautta.
Jatkuvan sijaan järjestelmä voi olla myös diskreetti. Diskreetin järjestelmän tilan määrittämät muuttujat saavat diskreettejä arvoja kuten kokonaisluku- tai boolean arvoja (tosi/epätosi). Järjestelmää jossa on sekä diskreettejä että jatkuvia muuttujia nimitetään hybridijärjestelmiksi. Diskreetin järjestelmän dynamiikkaa voidaan aina kuvat tilasiirtymärelaatiolla, joka kertoo mihin muihin tiloihin jostakin tietystä tilasta voidaan päätyä. Tämä relaatio on funktio jos järjestelmä ei ole epädeterministinen, ja jos järjestelmä on stokastinen, niin funktion arvoina ovat jakaumat tilojen yli.
Predikaattiabstraktio viittaa siihen, että osa muuttujista korvataan predikaateilla. Predikaatti on totuusarvoinen väittämä joka koskee muuttujaa tai muuttujajoukkoa. Esimerkiksi jos meillä on muuttujat x ja y, niin väittämät x < y, x+y > 3, x < 0 jne ovat predikaatteja jotka puhuvat muuttujista x ja y. Tyypillisesti jos me käsittelemme jatkuvaa järjestelmää, predikaattiabstraktio on yksi tapa muuttaa järjestelmä diskreetiksi. Jos esimerkiksi x ja y ovat jatkuvia muuttujia, järjestelmän tilaa saatettaisiin abstrahoida esittämällä se kolmen predikaatin avulla: x < 0, y < 0 ja x2 + y2 < 9. Tällöin meillä olisi kahdeksan erilaista "tilaa" sen mukaan, missä kvadrantissa x ja y ovat ja sen mukaan ovatko ne 3-säteisen ympyrän sisällä vai eivät. Predikaattiabstraktio tuottaa epädeterminismiä vaikka alkuperäinen järjestelmä olisi kuvattu deterministisellä differentiaaliyhtälöllä. Esimerkiksi kun x = 5 ja y = 1, järjestelmä kehittyy niin, että y muuttuu negatiiviseksi, mutta pysyy ympyrän ulkopuolella ja kun x = 1 ja y = 5, y pienenee mutta pysyy positiivisena niin, että järjestelmä siirtyy ympyrän sisäpuolelle. Kumpikin arvoiyhdistelmä on kuitenkin mainittujen predikaattien kannalta "sama", eli abstraktio samastaa eri tavoin käyttäytyviä tiloja.
Jos tunnemme järjestelmän "riittävän hyvin" ja meillä on "riittävän hyvät" abstraktiot siten, että laadullisesti abstraktion tuottama malli kertoo meille "riittävästi", voimme luoda järjestelmän toiminnasta diskreetin mallin ja ennustaa, onko alkuperäisellä systeemillä jokin tietty abstrakti tila johon se päätyisi. Esimerkiksi voiko käydä niin, että sekä x että y ovat negatiivisia ja ympyrän ulkopuolella.
Sivuutan tässä nyt sen problematiikan joka liittyy tilasiirtymärelaation esittämiseen. Huomautan lisäksi että yleisessä tapauksessa tällaiset abstraktiot sisältävät potentiaalisesti satoja tai tuhansia predikaatteja siten, että järjestelmän diskreettienkin tilojen määrä on suurempi kuin koko maailmankaikkeudessa olevien atomien määrä; tällaisen järjestelmän kaikkien tilojen tutkiminen on yksinkertaisesti mahdotonta.
Voimme kuitenkin käyttää tähän logiikkaa, niin erikoiselta kuin se kuulostaakin. Yksi takavuosien menestyksekäs metodi oli niin kutsuttu rajoitettu mallintarkastus eli bounded model checking. Sen ideana on, että me esitämme järjestelmän alkutilan predikaattien avulla, esimerkiksi p1 & p2 & not p3 jne. Tämän lisäksi esitämme tilasiirtymärelaation logiikan kaavana siten, että jos tämänhetkisessä tilassa puhutaan predikaatista p, niin jälkimmäisessä puhutaan predikaatista p'. Esimerkiksi jos p on predikaatti joka vaihtaa totuusarvoaan jokaisessa siirtymässä, tätä merkitään p -> p', joka taas sievenee muotoon not p or p'.
Oletetaan, että "virheellinen tila" voidaan ilmaista kaavalla Y. Jos meillä on jotakin tilajoukkoa kuvaava kaava X ja tilasiirtymän kaava P( ), niin sitä tilajoukkoa joka saavutetaan joukosta X käsin, voidaan ilmaista P(X). (Tämä on siis taas kaava). Kaikki predikaatit esiintyvät tässä kaavassa (se voi olla hyvinkin suuri) pelkkinä propositioina. alkutilan ollessa x, tarkistamme onko kaava X = (x tai P(x) tai P(P(x)) tai ....) yhdessä kaavan Y kanssa mahdollista tehdä todeksi, eli onko kyseinen kaava X ja Y satisfiable eli SAT. Valitettavasti X voi kuvata vain äärellisen määrän askelia (siitä nimitys "bounded") joten tämä menetelmä voi kyllä löytää virheitä, muttei voi todistaa että järjestelmässä ei sellaisia ole.
SAT on NP-täydellinen ongelma, mutta modernit SAT-ratkaisijat ovat niin tehokkaita, ja todellisista järjestelmistä peräisin olevat mallit ovat niin strukturoituja että SAT-ratkaisijat kykenevät ratkomaan tuhansien ja jopa miljoonien klausuulien mittaisia kaavoja, joissa on kymmeniä tuhansia tai satoja tuhansia muuttujia. Toki on aina patologisia tapauksia jotka tyystin tukahduttavat ratkaisijat, mutta ne ovat todellisen maailman malleissa hyvin harvinaisia.
Meidän ei ole kuitenkaan aivan pakko tyytyä siihen ettemme koskaan saisi todistettua järjestelmää täysin oikeaksi. On nimittäin mahdollista toisinaan löytää induktiivisia invariantteja jos sovelletaan abstraktiota luovasti.
Ensimmäinen, yksinkertainen tapa on yrittää löytää ns kiintopiste. Jos kaava X kuvaa kaikkia niitä tiloja joihin voidaan päästä n:llä tai sitä pienemmällä määrällä askelia, ja jos kaava (P(X) tai X) on yhtäpitävä kaavan X kanssa, tiedämme, että kaava X itseasissa kuvaa jo kaikki mahdolliset saavutettavat tilat; jos kaava (X ja Y) on ristiriitainen, ei järjestelmä voi saavuttaa tilaa jossa Y pätee.
Tällainen kiintopiste voi olla kuitenkin niin monen askeleen päässä -- tai mikä pahempaa, järjestelmällä voi olla ääretön määrä mahdollisia tiloja (mikä tosin ei ole mahdollista jos käytämme tiukkaa predikaattiabstraktiota, mutta sivuutan sen nyt) -- että meiltä loppuu muisti tai aika ennenkuin löydämme kiintopisteen. Jos olemme nyt -- jonkin askelmäärän jälkeen -- todenneet että X kuvaa siihen mennessä saavutettavia tiloja, ja X ja Y ei ole SAT, voimme aina löytää tälle kaavalle niinsanotun interpolantin. Interpolantti on kaava Z, joka sisältää vain X:lle ja Y:lle yhteisiä symboleja, X implikoi Z:n ja Z on ristiriidassa Y:n kanssa.
Interpolantti Z voidaan nyt abstrahoida, siis tehdä siitä heikompi, kunhan se on edelleen ristiriidassa Y:n kanssa. Jos tätä merkitään kaavalla Z' niin sopivalla abstraktion valinnalla saatamme esimerkiksi pystyä osoittamaan että kaava Z' onkin kiintopiste -- se on siis induktiivinen invariantti, kaava joka kerran todeksi tultuaan pätee vaikka tekisimme kuinka tilasiirtymiä. Jos tällainen abstraktio löydetään, olemme kertakaikkisesti osoittaneet että Y ei voi toteutua järjestelmässä.
Systeemin tila on jollakin ajanhetkellä muuttujan x arvo. Jos tunnemme systeemin tilan kahtena ajanhetkenä, niin oletamme että systeemi on siirtynyt ensimmäisestä tilasta toiseen; se, miten systeemi siirtyy tilasta toiseen, määrittää systeemin dynamiikan. Melko yleisiä systeemien dynamiikan kuvaamiseen käytettyjä formalismeja ovat esimerkiksi differentiaaliyhtälöt. Jos x koostuu komponenteista x1, x2, ..., xn, niin meillä on tyypillisesti useampia differentiaaliyhtälöitä jotka kuvaavat sitä miten muuttujien kehitys ajan suhteen riippuu toisistaan. Esimerkiksi voisi olla vaikkapa kahden muuttujan systeemi, jossa x1' = x2 ja x2' = -x1. Tämä on hyvin yksinkertainen systeemi, jossa siis x1 kasvaa sitä nopeammin mitä suurempi x2 on ja x2 taas pienenee sitä nopeammin mitä suurempi x1 on; tällainen systeemi on oskilloiva, mutta se ei nyt ole olennaista.
Differentiaaliyhtälöillä kuvataan järjestelmiä, jotka ovat jatkuvia. Jatkuvuus viittaa siis siihen, että aika etenee tasaista tahtia ja muuttujat ovat tyypillisesti reaali- tai kompleksilukuja. Differentiaaliyhtälöillä kuvataan lisäksi järjestelmiä jotka ovat deterministisiä, eli niiden toiminta on tarkalleen määrätty kun tila tunnetaan. Deterministisen sijaan järjestelmä voi olla esimerkiksi stokastinen, jolloin sen toimintaan liittyy jokin satunnainen komponentti, esimerkiksi differentiaaliyhtälössä voi esiintyä satunnaismuuttujia, jolloin saatu yhtälö ei kuvaakaan järjestelmän tilaa ajan funktiona vaan ainoastaan tilan jakaumaa. Kolmas vaihtoehto on, että järjestelmä on epädeterministinen, mikä tarkoittaa että sillä on aidosti useita eri polkuja; tätä käytetään erotuksena stokastisesta siten, että epädeterminismi tulee esimerkiksi mukaan malliin tuntemattomien vuorovaikutusten kautta.
Jatkuvan sijaan järjestelmä voi olla myös diskreetti. Diskreetin järjestelmän tilan määrittämät muuttujat saavat diskreettejä arvoja kuten kokonaisluku- tai boolean arvoja (tosi/epätosi). Järjestelmää jossa on sekä diskreettejä että jatkuvia muuttujia nimitetään hybridijärjestelmiksi. Diskreetin järjestelmän dynamiikkaa voidaan aina kuvat tilasiirtymärelaatiolla, joka kertoo mihin muihin tiloihin jostakin tietystä tilasta voidaan päätyä. Tämä relaatio on funktio jos järjestelmä ei ole epädeterministinen, ja jos järjestelmä on stokastinen, niin funktion arvoina ovat jakaumat tilojen yli.
Predikaattiabstraktio viittaa siihen, että osa muuttujista korvataan predikaateilla. Predikaatti on totuusarvoinen väittämä joka koskee muuttujaa tai muuttujajoukkoa. Esimerkiksi jos meillä on muuttujat x ja y, niin väittämät x < y, x+y > 3, x < 0 jne ovat predikaatteja jotka puhuvat muuttujista x ja y. Tyypillisesti jos me käsittelemme jatkuvaa järjestelmää, predikaattiabstraktio on yksi tapa muuttaa järjestelmä diskreetiksi. Jos esimerkiksi x ja y ovat jatkuvia muuttujia, järjestelmän tilaa saatettaisiin abstrahoida esittämällä se kolmen predikaatin avulla: x < 0, y < 0 ja x2 + y2 < 9. Tällöin meillä olisi kahdeksan erilaista "tilaa" sen mukaan, missä kvadrantissa x ja y ovat ja sen mukaan ovatko ne 3-säteisen ympyrän sisällä vai eivät. Predikaattiabstraktio tuottaa epädeterminismiä vaikka alkuperäinen järjestelmä olisi kuvattu deterministisellä differentiaaliyhtälöllä. Esimerkiksi kun x = 5 ja y = 1, järjestelmä kehittyy niin, että y muuttuu negatiiviseksi, mutta pysyy ympyrän ulkopuolella ja kun x = 1 ja y = 5, y pienenee mutta pysyy positiivisena niin, että järjestelmä siirtyy ympyrän sisäpuolelle. Kumpikin arvoiyhdistelmä on kuitenkin mainittujen predikaattien kannalta "sama", eli abstraktio samastaa eri tavoin käyttäytyviä tiloja.
Jos tunnemme järjestelmän "riittävän hyvin" ja meillä on "riittävän hyvät" abstraktiot siten, että laadullisesti abstraktion tuottama malli kertoo meille "riittävästi", voimme luoda järjestelmän toiminnasta diskreetin mallin ja ennustaa, onko alkuperäisellä systeemillä jokin tietty abstrakti tila johon se päätyisi. Esimerkiksi voiko käydä niin, että sekä x että y ovat negatiivisia ja ympyrän ulkopuolella.
Sivuutan tässä nyt sen problematiikan joka liittyy tilasiirtymärelaation esittämiseen. Huomautan lisäksi että yleisessä tapauksessa tällaiset abstraktiot sisältävät potentiaalisesti satoja tai tuhansia predikaatteja siten, että järjestelmän diskreettienkin tilojen määrä on suurempi kuin koko maailmankaikkeudessa olevien atomien määrä; tällaisen järjestelmän kaikkien tilojen tutkiminen on yksinkertaisesti mahdotonta.
Voimme kuitenkin käyttää tähän logiikkaa, niin erikoiselta kuin se kuulostaakin. Yksi takavuosien menestyksekäs metodi oli niin kutsuttu rajoitettu mallintarkastus eli bounded model checking. Sen ideana on, että me esitämme järjestelmän alkutilan predikaattien avulla, esimerkiksi p1 & p2 & not p3 jne. Tämän lisäksi esitämme tilasiirtymärelaation logiikan kaavana siten, että jos tämänhetkisessä tilassa puhutaan predikaatista p, niin jälkimmäisessä puhutaan predikaatista p'. Esimerkiksi jos p on predikaatti joka vaihtaa totuusarvoaan jokaisessa siirtymässä, tätä merkitään p -> p', joka taas sievenee muotoon not p or p'.
Oletetaan, että "virheellinen tila" voidaan ilmaista kaavalla Y. Jos meillä on jotakin tilajoukkoa kuvaava kaava X ja tilasiirtymän kaava P( ), niin sitä tilajoukkoa joka saavutetaan joukosta X käsin, voidaan ilmaista P(X). (Tämä on siis taas kaava). Kaikki predikaatit esiintyvät tässä kaavassa (se voi olla hyvinkin suuri) pelkkinä propositioina. alkutilan ollessa x, tarkistamme onko kaava X = (x tai P(x) tai P(P(x)) tai ....) yhdessä kaavan Y kanssa mahdollista tehdä todeksi, eli onko kyseinen kaava X ja Y satisfiable eli SAT. Valitettavasti X voi kuvata vain äärellisen määrän askelia (siitä nimitys "bounded") joten tämä menetelmä voi kyllä löytää virheitä, muttei voi todistaa että järjestelmässä ei sellaisia ole.
SAT on NP-täydellinen ongelma, mutta modernit SAT-ratkaisijat ovat niin tehokkaita, ja todellisista järjestelmistä peräisin olevat mallit ovat niin strukturoituja että SAT-ratkaisijat kykenevät ratkomaan tuhansien ja jopa miljoonien klausuulien mittaisia kaavoja, joissa on kymmeniä tuhansia tai satoja tuhansia muuttujia. Toki on aina patologisia tapauksia jotka tyystin tukahduttavat ratkaisijat, mutta ne ovat todellisen maailman malleissa hyvin harvinaisia.
Meidän ei ole kuitenkaan aivan pakko tyytyä siihen ettemme koskaan saisi todistettua järjestelmää täysin oikeaksi. On nimittäin mahdollista toisinaan löytää induktiivisia invariantteja jos sovelletaan abstraktiota luovasti.
Ensimmäinen, yksinkertainen tapa on yrittää löytää ns kiintopiste. Jos kaava X kuvaa kaikkia niitä tiloja joihin voidaan päästä n:llä tai sitä pienemmällä määrällä askelia, ja jos kaava (P(X) tai X) on yhtäpitävä kaavan X kanssa, tiedämme, että kaava X itseasissa kuvaa jo kaikki mahdolliset saavutettavat tilat; jos kaava (X ja Y) on ristiriitainen, ei järjestelmä voi saavuttaa tilaa jossa Y pätee.
Tällainen kiintopiste voi olla kuitenkin niin monen askeleen päässä -- tai mikä pahempaa, järjestelmällä voi olla ääretön määrä mahdollisia tiloja (mikä tosin ei ole mahdollista jos käytämme tiukkaa predikaattiabstraktiota, mutta sivuutan sen nyt) -- että meiltä loppuu muisti tai aika ennenkuin löydämme kiintopisteen. Jos olemme nyt -- jonkin askelmäärän jälkeen -- todenneet että X kuvaa siihen mennessä saavutettavia tiloja, ja X ja Y ei ole SAT, voimme aina löytää tälle kaavalle niinsanotun interpolantin. Interpolantti on kaava Z, joka sisältää vain X:lle ja Y:lle yhteisiä symboleja, X implikoi Z:n ja Z on ristiriidassa Y:n kanssa.
Interpolantti Z voidaan nyt abstrahoida, siis tehdä siitä heikompi, kunhan se on edelleen ristiriidassa Y:n kanssa. Jos tätä merkitään kaavalla Z' niin sopivalla abstraktion valinnalla saatamme esimerkiksi pystyä osoittamaan että kaava Z' onkin kiintopiste -- se on siis induktiivinen invariantti, kaava joka kerran todeksi tultuaan pätee vaikka tekisimme kuinka tilasiirtymiä. Jos tällainen abstraktio löydetään, olemme kertakaikkisesti osoittaneet että Y ei voi toteutua järjestelmässä.
torstai 14. marraskuuta 2013
Äärettömyys.
Usein esitetty filosofinen ongelma logiikan ja matematiikan suhteen on se, miten äärettömyyteen pitäisi suhtautua. Emme oikeastaan edes tiedä mitä tarkalleenottaen äärettömyydellä tarkoitetaan, ellemme määrittele sitä jotenkin. Lähdetään siis perusteista.
Lähdetään ensimmäisen kertaluvun kielestä, jossa emme nyt rajoita sen kummemmin ilmaisua. Oletetaan että voimme sanoa jotain sellaista että "a = b", ilmaistaksemme identiteettiä. Termit a ja b siis viittaavat "johonkin" ja identiteetti tarkoittaa että ne viittaavat samaan. Jos sanomme, että "ei a=b", niin sanomme, että a ja b eivät ole identtisiä. Ilmaisen tämän "a != b" Tällainen termi, ollessaan totta, ilmaisee jo (implisiittisesti) lukumäärää: Se sanoo että ainakin kaksi termiä viittaa eri asioihin.
Tästä erillisyydestä voimme jalostaa eräänlaisen äärettömyyden seuraavalla tavalla. Tarkastellaan binääristä relaatiota R, joka ilmaisee a:n ja b:n suhdetta. Sovitaan että R:llä on seuraavat ominaisuudet: 1. Jos R(a,b) pätee ja R(b,a) pätee, niin a = b. 2. Jos R(a,b) pätee, ja R(b,c) pätee,
niin R(a,c) pätee. 3. Jokaiselle alkiolle x on olemassa alkio y siten että x != y ja R(x,y) pätee.
Tälle relaatiolle ei ole olemassa äärellistä mallia. Nimittäin, jos mallissamme on äärellinen määrä - olkoon se mikä hyvänsä, esimerkiksi 3 - alkioita, voimme valita niistä yhden - minkä tahansa - ja merkitä tätä symbolilla "0". On olemassa alkio x, joka on erisuuri kuin 0, siten, että R(0,x) pätee. Toisaalta, ei voi päteä että R(x,0), koska tällöin x = 0 pätisi ominaisuuden 1 nojalla. Sovelletaan kohtaa 3 alkioon x, saamme uuden alkion, y. Edelleen, voimme kohdan 2 ja 1 nojalla toteamme, että myös y !=0. Itseasiassa, joka kerta kun sovellamme kohtaa 3, saamme alkion, jota emme ole vielä kohdanneet. Mutta jos mallissamme oli kolme alkiota, niin kolmas yritys soveltaa kohtaa 3 johtaa ristiriitaan: Uuden alkion pitää olla erisuuri kuin 0, x, tai y, koska 3:n kohdan nojalla se ei ole y, ja jos se olisi x, niin R(x,y):stä seuraisi kohdan 1 nojalla, että se uusi alkio olisi y, mikä on ristiriita. Ja jos uusi alkio olisi 0, niin kohdan 2 nojalla uusi alkio olisi taas x, mikä ei ole mahdollista.
Äärellisen mallin olettaminen johtaa siis väistämättä ristiriitaan. Tiukan finitistinen tulkinta matematiikasta sanoisi, että hyvä on, tämä tarkoittaa että alkuperäinen ominaisuuksien joukko on väistämättä ristiriitainen. Tämä vastaisi siis sellaista joukko-opin aksiomatisointia joka sanoisi että kaikki joukot ovat äärellisiä.
Mutta tämä johtaa ongelmiin sekin. Esimerkiksi, jos oletamme, että luonnollisten lukujen joukko on hyvin määritelty käsite, ja otamme relaation R(x,y) tarkoittamaan "y = x +1", niin luonnollisten lukujen joukko *on* malli R:lle, siis, tämä relaatio toteuttaa R:n ominaisuudet. Se on siis ääretön.
Luonnollisten lukujen joukkoa pidetään eräänlaisena standardimallina sille, mitä normaali aritmetiikka tarkoittaa. Tässä viittaan siis sellaisiin asioihin kuin "lukuteoria" tms, jossa on kyse siis yhteen- ja kertolaskusta ja niistä johdetuista operaatioista. Sitä voidaan pitää lukumäärien teorian standardimallina. Luonnollisten lukujen kanssa isomorfista(*) joukkoa nimitetään sanotaan numeroituvaksi joukoksi. Numeroituvan joukon alkioille voidaan kullekin antaa oma luonnollinen luku nimeksi tai indeksiksi. Numeroituvuus on tietyssä mielessä yksinkertaisin äärettömyyden laji.
Jo numeroituvuus synnyttää monia "paradoksaalisia" tuloksia. Esimerkiksi Gödelin ensimmäinen epätäydellisyyslause on mahdollista todistaa, kunhan meillä on riittävän ilmaisuvoimainen formalismi. Siihen vaaditaan luonnolliset luvut ja aritmeettiset perusoperaatiot, mutta ei juuri muuta. Tällöin saadaan luotua tilanne, jossa struktuurin ominaisuudet "karkaavat" yrityksiltä määritellä se: Struktuurilla voidaan "nähdä" olevan ominaisuuksia joita ei yksinkertaisesti ole mahdollista todistaa.
Sama ilmiö hiipii sisään kaikkiin formalismeihin, jotka sallivat "riittävästi" ilmaisuja jotta voimme erotella kaikki ne asiat jotka formalismi itse kykenee tekemään. Esimerkiksi kelpaavat rekursiiviset funktiot. Jos lähdemme luonnollisista luvuista sen kummemmin problematisoimatta niiden operaatioita, voimme määritellä funktioita jotka voidaan "kuvata" yksinkertaisista lähtökohdista lähtien. Yksinkertaisia peruskuvauksia ovat nollafunktio joka saa arvon 0 joka tilanteessa, seuraajafunktio joka saa arvon x ja palauttaa arvon x+1, i:s projektiofunktio joka saa n argumenttia ja palauttaa niistä i:nnen, kompositio kuvaa n-argumenttisen funktion: Kun g kuvaa k-argumenttisen funktion ja funktiot h1,..., hk kuvaavat n-argumenttisia funktiota, niin f(x) = g(h1(x), ... , hk(x)) on kompositio. Näiden lisäksi on kaksi kuvausta: rekursiokuvaus joka kuvaa n+1 parametrisen funktion: kun g on n parametrinen funktio ja h on n+2 parametrinen funktio, niin f(x,0) = g(x) ja f(x,y+1) = h(x,y,f(x,y)), ja minimointi joka kuvaa n-parametrisen funktion n+1 parametrisen funktion avulla. f(x) = μ y g(x,y). Tämä tarkoittaa, että f(x) saa arvokseen pienimmän sellaisen y:n arvon, jolla g(x,y) = 0. Näistä ainoastaan minimointi voi tuottaa jotakin mikä ei ole hyvin määritelty.
En lähde tässä sen tarkemmin käymään läpi rekursiivisten funktioiden teoriaa. Olennaisia asioita on kaksi: Kaikille rekursiivisille kuvauksille voidaan esittää numero, joka yksilöi juuri sen kuvauksen, ja että kaikkia funktioita ei voida kuvata rekursiivisilla kuvauksilla, mutta "suuri osa" voidaan. Aivan erityisesti, niiden avulla voidaan kuvata aivan kaikki sellaiset luonnollisten lukujen funktiot jotka ylipäätään voidaan laskea esimerkiksi tietokoneella. Siitä huolimatta voidaan määritellä aivan ymmärrettäviä ja intuitiivisesti hyvinmääriteltyjä funktioita joista kuitenkin voidaan todistaa, etteivät ne ole rekursiivisia. Epätäydellisyyslausekin voidaan ilmaista siten, että jokainen lukuteorian aksiomatisointi, joka voitaisiin tulostaa (päättymättömällä) tietokoneohjelmalla, on epätäydellinen, eli ei koskaan tuota kaikkia tosia väittämiä.
Finitistit eivät pääsääntöisesti hyväksy näitä tuloksia, ja tässä on argumenttina se, että vaikka teoriat muilta osin ovat aivan hyvin käyttäytyviä, ne postuloivat että "kaikki" funktiot tai "kaikki" tietokoneohjelmat - samoin kuin "kaikki" luonnolliset luvut - on huonosti määritelty käsite. Vaikka tämä näkemys on vähän ankea ja hankala, se ei ole täysin epärationaalinen. Sen tueksi on olemassa jopa joitakin tuloksia. Nimittäin, vaikka tiedämme esimerkiksi että universaalia pysähtymistesteriä ei ole - samoin kuin ei ole rekursiivista kuvausta funktiolle joka palauttaisi 0 kun sille annettu numero on sellaisen funktion kuvaus joka on kaikkialla hyvinmääritelty ja 1 muulloin - tiedämme myös, että jokaista tällaista turingin konetta tai rekursiivista kuvausta kohden on olemassa sellainen rekursiivinen funktio joka tunnistaa äärettömän määrän tällaisia koneita ja että juuri tämä kone kuuluu siihen luokkaan jonka ko. funktio tunnistaa.
Voidaan siis argumentoida, että ainoa ongelma on sellainen universaalius, joka lupaa jotain "kaikille" luvuille tai "kaikille" koneille tai "kaikille" funktiokuvauksille, ja että tämä ongelma ja ratkeamattomuus- ja epätäydellisyystulokset ovat seurausta tästä typerästä lupauksesta, koska mitään äärettömyyttä ei ole olemassakaan.
En itse usko että tämä on välttämättä hedelmällinen lähtökohta, mutta en myöskään voi kumota sitä millään sellaisella argumentilla, joka olisi täysin vakuuttava. Formalistina tietysti ajattelisin, että kysymys siitä onko äärettömyyttä "olemassa" ei ole merkitystä, vaan ainoastaan sillä, mitä voimme äärettömyydestä päätellä. Se ei ole "totta" tai ole olematta, vaan ainoastaan tietyn merkkijonopelin tuloksia. Tämä näkemys on kuitenkin kovin epätyydyttävä useimmille ihmisille filosofisesti. En ota vahvaa kantaa siihen, miksi näin on, mutta voi tietenkin olla vain niin, että ihmisen aivot nyt vaan ovat huonot koska ne etsivät liian yksinkertaisia vastauksia, puhtaasti omaa vajavaisuuttaan. Äärettömyyshän on lopulta vain nimi sille että lukumäärä ei todellakaan ole hyvinmääritelty.
Lähdetään ensimmäisen kertaluvun kielestä, jossa emme nyt rajoita sen kummemmin ilmaisua. Oletetaan että voimme sanoa jotain sellaista että "a = b", ilmaistaksemme identiteettiä. Termit a ja b siis viittaavat "johonkin" ja identiteetti tarkoittaa että ne viittaavat samaan. Jos sanomme, että "ei a=b", niin sanomme, että a ja b eivät ole identtisiä. Ilmaisen tämän "a != b" Tällainen termi, ollessaan totta, ilmaisee jo (implisiittisesti) lukumäärää: Se sanoo että ainakin kaksi termiä viittaa eri asioihin.
Tästä erillisyydestä voimme jalostaa eräänlaisen äärettömyyden seuraavalla tavalla. Tarkastellaan binääristä relaatiota R, joka ilmaisee a:n ja b:n suhdetta. Sovitaan että R:llä on seuraavat ominaisuudet: 1. Jos R(a,b) pätee ja R(b,a) pätee, niin a = b. 2. Jos R(a,b) pätee, ja R(b,c) pätee,
niin R(a,c) pätee. 3. Jokaiselle alkiolle x on olemassa alkio y siten että x != y ja R(x,y) pätee.
Tälle relaatiolle ei ole olemassa äärellistä mallia. Nimittäin, jos mallissamme on äärellinen määrä - olkoon se mikä hyvänsä, esimerkiksi 3 - alkioita, voimme valita niistä yhden - minkä tahansa - ja merkitä tätä symbolilla "0". On olemassa alkio x, joka on erisuuri kuin 0, siten, että R(0,x) pätee. Toisaalta, ei voi päteä että R(x,0), koska tällöin x = 0 pätisi ominaisuuden 1 nojalla. Sovelletaan kohtaa 3 alkioon x, saamme uuden alkion, y. Edelleen, voimme kohdan 2 ja 1 nojalla toteamme, että myös y !=0. Itseasiassa, joka kerta kun sovellamme kohtaa 3, saamme alkion, jota emme ole vielä kohdanneet. Mutta jos mallissamme oli kolme alkiota, niin kolmas yritys soveltaa kohtaa 3 johtaa ristiriitaan: Uuden alkion pitää olla erisuuri kuin 0, x, tai y, koska 3:n kohdan nojalla se ei ole y, ja jos se olisi x, niin R(x,y):stä seuraisi kohdan 1 nojalla, että se uusi alkio olisi y, mikä on ristiriita. Ja jos uusi alkio olisi 0, niin kohdan 2 nojalla uusi alkio olisi taas x, mikä ei ole mahdollista.
Äärellisen mallin olettaminen johtaa siis väistämättä ristiriitaan. Tiukan finitistinen tulkinta matematiikasta sanoisi, että hyvä on, tämä tarkoittaa että alkuperäinen ominaisuuksien joukko on väistämättä ristiriitainen. Tämä vastaisi siis sellaista joukko-opin aksiomatisointia joka sanoisi että kaikki joukot ovat äärellisiä.
Mutta tämä johtaa ongelmiin sekin. Esimerkiksi, jos oletamme, että luonnollisten lukujen joukko on hyvin määritelty käsite, ja otamme relaation R(x,y) tarkoittamaan "y = x +1", niin luonnollisten lukujen joukko *on* malli R:lle, siis, tämä relaatio toteuttaa R:n ominaisuudet. Se on siis ääretön.
Luonnollisten lukujen joukkoa pidetään eräänlaisena standardimallina sille, mitä normaali aritmetiikka tarkoittaa. Tässä viittaan siis sellaisiin asioihin kuin "lukuteoria" tms, jossa on kyse siis yhteen- ja kertolaskusta ja niistä johdetuista operaatioista. Sitä voidaan pitää lukumäärien teorian standardimallina. Luonnollisten lukujen kanssa isomorfista(*) joukkoa nimitetään sanotaan numeroituvaksi joukoksi. Numeroituvan joukon alkioille voidaan kullekin antaa oma luonnollinen luku nimeksi tai indeksiksi. Numeroituvuus on tietyssä mielessä yksinkertaisin äärettömyyden laji.
Jo numeroituvuus synnyttää monia "paradoksaalisia" tuloksia. Esimerkiksi Gödelin ensimmäinen epätäydellisyyslause on mahdollista todistaa, kunhan meillä on riittävän ilmaisuvoimainen formalismi. Siihen vaaditaan luonnolliset luvut ja aritmeettiset perusoperaatiot, mutta ei juuri muuta. Tällöin saadaan luotua tilanne, jossa struktuurin ominaisuudet "karkaavat" yrityksiltä määritellä se: Struktuurilla voidaan "nähdä" olevan ominaisuuksia joita ei yksinkertaisesti ole mahdollista todistaa.
Sama ilmiö hiipii sisään kaikkiin formalismeihin, jotka sallivat "riittävästi" ilmaisuja jotta voimme erotella kaikki ne asiat jotka formalismi itse kykenee tekemään. Esimerkiksi kelpaavat rekursiiviset funktiot. Jos lähdemme luonnollisista luvuista sen kummemmin problematisoimatta niiden operaatioita, voimme määritellä funktioita jotka voidaan "kuvata" yksinkertaisista lähtökohdista lähtien. Yksinkertaisia peruskuvauksia ovat nollafunktio joka saa arvon 0 joka tilanteessa, seuraajafunktio joka saa arvon x ja palauttaa arvon x+1, i:s projektiofunktio joka saa n argumenttia ja palauttaa niistä i:nnen, kompositio kuvaa n-argumenttisen funktion: Kun g kuvaa k-argumenttisen funktion ja funktiot h1,..., hk kuvaavat n-argumenttisia funktiota, niin f(x) = g(h1(x), ... , hk(x)) on kompositio. Näiden lisäksi on kaksi kuvausta: rekursiokuvaus joka kuvaa n+1 parametrisen funktion: kun g on n parametrinen funktio ja h on n+2 parametrinen funktio, niin f(x,0) = g(x) ja f(x,y+1) = h(x,y,f(x,y)), ja minimointi joka kuvaa n-parametrisen funktion n+1 parametrisen funktion avulla. f(x) = μ y g(x,y). Tämä tarkoittaa, että f(x) saa arvokseen pienimmän sellaisen y:n arvon, jolla g(x,y) = 0. Näistä ainoastaan minimointi voi tuottaa jotakin mikä ei ole hyvin määritelty.
En lähde tässä sen tarkemmin käymään läpi rekursiivisten funktioiden teoriaa. Olennaisia asioita on kaksi: Kaikille rekursiivisille kuvauksille voidaan esittää numero, joka yksilöi juuri sen kuvauksen, ja että kaikkia funktioita ei voida kuvata rekursiivisilla kuvauksilla, mutta "suuri osa" voidaan. Aivan erityisesti, niiden avulla voidaan kuvata aivan kaikki sellaiset luonnollisten lukujen funktiot jotka ylipäätään voidaan laskea esimerkiksi tietokoneella. Siitä huolimatta voidaan määritellä aivan ymmärrettäviä ja intuitiivisesti hyvinmääriteltyjä funktioita joista kuitenkin voidaan todistaa, etteivät ne ole rekursiivisia. Epätäydellisyyslausekin voidaan ilmaista siten, että jokainen lukuteorian aksiomatisointi, joka voitaisiin tulostaa (päättymättömällä) tietokoneohjelmalla, on epätäydellinen, eli ei koskaan tuota kaikkia tosia väittämiä.
Finitistit eivät pääsääntöisesti hyväksy näitä tuloksia, ja tässä on argumenttina se, että vaikka teoriat muilta osin ovat aivan hyvin käyttäytyviä, ne postuloivat että "kaikki" funktiot tai "kaikki" tietokoneohjelmat - samoin kuin "kaikki" luonnolliset luvut - on huonosti määritelty käsite. Vaikka tämä näkemys on vähän ankea ja hankala, se ei ole täysin epärationaalinen. Sen tueksi on olemassa jopa joitakin tuloksia. Nimittäin, vaikka tiedämme esimerkiksi että universaalia pysähtymistesteriä ei ole - samoin kuin ei ole rekursiivista kuvausta funktiolle joka palauttaisi 0 kun sille annettu numero on sellaisen funktion kuvaus joka on kaikkialla hyvinmääritelty ja 1 muulloin - tiedämme myös, että jokaista tällaista turingin konetta tai rekursiivista kuvausta kohden on olemassa sellainen rekursiivinen funktio joka tunnistaa äärettömän määrän tällaisia koneita ja että juuri tämä kone kuuluu siihen luokkaan jonka ko. funktio tunnistaa.
Voidaan siis argumentoida, että ainoa ongelma on sellainen universaalius, joka lupaa jotain "kaikille" luvuille tai "kaikille" koneille tai "kaikille" funktiokuvauksille, ja että tämä ongelma ja ratkeamattomuus- ja epätäydellisyystulokset ovat seurausta tästä typerästä lupauksesta, koska mitään äärettömyyttä ei ole olemassakaan.
En itse usko että tämä on välttämättä hedelmällinen lähtökohta, mutta en myöskään voi kumota sitä millään sellaisella argumentilla, joka olisi täysin vakuuttava. Formalistina tietysti ajattelisin, että kysymys siitä onko äärettömyyttä "olemassa" ei ole merkitystä, vaan ainoastaan sillä, mitä voimme äärettömyydestä päätellä. Se ei ole "totta" tai ole olematta, vaan ainoastaan tietyn merkkijonopelin tuloksia. Tämä näkemys on kuitenkin kovin epätyydyttävä useimmille ihmisille filosofisesti. En ota vahvaa kantaa siihen, miksi näin on, mutta voi tietenkin olla vain niin, että ihmisen aivot nyt vaan ovat huonot koska ne etsivät liian yksinkertaisia vastauksia, puhtaasti omaa vajavaisuuttaan. Äärettömyyshän on lopulta vain nimi sille että lukumäärä ei todellakaan ole hyvinmääritelty.
perjantai 18. lokakuuta 2013
Boolen algebrat
Lähdetään tilanteesta, jossa meillä on osittaisjärjestetty joukko, pari (S, ≤), joka on samalla ns. hila. Hilalla tarkoitetaan rakennetta, jossa osittaisjärjestyksen suhteen voidaan löytää kullekin alkioparille pienin yläraja (sup) ja suurin alaraja (inf). Näitä voidaan merkitä useammallakin symbolilla, mutta usein käytetään merkintöjä x ∨ y ja x ∧ y. Hila on täydellinen, jos jokaisella osajoukolla on sup ja inf, ja näinollen koko joukolla on suurin ja pienin alkio. Näitä on tapana merkitä symboleilla 1 ja 0, joskus myös T ja ⊥. (Tarkkaanottaen ensimmäinen ei ole "T", mutten löytänyt symbolia). Täydellinen hila on komplementoitu, jos jokaiselle alkiolle on komplementti, x*, siten että x ∨ x* = 1 ja x ∧ x* = 0. Hila on distributiivinen, jos x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z). Komplementoitu distributiivinen hila on Boolen algebra.
Jos meillä on ensimmäisen kertaluvun logiikka, sen kaavojen ekvivalenssiluokista voidaan muodostaa boolen algebra, jossa x ∨ y tarkoittaa kaavojen x ja y disjunktiota, x ∧ y konjunktiota ja x* negaatiota. Lisäksi pätee että x ≤ y jos ja vain jos x* ∨ y = 1. Tämä voidaan todistaa ominaisuuksista teoreemana. Operaatiota x* ∨ y merkitään logiikassa tavallisesti implikaationuolella.
Algebrallinen lähestymistapa kohtaa topologian myös logiikan kohdalla. Filtteri (suomeksi "suodatin", mutten käytä tätä sanaa koska mielestäni se ei ole sopiva tässä kohtaa) voidaan ajatella algebran osajoukoksi, jolla on muutama ominaisuus: Se ei sisällä alkiota 0, ja jos x ja y kuuluvat filtteriin, x ∧ y kuuluu filtteriin, ja se on ylöspäin suljettu, eli jos x on filtterissä, niin jokainen y siten että x ≤ y on myös filtterissä. Filtterit vastaavat logiikan struktuureina konsistentteja teorioita. Maksimaalinen filtteri on filtteri, jota ei voi kasvattaa. Maksimaalista filtteriä nimitetään myös ultrafilttereiksi.
Tärkeä algebrassa käytettävä kuvaus on homomorfismi. Kuvaus f algebralta X algebralle Y on homomorfismi, jos f(x * y) = f(x) * f(y) kaikille algebran operaatioille. Homomorfismin ja filtterin suhde on mielenkiintoinen. Nimittäin, jos f on homomorfismi X:ltä Y:lle, niin alkion 1 alkukuva X:ssä on filtteri. Jos homomorfismi on 2-arvoinen (eli saa vain arvoja 0 ja 1), niin alkukuva on ultrafiltteri.
Kun filtteri vastaa teoriaa, niin ultrafiltteri vastaa täydellistä teoriaa, siis teoriaa, joka määrittää jokaisen logiikan kaavan totuusarvon.
Filtterin F osajoukko X on kanta, jos jokaiselle filtterin alkiolle löytyy alaraja X:stä. Kanta vastaa aksiomatisointia.
Jos meillä on ensimmäisen kertaluvun logiikka, sen kaavojen ekvivalenssiluokista voidaan muodostaa boolen algebra, jossa x ∨ y tarkoittaa kaavojen x ja y disjunktiota, x ∧ y konjunktiota ja x* negaatiota. Lisäksi pätee että x ≤ y jos ja vain jos x* ∨ y = 1. Tämä voidaan todistaa ominaisuuksista teoreemana. Operaatiota x* ∨ y merkitään logiikassa tavallisesti implikaationuolella.
Algebrallinen lähestymistapa kohtaa topologian myös logiikan kohdalla. Filtteri (suomeksi "suodatin", mutten käytä tätä sanaa koska mielestäni se ei ole sopiva tässä kohtaa) voidaan ajatella algebran osajoukoksi, jolla on muutama ominaisuus: Se ei sisällä alkiota 0, ja jos x ja y kuuluvat filtteriin, x ∧ y kuuluu filtteriin, ja se on ylöspäin suljettu, eli jos x on filtterissä, niin jokainen y siten että x ≤ y on myös filtterissä. Filtterit vastaavat logiikan struktuureina konsistentteja teorioita. Maksimaalinen filtteri on filtteri, jota ei voi kasvattaa. Maksimaalista filtteriä nimitetään myös ultrafilttereiksi.
Tärkeä algebrassa käytettävä kuvaus on homomorfismi. Kuvaus f algebralta X algebralle Y on homomorfismi, jos f(x * y) = f(x) * f(y) kaikille algebran operaatioille. Homomorfismin ja filtterin suhde on mielenkiintoinen. Nimittäin, jos f on homomorfismi X:ltä Y:lle, niin alkion 1 alkukuva X:ssä on filtteri. Jos homomorfismi on 2-arvoinen (eli saa vain arvoja 0 ja 1), niin alkukuva on ultrafiltteri.
Kun filtteri vastaa teoriaa, niin ultrafiltteri vastaa täydellistä teoriaa, siis teoriaa, joka määrittää jokaisen logiikan kaavan totuusarvon.
Filtterin F osajoukko X on kanta, jos jokaiselle filtterin alkiolle löytyy alaraja X:stä. Kanta vastaa aksiomatisointia.
tiistai 15. lokakuuta 2013
Epätäydellisyys
Kuuluisia Gödelin epätäydellisyyslauseita on kaksi. Ensimmäinen koskee formaalin todistuksen ja "totuuden" suhdetta ja toinen koskee konsistenssin ja epäkonsistenssin todistettavuutta. Käsittelen tässä lähinnä ensimmäistä, mutta mainitsen myös toisen.
Jotta Gödelin lause voidaan ymmärtää, pitää ensin määritellä ns Gödel-numerointi. Oletetaan että meillä on ensimmäisen kertaluvun kieli, siis ensimmäisen kertaluvun predikaattilogiikka ja sillä esitetyt kaavat. Oletamme tässä yksinkertaisuuden vuoksi että käytössämme on yhtäsuuruus (=) ja funktiosymbolit "+", "*" ja "s", missä "s(x)" tarkoittaa samaa kuin "x:stä seuraava". Lisäksi voimme kvantifioida muuttujia - muuttujat ovat kotoisin numeroituvasta joukosta, esimerkiksi x, x', x'', jne. Vakioita on yksi, "a", ja sen tulkinta fiksataan niin, että se on tutummin nolla.
Gödel-numerointi tarkoittaa sitä, että annamme jokaiselle logiikan kielessä esiintyvälle symbolille - muuttujille, vakioille, funktiosymboleille, kvanttoreille, sulkumerkeille ja välimerkeillä - oman numeron. Varaamme lisäksi numeroita erilaisille yhdistelmämerkeille; voimme tehdä tämän "helposti" koska numeroitahan on äärettömästi. Täytyy vain pitää tarkkaan huolta, että jokaisella luvulla on yksikäsitteinen tulkinta.
En aio esittää varsinaista Gödel-numerointia tässä, mutta numerointi voidaan tehdä siten, että jokaiselle syntaktisesti oikein kirjoitetulle kaavalle, tai kaavojen sekvenssille saadaan uniikki luku, jonka tulkinta on yksikäsitteinen. Yksi mahdollinen numerointi löytyy Wikipedian artikkelista.
Lisäksi otamme lähtökohdaksi jonkin täydellisen 1-kertaluvun päättelyjärjestelmän. Esimerkki tällaisesta on vaikkapa Hilbertin järjestelmä. Ei ole olennaista, mikä tällainen järkestelmä on, kunhan se on täydellinen - eli jokainen tautologia predikaattilogiikassa voidaan sillä todistaa - ja äärellinen. Tällaisen järjestelmän säännöille voidaan siten antaa omat numeronsa, ja voimme näiden numeroiden avulla määritellä relaatio R(x,y) joka pätee tasan silloin kun x koodaa jonkin päättelyn niin, että y on laillinen seuraava askel tässä päättelyssä. Tällä tavoin saamme itseasiassa relaation joka sanoo, että luku y koodaa tietyn väittämän logiikassa ja x koodaa sen todistuksen, käyttäen pelkästään alkeellista aritmetiikkaa.
Voimme tunnistaa tällä järjestelmällä mielivaltaisen kaavan F joka on laillisesti kirjoitettu ja jossa on yksi vapaa muuttuja; vapaa muuttuja on osa kaavaa. joten jos annamme sille jonkin tietyn arvon, esimerkiksi 5, niin saamme toisen kaavan, F(5). Kaavan itsensä numeroa merkitsemme vaikkapa #F, ja tietysti #F on eri numero kuin #F(5).
Nyt predikaattio R(n,#F(5)) on tosi tasan silloin kun n on koodaus F(5):n todistukselle. Tarkastellaan väittämää R(n,#(F(#F)), joka sanoo, että n on koodaus sille todistukselle, joka todistaa että F(#F) pätee. Jokaisella tällaisella kaavalla on myös hyvinmääritelty yksikäsitteinen Gödel-numero.
Tämän jälkeen tarkastellaan kaavaa P(#F) joka sanoo että "Ei ole olemassa x:ää niin että R(x, #(F(#F))". pahoittelen loogisten symbolien puutetta, mutta ne on työlästä lisätä. Joka tapauksessa, koska tällekin kaavalle on Gödel-numerointi, se on ihan hyvin määritelty kaava.
Ja nyt se kikka: Mikä onkaan P(#P):n totuusarvo? Se nimittääin sanoo, että ei löydy x:ää niin, että R(x,#P(#P)) pitäisi paikkaansa. Tämä tarkoittaisi siis, että ei ole olemassa sellaista numeroa, joka koodaisi P(#P):n todistuksen.
Tämä predikaatti on aivan hyvinmääritelty. Se on väittämä joka joko pitää paikkansa tai sitten ei pidä. Jos se ei pidä paikkaansa, niin luonnollisista luvuista löytyisi sellainen alkio joka koodaisi väittämän todistuksen. Tiedämme kuitenkin, että esimerkiksi Hilbertin järjestelmä (tai mikä ikinä äärellinen päättelyjärjestelmä meillä onkaan käytössä) voi todistaa vain tosia väittämiä. Joten väittämälle ei voi olla todistusta.
Gödelin - ja kanoninen tulkinta ylipäänsä - tälle lauseelle on, että on olemassa aritmeettisia "totuuksia" joita ei voi todistaa. Tämä on todistusteoreettinen tulos; me emme voi todistaa että P(#P) on tosi kaikissa aritmetiikan malleissa. Se on selvästi tosi siinä mallissa jonka me yleensä ymmärrämme luonnollisiksi luvuiksi, ja joista Gödel-numerotkin olemme poimineet. Sensijaan se ei ole tosi kaikissa malleissa. Jos se nimittäin olisi tosi kaikissa malleissa, niin se olisi tautologia, ja me tiedämme, että kaikki tautologiat voidaan todistaa. On siis mahdollista luoda aritmetiikkajärjestelmä, jossa tämä väittämä on todistettavissa. Se on kuitenkin erilainen kuin se, jonka ominaisuuksiin nojaamme kun esitämme tämän todistuksen.
Tietojenkäsittelyllinen näkökulma ensimmäiseen epätäydellisyyslauseeseen on, että ei voida esittää sellaista algoritmia, joka tulostaisi ulos paikkansapitäviä aritmeettisiä väittämiä niin, että jokainen tosi väittämä tulee lopulta ulos, mutta ei yhtään epätotta väittämää. Tämä näkökulma tarjoaa lyhyemmän ja - joidenkin mielestä - ymmärrettävämmän tuloksen: Jokaiselle syntaktisesti erilaiselle kaavalle voidaan antaa numero, ja tästä johdetaan muutamalla tempulla ns. Berryn paradoksi. Berryn paradoksi menee jotenkin niin, että postuloidaan "Pienin luonnollinen luku, jota ei voi määritellä alle 11 sanalla", mikä itsessään on määritelmä joka on ristiriidassa itsensä kanssa; tietokoneohjelmasta joka tuottaa kaikki aritmeettiset totuudet, saadaan johdettua samantapainen paradoksi.
Toinen epätäydellisyyslause on samansukuinen, mutta siinä puhutaan aksioomajärjestelmän konsistenssista. Konsistenssilla tarkoitetaan sitä, että aksiomien joukosta ei voida löytää ristiriitoja, eli ei voida yhtä aikaa todistaa jotakin väittämää ja sen negaatiota. Gödel rakentaa tämän tuloksen samaan tapaan kuin ensimmäisen epätäydellisyyslauseenkin, mutta tämän lisäksi tarvitaan hyvin monimutkainen konstruktio jolla ilmaistaan konsistenssiväittämä. Konsistenssiväittämä on jotakuinkin se että "Ei ole olemassa toditusta epätodelle väittämälle". Konsistenssiväittämän todistus itsessään johtaa tilanteeseen, jossa samalla todistetaan ristiriita.
Jotta Gödelin lause voidaan ymmärtää, pitää ensin määritellä ns Gödel-numerointi. Oletetaan että meillä on ensimmäisen kertaluvun kieli, siis ensimmäisen kertaluvun predikaattilogiikka ja sillä esitetyt kaavat. Oletamme tässä yksinkertaisuuden vuoksi että käytössämme on yhtäsuuruus (=) ja funktiosymbolit "+", "*" ja "s", missä "s(x)" tarkoittaa samaa kuin "x:stä seuraava". Lisäksi voimme kvantifioida muuttujia - muuttujat ovat kotoisin numeroituvasta joukosta, esimerkiksi x, x', x'', jne. Vakioita on yksi, "a", ja sen tulkinta fiksataan niin, että se on tutummin nolla.
Gödel-numerointi tarkoittaa sitä, että annamme jokaiselle logiikan kielessä esiintyvälle symbolille - muuttujille, vakioille, funktiosymboleille, kvanttoreille, sulkumerkeille ja välimerkeillä - oman numeron. Varaamme lisäksi numeroita erilaisille yhdistelmämerkeille; voimme tehdä tämän "helposti" koska numeroitahan on äärettömästi. Täytyy vain pitää tarkkaan huolta, että jokaisella luvulla on yksikäsitteinen tulkinta.
En aio esittää varsinaista Gödel-numerointia tässä, mutta numerointi voidaan tehdä siten, että jokaiselle syntaktisesti oikein kirjoitetulle kaavalle, tai kaavojen sekvenssille saadaan uniikki luku, jonka tulkinta on yksikäsitteinen. Yksi mahdollinen numerointi löytyy Wikipedian artikkelista.
Lisäksi otamme lähtökohdaksi jonkin täydellisen 1-kertaluvun päättelyjärjestelmän. Esimerkki tällaisesta on vaikkapa Hilbertin järjestelmä. Ei ole olennaista, mikä tällainen järkestelmä on, kunhan se on täydellinen - eli jokainen tautologia predikaattilogiikassa voidaan sillä todistaa - ja äärellinen. Tällaisen järjestelmän säännöille voidaan siten antaa omat numeronsa, ja voimme näiden numeroiden avulla määritellä relaatio R(x,y) joka pätee tasan silloin kun x koodaa jonkin päättelyn niin, että y on laillinen seuraava askel tässä päättelyssä. Tällä tavoin saamme itseasiassa relaation joka sanoo, että luku y koodaa tietyn väittämän logiikassa ja x koodaa sen todistuksen, käyttäen pelkästään alkeellista aritmetiikkaa.
Voimme tunnistaa tällä järjestelmällä mielivaltaisen kaavan F joka on laillisesti kirjoitettu ja jossa on yksi vapaa muuttuja; vapaa muuttuja on osa kaavaa. joten jos annamme sille jonkin tietyn arvon, esimerkiksi 5, niin saamme toisen kaavan, F(5). Kaavan itsensä numeroa merkitsemme vaikkapa #F, ja tietysti #F on eri numero kuin #F(5).
Nyt predikaattio R(n,#F(5)) on tosi tasan silloin kun n on koodaus F(5):n todistukselle. Tarkastellaan väittämää R(n,#(F(#F)), joka sanoo, että n on koodaus sille todistukselle, joka todistaa että F(#F) pätee. Jokaisella tällaisella kaavalla on myös hyvinmääritelty yksikäsitteinen Gödel-numero.
Tämän jälkeen tarkastellaan kaavaa P(#F) joka sanoo että "Ei ole olemassa x:ää niin että R(x, #(F(#F))". pahoittelen loogisten symbolien puutetta, mutta ne on työlästä lisätä. Joka tapauksessa, koska tällekin kaavalle on Gödel-numerointi, se on ihan hyvin määritelty kaava.
Ja nyt se kikka: Mikä onkaan P(#P):n totuusarvo? Se nimittääin sanoo, että ei löydy x:ää niin, että R(x,#P(#P)) pitäisi paikkaansa. Tämä tarkoittaisi siis, että ei ole olemassa sellaista numeroa, joka koodaisi P(#P):n todistuksen.
Tämä predikaatti on aivan hyvinmääritelty. Se on väittämä joka joko pitää paikkansa tai sitten ei pidä. Jos se ei pidä paikkaansa, niin luonnollisista luvuista löytyisi sellainen alkio joka koodaisi väittämän todistuksen. Tiedämme kuitenkin, että esimerkiksi Hilbertin järjestelmä (tai mikä ikinä äärellinen päättelyjärjestelmä meillä onkaan käytössä) voi todistaa vain tosia väittämiä. Joten väittämälle ei voi olla todistusta.
Gödelin - ja kanoninen tulkinta ylipäänsä - tälle lauseelle on, että on olemassa aritmeettisia "totuuksia" joita ei voi todistaa. Tämä on todistusteoreettinen tulos; me emme voi todistaa että P(#P) on tosi kaikissa aritmetiikan malleissa. Se on selvästi tosi siinä mallissa jonka me yleensä ymmärrämme luonnollisiksi luvuiksi, ja joista Gödel-numerotkin olemme poimineet. Sensijaan se ei ole tosi kaikissa malleissa. Jos se nimittäin olisi tosi kaikissa malleissa, niin se olisi tautologia, ja me tiedämme, että kaikki tautologiat voidaan todistaa. On siis mahdollista luoda aritmetiikkajärjestelmä, jossa tämä väittämä on todistettavissa. Se on kuitenkin erilainen kuin se, jonka ominaisuuksiin nojaamme kun esitämme tämän todistuksen.
Tietojenkäsittelyllinen näkökulma ensimmäiseen epätäydellisyyslauseeseen on, että ei voida esittää sellaista algoritmia, joka tulostaisi ulos paikkansapitäviä aritmeettisiä väittämiä niin, että jokainen tosi väittämä tulee lopulta ulos, mutta ei yhtään epätotta väittämää. Tämä näkökulma tarjoaa lyhyemmän ja - joidenkin mielestä - ymmärrettävämmän tuloksen: Jokaiselle syntaktisesti erilaiselle kaavalle voidaan antaa numero, ja tästä johdetaan muutamalla tempulla ns. Berryn paradoksi. Berryn paradoksi menee jotenkin niin, että postuloidaan "Pienin luonnollinen luku, jota ei voi määritellä alle 11 sanalla", mikä itsessään on määritelmä joka on ristiriidassa itsensä kanssa; tietokoneohjelmasta joka tuottaa kaikki aritmeettiset totuudet, saadaan johdettua samantapainen paradoksi.
Toinen epätäydellisyyslause on samansukuinen, mutta siinä puhutaan aksioomajärjestelmän konsistenssista. Konsistenssilla tarkoitetaan sitä, että aksiomien joukosta ei voida löytää ristiriitoja, eli ei voida yhtä aikaa todistaa jotakin väittämää ja sen negaatiota. Gödel rakentaa tämän tuloksen samaan tapaan kuin ensimmäisen epätäydellisyyslauseenkin, mutta tämän lisäksi tarvitaan hyvin monimutkainen konstruktio jolla ilmaistaan konsistenssiväittämä. Konsistenssiväittämä on jotakuinkin se että "Ei ole olemassa toditusta epätodelle väittämälle". Konsistenssiväittämän todistus itsessään johtaa tilanteeseen, jossa samalla todistetaan ristiriita.
maanantai 14. lokakuuta 2013
Pitkä Juoksu 2, vol IV + vähän muuta.
Kävin perjantaina kokeilemassa polveani. Olen venytellyt ohjeiden mukaan - tosin joidenkin lähteiden mukaan ITBS:ää ei voi hoitaa venytyksin. Perjantainen juoksu sujui paremmin kuin aiemmat, joten paranemista lienee tapahtunut. Kipu alkoi kuudennella kilometrillä, ja vahingosta viisastuneena en yrittänyt juosta kipua vastaan. Pysähtelin ja venyttelin välillä, mutta luovutin noin kahdeksan kilometrin kohdalla ja vaihdoin hitaaseen kävelyyn.
Sunnuntaina juoksin reilu neljä kilometriä ilman kipua. Toistaiseksi suunnitelmani on, että juoksen nopeita lyhyitä lenkkejä ja toisinaan kokeilen paljonko polvi kestää.
Tämä myös sikäli helpotti päätöstäni Lanzaroten suhteen: en missään nimessä voi osallistua täysmaratonille. Puolikaskin voi olla liian pitkä, joten jos en ole pystynyt siihen mennessä luotettavasti ilman kipuja juoksemaan vähintään 20 kilometrin matkaa, osallistun esimerkiksi vain kympille. Matkaa en aio tietenkään perua, koska siitä on jo varausmaksu maksettu.
Tällä viikolla ei ole luentoja, ja teen ensi viikoksi luentomateriaalia. Kävin Ben-Arin ne osat läpi jo, joita pidän olennaisina: Propositiologiikan, Herbrandin teoreema, Löwenheim-Skolemin, kompaktisuuden, täydellisyyden ja Gödelin ensimmäisen epätäydellisyyden. Täydennän materiaalia algebrallisella lähestymisellä, mistä laajennan malliteoriaan juuri sen verran, että täydellisyys, kompaktisuus ja Löwenheim-Skolem saadaan käsiteltyä tästä näkökulmasta. Jos aikaa jää, otan rekursioteoriaa sen verran, että voin esittää laskennallisuustulkinnan Gödelin epätäydellisyyslauseesta.
Sunnuntaina juoksin reilu neljä kilometriä ilman kipua. Toistaiseksi suunnitelmani on, että juoksen nopeita lyhyitä lenkkejä ja toisinaan kokeilen paljonko polvi kestää.
Tämä myös sikäli helpotti päätöstäni Lanzaroten suhteen: en missään nimessä voi osallistua täysmaratonille. Puolikaskin voi olla liian pitkä, joten jos en ole pystynyt siihen mennessä luotettavasti ilman kipuja juoksemaan vähintään 20 kilometrin matkaa, osallistun esimerkiksi vain kympille. Matkaa en aio tietenkään perua, koska siitä on jo varausmaksu maksettu.
Tällä viikolla ei ole luentoja, ja teen ensi viikoksi luentomateriaalia. Kävin Ben-Arin ne osat läpi jo, joita pidän olennaisina: Propositiologiikan, Herbrandin teoreema, Löwenheim-Skolemin, kompaktisuuden, täydellisyyden ja Gödelin ensimmäisen epätäydellisyyden. Täydennän materiaalia algebrallisella lähestymisellä, mistä laajennan malliteoriaan juuri sen verran, että täydellisyys, kompaktisuus ja Löwenheim-Skolem saadaan käsiteltyä tästä näkökulmasta. Jos aikaa jää, otan rekursioteoriaa sen verran, että voin esittää laskennallisuustulkinnan Gödelin epätäydellisyyslauseesta.
tiistai 14. toukokuuta 2013
Logiikka ja tiede
Tilasin Ben-Arin Mathematical Logic for Computer Science oppikirjaksi syksyn matemaattisen logiikan kurssille. Kyseisen kirjan sisältö on melko tarkalleen sama kuin mikä oman tutkimusalani perusta. Ainoa puuttuva palanen, jonka olisin oppikirjalta halunnut, olisi ollut SMT, jota kirjassa ei ilmeisesti käsitellä.
Logiikalla viitataan arkikielessä usein kaikenlaiseen systemaattisen oloiseen päättelyyn, eli prosessiin, jolla tietyistä lähtökohdista tai oletuksista lähtien perustellaan jotakin muuta. Antiikin aikaan logiikalla tarkoitettiinkin lähinnä laadukasta argumentaatiota. Matemaattinen logiikka on periaatteessa joukko abstraktioita, joiden avulla tutkitaan matemaattisen tarkasti, mitä voidaan päätellä ylipäätään. Laskettavuuden teoria nivoutuu yhteen tähän kysymykseen, koska laskettavuus tarkoittaa kysymyksiä siitä miten voidaan päätellä, ja kuinka paljon resursseja (aikaa, muistia, jne) täytyy käyttää jotta päättely voidaan suorittaa loppuun.
Tietojenkäsittelyn ja laskettavuuden teoriaa on joskus vähättelevästi nimitetty "tietokoneohjelmien tutkimiseksi". Tämä on kuitenkin pitkälti virheellinen käsitys asiasta. Pikemminkin kyse on totuuden säilyttävistä siirtymistä erilaisten struktuurien välillä, ja siitä, missä määrin nämä siirtymät on mahdollista toteuttaa ns. normaaleja luonnolakeja noudattavien mekanismien avulla. On esitetty, että ko. ala ei ole "tiedettä", koska siinä ei tutkita mitään tosiasioita, vaan ainoastaan keksitään tai konstruoidaan sellaisia ja sitten tutkitaan näin konstruktioita.
Church-Turingin teesi on eräänlainen paradigmaattinen väittämä, jota pidetään alan jonkinlaisena teoreettisena pohjaoletuksena. Väittämä menee jotakuinkin niin, että jokainen mielekäs laskentaa tai päättelyä tekevä järjestelmä joka on ilmaisu- ja ratkaisuvoimaltaan Turing-vahva, on ekvivalentti Turingin koneen (ja melko suuren joukon muita laskennan malleja) kanssa. Teesi saa jonkin verran vahvistusta siitä, että Chomskyn hierarkia päättyy tyypin nolla kielioppeihin, ja nämä ovat ilmaisuvoimaltaan ekvivalentteja Turingin koneen kanssa.
Päättelyn automatisointi on eräs tärkeä matemaattisen logiikan ja laskettavuuden risteyskohdassa olevaa tutkimusaihetta. Oma tutkimukseni on ollut tällaisen automaattisen päättelyn soveltamista, ja teoreettinen kytkös on melko heikko. Suurimmaksi osaksi työni on keskittynyt tiettyjen modaalilogiikoiden mallintarkastukseen. Mallintarkastus ei viittaa tässä siihen, että rakennetaan malli ja tarkastetaan se (vaikka tällainen tulkinta onkin helppo tehdä, eikä olekaan täysin väärä!), vaan siihen, että tarkastetaan että annettu järjestelmän kuvaus on malli jollekin modaalilogiikan teorialle. Selitän tarkemmin.
Malliteoria toimii logiikassa osapuilleen näin: Meillä on jokin (formaali) logiikan ilmaisutapa. Esimerkiksi ensimmäisen kertaluvun predikaattilogiikka, tai sitten jokin modaalilogiikka tms. Tällä logiikalla ilmaistaan jokin väittämä, eli käytännössä, kirjoitetaan jokin kaava. Olkoon se "p tai q". Kun meillä on tällainen kaava, kaavassa esiintyville symboleille voidaan antaa tulkinta, esimerkiksi "p" tarkoittaa "ulkona sataa" ja q tarkoittaa "ulkona tuulee". Tulkinta on logiikassa se, mitä olen tieteenfilosofiassa nimittänyt operationalisoinniksi. Tulkinta tehdään jonkin struktuurin suhteen; käytännössä tulkinta on kuvaus, joka antaa symboleille merkityksen struktuurissa. Struktuurimme tässä voisi olla esimerkiksi kaksi mittasuuretta: Ensimmäinen on anturi joka rekisteröi sen päälle putoavia sadepisaroita ja toinen mittari, joka mittaa tuulen voimakkuutta. "Sataa" esimerkiksi operationalisoituu niin, että pisaroita tulee 5 sekunnin sisällä vähintään kolme, ja "tuulee" niin, että tuulen nopeus on vähintään 4 metriä sekunnissa. Ulkona vallitseva säätila on jollakin ajanhetkellä malli tälle kaavalle.
Aikalogiikassa on yksinkertaisten propositiosymbolien lisäksi modaalioperaattoreita. Yksi tällainen (jonka avulla voidaan jo ilmaista paljon) voisi olla binäärinen modaalioperaattori "kunnes". "p kunnes q" tulkittaisiin niin, että "tuulee kunnes sataa". Ulkona vallitseva säätila olisi tämän kaavan malli, jos tuuli ei tyynny ennen sadetta. Tätä voidaan soveltaa moneen asiaan, mutta sitä on perinteisesti sovellettu rinnakkaisten ja reaktiivisten järjestelmien spesifioimiseen. Esimerkkispesifikaatioita voisi olla vaikkapa "asiakas odottaa kunnes asiakasta palvellaan" ´ja "asiakasta palvellaan lopulta, jos asiakas odottaa". Mallintarkastuksessa siis selvitetään, päteekö annetun systeemin sisällä annettu kaava.
Mitään periaatteellista syytää rajoittua "konstruktioihin" aikalogiikan ja sitä sivuavien menetelmien kanssa ei kuitenkaan ole. Esimerkiksi probabilistista versiota mallintarkastuksesta on sovellettu systeemibiologiaan. Probabilistisessa versiossa aikalogiikasta on modaalioperaattoreita jotka antavat jonkin väittämän paikkansapitävyydelle todennäköisyyden. Esimerkiksi kaava voi olla muotoa "proteiinin X pitoisuus ylittää kynnysarvon Y todennäköisyydellä p, ennenkuin proteiinin Z pitoisuus laskee alle arvon A". Mallintarkastuksessa rakennetaan tällöin jonkinlainen matemaattinen struktuuri, joka itsessään on operationaalisessa suhteessa tutkittavaan kohteeseen - vaikkapa soluun - ja tämän struktuurin vastaavuutta voidaan empiirisesti arvioida. Konstruktio voidaan tehdä käsin teorian pohjalta tai mallinnos voi olla täysin automaattinen mittaustulosten perusteella. Mallintarkastus antaa joukon hypoteeseja, jotka voidaan myöhemmin falsifikoida empiirisesti itse kohteesta. Takaisinkytkentä malliin voi olla myös täysin automatisoitu.
Opetus jatkuu keväällä tietojenkäsittelyn teorian kurssilla, joka paneutuu logiikan sijaan kompleksisuusteoriaan. Siitä kirjoitan toisella kertaa.
Logiikalla viitataan arkikielessä usein kaikenlaiseen systemaattisen oloiseen päättelyyn, eli prosessiin, jolla tietyistä lähtökohdista tai oletuksista lähtien perustellaan jotakin muuta. Antiikin aikaan logiikalla tarkoitettiinkin lähinnä laadukasta argumentaatiota. Matemaattinen logiikka on periaatteessa joukko abstraktioita, joiden avulla tutkitaan matemaattisen tarkasti, mitä voidaan päätellä ylipäätään. Laskettavuuden teoria nivoutuu yhteen tähän kysymykseen, koska laskettavuus tarkoittaa kysymyksiä siitä miten voidaan päätellä, ja kuinka paljon resursseja (aikaa, muistia, jne) täytyy käyttää jotta päättely voidaan suorittaa loppuun.
Tietojenkäsittelyn ja laskettavuuden teoriaa on joskus vähättelevästi nimitetty "tietokoneohjelmien tutkimiseksi". Tämä on kuitenkin pitkälti virheellinen käsitys asiasta. Pikemminkin kyse on totuuden säilyttävistä siirtymistä erilaisten struktuurien välillä, ja siitä, missä määrin nämä siirtymät on mahdollista toteuttaa ns. normaaleja luonnolakeja noudattavien mekanismien avulla. On esitetty, että ko. ala ei ole "tiedettä", koska siinä ei tutkita mitään tosiasioita, vaan ainoastaan keksitään tai konstruoidaan sellaisia ja sitten tutkitaan näin konstruktioita.
Church-Turingin teesi on eräänlainen paradigmaattinen väittämä, jota pidetään alan jonkinlaisena teoreettisena pohjaoletuksena. Väittämä menee jotakuinkin niin, että jokainen mielekäs laskentaa tai päättelyä tekevä järjestelmä joka on ilmaisu- ja ratkaisuvoimaltaan Turing-vahva, on ekvivalentti Turingin koneen (ja melko suuren joukon muita laskennan malleja) kanssa. Teesi saa jonkin verran vahvistusta siitä, että Chomskyn hierarkia päättyy tyypin nolla kielioppeihin, ja nämä ovat ilmaisuvoimaltaan ekvivalentteja Turingin koneen kanssa.
Päättelyn automatisointi on eräs tärkeä matemaattisen logiikan ja laskettavuuden risteyskohdassa olevaa tutkimusaihetta. Oma tutkimukseni on ollut tällaisen automaattisen päättelyn soveltamista, ja teoreettinen kytkös on melko heikko. Suurimmaksi osaksi työni on keskittynyt tiettyjen modaalilogiikoiden mallintarkastukseen. Mallintarkastus ei viittaa tässä siihen, että rakennetaan malli ja tarkastetaan se (vaikka tällainen tulkinta onkin helppo tehdä, eikä olekaan täysin väärä!), vaan siihen, että tarkastetaan että annettu järjestelmän kuvaus on malli jollekin modaalilogiikan teorialle. Selitän tarkemmin.
Malliteoria toimii logiikassa osapuilleen näin: Meillä on jokin (formaali) logiikan ilmaisutapa. Esimerkiksi ensimmäisen kertaluvun predikaattilogiikka, tai sitten jokin modaalilogiikka tms. Tällä logiikalla ilmaistaan jokin väittämä, eli käytännössä, kirjoitetaan jokin kaava. Olkoon se "p tai q". Kun meillä on tällainen kaava, kaavassa esiintyville symboleille voidaan antaa tulkinta, esimerkiksi "p" tarkoittaa "ulkona sataa" ja q tarkoittaa "ulkona tuulee". Tulkinta on logiikassa se, mitä olen tieteenfilosofiassa nimittänyt operationalisoinniksi. Tulkinta tehdään jonkin struktuurin suhteen; käytännössä tulkinta on kuvaus, joka antaa symboleille merkityksen struktuurissa. Struktuurimme tässä voisi olla esimerkiksi kaksi mittasuuretta: Ensimmäinen on anturi joka rekisteröi sen päälle putoavia sadepisaroita ja toinen mittari, joka mittaa tuulen voimakkuutta. "Sataa" esimerkiksi operationalisoituu niin, että pisaroita tulee 5 sekunnin sisällä vähintään kolme, ja "tuulee" niin, että tuulen nopeus on vähintään 4 metriä sekunnissa. Ulkona vallitseva säätila on jollakin ajanhetkellä malli tälle kaavalle.
Aikalogiikassa on yksinkertaisten propositiosymbolien lisäksi modaalioperaattoreita. Yksi tällainen (jonka avulla voidaan jo ilmaista paljon) voisi olla binäärinen modaalioperaattori "kunnes". "p kunnes q" tulkittaisiin niin, että "tuulee kunnes sataa". Ulkona vallitseva säätila olisi tämän kaavan malli, jos tuuli ei tyynny ennen sadetta. Tätä voidaan soveltaa moneen asiaan, mutta sitä on perinteisesti sovellettu rinnakkaisten ja reaktiivisten järjestelmien spesifioimiseen. Esimerkkispesifikaatioita voisi olla vaikkapa "asiakas odottaa kunnes asiakasta palvellaan" ´ja "asiakasta palvellaan lopulta, jos asiakas odottaa". Mallintarkastuksessa siis selvitetään, päteekö annetun systeemin sisällä annettu kaava.
Mitään periaatteellista syytää rajoittua "konstruktioihin" aikalogiikan ja sitä sivuavien menetelmien kanssa ei kuitenkaan ole. Esimerkiksi probabilistista versiota mallintarkastuksesta on sovellettu systeemibiologiaan. Probabilistisessa versiossa aikalogiikasta on modaalioperaattoreita jotka antavat jonkin väittämän paikkansapitävyydelle todennäköisyyden. Esimerkiksi kaava voi olla muotoa "proteiinin X pitoisuus ylittää kynnysarvon Y todennäköisyydellä p, ennenkuin proteiinin Z pitoisuus laskee alle arvon A". Mallintarkastuksessa rakennetaan tällöin jonkinlainen matemaattinen struktuuri, joka itsessään on operationaalisessa suhteessa tutkittavaan kohteeseen - vaikkapa soluun - ja tämän struktuurin vastaavuutta voidaan empiirisesti arvioida. Konstruktio voidaan tehdä käsin teorian pohjalta tai mallinnos voi olla täysin automaattinen mittaustulosten perusteella. Mallintarkastus antaa joukon hypoteeseja, jotka voidaan myöhemmin falsifikoida empiirisesti itse kohteesta. Takaisinkytkentä malliin voi olla myös täysin automatisoitu.
Opetus jatkuu keväällä tietojenkäsittelyn teorian kurssilla, joka paneutuu logiikan sijaan kompleksisuusteoriaan. Siitä kirjoitan toisella kertaa.
perjantai 8. kesäkuuta 2012
Peitos.
Peittävyys on käsite, joka esiintyy eri abstraktiotasoilla hyvin samaan tapaan, jopa arkikielessä. Matematiikassa (pistejoukkojen tapauksessa) esimerkiksi kokoelma joukkoja on peite jollekin joukolle, jos kaikki joukon alkiot kuuluvat johonkin kokoelman joukkoon. Useimmissa logiikoissa voidaan myös sanoa, että väittämä A peittää väittämän B jos A on B:n looginen seuraus. Huomatkaa: tämä menee tähän suuntaan totuuden säilyttävässä päättelyss, koska jos A on B:n looginen seuraus, niin A on yleisempi väittämä, siis useammin tosi kuin B.
Kripke-rakenne on modaalilogiikoiden (yleensä aikalogiikka) laskennassa yleensä käytetty malli, joka on periaatteessa graafi, jonka jokaisessa solmussa pätee jokin (esimerkiksi ensimmäisen kertaluokan) logiikan väittämäjoukko eli teoria. Esimerkiksi edellisessä kirjoituksessani käsittelemäni kontrollivuon analyysi voidaan ajatella Kripke-rakenteena, jossa siirrytään tilasta toiseen ja abstraktion määräämät väittämät joko pätevät tai eivät päde.
Rakennetta ei tunneta kokonaan, eikä sitä edes (yleisessä tapauksessa) voida tuntea, koska se voi olla ääretön. Abstraktio toisaalta yleensä takaa, että se on äärellinen. Esimerkiksi tietokoneohjelmaa analysoitaessa malli voidaan rakentaa jokaisella käytettävällä abstraktiotasolla kokonaan, mutta joissain tapauksissa se saattaa olla niin suuri, ettei sitä voi laskea. Tähän on olemassa keinoja, joilla ongelmaa helpotetaan. Yksi näistä on peittävyys.
Peittävyyttä käytetään seuraavalla tavalla: Oletetaan, että päädymme abstraktiin tilaan, jossa pätee väittämä P(x), ja kontrollin tila on a. Symboli "x" tässä nyt viittaa vain yleisesti kaikkeen siihen, mitä osaamme sanoa tilasta. Merkitään tätä parilla (a, P(x)). Tätä varten olemme lisänneet Kripke-rakenteeseemme (emme välttämättä tosiasiassa koskaan tee tätä rakennetta, se on matemaattinen abstraktio, jonka on tarkoitus kuvata prosessin eteneminen, ei välttämättä mikään todellinen ilmiö) uuden tilan. Olemme päätyneet tähän erinäisten vaiheiden kautta alkutilasta. Ja matkalla kontrolli on saattanut kulkea myös tilan a kautta. Tutkimme tilan historian (joka on tallessa joko osittain tai kokonaan) ja löydämme sieltä tilan (a, Q(x)). Jos kuitenkin huomaamme, että Q(x) on P(x):n looginen seuraus, meidän ei tarvitse tutkia pidemmälle, sillä tila (a, Q(x)) peittää tilan (a, P(x)). Siis, kaikki, mitä voimme sanoa voivan tapahtua tilassa (a, P(x)), voi tapahtua myös tilassa (a, Q(x)), koska jälkimmäinen on edellistä yleisempi tapaus. Se on siis abstraktimpi. Jos tila (a, Q(x)) on turvallinen, siis jos siitä ei voi suorittaa mitään virhettä, ei tällaista ole myöskään tilasta (a, P(x)). Kääntäen, jos tilasta (a, P(x)) voidaan tehdä virhe, sellainen voidaan tehdä myös tilasta (a, Q(x)).
Kripke-rakenne on modaalilogiikoiden (yleensä aikalogiikka) laskennassa yleensä käytetty malli, joka on periaatteessa graafi, jonka jokaisessa solmussa pätee jokin (esimerkiksi ensimmäisen kertaluokan) logiikan väittämäjoukko eli teoria. Esimerkiksi edellisessä kirjoituksessani käsittelemäni kontrollivuon analyysi voidaan ajatella Kripke-rakenteena, jossa siirrytään tilasta toiseen ja abstraktion määräämät väittämät joko pätevät tai eivät päde.
Rakennetta ei tunneta kokonaan, eikä sitä edes (yleisessä tapauksessa) voida tuntea, koska se voi olla ääretön. Abstraktio toisaalta yleensä takaa, että se on äärellinen. Esimerkiksi tietokoneohjelmaa analysoitaessa malli voidaan rakentaa jokaisella käytettävällä abstraktiotasolla kokonaan, mutta joissain tapauksissa se saattaa olla niin suuri, ettei sitä voi laskea. Tähän on olemassa keinoja, joilla ongelmaa helpotetaan. Yksi näistä on peittävyys.
Peittävyyttä käytetään seuraavalla tavalla: Oletetaan, että päädymme abstraktiin tilaan, jossa pätee väittämä P(x), ja kontrollin tila on a. Symboli "x" tässä nyt viittaa vain yleisesti kaikkeen siihen, mitä osaamme sanoa tilasta. Merkitään tätä parilla (a, P(x)). Tätä varten olemme lisänneet Kripke-rakenteeseemme (emme välttämättä tosiasiassa koskaan tee tätä rakennetta, se on matemaattinen abstraktio, jonka on tarkoitus kuvata prosessin eteneminen, ei välttämättä mikään todellinen ilmiö) uuden tilan. Olemme päätyneet tähän erinäisten vaiheiden kautta alkutilasta. Ja matkalla kontrolli on saattanut kulkea myös tilan a kautta. Tutkimme tilan historian (joka on tallessa joko osittain tai kokonaan) ja löydämme sieltä tilan (a, Q(x)). Jos kuitenkin huomaamme, että Q(x) on P(x):n looginen seuraus, meidän ei tarvitse tutkia pidemmälle, sillä tila (a, Q(x)) peittää tilan (a, P(x)). Siis, kaikki, mitä voimme sanoa voivan tapahtua tilassa (a, P(x)), voi tapahtua myös tilassa (a, Q(x)), koska jälkimmäinen on edellistä yleisempi tapaus. Se on siis abstraktimpi. Jos tila (a, Q(x)) on turvallinen, siis jos siitä ei voi suorittaa mitään virhettä, ei tällaista ole myöskään tilasta (a, P(x)). Kääntäen, jos tilasta (a, P(x)) voidaan tehdä virhe, sellainen voidaan tehdä myös tilasta (a, Q(x)).
Tilaa:
Blogitekstit (Atom)