header {* R22: Diagramas de decisión binarios *}
theory R22
imports Main
begin
text {*
Las funciones booleanas se pueden representar mediante diagramas de
decisión binarios (DDB). Por ejemplo, la función f definida por la
tabla de la izquierda se representa por el DDB de la derecha
+---+---+---+----------+ p
| p | q | r | f(p,q,r) | / \
+---+---+---+----------+ / \
| F | F | * | V | q q
| F | V | * | F | / \ / \
| V | F | * | F | V F F r
| V | V | F | F | / \
| V | V | V | V | F V
+---+---+---+----------+
Para cada variable, si su valor es falso se evalúa su hijo izquierdo y
si es verdadero se evalúa su hijo derecho.
*}
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos ddb para representar los
diagramas de decisión binarios. Por ejemplo, el DDB anterior se
representa por
N (N (H True) (H False)) (N (H False) (N (H False) (H True)))
---------------------------------------------------------------------
*}
datatype ddb = H bool | N ddb ddb
value "N (N (H True) (H False)) (N (H False) (N (H False) (H True)))"
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir ddb1 para representar el DDB del ejercicio 1.
---------------------------------------------------------------------
*}
abbreviation ddb1 :: ddb where
"ddb1 ≡ N (N (H True) (H False)) (N (H False) (N (H False) (H True)))"
text {*
---------------------------------------------------------------------
Ejercicio 3. Definir int1,..., int8 para representar las
interpretaciones del ejercicio 1.
---------------------------------------------------------------------
*}
abbreviation int1 :: "nat ⇒ bool" where
"int1 x ≡ False"
abbreviation int2 :: "nat ⇒ bool" where
"int2 ≡ int1 (2 := True)"
abbreviation int3 :: "nat ⇒ bool" where
"int3 ≡ int1 (1 := True)"
abbreviation int4 :: "nat ⇒ bool" where
"int4 ≡ int1 (1 := True, 2 := True)"
abbreviation int5 :: "nat ⇒ bool" where
"int5 ≡ int1 (0 := True)"
abbreviation int6 :: "nat ⇒ bool" where
"int6 ≡ int1 (0 := True, 2 := True)"
abbreviation int7 :: "nat ⇒ bool" where
"int7 ≡ int1 (0 := True, 1 := True)"
abbreviation int8 :: "nat ⇒ bool" where
"int8 ≡ int1 (0 := True, 1 := True, 2 := True)"
text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
valor :: "(nat ⇒ bool) ⇒ nat ⇒ ddb ⇒ bool"
tal que (valor i n d) es el valor del DDB d en la interpretación i a
partir de la variable de índice n. Por ejemplo,
valor int1 0 ddb1 = True
valor int2 0 ddb1 = True
valor int3 0 ddb1 = False
valor int4 0 ddb1 = False
valor int5 0 ddb1 = False
valor int6 0 ddb1 = False
valor int7 0 ddb1 = False
valor int8 0 ddb1 = True
---------------------------------------------------------------------
*}
fun valor :: "(nat ⇒ bool) ⇒ nat ⇒ ddb ⇒ bool" where
"valor i n a = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
ddb_op_un :: "(bool ⇒ bool) ⇒ ddb ⇒ ddb
tal que (ddb_op_un f d) es el diagrama obtenido aplicando el operador
unitario f a cada hoja de DDB d de forma que se conserve el valor; es
decir,
valor i n (ddb_op_un f d) = f (valor i n d)"
Por ejemplo,
value "ddb_op_un (λx. ¬x) ddb1"
= N (N (H False) (H True)) (N (H True) (N (H True) (H False)))
---------------------------------------------------------------------
*}
fun ddb_op_un :: "(bool ⇒ bool) ⇒ ddb ⇒ ddb" where
"ddb_op_un f a = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que la definición de ddb_op_un es correcta; es
decir,
valor i n (ddb_op_un f d) = f (valor i n d)"
---------------------------------------------------------------------
*}
theorem ddb_op_un_correcto:
"valor i n (ddb_op_un f d) = f (valor i n d)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 7. Definir la función
ddb_op_bin :: "(bool ⇒ bool ⇒ bool) ⇒ ddb ⇒ ddb ⇒ ddb"
tal que (ddb_op_bin f d1 d2) es el diagrama obtenido aplicando el
operador binario f a los DDB d1 y d2 de forma que se conserve el
valor; es decir,
valor i n (ddb_op_bin f d1 d2) = f (valor i n d1) (valor i n d2)
Por ejemplo,
ddb_op_bin (op ∧) ddb1 (N (H True) (H False))
= N (N (H True) (H False)) (N (H False) (N (H False) (H False)))
ddb_op_bin (op ∧) ddb1 (N (H False) (H True))
= N (N (H False) (H False)) (N (H False) (N (H False) (H True)))
ddb_op_bin (op ∨) ddb1 (N (H True) (H False))
= N (N (H True) (H True)) (N (H False) (N (H False) (H True)))
ddb_op_bin (op ∨) ddb1 (N (H False) (H True))
= N (N (H True) (H False)) (N (H True) (N (H True) (H True)))
---------------------------------------------------------------------
*}
fun ddb_op_bin :: "(bool ⇒ bool ⇒ bool) ⇒ ddb ⇒ ddb ⇒ ddb" where
"ddb_op_bin f d1 d2 = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que la definición de ddb_op_bin es correcta;
es decir,
valor i n (ddb_op_bin f d1 d2) = f (valor i n d1) (valor i n d2)
---------------------------------------------------------------------
*}
theorem ddb_op_bin_correcto:
"valor i n (ddb_op_bin f d1 d2) = f (valor i n d1) (valor i n d2)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 9. Definir la función
ddb_and :: "ddb ⇒ ddb ⇒ ddb"
tal que (ddb_and d1 d2) es el diagrama correspondiente a la conjunción
de los DDB d1 y d2 de forma que se conserva el valor; es decir,
valor i n (ddb_and d1 d2) = (valor i n d1 ∧ valor i n d2)
Por ejemplo,
ddb_and ddb1 (N (H True) (H False))
= N (N (H True) (H False)) (N (H False) (N (H False) (H False)))
ddb_and ddb1 (N (H False) (H True))
= N (N (H False) (H False)) (N (H False) (N (H False) (H True)))
---------------------------------------------------------------------
*}
definition ddb_and :: "ddb ⇒ ddb ⇒ ddb" where
"ddb_and ≡ undefined"
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que la definición de ddb_and es correcta;
es decir,
valor i n (ddb_and d1 d2) = (valor i n d1 ∧ valor i n d2)
---------------------------------------------------------------------
*}
theorem ddb_and_correcta:
"valor i n (ddb_and d1 d2) = (valor i n d1 ∧ valor i n d2)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 11. Definir la función
ddb_or :: "ddb ⇒ ddb ⇒ ddb"
tal que (ddb_or d1 d2) es el diagrama correspondiente a la disyunción
de los DDB d1 y d2 de forma que se conserva el valor; es decir,
valor i n (ddb_or d1 d2) = (valor i n d1 ∨ valor i n d2)
Por ejemplo,
ddb_or ddb1 (N (H True) (H False))
= N (N (H True) (H True)) (N (H False) (N (H False) (H True)))
ddb_or ddb1 (N (H False) (H True))
= N (N (H True) (H False)) (N (H True) (N (H True) (H True)))
---------------------------------------------------------------------
*}
definition ddb_or :: "ddb ⇒ ddb ⇒ ddb" where
"ddb_or ≡ undefined"
text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar que la definición de ddb_or es correcta;
es decir,
valor i n (ddb_or d1 d2) = (valor i n d1 ∨ valor i n d2)
---------------------------------------------------------------------
*}
theorem ddb_or_correcta:
"valor i n (ddb_or d1 d2) = (valor i n d1 ∨ valor i n d2)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 13. Definir la función
ddb_not :: "ddb ⇒ ddb"
tal que (ddb_not d) es el diagrama correspondiente a la negación
del DDB d de forma que se conserva el valor; es decir,
valor i n (ddb_or d1 d2) = (valor i n d1 ∨ valor i n d2)
Por ejemplo,
ddb_not ddb1
= N (N (H False) (H True)) (N (H True) (N (H True) (H False)))
---------------------------------------------------------------------
*}
definition ddb_not :: "ddb ⇒ ddb" where
"ddb_not ≡ undefined"
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar que la definición de ddb_not es correcta;
es decir,
valor i n (ddb_not d) = (¬ valor i n d)
---------------------------------------------------------------------
*}
theorem ddb_not_correcta:
"valor i n (ddb_not d) = (¬ valor i n d)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función
xor :: "bool ⇒ bool ⇒ bool"
tal que (xor x y) es la disyunción excluyente de x e y. Por ejemplo,
xor True False = True
xor True True = False
---------------------------------------------------------------------
*}
definition xor :: "bool ⇒ bool ⇒ bool" where
"xor x y ≡ undefined"
text {*
---------------------------------------------------------------------
Ejercicio 16. Definir la función
ddb_xor :: "ddb ⇒ ddb ⇒ ddb"
tal que (ddb_xor d1 d2) es el diagrama correspondiente a la disyunción
excluyente de los DDB d1 y d2. Por ejemplo,
ddb_xor ddb1 (N (H True) (H False))
= N (N (H True) (H True)) (N (H False) (N (H False) (H True)))
ddb_xor ddb1 (N (H False) (H True))
= N (N (H True) (H False)) (N (H True) (N (H True) (H True)))
---------------------------------------------------------------------
*}
definition ddb_xor :: "ddb ⇒ ddb ⇒ ddb" where
"ddb_xor ≡ undefined"
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar que la definición de ddb_xor es correcta;
es decir,
valor i n (ddb_xor d1 d2) = xor (valor i n d1) (valor i n d2)
---------------------------------------------------------------------
*}
theorem ddb_xor_correcta:
"valor i n (ddb_xor d1 d2) = xor (valor i n d1) (valor i n d2)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 18. Definir la función
ddb_var :: "nat ⇒ ddb" where
tal que (ddb_var n) es el diagrama equivalente a la variable p(n). Por
ejemplo,
ddb_var 0
= N (H False) (H True)
ddb_var 1
= N (N (H False) (H True)) (N (H False) (H True))
---------------------------------------------------------------------
*}
fun ddb_var :: "nat ⇒ ddb" where
"ddb_var n = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 19. Demostrar que la definición de ddb_var es correcta;
es decir,
"valor i 0 (ddb_var n) = i n
---------------------------------------------------------------------
*}
lemma ddb_var_correcta:
"valor i 0 (ddb_var n) = i n"
oops
text {*
---------------------------------------------------------------------
Ejercicio 20. Definir el tipo de las fórmulas proposicionales
contruidas con la constante T, las variables (Var n) y las conectivas
Not, And, Or y Xor.
---------------------------------------------------------------------
*}
datatype form = T
| Var nat
| Not form
| And form form
| Or form form
| Xor form form
text {*
---------------------------------------------------------------------
Ejercicio 21. Definir la función
valor_fla :: "(nat ⇒ bool) ⇒ form ⇒ bool"
tal que (valor_fla i f) es el valor de la fórmula f en la
interpretación i. Por ejemplo,
valor_fla (λn. True) (Xor T T) = False
valor_fla (λn. False) (Xor T (Var 1)) = True
---------------------------------------------------------------------
*}
fun valor_fla :: "(nat ⇒ bool) ⇒ form ⇒ bool" where
"valor_fla i f = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 22. Definir la función
ddb_fla :: "form ⇒ ddb"
tal que (ddb_fla f) es el DDB equivalente a la fórmula f; es decir,
valor i 0 (ddb_fla f) = valor_fla i f
---------------------------------------------------------------------
*}
fun ddb_fla :: "form ⇒ ddb" where
"ddb_fla f = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 23. Demostrar que la definición de ddb_fla es correcta; es
decir,
valor i 0 (ddb_fla f) = valor_fla i f
---------------------------------------------------------------------
*}
theorem ddb_fla_correcta:
"valor e 0 (ddb_fla f) = valor_fla e f"
oops
text {*
Referencias:
· J.A. Alonso, F.J. Martín y J.L. Ruiz "Diagramas de decisión
binarios". En
http://www.cs.us.es/cursos/lp-2005/temas/tema-07.pdf
· Wikipedia "Binary decision diagram". En
http://en.wikipedia.org/wiki/Binary_decision_diagram
*}
end
