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.

Gør klimaforandringerne os pylrede?

Her til morgen syntes jeg, der var koldt. Flere andre, jeg talte med i min frokostpause sagde det samme; jeg var ikke den eneste, der frøs fingrene på min morgencykeltur, selv om vi i skrivende stund kun befinder os i begyndelsen af oktober.

En artikel i Smithsonian Magazine fra 2014 (!!) giver imidlertid en anden forklaring end at det skulle være usædvanligt koldt; fordi temperaturoplevelse er subjektiv, vil man føle at det er ekstra koldt, hvis man er vant til temperaturer over gennemsnittet for årstiden. Så vi kuldskære mennesker er først og fremmest pyrlerede.

Klimaforskeren Andrew Dessler fra Texas A&M University udtaler endda at

“I think that people’s memory about climate is really terrible,” … “So I think this cold event feels more extreme than it actually is because we’re just not used to really cold winters anymore.”

Hvis det er tilfældet, er det skræmmende, for når basislinjen flytter sig, betyder det så simpelthen at alle vænner sig til at klimaet bliver varmere. Dermed bliver det sværere at forstå og tro på, at der faktisk bliver varmere her på Jorden. Et vigtigt modspil må bestå i at dokumentere hvordan vejret var før i tiden.

Situationen ligner den, vi kender fra mange andre sammenhænge. De store forandringer kan på det korte stræk være så små og umærkelige, at man ikke bemærker dem, før det er for sent.

Enten-eller

I dag, da jeg underviste i Beregnelighed og kompleksitet, undrede flere studerende sig uafhængigt af hinanden over en opgave, jeg stillede, hvor man skulle finde en beregnbar funktion mellem to mængder af strenge, A og B. Det eneste, opgaven fortalte, var at der fandtes strenge, som var elementer i B og andre strenge, der ikke var med i B.

Så kunne man derfor definere funktionen, så den på elementer fra A gav en fast streng u fra B som resultat og fra elementer uden for A gav en fast streng v uden for B som resultat. Funktionen er endda beregnbar, hvis man med en algoritme kan afgøre om strenge er elementer i A. Men de studerende, der undrede sig, syntes at det virkede som snyd. Vi får aldrig at vide, hvad u og v egentlig er. Så vi ved egentlig ikke, hvordan funktionen skal beregnes.

Og jeg måtte give dem ret. Hvis funktionen, som jeg har skrevet ovenfor, er en funktion over de naturlige tal, er den veldefineret og den er endda også beregnelig. Den er nemlig en konstant funktion, og konstante funktioner er nemme at beregne. Vi ved bare ikke, om dens værdi altid er 1 eller altid er 0. Men på en eller måde synes man, at beregningen af funktionsværdien kræver at vi skal vide om der er liv uden for solsystemet eller ej.

I det omfang jeg overhovedet kan siges at være matematiker, er jeg konstruktiv matematiker, og de studerendes betænkeligheder er helt rimelige, hvis man spørger mig. Det store underliggende problem er nemlig, at påstanden Enten er der liv i solsystemet eller også er der ikke har en sandhedsværdi ifølge klassisk logik, men er meningsløs i konstruktiv matematik. I konstruktiv matematik kan jeg nemlig kun bevise en påstand på formen P eller Q ved at præsentere enten et bevis for påstanden eller et bevis for påstanden Q. Så jeg skal enten bevise, at der er liv uden for solsystemet eller bevise, at der ikke er. (Det er lidt svært.)

Presburger og hans speciale på 9 sider

Her i ferien har jeg omsider fået tid til at få læst Anita og Solomon Fefermans biografi Alfred Tarski – Life and Logic færdig. Bogen giver et fascinerende indblik i det livlige miljø blandt matematikere og logikere i 1920erne og 1930erne. En af bogens mange sidehistorier er den om Alfred Tarskis studerende Mojzesz Presburger; Tarski var blevet interesseret i hvordan man viser at logiske teorier er afgørbare ved hjælp af den dengang nye teknik, der kaldes elimination af kvantorer. Og som en øvelse i sin undervisning gav han en af sine studerende, Mojzesz Presburger, den udfordring at prøve at vise at teorien for naturlige tal under addition er afgørbar. Dvs. at vise, at der er en algoritme, der kan fortælle os om udsagn som

\forall x. \exists y.y + 1 = x

er sande. Udsagnet ovenfor siger i øvrigt, at for ethvert naturligt tal findes der et naturligt tal, som er dets forgænger. (Dette udsagn er falsk, for det gælder ikke for det mindste naturlige tal.)

