Tiede ja teknologia

Palasin Singaporesta eilen, joten on mahdotonta vielä arvioida luotettavasti, missä määrin olen toipunut aikaerosta. Pitkän reissun ja pakolla valvomisen jälkeen oli suhteellisen helppoa nukkua "normaali" yöuni viime yönä, mutta todellinen haaste tulee ensi yönä kun takana ei ole vastaavaa univelkaa.

Matkani tarkoitus oli tutkimus, ja kirjoitinkin jo edellisessä kirjoituksessani hieman yhdestä aiheesta jota tutkimme. Toinen aihe liittyi tietoturvaan, jossa sovelsimme prosessialgebraa, ja tämä yhteistyö saattaa hyvinkin -- ainakin toivon niin -- johtaa myös lisäyhteistyöhön, joten saatan lähteä uudelle reisulle jo muutaman kuukauden sisällä.

Sosiaalisessa mediassa kiersi muutama päivä Wall Street Journalin artikkeli, jossa kyseenalaistetaan paitsi IPR-järjestelmä myös perinteinen käsitys tieteestä teknologian kantavana voimana.

Artikkelin alkuosa heijastelee pitkälti niitä näkemyksiä joita olen jo vuosikaudet blogissani esitellyt, eli että teknologian kehitys on lopulta melko vähän riippuvainen "positiivisista" kannustimista, kuten patenteista ja muusta väkivallasta, ja enemmänkin kyse on kaupallisten intressien välttämättömyydestä, kilpailun paineesta ja ihmisen luontaisesta kokeilunhalusta. Olen toistanut argumentit moneen kertaan, ja uudelleen toisteleminen on pitkälti turhaa.

Kirjoituksen loppupuolella esitetään argumentti -- oikea minun mielestäni -- että teknisen kehityksen ajuri ei ole tieteellinen metodi ja abstraktit teoreettiset tarkastelut, vaan tarve parannella olemassaolevia ratkaisuja ja päihittää kilpailijat. Tämä on totta, enkä usko että tästä on kovin suurta erimielisyyttä sellaisten ihmisten parissa, jotka ovat edes vähän perehtyneet molempiin -- siis ns perustutkimukseen ja teknologiseen innovointiin.

Kirjoitus syyllistyy kuitenkin melko tavanomaiseen inhimilliseen argumentaatiovirheeseen, nimittäin siihen ajatukseen että jos kohta poliittisesti ja sosiaalisesti hyväksytty yksiviivainen käsitys tieteestä teknologisen kehityksen perusedellytyksenä ja tärkeimpänä sitä edistävänä voimana selvästi on väärä ja puutteellinen, ei tästä seuraa että kausaatio menee tarkalleen päinvastaiseen suuntaan, tai että perustutkimus on turhaa. Yhden yksinkertaistuksen -- eli abstraktion -- osoittautuessa virheelliseksi on nimittäin syytä huomata toinen asia jota olen toitottanut kirjoituksissani vuosia on että abstraktiot ovat aina vääriä. Jos joku on yrittänyt todistaa esimerkiksi jotakin teoreemaa ja esittänyt virheellisen todistuksen joka on uskottu pitkään, ei todistuksessa esiintyvästä virheestä seuraa että teoreema on väärä ja sen negaatio oikea. Tämä on kaikille selvää kun puhutaan jostain muusta, mutta jostain syystä argumentti tuntuu kelpaavan monille kovin helposti aina kun jokin riittävän "syvä totuus" tulee kyseenalaiseksi.  Kirjoitus osuu kuitenkin yhteen ns syvään totuuteen, joka esitetään tekstin lopussa:

The perpetual-innovation machine that feeds economic growth and generates prosperity is not the result of deliberate policy at all, except in a negative sense. Governments cannot dictate either discovery or invention; they can only make sure that they don’t hinder it.

 Tästä en ole lainkaan eri mieltä. Jos ajattelemme taloudellis-sosiaalista "innovaatiotaloutta" tai "innovaatiojärjestelmää", niin erityisestä suomalaisten olisi nyt jo aika huomata tämä. Meillä on tavattoman kankea ja turvonnut koneisto alati niukkenevan julkisen rahan jakamiseen tieteelle ja tutkimukselle. Rahanjaosta päätetään komiteoissa ja työryhmissä ja arvioijat pistävät suunnitelmia paremmuusjärjestykseen, niitä pisteytetään mielivaltaisilla kriteereillä ilman mitään todellista syytä edes uskoa että mekanismi oikeasti kohdentaa rahanjaon tarkoituksenmukaisesti. Itseasiassa, rohkenen väittää, ilman mitään todellista vakuuttavaa syytä uskoa että mikään tapa jakaa rahaa hyödyttäisi.

