Вікіпедія

Coq

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

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

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

ред.

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 можна відзначити:[джерело?]

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

ред.

Жорж Гонтье (з 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».
    • Неявне приведення типів, або спадкування
  • Автоматичне виведення типів
  • Виведення значень аргументів з типів
  • Тактики можна писати на:
    • Мові програмування 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. Архів оригіналу за 31 грудня 2019. Процитовано 30 листопада 2019.
  2. ↑ Adam Chlipala. Library Universes (англ.). Архів оригіналу за 2 січня 2014. Процитовано 3 грудня 2019.
  3. ↑ Hartnett, Kevin (19 травня 2015). Will Computers Redefine the Roots of Math?. Quanta Magazine.
  4. ↑ Manual, 2009, «Building a toplevel extended with user tactics».
  5. ↑ Manual, 2009, «The tactic language».
  6. ↑ Manual, 2009, «Program».
Отримано з https://uk.wikipedia.org/w/index.php?title=Coq&oldid=40586966