Tilbage til lambda-kalkylen

Så vendte jeg omsider tilbage til hverdagen; der er snart ikke flere antibiotika tilbage i pilleæsken, og en dag slutter min hoste forhåbentlig også.

På fredag d. 25. kl. 12.30 kan jeg holde det foredrag på Institut for Matematiske Fag om Alan Turings liv og værk, som jeg længe har set frem til. Forhåbentlig er min stemme mindre slidt på det tidspunkt. Og på onsdag skal jeg holde sidste forelæsning i kurset Programmeringsparadigmer; det ser jeg ikke helt så meget frem til – simpelthen fordi jeg mangler at forberede mig en del på denne forelæsning. Der er en fællesnævner for de to foredrag, nemlig lambda-kalkylen. De fleste forbinder lambda-kalkylen med Alonzo Church (som da også fandt på den); ikke mange tænker dog på at også Alan Turing ydede vigtige tidlige bidrag her og bl.a. lavede tre artikler om den simpelt typede lambda-kalkyle. Allerede i Turings banebrydende On Computable Numbers, with an application to the Entscheidungsproblem, hvor Turing-maskinmodellen dukker op for første gang, skriver Turing om ækvivalens med lambda-kalkylen. Dette ækvivalensbevis skyldes i høj grad et forsøg på at yde et yderligere bidrag i lyset af at Turing fik kendskab til at Church omkring det tidspunkt hvor det første manuskript til On Computable Numbers… forelå, uafhængigt af ham havde vist netop det resultat om uafgørbarhed af logik, som Turing havde fundet frem til.

Det er svært at skrive en forelæsningsnote om lambda-kalkylen, når der allerede findes meget. Mit mål er at skrive en minimal fremstilling, der på én lang kursusgang netop berører den utypede lambda-kalkyles semantik, den simpelt typede lambda-kalkyle og Hindley-Milner-typesystemet for polymorf typeinferens. Alle beviserne skal være der, men tilpas gemt af vejen af hensyn til den mindre matematisk begejstrede læser (den slags mennesker findes, må man sande med alderen). En sådan minimal fremstilling har jeg desværre ikke kunnet finde nogen steder, så nu laver jeg den selv.

En interessant artikel (som jeg lover at få læst ordentligt en dag) om lambda-kalkylen er The impact of the lambda calculus af Henk Barendregt. Alle, der har beskæftiget med lambda-kalkylen ved (forhåbentlig) at Barendregt er den helt store autoritet inden for dette emne; hans “gule” bog er en klassiker og hans klassifikation af typesystemer som en kube er også et helt fundamentalt bidrag. Citatet ovenfor er snuppet fra artiklen; det giver et af de interessante eksempler på hvordan en central matematisk notation kan blive født ved et tilfælde.

(Visited 124 times, 1 visits today)
Loading Facebook Comments ...

Skriv et svar