Perustutkimuksen eli ns. tieteellisen tutkimuksen kohdalla tilanne on monimutkaisempi.Isoja, tieteellisesti mielenkiintoisia projekteja -- ajatellaan vaikka LHC:tä tai avaruusohjelmia -- on vaikea viedä eteenpäin ilman isojen organisaatioiden rahoitusta, ja modernissa maailmassa valtiot ja monikansalliset "sosialistiset" organisaatiota kuten EU, ovat ainoita tahoja joilla on sellaisia resursseja käytössään että tällaisia projekteja voidaan rahoittaa. USA:ssa toki on esimerkiksi yksityisiä avaruusprojekteja, ja tällaisissa onkin lopulta kyse vain tekniikan kehityksestä ja taloudellisista intresseistä -- ei niinkään tieteellisestä kunnianhimosta.

Yksi huti tekstissä on kuitenkin: Deep scientific insights are the fruits that fall from the tree of technological change. Argumentti tällä tasolla tuntuu menevän, että koska käsitys, jonka mukaan tieteellinen teorianmuodostus ja sen vaatima innovointi ei ole pääasiallinen teknisen kehityksen syy, ja koska näillä selvästi on jokin yhteys, täysyy asia olla pikemminkin niin päin, että teknologinen muutos on tieteellisen tiedon lähde.

Tässä nyt ei varmaan ole oikein ymmärretty prosessin käsitettä.

Ensiksikin, on ihan selvää, että kyse on takaisinkytkennästä. On aivan varmaa, että esimerkiksi ilman teknologiaa joka mahdollistaa vaikkapa erittäin matalan paineen pumppaamisen lasiputkeen, ei olisi voitu tutkia plasmaa ja sen ominaisuusksia. Tarkempi mittatekniikka ja koneistus olivat tärkeitä teknologisia edistysaskelia jotta voitiin siirtyä sarjavalmistukseen; näiden teknologisten innovaatioiden ajavana voimana oli todellakin jokin muu kuin perustutkimus. Toinen esimerkki on transistori; Lillenfeld keksi transistorin toimintaperiaatteen jo ennen kvanttimekaniikan kehittymistä tasolle jossa se voitiin selittää kunnolla, ja toisaalta transistorien kehitystyö toi esille lukuisia kvanttimekaanisia ilmiöitä joiden selittäminen sitten vei teoriaa eteenpäin.

Kuitenkin, transistorien ja myöhemmin mikropiirien kehitystyö toimi myös toisin päin. On totta, että kaikenlainen pienimuotoinen optimointi ja säätäminen johtivat ajan oloon transistorien pienenemiseen niin, että nyt puhutaan muutaman atomin kokoluokasta; tämän kehityksen kuluessa on tarvittu kuitenkin kvanttimekaanista ymmärrystä joka on kehittynyt perustutkimuksen ja tämän teknologisen kehityksen yhdistymisestä. Ilman kiinteän olomuodon fysiikan teoreettista kehitystä tähän tuskin olisi pystytty.

Toisaalta, Röntgen, Becquerel ja Curiet olivat kaikki ensisijaisesti tutkijoita joita kiinnosti ionisoiva säteily, sen luonne ja mistä se oli peräisin. Heidän tutkimuksensa oli luonteeltaan kokeellista perustutkimusta, mutta johti paitsi tieteellisiin, myös teknisiin läpimurtoihin. Röntgenkuvaukselle ei ollut esimerkiksi mitään kehittämismahdollisuuksia jonkin olemassaolevan tekniikan pohjalta, koska mikään olemassaoleva laite tai tuote ei tuottanut tarkoituksella säteilyä joka läpäisee joitain aineita ja joitain ei. Näiden tutkimusten seurauksena lähdettiin etsimään useampiakin tieteellisiä -- ja myöhemmin teknisiä -- läpimurtoja mukaanlukien ydinaseet ja myöhemmin ydinvoima.

On selvää, että naivi käsitys jonka mukaan "kun vaan laitamme rahaa tieteelliseen perustutkimukseen, niin saamme paljon keksintöjä" on täysin väärä. Väitän itseasiassa että me emme yksinkertaisesti tiedä mitään ulkoista seikkaa tai mekanismia jolla keksintöjen ja innovaatioiden määrää voidaan lisätä. Toki tiedetään, että näitä voidaan varmasti haitata monin tavoin: autoritäärisellä johtamisella kuten sanelupolitiikalla, kilpailun estämisellä, nepotismilla, ja ennenkaikkea liian vahvalla patentti- ja IPR-järjestelmällä. Todennäköisesti jonkin verran haittaa on siitä, että tutkimussuunnitelmia ylipäätään arvostellaan muutoin kuin selkeyden osalta; että rahaa jaetaan projekteille jotka ovat poliittisesti suosittuja (tämä mahdollistaa lahjakkaimpien yksilöiden palkkaamiseen huonoihin projekteihin); että patenttisuojaus ylipäätään on mahdollista.

