Alle veje fører bort fra Rom

2013-01-25 17.34.21

 

Det uventede sker altid, når man mindst venter det. Sådan en tautologisk formulering kunne der så i en af de projektrapporter fra 1. semester, jeg i disse dage prøver at læse uden alt for voldsom brug af rød kuglepen. Men faktisk passer det jo.

Jeg kom tilbage til hotellet efter en ikke særligt festlig festmiddag til POPL, pakkede og gik i seng. Morgenen startede på hotellet, hvor jeg delte morgenbord med bl.a. Earl Barr (en amerikaner i London), der skulle holde foredrag om eftermiddagen – hvor jeg desværre var på vej hjem – og Loris D’Antoni (en italiener i Philadelphia). Han fortalte mig om et lille projekt, han er ved at lave om automatisk retning af opgaver i automatteori. Ideen er baseret på at de regulære sprog har samme udtrykskraft som andenordens monadisk logik over endelige strukturer; dvs. at man ud fra en logisk formel, der beskriver et regulært sprog, med en algoritme kan konstruere en automat, der genkender sproget. Alle opgaver om at konstruere automater i f.eks. Sipsers bog bruger formuleringer, der ligner andenordens monadisk logik en hel del. Og på baggrund af dette kan man så lave et stykke software, der kan hjælpe med at give feedback på studerendes løsninger på opgaver af denne slags. Den sidste idé var især overraskende.

Oppe på mit værelse skulle jeg til at hente min kuffert, da telefonen ringede. Min mor, der er dement og har boet på plejehjem siden 2001, havde fået en blodprop og var faldet. Det var noget af et chok at få denne besked, og efter jeg havde tjekket ud og var henne til de sidste POPL-foredrag jeg kunne nå, kneb det lidt for mig at koncentrere mig om at følge med i det inviterede foredrag. Men min kone tog hen for at besøge min mor og kunne skrive til mig, at min mor allerede var i klar bedring. Min kone er et helt utroligt godt menneske!

Således lettet kunne jeg gå til pausen, og her traf jeg igen Daniel Hirschkoff, der er lektor på universitetet i Lyon. Vi havde snakket sammen til BETTY-mødet i Bruxelles tilbage i oktober, og igen her til POPL. Daniel var interesseret i både mit arbejde fra 2011 om simpelt typede psi-kalkyler og det arbejde, jeg lige nu slås med at få færdigt om resursesensitive typesystemer for psi-kalkyler. Så det endte vi med at sidde og snakke om, og jeg endte med at love at jeg vil have min nye artikel klar til sidst i marts. Det lover jeg hermed også her.

Sådan havde jeg ved POPL i løbet af 35-40 minutter haft bedre muligheder for at snakke med nogen om min aktuelle forskning end jeg har haft i hele det forgangne år hjemme i Aalborg. Det er desværre lidt for sigende.

Jeg nåede at høre endnu et foredrag, hvor Damien Pous (en af Daniel Hirschkoffs tidligere PhD-studerende) holdt et forbløffende enkelt foredrag om noget så tilsyneladende elementært som en ny og enkel afgørbarhedsprocedure for ækvivalens af NFA’er; den bruger det, vi kalder koinduktion og op-til-teknikker. Dette var et foredrag, som en kvik tredjeårsstuderende nemt ville kunne følge med i og holde af. Til sidst stillede en fyr fra Birmingham en værre glædesdræber af et spørgsmål, nemlig om ikke alt dette kunne formuleres kategoriteoretisk. Og jo, det kunne det. Mere fik vil (heldigvis) ikke at vide her.

Derefter verdens hurtigste frokost – penne all’arrabbiata på under 10 minutter – og så i taxi ned til banegården til det gennemgående tog ud til lufthavnen. Toget leverede i dagens anledning en forsinkelse af den slags, som dataloger kan bruge i foredrag, når de skal overbevise alle om at programanalyse er vigtig. Midt i det hele standsede det gennemgående tog, og lyset og alle informationsskærme gik ud. Efter nogle minutter tændtes informationsskærmene igen, og sørme om ikke det viste at togets computer var ved at genstarte! Vi var strandet her på grund af hvad der formodentlig var en softwarefejl.

Vel ude i lufthavnen, henne ved gaten mødte jeg ingen ringere end Hanne Riis Nielson fra DTU. Hun var mindst lige så overrasket over at se mig som var jeg var over at se hende. Og nej, hun havde ikke været til POPL, men til et møde i forbindelse et EU-projekt om “security and safety”. Jeg var nødt til at fortælle hende historien om toget.