Presburger viste at teorien for naturlige tal under addition er afgørbar ved en snedig brug af elimination af kvantorer og den resulterende artikel på 9 sider blev til hans speciale. Nogle mente senere, at dette resultat burde være nok til at give ham en Ph.D. Dette ville i så fald have været en af de korteste Ph.D-afhandlinger nogensinde (det var allerede et kort speciale!).

Mojzesz Presburger forlod dog universitetet og blev ansat ved et forsikringsselskabet. Men man kalder i dag teorien for naturlige tal under addition for Presburger-aritmetik. Og I 2010 opkaldte European Association for Theoretical Computer Science en særlig pris, Presburger-prisen, efter ham. Prisen gives til en ung forsker inden for teoretisk datalogi for banebrydende resultater.

Den meget tragiske del af historien er, at Mojzesz Presburger aldrig nåede at opleve noget af dette. Han døde i Holocaust, formodentlig i 1943.

Nætter med Tarski

I går fik jeg Alfred Tarski: Life and Logic, biografien om den polsk-amerikanske logiker Alfred Tarski. Bogen er skrevet af Anita Burgman Feferman og hendes mand Solomon Feferman, der begge kendte Tarski godt. Solomon, der selv er logiker, var endda en af Tarskis PhD-studerende ved Berkeley University, hvor Tarski tilbragte det meste af sin karriere efter 1939.

Alfred Tarski rangerer helt deroppe med Kurt Gödel og Bertrand Russell som en stor skikkelse inden for matematisk logik, og hans arbejde inden for semantik af formelle sprog har også haft stor betydning for mit eget forskningsfelt, der er semantik af programmeringssprog. Tilfældet ville, at det faktisk var i dag, jeg holdt sidste kursusgang i “Syntaks og semantik”, hvor emnet var en sætning om eksistens af mindste fikspunkter, som Tarski var med til at finde frem til.

Jeg har selvsagt ikke fået læst bogen endnu, men har selvfølgelig ikke kunnet nære mig for at bladre lidt. Bogen er fuld af anekdoter, kan jeg se. Ud over at være meget egenrådig og dameglad (hans hustru var bestemt ikke den eneste, der fik hans opmærksomhed), var Tarski tydeligvis arbejdsnarkoman, og vel også mere end dét – han var et ekstremt B-menneske, der holdt sig oppe hele natten takket være benzedrin (der er beslægtet med amfetamin). Og så var han storryger. En af hans PhD-studerende, Chen-Chung Chang, fortæller i bogen om hvordan han var hjemme ved Tarski til vejledning. Kl. 21 var Tarski som regel ved at komme op i omdrejninger. Der måtte ikke luftes ud, for den gode Alfred mente at røgen gavnede hans tankevirksomhed. Desværre var Chang astmatiker, men det var der ikke så meget at gøre ved. Ved to-tiden råbte Tarski på sin hustru. Lidt efter kom Maria så med kaffe til de to. Klokken halv fem om morgenen var Tarski stadig i fuld gang, og Chang kom først hjem og ud i den friske luft, når solen stod op!

(Uvilkårligt kommer jeg til at tænke på en polsk gæstelektor, jeg havde i min studietid. Han var storryger og røg hele tiden, mens han forelæste. Nogen Tarski var han dog ikke, men til gengæld var hans kursus ikke obligatorisk!)

Når jeg ser anekdoterne om Tarski i Feferman’ernes bog, kommer jeg til at føle mig usædvanligt almindelig. Der er næppe mange originaler som Tarski i dag, og det er både godt og skidt.

En løsning på bedsteforældre-paradokset?

Der er masser af stof til eftertanke i tanken om tidsrejser, og bedst kendt er vel bedsteforældreparadokset, hvor X rejser tilbage i tiden og slår en af sine bedsteforældre ihjel, inden bedsteforælderen selv får børm. Men så kunne X aldrig selv være kommet til verden og ikke derfor ikke rejse tilbage i tiden.

De tre mest almindelige forsøg på at løse dette paradoks er

  1. At konkludere at dette viser, at man ikke kan rejse tilbage i tiden
  2. At konkludere at man godt kan rejse tilbage i tiden, men ikke ændre fortiden (dvs. at forsøget på at slå bedsteforælderen ihjel skal gå galt)
  3. At tidsrejser kun er konsistente med “mangeverdensfortolkningen” af kvantefysik, hvor alle tilstand af enhver elementarpartikel er lige virkelige. Derfor vil der være én verden, hvor X aldrig blev født og en anden, hvor X findes.