Todennäköisesti hyödyttömiä, mutta myös todennäköisesti harmittomia keinoja, ovat massiivisten ihmisjoukkojen koulutus (tästä voi olla haittaa jos se sitoo muita resursseja, mutta voi myös olla marginaalinen hyöty jos joku riittävän luova mutta laiska ihminen tulee hankkineeksi tietoa jota voi hyödyntää), innovaatioiden julkinen rahoittaminen tyyliin TEKES ja vastaavat, ja perustutkimuksen massiivinen rahoittaminen suoraan nykyisessä mittakaavassa. Sanon tämän nyt näin: Siis, uskon että ns perustutkimuksen mittava rahoittaminen ei ainakaan Suomen kokoisessa maassa ole perusteltavissa sillä, että se ajaisi suomalaista taloudellisesti merkittävää innovointia suuressa määrin. Tämä tarkoittaa, että marginaalinen euro joka laitetaan tieteelliseen perustutkimukseen, tuskin tulee takaisin marginaalisena eurona kansantuotteessa parempien innovaatioiden ansiosta. Nettovaikutus voi olla toki positiivinen, mutta se on pienempi kuin yleisesti kuvitellaan.

On syytä korostaa nyt heti, että tämä ei ole argumentti perustutkimuksen rahoitusta vastaan. Perustutkimuksesta voi olla hyötyä, ja todennäköisesti on, monella muulla tavalla. Tällä on tarkoitus sanoa, että syy rahoittamiselle ei pitäisi olla uskomus että perustutkimuksen rahoittaminen tuottaa parempaa tuotekehitystä yrityksissä, koska tämä uskomus on todennäköisesti väärä.

On myös syytä huomata, että mikäli uskomme ylläolevan, niin tärkeämpää kuin rahan syytäminen poliitikkojen ja byrokraattien lemmikkiprojekteihin, olisi esteiden purkaminen. Tässä ei olla ihan niin huonoja kuin voisi kuvitella, eikä tässä toimita niin huonosti kuin usein ehkä kirjoituksistani saa käsityksen. Jos ja kun rahoitetaan asioita jotka liittyvät tutkimukseen ja innovointiin, niin yksi kohta missä tätä voidaan todennäköisimmin tarkoituksenmukaisimmin tehdä, on infrastruktuurin kehittäminen. Tahtoo sanoa, että on mielekästä että on tiloja, laitteita, ja mahdollisuuksia käyttää näitä juuri sellaisella tavalla joka tuottaa todennäköisemmin tulosta.

Esimerkiksi joissakin yliopistoissa -- myös Suomessa -- on alettu perustaa opiskelijoille erilaisia protopajoja joissa nämä voivat melko halvoilla laitteilla rakennella prototyyppejä ja "leikkiä" tietyn osan ajasta tekniikalla ja tutkia sen mahdollisuuksia. On myös lähdetty enemmän avaamaan ovia elinkeinoelämän suuntaan niin, että nimenomaan ne taidot joita tarvitaan tällaiseen "näpertelyyn" saavat enemmän tilaa ja toisaalta tutkijoiden näpertelyn kohteeksi saadaan enemmän sellaisia teknisiä haasteita joita ns todellisessa maailmassa voidaan ratkaista.

Omassa työssäni esimerkiksi mahdollisuudet tällaiseen ovat hyvin suuret. En pidä itseäni "insinöörinä", "tietojenkäsittelijänä" enkä "matemaatikkona", vaan Nassim Talebin tapaan pidän itseäni enemmän epistemologina; tutkin sitä mitä voimme tietää. Perustutkimuksen tulokset ovat minulle tutkimuksen kohteita, ja oma mielenkiintoni kohdistuu siihen, millaisia abstraktioita "todellisesta" maailmasta voidaan tehdä. Tämän mielenkiintoni ohjaamana osallistun kolleegoideni näpertelyyn. Käymme läpi jotakin teknistä ratkaisua joka pyrkii löytämään "virheen" eli tilanteen jossa järjestelmän käyttäytyminen poikkeaa toivotusta. Oma mielenkiintoni ja ajatteluni kohdistuu enemmän siihen "miten voimme tietää" tai "mitä voimme tietää", mutta koska tieto on merkityksellistä vain jossakin konkreettisen asian tietämisessä, pyrin aina kysymään tämän kysymyksen juuri siinä kontekstissa ja käsillä olevan ongelman ehdoilla, joten minun täytyy toistuvasti "liata käteni".  Myönnnän että Taleb on suuresti vaikuttanut ajatteluuni tässä suhteessa. Kuten Taleb, minäkin tunnen suurta vetoa stoalaisuutta kohtaan.