Og her sidder jeg så nu i Københavns Lufthavn (i den italienske café efter indtagelse af en pizza med en meget uitaliensk og lidt for paplignende bund), hvor vinteren er på sikker afstand af en rude. Min kone kunne fortælle mig, at vores datter har fået konstateret en penicilinkrævende streptokok-infektion; det er derfor hun stadig har ondt i halsen. På den måde lykkedes det vores familie at få strakt vores infektions-sæson på tværs af julen ind i februar. Surt for alle parter. Men om et par timer er jeg hjemme.

En anderledes januar

2013-01-24 13.27.58

Frokostpausen var så tilpas lang, at jeg i dag nemt kunne nå at gå en tur i solen. Man opdager meget hurtigt at januar i Italien (i hvert fald i denne del af Italien) er meget anderledes end januar i Danmark. Træerne er grønne og appelsintræerne er fyldt med appelsiner. Af og til kommer der en kort regnbyge, men det er så også dét. Temperaturen er omkring 12 grader. Jeg vænner mig nok aldrig til den danske vinter, og det bliver ikke nemmere for mig med årene. Den italienske vinter kunne jeg derimod sagtens vænne mig til.

Der var nu ellers en del interessante foredrag i dag også; formiddagens sidste foredrag af Fabrizio Montesi (der er på ITU til daglig) handlede interessant nok om præcis det, som var centralt i det ITU-kursus, jeg havde været censor på i mandags. Det var godt at høre en god og letforståelig fremstilling af dette spændende emne. Der var i det hele taget flere gode foredrag. Også det indbudte foredrag med den indiskfødte professor Shiram Krishnamurthi var interessant – fokus var på hvordan man kan ræsonnere om det skrækkelige, men meget udbredte Javascript og om det er muligt at undgå at bannerreklamer (der typisk eksekverer Javascript-kode) gør noget ondsindet (eller bare uønsket) på en webside. Det glædede mig selvfølgelig, at Krishnamurthi betonede vigtigheden af et godt typesystem, men det var også interessant at høre hans overvejelser om hvordan datalogi jo faktisk er en naturvidenskab og om hvordan hans arbejde med at analysere et system ved navn AdSafe, som Yahoo har lavet til at beskytte mod “onde” bannerreklamer, faktisk er et paradigmatisk eksempel vores videnskabelige metode. I andre naturvidenskaber forsøger man at finde stærke, men enkle modeller, der kan beskrive naturfænomener og forudsige deres adfærd. Det gør vi jo faktisk også i datalogi, men forskellen er at “naturfænomenerne” i datalogi i sidste ende altid er menneskeskabte. Derfor kan vi også bevidst forandre dem, så på dén måde er datalogi forskellig fra de andre naturvidenskaber.

Der var også en lidt underlig oplevelse i et af de andre foredrag, jeg havde glædet mig til. En af forfatterne, en portugisisk kollega som jeg kender nogenlunde godt, var synligt meget nervøs gennem hele sit foredrag. Hans foredrag blev underligt usammenhængende. Sådan havde jeg aldrig set ham før; han er en meget dygtig og erfaren mand og har en behagelig og rolig udstråling i øvrigt – og det havde han da også til frokosten bagefter, hvor jeg kom til at sidde ved siden af ham. Måske var det at holde foredrag ved en så prestigefyldt konference som POPL alligevel for stor en oplevelse selv for ham?

POPL

popl
Udsigt over parallelfrokost nr. 1 ved POPL 2013.

I dag startede hovedkonferencen Principles of Programming Languages, bedre kendt som POPL. POPL er på mere end én måde en af de største konferencer, jeg har været til (jeg har været med flere gange tidligere). For det første er antallet af deltagere overvældende stort – der er så mange, at der er tre parallelle frokost-serveringer i tre store lokaler. Dét har jeg aldrig set før, heller ikke til de tidligere POPL, jeg har deltaget i. Og for det andet er kvaliteten af bidragene rigtig høj. Det er måske ikke alt, der er lige spændende for alle og heller ikke for mig, men jeg bed mig som sædvanlig fat i nogle foredrag.

