¿Cómo puedo convencer a Coq de que la función recursiva dada a continuación termina? La función toma dos argumentos inductivos. Intuitivamente, la recursión termina porque cualquiera de los argumentos se descompone.
Específicamente, la función toma dos árboles como entrada.
Inductive Tree :=
| Tip: Tree
| Bin: Tree -> Tree -> Tree.
En los árboles, me gusta hacer el siguiente estilo de inducción.
Inductive TreePair :=
| TipTip : TreePair
| TipBin : Tree -> Tree -> TreePair
| BinTip : Tree -> Tree -> TreePair
| BinBin : TreePair -> TreePair -> TreePair.
Fixpoint pair (l r: Tree): TreePair :=
match l with
| Tip =>
match r with
| Tip => TipTip
| Bin rl rr => TipBin rl rr
end
| Bin ll lr =>
match r with
| Tip => BinTip ll lr
| Bin rl rr => BinBin (pair l rl) (pair lr r)
end
end.
Se acepta la definición de TreePair, pero la definición del par de funciones produce el mensaje de error:
Error: Cannot guess decreasing argument of fix.
Así que estoy interesado en cómo convencer a Coq de la terminación.
pair
esté bien definida. Coq es simplemente el vehículo.Respuestas:
Las definiciones de punto fijo de Coq requieren que las llamadas inductivas reciban un argumento estructuralmente más pequeño. En el fondo, una construcción de punto de fijación toma un solo argumento: no hay un concepto incorporado de una definición recursiva sobre dos argumentos. Afortunadamente, la definición de Coq de estructuralmente más pequeña incluye tipos de orden superior, lo cual es extremadamente poderoso.
La definición de punto fijo de dos argumentos sigue un patrón simple: el primer argumento se vuelve más pequeño o el primer argumento permanece idéntico y el segundo argumento se vuelve más pequeño. Este patrón bastante común se puede manejar con una simple reparación.
Para casos más complejos, o si sus gustos se ejecutan de esa manera, puede usar la recursión más cerca de la forma en que se enseña en los cursos de matemáticas, construyendo el punto de fijación a partir de un cálculo de pasos y un argumento de fundamento separado , a menudo utilizando una medida entera . También puede hacer que su definición se parezca más a un programa clásico en un lenguaje no total con una terminación separada usando el lenguaje
Program
vernáculo .fuente
fix pair1 r
en la segunda rama del nivel superiormatch
(y, por supuesto, adapto la primera rama para devolver un tipo de función en consecuencia)?