Talebin tapaan, innovaatiopolitiikan (jos sellaista ylipäätään on järkeä olla) pitäisi olla "antifragiilia". Perustutkimuksen metodologian -- samoin kuin teknologisen kehityksen -- voidaan ideaalisesti ajatelle nimenomaan vahvistuvan kaikenlaisista shokeista ja yllätyksistä joita se kohtaa. Haasteet, virheet, puutteet, uudet ja yllättävät ilmöit, jne, nämä vievät tutkimusta eteenpäin.

Induktio.

Mallintarkastus (model checking) tarkoittaa tekniikkaa, jossa jonkin järjestelmän virheettömyys osoitetaan ns. malliteoreettisella argumentilla. Jos meillä on järjestelmä M ja ominaisuus P, niin mallintarkastus pyrkii toteamaan, päteekö M |= P, eli että järjestelmän kuvaus M on ominaisuuden P malli. 

Vaihtoehtoja järjestelmän mallille on monia, samoin ominaisuus voi olla monella eri tavalla esitetty. Niin kutsutussa eksplisiittisessä mallintarkastuksessa järjestelmä esitetään tilakoneena tms, jonka kaikki tilat tutkitaan ja tarkastetaan että ominaisuus P pätee, tai sitten löydetään virhe, eli jokin järjestelmän suoritus jossa P rikkoutuu.

Symbolisesta mallintarkastuksesta puhutaan usein silloin, kun järjestelmä on esitetty symbolisesti, eli esimerkiksi jonkinlaisten logiikan kaavojen tms avulla siten, että yksittäiselle tilalle ei välttämättä ole mitään esitystä. Symbolinen mallintarkastus oli suosittua 80- ja 90-luvulla ns. binääristen päätöskaavioiden (BDD) ansiosta.  BDD kykenee esittämään joukon järjestelmän tiloja kompaktisti, jos järjestelmä on riittävän säännönmukainen. Järjestelmän tilasiirtymät esitetään symbolisesti loogisena funktiona T ja kun meillä on jokin joukko tiloja S (esitetty esimerkiksi BDD:n avulla), T(S) kuvaa ne tilat joihin voidaan päätyä jos tehdään siirtymiä joukosta S.  Kun BDD:ille on annettu jokin kanoninen esitystapa, niin kahden BDD:n ekvivalenssi on helppo laskea, samoin implikaatio -- eli käytännössä osajoukkorelaatio. Jos T(S) on S:n osajoukko, niin sanomme että S on kiintopiste eli ns. fixed point. Tämä tarkoittaa sitä, että jos tiedämme järjestelmän olevan jossakin S:n tilassa, ja T(S) on S:n osajoukko, niin tiedämme että S sisältää kaikki sellaiset tilat johon järjestelmä voi ylipäätään päätyä.

90-luvun lopulla alkoi tapahtua tietojenkäsittelyssä, kun yhtä aikaa tietokoneet olivat tulleet nopeammiksi ja tehokkaammiksi, ja toisaalta algoritmit kehittyneet. Tunnettu NP-täydellinen ongelma on niin sanottu SAT-ongelma. SAT tarkoittaa ongelmaa, jossa jos meille on annettu propositiologiikan kaava X, niin kysytään, voidaanko propositioille löytää sellaiset arvot että kaava on tosi. Huolimatta ongelman NP-täydellisyydestä, valtavan moni yksittäinen SAT-ongelma itseasiassa ratkeaa hyvinkin tehokkaasti, eli patologiset tapaukset ovat varsin harvinaisia. Armin Biere ja muutama muu keksivät mallintaa järjestelmän propositiologiikan avulla ja keksivät ns. rajoitetun mallintarkastuksen (Bounded Model Checking,BMC). Siinä järjestelmän toiminta esitetään tiettyyn askelmäärärajaan k asti propositiologiikan kaavana X(k), ja tarkastettava ominaisuus P esitetään myös kaavana, ja kysytään, onko kaava (X(k) & !P) SAT instanssi. Jos se on, niin olemme löytäneet virheen, jos ei, niin olemme osoittaneet että virhettä ei ole ensimmäisen k-askeleen jälkeen.

BMC:n ongelma on, että kaavan pituus kasvaa koko ajan eikä siinä sellaisenaan ole mitään fixed point- karakterisointia. Jokainen askel tuo kaavaan lisää muuttujia, ja sitäpaitsi, järjestelmän toiminta voi hyvinkin olla ääretön, jolloin mitään kiintopistettä ei edes teoriassa voi löytää.