Det seneste, jeg har læst om dette, kommer faktisk fra datalogiens verden. Doron Friedman, en israelsk forsker inden for maskinintelligens, har lavet et stykke software, der modellerer kausalitet. Computersimuleringen finder faktisk to mulige løsninger på den lidt simplere udgave, nemlig far-paradokset, hvor en forsøgsperson rejser tilbage i tiden og slår sin far ihjel,

Den ene er at X’s far foretager en tidsrejse frem i tiden og gør X’s mor gravid og derefter rejser tilbage – kun for at blive slået ihjel af X.

Den anden udgave antager at X er en mand – og sørger for at han bliver sin egen bedstefar. X rejser tilbage i tiden og slår sin far ihjel, men gør derefter sin bedstemor gravid med et drengebarn, der så mange år senere bliver far til X.

Disse løsninger er (ud over at være særdeles spidsfindige) for mig at se reelt variationer af mulighed 2 ovenfor; i begge tilfælde sker der dét, at X gennem sine handlinger bare sørger for at begrebet “far til X” stadig er meningsfyldt. Men det egentlig interessante er, at man nu kaster sig over et filosofisk spørgsmål ved at bruge software til at foretage et tankeeksperiment med, og at vi på denne måde har at gøre med en form for eksperimentel filosofi, som er et begreb jeg skrev om her for tre et halvt år siden.

(Det er i øvrigt foruroligende, at Doron Friedmans artikel er skrevet i Microsoft Word.)

En stor bunke sten?

Der var engang et band, der hed Guns’n’Roses. Men alle medlemmerne gik eller blev smidt ud, på nær Axl Rose. Og så spillede de i Aalborg. Var det stadig Guns’n’Roses? Det er 37 år siden, Bon Scott døde. Malcolm Young og Brian Johnson er nu også væk, og deres sanger er nu – Axl Rose. Er det stadig AC/DC? Dødsmetal/grindcore-pionererne Napalm Death findes stadig – eller gør de nu dét?, Der er nemlig ikke ét eneste af de oprindelige medlemmer tilbage. I Richie Blackmore’s Rainbow er der nu ikke ét eneste medlem tilbage fra bandets oprindelige storhedstid.

Det. vi har med at gøre, er rockmusikkens udgave af sorites-paradokset, som jeg har skrevet om her for år tilbage:  Hvis jeg har en stor bunke sten og fjerner én sten, er der stadig en stor bunke sten. Så fjerner jeg en sten mere, og vi har stadig en stor bunke sten. Men hvis jeg fortsætter på denne måde, er der kun to sten tilbage, og det er tydeligvis ikke en stor bunke sten. Hvornår skete overgangen? Sorites-paradokset kan løses ved at sige at begrebet “stor bunke sten” er et vagt begreb, dvs. at det ikke har en veldefineret afgrænsning.

Om 25 år er alle de oprindelige medlemmer af AC/DC sikkert afgået ved døden, og lur mig om ikke der stadig vil være AC/DC-koncerter til den tid, som kan fylde store koncertsale. Vil det band, der spiller til den tid, være AC/DC eller et AC/DC-hyldestband?

Wason-testen

Her er et billede af fire kort. Kortene har et bogstav på den ene side og et tal på den anden. Hvilke kort skal man vende for at finde ud af om der gælder den regel, at hvis et kort har D på den ene side, så står der 7 på den anden side?

Prøv selv at tænke dette igennem.

Denne test blev skabt af den engelske psykolog Peter Wason, og det viser sig at de fleste mener at man skal vende D-kortet. Og det er korrekt. Omkring 75 procent svarer til gengæld også at man skal vende 7-kortet. Men det er ukorrekt; dette kort er helt irrelevant – derimod skal man vende 4-kortet. For hvis der viser sig at stå D på den anden side, har man opdaget at reglen ikke gælder.

Når vi tænker på dette som et problem om udsagnslogik, er det, vi beder forsøgspersonerne om, at finde ud af om de kan falsificere implikationen P \rightarrow Q for nogle givne atomare påstande P og Q.

Men det er interessant, at forsøgspersonerne klarer sig meget bedre, hvis man vælger en anden opsætning af problemet, f.eks. denne:

“Her er fire ansatte i et firma. For hver af dem får du enten at vide hvor længe de har været ansat eller om de er med i firmaets pensionsordning. Hvilke af de ansatte skal du spørge for at finde ud af om det er tilfældet, at hvis man er med i firmaets pensionsordning, har man været ansat i mere end 10 år?”

