Coq 8.9

Сложная штука

Очень большой философский вопрос, насколько можно доверять доказательству теоремы, сделанному машиной?

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

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

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

man продукционные системы Поста

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

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

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

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

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

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

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

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

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

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

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

А что ты понимаешь под «вымрет»?

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

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

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

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

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

Юзает кто? Расскажите, для каких задач используете?

Посоны, Мочидзуку ещё не coq-нули? Он всех задрал! Или это СЛОЖНА пока исчо?

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

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

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

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

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

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

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

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

Проблема остановки неразрешима на машине Тьюринга, доказано Тьюрингом в 37 году.

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

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

Значит я всё-таки прав. Ок, не всё ещё забыл.

«Открытые математические проблемы»

Источник: https://intellect.ml/otkrytye-matematicheskie-problemy-884

Ищем слово «Жизнь».

каждый шлак

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

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

Старый, видимо, список, т.к. конкретно про «жизнь» (точнее, правило 110), есть доказательство тьюринг-полноты.

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

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

Существуют-таки на этой планете люди, которые занимаются чем-то полезным.

А где можно посмотреть примеры использования? Желательно на русском языке.

Вот, на Coq’е.

http://cosette.cs.washington.edu/

https://github.com/uwdb/Cosette

https://github.com/uwdb/Cosette/blob/master/hott/library/UnivalentSemantics.v

Univalent Foundations https://github.com/UniMath

Основаны на работах Воеводского.

Тогда уже сразу https://github.com/HoTT/HoTT.

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

Для этого руководствуются «принципом де Брёйна» и делают само ядро прувера как можно более простым.

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

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

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

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

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

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

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

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

Удалена утилита gallina

Бедную курицу пустили на суп. Галина бланка буль буль...

Там проверять необходимо только тайпчекер, что не такая сложная задача.

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

и в прочих идрисах

В (дефолтном) идрисе разве есть fix? Он же не Тюринг-полный с дефолтными проверками

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

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

А есть ли у этого Coq свой CoC?

Есть

Coq — это ведь петух по-французски. Там случайно нет компонента «Lait concentré»?

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

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

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

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

Чем оно лучше Mizar?

А у Mizar гарантирована завершимость, кстати?

все, генерируют перегной, что может быть полезнее?