LINUX.ORG.RU

Coq 8.9

 , , , ,


3

3

Состоялся релиз Coq 8.9. Его разработка заняла 7 месяцев с момента выпуска Coq 8.8. Этот релиз является результатом ≈2000 коммитов и ≈500 pull request’ов.

Coq — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования с зависимыми типами.

Особенностью Coq является широкое использование тактик для построения доказательств, в отличие от таких систем, как Agda или Idris.

Основные изменения в этой версии:

  • Поддержка взаимно рекурсивных record’ов (Pierre-Marie Pédrot).
  • Добавлена команда Numeral Notation для перегрузки десятичных чисел сторонними типами (Daniel de Rauglaudre, Pierre Letouzey и Jason Gross).
  • { теперь поддерживает именованные цели, например [x]:{ (Théo Zimmermann).
  • Удалены команды Arguments Scope и Implicit Arguments.
  • coqtop и coqide теперь могут подсвечивать разницу в шагах доказательства, используя команду Diffs.
  • Изменения в стандартной библиотеке: в библиотеках VectorDef, Ascii, String.
  • Удалена утилита gallina.
  • Многочисленные исправления в новой документации, основанной на Sphinx.

>>> Подробности

Ответ на: комментарий от JSha

В данном случае — на все сто процентов.

Потому что Coq не нацеливается на автоматическую генерацию доказательств, а на проверку корректности доказательств.

Да, есть тактики, которые могут автоматически доказывать узкий круг теорем; но термы, сгенерированные ими, проходят проверку типов в ядре отдельно, поэтому сломанная тактика не позволит нам построить элемент пустого типа.

Guest_1488 ()
Ответ на: комментарий от Guest_1488

Непонятно зачем это нужно? Я читал, что сейчас все настолько сложно, что доказательсво Перельмана понимает несколько человек во всем мире, как это можно доказывать корректность при помощи компьютера? Про какие теоремы идет речь?

JSha ()
Ответ на: комментарий от JSha

Собери Hello World на С++. А потом задай вопрос в чью голову могут вместиться все ассемблерные инструкции которые сгенерировал компилятор. Таких людей нет. Компьютеры что-то делают лучше, а именно следуют фиксированным наборам правил. Доказательства - один из таких алгоритмов

vertexua ★★★☆☆ ()
Последнее исправление: vertexua (всего исправлений: 1)
Ответ на: комментарий от JSha

Непонятно зачем это нужно?

А зачем нужно верифицировать ПО вообще?

Я читал, что сейчас все настолько сложно, что доказательсво Перельмана понимает несколько человек во всем мире, как это можно доказывать корректность при помощи компьютера?

У нас имеется соответствие между логикой и теорией типов, поэтому если терм проходит проверку типов — теорема доказана.

Про какие теоремы идет речь?

Которые сможешь сформулировать.

Guest_1488 ()
Ответ на: комментарий от vertexua

Доказательства - один из таких алгоритмов

Сначала нужно доказать существование такого алгоритма, или он у тебя универсальный на все случае жизни?

Взять для примера игру «жизнь», существует ли алгоритм, распознающий по произвольной позиции игры «вымрет» ли она? Ведь до сих пор не решена, не говоря уже о более сложных вещах типа P=NP.

JSha ()
Ответ на: комментарий от JSha

Взять для примера игру «жизнь», существует ли алгоритм, распознающий по произвольной позиции игры «вымрет» ли она?

Нет. Игра «жизнь» - Тьюринг-полная, а одно из основных свойств Тьюринг-полных систем - невозможность достоверно определить конечность исчисления. (Любители матана и прочие CS, поправьте меня если туплю).

balsoft ()
Ответ на: комментарий от JSha

Все клетки станут пустыми.

Просто прогнать симуляцию пока ситуация не стабилизируется. Впрочем в Жизни много осцилляторов и гораздо вероятнее что несколько из них сформируется. Можешь прогнать в любом жизнёвом автомате рандомный паттерн и увидишь как он стабилизируется очень быстро превратившись в суп из осцилляторов

Xenius ★★★★★ ()
Ответ на: комментарий от Xenius

пока ситуация не стабилизируется

Она может никогда не стабилизироваться. Не любое состояние сводится к циклу состояний, иногда они бесконечно меняются (простейший glider тому пример).

balsoft ()
Ответ на: комментарий от balsoft

невозможность достоверно определить конечность исчисления

Тем самым автоматически доказывается отсутствие такого алгоритма. Но тем не менее эта задача присутствует в перечне открытых математических проблем 21 века.

JSha ()

Неужто с новостями все так стало туго, что каждый шлак подтверждаем ?

Уж лучше бы про NomadBSD написали, там хоть можно грабить корованы запуститься в лайв-режиме с флешки.

windows10 ()
Ответ на: комментарий от Xenius

Это ничего не доказывает. Вопрос в самой принципиальной возможности по начальному состоянию доказать наступление указанного состояния.

Например возьмем опытного электронщика. Он смотрит на схему и даже не включая ее говорит «работать не будет». Значит у него в голове существует алгоритм, позволяющий прийти к такому выводу.

JSha ()
Ответ на: комментарий от JSha

Он смотрит на схему и даже не включая ее говорит «работать не будет». Значит у него в голове существует алгоритм, позволяющий прийти к такому выводу.

Только вот даже самые опытные электронщики ошибаются. Я почти уверен, что можно довести алгоритм определения до точности 99% на случайных полях, но ты же просишь 100%.

balsoft ()
Ответ на: комментарий от windows10

каждый шлак

интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования с зависимыми типами.

дружище, поди яги попей или рэпчик послушай, не для тебя здесь новости и не для таких как ты.

Alve ★★★★★ ()
Ответ на: комментарий от JSha

Не нужно мыслить задачами или, тем более, баззвордами. Математика — это исследовательские программы и теории внутри них, а только потом задачи.

Вещи вроде Coq могут в перспективе сильно облегчить жизнь. Например, построил ты свою теорию для вещественных чисел и начинаешь думать, а какие свойства этих чисел можно выкинуть так, что твоя теория останется в силе. Приблизительно как дженерики в программировании (ну это если совсем на пальцах). Вручную — это годы бесполезного пердолинга с кучей шансов на ошибку.

buddhist ★★★★★ ()

А кто докажет что сама Coq 8.9 работает правильно и без глюков ? Кто проверяет проверяющего ? ))) Зная качество современного ПО что то терзают большие сомнения на этот счет

