stringtranslate.com

Coq (software)

Una sesión de prueba interactiva en CoqIDE, que muestra el script de prueba a la izquierda y el estado de la prueba a la derecha.

Coq es un demostrador de teoremas interactivo lanzado por primera vez en 1989. Permite expresar afirmaciones matemáticas, verifica mecánicamente las pruebas de estas afirmaciones, ayuda a encontrar pruebas formales y extrae un programa certificado a partir de la prueba constructiva de su especificación formal . Coq trabaja dentro de la teoría del cálculo de construcciones inductivas , una derivada del cálculo de construcciones . Coq no es un demostrador de teoremas automatizado , pero incluye tácticas ( procedimientos ) de demostración de teoremas automáticas y varios procedimientos de decisión .

La Association for Computing Machinery premió a Thierry Coquand , Gérard Huet , Christine Paulin-Mohring , Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot y Pierre Castéran con el premio ACM Software System Award 2013 por Coq.

El nombre "Coq" es un juego de palabras con el nombre de Thierry Coquand, Cálculo de construcciones o "CoC" y sigue la tradición informática francesa de nombrar software con nombres de animales ( coq en francés significa gallo). [2] El 11 de octubre de 2023, el equipo de desarrollo anunció que Coq pasará a llamarse "The Rocq Prover" en los próximos meses y ha comenzado a actualizar el código base, el sitio web y las herramientas asociadas. [3]

Descripción general

Cuando se ve como un lenguaje de programación, Coq implementa un lenguaje de programación funcional escrito de forma dependiente ; [4] cuando se ve como un sistema lógico, implementa una teoría de tipos de orden superior . El desarrollo de Coq ha contado con el apoyo desde 1984 de INRIA , ahora en colaboración con la École Polytechnique , la Universidad Paris-Sud , la Universidad Paris Diderot y el CNRS . En los años 1990, la ENS Lyon también formó parte del proyecto. El desarrollo de Coq fue iniciado por Gérard Huet y Thierry Coquand, y más de 40 personas, principalmente investigadores, han contribuido con funciones al sistema central desde su inicio. El equipo de implementación ha sido coordinado sucesivamente por Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin y Matthieu Sozeau. Coq se implementa principalmente en OCaml con un poco de C. El sistema central se puede ampliar mediante un mecanismo enchufable . [5]

El nombre coq significa " gallo " en francés y proviene de una tradición francesa de nombrar las herramientas de desarrollo de investigación con nombres de animales. [6] Hasta 1991, Coquand estaba implementando un lenguaje llamado Cálculo de Construcciones y en ese momento simplemente se llamaba CoC. En 1991, se inició una nueva implementación basada en el Cálculo de Construcciones Inductivas extendido y se cambió el nombre de CoC a Coq en una referencia indirecta a Coquand, quien desarrolló el Cálculo de Construcciones junto con Gérard Huet y contribuyó al Cálculo de Construcciones Inductivas. con Christine Paulin-Mohring. [7]

Coq proporciona un lenguaje de especificación llamado Gallina [8] (" gallina " en latín, español, italiano y catalán). Los programas escritos en Gallina tienen la propiedad de normalización débil , lo que implica que siempre terminan. Esta es una propiedad distintiva del lenguaje, ya que los bucles infinitos (programas sin terminación) son comunes en otros lenguajes de programación, [9] y es una forma de evitar el problema de la detención .

Como ejemplo, una prueba de conmutatividad de la suma de números naturales en Coq:

plus_comm  = fun  n  m  :  nat  => nat_ind  ( fun  n0  :  nat  =>  n0  +  m  =  m  +  n0 )  ( plus_n_0  m )  ( fun  ( y  :  nat )  ( H  :  y  +  m  =  m  +  y )  =>  eq_ind  ( S  ( m  +  y ))  ( fun  n0  :  nat  =>  S  ( y  +  m )  =  n0 )  ( f_equal  S  H )  ( m  +  S  y )  ( plus_n_Sm  m  y ))  n  :  forall  n  m  :  nat ,  n  +  metro  =  metro  +  norte

nat_indrepresenta la inducción matemática , eq_indla sustitución de iguales y f_equalla toma de la misma función en ambos lados de la igualdad. Se hace referencia a teoremas anteriores que muestran y .