Dagens første foredrag var et indbudt foredrag af Georges Gonthier fra INRIA/Microsoft Research, der fortalte om det maskintjekkede bevis for Feit-Thompsons sætning om entydig faktorisering af grupper af ulige orden. Det har jeg tidligere skrevet om her. Gonthier fortalte først om sætningen og dens gruppeteoretiske grundlag og dernæst om arbejdet med at repræsentere beviset i typeteorien Calculus of Constructions eller rettere i værktøjet Coq, der er en implementation af denne. Den helt centrale indsigt som Feit og Thompson gjorde var at betingelserne for at være en gruppe, der ikke opfylder entydighedsbetingelsen i sætningen kan fanges i Galois-teori. Men det betyder så også at en repræsentation i Coq skal fange en hel masse standardbegreber i gruppeteori og resultater om dem – helt fra simple begreber som grupper, normale undergrupper og sideklasser over Sylows sætninger, Frobenius-grupper og sætninger i Galois-teori. Intet under at det tog så mange mennesker så lang tid at lave dette maskintjekkede bevis; én ting er at forstå gruppeteorien, en anden er at beskrive den inden for typeteori og formalisere hvert eneste lille lemma i Coq. Gonthiers foredrag var lidt for langt og af og til fortabte han sig i de mange interessante detaljer af både matematisk, typeteoretisk og mere programmeringsnær art, dette imponerende projekt rummer. Men jeg hæftede mig ved to ting. For det første lader det til at “rigtige” algebraikere (ifølge Gonthier) synes at dette er spændende. For det andet opdagede Gonthier og hans kolleger undervejs at der faktisk var en træls trykfejl i Feit og Thompsons artikel, der sneg sig videre fra den første af deres første lange artikler med det oprindelige bevis ind i den anden – men at denne trykfejl ingen betydning havde, da den optrådte i en betingelse, der i det computertjekkede bevis viste sig at være overflødig!

Der var også andre interessante foredrag om bl.a nominelle mængder (et emne, jeg selv er endt med at berøre), om typeinferens for forfiningstyper (et andet emne, jeg engang kastede mig over – men min tidligere samarbejdspartner Naoki Kobayashi opdagede at han kunne genbruge et trick med at reducere dette problem til løsning af lineære uligheder!) og et spændende foredrag af Sam Staton om hvordan man kan forstå typereglerne for funktionsorienterede programmeringssprog ved brug af kategoriteori. Alle tre foredrag rummede resultater af stor værdi, men hvad bedre var: foredragsholderne fik præsenteret de vigtige ideer uden at fortabe sig i detaljer. Det er bestemt ikke altid at selv et foredrag på en prestigefyldt konference når ud over scenekanten.

Jeg blev væk fra nogle foredrag for at tage en lille tur ud i byen. Jeg fik skimtet Colosseum og Vittorio Emmanuele-monumentet i det fjerne og det gik op for mig, at jeg var havnet i samme del af den italienske hovedstad som jeg havde set, sidst jeg var for over 26 år siden! En mindre stolt oplevelse er at jeg ikke kunne finde ud af at tage bussen – eller rettere: Det kunne jeg godt, men jeg vidste ikke, at man ikke kunne købe billetter i bussen. De kan købes i kiosker og tobaksforretninger og kun dér. Så hvis buschaufføren læser dette indlæg, kan han vel egentlig afkræve mig kontrolafgift for at have kørt i bus uden billet (jeg fik dog købt en billet på tilbagevejen).

Internetforbindelsen på mit hotel er ikke fantastisk, vel ofte sammenlignelig med gamle dages 28 kilobaud-modemmer, og til konferencen er forbindelsen hurtigere men til gengæld ekstremt overbelastet (vel at forvente, når man placerer flere hundrede mennesker med hver deres computer i samme lokale), så underligt nok er jeg mere offline end jeg ellers er på rejse. Til gengæld lærer jeg en del om stoisk tålmodighed på denne rejse af dårlige netforbindelser og køer i lufthavne og hoteller og til servering af mad og drikke; det er måske ikke så overraskende, at stoicismens vigtigste repræsentanter Seneca og Marcus Aurelius var romere.

Finalmente: Roma!

navneskilt

