Programas Funcionales
Especificaciones (PF)
Suponiendo que sabemos la definición de un programa dado:
\[\begin{array}{l} \Big\vert\ sum : [Num] \to Num \\ \overline{\Big\vert \; sum.[] \doteq 0} \\ \Big\vert\ sum.(x \triangleright xs) \doteq x + sum.xs \end{array} \]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:
\[sum.xs = \bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle \]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:
\[sum.xs = \bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle \]Caso base (cuanto vale \(sum.[]\))
\[\begin{array}{ll} \underline{sum.[]} \\ \\ \equiv \{ \textnormal{ Especificación de } sum \; \} \\ \\ \bigl \langle \; \sum i : 0 \leq i < \underline{ \# []} : [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \; \} \\ \\ \bigl \langle \; \sum i : \underline{0 \leq i < 0 }: [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ \bigl \langle \; \sum i : \underline{False} : [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ 0 \end{array} \]Por lo tanto, \(sum.[] = 0\)
Paso inductivo (cuanto vale \(sum.(x \triangleright xs)\))
\[HI : sum.xs = \bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle \] \[\begin{array}{ll} \underline{sum.(x \triangleright xs)} \\ \\ \equiv \{ \textnormal{ Especificación de } sum \; \} \\ \\ \bigl \langle \; \sum i : 0 \leq i < \underline{\# (x \triangleright xs)} : (x \triangleright xs).i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \; \} \\ \\ \underline{\bigl \langle \; \sum i : 0 \leq i < 1 + \# xs : (x \triangleright xs).i \; \bigr \rangle \\} \\ \\ \equiv \{ \textnormal{ Separación de un término } \} \\ \\ \underline{(x \triangleright xs).0} + \bigl \langle \; \sum i : 0 \leq i < \# xs : \underline{(x \triangleright xs).(i + 1)} \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } . \; \} \\ \\ x + \underline{\bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Hipótesis inductiva } \} \\ \\ x + sum.xs \end{array} \]Por lo tanto, \(sum.(x \triangleright xs) = x + sum.xs\)
El programa sería:
\[\begin{array}{l} \Big\vert\ sum : [Num] \to Num \\ \overline{\Big\vert \; sum.[] \doteq 0} \\ \Big\vert\ sum.(x \triangleright xs) \doteq x + sum.xs \end{array} \]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:
\[sum \_ par.n + \bigl \langle \; \sum i : 0 \leq i \leq n \land par.i : i \; \bigr \rangle \]Y en nuestro paso inductivo \((n + 1)\) llegamos a la siguiente expresión:
\[sum \_ par.n + \bigl \langle \; \sum i : i = n + 1 \land par.(n + 1) : i \; \bigr \rangle \]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)\)
\[\begin{array}{ll} sum \_ par.n + \bigl \langle \; \sum i : i = n + 1 \land \underline{par.(n + 1)} : i \; \bigr \rangle \\ \\ \equiv \{ \; \textnormal{Caso 1:} \; par.(n + 1) \; \} \\ \\ sum \_ par.n + \bigl \langle \; \sum i : i = n + 1 \land True : i \; \bigr \rangle \\ \\ ... \\ \\ sum \_ par.n + n + 1 \end{array} \]Caso 2: \(\neg par.(n + 1)\)
\[\begin{array}{ll} sum \_ par.n + \bigl \langle \; \sum i : i = n + 1 \land \underline{par.(n + 1)} : i \; \bigr \rangle \\ \\ \equiv \{ \; \textnormal{Caso 2:} \; \neg par.(n + 1) \; \} \\ \\ sum \_ par.n + \bigl \langle \; \sum i : i = n + 1 \land False : i \; \bigr \rangle \\ \\ ... \\ \\ sum \_ par.n \end{array} \]Nuestra definición final sería:
\[\begin{array}{l} \Big\vert\ sum \_ par : Num \to Num \\ \overline{\Big\vert \; sum \_ par.0 \doteq 0} \\ \Big\vert\ sum \_ par.(n + 1) \doteq ( \\ \Big\vert\ □ \; par.(n+1) → sum \_ par.n + n + 1 \\ \Big\vert\ □ \; \neg par.(n+1) → sum \_ par.n \\ \Big\vert\ ) \end{array} \]Modularización
Supongamos que nuestro programa tiene la siguiente especificación:
\[f.x.n = \bigl \langle \; \sum i : 0 \leq i \leq n : x^i \; \bigr \rangle \]Y en nuestro paso inductivo \((n + 1)\) llegamos a la siguiente expresión:
\[f.x.n + \textcolor{darkred}{x^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:
\[\begin{array}{l} \Big\vert\ exp : Num \to Num \to Num \\ \overline{\Big\vert \; exp.x.0 \doteq 1} \\ \Big\vert\ exp.x.(n + 1) \doteq n * exp.x.n \end{array} \]Y podemos reemplazar la expresión en nuestra definición:
\[\begin{array}{l} \Big\vert\ f : Num \to Num \to Num \\ \overline{\Big\vert \; f.x.0 \doteq x} \\ \Big\vert\ f.x.(n + 1) \doteq f.x.n + exp.x.n \end{array} \]Generalización
Supongamos que nuestro programa tiene la siguiente especificación:
\[psum.xs = \bigl \langle \; \forall i : 0 \leq i < \# xs : sum.(xs↑i) \geq 0 \; \bigr \rangle \]Al seguir en el paso inductivo \((x \triangleright xs)\), llegamos a la siguiente expresión:
\[\begin{array}{ll} \underline{psum}.(x \triangleright xs) \\ \\ \equiv \{ \textnormal{ Especificación de } psum \} \\ \\ \bigl \langle \; \forall i : 0 \leq i < \underline{\# (x \triangleright xs)} : sum.((x \triangleright xs)↑i) \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \} \\ \\ \bigl \langle \; \forall i : \underline{0 \leq i < 1 + \# xs} : sum.((x \triangleright xs)↑i) \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ \bigl \langle \; \forall i : \underline{i = 0 \lor 1 \leq i < \# xs + 1} : sum.((x \triangleright xs)↑i) \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de Rango } \} \\ \\ \underline{\bigl \langle \; \forall i : i = 0 : sum.((x \triangleright xs)↑i) \geq 0 \; \bigr \rangle \; \land \; \bigl \langle \; \forall i : 1 \leq i < \# xs + 1 : sum.((x \triangleright xs)↑i) \geq 0 \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Rango unitario, Cambio de Variable: i ← i + 1 } \} \\ \\ sum.((\underline{x \triangleright xs)↑0}) \geq 0 \; \land \; \bigl \langle \; \forall i : 1 \leq i < \# xs + 1 : sum.(\underline{(x \triangleright xs)↑(i + 1)}) \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } ↑, \textnormal{ Aritmética } \} \\ \\ \underline{sum.[]} \geq 0 \land \bigl \langle \; \forall i : 0 \leq i < \# xs : \underline{sum.((x \triangleright (xs↑i)))} \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } sum \} \\ \\ \underline{0 \geq 0} \land \bigl \langle \; \forall i : 0 \leq i < \# xs : x + sum.(xs↑i) \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética, Elemento neutro de } \land \} \\ \\ \bigl \langle \; \forall i : 0 \leq i < \# xs : x + sum.(xs↑i) \geq 0 \; \bigr \rangle \end{array} \]No aplicar nuestra Hipótesis Inductiva, ya que tenemos:
\[\begin{array}{ll} \bigl \langle \; \forall i : 0 \leq i < \# xs : sum.(xs↑i) \geq 0 \; \bigr \rangle \; (HI) \\ \\ \bigl \langle \; \forall i : 0 \leq i < \# xs : \textcolor{darkred}{x} + sum.(xs↑i) \geq 0 \; \bigr \rangle \end{array} \]Podemos generalizar \(psum\) definiendo una nueva función \(gpsum\), de forma tal que:
\[gpsum.n.xs = \bigl \langle \; \forall i : 0 \leq i < n : \textcolor{darkred}{n} + sum.(xs↑i) \geq 0 \; \bigr \rangle \]Podemos decir que \(psum.xs = gpsum.0.xs\), ya que:
\[\begin{array}{ll} \underline{gpsum}.0.xs \\ \\ \equiv \{ \textnormal{ Especificación de } gpsum \} \\ \\ \bigl \langle \; \forall i : 0 \leq i < \underline{0} : \underline{0 + sum.(xs↑i)} \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ \underline{\bigl \langle \; \forall i : 0 \leq i < 0 : sum.(xs↑i) \geq 0 \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Especificación de } psum \} \\ \\ psum.xs \end{array} \] \[\begin{array}{l} \Big\vert\ psum : [Num] \to Bool \\ \overline{\Big\vert \; psum.xs} \doteq gpsum.0.xs \end{array} \]Una vez derivado \(gpsum\), tendremos dos programas finales:
\[\begin{array}{l} \Big\vert\ gpsum : Num \to [Num] \to Bool \\ \overline{\Big\vert \; gpsum.n.[]} \doteq ... \\ \Big\vert\ gpsum.n.(x \triangleright xs) \doteq ... \end{array} \] \[\begin{array}{l} \Big\vert\ psum : [Num] \to Bool \\ \overline{\Big\vert \; psum.xs} \doteq gpsum.0.xs \end{array} \]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:
\[\begin{align} f.0 &\doteq \; ? \\ f.(n + 1) &\doteq \; ? \end{align} \]Inducción a lo Fibonacci:
\[\begin{align} fib.0 &\doteq 0 \\ fib.1 &\doteq 1 \\ fib.(n + 2) &\doteq fib.(n + 1) + fib.n \end{align} \]En el caso de la inducción con listas, tenemos:
Inducción básica: (\(sum\), \(prod\), etc.)
\[\begin{align} f.[] &\doteq ? \\ f.(x \triangleright xs) &\doteq ? \end{align} \]Inducción con dos o más elementos: (funciones \(iguales\), \(minimo\) y \(creciente\))
\[\begin{align} f.[] &\doteq ? \\ f.[x] &\doteq ? \\ f.(x \triangleright y \triangleright xs) &\doteq ? \end{align} \]Ejemplo:
\[minimo.xs = \bigl \langle \; \textnormal{Min} \; i : 0 \leq i < \# xs : xs.i \bigr \rangle \]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.
\[Q.xs.ys = \bigl \langle \; \exists bs :: ys = xs \textnormal{⧺} bs \; \bigr \rangle \]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:
\[sum.xs = \bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle \]Aplicamos la especificación de \(sum\) para la lista \([1, 2, 3, 4]\):
\[\begin{array}{ll} \underline{sum}.[1, 2, 3, 4] \\ \\ \equiv \{ \textnormal{ Especificación de } sum \; \} \\ \\ \bigl \langle \; \sum i : \underline{0 \leq i < \# [1, 2, 3, 4]} : [1, 2, 3, 4].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Calculo rango sabiendo } \#xs = 4 \; \} \\ \\ \bigl \langle \; \underline{\sum i : i \in \{0, 1, 2, 3\} : [1, 2, 3, 4].i} \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aplico el término a cada elemento del rango } \} \\ \\ \underline{[1, 2, 3, 4].0} + \underline{[1, 2, 3, 4].1} + \underline{[1, 2, 3, 4].2} + \underline{[1, 2, 3, 4].3} \\ \\ \equiv \{ \textnormal{ Evalúo indexaciones } \} \\ \\ \underline{1 + 2 + 3 + 4} \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ 10 \end{array} \]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):
\[pin8.xs = \bigl \langle \; \exists as, bs : xs = as \textnormal{⧺} bs : prod.as = 8 \; \bigr \rangle \]Primero evaluamos el caso base, \(xs = []\):
\[\begin{array}{ll} \underline{pin8}.[] \\ \\ \equiv \{ \textnormal{ Especificación de } pin8 \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{ [] = as \textnormal{⧺} bs }: prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Propiedad de } \textnormal{⧺} \} \\ \\ \bigl \langle \; \exists as, bs : \underline{as} = [] \land bs = [] : prod.\underline{as} = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Eliminación de variable } as \; \} \\ \\ \bigl \langle \; \exists bs : \underline{bs = []} : prod.[] = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango unitario} \; \} \\ \\ \underline{prod.[]} = 8 \\ \\ \equiv \{ \textnormal{ Definición de } prod \; \} \\ \\ \underline{1 = 8} \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ False \end{array} \]Por lo tanto, \(pin8.[] = False\)
Para el Paso inductivo, seguimos con \(xs = (x \triangleright xs)\):
\[\begin{array}{ll} \underline{pin8}.(x \triangleright xs) \\ \\ \equiv \{ \textnormal{ Especificación de } pin8 \; \} \\ \\ \bigl \langle \; \exists as, bs : (x \triangleright xs) = \underline{as} \textnormal{⧺} bs : prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Tercero excluido de } as \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{(x \triangleright xs) = as \textnormal{⧺} bs \land (as = [] \lor as \neq [])} : prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Distributividad de } \land \; \textnormal{con} \; \lor \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{(x \triangleright xs) = as \textnormal{⧺} bs \land as = [] \lor (x \triangleright xs) = as \textnormal{⧺} bs \land as \neq []} : prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de rango, eliminación de variable } as \; \} \\ \\ \bigl \langle \; \exists bs : (x \triangleright xs) = \underline{[]} \textnormal{⧺} bs : prod.[] = 8 \; \bigr \rangle \\ \lor \\ \bigl \langle \; \exists as, bs : (x \triangleright xs) = \underline{as} \textnormal{⧺} bs : prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \textnormal{⧺}, \textnormal{ Cambio de variable: } as \rightarrow (a \triangleright as) \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{(x \triangleright xs) = bs} : prod.[] = 8 \; \bigr \rangle \\ \lor \\ \bigl \langle \; \exists a, as, bs : \underline{(x \triangleright xs) = (a \triangleright as) \textnormal{⧺} bs} : prod.(a \triangleright as) = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango unitario, Propiedad de las } [] \; \} \\ \\ prod.[] = 8 \; \lor \; \bigl \langle \; \exists a, as, bs : \underline{x = a} \land xs = as \textnormal{⧺} bs : prod.(a \triangleright as) = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Eliminación de una variable } \} \\ \\ prod.[] = 8 \; \lor \; \bigl \langle \; \exists a, as, bs : xs = as \textnormal{⧺} bs : \underline{prod.(x \triangleright as)} = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } prod \; \} \\ \\ prod.[] = 8 \; \lor \; \bigl \langle \; \exists a, as, bs : xs = as \textnormal{⧺} bs : \textcolor{darkred}{x} * as = 8 \; \bigr \rangle \end{array} \]Es necesario generalizar la función \(pin8\) para poder derivarla. Definimos una nueva función \(gpin8\) tal que:
\[gpin8.1.xs = \bigl \langle \; \exists as, bs : xs = as \textnormal{⧺} bs : prod.as = 8 \; \bigr \rangle \] \[gpin8.n.xs = \bigl \langle \; \exists as, bs : xs = as \textnormal{⧺} bs : \textcolor{darkred}{n} * prod.as = 8 \; \bigr \rangle \]Evaluamos el caso base de \(gpin8\):
\[\begin{array}{ll} \underline{gpin8}.n.[] \\ \\ \equiv \{ \textnormal{ Especificación de } gpin8 \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{ [] = as \textnormal{⧺} bs } : n * prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Propiedad de } ⧺ \; \} \\ \\ \bigl \langle \; \exists \underline{as}, bs : \underline{as} = [] \land bs = [] : n * prod.\underline{as} = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Eliminación de variable } as \; \} \\ \\ \bigl \langle \; \exists bs : \underline{[] = bs} : n * prod.[] = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ n * \underline{prod.[]} = 8 \\ \\ \equiv \{ \textnormal{ Definición de } prod \; \} \\ \\ \underline{n * 1} = 8 \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ n = 8 \end{array} \]Seguimos con el paso inductivo de \(gpin8\):
\[\begin{array}{ll} \underline{gpin8}.n.(x \triangleright xs) \\ \\ \equiv \{ \textnormal{ Especificación de } gpin8 \; \} \\ \\ \bigl \langle \; \exists as, bs : (x \triangleright xs) = \underline{as} \textnormal{⧺} bs : n * prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Tercero excluido de } as \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{(x \triangleright xs) = as \textnormal{⧺} bs \land (as = [] \lor as \neq [])} : n * prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Distributividad de } \land \; \textnormal{con} \; \lor \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{(x \triangleright xs) = as \textnormal{⧺} bs \land as = [] \lor (x \triangleright xs) = as \textnormal{⧺} bs \land as \neq []} : n * prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de rango, eliminación de variable } as \; \} \\ \\ \bigl \langle \; \exists bs : (x \triangleright xs) = \underline{[]} \textnormal{⧺} bs : n * prod.[] = 8 \; \bigr \rangle \\ \lor \\ \bigl \langle \; \exists as, bs : (x \triangleright xs) = \underline{as} \textnormal{⧺} bs : n * prod.as = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \textnormal{⧺}, \textnormal{ Cambio de variable: } as \rightarrow (a \triangleright as) \; \} \\ \\ \bigl \langle \; \exists as, bs : \underline{(x \triangleright xs) = bs} : n * prod.[] = 8 \; \bigr \rangle \\ \lor \\ \bigl \langle \; \exists a, as, bs : \underline{(x \triangleright xs) = (a \triangleright as) \textnormal{⧺} bs} : n * prod.(a \triangleright as) = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango unitario, Propiedad de las } [] \; \} \\ \\ n * prod.[] = 8 \; \lor \; \bigl \langle \; \exists \underline{a}, as, bs : \underline{x = a} \land xs = as \textnormal{⧺} bs : n * prod.(\underline{a} \triangleright as) = 8 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Eliminación de variable } a \; \} \\ \\ n * \underline{prod.[]} = 8 \; \lor \; \bigl \langle \; \exists as, bs : xs = as \textnormal{⧺} bs : \underline{n * prod.(x \triangleright as) = 8} \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } prod \; \} \\ \\ \underline{n * 1} = 8 \; \lor \; \underline{\bigl \langle \; \exists as, bs : xs = as \textnormal{⧺} bs : n * x * prod.as = 8 \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Aritmética, hipótesis inductiva con } n = (n * x) \; \} \\ \\ n = 8 \; \lor \; gpin8.(n * x).xs \end{array} \]Los programas son:
\[\begin{array}{l} \Big\vert\ pin8 : [Num] \to Bool \\ \overline{\Big\vert\ pin8.(x \triangleright xs)} \doteq gpin8.1.(x \triangleright xs) \end{array} \] \[\begin{array}{l} \Big\vert\ gpin8 : Num \to [Num] \to Bool \\ \overline{\Big\vert \; gpin8.n.xs} \doteq n = 8 \\ \Big\vert\ gpin8.n.(x \triangleright xs) \doteq n = 8 \; \lor \; gpin8.(n * x).xs \end{array} \]3.
Derivar la función \(minimo\) a partir de la especificación:
\[minimo.xs = \bigl \langle \; \textnormal{Min} \; i : 0 \leq i < \# xs : xs.i \; \bigr \rangle \]Primero evaluamos el caso base, \(xs = []\):
\[\begin{array}{ll} \underline{minimo}.[] \\ \\ \equiv \{ \textnormal{ Especificación de } minimo \; \} \\ \\ \bigl \langle \; \textnormal{Min} \; i : 0 \leq i < \underline{\# []} : [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \; \} \\ \\ \bigl \langle \; \textnormal{Min} \; i : \underline{0 \leq i < 0} : [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ \bigl \langle \; \textnormal{Min} \; i : \underline{False} : [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ +\infty \end{array} \]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]\).
\[\begin{array}{ll} \underline{minimo}.[x] \\ \\ \equiv \{ \textnormal{ Especificación de } minimo \; \} \\ \\ \bigl \langle \; \textnormal{Min} \; i : 0 \leq i < \underline{\# [x]} : [x].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \; \} \\ \\ \bigl \langle \; \textnormal{Min} \; i : \underline{0 \leq i < 1} : [x].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ \bigl \langle \; \textnormal{Min} \; i : \underline{i = 0} : [x].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ \underline{[x].0} \\ \\ \equiv \{ \textnormal{ Definición de } . \; \} \\ \\ x \end{array} \]Ahora seguimos con el paso inductivo \(xs = (x \triangleright y \triangleright xs)\):
\[\begin{array}{ll} \underline{minimo}.(x \triangleright y \triangleright xs) \\ \\ \equiv \{ \textnormal{ Especificación de } minimo \; \} \\ \\ \bigl \langle \; \textnormal{Min} \; i : 0 \leq i < \underline{\# (x \triangleright y \triangleright xs)} : (x \triangleright y \triangleright xs).i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \; \} \\ \\ \underline{ \bigl \langle \; \textnormal{Min} \; i : 0 \leq i < 1 + \# (y \triangleright xs) : (x \triangleright y \triangleright xs).i \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Separación de un término } \} \\ \\ \underline{(x \triangleright y \triangleright xs).0} + \bigl \langle \; \textnormal{Min} \; i : 0 \leq i < \# (y \triangleright xs) : \underline{(x \triangleright y \triangleright xs).(i + 1)} \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } . \; \} \\ \\ x \; \textnormal{min} \; \underline{\bigl \langle \; \textnormal{Min} \; i : 0 \leq i < \# (y \triangleright xs) : (y \triangleright xs).i \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Hipótesis Inductiva con } (y \triangleright xs) \; \} \\ \\ x \; \textnormal{min} \; minimo.(y \triangleright xs) \end{array} \]Nuestro programa final sería:
\[\begin{array}{l} \Big\vert\ minimo : [Num] \to Num \\ \overline{\Big\vert \; minimo.[x] \doteq x} \\ \Big\vert\ minimo.(x \triangleright y \triangleright xs) \doteq x \; \textnormal{min} \; minimo.(y \triangleright xs) \end{array} \]Verificación (PF)
Podemos demostrar que \(\bigl \langle \forall xs :: P.xs \bigr \rangle\)
Cumple con:
\[P.xs : sum.xs = \bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle \]Para lograrlo podemos utilizar inducción matemática o inducción estructural sobre listas (en este caso, la segunda):
Caso base: (\(xs = []\))
Debemos demostrar que:
\[P.[] : sum.[] = \bigl \langle \; \sum i : 0 \leq i < \# [] : [].i \; \bigr \rangle \]Para ello podemos comenzar del lado derecho:
\[\begin{array}{ll} \bigl \langle \; \sum i : 0 \leq i < \underline{\#[]} : [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \; \} \\ \\ \bigl \langle \; \sum i : \underline{0 \leq i < 0} : [].i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ \bigl \langle \; \underline{\sum i : False : [].i} \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ \underline{0} \\ \\ \equiv \{ \textnormal{ Definición de } sum\; \} \\ \\ sum.[] \end{array} \]Por lo tanto, probamos la propiedad \(P.[]\)
Paso inductivo: (\(x \triangleright xs\))
Debemos demostrar que:
\[\begin{array}{ll} P.xs : sum.xs = \bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle \implies \\ \\ P.(x \triangleright xs) : sum.(x \triangleright xs) = \bigl \langle \; \sum i : 0 \leq i < \# (x \triangleright xs) : (x \triangleright xs).i \; \bigr \rangle \end{array} \]Donde \(P.xs\) es la hipótesis inductiva.
Para ello podemos comenzar del lado derecho:
\[\begin{array}{ll} \bigl \langle \; \sum i : 0 \leq i < \underline{ \# (x \triangleright xs) } : (x \triangleright xs).i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } \# \; \} \\ \\ \bigl \langle \; \underline{ \sum i : 0 \leq i < 1 + \# xs : (x \triangleright xs).i } \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Separación de un término } \} \\ \\ \underline{ (x \triangleright xs).0 } + \bigl \langle \; \sum i : 0 \leq i < \# xs : \underline{(x \triangleright xs).(i + 1)} \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Definición de } .\; \} \\ \\ x + \underline{\bigl \langle \; \sum i : 0 \leq i < \# xs : xs.i \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Hipótesis inductiva } \} \\ \\ x + sum.xs \end{array} \]Por lo tanto, probamos la propiedad \(P.(x \triangleright xs)\), y su validez en cualquier lista.
Última vez actualizado el 9 de marzo de 2025