Usos notables

Teorema de los cuatro colores y extensión SSReflect

Georges Gonthier de Microsoft Research en Cambridge , Inglaterra y Benjamin Werner de INRIA utilizaron Coq para crear una prueba encuestable del teorema de los cuatro colores , que se completó en 2002. [10] Su trabajo condujo al desarrollo del SSReflect ("Reflexión a pequeña escala"). "), que fue una extensión significativa de Coq. [11] A pesar de su nombre, la mayoría de las características agregadas a Coq por SSReflect son características de propósito general y no se limitan al estilo de prueba de reflexión computacional. Estas características incluyen:

SSReflect 1.11 está disponible gratuitamente, tiene doble licencia bajo la licencia de código abierto CeCILL-B o CeCILL-2.0 y es compatible con Coq 8.11. [12]

Otras aplicaciones

lenguaje táctico

Además de construir términos de Gallina explícitamente, Coq admite el uso de tácticas escritas en el lenguaje integrado Ltac o en OCaml. Estas tácticas automatizan la construcción de pruebas, llevando a cabo pasos triviales u obvios en las pruebas. [17] Varias tácticas implementan procedimientos de decisión para diversas teorías. Por ejemplo, la táctica del "anillo" decide la teoría de la igualdad de los axiomas de módulo de anillo o semianillo mediante reescritura asociativa - conmutativa . [18] Por ejemplo, la siguiente prueba establece una igualdad compleja en el anillo de números enteros en una sola línea de prueba: [19]

Requerir  importar  ZARith . Abra  el ámbito  Z_scope . Objetivo  para todos  a  b  c : Z ,  ( a  +  b  +  c )  ^  2  =  a  *  a  +  b  ^  2  +  c  *  c  +  2  *  a  *  b  +  2  *  a  *  c  +  2  *  b  *  c .  introducciones ;  anillo . Qed .

Los procedimientos de decisión incorporados también están disponibles para la teoría vacía ("congruencia"), la lógica proposicional ("tauto"), la aritmética lineal de enteros sin cuantificadores ("lia") y la aritmética lineal racional/real ("lra"). [20] [21] Se han desarrollado otros procedimientos de decisión como bibliotecas, incluida una para álgebras de Kleene [22] y otra para ciertos objetivos geométricos . [23]

Ver también

