Coq
Тип | Proof assistant |
---|---|
Розробник | The Coq development team |
Перший випуск | 1 травня, 1989 (version 4.10) |
Стабільний випуск | 8.10.2[1] (29 листопада, 2019 ) |
Платформа | кросплатформова програма |
Операційна система | Cross-platform |
Мова програмування | OCaml |
Доступні мови | English |
Ліцензія | LGPLv2.1 |
Репозиторій | github.com/coq/coq |
Вебсайт | coq.inria.fr |
Coq (фр. coq — півень) — інтерактивний програмний засіб доведення теорем, використовує власну мову функціонального програмування (Gallina)[2] з залежними типами. Дозволяє записувати математичні теореми і їхні доведення, починаючи з цілі (гіпотези, яку потрібно довести). Coq може автоматично знаходити доведення в деяких обмежених теоріях за допомогою тактик. Coq використовується для верифікації програм.
Coq розроблений у Франції в рамках проекту TypiCal (раніше — LogiCal), спільно керується INRIA [Архівовано 26 лютого 2009 у Wayback Machine.], Політехнічною школою, Університетом Париж-Південь XI і Національним центром наукових досліджень, раніше була виділена група і в Вищій школі Ліона.
Теоретичною базою Coq є числення конструкцій; а назва — це абревіатура (CoC, англ. calculus of constructions) і скорочення прізвища творця обчислення — Тьєррі Кокана.
У 2013 році асоціація обчислювальної техніки нагородила Тьєррі Кокана, Жерар П'єр Хуета, Крістін Пауліна-Морінга, Бруно Барраса та інших премією ACM Software System Award за Coq.
Coq дозволяє:
- маніпулювати твердженнями обчислення
- механічно перевіряти докази цих тверджень
- сприяти пошуку формальних доведень
- синтезувати сертифіковані програми на основі конструктивного підтвердження їх специфікацій
Нещодавно[коли?] Coq удосконалили все більшими можливостями автоматизації. До них належить тактика Омега, яка визначає арифметику Пресбургера.
Це безкоштовне програмне забезпечення, яке розповсюджується на умовах ліцензії GNU LGPL.
Се��ед великих успіхів Coq можна відзначити:[джерело?]
- Проблема чотирьох фарб: була повністю механізована, демонстрація була завершена в 2005 році Жоржем Гонтьє та Бенджаміном Вернером
- Система неперетинних множин: доказ коректності у Coq був опублікований у 2007 році.
- Теорема Фейта-Томпсона: доказ теореми був завершений Жоржем Гонтьє та його командою у вересні 2012 року
- CompCert: компілятор, оптимізований для мови програмування C, який значною мірою запрограмований та перевірений у Coq
Жорж Гонтье (з Microsoft Research, в Кембриджі , Англія) і Бенджамін Вернер (з INRIA) використовуючи Coq довели теорему про Проблему чотирьох фарб.
На основі цієї роботи було розроблено значне розширення Coq під назвою Ssreflect (що означає «відображення в малих масштабах»). Більшість нових функцій, доданих в Ssreflect, є загальноприйнятими функціями, корисними не просто для стилю обчислювального відображення доведення. До них належать:
- Додаткові зручні позначення для неспростовного та спростовуваного узгодження шаблону на індуктивних типах з одним або двома конструкторами
- Неявні аргументи для функцій, застосованих до нульових аргументів — що корисно при програмуванні з функціями вищого порядку
- Стислі анонімні аргументи
- Вдосконалена
set
тактика з більш потужним узгодженням - Підтримка роздумів
Ssreflect 1.4 є у вільному доступі з подвійною ліцензією за ліцензією CeCILL-B або CeCILL-2.0 з відкритим кодом та сумісний з Coq 8.4.
До користувачів системи Coq належав Володимир Воєводський, лауреат медалі Філдса.[3]
- Мова реалізації — OCaml і С
- Ліцензія — GNU Lesser General Public Licence Version 2.1
- Середовища розробки:
- Компілятор coqc і інструменти для роботи з проектами, що складаються з безлічі файлів
- coqtop — консольна інтерактивне середовище
- Середовища розробки з графічним інтерфейсом користувача :
- CoqIDE
- Eclipse Proof General
- Режим для Emacs
- coqdoc — генератор документації до бібліотек, вихід в LaTeX і HTML
- Експорт доказів в XML для проектів HELM1 і MoWGLI
- Конструктивна математика відома тим, що з доказів існування величини можна екстрагувати алгоритм отримання цієї величини. Coq може експортувати алгоритми в мови ML і Haskell . Значення, які мають тип, що належить до сорту Prop, не екстрагуються; зазвичай ці значення є доведенням.
- Coq можна розширювати, не погіршуючи надійності. Коректність перевірки доказів залежить від proof-checker, який є невеликою частиною від усього проекту. Він перевіряє докази, згенеровані тактиками, тому некоректна тактика не призводить до прийняття доведення з помилкою. Таким чином, Coq слідує принципу де Брейна .
- Користувач може вводити власні аксіоми
- Заснований на предикативному обчисленні (до) індуктивних конструкцій, що означає:
- Всі можливості числення конструкцій:
- Кумулятивна ієрархія універсумів, що складається з Prop, Set і множини Type, індексованої натуральними числами
- Prop імпредикативний, Set і Type предикативні
- Індуктивні або алгебричні типи даних
- Коіндуктивні типи даних
- Можливо задати тільки частково рекурсивні функції, тобто такі функції, обчислення яких зупиняється, тобто не зациклюється. У Coq можна записати функцію Аккермана. Зупинка рекурсії по індуктивним типам даних (таким, як натуральні числа і списки) гарантується синтаксичною перевіркою визначення функції, так званою «guarded by destructors». Зупинка функцій, які використовують зіставлення зі зразком коіндуктивних типів, гарантується умовою «guarded by contructors».
- Неявне приведення типів, або спадкування
- Автоматичне виведення типів
- Виведення значень аргументів з типів
- Тактики можна писати на:
- Має великий набір примітивних тактик (наприклад, intro, elim) і менший набір розвинених тактик для специфічних теорій (наприклад, field для поля, omega для арифметики Пресбургер)
- Тактики групи setoid для імітації фактор-множин: задається відношення еквівалентності; функції, що зберігають це відношення; далі можна підставляти в термах еквівалентні (за вищезазначеною відношенню) значення
- Інтегровані класи типів (в стилі Haskell, починаючи з версії 8.2)
- Program і Russel для створення верифікованих програм з не верифікованих[6]
- The Coq proof assistant [Архівовано 25 серпня 2004 у Wayback Machine.] — офіційний англійський вебсайт
- coq/coq [Архівовано 31 грудня 2019 у Wayback Machine.] — сховище коду на GitHub
- JsCoq Interactive Online System [Архівовано 14 жовтня 2019 у Wayback Machine.] — дозволяє запускати Coq у веббраузері без необхідності будь-якої інсталяції програмного забезпечення
- Coq Wiki [Архівовано 24 грудня 2019 у Wayback Machine.]
- Mathematical Components library [Архівовано 21 листопада 2019 у Wayback Machine.] –широко використовувана бібліотека математичних структур, частиною якої є мова Ssreflect
- Constructive Coq Repository at Nijmegen [Архівовано 2 жовтня 2011 у Wayback Machine.]
- Math Classes [Архівовано 1 січня 2019 у Wayback Machine.]
Підручники:
- The Coq'Art [Архівовано 24 вересня 2019 у Wayback Machine.] — книга про Coq Іва Бертота та П'єра Кастерана
- Certified Programming with Dependent Types [Архівовано 9 вересня 2011 у Wayback Machine.] — онлайн та друкований підручник Адама Чліпала
- Software Foundations [Архівовано 9 листопада 2013 у Wayback Machine.] — онлайн-підручник Бенджаміна К. Пірса та ін.
- An introduction to small scale reflection in Coq [Архівовано 23 лютого 2020 у Wayback Machine.] — навчальний посібник з SSreflect Жоржа Гонтьє та Ассіа Махбубі
- Introduction to the Coq Proof Assistant [Архівовано 4 грудня 2019 у Wayback Machine.] — відео лекція Ендрю Апеля в Інституті підвищення кваліфікації
- Video tutorials for the Coq proof assistant [Архівовано 4 грудня 2019 у Wayback Machine.] від Андрея Бауера
- ↑ Coq 8.10.2 is out. 29 листопада 2019. Архів оригіналу за 31 грудня 2019. Процитовано 30 листопада 2019.
- ↑ Adam Chlipala. Library Universes (англ.). Архів оригіналу за 2 січня 2014. Процитовано 3 грудня 2019.
- ↑ Hartnett, Kevin (19 травня 2015). Will Computers Redefine the Roots of Math?. Quanta Magazine.
- ↑ Manual, 2009, «Building a toplevel extended with user tactics».
- ↑ Manual, 2009, «The tactic language».
- ↑ Manual, 2009, «Program».