Buenas noches
Nos surgió una duda realizando la parte 1 del ejercicio 8: con definir la función size que se pide y el orden elt ya alcanza? O debemos de alguna forma justificar "la terminación
de los programas que evalúan expresiones (de forma ansiosa y perezosa)" ?
Definimos una función size y en la parte 2 demostramos que elt es un orden bien fundado, pero nos queda la duda de si tenemos que hacer algo más en la parte 1.
Gracias y saludos
Hola!
Lo que hicieron es lo que se pedía: definir la función size, luego elt y probar que elt es bien fundada.
Saludos, Carlos
Hola.
Acoto algo más.
Es un buen ejercicio para usar el resultado de inverse_image, considerando que la relación menor entre naturales es bien fundada (lt_wf).
Al probar que la relación elt entre árboles (un árbol es menor que otro si tiene menos nodos) es bien fundada, habilitaría a usar este orden para justificar la terminación de una función sobre árboles que no sea definida por recursión estructural (con Fixpoint). Para justificar su terminación habría que ver que los árboles en las llamadas recursivas tienen menos nodos que el árbol parámetro (pero esto no se pide en el ejercicio).
Saludos, Carlos
