next up previous contents
Next: Operationel Semantik Up: Teoretisk Datalogi Previous: Algebraisk Semantik

Denotations Semantik

Church's -kalkyle viste sig at være den model for beregnelighed som lå og ligger nærmest de programmeringssprog vi kender som Algol 60, Pascal, m.fl. Man kunne faktisk forklare f.eks. Algol 60 ved omskrivninger til -udtryk. Da -kalkylen indtil 1970 kun kunne forstås `mekanisk': ved såkaldt reduktion (dvs. ren syntaktisk omskrivning) af udtryk til en ikke-reducérbar form (hvis den da eksisterer), ja så blev det magtpåliggende at forstå også -kalkylen ved dens indlejring i den klassiske matematik. Dette skete i 1970 (Dana Scott). Samtidig kunne Scott's opdagelse bruges dels til at beskrive kommercielle programmeringssprog præcist for derved at opnå mere pålidelige oversættere, dels i ganske almindelig udvikling af generelle programmer. Dette sidste blev ``opdaget'' og gennemført ved IBM's Wiener Laboratorium omkring 1973.gif Hvor algebraisk semantik som tyd af udsagn knytter algebraer, der knytter denotations-semantikken -- som Scott's arbejde blev kaldt -- en tyd i form af en matematisk funktion. Denotations-semantik er derfor en hjørnesten i enhver datalogs uddannelse og arbejde. Scott benyttede, i sin løsning af hvilken fikspunkt-tyd rekursivt formulerede -udtryk bestemmer, sig af gitterteori, og siden er mange andre former fra ikke-standard analyse blvet taget i brug. Den teoretiske datalog forventes derfor at have en stærk befæstning i gitterteori, Hausdorfske topologier, metriske rum, mv.

Ved ID/DTH blev der i 1980rne ydet væsentlige bidrag til denotationssemantikker for industrivendte programmeringssprog (CCITTs CHILL og US DoDs Ada) og for det første internationalt (ISO) standardiserede specifikationssprog VDM-SL. Uden først lektor Hans Bruun's og siden lektor Bo Stig Hansen's banebrydende arbejder ville ingen af disse tre sprog idag have en fornuftig formel semantik -- og ihvertfald ikke nogle der var lavet i Danmark! ID/DTH opnåede herved en internationalt anerkendt førerplads på området.



Dines Bjorner
Fri Sep 5 08:26:58 MET DST 1997