Semántica formal

La semántica formal es el estudio de las interpretaciones de los lenguajes formales.^[1] Los lenguajes formales pueden definirse sin necesidad de dar ningún significado a sus expresiones.^[1] Una interpretación de un lenguaje formal es básicamente una asignación de significados a sus símbolos, y de condiciones de verdad a sus fórmulas bien formadas.^[1]

Un objetivo importante de la construcción de una semántica formal para un lenguaje formal es la caracterización de la relación de consecuencia lógica en términos semánticos, y la demostración de metateoremas a partir de esa caracterización.^[1] Una vez definido lo que es una interpretación para un lenguaje formal, se dice que una fórmula A es una consecuencia semántica de un conjunto de fórmulas $\Gamma$ , si y sólo si para toda interpretación que hace verdaderas a las fórmulas en $\Gamma$ , A también es verdadera.^[1]

Semántica denotacional

En ciencias de la computación la semántica denotacional (inicialmente como semántica matemática o semántica Scott-Strachey) es una aproximación de la formalización de lenguajes de programación por construcciones de objetos matemáticos (denotaciones) que describe el significado de expresiones del lenguaje.

Dar una semántica denotacional para un lenguaje consiste en definir funciones de valoración semántica que asignan a cada elemento del lenguaje un objeto matemático (como un conjunto) que modele su significado.

Los pioneros en la aproximación de la semántica denotacional fueron Christopher Strachey y Dana Scott, quienes publicaron originalmente su trabajo a principios de la década de 1970.

Una expresión aritmética^[2] $a\in \mathbf {Aexp}$ se denotará por ${\mathcal {A}}[[a]]:\Sigma \to \mathbf {N}$ , donde $\mathbf {Aexp}$ está determinada por la sintaxis

$a::=n\;|\;X\;|\;a_{0}+a_{1}\;|\;a_{0}-a_{1}\;|\;a_{0}\times a_{1}$

y $\Sigma$ es el conjunto de los estados por la cual está identificado cada elemento. Los brackets $[[\;]]$ son tradicionales en la notación de semántica denotacional. En realidad ${\mathcal {A}}$ es una función de expresiones aritméticas de tipo $\mathbf {Aexp} \to (\Sigma \to \mathbf {N} )$ . Por ejemplo, podríamos escribir ${\mathcal {A}}('3+5')\sigma =8$ en lugar de ${\mathcal {A}}[[3+5]]\sigma =8$ . De forma más sutil, cuando se escriban denotaciones como ${\mathcal {A}}[[a_{0}+a_{1}]]$ donde $a_{0},a_{1}$ son metavariables, los interpretaremos como objetos del lenguaje, y la suma es el objeto sintáctico obtenido al reemplazar el símbolo "+" entre los objetos sintácticos $a_{0}$ y $a_{1}$ .

Esta idea puede extenderse para expresiones booleanas y comandos. Si denotamos a $\mathbf {N} =\{1,2,\dots \}$ al conjunto de los números naturales y $\mathbf {T} =\{true,false\}$ al conjunto de valores de verdad, definimos las funciones semánticas ${\mathcal {A}}:{\textbf {Aexp}}\to (\Sigma \to \mathbf {N} ),\;{\mathcal {B}}:{\textbf {Bexp}}\to (\Sigma \to \mathbf {N} ),\;{\mathcal {C}}:\mathbf {Com} \to (\Sigma \to \Sigma )$ por inducción estructural.

Véase también

Notas y referencias

↑ ^a ^b ^c ^d ^e Robert Audi, ed. (1999). «formal semantics». The Cambridge Dictionary of Philosophy (en inglés) (2da edición edición). Cambridge University Press.
↑ Winskel, Glynn (1994). «Capítulo 5 - The denotational semantics of IMP». The formal Semantics of Programming Languages. An Introduction. (en inglés). Estados Unidos: MIT. ISBN 0-262-23169-7.

Datos: Q963731

[Cambridge-1] Robert Audi, ed. (1999). «formal semantics». The Cambridge Dictionary of Philosophy (en inglés) (2da edición edición). Cambridge University Press.

[2] Winskel, Glynn (1994). «Capítulo 5 - The denotational semantics of IMP». The formal Semantics of Programming Languages. An Introduction. (en inglés). Estados Unidos: MIT. ISBN 0-262-23169-7.

[1]

[2]