Buenas,
Estoy teniendo problemas para definir inductivamente los tipos sorted, mirror e isomorfo. En el caso de sorted no veo como interpretar la relacion de orden. En cuanto a mirror e isomorfo, no entiendo como trabajar con la estructura del arbol. El arbol binario lo defini de la siguiente manera:
Inductive bintree (A:Set):Set :=
empty_bintree : bintree A
| node : A -> bintree A -> bintree A -> bintree A.
Muchas gracias, saludos.
Buenas, seguimos sin entender como trabajar con la estructura del árbol binario. Lo que no vemos es como aplicar la recursión sobre los subarboles.
Gracias, saludos.
Hola.
Quizás lo que los complica es que cuando uno piensa la definición de un tipo inductivo (por ejemplo mirror para árboles binarios) tiene que dar todas las reglas de construcción del tipo que quiere generar. Esto es al revés que cuando uno piensa la definición de una función recursiva (por ejemplo inverse); en este caso uno va consumiendo la estructura (ya está construida) para computar algo (por ejemplo el espejo de un árbol).
Para el ejemplo:
Inductive bintree (A : Set) : Set :=
| empty_bt : bintree A
| node : bintree A -> A -> bintree A -> bintree A.
Inductive mirror (A : Set) : bintree A -> bintree A -> Prop :=
| mirror_empty : mirror A (empty_bt A) (empty_bt A)
| mirror_node :
forall (a : A) (t11 t12 t21 t22 : bintree A),
mirror A t11 t22 ->
mirror A t12 t21 ->
mirror A (node A t11 a t12) (node A t21 a t22).
Fixpoint inverse (A : Set) (t : bintree A):
bintree A :=
match t with
| empty_bt _ => empty_bt A
| node _ t1 a t2 => node A (inverse A t2) a (inverse A t1)
end.
Saludos, Carlos
