**Semántica Denotacional: cómo se demuestra que un programa es correcto** Es habitual escribir que una de las bondades habituales de los lenguajes funcionales (puros) es la capacidad que nos proporcionan para poder asegurar que los programas (funciones) escritos en ellos hacen realmente lo que decimos que hacen (es decir, que se ajustan fielmente al objetivo para el que fueron diseñados). En esencia, el mecanismo más fiable que tenemos para poder asegurar la veracidad de una afirmación en cualquier dominio de conocimiento pasa por proyectar una sección de dicho dominio sobre un lenguaje formal matemático para, posteriormente, utilizar la lógica matemática con el fin de dar una demostración completa de que, en efecto, la afirmación es correcta. En el mundo de la verificación de programas hay dos técnicas que destacan por encima de las demás para realizar todo el proceso desde un punto de vista matemático: la **semántica operacional** y la **semántica denotacional**. !!!side:1 Normalmente, dan lugar a complejas demostraciones que no parecen estar en la línea de las abstracciones generalistas que podemos encontrar en la mayoría de las demostraciones matemáticas. El primero de ellos, la semántica operacional, intenta dar un significado a las construcciones del lenguaje de programación (programas) por medio de la computación que generan cuando se ejecuta en una máquina/compilador/intérprete hipotético. De esta forma, la semántica operacional se preocupa más por el *cómo* se ejecutan los programas en lugar de hacer énfasis en los resultados, por lo que dependen en gran medida de la implementación concreta tanto de las primitivas del lenguaje de programación que se usen como del programa concreto que estemos verificando y que hace uso de ellas. Ha sido, bastante utilizado para verificar programas de lenguajes de programación imperativos, ya que, por las características de estos, se ajustan mejor para ver cómo la sucesión de operaciones modifica el estado global que determina la computación del programa [1]. !!!side:2 D. Scott, C. Strachey. *Toward a mathematical semantics for computer languages*, Oxford Programming Research Group, Technical Monograph. PRG-6. 1971. En consecuencia, no es de extrañar que esta técnica quede lejos del espíritu que guía a los lenguajes funcionales, que en su fondo y forma se acercan más a un lenguaje formal matemático que a una simple descripción de una máquina operativa. Por ello, a finales de los años 60, **Scott** y **Strachey** introdujeron la semántica denotacional como un método alternativo de realizar esta tarea y que se ajustaba especialmente bien para la verificación de programas escritos en lenguajes funcionales [2]. Esta proyección del dominio del programa original en el dominio de las matemáticas es lo que de hecho se conoce como una **semántica**, es decir, una interpretación de los componentes funcionales que se usan de facto por medio de los objetos matemáticos que se usarán para demostrar su validez. !!!side:3 Es decir, deja de poner el foco en el *cómo* para centrarse en el *qué*. !!!alg En general, el propósito de la semántica denotacional es proporcionar las descripciones matemáticas de los lenguajes de programación de forma independiente de su comportamiento operativo [3]. Veremos que, sea cual sea el lenguaje de programación que use el programa que queremos verificar, la semántica denotacional hace uso extensivo del lambda cálculo (en su versión extendida con recursión) para esta tarea, por lo que no resulta extraño que sea especialmente adecuado para los lenguajes de programación funcionales, que también se basan en ese mismo formalismo. Aunque el objetivo de esta entrada no es dar una visión en profundidad de esta técnica, que cubre toda un área de la computación matemática, sí que se intentará dar la suficiente información acerca de cómo se relaciona este método con la existencia de las funciones definidas por recursión. # Conceptos Básicos y Ejemplos Ya hemos visto en otras entradas relacionadas con la programación funcional cómo el uso del patrón de recursión es especialmente natural para definir funciones y dar soluciones a problemas. Esto no es así en la mayoría de lenguajes imperativos, donde a menudo hay que hacer uso de complejas estructuras de punteros para conseguir realizar una recursión, lo que provoca obtener soluciones muy ineficientes, ya que los compiladores no están optimizados para su uso. ## Definiciones recursivas de funciones En el contexto de las definiciones denotacionales, cuando se define un nuevo símbolo en un programa, esperamos que haya coherencia para poder reemplazar cada aparición del símbolo por su significado (o valor). En esencia, un símbolo nuevo no es más que un atajo de la expresión que se le asocia (de forma similar a como se reconocen las variables en los lenguajes funcionales, algo muy distinto a lo que ocurre en los lenguajes imperativos). En particular, esperamos que el símbolo se defina en términos de otros conceptos (preferiblemente más simples) de forma que cualquier expresión en la que intervenga se pueda reescribir sustituyéndolo por su definición. !!!ejemplo Con esta idea en mente, vamos a considerar las dos definiciones siguientes: $$f(n)= \left\{ \begin{array}{lcc} 1, & si & n = 0 \\ f(n-1), & si & n \neq 0 \end{array} \right.$$ $$g(n)= \left\{ \begin{array}{lcc} 1, & si & n = 0 \\ g(n+1), & si & n \neq 0 \end{array} \right.$$ Debido a que ambas definiciones hacen uso del propio símbolo en el cuerpo de definición, es imposible seguir la regla de que el símbolo pueda ser reemplazado por su definición. De alguna forma, las definiciones son circulares, pero eso no significa que no sean correctas y no signifiquen nada, sino que su significado lo obtendremos por medio de algún mecanismo distinto a la simple sustitución. En este sentido, y siguiendo otras situaciones similares de definiciones circulares que se dan en matemáticas, podremos obtener el significado del símbolo por medio de las soluciones a una determinada ecuación que se extrae de la definición circular que se ha dado. !!!side:4 En esta entrada estamos buscando computaciones deterministas, pero podríamos buscar definiciones válidas para computaciones no deterministas,... aunque no en esta entrada. !!!ejemplo Por ejemplo, encontramos una definición circular habitual en las ecuaciones algebraicas, cuando decimos que: $$x = 2x - 1$$ $$x = x^2 - 4x + 6$$ $$x = x + 1$$ $$x = x^2 / x$$ donde las soluciones que se obtienen nos dicen, respectivamente, que \(x=1\) (solución única), \(x=\{2,3\}\) (solución multiple), \(x\) no existe, o \(x\) tiene infinitas soluciones. Si vamos a trabajar con el significado de \(x\) para sustituirlo posteriormente, debemos dar un mecanismo para tenerlo siempre definido y de forma única [4]. Observa que en todos los casos anteriores estamos resolviendo una ecuación del tipo: $$x = P(x)$$ por lo que decimos que hemos buscado un **punto fijo** de \(P\) para obtener el significado de \(x\) (se dice que es un punto fijo porque, una vez que obtenemos el valor de \(x\) verificando \(P(x)=x\), la aplicación sucesiva de \(P\) no lo modifica). !!!ejemplo Aunque todavía no tenemos medios para probarlo, podemos intentar buscar soluciones intuitivas a las funciones definidas anteriormente, y tras analizar cómo se comportan sobre ciertos valores concretos, podemos concluir que: $$f(n) = 1, \forall n$$ $$g(n)= \left\{ \begin{array}{lcc} 1, & si & n = 0 \\ no\ definida, & si & n \neq 0 \end{array} \right.$$ Precisamente, uno de los puntos fundamentales de la semántica denotacional es el de dar un mecanismo para poder extraer una solución única de definiciones recursivas como las anteriores. Al igual que en las ecuaciones algebraicas hemos buscado el punto fijo de una determinada ecuación para obtener el significado de \(x\), en el caso de la definición recursiva de funciones también veremos que existe una función (que opera sobre funciones) cuyo punto fijo es precisamente la función recursiva que estamos definiendo. De esta forma, nos saltamos el proceso de definición recursivo para definir \(f\) y obtenemos directamente su significado, haciendo posible el objetivo denotacional de poder reemplazar de forma segura el símbolo por una expresión que hace uso de elementos más simples. Las funciones en general son centrales en ciencias de la computación, y en particular las definiciones por recursión no solo tienen interés a la hora de definir otras funciones y programas, sino que se usan también para describir la semántica de los lenguajes de programación y los tipos de datos más complejos. Sin embargo, debido a que la mayoría de las paradojas lógicas y de teoría de conjuntos provienen de definiciones circulares, la recursión suele levantar ciertas suspicacias y requiere una demostración concluyente para poder asegurar que los objetos definidos por este medio no plantearán problemas y tienen asociados objetos matemáticos consistentes. La forma más directa y elegante de conseguir esta demostración es haciendo uso de lo que se llama **Teoría de Dominios** (conjuntos completos parcialmente ordenados) y una **Teoría de Punto Fijo** asociada. Aunque un blog como este no es el lugar adecuado para dar una visión en profundidad de la conjunción de estas teorías, intentaremos presentar en las siguientes líneas las ideas principales que nos permiten intuir la forma en que podría ir la demostración general. # Interpretando funciones parciales como funciones totales Como hemos visto en los ejemplos anteriores, podemos encontrarnos con funciones que para alguno (o muchos) de los valores de entrada no devuelven ningún valor (si las funciones son el resultado de la ejecución de un programa, este hecho sería el resultado, por ejemplo, de una computación que no para). Con el fin de poder manipular este tipo de funciones desde un punto de vista formal, lo primero que vamos a hacer va a ser completarlas añadiendo un valor adicional que significará *no definido*, y que denotaremos por \(\bot\). !!!def A las funciones que están definidas en todo su dominio se les denomina **totales**, frente a las **parciales**, que presentan problemas de definición o cálculo en alguna parte de su dominio. De esta forma, si tenemos una función \(g:\mathbb{N} \rightarrow \mathbb{N}\), que para algunos valores no está definida, podemos considerar la extensión natural, \(g^*\), a \(\mathbb{N}\cup \{\bot\}\), de forma que se comporte exactamente igual que \(g\) para aquellos casos en que no hay problemas de definición y como \(g^*(n)=\bot\) para aquellos casos en que \(g\) no está definida. Para no tener que hacer separaciones entre funciones totales y parciales, añadiremos también el nuevo objeto al dominio, haciendo que \(g^*(\bot)=\bot\). !!!ejemplo Por ejemplo, haciendo uso de la función recursiva que definimos anteriormente: $$g^*: \mathbb{N}\cup \{\bot\} \rightarrow \mathbb{N}\cup \{\bot\}$$ $$g^*(n)= \left\{ \begin{array}{lcc} 1 & si & n = 0 \\ \bot & si & n \neq 0 \end{array} \right.$$ !!!side:5 La función \(\bot\) será una función que no está definida en ningún punto de su dominio, es decir: \(\bot(x)=\bot\), haciendo uso extendido del símbolo \(\bot\). Evidentemente, esta extensión se puede hacer no solo para las funciones definidas sobre los números naturales, sino para las funciones definidas sobre cualquier tipo de datos, incluso aquellos tipos que representan funciones, algo habitual en los lenguajes de programación funcional. Y es más, el elemento \(\bot\) es el mismo para todos ellos, y tendrá el mismo significado de *no definido* [5]. Tras esta extensión, hay que tener en cuenta algunas consideraciones para que todo siga funcionando igual, ya que, por ejemplo, no tiene sentido definir algo como \(g(\bot)=1\), sino que debería cumplirse siempre que \(g(\bot)=\bot\) sea cual sea \(g\). En general, hemos de imponer algunas condiciones adicionales para estar seguros de que la convergencia de funciones se comporta como esperamos, y esta convergencia será necesaria para asegurar que matemáticamente podemos encontrar siempre la función que se define por medios recursivos. Concretamente, exigiremos lo que se conoce como **monoticidad** respecto de la información almacenada en los elementos. !!!def En general, si añadimos el elemento \(\bot\) a cualquier dominio para considerar su extensión natural, diremos que **\(\bot\) es menos informativo que cualquier otro elemento del dominio**. De esta forma, damos un medio de comparar esos objetos, y lo escribiremos como \(\bot \sqsubseteq x\). Además, impondremos que el resto de elementos del mismo dominio no son comparables entre si (salvo cada objeto consigo mismo), dando lo que se conoce como un **orden parcial**.  !!!def Dado este orden en los dominios, diremos que una función, \(f:\mathbb{D}\rightarrow \mathbb{D}\) (\(\mathbb{D}\) es su dominio extendido) es **monótona** (a veces también se habla de **continuidad**) si: $$\forall x,y\in \mathbb{D},\ x \sqsubseteq y \Rightarrow f(x) \sqsubseteq f(y)$$ !!!side:6 Observa que, en principio, haber dado una expresión por recursión no asegura que se corresponda con una función matemática, eso es parte de lo que hay que probar. De esta forma conseguimos ciertas propiedades (que no veremos aquí) que son de vital importancia para asegurar la existencia de la función matemática que se corresponde con la función que hemos definido por recursión [6]. La teoría matemática que hay detrás de estas extensiones y los resultados que los soportan es lo que se conoce como **Teoría de Dominios**. # Recursión como Punto Fijo Para ilustrar el método que se sigue para probar la existencia de la función definida por recursión, vamos a utilizar la función más habitual de las que se definen por recursión: la **función factorial** (\(f(n)=n!=n\cdot (n-1)\cdot\dots\cdot 1\)), cuya expresión recursiva más habitual es la siguiente: $$f(n)= \left\{ \begin{array}{lcc} 1, & si & n = 0 \\ n\cdot f(n-1), & si & n \neq 0 \end{array} \right.$$ Vamos a convertir las llamadas recursivas en una sucesión de funciones que, poco a poco, se van aproximando a la función que, intuitivamente, hemos definido por recursión. Para eso: $$f_0(n)=\bot, \forall n$$ $$f_{k+1}(n)= \left\{ \begin{array}{lcc} 1 & si & n = 0 \\ n\cdot f_k(n-1) & si & n \neq 0 \end{array} \right.$$  Los valores que van calculando estas funciones son: $$f_0=\{\bot,\ \bot,\ \dots\}$$ $$f_1=\{1,\ \bot,\ \dots\}$$ $$f_2=\{1,\ 1,\ \bot,\ \dots\}$$ $$f_3=\{1,\ 1,\ 2,\ \bot,\ \dots\}$$ $$f_4=\{1,\ 1,\ 2,\ 6,\ \bot,\ \dots\}$$ De esta forma, si consideramos las funciones como el tipo de datos sobre el que trabajamos, podemos escribir: $$\bot=f_0 \sqsubseteq f_1 \sqsubseteq f_2 \sqsubseteq f_3 \sqsubseteq f_4 \sqsubseteq \dots$$ Si definimos la siguiente función de orden superior (que no es una función recursiva): $$Fix(f) (n)= \left\{ \begin{array}{lcc} 1 & si & n = 0 \\ n\cdot f(n-1) & si & n \neq 0 \end{array} \right.$$ entonces podemos escribir la sucesión anterior como: $$\bot,\ Fix(\bot),\ Fix(Fix(\bot)),\ Fix(Fix(Fix(\bot))),\ \cdots$$ !!!side:7 En este caso, el punto fijo es el mínimo superior de esta cadena, que es la función factorial completa, que puede expresarse como la unión $${\displaystyle \bigcup _{i\in \mathbb {N} }Fix^{i}(\bot)}$$ El punto fijo que encontramos es el menor punto fijo de $Fix$, porque nuestra iteración empezó con el elemento más pequeño del dominio (la función no definida). Para demostrarlo necesitamos un teorema de punto fijo más complejo, como el [Teorema de Knaster-Tarski](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem). Por lo que la función factorial que hemos definido por recursión se convierte en el punto fijo de \(Fix\) (por eso el nombre que le hemos dado a la función). La existencia de tal punto fijo la aseguran algunos resultados de convergencia generales bien establecidos (y que no veremos aquí). !!!side:8 Observa que \(Fix\) hace uso de las mismas funciones componentes con las que se construye \(f\), pero sin hacer uso de recursión. Lo interesante del método que hemos mostrado es que se puede reconstruir para cualquier función recursiva, construyendo una función \(Fix\) específica para cada función recursiva que estamos comprobando [8]. Además, aprovechando el uso de las definiciones de orden superior, incluso podríamos dar una definición de \(F\) más general y que no dependiera de la expresión de la \(f\) original, sino que puede utilizar de forma abstracta el patrón recursivo que se quiere comprobar y que valiese de forma general. # Conexiones con otras áreas !!!alg *No es necesario que la semántica determine una implementación, pero debe proporcionar criterios para demostrar que una implementación es correcta*. (Dana Scott, 1980) Al interpretar los tipos como dominios en el sentido de la teoría de dominios, el área se relaciona con la *Teoría de modelos*, lo que ha dado lugar a conexiones con la *Teoría de Tipos* y la *Teoría de Categorías*. Dentro de la informática, existen conexiones con la interpretación abstracta, la verificación de programas y la comprobación de modelos. (insert menu.md.html here)