Bortset fra endnu en Lufthansa-forsinkelse, der skyldtes en passager, der havde tjekket sin bagage ind men aldrig var dukket op selv (hvorfor den pågældende persons bagage skulle lokaliseres og fjernes fra flyet), gik resten af turen som den skulle. Dvs. det var underligt at sidde i flyet og vide at de andre var i gang med 1st Workshop on Behavioural Types (BEAT’13). Vi nåede frem til Hotel Parco dei Principi kl. 12.30 i dag, og de fleste deltagerne fra BEAT stod i foyeren og ventede. Vejret her er meget mildere end i Danmark; ikke antydningen af sne og temperaturer, der i Danmark ville passe bedre til april. Det var rart at kunne lægge vinterstøvler og vamset trøje i en pose for en stund.

Vi tog os en god og overraskende billig frokost på en café ved navn Gaudi. Italiernene sagde, at det ikke var en “rigtig restaurant”, men der var venlig betjening og hyggeligt interiør. I brødkurven var der noget, der lignede æbleskiver ; det var pizzadej dybstegt i olivenolie. En simpel og forbløffende delikat oplevelse, men nok ikke god, hvis man vil tabe sig. Der var en stor frokostbuffet, og jeg lærte udtrykket kilometro zero, der vist nærmest kan oversættes til “årstidens lokale grøntsager” (som man skal 0 kilometer væk for at hente – vel lidt af en overdrivelse, i al fald når man taler om centrum af Rom).

Mange af os er også med i det nye forskernetværk BETTY (det, der tilbage i oktober fik sendt mig til opstartsmøde i Bruxelles) og her fik vi snakket om hvordan vi skal lave det rigtige opstartsmøde til marts. Det bliver forresten også her i Rom.

Jeg fik desværre kun hørt de tre sidste foredrag til BEAT og gik bl.a. glip af Naoki Kobayashis gennemgang af hans resultater om adfærdstyper; Naoki har engang besøgt mig i Aalborg og han holder nogle rigtig gode og klare foredrag.

Thomas Hildebrandts foredrag havde jeg allerede hørt ugen inden i Aalborg. Vasco Vasconcelos fortalte først om Kohei Honda, der døde så pludseligt i sidste måned, og derefter om sit eget nye arbejde, der lader lineære typer og korrespondanceudsagn møde sessionstyper. Og til sidst gav Jakob Rehof (der er dansker, men snart i mange år har været i Dortmund, hvor han er professor og leder af Fraunhofer-instituttet) et spændende foredrag, hvor gamle resultater fra matematisk logik, nærmere bestemt Tarskis gamle arbejde med bevisbarhed i udsagnslogik og Church, Schönfinkel m.fl.’s arbejde med typet kombinatorlogik, kan bruges til at forklare, hvordan man ud fra et programbibliotek (hvor programmerne er typede kombinatorer) kan syntetisere et nyt program. Det hele er selvfølgelig muligt pga. Curry-Howard-isomorfien mellem typer og udsagn og det hele er selvfølgelig også enten uafgørbart eller (i specialtilfælde) EXPTIME-fuldstændigt, sådan som mange spændende beslutningsproblemer desværre skal være.

Og den egentlig ret lange dag endte på en ristorante, hvor Juventus spillede 1-1 mod Lazio i baggrunden og de italienske deltagere i selskabet kappedes om at fordømme Silvio Berlusconi.

Strandet

Fotografi den 21-01-13 kl. 20.48 #2

Alle fly videre fra München var forsinket, og kabinepersonalet var så venlige at fortælle at vi bare skulle gå til gate G8. Der var dog ét fly, der ikke var forsinket – og det var flyet til Rom. Så her sidder jeg og Thomas Hildebrandt i München. Det mest trælse er at gå glip af meget af den workshop, jeg selv havde været med til at organisere og brugt en del tid på. Men i det mindste er der da et hotel at overnatte på.

 

Sent, sent, sent

20130121-171903.jpg

Det var den dag, hvor jeg var censor ved en eksamen på IT-Universitetet og derefter sammen med eksaminator Thomas Hildebrandt skulle videre til en workshop ved navn BEAT i ROM. Thomas skal holde foredrag, jeg selv er formand for programkomiteen og skal åbne workshoppen. Men flyet til München hvorfra vi skal videre til Rom er forsinket, og det er lige nu uvist om vi når videre til Italien i aften. Af og til er det lige lovlig spændende at være på farten.

Skagen

I dag og i morgen er jeg med Institut for datalogi til institutseminar i Skagen. Mange af os deltog i udflugten til Grenen og Den Tilsandede Kirke. Dette er første gang, jeg er i Skagen om vinteren – og Grenen er stadig interessant, samtidig endnu mere vindomsust. Der var mange spændende huer at se.

