In de programmeertaaltheorie is semantiek de rigoureuze wiskundige studie van de betekenis van programmeertalen. Semantiek kent computationele betekenis toe aan geldige tekenreeksen in de syntaxis van een programmeertaal. Het is nauw verwant met de semantiek van wiskundige bewijzen.

Semantiek beschrijft de processen die een computer volgt bij het uitvoeren van een programma in die specifieke taal. Dit kan door de relatie tussen de input en output van een programma te beschrijven, of door uitleg te geven over hoe het programma op een bepaald platform zal worden uitgevoerd; vandaar het creëren van een rekenmodel.

Overzicht

Het gebied van de formele semantiek omvat al het volgende:

• De definitie van semantische modellen
• De relaties tussen verschillende semantische modellen
• De relaties tussen verschillende benaderingen van betekenis
• De relatie tussen berekeningen en de onderliggende wiskundige structuren uit velden als logica, verzamelingenleer, modeltheorie, categorietheorie, enz.

Het heeft nauwe banden met andere gebieden van de informatica, zoals het ontwerpen van programmeertalen, typetheorie, compilers en interpreters, programmaverificatie en model checking.

Benaderingen

Er zijn veel benaderingen van formele semantiek. Deze benaderingen behoren tot drie hoofdklassen:

• Denotationele semantiek, hierbij wordt elke zin in de taal geïnterpreteerd als een denotatie, dat wil zeggen een conceptuele betekenis die abstract kan worden bedacht. Dergelijke denotaties zijn vaak wiskundige objecten die een wiskundige ruimte bewonen, maar het is geen vereiste dat dit zo zou zijn. Uit praktische noodzaak worden denotaties beschreven met behulp van een of andere vorm van wiskundige notatie, die op zijn beurt kan worden geformaliseerd als een denotationele metataal. Denotationele semantiek van functionele talen vertaalt de taal bijvoorbeeld vaak in domeintheorie. Denotationele semantische beschrijvingen kunnen ook dienen als compositorische vertalingen van een programmeertaal naar de denotationele metataal. Deze beschrijvingen worden gebruikt als basis voor het ontwerpen van compilers.
• Operationele semantiek, hierbij wordt de uitvoering van de taal direct beschreven (in plaats van door vertaling). Operationele semantiek komt losjes overeen met interpretatie, hoewel de ‘implementatietaal’ van de tolk over het algemeen een wiskundig formalisme is. Operationele semantiek kan een abstracte machine definiëren (zoals de SECD-machine), en betekenis geven aan zinsdelen door de overgangen te beschrijven die ze teweegbrengen in de toestanden van de machine. Als alternatief kan, net als bij de pure lambdacalculus, operationele semantiek worden gedefinieerd via syntactische transformaties op zinnen van de taal zelf;
• Axiomatische semantiek, hierbij geeft men betekenis aan zinnen door de axioma's te beschrijven die erop van toepassing zijn. Axiomatische semantiek maakt geen onderscheid tussen de betekenis van een zin en de logische formules die deze beschrijven; de betekenis ervan is precies wat er in een bepaalde logica over bewezen kan worden. Het canonieke voorbeeld van axiomatische semantiek is de hoarelogica.

Afgezien van de keuze tussen denotationele, operationele of axiomatische benaderingen, komen de meeste variaties in formele semantische systemen voort uit de keuze om wiskundig formalisme te ondersteunen.