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

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

[ред. | ред. код]

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

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

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

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

До користувачів системи Coq належав Володимир Воєводський, лауреат медалі Філдса.[3]

Інструменти

[ред. | ред. код]
  • 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».