Dado que no permite el cómputo no determinante, Coq no es necesariamente completo de Turing. ¿Cuál es la clase de funciones que Coq puede calcular? (¿hay una caracterización interesante de los mismos?)
22
Dado que no permite el cómputo no determinante, Coq no es necesariamente completo de Turing. ¿Cuál es la clase de funciones que Coq puede calcular? (¿hay una caracterización interesante de los mismos?)
Benjamin Werner ha demostrado la capacidad de interpretación mutua de ZFC con innumerables inaccesibles y el cálculo de construcciones inductivas, en su papel Conjuntos en tipos, tipos en conjuntos .
Esto significa, más o menos, que cualquier función que se pueda demostrar que es total en ZFC con innumerables inaccesibles se puede definir en Coq. Entonces, a menos que sea un teórico de conjunto que trabaje en cardenales grandes, es poco probable que cualquier función computable que alguna vez haya deseado no pueda definirse en Coq.