Denotationell semantik

Semantik för programspråk
Översikt – Grundbegrepp
Programspråk • Datavetenskap • Programmering • Kompilator • Formella metoder
Översikt – Typteori (nära kopplat)
Typsystem • Typsäkerhet • Datatyp
Semantikstilar
Denotationell semantik • Operationell semantik • Axiomatisk semantik • Aktionssemantik • Spelsemantik
Nyckelbegrepp
Kompositionalitet • Domänteori • Fixpunkt • Lambda-kalkyl • Monad • Abstrakt interpretation
Logik och formalisering
Logik • Modellteori • Syntax • Härledningsbegrepp
Språkvetenskaplig semantik (avgränsning)
Semantik • Denotation
Datalogi • Programmering • Formella metoder • Semantik

Inom datavetenskap är denotationell semantik (ibland kallad matematisk semantik eller Scott–Strachey-semantik) en metod för att formellt beskriva betydelsen av programmeringsspråk. Metoden bygger på att program och programuttryck tilldelas matematiska objekt, kallade denotationer, som representerar deras betydelse.[1]

Denotationell semantik är en av de tre klassiska angreppssätten inom formell semantik för programmeringsspråk, vid sidan av operationell semantik och axiomatisk semantik.[2]

Ett centralt krav inom denotationell semantik är att semantiken ska vara kompositionell: betydelsen av ett sammansatt programuttryck ska bestämmas entydigt av betydelsen hos dess deluttryck.[3]

Översikt

Grundidén i denotationell semantik är att tolka program som matematiska funktioner eller andra abstrakta strukturer. Till exempel kan:

  • uttryck tolkas som funktioner från en omgivning (miljö) till värden,
  • program tolkas som funktioner från indata till utdata,
  • icke-terminerande beräkningar representeras med särskilda bottenelement (⊥).[1]

För att kunna modellera rekursion och potentiellt oändliga beräkningar används ofta domänteori, där betydelser beskrivs med partiellt ordnade mängder och fixpunkter.[2]

Historik

Denotationell semantik utvecklades under slutet av 1960-talet och början av 1970-talet, främst genom arbeten av Dana Scott och Christopher Strachey. Deras mål var att ge programmeringsspråk en exakt matematisk grund som var oberoende av hur program faktiskt exekveras på en dator.[4]

Scott introducerade användningen av kontinuerliga funktioner över fullständigt partiellt ordnade mängder (CPO:er) för att hantera rekursion på ett matematiskt välgrundat sätt. Detta lade grunden för modern domänteori och denotationell semantik.[3]

Grundläggande begrepp

Domäner

En domän är ett matematiskt objekt som representerar möjliga värden av ett uttryck eller ett program. Domäner innehåller ofta ett särskilt element ⊥ som representerar icke-terminering eller odefinierade beräkningar.[1]

Miljöer

Betydelsen av ett programuttryck definieras ofta relativt en miljö, som anger vilka värden fria variabler har. Semantiken blir då en funktion från miljöer till värden i en domän.[2]

Fixpunkter

Rekursiva definitioner ges betydelse genom minsta fixpunkter av funktioner på domäner. Detta gör det möjligt att formellt definiera funktioner som till exempel fakultet eller rekursiva loopar.[3]

Exempel

Ett aritmetiskt uttryck som n * m tolkas i denotationell semantik som en funktion som, givet en miljö där n och m har värden, returnerar produkten av dessa värden.[1]

Rekursiva funktioner konstrueras som gränsvärden av successivt mer definierade approximationer, vilket säkerställer att betydelsen är matematiskt väldefinierad.[2]

Utvidgningar

Denotationell semantik har vidareutvecklats för att hantera mer avancerade språkegenskaper, såsom:

I vissa fall används alternativa matematiska ramverk, till exempel kategoriteori och spelbaserad semantik.[2]

Relation till andra semantiska metoder

Denotationell semantik skiljer sig från:

  • operationell semantik, som beskriver program genom exekveringssteg,
  • axiomatisk semantik, som beskriver program genom logiska egenskaper och bevis.[2]

En viktig forskningsfråga är i vilken utsträckning denotationell och operationell semantik sammanfaller, särskilt vad gäller full abstraktion.[3]

Betydelse och användning

Denotationell semantik används främst inom:

  • teoretisk datavetenskap,
  • utveckling och analys av programmeringsspråk,
  • formell verifiering och programsäkerhet,
  • undervisning i programmeringsspråksteori vid universitet och högskolor.[1]

Metoden ger ett kraftfullt verktyg för att resonera matematiskt om programs korrekthet och egenskaper, oberoende av implementation.[3]

Referenser

  1. 1 2 3 4 5 Joseph E. Stoy (1977). Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. ISBN 978-0262191470
  2. 1 2 3 4 5 6 Carl A. Gunter (1992). Semantics of Programming Languages: Structures and Techniques. ISBN 978-0262071437
  3. 1 2 3 4 5 6 Glynn Winskel (1993). The Formal Semantics of Programming Languages. ISBN 978-0262731034
  4. ↑ R. E. Milne & Christopher Strachey (1976). A Theory of Programming Language Semantics. Chapman and Hall. ISBN 978-0-412-16500-9

Vidare läsning

  • Joseph E. Stoy (1977). Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. ISBN 978-0262191470 
  • Glynn Winskel (1993). The Formal Semantics of Programming Languages. ISBN 978-0262731034 
  • Carl A. Gunter (1992). Semantics of Programming Languages: Structures and Techniques. ISBN 978-0262071437 

Externa länkar

Denna artikel är utgiven av Wikipedia. Texten är tillgänglig under Creative Commons Attribution-Share Alike 4.0 om inget annat anges. Ytterligare villkor kan gälla för mediefilerna.