Ken McMillan ja muutamat muut keksivät jossain kohtaa soveltaa ns. Craigin interpolantteja BMC:hen. Interpolantti toimii suunnilleen niin, että jos meillä on kaava A & B, joka ei ole SAT, eli se on ristiriitainen, niin löytyy kaava I (vasen interpolantti), jolla on ominaisuudet 1) A => I, 2) I & B ei ole SAT ja 3) I:ssä esiintyy vain sellaisia propositioita jotka ovat yhteisiä A:lle ja B:lle.  Oikea interpolantti olisi symmetrisesti sellainen jossa B => I jne.

Kun järjestelmän toimintaa mallinnetaan jollakin kaavalla, erityisesti, jos A on kaava joka sisältää sekä propositioita joiden on tarkoitus kuvata tiloja että propositioita jotka kuvaavat transitioiden ominaisuuksia ja B kuvaa pelkästään tilojen ominaisuuksia, niin interpolantti esittää jonkin joukon tiloja. Koska A => I pätee, niin ne tilat joista A puhuu, muodostavat niiden tilojen osajoukon joista I puhuu. I on tietyssä mielessä abstraktio joka vangitsee A:n tiloista jotain siitä miksi A & B ei ole SAT. Koska A kuvaa järjestelmän suoritusta johonkin rajaan asti, I on eräänlainen selitys sille, miksi A ei sisällä virhettä. 

Vedän tässä hieman oikoiseksi mutkia, mutta jos suoritamme BMC:tä johonkin rajaan k asti, emmekä löydä virhettä, niin X(k) & !P ei ole SAT. Jos tässä kohtaa etsimme interpolantin I, niin I & !P ei ole SAT ja I esittää joukon tiloja. Kun käytämme propositio- tai predikaattilogiikkaa tilasiirtymien esittämiseen, joudumme aina esittämään joka askelella uusia muuttujia. Jos meillä on joukko muuttujia V, niin tilasiirtymät esitetään kaavalla T(V,V') niin, että joukon V' muuttujat kuvaavat muuttujien arvoja tämän siirtymän jälkeen. Koska interpolantti I esittää myöskin joukon tiloja, yleensä ajattelemme että se on muotoa I(V), mutta V':n muuttujia siinä ei tietenkään esiinny.  Kaava (I(V) & T(V,V')) kuvaa sitä joukkoa tiloja joihin päästään jos lähtötiloina ovat tarkalleen ne tilat joissa pätee I(V). Nyt, jos (I(V) & T(V,V')) implikoi kaavan I(V'), niin olemme itseasiassa löytäneet jällleen kiintopisteen.  Sanotaan myös, että I on induktiivinen relaation T(V,V') suhteen.

Ilman BDD:itäkin mallintarkastus voidaan siis tehdä sellaiseksi että se myös voi todistaa järjestelmän oikeaksi kokonaan, ei vain johonkin rajaan saakka, jos löydämme induktiivisen interpolantin. Voimme tällöin jakaa mallintarkastuksen kolmeen vaiheeseen: 1) Meidän pitää löytää kaava joka esittää jonkin joukon tiloja joista ainakin osaan alkutilasta voidaan päästä, 2) Virheen ja kaavan konjunktion pitää olla ristiriitainen 3) Kaavan pitää olla induktiivinen tilasiirtymärelaation suhteen. BMC-pohjainen mallintarkastus lähtee alkutilasta ja kasvattaa kaavaa johonkin rajaan asti, tämän jälkeen se muodostaa interpolantin. Tämä prosessi takaa että kaksi ensimmäistä ominaisuutta toteutuvat, mutta induktiivisuutta se ei takaa.

Niin sanottu CEGAR (counterexample-guided abstraction refinement) taas perustuu ajatukseen, että tutkimme koko ajan kaavaa joka on sekä induktiivinen että sisältää alkutilan. Alussa tällainen kaava on tautologinen, ja esittää siten kaikkien mahdollisten (ja mahdottomien) tilojen joukon. Se kuitenkin esittää myös virheen. Kaava on siis "liian abstrakti" eikä ota huomioon järjestelmän toiminnan rajoitteita. Algoritmi toimii niin, että tähän reagoidaan lisäämällä jokin rajoite joka varmasti on voimassa transitiorelaatiossa, ja joka ei riko induktiivisuutta, ja tarkastetaan uudelleen. Tässä rikon hieman rajoja, koska näen prosessit samoina, oli kyse sitten eksplisiittisestä tai symbolisesta mallintarkastuksesta. Minulla kesti melkein 14 vuotta ymmärtää että sillä ei ole oikeastaan tässä kohtaa mitään merkitystä; Eksplisiittinen mallintarkastus tavallaan perustuu siihen että järjestelmänkuvauksesta tutkittavana oleva osa on aina "induktiivinen", se vain on niin suuri ettei sitä voida kokonaan tarkastella. Abstraktiolla tuotetaan pienempi malli joka on takuulla induktiivinen mutta saattaa tuoda virhetilan vahingossa malliin.