Referencias

  1. ^ "Lanzamiento de Coq 8.19.2". 10 de junio de 2024 . Consultado el 17 de julio de 2024 .
  2. ^ "Nombres alternativos · coq/coq Wiki". GitHub . Consultado el 3 de marzo de 2023 .
  3. ^ "Hoja de ruta de Coq 069". GitHub .
  4. ^ Una breve introducción a Coq
  5. ^ Avigad, Jeremy; Mahboubi, Assia (3 de julio de 2018). Demostración interactiva de teoremas: Novena Conferencia Internacional, ITP 2018, celebrada como... Springer. ISBN 9783319948218. Consultado el 21 de octubre de 2018 .
  6. ^ "Preguntas frecuentes". GitHub . Consultado el 8 de mayo de 2019 .
  7. ↑ «Introducción al Cálculo de Construcciones Inductivas» . Consultado el 21 de mayo de 2019 .
  8. ^ Adán Chlipala. "Programación certificada con tipos dependientes": "Universos de biblioteca".
  9. ^ Adán Chlipala. "Programación certificada con tipos dependientes": "Biblioteca GeneralRec". "Biblioteca de tipos inductivos".
  10. ^ Gonthier, Georges (2008). "Demostración formal: el teorema de los cuatro colores" (PDF) . Avisos de la Sociedad Matemática Estadounidense . 55 (11): 1382-1393. SEÑOR  2463991.
  11. ^ Gonthier, Georges; Mahboubi, Assia (2010). "Una introducción a la reflexión a pequeña escala en Coq". Revista de razonamiento formalizado . 3 (2): 95-152. doi :10.6092/ISSN.1972-5787/1979.
  12. ^ "La biblioteca de componentes matemáticos 1.11.0". GitHub .
  13. ^ Conchón, Sylvain; Filliâtre, Jean-Christophe (2007). "Una estructura de datos persistente para encontrar sindicatos". En Russo, Claudio V.; Dreyer, Derek (eds.). Actas del taller ACM sobre ML, 2007, Friburgo, Alemania, 5 de octubre de 2007. Asociación de Maquinaria de Computación. págs. 37–46. doi :10.1145/1292535.1292541.
  14. ^ "El teorema de Feit-Thompson ha sido totalmente comprobado en Coq". msr-inria.inria.fr. 2012-09-20. Archivado desde el original el 19 de noviembre de 2016 . Consultado el 25 de septiembre de 2012 .
  15. ^ "[2 de julio de 2024] Hemos demostrado" BB(5) = 47.176.870"". El desafío del castor ocupado . 2024-07-02 . Consultado el 2 de julio de 2024 .
  16. ^ "El desafío del castor ocupado". bbchallenge.org . Consultado el 2 de julio de 2024 .
  17. ^ Kaiser, Jan-Oliver; Ziliani, Beta; Krebbers, Robbert; Régis-Gianas, Yann; Dreyer, Derek (30 de julio de 2018). "Mtac2: tácticas escritas para el razonamiento hacia atrás en Coq". Actas de la ACM sobre lenguajes de programación . 2 (CIFP): 78:1–78:31. doi : 10.1145/3236773 . hdl : 21.11116/0000-0003-2E8E-B .
  18. ^ Grégoire, Benjamín; Mahboubi, Assia (2005). "Demostración de igualdades en un anillo conmutativo hecho correctamente en Coq". En Hurd, Joe; Melham, Tom (eds.). Demostración de teoremas en lógica de orden superior: 18ª Conferencia Internacional, TPHOLs 2005, Oxford, Reino Unido, 22 al 25 de agosto de 2005, Actas. Apuntes de conferencias sobre informática. Berlín, Heidelberg: Springer. págs. 98-113. doi :10.1007/11541868_7. ISBN 978-3-540-31820-0.
  19. ^ "Las familias de tácticas de anillo y campo: documentación de Coq 8.11.1". coq.inria.fr . Consultado el 4 de diciembre de 2023 .
  20. ^ Besson, Federico (2007). "Tácticas aritméticas reflexivas rápidas en el caso lineal y más allá". En Altenkirch, Thorsten; McBride, Conor (eds.). Tipos de pruebas y programas: taller internacional, TIPOS 2006, Nottingham, Reino Unido, 18 al 21 de abril de 2006, artículos seleccionados revisados . Apuntes de conferencias sobre informática. vol. 4502. Berlín, Heidelberg: Springer. págs. 48–62. doi :10.1007/978-3-540-74464-1_4. ISBN 978-3-540-74464-1.
  21. ^ "Micromega: solucionadores de objetivos aritméticos sobre anillos ordenados - documentación de Coq 8.18.0". coq.inria.fr . Consultado el 4 de diciembre de 2023 .
  22. ^ Braibant, Thomas; Pous, Damián (2010). Kaufmann, Matt; Paulson, Lawrence C. (eds.). Una táctica Coq eficaz para decidir las álgebras de Kleene. Demostración interactiva de teoremas: Primera conferencia internacional, ITP 2010 Edimburgo, Reino Unido, 11 al 14 de julio de 2010, Actas. Apuntes de conferencias sobre informática. Berlín, Heidelberg: Springer. págs. 163-178. doi :10.1007/978-3-642-14052-5_13. ISBN 978-3-642-14052-5. S2CID  3566183.
  23. ^ Narboux, Julien (2004). "Un procedimiento de decisión para la geometría en Coq". En Slind, Konrad; Búnker, Annette; Gopalakrishnan, Ganesh (eds.). Demostración de teoremas en lógica de orden superior: 17ª Conferencia Internacional, TPHOLS 2004, Park City, Utah, EE. UU., 14 al 17 de septiembre de 2004, Actas . Apuntes de conferencias sobre informática. vol. 3223. Berlín, Heidelberg: Springer. págs. 225–240. doi :10.1007/978-3-540-30142-4_17. ISBN 978-3-540-30142-4. S2CID  11238876.

enlaces externos

Wikimedia Commons tiene medios relacionados con Coq (lenguaje de programación) .
Libros de texto
Tutoriales