header {* Tema 10: Heurísticas para la inducción y recursión general *}
theory Tema_10
imports Main Tema_7 Efficient_Nat
begin
section {* Heurísticas para la inducción *}
text {*
Definición. [Definición recursiva de inversa]
(inversa xs) la inversa de la lista xs. Por ejemplo,
inversa [2,5,3] = [3,5,2]
*}
primrec inversa :: "'a list ⇒ 'a list" where
"inversa [] = []" |
"inversa (x#xs) = (inversa xs) @ [x]"
value "inversa [2::nat,5,3]"
text {*
Definición. [Definición de inversa con acumuladores]
(inversaAc xs) es la inversa de la lista xs calculada con
acumuladores. Por ejemplo,
inversaAc [2,5,3] = [3,5,2]
inversaAcAux [2,5,3] [] = [3,5,2]
*}
primrec inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys" |
"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"
definition inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs ≡ inversaAcAux xs []"
value "inversaAcAux [2::nat,5,3] []"
value "inversaAc [2::nat,5,3]"
text {*
Lema. [Ejemplo de equivalencia entre las definiciones]
La inversa de [1,2,3] es lo mismo calculada con la primera definición que
con la segunda.
*}
lemma "inversaAc [1,2,3] = inversa [1,2,3]"
by (simp add: inversaAc_def)
text {*
Nota. [Ejemplo fallido de demostración por inducción]
El siguiente intento de demostrar que para cualquier lista xs, se tiene que
"inversaAc xs = inversa xs" falla.
*}
lemma "inversaAc xs = inversa xs"
proof (induct xs)
show "inversaAc [] = inversa []" by (simp add: inversaAc_def)
next
fix a xs assume HI: "inversaAc xs = inversa xs"
have "inversaAc (a#xs) = inversaAcAux (a#xs) []" by (simp add: inversaAc_def)
also have "… = inversaAcAux xs [a]" by simp
also have "… = inversa (a#xs)"
-- "Problema: la hipótesis de inducción no es aplicable."
oops
text {*
Nota. [Heurística de generalización]
Cuando se use demostración estructural, cuantificar universalmente las
variables libres (o, equivalentemente, considerar las variables libres como
variables arbitrarias).
Lema. [Lema con generalización]
Para toda lista ys se tiene
inversaAcAux xs ys = (inversa xs) @ ys
*}
lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs)@ys"
proof (induct xs arbitrary: ys)
show "⋀ys. inversaAcAux [] ys = (inversa [])@ys" by simp
next
fix a xs
assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
proof -
fix ys
have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp
also have "… = inversa xs@(a#ys)" using HI by simp
also have "… = inversa (a#xs)@ys" by simp
finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp
qed
qed
text {*
Corolario. Para cualquier lista xs, se tiene que
inversaAc xs = inversa xs
*}
corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa inversaAc_def)
text {*
Nota. En el paso "inversa xs@(a#ys) = inversa (a#xs)@ys" se usan
lemas de la teoría List. Se puede observar, activando "Trace
Simplifier" y D"|Trace Rules", que los lemas usados son
· append_assoc: (xs @ ys) @ zs = xs @ (ys @ zs)
· append.append_Cons: (x#xs)@ys = x#(xs@ys)
· append.append_Nil: []@ys = ys
Los dos últimos son las ecuaciones de la definición de append.
En la siguiente demostración se detallan los lemas utilizados.
*}
lemma "(inversa xs)@(a#ys) = (inversa (a#xs))@ys"
proof -
have "(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))"
by (simp only:append.append_Nil)
also have "… = (inversa xs)@([a]@ys)" by (simp only:append.append_Cons)
also have "… = ((inversa xs)@[a])@ys" by (simp only:append_assoc)
also have "… = (inversa (a#xs))@ys" by (simp only:inversa.simps(2))
finally show ?thesis .
qed
section {* Recursión general. La función de Ackermann *}
text {*
El objetivo de esta sección es mostrar el uso de las definiciones
recursivas generales y sus esquemas de inducción. Como ejemplo se usa la
función de Ackermann (se puede consultar información sobre dicha función en
http://en.wikipedia.org/wiki/Ackermann_function).
Definición. La función de Ackermann se define por
A(m,n) = n+1, si m=0,
A(m-1,1) si m>0 y n=0,
A(m-1,A(m,n-1)), si m>0 y n>0
para todo los números naturales.
La función de Ackermann es recursiva, pero no es primitiva recursiva.
*}
fun ack :: "nat ⇒ nat ⇒ nat" where
"ack 0 n = n+1" |
"ack (Suc m) 0 = ack m 1" |
"ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"
text {*
Nota. [Ejemplo de cálculo]
El cálculo del valor de la función de Ackermann para 2 y 3 se realiza
mediante "value"
*}
value "ack 2 3" (* devuelve 9 *)
text {*
Nota. [Definiciones recursivas generales]
· Las definiciones recursivas generales se identifican mediante "fun".
· Al definir una función recursiva general se genera una regla de
inducción. En la definición anterior, la regla generada es
ack.induct:
⟦⋀n. P 0 n;
⋀m. P m 1 ⟹ P (Suc m) 0;
⋀m n. ⟦P (Suc m) n; P m (ack (Suc m) n)⟧ ⟹ P (Suc m) (Suc n)⟧
⟹ P a b
Lema. Para todos m y n, A(m,n) > n.
*}
lemma "ack m n > n"
proof (induct m n rule: ack.induct)
fix n :: "nat"
show "ack 0 n > n" by simp
next
fix m assume "ack m 1 > 1"
thus "ack (Suc m) 0 > 0" by simp
next
fix m n
assume "n < ack (Suc m) n" and
"ack (Suc m) n < ack m (ack (Suc m) n)"
thus "Suc n < ack (Suc m) (Suc n)" by simp
qed
text {*
El lema anterior se puede demostrar automáticamente, como sigue.
*}
lemma "ack m n > n"
by (induct m n rule: ack.induct) simp_all
text {*
Nota. [Inducción sobre recursión]
El formato para iniciar una demostración por inducción en la regla inductiva
correspondiente a la definición recursiva de la función f m n es
proof (induct m n rule:f.induct)
*}
section {* Recursión mutua e inducción *}
text {*
Nota. [Ejemplo de definición de tipos mediante recursión cruzada]
· Un árbol de tipo a es una hoja o un nodo de tipo a junto con un
bosque de tipo a.
· Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo
un árbol de tipo a a un bosque de tipo a.
*}
datatype 'a arbol = Hoja | Nodo "'a" "'a bosque"
and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"
text {*
Nota. [Regla de inducción correspondiente a la recursión cruzada]
La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
⟦P1 Hoja;
⋀x b. P2 b ⟹ P1 (Nodo x b);
P2 Vacio;
⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧
⟹ P1 a ∧ P2 b
Nota. [Ejemplos de definición por recursión cruzada]
· aplana_arbol a) es la lista obtenida aplanando el árbol a.
· (aplana_bosque b) es la lista obtenida aplanando el bosque b.
· (map_arbol a h) es el árbol obtenido aplicando la función h a
todos los nodos del árbol a.
· (map_bosque b h) es el bosque obtenido aplicando la función h a
todos los nodos del bosque b.
*}
fun
aplana_arbol :: "'a arbol ⇒ 'a list" and
aplana_bosque :: "'a bosque ⇒ 'a list" where
"aplana_arbol Hoja = []"
| "aplana_arbol (Nodo x b) = x#(aplana_bosque b)"
| "aplana_bosque Vacio = []"
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"
fun
map_arbol :: "'a arbol ⇒ ('a ⇒ 'b) ⇒ 'b arbol" and
map_bosque :: "'a bosque ⇒ ('a ⇒ 'b) ⇒ 'b bosque" where
"map_arbol Hoja h = Hoja"
| "map_arbol (Nodo x b) h = Nodo (h x) (map_bosque b h)"
| "map_bosque Vacio h = Vacio"
| "map_bosque (ConsB a b) h = ConsB (map_arbol a h) (map_bosque b h)"
text {*
Lema. [Ejemplo de inducción cruzada]
· aplana_arbol (map_arbol a h) = map h (aplana_arbol a)
· aplana_bosque (map_bosque b h) = map h (aplana_bosque b)
*}
lemma "aplana_arbol (map_arbol a h) = map h (aplana_arbol a)
∧ aplana_bosque (map_bosque b h) = map h (aplana_bosque b)"
proof (induct_tac a and b)
show "aplana_arbol (map_arbol Hoja h) = map h (aplana_arbol Hoja)" by simp
next
fix x b
assume HI: "aplana_bosque (map_bosque b h) = map h (aplana_bosque b)"
have "aplana_arbol (map_arbol (Nodo x b) h)
= aplana_arbol (Nodo (h x) (map_bosque b h))" by simp
also have "… = (h x)#(aplana_bosque (map_bosque b h))" by simp
also have "… = (h x)#(map h (aplana_bosque b))" using HI by simp
also have "… = map h (aplana_arbol (Nodo x b))" by simp
finally show "aplana_arbol (map_arbol (Nodo x b) h)
= map h (aplana_arbol (Nodo x b))" .
next
show "aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)" by simp
next
fix a b
assume HI1: "aplana_arbol (map_arbol a h) = map h (aplana_arbol a)"
and HI2: "aplana_bosque (map_bosque b h) = map h (aplana_bosque b)"
have "aplana_bosque (map_bosque (ConsB a b) h)
= aplana_bosque (ConsB (map_arbol a h) (map_bosque b h))" by simp
also have "… = aplana_arbol(map_arbol a h)@aplana_bosque(map_bosque b h)"
by simp
also have "… = (map h (aplana_arbol a))@(map h (aplana_bosque b))"
using HI1 HI2 by simp
also have "… = map h (aplana_bosque (ConsB a b))" by simp
finally show "aplana_bosque (map_bosque (ConsB a b) h)
= map h (aplana_bosque (ConsB a b))" by simp
qed
lemma "aplana_arbol (map_arbol a h) = map h (aplana_arbol a)
∧ aplana_bosque (map_bosque b h) = map h (aplana_bosque b)"
by (induct_tac a and b) auto
end