Semántica

Objetivo de aprendizaje

Al concluir este tema, el estudiante será capaz de:

1. Distinguir un programa correcto en su forma de uno que además tiene significado, y clasificar un error como léxico, sintáctico, semántico o de ejecución.
2. Describir el significado de una expresión mediante reducciones paso a paso, utilizando un entorno que asocia nombres con valores (semántica operacional).
3. Aplicar reglas de tipado para verificar una expresión antes de ejecutarla y justificar el tipo de cada subexpresión.
4. Explicar de manera intuitiva las semánticas denotacional y axiomática, y relacionarlas con la operacional.
5. Determinar si una tripleta de Hoare {P} S {Q} es válida y justificar la respuesta.

Ruta de trabajo del tema

1. Planteamiento inicial

En 1957, el lingüista Noam Chomsky propuso la siguiente oración para mostrar que la forma y el significado son asuntos distintos:

«Las ideas verdes incoloras duermen furiosamente».

La oración respeta la gramática del español: tiene sujeto, verbo y adverbio en el orden correcto. Sin embargo, carece de sentido, porque las ideas no tienen color, nada puede ser a la vez verde e incoloro, y las ideas no duermen. En un programa ocurre algo análogo. Considere la sentencia:

total = precio + descuento;

Es una sentencia bien formada: sus lexemas pertenecen al lenguaje y su estructura respeta la gramática. Sin embargo, no está claro que tenga significado.

Esta hipótesis se retomará al final de la sección 5.

2. Significado y semántica

Definición — Semántica: la semántica de un lenguaje de programación asigna significado a las construcciones sintácticamente válidas. Responde la pregunta: ¿qué hace este programa?

Las comprobaciones de significado se dividen en dos momentos:

• La semántica estática comprende las verificaciones que pueden realizarse antes de ejecutar el programa a partir de su texto: que cada variable esté definida y que los tipos de las operaciones sean compatibles.
• La semántica dinámica describe lo que ocurre durante la ejecución: qué valores se calculan, cómo cambia el estado y qué errores solo pueden descubrirse al conocer valores concretos.

Caso de estudio. Los cuatro tipos de error del procesamiento de un programa difieren en la fase que los detecta y en el momento en que ocurren:

Importante: existe además una cuarta categoría que ninguna fase detecta: el error lógico, en el que el programa es válido en todos los niveles y se ejecuta sin fallas, pero no hace lo que su autor pretendía (por ejemplo, calcular total = precio + descuento; cuando se quería restar el descuento). La semántica axiomática, que se estudia en la sección 5.2, ofrece una herramienta para razonar sobre este tipo de error.

Aplicación práctica: Mini v2. Para estudiar la semántica se amplía el lenguaje de juguete del tema anterior con sentencias, cadenas de texto y tres tipos de valor: entero, decimal y texto. Su gramática, en EBNF, es la siguiente:

<programa>  ::= { <sentencia> }
<sentencia> ::= IDENTIFICADOR "=" <expresion> ";"
              | "print" <expresion> ";"
<expresion> ::= <termino> { ("+" | "-") <termino> }
<termino>   ::= <factor> { ("*" | "/") <factor> }
<factor>    ::= NUMERO | TEXTO | IDENTIFICADOR | "(" <expresion> ")"

Práctica A: clasificación de errores por fase

Para cada programa, determine qué fase lo rechaza primero. Después de responder, la franja inferior muestra el recorrido del programa por las cuatro fases. Al final puede probar un programa propio.

3. Semántica operacional

Definición — Semántica operacional: describe el significado de un programa mediante su ejecución paso a paso en una máquina abstracta. El estado de la máquina incluye un entorno ρ: una asociación entre nombres de variables y valores.

Se escribe ⟨e, ρ⟩ ⇒ ⟨e′, ρ⟩ para indicar que, en el entorno ρ, la expresión e se reduce en un paso a la expresión e′. Las reglas de reducción de Mini son:

Las dos últimas reglas fijan el orden de evaluación: primero se reduce el operando izquierdo hasta que sea un valor, después el derecho, y solo entonces se aplica el operador. Por eso, en cada paso se reduce la subexpresión más interna situada más a la izquierda.

