At aksiomatisere det hele

Det kommutative diagram for et pullback.

En person fra mit fagområde sagde engang i al venskabelighed, at han ligesom jeg gerne ville kunne aksiomatisere det hele, men at det jo langt fra er alle inden for datalogi, der har det på den måde. Han havde og har ret. En del af mine publikationer fra de seneste år er netop forsøg på at give en generel teoretisk forståelse af en bestemt slags typesystemer, og på den måde har jeg netop haft som formål at aksiomatisere, om ikke det hele, så dog et lille hjørne.

Det er fascinerende at læse om mere ambitiøse anstrengelser i matematisk regi. Quanta Magazine har nu en artikel (også udgivet hos Wired) om kategoriteori – eller rettere toposteori – som et bud på matematikkens grundlag. Her er det interessant at læse forsøgene på at forklare toposteori for lægfolk med interesse for matematik; jeg er ikke sikker på at det helt er lykkedes.

Jeg ville selv ønske, at jeg havde et mere naturligt forhold til kategoriteori. Selv om jeg engang har fulgt et kursus i kategoriteori, da jeg var PhD-studerende i Edinburgh, har jeg haft en ærgerlig fornemmelse af at skulle gen-lære kategoriteori, de få gange jeg har haft brug for det senere. Det er desværre stadig ikke et sprog, jeg taler flydende, selv om jeg er sådan én, der gerne ville aksiomatisere det hele. Min eneste trøst (og den er en underlig én) er, at jeg ikke er den eneste, der har det sådan. Selv blandt “rigtige” matematikere er det ikke alle forundt at beherske sproget flydende. Mit håb er nu at kunne genbesøge kategoriteori ud fra en forståelse af den som en visualisering af begreber inden for funktionel programmering – men det er en anden snak.

Per Martin-Löf og H-indekset