At komme hjem

Jeg kommer måske til at virke moraliserende eller selvgod, når jeg skriver dette. Hvis det er tilfældet, så beklager jeg. Min kone og jeg var på vej hjem sent i går aftes efter et familiebesøg på Fyn, og da vi skulle af bussen, så vi en ung mand, der tydeligt var meget beruset. Nogle andre passagerer, der ikke skulle af, prøvede at få ham ud af bussen på en venlig måde. Da vi så, hvordan han knap kunne gå, besluttede vi os til at følge ham hjem. Temperaturen var under 10 minusgrader, det var glat, han kunne knap nok gå og hans ikke helt varme tøj var i stykker. Tilsyneladende havde han også mistet sin telefon. Vi fulgte ham hjem til hans kæreste.

Bente Klarlund skriver i Politiken:

Men alkohol får blodkarrene til at udvide sig. Dermed taber man varme og bliver kold indeni. Og er man fuld og træt nok, er der risiko for, at man falder eller lægger sig ned for at hvile, og så bliver den berusede krop hurtigt afkølet med alvorlige konsekvenser, der kan ende med død.

Så det gode råd er at tage godt med varmt tøj på til julefrokosten – eller drikke lidt mindre.

Jeg kan huske, at jeg sagde til ham at jeg syntes at han var en idiot. Det var lige vel hårdt sagt. Der er også andre, der har dummet sig. Nogen har siddet og drukket sammen med ham; det er endda sandsynligt at han havde været til julefrokost.

Da min kone og jeg kom hjem, talte vi længe om det, vi havde oplevet, og mine tanker gik til en anden og meget tragisk episode. For nogle år siden på denne tid af året forlod en god bekendt af mig en fest ud på de små timer; andre kunne bagefter fortælle at han havde været påvirket. Han havde ikke gået ret langt før han blev ramt af en bil; to børn mistede deres far.

Det, der foruroliger mig, er at ingen forhindrede dem i at tage alene hjem.

Enschede

20121105-100715.jpg

I dag er jeg igen af sted i forbindelse med et europæisk forskningsinitiativ, denne gang i Enschede i Nederlandene og denne gang et europæisk projekt ved navn TRESPASS. Det er et krydsfagligt projekt, hvor problemstillingen er datasikkerhed i organisationer. Det er en problemstilling, der rummer aspekter af både datalogi og sociologi. Fra Aalborg er det min gode kollega René Rydhof Hansen, der er hovedinitiativtageren.

Her er nogle linjer fra projektbeskrivelsen:

Everybody is familiar with the yellow Post-It memos, showing login details, that are often found stuck to computer monitors. The same goes for USB sticks found in car parks. However few grasp the real impact of such actions on an organization’s business or brand. Both may eventually lead to data theft, not as a result of any technical failure, but as a result of the vagaries of human behaviour.

Jeg ved ikke om dette var bevidst, men alle deltagere i dag fik – en USB-stick med samme farve som en Post-It-seddel (se bare billedet).

Det er en helt anden fornemmelse at være til stede her end til mødet i Bruxelles; her er kun få til stede som jeg kender (og som kender mig). Men problemstillingen er interessant, og der bør være mulighed for at lære nye mennesker at kende.

På vej hjem igen

I skrivende stund er jeg havnet i Københavns lufthavn i en slags allemandsland (eller ingenmandsland) mellem indenrigsterminalen og udenrigsterminalen. Om alt går vel, kan jeg snart komme om bord på flyet til Aalborg.

Det var en udbytterig og egentlig også intens tur. Samtaler sent om aftenen kan få de mest uventede ting frem. Jeg fandt først i går midnat over et glas altbier ud af at min bror Alexander for 13 år siden overlevede et fald fra tredje sals højde, da hans daværende lejlighed brændte. Han er den første person jeg kender, der på denne måde har set døden i øjnene. Dét giver mig et helt nyt syn på ham. Og jeg spekulerer på hvad jeg mon lavede den oktobernat hjemme i Nørresundby den nat i 1999, en del år før jeg vidste at jeg havde en bror i Tyskland.

Næste weekend er jeg på farten igen – først som medlem af Amnesty International på en lille tur til Odense, og siden igen som forsker på en tur til Enschede i Nederlandene. Om forskerturen bliver lige så god i den omgang, ved jeg ikke. Jeg har lov til at både tvivle og håbe.