Kaikkien kaavojen joukossa, joita voimme muodostaa -- tämä on hyvinmääritelty, jos kohta ääretön joukko -- annetun järjestelmän atomisista ominaisuuksista, on mielenkiintoinen rakenne malliteoreettisessa ja algebrallisessa mielessä. Tässä kohtaa olen hyvin mielissäni, että sain opettaa pari vuotta matemaattista logiikkaa,  kumpa olisin saanut tehdä niin jo vuosia aiemmin, olisin ymmärtänyt tämän jo ennen kuin matalalla roikkuvat hedelmät aihepiiristä oli poimittu. Nimittäin, kaavoilla on ns. hilarakenne. Otetaan kaavojen sijaan niiden ekvivalenssiluokat, eli samastetaan kaavat jotka ovat loogisesti yhtäpitäviä. Hilassa on maksimaalinen ja minimaalinen alkio: Identtisesti todet kaavat ja identtisesti epätodet kaavat, eli [T] ja [F].  Osittaisjärjestyrelaationa on se, että jos [P => Q] = [T], niin P < Q.  Kahdella kaavalla A ja B on supremum, [A || B] (A or B) ja infimum [A && B].

Tässä hilassa on monta mielenkiintoista alihilaa. Esimerkiksi jos T(V,V') -- transitiorelaatio -- on fiksattu, niin induktiivisten kaavojen joukko muodostaa alihilan: Sekä True että False ovat induktiivisia, mikä ei ole vaikea todistaa. Myös kahden induktiivisen kaavan disjunktio ja konjunktio ovat induktiivisia. Negaatio ei ole induktiivinen yleisessä tapauksessa, mutta negaation suhteen suljettujen induktiivisten kaavojen joukko on itsessään tämän alihilan alihila, ja se ei ole vaike nähdä myöskään; kyseinen alihila sisältää aina vähintäänkin kaavat True ja False (jotka ovat siis toistensa negaatioita). Joka tapauksessa, merkitään T(V,V'):n suhteen induktiivisten kaavojen alihilaa IL(T).

Ja tästä -- anteeksi pitkä johdanto -- pääsemmekin mielenkiintoiseen asiaan, eli siihen, miten T(V,V') vaikuttaa tähän hilarakenteeseen jos voimme "häiritä" sitä. Nimittäin, oma erikoisalani osittaisjärjestyreduktio (POR, partial order reduction) toimii niin, että tietyissä oloissa voimme eliminoida joitakin transitioita järjestelmästä. Käytännössä tämä tarkoittaa, että luomme kaavan R(V,V') jolla on se ominaisuus että R(V,V') => T(V,V') ja että M(T) |= P jos ja vain jos M(R) |= P. Tässä siis M(T) viittaa malliin joka on rakennettu käyttäen relaatiota T ja M(R) käyttäen relaatiota R.

Kansanviisaus alalla on sanonut, että POR on hyödyllistä eksplisiittisessä mallintarkastuksessa, muttei juurikaan symbolisessa. Kaiken muun huvittavan lisäksi, niiltä osin kun sitä on symbolisessa mallintarkastuksessa ylipäätään käytetty, sen on ajateltu soveltuvan vain asyklisten järjestelmien mallintarkastukseen, koska syklisyys aiheuttaa tietyissä tilanteissa ongelmia oikeellisuuden kannalta. Tämä ongelma kuitenkin ratkaistiin vajaa vuosi sitten käytännössä kokonaan uudella tavalla, jota en nyt tässä ala referoimaan, ja tämä tapa poisti käytännössä ongelman kokonaan.

On helppo todistaa, että jos R(V,V') on rajoittavampi kaava kuin T(V,V'), IL(T) on IL(R):n alihila. Se, mitä aiomme nyt seuraavaksi tehdä, on tutkia jos voisimme löytää IL(R)-alihilalle (tai sen jollekin alihilalle) joukon eräänlaisia kanta-alkoita, joita yhdistämällä konjunktiivisesti ja disjunktiivisesti voimme löytää sellaisen induktiivisen kaavan, joka sisältää alkutilan mutta ei sisällä virhetilaa, ja, jonka avulla vielä voisimme nopeasti löytää todisteet sille että tällaista kaavaa ei ole, mikäli tämä todella on tilanne.

