Lenguaje de Programación para Matemática | Coq / Gallina

Coq (gallo en francés) es un sistema de ayuda para la demostración de teoremas que maneja aserciones matemáticas, verifica mecánicamente las pruebas de aserciones, ayuda a encontrar pruebas para esas aserciones y extrae programas certificados (correctos) a partir de las pruebas constructivas de aserciones que representan su especificación formal. Coq trabaja basándose en la teoría del Cálculo de Construcciones Inductivas, que es una teoría derivada del Cálculo de Construcciones.

Fue desarrollado en Francia, en el proyecto LogiCal, entre el INRIA, la École Polytechnique, la Universidad París XI y el CNRS. Dirigen el desarrollo los investigadores Gilles Dowek y Christine Paulin-Mohring. Coq está escrito en el lenguaje Ocaml.

Coq y Gallina

Coq implementa un programa especifico y un  lenguaje matemática de alto nivel  llamado Gallina que se basa en un lenguaje formal expresiva llama el cálculo de inductivos construcciones que combina en sí tanto una lógica de orden superior y un lenguaje de programación funcional mecanografiado ricamente. A través de una lengua vernácula de comandos, Coq permite:

  • Definir funciones o predicados, que pueden ser evaluados eficientemente;
  • Establecer teoremas matemáticos y especificaciones de software;
  • Desarrollar interactivamente pruebas formales de estos teoremas;
  • Para verificar a máquina estas pruebas mediante un “núcleo” de certificación relativamente pequeño;
  • Para extraer programas certificados a lenguajes como Objective Caml, Haskell o Scheme.
  • Como sistema de desarrollo de la prueba, Coq ofrece métodos interactivos, a prueba de algoritmos de decisión y semi-decisión, y un lenguaje táctica para permitir al usuario definir sus propios métodos de
  • Prueba. La conexión con el sistema de álgebra computacional externa o los probadores de teorema está disponible.

Como plataforma para la formalización de las matemáticas o el desarrollo de programas, Coq proporciona soporte para notaciones de alto nivel, contenido implícito y varios otros tipos de macros útiles.

El paquete Coq

Coq viene con bibliotecas para aritmética eficiente en N, Z y Q, bibliotecas sobre listas, conjuntos finitos y mapas finitos, bibliotecas sobre conjuntos abstractos, relaciones, análisis clásico, etc.

Coq viene con:

  • Una interfaz gráfica de usuario basada en GTK (CoqIde)
  • Herramientas de documentación (coqdoc y coq-tex) y una herramienta de estadísticas (coqwc),
  • Dependencia y generación de herramientas para el makefile Coq (coq_makefile y coqdep),
  • Un verificador independiente de la prueba.

Fuentes:

https://es.wikipedia.org/wiki/Coq

https://coq.inria.fr

 

Guardar