Per Martin-Löf (https://commons.wikimedia.org/wiki/File:Per_MartinLoef.jpg)

I vore dage er der gjort masser af forsøg på at kvantificere forskningspublikationers impact og på at måle styrken af forskningsresultater. Et mål er det såkaldte h-index. Et h-index på h, betyder, at man har h publikationer, der hver er citeret mindst h gange. Derfor kan man ikke have noget højt h-indeks, hvis man kun har få publikationer, selv om de så er citeret mange gange. Jeg har selvfølgelig også et h-indeks, og det er ikke så imponerende igen.

En af de mest indflydelsesrige personer i programmeringssprogenes nyere historie er formodentlig den svenske logiker Per Martin-Löf. Hans arbejde inden for intuitionistisk typeteori og specielt arbejdet med afhængige typer er centralt for programmeringssprog og bevisassistenter som Coq, Agda, Idris m.fl. Martin-Löf udviklede og implementerede ikke selv noget af dette, men hans indflydelse har været enorm. Hele arbejdet med formalisering af matematik og alle de praktiske resultater med maskintjekkede beviser af firefarvesætningen fra grafteori, Feit og Thompsons sætning fra gruppeteori m.m.m. ville være utænkeligt uden.

Der er et websted med alle Martin-Löfs artikler, og lidt afhængigt af hvordan man tæller, er der op til 33 publikation i perioden fra 1966 til 2014. Jeg ved ikke, hvad Martin-Löfs h-indeks er, men det kan ikke være så højt igen. Det er i sig selv tankevækkende.

Sidste dag med ICWL 2019

I dag var sidste dag med ICWL2019-konferencen. Jeg kom lige akkurat for sent til begyndelsen på foredraget om arbejdsvaner hos de, der følger universitetsuddannelser som fjernundervisning. Det var rigtig interessante forskningsresultater, og det var især bemærkelsesværdigt, at resultaterne viste, at 20 procent af deltagerne i undersøgelsen desværre ikke havde nogle systematiske studieteknikker.

Dette var desværre også en af de præsentationer, der ikke kom godt ud over scenekanten. Den, der præsenterede, stod og læste op fra sin iPad på et temmelig famlende engelsk med meget udpræget accent – der denne gang var fransk. Jeg nåede at tænke, at jeg troede at engelskundervisningen var bedre i Frankrig end tilfældet åbenbart var. Men til allersidst, da præsentationen kom ind på forskernes øvrige resultater, opdagede jeg at den, der fremlagde, faktisk var fra Canada. Fransk-canadiere kan åbenbart være lige så uvante med engelsk som engelsk-canadiere efter min erfaring kan være med fransk.

Konferencens sidste foredrag var noget af det underligste, jeg har oplevet. Ingen af artiklens forfattere, der begge var fra Kina, var til stede. Den slags kan jo ske, men det var påfaldende, at forfatterne ikke havde gjort særlig meget i den anledning. De havde faktisk også fået en anden artikel optaget, som havde været på programmet i en anden session tidligere på dagen og selvfølgelig heller ikke kunne præsenteres. Til begge præsentationer var der lavet en videopræsentation optaget i den ene forfatters ikke helt ryddelige lejlighed. Det var så overladt til den tilstedeværende ordstyrer at vise nogle PowerPoint-slides samtidig. Men takket være de ikke så uoverskuelige slides, det svært gennemtrængelige indhold og en usædvanligt dårlig lydkvalitet på videoen opdagede vi denne gang først til sidst, at det var de forkerte slides vi havde fået at se. Heldigvis var præsentationen meget kort, og der var ingen spørgsmål (hvem skulle man også kunne stille dem til?), så vi kom ikke for sent til frokost.

Efter frokost var der den traditionsrige Best Paper Award, der denne gang gik til Aditya Johri fra George Mason University i USA. Han havde lavet en god præsentation af sin analyse af hvordan børn og unge lærer at programmere i det visuelle sprog Scratch, og det var fuldt fortjent at prisen gik til ham. (Det tjener ham også til ære, at han stillede et godt spørgsmål efter min præsentation, synes jeg.)

Efter konferencen tilbragte jeg en rolig eftermiddag og aften i Magdeburg. Jeg fik nærstuderet relieffet, der hyldede den russiske soldat som for præcis 50 år siden reddede en lille tysk pige fra et fald fra første sal. Relieffets stil mindede mig nu i forbløffende grad om udtrykket hos om min kære tyske kunstner-nabo fra Edinburgh, Sylvia von Hartmann.

Aftenen blev afsluttet med et lille restaurant på Botanica, en populær vegansk restaurant. Forlokalet på Botanica var optaget af et akvarelkursus (!!!) og mine tanker igen gik uvilkårligt til Sylvia, der er kendt bl.a. for sine akvareller.,

Fri forskning?

I denne uge er der fokus på hvad der sker, når man tager imod forskningsmidler fra private aktører, i kølvandet på dagbladet Informations afsløring af omstændighederne om en rapport om klimabelastningen af oksekød. Institutlederen for Institut for Agroøkologi på Aarhus Universitet nu har valgt at trække sig fra sin post og forlader universitetet.

I datalogi er ekstern privat finansiering også udbredt. Tilbage i februar åbnede Concordium Blockchain Research Center ved på Aarhus Universitet. Det nye forskningscenter bliver støttet af Concordium Foundation, der udvikler en ny generation af blockchain med fokus på brugeridentifikation og gennemsigtighed. Fondsstøtten er på omkring 10 millioner pr. år i de første fem år af centrets levetid.

Hele blockchain-ideen har mange interessante problemstillinger i datalogi knyttet til sig, men det er i det hele taget tilfældet for hele fintech-verdenen. Finansverdenen, der ofte har været i mediernes søgelys inden for de seneste år, er blevet en væsentlig aktør. Og det er også tilfældet her.

Concordium Foundation bliver lanceret som en non-profit-fond, men her er det interessant, at en af hovedpersonerne bag denne fond er Lars Seier Christensen, som er leder af Saxo Bank og økonomisk og ideologisk støtte bag Liberal Alliance. Så formodentlig er der også potentielle interessekonflikter mellem fri forskning og virksomhedsinteresser i denne tilsyneladende uskyldige konstruktion.

En tidsskriftsartikel

I dag fik jeg omsider publiceret en artikel i det ikke helt ukendte (og meget anerkendte) tidsskrift Acta Informatica. Det giver mig 2 point ifølge den Bibliometriske Forskningsindikator (BFI). Det tog to år. Desværre er udgivelsen ikke open access, men den tæller også, selv om det ikke er nok at få BFI-point. Der skal mere til, er der dem, der siger. Det er ikke alle, der performer godt nok, hedder det sig. Men jeg er nu tilfreds alligevel.

Begrebsmaskiner

Fra Felienne Hermanns’ websted (kilde: http://www.felienne.com/archives/6375)

Et af de nye tiltag inden for forskning i datalogi ser ud til at bringe to forskningsområder, som jeg beskæftiger mig med, sammen – semantik af programmeringssprog og uddannelsesforskning inden for datalogi. I juli i år har der således været et Dagstuhl-seminar hvor forskere fra disse to områder mødtes . Den amerikanske datalog og uddannelsesforsker Mark Guzdial skriver

A notional machine is a human-facing, student-accessible explanation for how some aspect of the computational machine works — it might be an explanation of a language feature, or an explanation of some aspect of a running program (e.g., how swap() works). To be able to debug a program, a student needs to understand it, i.e., to have a mental model of how the program works. A student has to be able to predict what their program does, simulating it in their head. A notional machine is a teaching tool for helping the student develop a successful (predictive) mental model.

Dette begreb, der bl.a. skyldes Guzdial, er centralt i de didaktiske overvejelser om programmeringsundervisning, og det er formodentlig broen til at knytte uformel og formel forståelse sammen.

Jeg ved ikke, hvordan begrebet notional machine bedst oversættes – måske “begrebsmaskine”? Dette begreb er interessant, og det er måske endda det, man i fagdidaktiske sammenhænge kalder for et tærskelbegreb. Ofte har vi lidt vagt talt om at man skal lære “principper i programmeringssprog”, men det, vi faktisk efterlyser, er denne form for abstrakt maskine i delvist uformel form.

Jeg har gennem mange år undervist i semantik af programmeringssprog. Min egen erfaring fra undervisningssammenhænge er her, at det desværre i høj grad er muligt at kunne programmere, men samtidig have store problemer med at forstå formel semantik af programmeringssprog. Min fornemmelse er, at denne kløft typisk skyldes at man i så fald ikke har en systematisk forståelse af det programmeringssprog, man anvender, herunder et begrebsapparat der ville kunne understøtte en sådan forståelse. Så vidt jeg kan se, er det netop en “begrebsmaskine”, der er behov for, for den kan hjælpe med at lære programmeringsfærdigheder og samtidig fungere som en bro til den forståelse af formel semantik, der er nødvendig i sprogdesign, oversætterkonstruktion og egentlig programanalyse. En af mine overvejelser er lige nu, om man mon i højere grad skulle bygge programmeringsundervisningen op med et af de centrale læringsmål (og med den sprogbrug) at den lærende skal kunne gøre rede for og anvende en sådan begrebsmaskine.

A.P. Ravn 1947-2019

I dag kunne jeg læse den triste nyhed, at Anders Peter Ravn, af mange kendt som A.P., er gået bort efter længere tids sygdom. A.P. var gennem mange år professor i datalogi, og jeg så ham ofte i mit daglige virke. Han var en god og dygtig videnskabsmand og en rar mand tillige; det er underligt, at jeg aldrig skal se ham igen. Æret være hans minde.

En regnvejsdag i Leicester

I dag var der en workshop, hvor der var mulighed for alle til at tale om de faglige emner, der er i fokus for vores Horizon 2020-projekt. Jeg fik også tid til at snakke med mine kolleger andetsteds fra om den artikel, vi sender ind til en konference i næste uge. Og i frokostpausen blev der også tid til at stå i kø i den engelske sommerregn. En italiensk kollega bemærkede, at dette var en kærkommen forandring fra den hedebølge, de lige nu slås med i Sydeuropa.

Projektmøde i Leicester

Vandhanen på mit hotelværelse i Leicester.

I dag var det tid til det officielle statusmøde i forbindelse med vores projekt under EUs RISE-program. Undervejs i mødet fortalte koordinatoren Adrian Francalanza fra Malta om det der med API’er i software, og han brugte en god analogi– nemlig en vandhane! Det handler her ikke om brugervenlighed, men om hvad vandhanens håndtag tillader os at justere og om rækkefølgen, vi skal bruge håndtagene i. Det er faktisk et lille eksempel på det, vi i datalogi kalder for en protokol. Bagefter kom jeg til at tænke på nogle observationer om vandhaner og deres grænseflade, som jeg gjorde under en sommerferie for nogle år siden. Måske er kimen lagt til et populærvidenskabeligt foredrag?

Vi var alle lidt nervøse inden mødet, for EU-kommissionen havde sendt en officel repræsentant, der skulle give os et foreløbigt skudsmål. Der havde været problemer med enkelte partnere i konsortiet, der havde trukket sig tidligt – men det var jo ikke vi andres skyld. Vi endte også med at tale om hvad vi mon kunne gøre for at få en bedre kønsfordeling i projektet, noget der desværre er svært, givet at der er tale om et projekt inden for et voldsomt mandsdomineret fagområde. Ingen er stolte over dette, og heller ikke os.

Heldigvis fik vi en forsigtigt positiv tilbagemelding fra EUs repræsentant, og jeg tror faktisk at hun tager med os alle på restaurant her til aften. Leicester er en af de byer i Storbritannien (og vel specielt i England), der er kendt for sine gode indiske/pakistanske/nepalesiske restauranter, så det er her, vi skal spise.

Projektmødet som disse ender også ofte med at handle om mere end selve projektet. Alle er selvfølgelig akademikere, men et stort flertal af os har derudover en fælles referenceramme fra ansættelser i universitetsverdenen. På vej fra mødet snakkede jeg med en kollega fra IT-Universitet i København. Han spurgte mig om hvordan jeg havde det med mit arbejdsliv i lyset af alt det, jeg har oplevet i år og berettet om for andre. Jeg svarede ham ærligt; mere kan jeg ikke skrive her.