anonymous ()
Ответ на: комментарий от JSha

Ну вот coq как раз такая штука, которая отвечает на вопрос, верно ли доказательство, составленное какимто умником, без необходимости самому вникать в это доказательство. Проблема в том, что доказательство должно быть приведено к соответсвующему виду, который петух сможет склевать, что на практике означает, что математик обязан изначально узать coq при составлении своего доказательства. Плюс еще постановка задачи может быть неправильной, если речь идёт например о разработке языков программирования. Ну для всяких там математических головоломок аля теорема Ферма - вещь неоценимая.

q0tw4 ★★★ ()
Ответ на: комментарий от JSha

Сначала нужно доказать существование такого алгоритма, или он у тебя универсальный на все случае жизни?

Уже доказано: тайпчекинг для calculus of constructions разрешим. Term finding вот неразрешим, это да.

Иными словами, проверить доказательство можно алгоритмически, найти доказательство (или опровержение) произвольного утверждения — нет.

anonymous ()
Ответ на: комментарий от anonymous

тайпчекинг для calculus of constructions разрешим

Это что значит все хаскельные потуги с расширением SystemF - пустая трата времени и надо было сразу DT-haskell пилить? А то плакались, что в DT тайпчек может повиснуть, так что продолжаем добавлять разнообразные костыли ради подражания DT языкам.

q0tw4 ★★★ ()
Ответ на: комментарий от q0tw4

А в хаскеле не System F.

В λC нет рекурсивных функций (fix нетипизируем, его надо вводить как примитив), например, а в хаскеле (и в прочих идрисах) они есть, откуда и вылезают все проблемы.

anonymous ()
Ответ на: комментарий от anonymous

Ну там проблемы начинаются еще из Type: Type, что жутко удобно на практике. Кстати, а кто нибуть пробовал разработать Dependent types with subtyping? А то как-то нудно все везде руками передавать и конвертить.

q0tw4 ★★★ ()
Ответ на: комментарий от anonymous

Там эта тьюринг-(не)полнота по-другому работает.

fix есть, и рекурсивные определения тоже есть. Даже для тотальных функций (тоталити чекер там через абсолютно тупую проверку уменьшения синтаксического размера работает, если не залезать в well-founded и вот это всё).

anonymous ()
Ответ на: комментарий от te111011010

Так на это и расчёт типа: Петуховены , а вы видели систему будущего котррую опять своруют корпо пораши и выдадут очередной пирует что это что то новое и сделали это именно они всей своей корпо порашей , все делается что бы НН платить истенному создателю который типа васян , так что надежда что эти корпо пораши как то вычисляли и были такие институты вычисления ведь не могут же корпо пораши получать за то что они творчески так сказать не изрбрели

anonymous ()
Ответ на: комментарий от anonymous

Про синтаксический размер слышал. А есть другие способы проверки терминируемости?

И есть ли класс функций, про которые известно, что они всегда завершаются на всех допустимых значениях аргументов, но не выразимы (т.е. не проходят проверку тоталити чекера) в Idris/Agda/Coq/etc?

anonymous ()
Ответ на: комментарий от anonymous

Ну примером такой функции может стать известная задачка 3n + 1, если гипотеза верна. Ну даже если и не она, то вроде как доказано существование верных, но не доказуемых в рамках конкретного исчисления утверждений, правда в детали я не вдавался, так что может быть неправильно понял.

q0tw4 ★★★ ()