Source: https://www.glc.us.es/~jalonso/vestigium/2020/05/
Timestamp: 2020-08-03 14:15:00+00:00

Document:
mayo, 2020 | Vestigium
José A. Alonso- 28 mayo 2020 -LMF2019
En la segunda parte de la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir en Isabelle/HOL conjuntos y relaciones inductivas y cómo demostrar sus propiedades.
La clase se ha dado mediante videoconferencia y el vídeo correspondiente es
La teoría con los ejemplos presentados en la clase es la siguiente:
José A. Alonso- 27 mayo 2020 -I1M2019
En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de datos de los grafos y dos de sus implementaciones en Haskell: mediante vectores y matrices de adyacencia.
La clase se ha dado mediante videoconferencia los correspondientes vídeos son
El TAD de grafos mediante vectores
El TAD de grafos mediante matricess
Los apuntes correspondientes a la clase es la sección 1 del tema 22
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.
José A. Alonso- 22 mayo 2020 -I1M2019
En la clase de hoy de del curso Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante búsqueda en escalada en espacios de estados.
En primer lugar se explicó la idea de la búsqueda en escalada y cómo, usando dicha idea, se puede transformar el patrón de búsqueda por primero el mejor en el de búsqueda en escalada. Finalmente, se aplicó el patrón de búsqueda en escalada a la resolución del problema del cambio de monedas.
La clase se ha dado mediante videoconferencia y el correspondiente vídeo es
Los apuntes correspondientes a la clase es la sección 3 del tema 23
El código del problema del cambio de monedas usado en la clase es
José A. Alonso- 21 mayo 2020 -LMF2019
En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo desarrollar en Isabelle/HOL teorías axiomáticas usando entornos locales (“locales”) y clases de tipos (“class”). Se ha aplicado al desarrollo de las teorías de grupos y a las de órdenes. videoconferencia.
La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:
José A. Alonso- 20 mayo 2020 -I1M2019
En la clase de hoy de del curso Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante búsqueda informada en espacios de estados.
En primer lugar se estudiaron los algoritmos búsqueda con información (coste, heurística y A*). A continuación se estudió cómo adaptar el patrón de búsqueda ciega a búsqueda informada usando las colas de prioridad. Finalmente, se aplicó el patrón de búsqueda por primero el mejor a la resolución del problema del 8 puzzle.
Algoritmos de búsqueda informada en espacios de estados
El patrón de búsqueda por primero el mejor en Haskell
El código de la primera solución del problema del 8 puzzle usado en la clase es
José A. Alonso- 17 mayo 2020 -LMF2019
Con motivo de la pandemia henos tenido que pasar la docencia al formato no presencial.
En la asignatura de Lógica de 3º de Matemática el cambio ha tenido lugar al principio de la segunda parte del curso en la que se estudia el razonamiento automático con Isabelle/HOL.
Todas las clases no presenciales las he dado por videoconferencia y he subido sus vídeos a YouTube. En este momento hay 12 vídeos correspondientes a las clases no presenciales impartidas:
Deducción natural proposicional con Isabelle/HOL.
Deducción natural en lógica de primer orden con Isabelle/HOL (Parte 1 de 2).
Deducción natural en lógica de primer orden con Isabelle/HOL (Parte 2 de 2).
Programación funcional en Isabelle/HOL.
Razonamiento sobre programas con Isabelle/HOL (Parte 1 de 5).
Razonamiento sobre programas con Isabelle/HOL (Parte 2 de 5).
Razonamiento sobre programas con Isabelle/HOL (Parte 3 de 5).
Razonamiento sobre programas con Isabelle/HOL (Parte 4 de 5).
Razonamiento sobre programas con Isabelle/HOL (Parte 5 de 5).
Razonamiento por casos y por inducción en Isabelle/HOL.
Razonamiento sobre árboles binarios con Isabelle/HOL.
Árboles y bosques: Recursión mutua e inducción con Isabelle/HOL.
José A. Alonso- 17 mayo 2020 -Haskell
Con motivo de la pandemia hemos tenido que pasar la docencia al formato no presencial.
En la asignatura de Informática de 1º de Matemáticas el cambio ha tenido lugar al principio de la segunda parte del curso en el que aplica la programación funcional con Haskell, estudiada en la primera parte, a problemas de algorítmica.
Todas las clases no presenciales las he dado por videoconferencia y he subido sus vídeos a YouTube. En este momento hay 16 vídeos correspondientes a las 9 clases no presenciales impartidas:
Análisis de complejidad de algoritmos.
El TAD de las pilas.
El TAD de las colas.
El TAD de las colas de prioridad.
El TAD de los conjuntos.
Las librerías de conjuntos y de diccionarios.
El TAD de las árboles binarios de búsqueda.
El TAD de los montículos.
El TAD de los polinomios (Parte 1 de 3).
El TAD de los polinomios (Parte 2 de 3).
El TAD de los polimomios (Parte 3 de 3).
La técnica divide y vencerás.
Representación de problemas mediante espacios de estados.
Algoritmos de búsqueda en espacios de estados.
El patrón de búsqueda en espacios de estados.
I1M2019: El patrón de búsqueda en espacios de estados en Haskell
José A. Alonso- 15 mayo 2020 -I1M2019
En la clase de hoy de del curso Informática de 1º del Grado en Matemáticas hemos estudiado cómo programar en Haskell los algoritmos de búsqueda en espacios de estados que vimos en la clase anterior y su aplicación al problema de las N reinas.
Los apuntes correspondientes a la clase son la segunda sección de
LMF2019: Razonamiento sobre árboles y bosques en Isabelle/HOL
José A. Alonso- 14 mayo 2020 -LMF2019
En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.
Primera parte: Razonamiento sobre árboles binarios
Segunda parte: Árboles y bosques: Recursión mutua e inducción
La teoría utilizada es la siguiente
chapter ‹Tema 8: Razonamiento sobre árboles›
theory T8_Razonamiento_sobre_arboles
text ‹En este tema se estudia razonamiento sobre otras estructuras
recursivas como árboles binarios, árboles generales y bosques.
También se muestra cómo definir tipos de datos por recursión cruzada y
la demostración de sus propiedades por inducción.›
section ‹Razonamiento sobre árboles binarios›
text ‹Ejemplo de definición de tipos recursivos:
Definir un tipo de dato para los árboles binarios.›
datatype 'a arbolB = Hoja "'a"
| Nodo "'a" "'a arbolB" "'a arbolB"
text ‹Regla de inducción correspondiente a los árboles binarios:
La regla de inducción sobre árboles binarios es arbolB.induct:
⟦ ⋀x. P (Hoja x);
⋀x i d. ⟦P i; P d⟧ ⟹ P (Nodo x i d)⟧
⟹ P a
thm arbolB.induct
text ‹Ejemplo de definición sobre árboles binarios:
Definir la función "espejo" que aplicada a un árbol devuelve su imagen
especular.›
fun espejo :: "'a arbolB ⇒ 'a arbolB" where
"espejo (Hoja x)     = Hoja x"
| "espejo (Nodo x i d) = Nodo x (espejo d) (espejo i)"
value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) =
Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"
text ‹Ejemplo de demostración sobre árboles binarios:
Demostrar que la función "espejo" es involutiva; es decir, para
cualquier árbol a, se tiene que
espejo (espejo a) = a.›
― ‹La demostración declarativa es›
fixes a :: "'b arbolB"
shows "espejo (espejo a) = a" (is "?P a")
show "?P (Hoja x)"
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (Nodo x i d)"
have "espejo (espejo (Nodo x i d)) =
espejo (Nodo x (espejo d) (espejo i))"
also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))"
also have "… = Nodo x i d"
using h1 h2 by simp
finally show "?P (Nodo x i d)"
― ‹La demostración declarativa detallada es›
by (simp only: espejo.simps(1))
by (simp only: espejo.simps(2))
using h1 h2
by (simp only:)
text ‹Comentarios sobre la demostración anterior:
· (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario
cuyos elementos son de tipo b".
· (induct a) indica que el método de demostración es por inducción
en el árbol binario a.
· Se generan dos casos:
1. ⋀a. espejo (espejo (Hoja a)) = Hoja a
2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2;
espejo (espejo a3) = a3⟧
⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3›
― ‹La demostración aplicativa es›
"espejo (espejo a) = a"
apply (induct a)
― ‹La demostración aplicativa detallada es›
apply (simp only: espejo.simps(1))
apply (simp only: espejo.simps(2))
― ‹La demostración automática es›
by (induct a) simp+
― ‹La demostración automática detallada es›
by (induct a) (simp only: espejo.simps)+
text ‹Ejemplo. [Aplanamiento de árboles]
Definir la función "aplana" que aplane los árboles recorriéndolos en
orden infijo.›
fun aplana :: "'a arbolB ⇒ 'a list" where
"aplana (Hoja x)     = [x]"
| "aplana (Nodo x i d) = aplana i @ [x] @ aplana d"
value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) =
[c, b, d, a, e]"
text ‹Ejemplo. [Aplanamiento de la imagen especular] Demostrar que
aplana (espejo a) = rev (aplana a)›
shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
have "aplana (espejo (Nodo x i d)) =
aplana (Nodo x (espejo d) (espejo i))"
also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))"
also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))"
also have "… = rev ((aplana i) @ [x] @ (aplana d))"
also have "… = rev (aplana (Nodo x i d))"
― ‹Lema auxiliar para la demostración declarativa detallada›
lemma rev_unit: "rev [x] = [x]"
have "rev [x] = rev [] @ [x]"
by (simp only: rev.simps(2))
also have "… = [] @ [x]"
by (simp only: rev.simps(1))
also have "… = [x]"
by (simp only: append.simps(1))
― ‹La demostración estructurada y detallada es›
fix x :: 'b
have "aplana (espejo (Hoja x)) = aplana (Hoja x)"
by (simp only: aplana.simps(1))
also have "… = rev [x]"
by (simp only: rev_unit)
also have "… = rev (aplana (Hoja x))"
finally show "?P (Hoja x)"
by (simp only: aplana.simps(2))
by (simp only: h1 h2)
(* find_theorems "rev (_ @ _)" *)
by (simp only: rev_append rev_unit append_assoc)
lemma "aplana (espejo a) = rev (aplana a)"
apply (simp only: espejo.simps(1) aplana.simps(1))
apply (simp only: rev_unit)
apply (simp only: espejo.simps(2) aplana.simps(2))
apply (simp only: rev_append)
apply (simp only: append_assoc)
― ‹La demostración aplicativa detallada compacta es›
apply (simp only:
espejo.simps(1)
aplana.simps(1)
espejo.simps(2)
aplana.simps(2)
rev_append
append_assoc)+
― ‹La demostración aplicativa detallada más compacta es›
espejo.simps
aplana.simps
by (induct a) simp_all
by (induct a)
(simp only:
section ‹Árboles y bosques. 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 = Nodo "'a" "'a bosque"
and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"
text ‹Regla de inducción correspondiente a la recursión cruzada:
La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
⟦⋀x b. P2 b ⟹ P1 (Nodo x b);
P2 Vacio;
⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧
⟹ P1 a ∧ P2 b›
thm arbol_bosque.induct
text ‹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 f a) es el árbol obtenido aplicando la función f a
todos los nodos del árbol a.
· (map_bosque f b) es el bosque obtenido aplicando la función f a
todos los nodos del bosque b. ›
fun aplana_arbol :: "'a arbol ⇒ 'a list" and
aplana_bosque :: "'a bosque ⇒ 'a list" where
"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 ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and
map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where
"map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)"
| "map_bosque f Vacio       = Vacio"
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"
text ‹Ejemplo de demostración por inducción cruzada:
· aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
· aplana_bosque (map_bosque f b) = map f (aplana_bosque b)›
declare [[names_short]]
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
fix x b
assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
have "aplana_arbol (map_arbol f (Nodo x b)) =
aplana_arbol (Nodo (f x) (map_bosque f b))"
also have "… = (f x) # (aplana_bosque (map_bosque f b))"
also have "… = (f x) # (map f (aplana_bosque b))"
using HI by simp
also have "… = map f (aplana_arbol (Nodo x b))"
finally show "aplana_arbol (map_arbol f (Nodo x b)) =
map f (aplana_arbol (Nodo x b))"
show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)"
assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
have "aplana_bosque (map_bosque f (ConsB a b)) =
aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp
also have "… = aplana_arbol (map_arbol f a) @
aplana_bosque (map_bosque f b)"
also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))"
using HI1 HI2 by simp
also have "… = map f (aplana_bosque (ConsB a b))" by simp
finally show "aplana_bosque (map_bosque f (ConsB a b)) =
map f (aplana_bosque (ConsB a b))"
by (simp only: map_arbol.simps(1))
by (simp only: aplana_arbol.simps(1))
using HI
(* find_theorems "map _ (_ # _)" *)
by (simp only: list.map aplana_arbol.simps(1))
by (simp only: aplana_bosque.simps(1)
map_bosque.simps(1)
list.map)
aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))"
by (simp only: map_bosque.simps(2))
by (simp only: aplana_bosque.simps(2))
by (simp only: HI1 HI2)
also have "… = map f (aplana_arbol a @ aplana_bosque b)"
(* find_theorems "map _ (_ @ _)" *)
by (simp only: map_append)
also have "… = map f (aplana_bosque (ConsB a b))"
· (induct_tac a and b) indica que el método de demostración es por
inducción cruzada sobre a y b.
· Se generan 3 casos:
1. ⋀a bosque.
aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹
aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =
map h (aplana_arbol (arbol.Nodo a bosque))
2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
3. ⋀arbol bosque.
⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);
aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧
⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
map h (aplana_bosque (ConsB arbol bosque))›
apply (induct_tac a and b)
apply (simp only: map_arbol.simps aplana_arbol.simps)
apply (simp only: list.map(2))
apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1))
apply (simp only: list.map(1))
apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2))
apply (simp only: map_append)
map_arbol.simps
aplana_arbol.simps
list.map(2)
aplana_bosque.simps(1)
list.map(1)
map_bosque.simps(2)
aplana_bosque.simps(2)
map_append)+
map_bosque.simps
aplana_bosque.simps
by (induct_tac a and b) simp+
by (induct_tac a and b)
chapter ‹Tema 8: Razonamiento sobre árboles› theory T8_Razonamiento_sobre_arboles imports Main begin text ‹En este tema se estudia razonamiento sobre otras estructuras recursivas como árboles binarios, árboles generales y bosques. También se muestra cómo definir tipos de datos por recursión cruzada y la demostración de sus propiedades por inducción.› section ‹Razonamiento sobre árboles binarios› text ‹Ejemplo de definición de tipos recursivos: Definir un tipo de dato para los árboles binarios.› datatype 'a arbolB = Hoja "'a" | Nodo "'a" "'a arbolB" "'a arbolB" text ‹Regla de inducción correspondiente a los árboles binarios: La regla de inducción sobre árboles binarios es arbolB.induct: ⟦ ⋀x. P (Hoja x); ⋀x i d. ⟦P i; P d⟧ ⟹ P (Nodo x i d)⟧ ⟹ P a › thm arbolB.induct text ‹Ejemplo de definición sobre árboles binarios: Definir la función "espejo" que aplicada a un árbol devuelve su imagen especular.› fun espejo :: "'a arbolB ⇒ 'a arbolB" where "espejo (Hoja x) = Hoja x" | "espejo (Nodo x i d) = Nodo x (espejo d) (espejo i)" value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))" text ‹Ejemplo de demostración sobre árboles binarios: Demostrar que la función "espejo" es involutiva; es decir, para cualquier árbol a, se tiene que espejo (espejo a) = a.› ― ‹La demostración declarativa es› lemma fixes a :: "'b arbolB" shows "espejo (espejo a) = a" (is "?P a") proof (induct a) fix x show "?P (Hoja x)" by simp next fix x fix i assume h1: "?P i" fix d assume h2: "?P d" show "?P (Nodo x i d)" proof - have "espejo (espejo (Nodo x i d)) = espejo (Nodo x (espejo d) (espejo i))" by simp also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" by simp also have "… = Nodo x i d" using h1 h2 by simp finally show "?P (Nodo x i d)" by this qed qed ― ‹La demostración declarativa detallada es› lemma fixes a :: "'b arbolB" shows "espejo (espejo a) = a" (is "?P a") proof (induct a) fix x show "?P (Hoja x)" by (simp only: espejo.simps(1)) next fix x fix i assume h1: "?P i" fix d assume h2: "?P d" show "?P (Nodo x i d)" proof - have "espejo (espejo (Nodo x i d)) = espejo (Nodo x (espejo d) (espejo i))" by (simp only: espejo.simps(2)) also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" by (simp only: espejo.simps(2)) also have "… = Nodo x i d" using h1 h2 by (simp only:) finally show ?thesis by this qed qed text ‹Comentarios sobre la demostración anterior: · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario cuyos elementos son de tipo b". · (induct a) indica que el método de demostración es por inducción en el árbol binario a. · Se generan dos casos: 1. ⋀a. espejo (espejo (Hoja a)) = Hoja a 2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; espejo (espejo a3) = a3⟧ ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3› ― ‹La demostración aplicativa es› lemma "espejo (espejo a) = a" apply (induct a) apply simp apply simp done ― ‹La demostración aplicativa detallada es› lemma "espejo (espejo a) = a" apply (induct a) apply (simp only: espejo.simps(1)) apply (simp only: espejo.simps(2)) done ― ‹La demostración automática es› lemma "espejo (espejo a) = a" by (induct a) simp+ ― ‹La demostración automática detallada es› lemma "espejo (espejo a) = a" by (induct a) (simp only: espejo.simps)+ text ‹Ejemplo. [Aplanamiento de árboles] Definir la función "aplana" que aplane los árboles recorriéndolos en orden infijo.› fun aplana :: "'a arbolB ⇒ 'a list" where "aplana (Hoja x) = [x]" | "aplana (Nodo x i d) = aplana i @ [x] @ aplana d" value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = [c, b, d, a, e]" text ‹Ejemplo. [Aplanamiento de la imagen especular] Demostrar que aplana (espejo a) = rev (aplana a)› ― ‹La demostración declarativa es› lemma fixes a :: "'b arbolB" shows "aplana (espejo a) = rev (aplana a)" (is "?P a") proof (induct a) fix x show "?P (Hoja x)" by simp next fix x fix i assume h1: "?P i" fix d assume h2: "?P d" show "?P (Nodo x i d)" proof - have "aplana (espejo (Nodo x i d)) = aplana (Nodo x (espejo d) (espejo i))" by simp also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" by simp also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" using h1 h2 by simp also have "… = rev ((aplana i) @ [x] @ (aplana d))" by simp also have "… = rev (aplana (Nodo x i d))" by simp finally show "?P (Nodo x i d)" by this qed qed ― ‹Lema auxiliar para la demostración declarativa detallada› lemma rev_unit: "rev [x] = [x]" proof - have "rev [x] = rev [] @ [x]" by (simp only: rev.simps(2)) also have "… = [] @ [x]" by (simp only: rev.simps(1)) also have "… = [x]" by (simp only: append.simps(1)) finally show ?thesis by this qed ― ‹La demostración estructurada y detallada es› lemma fixes a :: "'b arbolB" shows "aplana (espejo a) = rev (aplana a)" (is "?P a") proof (induct a) fix x :: 'b have "aplana (espejo (Hoja x)) = aplana (Hoja x)" by (simp only: espejo.simps(1)) also have "… = [x]" by (simp only: aplana.simps(1)) also have "… = rev [x]" by (simp only: rev_unit) also have "… = rev (aplana (Hoja x))" by (simp only: aplana.simps(1)) finally show "?P (Hoja x)" by this next fix x :: 'b fix i assume h1: "?P i" fix d assume h2: "?P d" show "?P (Nodo x i d)" proof - have "aplana (espejo (Nodo x i d)) = aplana (Nodo x (espejo d) (espejo i))" by (simp only: espejo.simps(2)) also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" by (simp only: aplana.simps(2)) also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" by (simp only: h1 h2) also have "… = rev ((aplana i) @ [x] @ (aplana d))" (* find_theorems "rev (_ @ _)" *) by (simp only: rev_append rev_unit append_assoc) also have "… = rev (aplana (Nodo x i d))" by (simp only: aplana.simps(2)) finally show ?thesis by this qed qed ― ‹La demostración aplicativa es› lemma "aplana (espejo a) = rev (aplana a)" apply (induct a) apply simp apply simp done ― ‹La demostración aplicativa detallada es› lemma "aplana (espejo a) = rev (aplana a)" apply (induct a) apply (simp only: espejo.simps(1) aplana.simps(1)) apply (simp only: rev_unit) apply (simp only: espejo.simps(2) aplana.simps(2)) apply (simp only: rev_append) apply (simp only: rev_unit) apply (simp only: append_assoc) done ― ‹La demostración aplicativa detallada compacta es› lemma "aplana (espejo a) = rev (aplana a)" apply (induct a) apply (simp only: espejo.simps(1) aplana.simps(1) rev_unit espejo.simps(2) aplana.simps(2) rev_append append_assoc)+ done ― ‹La demostración aplicativa detallada más compacta es› lemma "aplana (espejo a) = rev (aplana a)" apply (induct a) apply (simp only: espejo.simps aplana.simps rev_unit rev_append append_assoc)+ done ― ‹La demostración automática es› lemma "aplana (espejo a) = rev (aplana a)" by (induct a) simp_all ― ‹La demostración automática detallada es› lemma "aplana (espejo a) = rev (aplana a)" by (induct a) (simp only: espejo.simps aplana.simps rev_unit rev_append append_assoc)+ section ‹Árboles y bosques. 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 = Nodo "'a" "'a bosque" and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque" text ‹Regla de inducción correspondiente a la recursión cruzada: La regla de inducción sobre árboles y bosques es arbol_bosque.induct: ⟦⋀x b. P2 b ⟹ P1 (Nodo x b); P2 Vacio; ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ ⟹ P1 a ∧ P2 b› thm arbol_bosque.induct text ‹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 f a) es el árbol obtenido aplicando la función f a todos los nodos del árbol a. · (map_bosque f b) es el bosque obtenido aplicando la función f a todos los nodos del bosque b. › fun aplana_arbol :: "'a arbol ⇒ 'a list" and aplana_bosque :: "'a bosque ⇒ 'a list" where "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 ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where "map_arbol f (Nodo x b) = Nodo (f x) (map_bosque f b)" | "map_bosque f Vacio = Vacio" | "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)" text ‹Ejemplo de demostración por inducción cruzada: Demostrar que: · aplana_arbol (map_arbol f a) = map f (aplana_arbol a) · aplana_bosque (map_bosque f b) = map f (aplana_bosque b)› declare [[names_short]] ― ‹La demostración declarativa es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" proof (induct_tac a and b) fix x b assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" have "aplana_arbol (map_arbol f (Nodo x b)) = aplana_arbol (Nodo (f x) (map_bosque f b))" by simp also have "… = (f x) # (aplana_bosque (map_bosque f b))" by simp also have "… = (f x) # (map f (aplana_bosque b))" using HI by simp also have "… = map f (aplana_arbol (Nodo x b))" by simp finally show "aplana_arbol (map_arbol f (Nodo x b)) = map f (aplana_arbol (Nodo x b))" by this next show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" by simp next fix a b assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)" and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" have "aplana_bosque (map_bosque f (ConsB a b)) = aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp also have "… = aplana_arbol (map_arbol f a) @ aplana_bosque (map_bosque f b)" by simp also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" using HI1 HI2 by simp also have "… = map f (aplana_bosque (ConsB a b))" by simp finally show "aplana_bosque (map_bosque f (ConsB a b)) = map f (aplana_bosque (ConsB a b))" by this qed ― ‹La demostración declarativa detallada es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" proof (induct_tac a and b) fix x b assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" have "aplana_arbol (map_arbol f (Nodo x b)) = aplana_arbol (Nodo (f x) (map_bosque f b))" by (simp only: map_arbol.simps(1)) also have "… = (f x) # (aplana_bosque (map_bosque f b))" by (simp only: aplana_arbol.simps(1)) also have "… = (f x) # (map f (aplana_bosque b))" using HI by (simp only:) also have "… = map f (aplana_arbol (Nodo x b))" (* find_theorems "map _ (_ # _)" *) by (simp only: list.map aplana_arbol.simps(1)) finally show "aplana_arbol (map_arbol f (Nodo x b)) = map f (aplana_arbol (Nodo x b))" by this next show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" by (simp only: aplana_bosque.simps(1) map_bosque.simps(1) list.map) next fix a b assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)" and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" have "aplana_bosque (map_bosque f (ConsB a b)) = aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by (simp only: map_bosque.simps(2)) also have "… = aplana_arbol (map_arbol f a) @ aplana_bosque (map_bosque f b)" by (simp only: aplana_bosque.simps(2)) also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" by (simp only: HI1 HI2) also have "… = map f (aplana_arbol a @ aplana_bosque b)" (* find_theorems "map _ (_ @ _)" *) by (simp only: map_append) also have "… = map f (aplana_bosque (ConsB a b))" by (simp only: aplana_bosque.simps(2)) finally show "aplana_bosque (map_bosque f (ConsB a b)) = map f (aplana_bosque (ConsB a b))" by this qed text ‹Comentarios sobre la demostración anterior: · (induct_tac a and b) indica que el método de demostración es por inducción cruzada sobre a y b. · Se generan 3 casos: 1. ⋀a bosque. aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹ aplana_arbol (map_arbol (arbol.Nodo a bosque) h) = map h (aplana_arbol (arbol.Nodo a bosque)) 2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio) 3. ⋀arbol bosque. ⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol); aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧ ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) = map h (aplana_bosque (ConsB arbol bosque))› ― ‹La demostración aplicativa es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" apply (induct_tac a and b) apply simp+ done ― ‹La demostración aplicativa detallada es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" apply (induct_tac a and b) apply (simp only: map_arbol.simps aplana_arbol.simps) apply (simp only: list.map(2)) apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1)) apply (simp only: list.map(1)) apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2)) apply (simp only: map_append) done ― ‹La demostración aplicativa detallada compacta es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" apply (induct_tac a and b) apply (simp only: map_arbol.simps aplana_arbol.simps list.map(2) map_bosque.simps(1) aplana_bosque.simps(1) list.map(1) map_bosque.simps(2) aplana_bosque.simps(2) map_append)+ done ― ‹La demostración aplicativa detallada más compacta es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" apply (induct_tac a and b) apply (simp only: map_arbol.simps map_bosque.simps aplana_arbol.simps aplana_bosque.simps list.map map_append)+ done ― ‹La demostración automática es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" by (induct_tac a and b) simp+ ― ‹La demostración automática detallada es› lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" by (induct_tac a and b) (simp only: map_arbol.simps map_bosque.simps aplana_arbol.simps aplana_bosque.simps list.map map_append)+ end
I1M2019: Resolución de problemas mediante búsqueda en espacios de estados
José A. Alonso- 13 mayo 2020 -I1M2019
En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante búsqueda en espacios de estados.
En primer lugar se ha visto cómo se describen los problemas mediante el estado inicial, los sucesores de los estados y los estados finales. Aplicándola a los problemas del 8-puzzle, del granjero, de las jarras y del viaje.
A continuación se han explicado los procedimientos básicos de búsquedas: en anchura, en profundidad, en profundidad acotada y en profundidad iterativa.
La clase se ha dado mediante videoconferencia y los correspondientes vídeos son
Representación de problemas mediante espacios de estados:
Algoritmos de búsqueda en espacios de estados:
Los apuntes correspondientes son las 53 primeras transparencias del tema 23a.
Resumen de lecturas compartidas durante julio de 2020
Resumen de lecturas compartidas durante junio de 2020
Resumen de lecturas compartidas durante mayo de 2020
Archivos Elegir mes agosto 2020 (1) julio 2020 (1) junio 2020 (1) mayo 2020 (14) abril 2020 (12) marzo 2020 (16) febrero 2020 (26) enero 2020 (15) diciembre 2019 (15) noviembre 2019 (20) octubre 2019 (17) septiembre 2019 (5) agosto 2019 (1) julio 2019 (1) junio 2019 (5) mayo 2019 (16) abril 2019 (16) marzo 2019 (27) febrero 2019 (19) enero 2019 (13) diciembre 2018 (11) noviembre 2018 (16) octubre 2018 (19) septiembre 2018 (10) agosto 2018 (1) julio 2018 (4) junio 2018 (1) mayo 2018 (1) abril 2018 (13) marzo 2018 (25) febrero 2018 (21) enero 2018 (1) diciembre 2017 (12) noviembre 2017 (17) octubre 2017 (13) septiembre 2017 (7) julio 2017 (1) mayo 2017 (1) febrero 2017 (17) enero 2017 (3) diciembre 2016 (13) noviembre 2016 (19) octubre 2016 (14) septiembre 2016 (7) agosto 2016 (5) julio 2016 (5) mayo 2016 (12) abril 2016 (13) marzo 2016 (20) febrero 2016 (15) enero 2016 (10) diciembre 2015 (14) noviembre 2015 (16) octubre 2015 (20) septiembre 2015 (22) agosto 2015 (17) julio 2015 (3) junio 2015 (4) mayo 2015 (10) abril 2015 (14) marzo 2015 (15) febrero 2015 (17) enero 2015 (19) diciembre 2014 (25) noviembre 2014 (25) octubre 2014 (20) septiembre 2014 (15) julio 2014 (12) junio 2014 (5) mayo 2014 (10) abril 2014 (16) marzo 2014 (18) febrero 2014 (24) enero 2014 (25) diciembre 2013 (33) noviembre 2013 (26) octubre 2013 (29) septiembre 2013 (24) agosto 2013 (16) julio 2013 (12) junio 2013 (15) mayo 2013 (36) abril 2013 (45) marzo 2013 (23) febrero 2013 (18) enero 2013 (14) diciembre 2012 (21) noviembre 2012 (26) octubre 2012 (27) septiembre 2012 (13) agosto 2012 (19) julio 2012 (4) junio 2012 (4) mayo 2012 (5) abril 2012 (12) marzo 2012 (28) febrero 2012 (20) enero 2012 (14) diciembre 2011 (20) noviembre 2011 (29) octubre 2011 (17) septiembre 2011 (10) agosto 2011 (11) julio 2011 (10) junio 2011 (7) mayo 2011 (15) abril 2011 (16) marzo 2011 (19) febrero 2011 (22) enero 2011 (14) diciembre 2010 (19) noviembre 2010 (26) octubre 2010 (18) septiembre 2010 (22) agosto 2010 (25) julio 2010 (2) marzo 2010 (3) febrero 2010 (16) enero 2010 (26)

References: resolución 
 resolución 
 resolución 
 resolución 
 Resolución 
 resolución