Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

Coq фр coq півень інтерактивний програмний засіб доведення теорем використовує власну мову функціонального програмування

Coq

Coq

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

Coq (software)
image
image
Тип
Розробник The Coq development team
Перший випуск 1 травня, 1989; 35 років тому (1989-05-01) (version 4.10)
Стабільний випуск 8.10.2 (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 році асоціація обчислювальної техніки нагородила Тьєррі Кокана, Жерар П'єр Хуета, Крістін Пауліна-Морінга, Бруно Барраса та інших премією за Coq.

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

Coq дозволяє:

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

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

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

Використання

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

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

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

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

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

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

Інше

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

Інструменти

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

Див. також

Посилання

  • 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.] від Андрея Бауера

Джерела

  1. . 29 листопада 2019. Архів оригіналу за 31 грудня 2019. Процитовано 30 листопада 2019.
  2. Adam Chlipala. (англ.). Архів оригіналу за 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».

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

Coq fr coq piven interaktivnij programnij zasib dovedennya teorem vikoristovuye vlasnu movu funkcionalnogo programuvannya Gallina z zalezhnimi tipami Dozvolyaye zapisuvati matematichni teoremi i yihni dovedennya pochinayuchi z cili gipotezi yaku potribno dovesti Coq mozhe avtomatichno znahoditi dovedennya v deyakih obmezhenih teoriyah za dopomogoyu taktik Coq vikoristovuyetsya dlya verifikaciyi program Coq software TipRozrobnik The Coq development teamPershij vipusk 1 travnya 1989 35 rokiv tomu 1989 05 01 version 4 10 Stabilnij vipusk 8 10 2 29 listopada 2019 4 roki tomu 2019 11 29 Platforma krosplatformova programaOperacijna sistema Cross platformMova programuvannya OCamlDostupni movi EnglishLicenziya LGPLv2 1Repozitorij github com coq coqVebsajt coq inria fr Mediafajli u VikishovishiIstoriya rozrobkiCoq rozroblenij u Franciyi v ramkah proektu TypiCal ranishe LogiCal spilno keruyetsya INRIA 26 lyutogo 2009 u Wayback Machine Politehnichnoyu shkoloyu Universitetom Parizh Pivden XI i Nacionalnim centrom naukovih doslidzhen ranishe bula vidilena grupa i v Teoretichnoyu bazoyu Coq ye chislennya konstrukcij a nazva ce abreviatura CoC angl calculus of constructions i skorochennya prizvisha tvorcya obchislennya U 2013 roci asociaciya obchislyuvalnoyi tehniki nagorodila Tyerri Kokana Zherar P yer Hueta Kristin Paulina Moringa Bruno Barrasa ta inshih premiyeyu za Coq Osoblivosti programnogo zabezpechennyaCoq dozvolyaye manipulyuvati tverdzhennyami obchislennya mehanichno pereviryati dokazi cih tverdzhen spriyati poshuku formalnih doveden sintezuvati sertifikovani programi na osnovi konstruktivnogo pidtverdzhennya yih specifikacij Neshodavno koli Coq udoskonalili vse bilshimi mozhlivostyami avtomatizaciyi Do nih nalezhit taktika Omega yaka viznachaye arifmetiku Presburgera Ce bezkoshtovne programne zabezpechennya yake rozpovsyudzhuyetsya na umovah licenziyi GNU LGPL VikoristannyaSered velikih uspihiv Coq mozhna vidznachiti dzherelo Problema chotiroh farb bula povnistyu mehanizovana demonstraciya bula zavershena v 2005 roci ta Sistema neperetinnih mnozhin dokaz korektnosti u Coq buv opublikovanij u 2007 roci dokaz teoremi buv zavershenij ta jogo komandoyu u veresni 2012 roku kompilyator optimizovanij dlya movi programuvannya C yakij znachnoyu miroyu zaprogramovanij ta perevirenij u Coq Problema chotiroh farb ta rozshirennya Ssreflect Zhorzh Gonte z Microsoft Research v Kembridzhi Angliya i Bendzhamin Verner z INRIA vikoristovuyuchi Coq doveli teoremu pro Problemu chotiroh farb Na osnovi ciyeyi roboti bulo rozrobleno znachne rozshirennya Coq pid nazvoyu Ssreflect sho oznachaye vidobrazhennya v malih masshtabah Bilshist novih funkcij dodanih v Ssreflect ye zagalnoprijnyatimi funkciyami korisnimi ne prosto dlya stilyu obchislyuvalnogo vidobrazhennya dovedennya Do nih nalezhat Dodatkovi zruchni poznachennya dlya nesprostovnogo ta sprostovuvanogo na z odnim abo dvoma konstruktorami Neyavni argumenti dlya funkcij zastosovanih do nulovih argumentiv sho korisno pri programuvanni z funkciyami vishogo poryadku Stisli anonimni argumenti Vdoskonalena settaktika z bilsh potuzhnim uzgodzhennyam Pidtrimka rozdumiv Ssreflect 1 4 ye u vilnomu dostupi z podvijnoyu licenziyeyu za licenziyeyu abo CeCILL 2 0 z vidkritim kodom ta sumisnij z Coq 8 4 Inshe Do koristuvachiv sistemi Coq nalezhav Volodimir Voyevodskij laureat medali Fildsa InstrumentiMova realizaciyi OCaml i Si Licenziya GNU Lesser General Public Licence Version 2 1 Seredovisha rozrobki Kompilyator coqc i instrumenti dlya roboti z proektami sho skladayutsya z bezlichi fajliv coqtop konsolna interaktivne seredovishe Seredovisha rozrobki z grafichnim interfejsom koristuvacha CoqIDE Eclipse Proof General Rezhim dlya Emacs coqdoc generator dokumentaciyi do bibliotek vihid v LaTeX i HTML Eksport dokaziv v XML dlya proektiv HELM1 i MoWGLI Konstruktivna matematika vidoma tim sho z dokaziv isnuvannya velichini mozhna ekstraguvati algoritm otrimannya ciyeyi velichini Coq mozhe eksportuvati algoritmi v movi ML i Haskell Znachennya yaki mayut tip sho nalezhit do sortu Prop ne ekstraguyutsya zazvichaj ci znachennya ye dovedennyam Coq mozhna rozshiryuvati ne pogirshuyuchi nadijnosti Korektnist perevirki dokaziv zalezhit vid proof checker yakij ye nevelikoyu chastinoyu vid usogo proektu Vin pereviryaye dokazi zgenerovani taktikami tomu nekorektna taktika ne prizvodit do prijnyattya dovedennya z pomilkoyu Takim chinom Coq sliduye Osoblivosti moviKoristuvach mozhe vvoditi vlasni aksiomi Zasnovanij na predikativnomu obchislenni do induktivnih konstrukcij sho oznachaye Vsi mozhlivosti chislennya konstrukcij Kumulyativna iyerarhiya universumiv sho skladayetsya z Prop Set i mnozhini Type indeksovanoyi naturalnimi chislami Prop impredikativnij Set i Type predikativni Induktivni abo algebrichni tipi danih Koinduktivni tipi danih Mozhlivo zadati tilki chastkovo rekursivni funkciyi tobto taki funkciyi obchislennya yakih zupinyayetsya tobto ne zaciklyuyetsya U Coq mozhna zapisati funkciyu Akkermana Zupinka rekursiyi po induktivnim tipam danih takim yak naturalni chisla i spiski garantuyetsya sintaksichnoyu perevirkoyu viznachennya funkciyi tak zvanoyu guarded by destructors Zupinka funkcij yaki vikoristovuyut zistavlennya zi zrazkom koinduktivnih tipiv garantuyetsya umovoyu guarded by contructors Neyavne privedennya tipiv abo spadkuvannya Avtomatichne vivedennya tipiv Vivedennya znachen argumentiv z tipiv Taktiki mozhna pisati na Movi programuvannya ML Specialnij movi dlya taktik Ltac Coq vikoristovuyuchi taktiku quote Maye velikij nabir primitivnih taktik napriklad intro elim i menshij nabir rozvinenih taktik dlya specifichnih teorij napriklad field dlya polya omega dlya arifmetiki Presburger Taktiki grupi setoid dlya imitaciyi faktor mnozhin zadayetsya vidnoshennya ekvivalentnosti funkciyi sho zberigayut ce vidnoshennya dali mozhna pidstavlyati v termah ekvivalentni za vishezaznachenoyu vidnoshennyu znachennya Integrovani klasi tipiv v stili Haskell pochinayuchi z versiyi 8 2 Program i Russel dlya stvorennya verifikovanih program z ne verifikovanihDiv takozhLeanPosilannyaThe Coq proof assistant 25 serpnya 2004 u Wayback Machine oficijnij anglijskij vebsajt coq coq 31 grudnya 2019 u Wayback Machine shovishe kodu na GitHub JsCoq Interactive Online System 14 zhovtnya 2019 u Wayback Machine dozvolyaye zapuskati Coq u vebbrauzeri bez neobhidnosti bud yakoyi instalyaciyi programnogo zabezpechennya Coq Wiki 24 grudnya 2019 u Wayback Machine Mathematical Components library 21 listopada 2019 u Wayback Machine shiroko vikoristovuvana biblioteka matematichnih struktur chastinoyu yakoyi ye mova Ssreflect Constructive Coq Repository at Nijmegen 2 zhovtnya 2011 u Wayback Machine Math Classes 1 sichnya 2019 u Wayback Machine Pidruchniki The Coq Art 24 veresnya 2019 u Wayback Machine kniga pro Coq Iva Bertota ta P yera Kasterana Certified Programming with Dependent Types 9 veresnya 2011 u Wayback Machine onlajn ta drukovanij pidruchnik Adama Chlipala Software Foundations 9 listopada 2013 u Wayback Machine onlajn pidruchnik Bendzhamina K Pirsa ta in An introduction to small scale reflection in Coq 23 lyutogo 2020 u Wayback Machine navchalnij posibnik z SSreflect Zhorzha Gontye ta Assia Mahbubi Introduction to the Coq Proof Assistant 4 grudnya 2019 u Wayback Machine video lekciya Endryu Apelya v Instituti pidvishennya kvalifikaciyi Video tutorials for the Coq proof assistant 4 grudnya 2019 u Wayback Machine vid Andreya BaueraDzherela 29 listopada 2019 Arhiv originalu za 31 grudnya 2019 Procitovano 30 listopada 2019 Adam Chlipala angl Arhiv originalu za 2 sichnya 2014 Procitovano 3 grudnya 2019 Hartnett Kevin 19 travnya 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

Дата публікації:
Топ