perjantai 30. syyskuuta 2011

Akatemia vs tohtori, erä II.

Kun trance tyylilajina todella löi läpi joskus 90-luvun loppupuoliskolla, olin jo vähän ikäänkuin kyllästynyt siihen. Tai oikeastaan, olin olevinani liian cool digatakseni musiikista, jonka keskeinen funktio oli verraten primitiivisten emotionaalisten reaktioiden aikaansaaminen. Pushin "Universal Nation" on sikäli hassu kappale, että se on aivan tavattoman yksinkertainen, ja silti kovin tehokas tässä suhteessa. En tiedä miten muut sen kokevat, mutta minusta kappaleessa on jonkinlainen jatkuvan kriisin tai takaa-ajon tunnelma. Mieli- ja muistikuvissani kuulen sen aina varsinaisen tanssisalin ulkopuolelta, kädet hikoillen, hermostuneena miettien, tuleeko tänään klubille tarpeeksi maksavaa porukkaa, jotta laskut saadaan maksettua, vetääkö joku vessassa överit tai palaako paikka.

Jostain syystä akatemiahakemusta tehdessäni minulle tulee myös tämä kappale mieleen. Jätin hakemuksen juuri äsken. Tämä on viimeinen mahdollisuuteni saada tutkijatohtorin rahoitus. Mikäli saisin sen, voisin keskittyä seuraavat kolme vuotta tutkimaan, ja voisin jopa julkaista papereita. Alallamme on nimittäin sellainen kummallinen kulttuuri, että lehtijulkaiseminen ei tuo lainkaan näkyvyyttä eikä pahemmin viittauksia, vaan arvostetuimmat kanavat ovat muutama tärkein konferenssi. Koska en enää salaile alaani, voin pari mainita, eli Tools and Algorithms for Construction and Analysis of Systems, eli tuttavallisemmin TACAS (olen kerran julkaissut täällä) ja Computer Aided Verification (ei julkaisuja) ovat parhaat, itselleni sopivista Concurrency Theory tulee jossain selvästi perässä (1 julkaisu) ja APN jo aika kaukana (2 julkaisua). Näitä voi pitää "korkean profiilin" julkaisuinani. Sitten on kymmenkunta B-luokan julkaisua, joilla voisi periaatteessa vaikka pyyhkiä per...ussuomalaisten ruokapöytää. Jollakin tavalla vaikeasti arvioitava on vielä Quantitative Evaluation of SysTems, eli QEST, joka on pääasiallinen kvantitatiivisen mallintarkastuksen pääfoorumi; siellä julkaiseminen on helpompaa, mutta keskimäärin viittausten määrä on suurempi kuin monissa muuten "paremmissa" julkaisukanavissa.

Viime vuonna akatemian arvioijat itseasiassa pitivät, itselleni yllättäen, julkaisuluettelotani hyvinkin solidina ja vakuuttavana. Ihmettelen sitä hieman, mutta nämä ovat todennäköisesti tyyppejä, jotka ovat alan oikeita asiantuntijoita, ja tietävät, että esimerkiksi TACAS:in hyväksymisprosentti on pahimpina vuosina alle kymmenen, ja CONCURissakin alle kaksikymmentä. Se ei tietenkään vielä kerro mitään. Omituisinta hylkäyksessä oli se, että eniten pisteytystä laskevaksi tekijäksi oli mainittu se, että suunnitelmani oli liian kansainvälinen, siis koska minulla ei ole omaa tutkimusryhmää, ja koska olen osoittanut tekeväni paljon kansainvälistä yhteistyötä, ei ole järkeä rahoittaa työskentelyäni Suomessa. Logiikka ei oikein auennut minulle, mutta koetin korjata tämän asian tänä vuonna. Olen varma kylläkin, että sekin menee pieleen.

Olen tapellut myös revisioitavan lehtiartikkelin kanssa. (Tämä on muuten periaatteessa sama paperi, joka hylättiin liian teoreettisena) Positiivisen arvion antanut pyysi tarkennosta erään todistuksen tekniikkaan, koska argumentti ei ollut aivan ehkä. Mikä olikin hyvä idea, koska argumentissa oli supikoiran mentävä reikä. Tulos on kyllä oikein, mutta eräs ei-triviaali tapaus ei tullut alkuperäisessä todistuksessa käsitellyksi. Koen jotenkin niin, että jos paperi olisi suoraan hylätty tällaisen perusteen vuoksi, olisin ollut suorastaan tyytyväinen, koska vertaisarvioinnin tehtävä on juuri virheiden löytäminen. Sensijaan se keskittyy nykyään aivan liiaksi siihen viimekädessä täysin mielivaltaiseen sosiaaliseen aspektiin, onko tulos riittävän mielenkiintoinen tullakseen julkaistuksi. Ymmärrän, että tämä on olennaista, mutta jos meillä on teoreettinen tulos, joka ei ole triviaali todistaa, ja sitä tarjotaan asiaankuuluvaan foorumiin, niin en oikein ymmärrä miksi tämä olisi keskeistä.

