Coq

Coq (фр. coq — півень) — інтерактивний програмний засіб доведення теорем, використовує власну мову функціонального програмування (Gallina)[3] з залежними типами. Дозволяє записувати математичні теореми і їхні доведення, починаючи з цілі (гіпотези, яку потрібно довести). Coq може автоматично знаходити доведення в деяких обмежених теоріях за допомогою тактик. Coq використовується для верифікації програм.

Coq (software)
Тип Proof assistant
Розробник The Coq development team
Перший випуск 1 травня, 1989 (1989-05-01) (version 4.10)
Стабільний випуск 8.10.2[1] (29 листопада, 2019 (2019-11-29))
Версії 8.15.0 (13 січня 2022)[2]
Репозиторій github.com/coq/coq
Платформа крос-платформова програма
Операційна система Cross-platform
Мова програмування OCaml
Доступні мови English
Ліцензія LGPLv2.1
Вебсайт coq.inria.fr
 Coq (software) у Вікісховищі

Історія розробки

Coq розроблений у Франції в рамках проекту TypiCal (раніше — LogiCal), спільно керується INRIA, Політехнічною школою, Університетом Париж-Південь XI і Національним центром наукових досліджень, раніше була виділена група і в Вищій школі Ліона.

Теоретичною базою Coq є обчислення конструкцій; а назва - це абревіатура (CoC, англ. англ. calculus of constructions) і скорочення прізвища творця обчислення — Тьєррі Кокана.

У 2013 році асоціація обчислювальної техніки нагородила Тьєррі Кокана , Жерар П'єр Хуета , Крістін Пауліна-Морінга , Бруно Барраса та інших премією ACM Software System Award за Coq.

Особливості програмного забезпечення

Coq дозволяє:

  • маніпулювати твердженнями обчислення
  • механічно перевіряти докази цих тверджень
  • сприяти пошуку формальних доведень
  • синтезувати сертифіковані програми на основі конструктивного підтвердження їх специфікацій

Нещодавно[коли?] Coq удосконалили все більшими можливостями автоматизації. До них належить тактика Омега, яка визначає арифметику Пресбургера.

Це безкоштовне програмне забезпечення, яке розповсюджується на умовах ліцензії GNU LGPL.

Серед великих успіхів Coq можна відзначити:

  • Проблема чотирьох фарб: була повністю механізована, демонстрація була завершена в 2005 році Жоржем Гонтьє та Бенджаміном Вернером
  • Система неперетинних множин: доказ коректності у Coq був опублікований у 2007 році.
  • Теорема Фейта-Томпсона: доказ теореми був завершений Жоржем Гонтьє та його командою у вересні 2012 року
  • CompCert: компілятор, оптимізований для мови програмування C, який значною мірою запрограмований та перевірений у Coq

Проблема чотирьох фарб та розширення Ssreflect 

Жорж Гонтье (з Microsoft Research , в Кембриджі , Англія ) і Бенджамін Вернер (з INRIA ) використовуючи Coq довели теорему про Проблему чотирьох фарб.

На основі цієї роботи було розроблено значне розширення Coq під назвою Ssreflect (що означає «відображення в малих масштабах»).  Більшість нових функцій, доданих в Ssreflect, є загальноприйнятими функціями, корисними не просто для стилю обчислювального відображення доведення. До них належать:

  • Додаткові зручні позначення для неспростовного та спростовуваного узгодження шаблону на індуктивних типах з одним або двома конструкторами
  • Неявні аргументи для функцій, застосованих до нульових аргументів - що корисно при програмуванні з функціями вищого порядку
  • Стислі анонімні аргументи
  • Вдосконалена setтактика з більш потужним узгодженням
  • Підтримка роздумів

Ssreflect 1.4 є у вільному доступі з подвійною ліцензією за ліцензією CeCILL-B або CeCILL-2.0 з відкритим кодом та сумісний з Coq 8.4.

Інструменти
  • Мова реалізації - 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».
    • Неявне приведення типів, або спадкування
  • Автоматичне виведення типів
  • Виведення значень аргументів з типів
  • Тактики можна писати на:
    • Мові програмування ML[4]
    • Спеціальній мові для тактик Ltac [5]
    • Coq, використовуючи тактику quote
  • Має великий набір примітивних тактик (наприклад, intro, elim) і менший набір розвинених тактик для специфічних теорій (наприклад, field для поля, omega для арифметики Пресбургер)
  • Тактики групи setoid для імітації фактор-множин: задається відношення еквівалентності; функції, що зберігають це відношення; далі можна підставляти в термах еквівалентні (за вищезазначеною відношенню) значення
  • Інтегровані класи типів (в стилі Haskell , починаючи з версії 8.2)
  • Program і Russel для створення верифікованих програм з не верифікованих[6]

Див. також

Підручники:

Джерела
  1. Coq 8.10.2 is out. 29 листопада 2019.
  2. Release Coq 8.15.0 — 2022.
  3. Adam Chlipala. Library Universes (англ.).
  4. Manual, 2009, «Building a toplevel extended with user tactics».
  5. Manual, 2009, «The tactic language».
  6. Manual, 2009, «Program».
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.