Der er mange bud på en forklaring af hvorfor forsøgspersonerne nu klarer sig bedre. De har alle én ting fælles, nemlig at reglen nu bliver forklaret som en form for fortælling (måske en slags social kontrakt). Det er åbenbart nemmere for de fleste mennesker at forstå en fortælling om adfærd og konsekvenser end at forstå et egentligt logisk ræsonnement.

Jeg spekulerer på om der mon er noget, vi kan lære af det, når vi underviser i fag, hvor logiske ræsonnementer er centrale – og her tænker jeg selvfølgelig på fag som matematik og datalogi.

Så blev det min tur

2016-11-22-20-59-18
Uden for Ly Club, hvor festbanketten var.

2016-11-22-20-59-08
Faktisk var banketten nu på 2. sal.

2016-11-22-19-07-05
The Carpenters spillet på pipa.

2016-11-22-10-33-18
Furio Honsell, borgmester i Udine og logiker tillige.

2016-11-22-10-21-11
Konferencelokalet var egentlig et stort mødelokale, og bordopstillingen stod desværre ikke til at ændre.

2016-11-22-10-19-50
Den imponerende 10 etager høje bygning på HUST (Hanoi University of Science and Technology) set indefra.

2016-11-22-10-21-02
Furio Honsell og Luigi Liquori hygger sig med lidt typeteori.

2016-11-22-09-49-26
Frank Pfenning fortæller om substrukturelle logikker og transducere.

Så blev det tid til endnu en dag på konferencen, og jeg skulle selv holde mit foredrag som den næstsidste.

Dagens mest interessante foredrag var det indbudte foredrag med Frank Pfenning, der er professor ved Carnegie-Mellon. Han fortalte om sit nye arbejde, der giver en interessant korrespondance mellem en lille substrukturel logik (som er et fragment af lineær logik) og endelige automater med output (de såkaldte transducere). Føjer man de symmetriske bevisregler til logikken, får man en korrespondance til Turing-maskiner – eller rettere: til en generalisering af dem kaldet lineært kommunikerende automater. Der er i øvrigt også en forbindelse til sessionstyper.

Senere var der et foredrag med Furio Honsell, der i de seneste mange år knap har haft tid til at forske – han er nemlig borgmester i Udine i det nordøstlige Italien. Han har da også anlagt sig en for det akademiske miljø temmelig borgmesteragtig fremtoning.

Efter frokosten kom der en poster-session, hvor der var god mulighed for snakke med dem, der præsenterede deres poster.

Så var der et foredrag med den ikke specielt forkølede A. Tiu, der i sin artikel faktisk citerede en af mine artikler fra 2002. Og til sidst blev det så omsider min tur. Jeg havde selv været temmelig udmattet, dels på grund af jet lag, dels på grund af min nyerhvervede forkølelse, og et par gange i løbet af dagen var jeg faktisk faldet hen under foredragene. Jeg håber ikke, at jeg snorkede!

Mit foredrag gik nogenlunde, tror jeg. Der kom faktisk et par gode spørgsmål bagefter. (Mine slides kan man se ovenfor.)

Og efter endnu et foredrag kunne vi tage af sted ud til en restaurant, hvor der var konferencemiddag. Jeg endte ved et bord, hvor der var ganske mange japanere og fik en lang snak med Hidehiko Masuhara, en professor fra Tokyo som flere gange i årenes løb havde besøgt Aarhus Universitet. Vi endte med at tale længe om – Grønland. Det er forbløffende, hvor ofte jeg i tidens løb til konferencer har skulle fortælle udenlandske kolleger om netop denne store, kolde ø. Næst efter H.C. Andersen er Grønland tilsyneladende en af de faste associationer, mange har med Danmark. Gad vide hvad grønlænderne synes om dét.

Undervejs underholdt en vietnamesisk musiker, der spillede på pipa. En pipa er ikke et blæseinstrument, men en slags firestrenget lut. Jeg synes at jeg kendte en af melodierne og opdagede til min forbløffelse, at det var “Top of the world”, der i sin tid var et hit for The Carpenters. Herefter fulgte flere gamle amerikanske og europæiske popnumre. Heldigvis var der også umiskendeligt asiatisk klingende numre. Godt at der da i det mindste var nogle vietnamesiske sange iblandt, for ellers ville det næsten være for plat. Dvs. da vi skulle til at gå, fortalte Hidehiko mig, at den vietnamesiske musiker i den flotte røde kjole faktisk havde spillet en del kendte japanske sange i løbet af aftenen. Så meget for autenticiteten.