« Llegan las Jornadas F… « || Inicio || » Curso acelerado de Ló… »

Cómo se demuestra que un programa es correcto: Semántica Denotacional

Última modificación: 10 de Noviembre de 2015, y ha tenido 345 vistas

Etiquetas utilizadas: || || || ||

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.

El primero de ellos, la semántica operacional, intenta dar un signficado 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 éstos, se ajustan mejor para ver cómo la sucesión de operaciones modifica el estado global que determina la computación del programa. 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.

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

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, es decir, deja de poner el foco en el "cómo" para centrarse en el "qué". Veremos que la semántica denotacional hace uso extensivo del lambda cálculo (en su versión extendida con recursión) para esta tarea, sea cual sea el lenguaje de programación que use el programa que queremos verificar, 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 no pretendemos dar una visión en profundidad de esta técnica, que cubre toda un área de la computación matemática, intentaremos 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 que muy comúnmente se obtengan soluciones muy ineficientes, ya que los compiladores no están optimizados para su uso.

Definiciones recursivas de funciones

En el contexto de las defniciones 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. 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. Por ejemplo, encontramos una definición circular habitual en las ecuaciones algebráicas, cuando decimos que:

\(x = 2x - 1\)

\(x = x^2 - 4x + 6\)

\(x = x + 1\)

\(x = x^2 / x\)

donde las soluciones respectivas 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 (porque estamos buscando computaciones deterministas... aunque podríamos intentar definir computaciones no deterministas, eso está fuera de las intenciones de esta entrada). 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).

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 algebráicas 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 un objeto matemático consistente. 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\). 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\). 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.\)

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" (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\)).

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.

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.

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)\)

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 (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). 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\)

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í).

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 (observa que \(Fix\) hace uso de las mismas funciones componentes con las que se construye \(f\), pero sin hacer uso de recursión). Pero aprovechando el uso de las definiciones de orden superior, incluso podemos dar una definición de \(F\) que es más general y no depende de la expresión de la \(f\) original, sino que puede utilizar de forma abstracta el patrón recursivo que se quiere comprobar.

Para saber más...

Haskell/Fix and recursion

Haskell/Denotational semantics

You could have re-invented fix too!

Denotational semantics

« Llegan las Jornadas F… « || Inicio || » Curso acelerado de Ló… »