Semàntica formal

La semàntica formal és l'estudi de les interpretacions dels llenguages formals. Els llenguages formals poden definir-se sense necessitat de donar cap significat a les seues expressions. Una interpretació d'un llenguage formal és bàsicament una assignació de significats als seus símbols, i de condicions de veres a les seues fòrmules ben formades.

Un objectiu important de la construcció d'una semàntica formal per a un llenguage formal és la caracterisació de la relació de conseqüència llògica en térmens semàntics, i la demostració de metateoremas a partir d'eixa caracterisació. Una volta definit lo que és una interpretació per a un llenguage formal, es diu que una fòrmula A és una conseqüència semàntica d'un conjunt de fòrmules $\Gamma$, si i només si para tota interpretació que fa verdaderes a les fòrmules en $\Gamma$, A també és verdadera.

Semàntica denotacional

En ciències de la computació la semàntica denotacional (inicialment com a semàntica matemàtica o semàntica Scott-Strachey) és una aproximació de la formalisació de llenguages de programació per construccions d'objectes matemàtics (denotació) que descriu el significat d'expressions del llenguage.

Donar una semàntica denotacional per a un llenguage consistix en definir funcions de valoració semàntica que assignen a cada element del llenguage un objecte matemàtic (com un conjunt) que modele el seu significat.

Els pioners en l'aproximació de la semàntica denotacional varen ser Christopher Strachey i Dana Scott, els qui varen publicar originalment el seu treball a principis de la década de 1970.

Una expressió aritmètica $a\in 𝐀𝐞𝐱𝐩$ es denotarà per $𝒜[[a]]:\Sigma \to 𝐍$, a on $𝐀𝐞𝐱𝐩$ està determinada per la sintaxis

$a::=n|X|a_0+a_1|a_0-a_1|a_0\times a_1$

i $\Sigma$ és el conjunt dels estats per la qual està identificat cada element. Els brackets $[[]]$ són tradicionals en la notació de semàntica denotacional. En realitat $𝒜$ és una funció d'expressions aritmètiques de tipo $𝐀𝐞𝐱𝐩\to (\Sigma \to 𝐍)$. Per eixemple, podríem escriure $𝒜{(}^{\prime }3+5^{\prime })\sigma =8$ en lloc de $𝒜[[3+5]]\sigma =8$. De forma més sotil, quan s'escriguen denotació com $𝒜[[a_0+a_1]]$ a on $a_0,a_1$ són metavariables, els interpretarem com a objectes del llenguage, i la suma és l'objecte sintàctic obtingut en reemplaçar el símbol "+" entre els objectes sintàctics $a_0$ i $a_1$.

Esta idea pot estendre's per a expressions booleanas i comandos. Si denotem a $𝐍=\{1,2,\dots \}$ al conjunt dels número natural i $𝐓=\{true,false\}$ al conjunt de valors de veres, definim les funcions semàntiques $𝒜:\mathbf{\text{𝐀𝐞𝐱𝐩}}\to (\Sigma \to 𝐍),ℬ:\mathbf{\text{𝐁𝐞𝐱𝐩}}\to (\Sigma \to 𝐍),𝒞:𝐂𝐨𝐦\to (\Sigma \to \Sigma )$per inducció estructural.

Vore també

• Interpretació (llògica)
• Llenguage formal