Mokutus.

Lähdin eilen hetken mielijohteesta kiinalaisen työkaverin kanssa pelaamaan sulkapalloa. Seurueessa oli romanialainen mies, (itä)saksalainen pariskunta, kaksi kiinalaista ja minä. Myöhemmin illalliselle joukkoon liittyi myös yksi turkkilainen.

Kiinalaiset kertoivat vitsin. Ulkoavaruudesta kotoisin oleva muukalainen tekee pakkolaskun Kiinaan. Jos hän laskeutuu Pekingiin, paikalliset täyttävät ja balsamoivat muukalaisen ja laittavat museoon näytille. Jos hän laskeutuu Shanghaihin, paikalliset pukevat muukalaisen koreaksi ja myyvät tämän torilla eniten tarjoavalle. Jos hän laskeutuu Kantoniin, paikalliset laittavat muukalaisesta herkullisen aterian. Kiinlainen kulttuuri ei ole minulla niin tuttu, että olisin osannut arvostaa vitsin nyansseja, mutta vitsin kertoja oli Pekingistä ja toinen Shanghaista, ja kumpikin oli sitä mieltä että vitsi on hauska. Yhtään kantoninkiinalaista en tavoittanut kysyäkseni mielipidettä.

Päädyimme illalliselle Arabikadulle (kirjaimellisesti, Arab Street). Kadun päässä on melko suuri ja uusi, koreasti valaistu ja kullatuin (??) kupolein varustettu moskeija, josta iltasella kuului rukouskutsua. Kaikki varmasti tietävät mitä tarkoitan, muuan Teuvo Hakkarainen (ps) teki tunnetuksi kyseisen joikun. 

Matkalla illalliselle taksikuskinamme oli joviaali kiinalaismies, joka selitti että hänen tyttärensä on lentoemäntänä Finnairilla ja hänen poikansa opiskelee kirjanpitäjäksi. Itse mies oli asunut Japanissa ja ties missä, ja höpötti kaiken aikaa. Hän intoili siitä, miten hienoa on se, että Singapore on monikulttuurinen yhteiskunta. Hänenkin tyttärensä, ajatelkaa, Finnairilla. Fazerin suklaa on kuulemma parasta suklaata maailmassa, ja hän on samaa mieltä. Hän myös uumoili, että korkean teknologian tiedemiehenä (you a High Tech Scientist!) minä varmasti tienaan Suomessa paljon, koska Suomessa kaikkien täytyy olla suunnattoman rikkaita. Koetin selittää, että Singapore on itseasiassa vauraampi maa kuin Suomi, mutta hän totesi että täällä vain valtio ja muutamat tyypit ovat rikkaita. Mutta myönsi että taksikuskikin tulee ihan hyvin toimeen ja hänen lapsensa voivat tehdä mitä tahansa. Vaikka päätyä lentoemännäksi Finnairille!

Olisin halunnut Arabikadulla ravintolaan jossa olisimme saaneet shawarmaa, mutta istuimme sitten turkkilaisen ravintolan terassille. Seuraamme liittynyt turkkilaismies oli verraten rasittava ekstrovertti joka uskoi tietävänsä kaikesta kaiken. Selitti käyvänsä Burning Manissä joka vuosi ja tuntevansa kaikki turkkilaiset Singaporessa. Tai siis ainakin hänen setänsä tuntee. Ja kuuntelevansa joka aamu sotaisaa heavymetallia ja voittavansa joka päivä. Ja ihailevansa Vladimir Putinia -- onhan miehellä "musta vyö Taekwondossa" (sic). En edes jaksanut alkaa korjailla hänen täydellisellä varmuudella laukomiaan konfabulaatioita, vaan lähdin leikkiin mukaan ja vastasin, että uskon että Putin on kova jätkä kun hän kyykkää ja vetää maasta yli 250 kiloa. Myös venäläisten "homopropagandan" vastaisia toimia kommentoin että uumoilen Putinin vain haluavan estää kilpailevan homopropagandan, sillä kun katsoo hänen kuviaan, ei voi olla ajattelematta että ei niitä heteroyleisölle ole suunnattu.

Arabikadun väkijoukko oli pääosin eurooppalaisen näköistä. Kävin Seven-Elevenissä ostamassa (vihdoin) sim-kortin puhelimeeni ja edessäni kassalla oli nuori lyhyenläntä vaalea mies jonka luottokortti ei kelvannut maksuvälineeksi. Mies oli hämmentyneen oloinen, ja totesin hänell, että ota ostoksesi, minä maksan. Loppusumma oli vain yhden dollarin -- mies oli ostamassa pähkinöitä tai jotain.

