Considere un tipo inductivo que tiene algunas ocurrencias recursivas en una ubicación anidada, pero estrictamente positiva. Por ejemplo, árboles con ramificación finita con nodos que utilizan una estructura de datos de lista genérica para almacenar los elementos secundarios.
Inductive LTree : Set := Node : list LTree -> LTree.
La forma ingenua de definir una función recursiva sobre estos árboles recurriendo sobre árboles y listas de árboles no funciona. Aquí hay un ejemplo con la size
función que calcula el número de nodos.
Fixpoint size (t : LTree) : nat := match t with Node l => 1 + (size_l l) end
with size_l (l : list LTree) : nat := match l with
| nil => 0
| cons h r => size h + size_l r
end.
Esta definición está mal formada (mensaje de error extraído):
Error:
Recursive definition of size_l is ill-formed.
Recursive call to size has principal argument equal to
"h" instead of "r".
¿Por qué la definición está mal formada, aunque r
es claramente un subterráneo l
? ¿Hay alguna manera de definir funciones recursivas en dicha estructura de datos?
Si no tiene fluidez en la sintaxis de Coq: LTree
es un tipo inductivo que corresponde a la siguiente gramática.
Intentamos definir la size
función por inducción sobre árboles y listas. En OCaml, eso sería:
type t = Node of t list
let rec size = function Node l -> 1 + size_l l
and size_l = function [] -> 0
| h::r -> size h + size_l r
fuente
Respuestas:
Que funciona
Si anida la definición del punto de fijación en las listas dentro de la definición del punto de fijación en los árboles, el resultado está bien escrito. Este es un principio general cuando tiene recursión anidada en un tipo inductivo, es decir, cuando la recursión pasa por un constructor como
list
.O si prefiere escribir esto más brevemente:
(No tengo idea de quién lo escuché primero; esto ciertamente se descubrió independientemente muchas veces).
Un predicado de recursión general
De manera más general, puede definir el principio de inducción "adecuado"
LTree
manualmente. El principio de inducción generado automáticamenteLTree_rect
omite la hipótesis en la lista, porque el generador del principio de inducción solo comprende las ocurrencias estrictamente positivas no anidadas del tipo inductivo.Agreguemos la hipótesis de inducción en las listas. Para cumplirlo en la llamada recursiva, llamamos al principio de inducción de la lista y lo pasamos al principio de inducción del árbol en el árbol más pequeño dentro de la lista.
Por qué
La respuesta a por qué radica en las reglas precisas para aceptar funciones recursivas. Estas reglas son forzosamente sutiles, porque hay un delicado equilibrio entre permitir casos complejos (como este, con recursión anidada en el tipo de datos) y falta de solidez. El manual de referencia de Coq presenta el lenguaje (el cálculo de las construcciones inductivas, que es el lenguaje de prueba de Coq), principalmente con definiciones formalmente precisas, pero si desea las reglas exactas con respecto a la inducción y la coinducción necesitará ir a los trabajos de investigación, sobre este tema de Eduardo Giménez [1].
Fix
l
t
size
h
l
size_l
r
l
size_l
La razón por la cual
h
no es estructuralmente más pequeña quel
según el intérprete de Coq no me resulta clara. Según tengo entendido por las discusiones sobre la lista de Coq-club [1] [2], esta es una restricción en el intérprete, que en principio podría eliminarse, pero con mucho cuidado para evitar la introducción de una inconsistencia.Referencias
Cocorico, el wiki de Coq no terminante: inducción mutua
Lista de correo de Coq-Club:
El equipo de desarrollo de Coq. The Coq Proof Assistant: Manual de referencia . Versión 8.3 (2010). [ web ] cap. 4 .
Eduardo Giménez. Codificación de definiciones guardadas con esquemas recursivos . En Tipos'94: Tipos de pruebas y programas , LNCS 996. Springer-Verlag, 1994. doi: 10.1007 / 3-540-60579-7_3 [ Springer ]
Eduardo Giménez. Definiciones recursivas estructurales en la teoría de tipos . En ICALP'98: Actas del 25º Coloquio internacional sobre autómatas, idiomas y programación. Springer-Verlag, 1998. [ PDF ]
fuente
Obviamente, este es un problema específico de Coq, ya que creo que hay formas más agradables de solucionarlo con otros asistentes de prueba (estoy mirando Agda)
Al principio pensé que
r
no era reconocido como estructuralmente más pequeño porque la estructura solo se trata de la definición inductiva que actualmente manejaFixpoint
: por lo que esto no es unLTree
subterráneo, incluso si es unlist
subterráneo.Pero si expande el procesamiento de la lista, entonces funciona:
O como la función auxiliar ya existe en la biblioteca estándar:
Para ser sincero, no estoy seguro de por qué Coq los acepta, pero estoy feliz de que lo sean.
También hay una solución que funciona con más frecuencia y no solo para las listas: definir un tipo inductivo autónomo. En este caso, puede definir su
size
función manualmente. (con dos puntos de fijación)Tenga en cuenta que si tiene problemas para definiciones inductivas más complejas, puede usar un argumento de disminución de tamaño. Eso es posible pero engorroso para este problema (y me atrevería a decir que para la mayoría de los problemas)
fuente