¿Existe algún trabajo para crear un Marco de Teoría de Número Real / Probabilidad en COQ?

8

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?

HdM
fuente
Se parece que hace números reales de apoyo en la biblioteca estándar, por lo que es probable que también tiene un montón de teoremas.
Raphael

Respuestas:

7

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)

jmad
fuente