¿Cómo se puede construir una tabla de memorización coinductiva para funciones recursivas sobre árboles binarios?
La biblioteca StreamMemo para Coq ilustra cómo memorizar una función f : nat -> Asobre los números naturales. En particular cuando f (S n) = g (f n), imemo_makecomparte el cálculo de llamadas recursivas. Supongamos que, en lugar de números naturales, queremos memorizar funciones recursivas...