WikiSysop: Texto reemplazado: «isar» por «isabelle»

2018-07-16T15:46:11Z

Texto reemplazado: «isar» por «isabelle»

Jalonso: Protegió «R8» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2014-01-09T11:55:42Z

Protegió «R8» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* R8: Árboles binarios completos } theory R8_Arboles_binarios_completos imports Main begin text { ---------------------------------------...'

2014-01-09T11:55:32Z

Página creada con '<source lang="isar"> header {* R8: Árboles binarios completos *} theory R8_Arboles_binarios_completos imports Main begin text {* ---------------------------------------...'

Página nueva

<source lang="isar">
header {* R8: Árboles binarios completos *}

theory R8_Arboles_binarios_completos
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que no tienen información ni en los nodos y ni en las
hojas. Por ejemplo, el árbol
·
/ \
/ \
· ·
/ \ / \
· · · ·
se representa por "N (N H H) (N H H)".
---------------------------------------------------------------------
*}

datatype arbol = H | N arbol arbol

value "N (N H H) (N H H)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
hojas :: "arbol => nat"
tal que (hojas a) es el número de hojas del árbol a. Por ejemplo,
hojas (N (N H H) (N H H)) = 4
---------------------------------------------------------------------
*}

fun hojas :: "arbol => nat" where
"hojas t = undefined"

value "hojas (N (N H H) (N H H))" -- "= 4"

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
profundidad :: "arbol => nat"
tal que (profundidad a) es la profundidad del árbol a. Por ejemplo,
profundidad (N (N H H) (N H H)) = 2
---------------------------------------------------------------------
*}

fun profundidad :: "arbol => nat" where
"profundidad t = undefined"

value "profundidad (N (N H H) (N H H))" -- "= 2"

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
abc :: "nat ⇒ arbol"
tal que (abc n) es el árbol binario completo de profundidad n. Por
ejemplo,
abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))
---------------------------------------------------------------------
*}

fun abc :: "nat ⇒ arbol" where
"abc 0 = undefined"

value "abc 3" -- "= N (N (N H H) (N H H)) (N (N H H) (N H H))"

text {*
---------------------------------------------------------------------
Ejercicio 6. Un árbol binario a es completo respecto de la medida f si
a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i
como d son árboles binarios completos respecto de f y, además,
f(i) = f(r).

Definir la función
es_abc :: "(arbol => 'a) => arbol => bool
tal que (es_abc f a) se verifica si a es un árbol binario completo
respecto de f.
---------------------------------------------------------------------
*}

fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f t = undefined"

text {*
---------------------------------------------------------------------
Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
size (N (N H H) (N H H)) = 3
---------------------------------------------------------------------
*}

value "size (N (N H H) (N H H))"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H)))"

text {*
---------------------------------------------------------------------
Nota. Tenemos 3 funciones de medida sobre los árboles: número de
hojas, número de nodos y profundidad. A cada una le corresponde un
concepto de completitud. En los siguientes ejercicios demostraremos
que los tres conceptos de completitud son iguales.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de hojas.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que un árbol binario a es completo respecto del
número de hojas syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que si a es un árbolo binario completo
respecto de la profundidad, entonces a es (abc (profundidad a)).
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de
(es_abc size).
---------------------------------------------------------------------
*}

end
</source>

← Revisión anterior		Revisión del 15:46 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R8: Árboles binarios completos *}		header {* R8: Árboles binarios completos *}

← Revisión anterior	Revisión del 11:55 9 ene 2014
(Sin diferencias)

R8 - Historial de revisiones

WikiSysop: Texto reemplazado: «isar» por «isabelle»

Jalonso: Protegió «R8» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* R8: Árboles binarios completos *} theory R8_Arboles_binarios_completos imports Main begin text {* ---------------------------------------...'

Jalonso: Página creada con ' header {* R8: Árboles binarios completos } theory R8_Arboles_binarios_completos imports Main begin text { ---------------------------------------...'