Lämmöllä.

Saavuin Singaporeen lauantaina, lähdettyäni perjantaina illalla Suomesta. Yö jonka vietin lennolla oli lyhyt -- viisi tuntia lyhyempi kuin normaalisti -- ja laskeuduimme noin kello 16. Lentoaika oli "vain" vajaa 11 tuntia, ilmeisesti suotuisien tuuliolosuhteiden ansiosta.

Singapore kärsii tällä hetkellä Sumatran metsäpaloista. Iso osa -- tarkkaa osuutta en tunne, mutta se ei ole 100% -- metsäpaloista johtuu kaskiviljelystä. Eräs tuttavani kommentoi ilmansaastetilannetta toteamalla että libertaarien pitäisi tulla käymään Singaporessa ja tutustua ulkoisvaikutuksen konkreettiseen merkitykseen. Tilannetta on vaikea korjata Coaselaisittain, koska vaikka tehtäisiin sopimus yksittäisen maanviljelijän kanssa kompensaatiosta joka maksetaan jotta tämä ei polta metsää, tästä syntyy entistä suurempi insentiivi jollekulle muulle polttaa metsää, ja metsäpalot usein riistäytyvät hallinnasta.

Ilmanlaadun heikkous on hyvin konkreettinen asia. Savun haistaa toisinaan ilmassa, ja näkyvyys kaupungin yli on heikko. Urheilutapahtumia on peruttu ja joinakin päivinä myös esimerkiksi uima-altaita on pidetty suljettuna, koska liikunta ulkosalla on epäterveellistä suuren hiukkaspitoisuuden vuoksi.

Kuntosali joka majoitukseeni sisältyy, on tavattoman ankea. Siellä on vain smith-kone, jolla ei oikeasti voi kyykätä niinkuin kuuluisi. Tämän lisäksi siellä on käsipainoja joista painavimmat ovat 25kg ja kahvakuulia joista painavimmat ovat 24kg. Maastavetoa ei siis voi tehdä käytännössä ollenkaan. Opiskelijakäytössä on kuntosali, jossa ilmeisesti on räkkejä -- nuoret miehet roudaavat penkit ja räkit iltapäivisin ulos uimakompleksin viereen ja nostelevat siellä painoja. Virallisten ohjeiden mukaan ko. sali on kuitenkin vain henkilökunnan ja opiskelijoiden käytössä ja säännöissä lukee erikseen että "visitors are not allowed".

Ensimmäinen yö oli vaikea. Väsymyksen vuoksi nukahdin helposti noin kello 9 illalla paikallista aikaa -- eli neljältä iltapäivällä Suomen aikaa -- mutta heräsin noin kello 1 aamuyöstä, enkä saanut nukuttua juurikaan. Seuraavat kaksi yötä nukuin hyvin, mutta neljäntenä yönä sama ilmiö toistui. Viidennen yön  nukuin hyvin ja koin sopeutuneeni, mutta kuudes yö oli jälleen katkonainen. Alan epäilemään, että syy ei olekaan aikaeroväsymyksessä, vaan on yhdistelmä muuttunutta ruokavaliota ja huonompaa liikuntaa. Ja toki ehkä ilmastoa.

Syön enemmän hiilihydraatteja, koska täällä on riisiä joka paikassa ja se on hyvää. Annokset ovat -- onneksi -- pienempiä kuin mihin olen Suomessa tottunut. Syön myös aamiaisen. Proteiininsaantini on todennäköisesti alle puolet, tai jopa kolmannes siitä, mitä Suomessa. Tämä kuulostaa rajulta pudotukselta, mutta Suomessa söin aivan liian proteiinipitoisesti; päivän energiasta toisinaan jopa 40% tuli proteiinista, jota sain 200-300 grammaakin välillä päivän mittaan, keskimäärin ehkä hieman alle 200. Aivan liikaa. Täällä arvioisin että proteiininsaantini on korkeintaan 100g päivässä, todennäköisesti selvästi alle sen.  Suurin syy tähän on rahkan ja juuston lähes täydellinen puuttuminen paikallisesta ruokavaliosta. Maitoa en (Plus Kaakaojuomaa lukuunottamatta) Suomessakaan ole juonut muutoin kuin kahvissa.

Singaporessa on melko tavanomaista, että ihmiset käyttävät työpaikalla melko lämpimiä vaatteita, sillä jostain syystä toimistotilat viilennetään ilmastoinnilla melko kylmiksi. Ulkona on tukalaa käytännössä missä tahansa muussa vaatetuksessa kuin sortsit + t-paita (siinäkin jos on suorassa auringonvalossa), mutta sisätiloissa on tällaisella varustuksella varsin kylmä.