Lyhyesti "nichts neues"

Marginal Revolutionin Cowen ottaa kantaa kapealla taloustieteen alalla superstarojen vähyyteen. Lainaus.

I find the diminution of superstars in particular areas not very surprising. As early as the 18th century, David Hume (1742, 135-137) and other writers in the Scottish tradition suggested that, in a given field, the presence of superstars eventually would diminish (Cowen 1998, 75-76). New creators would do tweaks at the margin, but once the fundamental contributions have been made superstars decline in their relative luster.

Taustalla on samantapainen näköharha kuin parissa muussa ilmiössä, eli esimerkiksi evoluution kohdalla on esitetty kysymys, miksi uusia pääjaksoja ei ole kehittynyt enää kambrikauden jälkeen, tai miksi "kaikki suuret keksinnöt" tehtiin jo 1800-luvulla tai varhain 1900-luvulla. En viitsi kommentoida asiaa sen kummemmin, koska luotan lukijoiden kykyyn ekstrapoloida ja olla turvautumatta taikauskoisuuteen.

Olen liian kiireinen kirjoittamaan kovin paljoa, koska syksyn logiikan kurssia varten joudun laatimaan luentomateriaalia mm. tableaux- menetelmistä. Tämän lisäksi olen paininut hieman DFA:n minimoinnin ja mallipohjaisen testauksen kanssa, ja sain vielä aamulla pöydälleni 62 korjattavaa tenttiä.

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.

Sekalaista taas

Vapun jälkeen olen keskittynyt - vaihtelevalla menestyksellä - taas työntekoon ja harrastuksiin. Työni osalta on nyt hiljaisempi vaihe, koska lähetin kolme käsikirjoitusta huhtikuussa ja opetuskausi lähestyy loppuaan.

Kuten olen maininnut, Suomeen paluun jälkeen pojat jatkoivat Taekwondoa paikallisessa seurassa. Seura osoittautui perheystävälliseksi, joten liityimme vaimoni kanssa myös. Vaimoni on harrastanut kyseistä lajia nuorempana SM-tasolla, ja paluu liki kahdenkymmenen vuoden jälkeen osoittautui innostavaksi. Itse olen joitain lajeja kokeillut ja hieman harrastanut myös liki 20 vuotta sitten kun ne olivat muodissa, joten aloittaminen ei tuntunut erityisen hankalalta. Eräs tuttavani varoitti minua että nivelet joutuvat lajissa koville. En ole tätä vielä kokenut; sain kyllä napakan potkun kylkeeni ja loukkasin itseni muutamia viikkoja sitten, mutta toistaiseksi muita loukkaantumisia ei ole ollut.

Ennen eilistä siis, kun harjoittelimme hyppypotkua. Kuten totesin, harjoittelin joskus nuorempana erästä toista lajia. Vaikka perustekniikat ovat erilaisia, niissä on jotain samaa, ja "lihasmuisti" (joka sijaitsee itseasiassa käsittääkseni pikkuaivoissa) ei juuri happane, tietyt liikeradat ikäänkuin ovat automatisoituneet. Valitettavasti lihasten jäntevyys ja venyvyys esimerkiksi eivät ole enää samanlaisia kuin ne olivat 20 vuotta sitten. Treenasimme muutaman suunnilleen itseni ikäisen miehen kanssa potkuja, ja tilanteen "henki" johti siihen että piti yrittää aina potkaista hieman korkeammalla olevaan kohteeseen. Kun lätkä oli hieman oman pääni yläpuolella, siihen osui kyllä "helposti", mutta tunsin repivän kivun takareidessäni. Nyt jalka on melko jäykkä; revähdys ei ollut paha eikä esimerkiksi juurikaan haittaa kävelyä, mutta tietynlainen tuntemus siinä kuitenkin on.

Kirjallisuuden puolella olen ollut hieman jumissa. Otin luettavakseni Kvanttivarkaan, ja vaikka pidän kirjasta, etenemiseni on ollut hidasta. Rajaniemi kirjoittaa preesensissä pitkälti kuvailevaa tekstiä. Scifille tyypillisiä julistuksia ja selityksiä ei juuri ole, vaan miljöö, historia jne, ilmenevät pikku hiljaa pienistä palasista. Tämä pitää mielen virkeänä. Minulla on lainassa myös kirjan jatko-osa, enkä näe syytä ettenkö siirtyisi heti sen kimppuun tämän lopetettuani.

Tutkimusrintamalla on, kuten totesin, kovin hiljaista. Kaksi paperin aihetta minulla on kesällä tai syksyllä kirjoitettavaksi, ja lisäksi olen (heikonlaisesti) ryhtynyt toimeen myös kirjan kirjoittamisen kanssa. Ideana on siis kirjoittaa erään yhteistyökumppanin kanssa kirja yhdestä keskeisestä tutkimusteemasta joka minulla on viimeiset neljä tai viisi vuotta ollut. Ehkä sitten pääsen siitä jo eroon.

Ajattelin kirjoittaa jotain Soininvaaran blogissa velloneesta keskustelusta, eli siitä mitä Euroopan kriisille pitäisi tehdä. Oma näkemykseni on, että Euroopan tilanne muistuttaa kovasti Mundell-Fleming- mallia tilanteessa, jossa pääoman liikkeet ovat (lähes) vapaita. Ideana on siis, että jokaisen yksittäisen maan julkisen sektorin investoinnit ja kulutus valuvat pitkälti rajan yli eivätkä pahemmin nosta työllisyyttä ja paranna taloutta. Krugman oli itseasiassa samaa mieltä mitä tulee yksittäisiin maihin, ja siksi pitäisi koordinoida; velkaelvytystä vaan ei voi, eikä mielestäni ole edes syytä koordinoida, koska se on epäreilua. Likviditeettiansa - jos siinä ollaan - voidaan murtaa rahapolitiikalla, ja se pitäisi tehdä kompensoimalla säästäminen ja korkeat verot pohjoiselle ja löysäämällä etelän "deflaatio"kierrettä. Minua viisaammat talousasiantuntijat varmasti osaisivat kehitellä tähän keinot. En kuitenkaan kannata tätä ennen kuin Etelä saa julkisen taloutensa sellaiselle uralle, josta se ei välittömästi pomppaa entiseen tuhlauslinjaan.

EDIT: Huomasin äskettäin, että Orson Scott Cardin scifiklassikko Ender's Game on filmatisoitu ja saapunee elokuviin kohdakkoin. Jostain syystä tämä kyseinen klassikko on jäänyt lukematta; jos joku lukijoistani pitää sitä hyllyssään, olisin kiinnostunut lainaamaan. Pahoittelen vapaamatkustamista, mutta minulla on jo nyt liikaa kirjoja, joten en haluaisi ostaa sitä. Kirjastossa siihen näyttäisi olevan useita varauksia.