Børn af Brouwer og Prior

Luitzen_Egbertus_Jan_Brouwer
L.E.J. Brouwer
prior
Arthur N. Prior

Det er værd at tænke over at to af de vigtige erkendelser i datalogi kommer fra filosofiens verden. Også jeg er blevet grundlæggende påvirket af disse erkendelser.

I mange år var temporallogik, dvs. studiet af de logiske egenskaber ved udsagn om tid, et rent filosofisk område. Det hele begyndte med Aristoteles. Senere gav den newzealandske logiker Arthur N. Prior (hans navn er et fantastisk ordspil – det er i sig selv en temporal modalitet!) præcise matematiske formuleringer af temporallogikkens grundlag. Temporallogik som en tilgang til beskrivelse af programegenskaber skyldes israelske og amerikanske matematikere med nu afdøde Amir Pnueli som en af de helt centrale skikkelser. Temporallogik er et område inden for modallogik, og også modallogik som sådan har fået vigtige anvendelser i datalogi. Mange af de gamle diskussioner om hvorvidt modallogik og temporallogik overhovedet giver mening at beskæftige sig med er blevet lagt døde af de konkrete anvendelser.

Også intuitionisme har været et kontroversielt emne inden for matematik. L.E.J. Brouwers konstruktions-orienterede tilgang til matematik var begrundet i hans filosofiske overvejelser om matematikkens grundlag. Men inden for de seneste 30 år er intuitionistisk typeteori blevet vigtig inden for datalogi. Bindeleddet er den svenske logiker og matematiker Per Martin-Löf. I dag finder findes interaktive bevistjekkere som Isabelle og Coq stor anvendelse både til formalisering af eksisterende matematik og til kontrol af nye resultater. Især inden for programmeringssprogsteori er dette barnebarn af Brouwer blevet et vigtigt redskab. Tidligere har jeg skrevet om hvordan den fransk-canadiske datalog Georges Gonthier har formaliseret store resultater i grafteori ved brug af netop Coq. I kraft af alle disse praktiske anvendelser er mange af de gamle diskussioner om berettigelsen af konstruktiv matematik reelt blevet lagt døde af konkrete anvendelser.

Det, der er sket i begge tilfælde, er samtidig at det er det  matematiske begrebsapparat, der er blevet til, som har vist sig at udgøre berettigelse, ikke den underliggende filosofiske motivation. Samtidig har der i datalogi været forskere med baggrund inden for matematik og filosofisk logik, som har kunnet se forbindelsen – folk som Dana Scott, Robin Milner og Per Martin-Löf har udgjort dette vigtige bindeled.

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

Skriv et svar