¿Cómo definir una función inductivamente en dos argumentos en Coq?

14

¿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.

yhirai
fuente
1
¿Has intentado pasar l y r juntos como producto en lugar de usar curry? Eso debería ayudarlo.
Por Vognsen
1
Algunas personas piensan que esta pregunta es acerca de la programación y está fuera del alcance de este sitio web. Si bien no estoy seguro de si estoy de acuerdo, es posible que desee saber sobre el posible problema. Si alguien tiene algo que decir sobre la idoneidad, escriba en la meta discusión a la que me vinculé.
Tsuyoshi Ito
3
Esta pregunta se trata realmente de especificar límites decrecientes monotónicamente en las estructuras de datos para garantizar que la operación pairesté bien definida. Coq es simplemente el vehículo.
Dave Clarke

Respuestas:

12

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.

Fixpoint pair l := fix pair1 (r : Tree) :=
  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 (pair1 rl) (pair lr r)
                   end
  end.

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 Programvernáculo .

Gilles 'SO- deja de ser malvado'
fuente
¡Ahora sé que esto es lo que pedí!
yhirai
¿Hará alguna diferencia si me meto fix pair1 ren la segunda rama del nivel superior match(y, por supuesto, adapto la primera rama para devolver un tipo de función en consecuencia)?
día
@plmday: trabajo en ambos sentidos. Son equivalentes extensionalmente para alguna definición razonable de extensionalidad, y lo más importante, ambos están bien tipificados (la reescritura extensional no cambia ninguna de las propiedades de covarianza (positividad) relevantes).
Gilles 'SO- deja de ser malvado'