tirsdag 14. desember 2010 Julekalender
Etter å ha åpnet luke 8 om Alan Turing vet du at Turingmaskinen er en slags målestokk for å bedømme beregnbarhet (eng: computability). Hvis noe kan beregnes på en Turingmaskin, så kan det beviselig beregnes; hvis noe ikke kan beregnes på en Turingmaskin, så sier vi det er uberegnelig.
Det finnes derimot en annen modell for beregnbarhet. Den er like kraftig, men ganske anderledes. Den heter lambda calculus, og oppfinneren heter Alonzo Church.
Denne adventskalenderen kan lett gi et inntrykk av at matematikere lever helt ekstraordinære liv. Er de ikke homofile kodeknekkere så er de krigshissende atombombeoppfinnere. Såvidt jeg vet levde Church et mye enklere liv.
Church var en amerikansk matematiker og logiker som gjorde betydelige bidrag innenfor matematisk logikk og grunnleggende informatikk. Teoriene han kom opp med forteller oss ikke bare hva som er mulig å få til med en datamaskin, men påvirket også hvordan vi har laget språk for å uttrykke løsningene – dvs. hvordan vi har designet programmeringsspråk. Alonzos arbeid har spesielt influert de funksjonelle programmeringsspråkene, men danner også grunnlag for moderne typesystemer.
Han lanserte Lambda calculus (også skrevet som λ-calculus) i 1936 da han demonstrerte at det finnes problemer som ikke lar seg løse. Dette var før Alan Turings berømte halting problem, som i praksis demonstrerte det samme. Church og Turing viste deretter at lambda calculus og Turingmaskinen var likeverdige i forhold til problemløsning. Deres arbeide kalles Church-Turing-tesen.
Altså, kort fortalt: Hvis det finnes en måte (en algoritme) for å utføre en beregning/kalkulasjon, så kan denne kalkulasjonen også utføres av en Turingmaskin. Og vha. en lambda-funksjon.
Og der rakk jeg jammenmeg å fullføre denne luken også, selv om det var på hengende håret 