Estamos algo trancados en esta parte del ejercicio 11.
No logramos interpretar que es lo que realiza el operador addAVLi.
Cualquier ayuda sirve!
Gracias
Hola.
Cada addAVLi sería un constructor (forma de generar) un árbol AVL no vacío válido. Por ejemplo:
Parameter addAVL1 : forall n:nat, nat -> AVLNat n -> AVLNat n -> AVLNat (n+1).
addAVL1 es correcto, aunque no permite generar todos los posibles AVLs; se precesia un addAVL2 y un addAVL3.
Saludos, Carlos
Hola. Yo había pensado esta definición de otra forma, y ahora mirando lo que vos decís me surge la siguiente duda:
en la definicion
Parameter addAVL1 : forall n:nat, nat -> AVLNat n -> AVLNat n -> AVLNat (n+1).
los AVLNat n representarían los sub-árboles izquierdo y derecho?
En ese caso, dónde está contada la raiz del árbol original?
Saludos y gracias.
Hola.
Está bien esta definición. Este sería el caso en que dado un natural (la raíz de tipo nat) y dados dos árboles (izquierdo y derecho) de la misma altura n (los dos argumentos de tipo: AVLNat n) se genera un árbol de altura n+1.
Saludos, Carlos
pd: notar que no alcanza con addAVL1, ya que un AVL se puede generar también a partir de un árbol de altura n y otro de altura n+1.
Podemos cambiarle el nombre a estos constructores? (en vez de addAVL_i ponerle algo más mnemónico (addAVL_r, addAVL_l, addAVL_b)).
Otra duda, esa definición de addAVL1, instanciada para un objeto n:nat, construye árboles de tamaño n+1 (a partir de árboles de tamaño n).
En las otras dos, para un n dado, construyo árboles de tamaño n+2 (a partir de árboles de prof n y n+1).
Se me ocurre que queda todo más claro si siempre para n:nat termino devolviendo algo del mismo tipo (quiero decir, que quede el tipo del parameter: forall n:nat, bla bla bla -> AVLNat (n+1)).
Pero para eso necesito tomar en addAVL_2 y addAVL_3 cosas de tipo AVLNat (n-1) como subarboles. (y escribir n-1 cuando hablamos de nats me da miedito)
No debería de ser problema porque simplemente no voy a poder crear nada con addAVL_{2,3} 0, el type checker no me deja, correcto?, pero no se si es "buena práctica" hacer eso, por ahí pasa la duda.
Espero haberme explicado bien, está bravo plantear la duda sin escribir la solución.
Saludos.
Hola.
Si, se pueden cambiar los nombres.
Está bien que un addAVL_i construya árboles de altua n+1 y las las otras generen árboles de altura n+2 (cuando los subárboles tienen diferencia de altura 1).
La alternativa mencionada tiene el problema referido sobre nat.
Saludos, Carlos