Jo sen todistus, että toinen menetelmistä toimii, on nykyisellään yli kolmen sivun mittainen. On totta, että sen jälkeen keskeisen ekvivalenssituloksen todistus ei ole kummoinenkaan, mutta tätä voi verrata niihin neutriinojen nopeusmittauksiin. Ei sellaistakaan tulosta ohiteta siksi, että itse koe kesti mikrosekunnin osia, kun mittalaitteiden rakentaminen ja kalibrointi kesti useita vuosia.

7 kommenttia:

Kumitonttu kirjoitti...

Jo sen todistus, että toinen menetelmistä toimii, on nykyisellään yli kolmen sivun mittainen.

Mikä laskutoimitus antaa tulokseksi kolme liuskaa numeroita? Maailmankaikkeuden atomeitako sun ohjelma laski?

Tiedemies kirjoitti...

Ei tässä ole kyse laskennasta siten kuin perinteisesti ymmärretään. Kyse on siitä, että meillä on matemaattinen struktuuri M, ja meillä on kuvaus T, joka tuottaa toisen struktuurin. Lisäksi meillä on ominaisuusluokka X, ja X[M] on niiden tämän luokan ominaisuuksien joukko, jotka M:lle pätevät.

Todistus on siis päättely, jossa näiden struktuurien ja kuvausten ominaisuuksiin vedoten osoitetaan, että X[M] = X[T(M)]. Mistään numeroista ei ole kyse, vaan loogisten yhteyksien osoittamisesta.

Tiedemies kirjoitti...

On siinä tietysti numeroista kyse lopulta, koska malli on Markovin päätösprosessi eli MDP. Kun järjestelmä kuvataan MDP:llä, voidaan arvioida tiettyjen suoritusten todennäköisyyksiä. Tiedämme, että PCTL-logiikan kaavojen todennäköisyydet ovat kahdelle MDP:lle samat, jos näiden välillä on pvb-simulaatio, eli probabilistinen näkyvä bisimulaatio.

Reduktio T karsii MDP:stä tiloja ja tilasiirtymiä, ja jättää joitain paikoilleen. Kolmisivuinen todistus siis keskittyy osoittamaan, että tämän karsinnan jälkeisen ja alkuperäisen MDP:n välillä on pvb-simulaatio.

Simulaation olemassaolon osoittaminen vaatii useampia väliaskelia, esimerkiksi tiettyjen polkujen ("polku" MDP:ssä on perättäisiä tilasiirtymiä) säilyminen pitää osoittaa, pitää osoittaa että tietty karsittu siirtymä voidaan suorittaa vähän myöhemmin ja saada sama todennäköisyys, jne. Varsinaista laskentaa ei tässä todistuksessa voi käyttää, vaan pitää näyttää että kun tietyn ominaisuuden omaavaa funktiota sovelletaan tiettyyn joukkoon, niin lopputuloksena saatavalla joukolla on tietty toinen ominaisuus. Lisäksi täytyy tehdä jonkun verran induktiota ja näyttää, että tietyt vaihtoehdot ovat loogisesti ristiriitaisia jne.

H-Baari kirjoitti...

Neutriinojen, ei neutronien.

Tiedemies kirjoitti...

Tsiisus, tuo oli nolo kirjoitusvirhe. Korjataan...

Ari kirjoitti...

"... jonka keskeinen funktio oli verraten primitiivisten emotionaalisten reaktioiden aikaansaaminen."

Eiköhän tämä koske lähes suurinta osaa populaarimusiikista?

ps. Itse en ymmärrä atonaalista taidemusiikkia.

Tiedemies kirjoitti...

Pointti tuossa genressä on se, että musiikki on täysin suunniteltu tuottamaan jokin hyvin yksinkertainen reaktio, ja siitä on enemmän tai vähemmän karsittu pois kaikki, mikä ei palvele tätä tarkoitusta.

Usein näissä vielä on tähdätty siihen, että se kuulostaisi mahdollisimman hyvältä tiettyjen tajusteiden vaikutuksen alaisena. Populaarimusiikin tarkoitus on myydä mahdollisimman paljon levyjä, näissä ei ole oikein sitä ideaa, vaan lähinnä se, että porukka menee tietynlaiseen tilaan tietyssä tilanteessa.