La biblioteca StreamMemo para Coq ilustra cómo memorizar una función f : nat -> A
sobre los números naturales. En particular cuando f (S n) = g (f n)
, imemo_make
comparte el cálculo de llamadas recursivas.
Supongamos que, en lugar de números naturales, queremos memorizar funciones recursivas sobre árboles binarios:
Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -> binTree -> binTree.
Supongamos que tenemos una función f : binTree -> A
que es estructuralmente recursiva, lo que significa que hay una función g : A -> A -> A
tal que f (Branch x y) = g (f x) (f y)
. ¿Cómo construimos una tabla de notas similar para f
Coq de modo que se compartan los cálculos recursivos?
En Haskell, no es demasiado difícil construir una tabla de notas (ver MemoTrie por ejemplo) y atar el nudo. Claramente, tales tablas de notas son productivas. ¿Cómo podemos organizar las cosas para convencer a un lenguaje mecanografiado de manera dependiente de que acepte que este nudo sea productivo?
Aunque especifiqué el problema en Coq, me encantaría recibir una respuesta en Agda o en cualquier otro lenguaje de tipo dependiente.
fuente
go
valor es una función de un parámetro Tamaño. En general, no se comparte entre llamadas a funciones independientes con el mismo valor. Esto probablemente se puede solucionar agregando una declaración let en la definición deh (Branch l r)
. En segundo lugar, la definición estratificada deBT
significa que dos, de otro modo árboles idénticos, tendrán valores diferentes cuando ocurran en niveles diferentes. Estos valores distintos no se compartirán en el MemoTrie.Memo
inbranch
. El verificador de positividad de Coq parece rechazar esto, haciendo las cosas más complicadas en Coq.Size
tipos terminen borrados.He creado una "solución" que memoriza recursivamente funciones estructuralmente recursivas de árboles binarios en Coq. Mi esencia está en https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b .
Funciona de manera similar a la solución de Saizan , estratificando árboles binarios basados en una métrica de tamaño, en mi caso contando el número de nodos internos de árboles binarios, y produciendo un flujo lento de contenedores de todas las soluciones para un tamaño particular. El intercambio se produce debido a una declaración let en el generador de flujo que contiene la parte inicial del flujo que se utilizará en partes posteriores del flujo.
Los ejemplos muestran que
vm_compute
, para evaluar un árbol binario perfecto con 8 niveles después de haber evaluado un árbol binario perfecto con 9 niveles es mucho más rápido que solo evaluar un árbol binario perfecto con 8 niveles.Sin embargo, dudo en aceptar esta respuesta porque la sobrecarga de esta solución en particular es mala, ya que funciona mucho peor que mi memorización sin recurrencia estructural para mis ejemplos de aportes prácticos. Naturalmente, quiero una solución que funcione mejor con entradas razonables.
Tengo algunos comentarios adicionales en " [Coq-Club] ¿Cómo puedes construir una tabla de memorización coinductiva para funciones recursivas sobre árboles binarios? ".
fuente