Caso de estudio. Con ρ = {x ↦ 3, y ↦ 4}, la expresión (x + 2) * y - 1 se reduce así: (x + 2) * y - 1 ⇒ (3 + 2) * y - 1 ⇒ 5 * y - 1 ⇒ 5 * 4 - 1 ⇒ 20 - 1 ⇒ 19.

Aplicación práctica. En la corrida siguiente se marca, en cada paso, la subexpresión que se va a reducir y se indica la regla aplicada. Se recomienda activar el modo de predicción: antes de cada paso se solicita identificar cuál subexpresión se reducirá.

De las expresiones a los programas

Una sentencia de asignación no es una ecuación, sino una instrucción que cambia el estado. Su regla es: se evalúa la expresión de la derecha con el entorno actual y el valor obtenido se asocia al nombre de la izquierda en el entorno (se escribe ρ[x ↦ v]). La sentencia print evalúa su expresión y escribe el valor en la salida. Así, x = x + 1; toma el valor que x tiene en este momento, le suma uno y lo guarda de nuevo en x.

La siguiente corrida ejecuta un programa sentencia por sentencia. Observe qué entrada de la tabla del entorno cambia y qué se escribe en la salida. El caso «Intercambio» muestra por qué se necesita una variable auxiliar, y el caso «Error de ejecución» muestra qué ocurre cuando una operación no puede completarse.

4. Sistema de tipos

Definición — Tipo y sistema de tipos: un tipo es un conjunto de valores junto con las operaciones permitidas sobre ellos. Un sistema de tipos es el conjunto de reglas que asigna un tipo a cada expresión y determina qué combinaciones son admisibles. La verificación de tipos es estática cuando se realiza antes de ejecutar y dinámica cuando se realiza durante la ejecución.

En Mini, la verificación es estática y el tipo de una variable queda fijado por su primera asignación. Las reglas de tipado de los operadores son las siguientes:

El verificador recorre el árbol de sintaxis abstracta de las hojas a la raíz: el tipo de una hoja procede de su literal o de la tabla de símbolos (la tabla que registra el tipo de cada variable definida), y el tipo de un operador se obtiene aplicando la regla a los tipos de sus operandos. Si no existe regla aplicable, se informa un error semántico sin haber ejecutado nada.

Aplicación práctica. La corrida siguiente muestra cómo los tipos se calculan nodo por nodo. Pruebe las expresiones con error (nombre * 2, precio + nombre y total + 1) y observe en qué nodo se detiene la verificación.

Error común: pensar que el verificador de tipos calcula los valores. La verificación estática solo razona con tipos: sabe que x / 0 es una operación numérica válida, pero no calcula el divisor. Por eso la división entre cero es un error de ejecución y no un error de tipos.

Nota: Mini no convierte automáticamente un texto en número ni al revés. Los lenguajes que no realizan esas conversiones implícitas se denominan de tipado fuerte (concepto que se amplía en el tema 2.5).

5. Otras formas de describir el significado

La semántica operacional responde cómo se ejecuta un programa. Existen dos enfoques formales adicionales que responden preguntas distintas. En este curso se estudian de manera intuitiva.

5.1 Semántica denotacional

Definición — Semántica denotacional: asocia a cada construcción del lenguaje un objeto matemático que representa su significado, normalmente una función. Una expresión con variables se interpreta como la función que, dado el valor de las variables, produce su resultado.

Caso de estudio. Las expresiones x + x y 2 * x tienen formas diferentes (distinta sintaxis y distintas reducciones), pero denotan la misma función: f(x) = 2x. Desde el punto de vista denotacional tienen el mismo significado. En cambio, x * x y x + x solo coinciden para algunos valores de x y, por tanto, denotan funciones distintas.

Aplicación práctica. Compare dos expresiones en el rango de valores x = −3, …, 5. El resultado indica si coinciden en todo el rango.

Nota: comprobar nueve valores no demuestra que dos expresiones sean equivalentes; solo permite descartar la equivalencia cuando aparece una diferencia. Una demostración exige razonar sobre todos los valores posibles de x. Esta distinción entre probar con ejemplos y demostrar es fundamental en la verificación de programas.

5.2 Semántica axiomática

Definición — Semántica axiomática: describe el significado de un programa mediante aserciones lógicas sobre su estado. Su unidad es la tripleta de Hoare {P} S {Q}, propuesta por C. A. R. Hoare en 1969: si antes de ejecutar S se cumple la precondición P, entonces después de ejecutarlo se cumple la poscondición Q.

