Semántica formal

estudio de las interpretaciones de los lenguajes formales

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 , si y sólo si para toda interpretación que hace verdaderas a las fórmulas en , A también es verdadera.[1]

Semántica denotacional

editar

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]  se denotará por  , donde   está determinada por la sintaxis

 

y   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   es una función de expresiones aritméticas de tipo  . Por ejemplo, podríamos escribir   en lugar de  . De forma más sutil, cuando se escriban denotaciones como   donde   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   y  .

Esta idea puede extenderse para expresiones booleanas y comandos. Si denotamos a   al conjunto de los números naturales y   al conjunto de valores de verdad, definimos las funciones semánticas  por inducción estructural.

Véase también

editar

Notas y referencias

editar
  1. 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. 
  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.