Soy curioso. He estado trabajando en este tipo de datos en OCaml :
type 'a exptree =
| Epsilon
| Delta of 'a exptree * 'a exptree
| Omicron of 'a
| Iota of 'a exptree exptree
Que se puede manipular utilizando funciones recursivas escritas explícitamente (una característica que se ha agregado recientemente). Ejemplo:
let rec map : 'a 'b. ('a -> 'b) -> 'a exptree -> 'b exptree =
fun f ->
begin function
| Epsilon -> Epsilon
| Delta (t1, t2) -> Delta (map f t1, map f t2)
| Omicron t -> Omicron (f t)
| Iota tt -> Iota (map (map f) tt)
end
Pero nunca he podido definirlo en Coq :
Inductive exptree a :=
| epsilon : exptree a
| delta : exptree a -> exptree a -> exptree a
| omicron : a -> exptree a
| iota : exptree (exptree a) -> exptree a
.
Coq se queja. No le gusta el último constructor, y dice algo que no entiendo completamente o no estoy de acuerdo:
Error: Non strictly positive occurrence of "exptree" in "exptree (exptree a) -> exptree a".
Lo que puedo entender es que los tipos inductivos que usan una negación dentro de su definición como type 'a term = Constructor ('a term -> …)
son rechazados, porque darían lugar a bestias feas no bien fundadas como términos λ (sin tipo). Sin embargo, este exptree
tipo de datos en particular parece bastante inocuo: mirando su definición OCaml , su argumento 'a
nunca se usa en posiciones negativas.
Parece que Coq es demasiado cauteloso aquí. Entonces, ¿hay realmente un problema con este tipo de datos inductivo en particular? ¿O podría Coq ser un poco más permisivo aquí?
Además, ¿qué pasa con otros asistentes de pruebas, son capaces de hacer frente a una definición tan inductiva (de forma natural)?
fuente