Apuntes de Funcional (Algoritmos I)

De Cuba-Wiki
Saltar a: navegación, buscar
Back.png Volver a la página de la materia

Reglas de terminacion[editar]

R1: Sea i entre 1 y n, y sea g y (g puede ser f) una expresión que aparece en Gi o en Ei. Si:

  • x hace verdadero Pf ,
  • valen ¬B1, . . . ,¬Bi−1,
  • si g y aparece en Ei vale además Bi,

entonces y debe hacer verdadero Pg.

Lo que esta regla expresa es que, toda vez que una función auxiliar (g y) va a ser evaluada (ya sea en una guarda, siendo todas las anteriores falsas, o en el lado derecho de la ecuación, en cuyo caso pedimos además que la guarda correspondiente sea verdadera), lo será dentro de su precondición.

R2: Si x están definidas y hacen verdadero Pf , entonces existe un i entre 1 y n tal que x hacen verdadero Bi. Con esta regla nunca puede suceder que no se encuentre una ecuación apropiada para la entrada.

Sea f una función definida por las ecuaciones:

Sean además Pf una precondición de f tal que se verifican R1 y R2, y Fv(x) una función variante. Para asegurar que f termina, basta verificar que:

R3: Si x están bien definidas y hacen verdadero Pf , entonces Fv(x) no es bottom.

R4: Sea i entre 1 y n, con Ei un caso recursivo, y x tales que se cumple (Pf ^ ¬B1 ^ . . . ^ ¬Bi−1 ^ Bi). Entonces, para cada aparición de fy en Ei, vale que Fv(x) > Fv(y).

R5: Existe una constante entera k, que denominaremos cota de Fv, con la siguiente propiedad:

Toda vez que x hace verdadero Pf y Fv(x) <= k, debe existir i entre 1 y n tal que Ei es un caso base, y vale (Pf ^ ¬B1 ^ . . . ^ ¬Bi−1 ^ Bi).

Analicemos lo que nos dicen estas reglas:

  • R3 pide simplemente que tenga sentido evaluar Fv(x)cuando vale la precondición.
  • R4 pide que Fv sea decreciente: esto es, que cada vez que se entre en un paso recursivo, el valor de la función variante aplicado a los argumentos del paso recursivo sea estrictamente menor que el valor de los argumentos en dicha evaluación.
  • Por último, R5 pide que Fv sea acotada, o sea, que exista una cota para el valor que puede tomar Fv(x) sin llegar al caso base. Si en algún momento Fv(x) corresponde a un valor por debajo de la cota, necesariamente tenemos que estar en un caso base.



Guardas[editar]

Cuando la forma de calcular el resultado depende de alg´un predicado (con respecto a los par´ametros), solemos usar guardas...

nombreFuncion :: Param1 -> Param2 -> ... -> ParamN -> Resultado

nombreFuncion p1 p2 ... pN |(p1 > p2) = ... |(p1 <= p2)= ...

Se analizan de arriba hacia abajo y cuando una de las condiciones se satisface, se determina qu´e ecuaci´on debe utilizarse. Si no hay guarda que se haga verdadera, la expresi´on que se trata de evaluar se indefine.