Para la asignación existe una regla de sustitución hacia atrás: para que Q se cumpla después de x = e, basta con que antes se cumpla Q con x sustituida por e. Por ejemplo, para que x > 4 se cumpla después de x = x + 1, debe cumplirse antes x + 1 > 4, es decir, x > 3.

Caso de estudio. La tripleta {x = 3} x = x + 1 {x = 4} es válida. La tripleta {x > 0} x = x - 5 {x > 0} no lo es: basta el estado x = 1, que cumple la precondición y termina con x = −4.

Aplicación práctica. Determine si cada tripleta es válida. El verificador la comprueba exhaustivamente sobre un rango de estados y, cuando no es válida, muestra un contraejemplo. La tripleta del intercambio con variable auxiliar es un caso clásico de razonamiento sobre el estado.

5.3 Comparación de los tres enfoques

Contraste con el planteamiento inicial

6. Relación entre los niveles

El análisis semántico continúa la cadena de transformaciones iniciada en el tema anterior:

flowchart TD
    A["Árbol de sintaxis abstracta<br/>(tema 1.2.1)"] --> B["Verificador semántico<br/>(tabla de símbolos y tipos)"]
    B --> C["Árbol validado y anotado con tipos"]
    C --> D["Ejecución o generación de código<br/>(tema 1.2.4)"]
    B -. "error semántico" .-> E["Informe de error<br/>antes de ejecutar"]

Cada nivel abstrae a los anteriores: el verificador semántico ya no se ocupa de los caracteres ni de la estructura gramatical, sino únicamente del significado de un árbol que se supone bien formado.

7. Errores conceptuales frecuentes

Error común: interpretar el símbolo = de la asignación como una igualdad matemática. Es una instrucción que modifica el entorno.

Error común: creer que un programa sin errores léxicos ni sintácticos es correcto. Aún pueden existir errores semánticos, de ejecución y lógicos.

Error común: confundir el error semántico con el sintáctico. Usar una variable no definida no viola la gramática (y = x + 1; tiene estructura válida): viola una regla de significado.

Error común: suponer que todos los errores de tipos se detectan al ejecutar. Los lenguajes con verificación estática los detectan antes; los de verificación dinámica, durante la ejecución.

Error común: considerar demostrada una equivalencia o una propiedad por haberla comprobado con unos pocos ejemplos.

8. Verificación del tema

9. Libreta de trabajo

Reúna sus respuestas, revíselas y expórtelas como evidencia para el portafolio.

10. Preguntas de reflexión

1. Un programa puede superar las cuatro fases y, aun así, no hacer lo que su autor pretendía. ¿A qué nivel pertenece ese error y qué herramientas permitirían detectarlo?
2. ¿Qué ventajas y qué desventajas tiene verificar los tipos antes de ejecutar frente a hacerlo durante la ejecución?
3. En x = x + 1, el símbolo = no significa igualdad. ¿Qué otras notaciones podría haber elegido el diseñador del lenguaje para evitar la confusión (por ejemplo := o ←)? ¿Qué ventaja tendría cada una?
4. ¿Cómo cambiaría la regla de tipado del operador + si el lenguaje permitiera sumar un texto con un entero mediante una conversión automática? ¿Qué riesgos introduciría?
5. ¿Para qué clase de problema elegiría la semántica operacional y para cuál la axiomática?

11. Lecturas recomendadas

• Sebesta, R. (2015). Concepts of programming languages (11th ed.), capítulo «Describing Syntax and Semantics» (sección de semántica: operacional, denotacional y axiomática). Pearson.
• Scott, M. (2015). Programming language pragmatics (4th ed.), capítulo sobre análisis semántico. Morgan Kaufmann.
• Nystrom, R. (2021). Crafting Interpreters, capítulos «Evaluating Expressions», «Statements and State» y «Resolving and Binding». Acceso libre en craftinginterpreters.com.
• Thain, D. (2020). Introduction to Compilers and Language Design (2nd ed.), capítulos sobre análisis semántico y verificación de tipos. Acceso libre en www3.nd.edu/~dthain/compilerbook.
• Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576–580. (Lectura histórica.)
• Harper, R. (2016). Practical Foundations for Programming Languages (2nd ed.). Cambridge University Press. (Lectura avanzada; disponible en la bóveda.)