COQ es un probador de teoremas interactivo que utiliza el cálculo de construcciones inductivas, es decir, se basa en gran medida en tipos inductivos. Utilizándolos, las estructuras discretas como números naturales, números racionales, gráficos, gramáticas, semánticas, etc. se representan de manera muy concisa.
Sin embargo, desde que me gustó el asistente de pruebas, me preguntaba si hay bibliotecas para estructuras incontables, como números reales, números complejos, límites de probabilidad y demás. Por supuesto, soy consciente de que no se pueden definir estas estructuras inductivamente (al menos no hasta donde yo sé), pero se pueden definir axiomáticamente, utilizando, por ejemplo, el enfoque axiomático .
¿Hay algún trabajo que proporcione propiedades básicas, o incluso límites probabilísticos como el enlace de Chernoff o el enlace de unión como una biblioteca?
Respuestas:
La biblioteca estándar de Coq tiene una sección sobre números reales. Estos son los números reales clásicos, usando la terminación Dedekind . También hay resultados sobre números complejos, supongo que hay varias bibliotecas, conozco esta . Tenga en cuenta que también hay muchos resultados para números constructivos reales y complejos, C-CoRN es la referencia.
Nota al margen: también podría definir inductivamente números reales (computables) con algunas de las axiomáticas constructivas, por ejemplo, usando números racionales de las secuencias de Cauchy o alguna versión constructiva de la propiedad de límite superior mínimo. No estoy seguro de cuánto inductivo que esto.
Sé que hay algunas personas trabajando en probabilidades con Coq. Lamentablemente, no estoy seguro de cuán avanzados son sus trabajos. Supongo que es probable que no haya un resultado tan específico sobre Chernoff o la unión. (Pero es solo una suposición)
fuente
¡Mira esto! http://coq.io/opam/coq-markov.8.5.0.html . Una biblioteca para la desigualdad de Markov basada en la teoría de la probabilidad matemática.
fuente