Programas Funcionales

Especificaciones (PF)

Suponiendo que sabemos la definición de un programa dado:

Por la definición de la función o por el problema que se nos plantea, podemos escribir una especificación mediante una expresión cuantificada:

Ya tenemos una una descripción formal de la tarea que el programa tiene que realizar

Derivaciones (PF)

Podemos no disponer de la definición de la función, pero sí de una especificación. En este caso, podemos derivar la definición de la función a partir de la especificación.

Por ejemplo, para encontrar el programa de la función $sum$ a partir de la especificación:

Caso base (cuanto vale $sum.[]$)

Por lo tanto, $sum.[] = 0$

Paso inductivo (cuanto vale $sum.(x \triangleright xs)$)

Por lo tanto, $sum.(x \triangleright xs) = x + sum.xs$

El programa sería:

Podemos recurrir a otras técnicas para derivar, estas se encuentran más abajo.

Análisis por casos

Supongamos que nuestro programa tiene la siguiente especificación:

Y en nuestro paso inductivo $(n + 1)$ llegamos a la siguiente expresión:

Observemos que la expresión $par.(n + 1)$ puede ser verdadera o falsa, por lo que debemos analizar ambos casos:

Caso 1: $par.(n + 1)$

Caso 2: $\neg par.(n + 1)$

Nuestra definición final sería:

Modularización

Supongamos que nuestro programa tiene la siguiente especificación:

Y en nuestro paso inductivo $(n + 1)$ llegamos a la siguiente expresión:

La expresión $x^n$ tiene sentido en el lenguaje de la matemática, no de los programas.
Podemos modularizar la expresión derivando otra función tal que:

Tras derivarla obtenemos:

Y podemos reemplazar la expresión en nuestra definición:

Generalización

Supongamos que nuestro programa tiene la siguiente especificación:

Al seguir en el paso inductivo $(x \triangleright xs)$, llegamos a la siguiente expresión:

No aplicar nuestra Hipótesis Inductiva, ya que tenemos:

Podemos generalizar $psum$ definiendo una nueva función $gpsum$, de forma tal que:

Podemos decir que $psum.xs = gpsum.0.xs$, ya que:

Una vez derivado $gpsum$, tendremos dos programas finales:

Esquemas de Inducción

En algunos casos los esquemas inductivos convencionales no son los necesarios para derivar.

En el caso de la inducción con naturales, tenemos:

Inducción Básica:

Inducción a lo Fibonacci:

En el caso de la inducción con listas, tenemos:

Inducción básica: ($sum$, $prod$, etc.)

Inducción con dos o más elementos: (funciones $iguales$, $minimo$ y $creciente$)

Ejemplo:

Si derivamos y el caso base es $[]$ , tendremos como resultado $\infty$.
Necesitamos reemplazar el caso base por $[x]$ y el Paso inductivo por $(x \triangleright y \triangleright xs)$.

Segmentos de listas

Podemos buscar un segmento inicial de una lista derivando la siguiente especificación.

Para derivarlo, nuestro esquema inductivo debe ser el siguiente:

Caso Base 1: ($xs = [], ys$)

Caso Base 2: ($xs, ys = []$)

Paso Inductivo: ($x \triangleright xs, y \triangleright ys$)

Ejercicios resueltos - Derivaciones y evaluaciones (PF)

1.

Calcular el resultado para la lista $[1, 2, 3, 4]$ dada la siguiente especificación:

Aplicamos la especificación de $sum$ para la lista $[1, 2, 3, 4]$:

El resultado para la lista $[1, 2, 3, 4]$ es $10$.

2.

Derivar la función $pin8$ a partir de la especificación (donde $prod$ es una función que devuelve el producto de los elementos de una lista):

Primero evaluamos el caso base, $xs = []$:

Por lo tanto, $pin8.[] = False$

Para el paso inductivo, seguimos con $xs = (x \triangleright xs)$:

Es necesario generalizar la función $pin8$ para poder derivarla. Definimos una nueva función $gpin8$ tal que:

Evaluamos el caso base de $gpin8$:

Seguimos con el paso inductivo de $gpin8$:

Los programas son:

3.

Derivar la función $minimo$ a partir de la especificación:

Primero evaluamos el caso base, $xs = []$:

No podemos computar $+\infty$, por lo que necesitamos cambiar nuestro esquema inductivo. Nuestra lista vacía no puede ser evaluada, por lo que necesitamos evaluar $[x]$.

Ahora seguimos con el paso inductivo $xs = (x \triangleright y \triangleright xs)$: