Тред успешных хлебателей борщей.Coq:https://coq.inria.fr/Lean:http://leanprover.github.io/Agda:https://github.com/agda/agdaHoTT:https://github.com/HoTT/HoTThttps://github.com/HoTT/HoTT-Agdahttps://github.com/gebner/hott3По теме: http://groupoid.space/.Cubical Type Theory:https://github.com/mortberg/cubicaltthttps://github.com/mortberg/yacctthttps://github.com/RedPRL/redtthttps://github.com/redprl/sml-redprlhttps://github.com/JetBrains/ArendНу и agda --cubical (недавно релизнулась 2.6.0, кубики ушли в релиз).По теме: http://cubical.systems/
>>1382928 (OP)Перед тем, как заходить в этот тред, надо включать мозг. Те, кто этого не делают, будут посланы нахуй быстрее, чем они успеют сказать "не понял".
>>1384999ОК, добавлю от себя рандомных ссылок по теме:https://github.com/jwiegley/category-theoryhttps://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.htmlhttp://www.karlin.mff.cuni.cz/~stanovsk/math/qptp.pdfhttps://arxiv.org/pdf/1811.00796.pdfhttps://github.com/moonad/Formality
В чём прикол интуиционистской логики? Ну откусили мы аксиому одну, ну и что? Стало только хуже ведь. Думал может она разрешима, так нихуя, так же алгоритмически неразрешима, как и обычная. Тогда в чём её преимущество в пруверстве? Извиняюсь за косноязычие, я не тупой, я ебанутый.
>>1399127>Ну откусили мы аксиому одну, ну и что? Стало только хуже ведь.Чего там тебе откусили, что ты правило вывода от аксиомы не отличаешь? Исключенное третье конструктивно доказуемо, хотя теорему Дьяконеску ты все равно не осилишь. Аксиома выбора в MLTT так же доказуемая теорема, а не заповедь.
>>1399303> Как доказать корректность сишного компилятора?Гугл -> CompCert, Verifiable Software Toolchain, deepspec.
>>1399303А, ещё есть книшка PLCC, Program Logic for Certified Compilers, Изумительная книга. Великая книга. Вы не понимаете ее потому, что у вас времени нет. А у меня было много времени, я читала по пять часов в день и прочла шесть раз. Сначала у меня тоже было такое чувство, будто я не понимаю, а потом все постепенно проступало, — знаете, как фотография, которую проявляют. Хемингуэй, Дос Пассос вышли из него. Они все питаются крохами с его стола.
>>1399344>Собрание колхоза. Председатель берет слово: - Товарищи! На повестке дня два вопроса - постройка сарая и постройка коммунизма. В связи с отсутствием досок предлагаю сразу перейти ко второму вопросу.Это я к тому, что они дрочат на верификацию компилятора, а верифицировать используемый им ассемблер даже не начинали.
>>1399485> верифицировать используемый им ассемблер даже не начинали.Ну раз тыскозал, значит так и есть, да? В компсерте верифицированы все промежуточные языки, в том числе ассемблер. В VST помимо прочего имеется MSL - готовое решение для separation logic, не привязанное ни к какому языку, с помощью неё можно верифицировать что угодно, если осилишь представление этого чего угодно в виде набора инструкций, пре и посткондишенов. Все инструменты для верификации есть + прогресс не стоит на месте, я упомянул деятелей, которые плотно занимаются этим вопросом - deepspec.
>>1399183Чегой-то я не отличаю? Всё я отличаю, исключённое третье это аксиома, а не правило вывода. Не агрись. плез, лучше расскажи в чём суть юзать интуиционистскую логику заместо обычной.>Исключенное третье конструктивно доказуемоНу бля, A(ну или -A) -> (A v -A), это-то понятно, но для этого надо доказать A или -A, в обычной логике же нихуя не нужно доказывать, значит формулы по типу --A -> A и тд невыводимы будут, то бишь множество выводимых формул интуиционистской логики подмножество множества выводимых формул обычной, так получается(откусили кусок).
>>1399352в чем основные трудности для понимания? алсо, там только теория, или есть практические примеры?
>>1399971> в чем основные трудности для понимания? От бэкграунда зависит. Как по мне, separation logic именно с практической стороны довольно сложная тема, теоретически общий смысл ясен, но конкретные примеры обычно полный пиздец, там помимо кока ещё С знать надо, все примеры ж на нем. > алсо, там только теория, или есть практические примеры?И то и то. VST это вполне практический проект.
>>1399615>все промежуточные языки, в том числе ассемблерКакие нахуй языки? Программа-ассемблер, часть тулчейна, которая после компоновки используется для генерации машинного кода. Доказана для нее корректность? Нет, не доказана:>http://compcert.inria.fr/compcert-C.html>Part 3: Assembling and linking. The abstract syntax tree for PowerPC or ARM or RISC-V or x86 assembly language produced by part 2 is printed in concrete assembly syntax. The system's assembler and linker are then called to produce object files and executable files, respectively. This part is not yet formally verified. A benefit of using the standard assembler and linker is that object files produced by CompCert can be linked with existing libraries compiled with gcc. This is convenient for testing, although the formal guarantees of semantic preservation apply only to whole programs that have been compiled as a whole by CompCert C.>можно верифицировать что угодно>GNU/Car.jpgТак возьми и верифицируй, а потом кукарекай, что есть формально корректный тулчейн.
>>1399183>теорему Дьяконеску ты все равно не осилишь.Чегой-то не осилю, всё я осилил.https://en.wikipedia.org/wiki/Diaconescu%27s_theoremТут получается, что(A v -A) -> (P -> P), где A это f(U) = f(V) и типа в обычной логике A v -A аксиома, а в необычной у нас по построению либо A либо -A будет верным в завимимости от предиката P.
>>1399183Ну так что, объяснишь вот этот момент?>Despite the serious challenges presented by the inability to utilize the valuable rules of excluded middle and double negation elimination, intuitionistic logic has practical use. One reason for this is that its restrictions produce proofs that have the existence property, making it also suitable for other forms of mathematical constructivism. Informally, this means that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object, a principle known as the Curry–Howard correspondence between proofs and algorithms. One reason that this particular aspect of intuitionistic logic is so valuable is that it enables practitioners to utilize a wide range of computerized tools, known as proof assistants. Почему это так? Что такого даёт это the existence property, что it enables practitioners to utilize a wide range of computerized tools, known as proof assistants. ??
>>1401369> Почему это так? Что такого даёт это the existence property, что it enables practitioners to utilize a wide range of computerized tools, known as proof assistants. ??Ну это ж азы. Конструктивная логика оперирует пруф-обьектами вместо аксиом. Классически исключенное третье истинно безотносительно того, можем ли мы доказать "А" или "не А". Конструктивно же мы должны доказать А или не А, как в теореме Дьяконеску. И вот это доказательство, построение, согласно изоморфизму Карри-Говарда, представляет собой готовый алгоритм. Если быть точнее, тут скорее речь об интерпретации логических констант по Брауэру-Гейтингу-Колмогорову, что позволяет использовать пруф-обьекты как программы.
>>1401389То есть если бы пруверы основывались на классической логике, то некоторые доказуемые утверждения о существовании нельзя было бы алгоритмически выразить, в интуиционистской же логике любому доказательству существования соответствует некоторый алгоритм и, и что? Почему это даёт возможность utilize a wide range of computerized tools? Ааа, так-так, погоди, смысл такой, что пользуясь классической логикой мы гораздо меньше можем переложить на вычислительную машину, а конструктивная даёт нам возможность использовать мощи компа на максимум, так что ли?
>>1401389>интерпретации логических констант по Брауэру-Гейтингу-КолмогоровуЭто типа А истинно тогда и только тогда, когда существует хотя бы одна выполняющая его функция?
>>1401414Ты в правильном направлении мыслишь, однако разница между классической и конструктивной логикой фундаментальнее. Я о разнице в понятии существования математического объекта. Классически существование обьекта это его непротиворечивость в заданной аксиоматике (ZFC, например), конструктивно существование это вычислимость.
>>1401414Аааа, или даже не так, так как доказательство <=> алгоритму то мы можем для доказательства не только исчисление логическое юзать, а любой язык программирования! С циклами, хуиклами, классами и тд, если в ходе работы программы получится объект то сам алгоритм и будет доказательством! Воо!>>1401423А соответствие Карри-Говарда говорит вообще про любое конструктивное доказательство <=> некоторому алгоритму или только про доказательство существования?
>>1401418> Это типа А истинно тогда и только тогда, когда существует хотя бы одна выполняющая его функция?А истинно если есть хотя бы один пруф-обьект, удовлетворяющий А, т.е если множество А не пусто. Т.е a:A, где a - пруф-обьект, элемент множества А. В зависимости от того, что есть А (это может быть любой тип, в т.ч стрелочный любой сложности), a так же может быть чем угодно, в т.ч функцией.
>>1401432Ну да, я понял, под функцией я имел нечто, принимающее на вход что-то, перемалывающее и выплёвывающее x, для которого A(x). Да короче соответствие Карри-Говарда каждому понятию логики ставит в соответствие понятие из вычислимости, так что накодив прогу ты автоматически написал конструктивное доказательство, осталось лишь как со словарём это перевести на язык логики, лол. Мощно.
>>1401429> так как доказательство <=> алгоритму то мы можем для доказательства не только исчисление логическое юзать, а любой язык программирования! С циклами, хуиклами, классами и тд, если в ходе работы программы получится объект то сам алгоритм и будет доказательством! Воо!Ну да, интерпретация по Колмогорову как раз об этом. Логические константы могут быть программами. > А соответствие Карри-Говарда говорит вообще про любое конструктивное доказательство <=> некоторому алгоритму или только про доказательство существования?Это одно и то же. Потому и соответствие, что любое конструктивное доказательство это и существование пруф-обьекта и соответствующий этому объекту алгоритм.
>>1401434>понятие из вычислимостиНу я не шарю в этом, как назвать, вычислимость, программирование, типы там, функции, компьютер сайнс короче.>>1401436 И в итоге получается, опуская чисто вкусовщину на то, правомерно ли искл третье, что с классической логикой ты можешь только с бумажкой, ручкой или примитивным подставляльщиком текста вместо текста бибу сосать, а с интуиционистской можешь использовать всю мощь компьютер сайнс. Нихуёво. Спасибо.
>>1401437Соответствие между языками программирования и конструктивной логикой более прямое и плотное, чем кажется. По Барендрегту 8 лямбда-исчислений а-ля Черч это то же самое что 8 конструктивных логик (например, простая типизированная лямбда соответствует конструктивному исчислению высказываний, proposition calculus итд). Самая упакованная из таких логик - CoC, calculus of construction - основа Coq'а. Поэтому на коке можно верифицировать вообще все, что можно наговнокодить на любом ЯП, даже несуществующем в настоящее время, т.к. любой ЯП представим в виде лямбда-исчисления.
>>1401454Да, ординал судя по всему, Predw это Higher order predicate calculus, а что значит weak, ну которые с чёрточкой внизу? Добавляются предикаты "для всех конечных" и "существует конечное число"?
>>1401450Ну меня больше восхищает обратное, что любое наговнокоженное на любом языке представляется в виде алгоритма в некотором лямбда-исчислении подходящего порядка и потом это лёгким движением руки по словарю Карри-Говарда переводится в доказательство в логике этого же порядка. Это охуеть же. Жаль, я не шарю пока в вычислимости, я только теорию множеств, логику высказываний, исчисление высказываний обычное и конструктивное, языки первого порядка и исчисление предикатов прошёл пока что. Дальше вот будет ещё полкниги про основы теории моделей, типа как вот ты научился чему-то общему, инструментам, как кванторы элиминировать, че такое элементарная эквивалентность и элементарной расширение, выразимость невыразимость игра Эйренфохта, Левенгейма-Сколема это про семантику, потом про синтаксис чё как вообще выводить, полнота и корректность, замена переменных, предварённая нормальная форма, сколемовские функции, ну короче синтаксис и семантика, изучил ты её, а теперь применения на конкретных теориях и их моделях и тд. Интересно пиздец. А вычислимость, теорема Гёделя та самая, Тарского, вычислимость, арифмтические множества, машина Тьюринга, Поста, ну кароч вся писечка мякотка она там, в третьей книге, потому если правый куб твой я понял примерно, типа ну понятна разница между исчислением высказываний и предикатов, между первым порядком и вторым, третьим блабла, то левый куб я очень отдалённо понял.Вообще чё я зашёл то сюда>Как мы увидим в разделе 5.4 (теорема Чёрча, c. 191), вопрос овыводимости произвольных формул языка первого порядка неразрешим: не существует алгоритма, который бы по произвольной замкнутой формуле определял бы, выводима она или нет. И я такой ок, потом наткнулся на статью про HoTT, Воеводского, унивалентные основания и тд, думаю бля, а как так, по идее и для интуиционистсской логики это верно ведь должно быть, думаю в чём тогда профит её юзать, а оно вон оно чё оказывается, огромнейший профит. Спасибо короче за всю хуйню, а то у меня обычно проблемы с выражением мыслей нормальным, я чё не спрошу все игнорят, типа даун, а я дурачок немного, но не то чтобы совсем уж даун.
>>1401450>любой ЯП представим в виде лямбда-исчисления.Хуй знает. Лямбда-исчисление и прочие модели основанные на математике используют понятие глобального состояния, чтобы определить «шаг вычисления». Каждый шаг вычисления идет от одного глобального состояния вычислений до следующего. В моделях с глобальным состоянием есть существенное ограничение - в них невозможен неограниченный недетерменизм. С другой стороны, вполне себе существуют модели с неограниченным недетерменизмом (модель акторов, современная CSP).https://en.m.wikipedia.org/wiki/Unbounded_nondeterminismВообще, связь модели акторов и мат.логики достаточно мутная. Например, тезис Роберта Ковальского о том, что «вычисления могут быть сгруппированы по логическим выводам». оказался ложным для одновременных вычислений в модели акторов. При этом он справедлив для некоторых видов параллельных вычислений, например, для лямбда-исчислений, но ни о каком неограниченном недетерменизме там речи не идёт, естественно. Подозреваю, что с CSP там та же проблема, типа, вычислительные шаги параллельных систем программирования логики не следуют дедуктивно из предыдущих шагов.
В прошлом треде была какая-то бешеная чушь про то, что Coq -- это просто мощные юнит-тесты, что анализ завершимости в Coq ненадёжный, так как построен на эвристиках. Там был анализ нескольких пруверов каким-то человеком, который явно их никогда не трогал дольше, чем пару дней, и никто ему даже ничего не возразил. Ну я подумал, что тред скоро умрёт, а вы тут всё ещё живы.Это хорошо, что вам интересны эти вещи: в них действительно можно хорошо развиться. Но мой совет всем, кто тут обитает, -- уходить из этого треда. Здесь туча ложной информации, просто какая-то толпа некомпетентных людей друг перед другом пальцы гнёт. Судить можно хотя бы по обилию терминов, которыми даже настоящие исследователи не пользуются нигде, кроме статей в Википедии. Достаточно почитать какие-нибудь статьи про внутреннее устройство пруверов, чтобы заметить, что там терминология проще, чем в этом треде.Покажу просто несколько примеров совсем отчаянного непонимания происходящего.>>1399183> ты правило вывода от аксиомы не отличаешь?Забавные слова в треде про пруверы! Казалось бы, здесь-то должны понимать, что логика некрасиво решает вопрос индуктивного задания определений и куда элегантнее не разделять аксиомы и правила вывода, а считать аксиомы правилами вывода с пустой посылкой.> Исключенное третье конструктивно доказуемо, хотя теорему Дьяконеску ты все равно не осилишь.Эта теорема выводит исключённое третье из аксиомы выбора, которая сама не является конструктивной.> Аксиома выбора в MLTT так же доказуемая теорема, а не заповедь.Это неправда. Проще всего на примере показать: CIC -- Calculus of Inductive Constructions -- расширяет Мартина-Лёфа, однако в Coq аксиому выбора не вывести, её можно только принять.И вообще весь этот ответ -- не ответ на исходный вопрос.>>1399127Польза конструктивизма в пруверах в редукцируемости. Если не принимать неконструктивные аксиомы, то каждое доказательство -- это алгоритм, который строит свидетельство. Это позволяет свободно взаимозаменять описания программ и доказательств. Например, можно написать доказательство того, что у каждого списка существует отсортированная перестановка, -- и это доказательство, если оно конструктивное, будет алгоритмом сортировки с дополнительными свидетельствами каких-то свойств результата. Перемешивать доказательства и программы вообще очень удобно: городишь какие-то функции, которые высчитывают что-то сложное и возвращают вместе с результатом ещё и доказательство того, что результат корректен, -- а потом экспортируешь код в Haskell и получаешь обычные программы, только ты знаешь, что они работают как надо.При этом некоторые старые пруверы принимают исключённое третье. Это вопрос того, каким образом прувер будет использоваться. На Coq вся эта автоматизация доказательств нужна в основном как раз для доказательства корректности программ (в математике такие многоэтажные доказательства встречаются редко и порицаются, поэтому большинство зрелых математических результатов можно закодировать безо всяких тактик).Польза интуиционизма как логики чуть сложнее. Во-первых, интуиционизм просто легче понять: если рассматривать существование как пару из значения и свидетельства выполнимости предиката на нём, а всеобщность -- как функцию из значения в свидетельство выполнимости предиката на нём, то многие вещи легко понять. Неконструктивные результаты часто нечитаемые, потому что слишком волшебные. Например, существует ли алгоритм, который говорит, встретится ли n последовательных семёрок в числе, которое я загадал? Да: если существует такое N, что в этом числе не более N семёрок подряд, то существует алгоритм вида "return n <= N"; иначе есть сколько угодно семёрок подряд и существует алгоритм "return true". Согласись, это доказательство странное: мы говорим, что алгоритм есть, но не знаем, какой.> Думал может она разрешимаНа всякий случай уточню, что обычная логика высказываний разрешима. Неразрешима логика предикатов.>>1401429>Аааа, или даже не так, так как доказательство <=> алгоритму то мы можем для доказательства не только исчисление логическое юзать, а любой язык программирования! С циклами, хуиклами, классами и тд, если в ходе работы программы получится объект то сам алгоритм и будет доказательством! Воо!Не совсем. Во-первых, любое верное интуиционистски доказательство верно, понятное дело, и классически. Так что если хочешь, доказывай всё через циклы и в классической логике. Другое дело, что только функции, которые гарантированно завершаются на всех входах, могут служить доказательствами. Иначе получается, как, к примеру, в Haskell, чтоf :: Bool -> af b = f (not b)Всё, у нас есть (f True :: a), то есть, по Карри-Говарду, мы населили любой тип.Так что ты не можешь взять свои программы на Хаскелле и говорить, что они что-то доказывают. По крайней мере, пока ты всех не убедишь, что они всегда за конечное время сообщают результат.>>1401437> И в итоге получается, опуская чисто вкусовщину на то, правомерно ли искл третье, что с классической логикой ты можешь только с бумажкой, ручкой или примитивным подставляльщиком текста вместо текста бибу сосать, а с интуиционистской можешь использовать всю мощь компьютер сайнс.К этому ответ выше тоже относится: если в Coq добавить исключённое третье, он не превратится в бумажку с ручкой, там всё ещё можно делать всё то же самое. Только некоторые функции (которые доказательства) не будут редуцироваться. Но в случае с Coq это вообще не так важно, потому что обычно все завершают свои доказательства словом Qed, а не Defined, и тела доказательств всё равно не редуцируются. Так что если ты используешь Qed, то вопрос, принимать ли исключённое третье, -- как раз вкусовщина.>>1401450> Поэтому на коке можно верифицировать вообще все, что можно наговнокодить на любом ЯП, даже несуществующем в настоящее время, т.к. любой ЯП представим в виде лямбда-исчисления. Это вообще какое-то размахивание руками, которое никак не относится ни к чему. Как говорится, it's not even wrong. Да, в Coq можно верифицировать что угодно, потому что в нём можно определить аксиомы Цермело-Франкеля и в их терминах описать всю современную математику, но это никак не относится к тому, где в лямбда-кубе Coq находится. Или можно на Coq задать описание того, как работают машины Тьюринга, и переводить программы в термы, описывающие их.Самая простая проблема в этом посте такая: тут, кажется, подразумевается, что в Coq можно оттранслировать программу из любого языка так, чтобы Coq её мог вычислить. Это неправда: Coq не примет незавершающиеся программы. Более того, в отличие от Agda, он отказывается принимать очень многие программы, про которые очевидно на глаз, что они завершаются.Кажется, человек, который писал этот пост, оперирует какими-то, как ему кажется, "интуитивными" представлениями обо всём этом.Мимо написал свой прувер на кубической теории типов
>>1401957>Мимо написал свой прувер на кубической теории типовСохацький, це тi? Поясни лучше, почему тут https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.RulesForTheStandardSetFormers пишут: Agda has A -> B : Set provided A, B : Set, whereas this is not the case in Martin-Löf's logical framework, ведь у Мартин-Лёфа все точно так же, только вместо типов арности, а вместо стрелки -> соответственно ->>, или я что-то важное упускаю?
>>1401957>Или можно на Coq задать описание того, как работают машины Тьюринга, и переводить программы в термы, описывающие их.>Самая простая проблема в этом посте такая: тут, кажется, подразумевается, что в Coq можно оттранслировать программу из любого языка так, чтобы Coq её мог вычислить. Это неправда: Coq не примет незавершающиеся программы.Ты ж себе противоречишь. Сначала пишешь, что на коке можно сделать универсальную машину Тьюринга (я так тебя понял), а потом - что кок не примет незавершающиеся программы, т.е. он не тьюринг-полный.
>>1401957>Это неправда. Проще всего на примере показать: CIC -- Calculus of Inductive Constructions -- расширяет Мартина-Лёфа, однако в Coq аксиому выбора не вывести, её можно только принять.У конструктухов там свой слабый выбор аля "счетный выбор", мб даже слабее.
>>1401389>изоморфизму Карри-Говарда>интерпретации логических констант по Брауэру-Гейтингу-Колмогоровуо, кейворды в бой пошли
>>1402075Ну есть Actor и различные его варики, и да, он Тьюринг-полный.http://www.cs.unibo.it/~laneve/papers/fullCONCUR2012.pdfВообще, судя по всему, Машина Тьюринга это частный случай модели акторов.
>>1401957>Польза конструктивизма в пруверах в редукцируемости. Если не принимать неконструктивные аксиомы, то каждое доказательство -- это алгоритм, который строит свидетельство. Это позволяет свободно взаимозаменять описания программ и доказательств. Например, можно написать доказательство того, что у каждого списка существует отсортированная перестановка, -- и это доказательство, если оно конструктивное, будет алгоритмом сортировки с дополнительными свидетельствами каких-то свойств результата. Перемешивать доказательства и программы вообще очень удобно: городишь какие-то функции, которые высчитывают что-то сложное и возвращают вместе с результатом ещё и доказательство того, что результат корректен, -- а потом экспортируешь код в Haskell и получаешь обычные программы, только ты знаешь, что они работают как надо.>что с классической логикой ты можешь только с бумажкой, ручкой или примитивным подставляльщиком текста вместо текста бибу сосать, а с интуиционистской можешь использовать всю мощь компьютер сайнс. Нихуёво. Спасибо.Да, спасибо, если пролистаешь тред чуть повыше я уже это понял. Польза интуиционизма как логики мне как раз менее интересна, потому что это вкусовщина, чьи-то интуиции принимают одно и не принимают другое, чьи-то наоборот, интересно было почему именно интуиционистская логика берётся за основу пруверов, чем обусловлен такой выбор, были мысли о разрешимости её, но это неправда же, были другие мысли, почему откусывание исключённого третьего могло бы быть полезно, но ни к чему не пришёл, а всё дело оказалось в изоморфизме Карри-Говарда, ну на этот вопрос исчерпывающий ответ уже дан, думаю.>На всякий случай уточню, что обычная логика высказываний разрешимаНе стоило, я понимаю разницу и конечно про предикатную говорил, так-то я и сам писал прувер для обычной логики высказываний через исчисление секвенций Гейтинга, типа мне потому и было любопытно в чём же профит, ведь так посмотришь почти та же самая хуйня, и при навешивании предикатов точно так же будет неразрешима. А вот нихуя, неразрешима-то она будет, но зато ты можешь всю мощь компа юзать, да и потом любой говнокод будет некоторым доказательством, любой вообще, нужно просто взять словарь Карри-Говарда и посмотреть какое понятие из computer science какому понятию из логики соответствует. Это сильно, очень.
>>1401957>Coq не примет незавершающиеся программы.Тогда я опять не понял, алгоритм? Алгоритм. Любой алгоритм эквивалентен конструктивному доказательству и наоборот. Так ведь? Почему тогда не примет?
>>1401989> Ты ж себе противоречишь. Сначала пишешь, что на коке можно сделать универсальную машину Тьюринга (я так тебя понял), а потом - что кок не примет незавершающиеся программы, т.е. он не тьюринг-полный.Coq -- да, не Тьюринг-полный. Однако Тьюринг-машину задать и верифицировать можно. Нельзя будет взять и потребовать, чтобы Coq вычислил результат работы машины Тьюринга.Дело в том, что есть два способа задать функцию в прувере: либо как раз как вычисляемую им функцию, либо как отношение на аргументах и результате. К примеру, функция, которая уменьшает натуральное число на единицу, может быть записана как вычислимое выражение или как отношение:Definition pred (n : nat) : option nat := match n with | 0 => None | S n' => Some n'end.Inductive isPred : nat -> nat -> Prop := | predS : forall n, isPred n (S n).Разница простая: первую функцию можно вычислить: подаёшь 0 -- она тебе None, подаёшь 10 -- она тебе Some 9. Индуктивное отношение же не даёт тееб возможность сказать: "Кок, а какое число идёт перед 10?" Оно просто определяет, что числа n и n+1 связаны отношением isPred.В этом случае можно, конечно, написать функцию, которая находит нужный экземпляр:Definition pred (n: nat) : n <> 0 -> sig (fun m => isPred m n).destruct n; try contradiction; repeat econstructor.Defined.но в общем случае отношения неразрешимы.Или можно написать, к примеру, сложение. Функция:Fixpoint plus (n m : nat): nat := match n with | 0 => m | S n => S (plus n m)end.Отношение:Inductive plus' : nat -> nat -> nat -> Set := | plus0 : forall m, plus' 0 m m | plusS : forall n m o, plus' n m o -> plus' (S n) m (S o).К примеру, можно построить свидетельство того, что (3, 4, 7) находятся в отношении:Theorem plus'347 : plus' 3 4 7. repeat econstructor.Defined.Print plus'347.( plus'347 = plusS 2 4 6 (plusS 1 4 5 (plusS 0 4 4 (plus0 4))) : plus' 3 4 7 )Или можно доказать, что неправда, что plus' 3 4 8:Theorem not_plus'348 : plus' 3 4 8 -> False.Proof. intro. inversion_clear H. inversion_clear H0. inversion_clear H. inversion_clear H0.Qed.В этот раз тоже можно написать функцию, которая находит `o` такое, что plus' n m o. Но, думаю, мысль уже ясна.И вот как отношение машину Тьюринга в Coq можно определить, а вот как функцию -- нет. Основная мысль в том, что мы можем определить тип для описания состояния машины Тьюринга, а также задать отношение "следует за" на состояниях машины. Всё ещё машину Тьюринга нельзя просимулировать, так что тотальность не нарушена, но доказать всё можно. К примеру, доказать, что "while true { }" не завершается, можно примерно так же, как я выше доказал, что "3 + 4 != 8". Если интересно больше, то можно тут посмотреть:https://softwarefoundations.cis.upenn.edu/plf-current/Hoare.html#lab73>>1401977> только вместо типов арности, а вместо стрелки -> соответственно ->>, или я что-то важное упускаю?Что? Это ну вообще никак не связано.Арность -- это описание того, сколько аргументов принимает функция. Арность не представляется в виде выражения на языке. Мы не можем спросить, какая арность у арности. Взятие арности -- это не оператор. Арность -- это какая-то внешняя по отношению к логической системе конструкция. Нельзя внутри языка написать высказывание про все операторы заданной арности.Здесь же речь об отношениях типизации. В какой вселенной типов находятся функции из натуральных чисел в натуральные числа? Coq говорит, что такие функции тоже находятся в Set:Check (nat -> nat).( nat -> nat : Set )Релевантная часть в книге, на которую ссылка, -- это 7.2.3.>>1401993Ну вроде как это не отменяет того, что тот ответ -- это не ответ на поставленный вопрос.>>1402242> ты можешь всю мощь компа юзать, да и потом любой говнокод будет некоторым доказательством, любой вообщеКажется, ты слишком сильно радуешься. По соответствию Карри-Говарда, типы соответствуют высказываниям, населяющие эти типы термы -- доказательствам. Поэтому почти весь обычный говнокод, который служит каким-то доказательством -- скажем, функция plus : Int -> Int -> Int -- если читать его по соответствию Карри-Говарда, говорит просто, что если существует два целых числа, то существует целое число. Это не сильно полезное высказывание, и функции на Си доказывают только совсем тривиальные утверждения такого же рода, когда доказывают вообще хоть что-то.>>1402246> Любой алгоритм эквивалентен конструктивному доказательству и наоборот. Так ведь?Не так.Вот есть у нас высказывание 2 + 2 = 5. Докажем его.Fixpoint bullshit (n : nat) : 2 + 2 = 5 := bullshit n.Или, может, на псевдо-Си удобнее?(2+2=5) bullshit(int n) { return bullshit(n);}Всё по типам сходится и bullshit 1 имеет тип 2 + 2 = 5, правда? Корректное, казалось бы, доказательство. Когда выполнение bullshit 1 завершится, оно действительно предоставит свидетельство того, что 2 + 2 = 5. Проблема только в том, что такого свидетельства нет и программа не завершится. Но ведь проверка типов не запускает сами функции (кроме как для нормализации при унификации) и не узнает, что здесь всё зависнет. С точки зрения Карри-Говарда, это можно считать доказательством того, что 2+2=5.И вот для того, чтобы абы какое высказывание не считалось правдой, мы запрещаем незавершающиеся программы: иначе можно доказать любое высказывание, аакой тогда смысл во всем этом?
Верификатор x86 на лиспеhttp://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/X86ISA____32-BIT-COMPUTE-MANDATORY-PREFIX-FOR-TWO-BYTE-OPCODE?path=3334/25788/10197/6233/12913/5196
>>1402527>Кажется, ты слишком сильно радуешься. По соответствию Карри-Говарда, типы соответствуют высказываниям, населяющие эти типы термы -- доказательствам. Поэтому почти весь обычный говнокод, который служит каким-то доказательством -- скажем, функция plus : Int -> Int -> Int -- если читать его по соответствию Карри-Говарда, говорит просто, что если существует два целых числа, то существует целое число. Это не сильно полезное высказывание, и функции на Си доказывают только совсем тривиальные утверждения такого же рода, когда доказывают вообще хоть что-то.Ааа, а я-то думал. Но всё равно неплохо.>С точки зрения Карри-Говарда, это можно считать доказательством того, что 2+2=5.С точки зрения логики как это выглядит? Ну само доказательство? Получается мы в ходе бесконечной рекурсии попадаем в ⊥, потом ⊥ -> (T -> (2+2=5)), я правильно понял?
>>1402550>⊥ -> (T -> (2+2=5))Ну типа. Это-то аксиома, потом из ⊥ и аксиомы выводим T -> (2+2=5) и из T и предыдущего выводим (2+2=5). Так?
>>1402550> С точки зрения логики как это выглядит? Ну само доказательство? Получается мы в ходе бесконечной рекурсии попадаем в ⊥, потом ⊥ -> (T -> (2+2=5)), я правильно понял? Тут два ответа.Простой ответ: да, бесконечная рекурсия позволяет выразить дно, а из него следует что угодно.Хаскелль тут все понимают?data Empty -- тип данных без конструкторов, то есть не населённый ничемbottom :: Emptybottom = bottom -- тоже бесконечная рекурсияex_falso :: Empty -> a -- для любого `a` выполняется `⊥ → a`ex_falso e = case e of { } -- для всех способов построить `e` (то есть для нуля) предоставили способ построить свидетельство для высказывания `a`Тогда можно сделать (ex_falso bottom :: 2 + 2 = 5)Сложный ответ: ясно, что в логике не доказать 2 + 2 = 5. Но чтобы понять, почему не работает доказательство, которое мы сейчас построили, надо осознать, как вообще работает соответствие Карри-Говарда.Ты в курсе, как вообще выглядят доказательства в каком-нибудь исчислении высказываний? Ну, деревья вывода? Если да, то происходящее можно так объяснить: по Карри-Говарду бесконечная рекурсия строит дерево вывода, поддерево которого равно самому дереву. То есть дерево типизации bullshit 1 в себя включает как поддерево дерево типизации bullshit 1. А логика такого, ясно, не позволяет. То есть по Карри-Говарду самому доказательству ничего не соответствует.>>1402551⊥ → A -- это действительно аксиома. Если вывели ⊥, получили что угодно. Бесконечная рекурсия даёт ⊥. Всё так.
>>1401957> Там был анализ нескольких пруверов каким-то человеком, который явно их никогда не трогал дольше, чем пару дней, и никто ему даже ничего не возразил.goviaji это ты? Ты ведь про меня, да? Я овердохуя понаписал про кучу пруверов свои первые ощущения от знакомства и подводные с которыми может столкнуться вкатывальщик. Получил в ответ вполне себе нормальный дискач.Одному только тебе хую что то все пекло на ровном месте. И до сих пор не отпустило похоже. Ты какой то опущ жизнью покалеченный.Соглашусь разве что с тем что местные эксперты сосут хуи. Зарекся отписываться в этом гадюшнике, но как же больно смотреть как конструктух взялся за старое и срет неофитам прямо в мозг, аж сердце кровью обливается.
>>1402642Ну как раз вторую часть хорошо поняд, не в курсе про деревья вывода, но в курсе, что вывод это некоторая конечная последовательность формул(которые либо аксиомы, либо получаются из аксиом с помощью правил вывода), видимо это можно представить в виде синтаксического дерева, то есть с бесконечной рекурсией у нас получается счётная последовательность формул, которая по определению выводом не является. Дп, но теперь непонятно, в каком тогда смысле ⊥ выражает бесконечную рекурсию. Ну в смысле пояснение понятно, нооо, непонятно немного как теперь получать какой-то вывод, допустим хочу я получить вывод Int, я должен запустить (ex_falso bottom :: Int)? Но там бесконечная рекурсия при вычислении bottom. или суть в том, что я могу данное значение юзать везде, где юзается Int? Типа эквивалентно в том смысле, что компилится? АаАааа клёёёво!!Prelude> data SomeTypePrelude> :{Prelude| f::SomeType -> IntPrelude| f x = 5Prelude| :}Prelude> f (ex_falso bottom :: SomeType)5Так, ща нужно мысли в кучу собрать, вот эта прога>>1402642>⊥ → A -- это действительно аксиомаНу да, точняк, там же немного другая система связок и аксиом, я имел ввиду -A -> (A -> B), ну да одна суть, просто -A это A -> ⊥ и дальше там всё друг через друга выражается..
>>1402709>вот эта прогаА хотя не, она ничего не даёт по сути, Int ведь и так обитаем. Ну то есть экземпляр-то необитаемого типа построить нельзя, но оно и правильно, потому что истинно ведь ⊥ -> A, а не A, ⊥ ведь невыводимо и вот эта штука (ex_falso bottom :: SomeType) может использоваться везде, где используется ⊥. И даже если А необитаем, ⊥ -> A обитаем для любого A, так получается.И что по итогу: алгоритмы с бесконечной рекурсией записываются выражаются как ⊥, программы, содержащие их конечно могут быть переведены по изоморфизму Карри-Говарда как доказательства, содержащие ⊥, но если мы именно впадаем в эту бесконечную рекурсию, то такая программа будет соответствовать ⊥ и не будет выводима. Coq же имеет проверку, что параметры функции должны уменьшаться на след шаге или типа того и запрещает такие вещи. Ок, то есть не любой говнокод можно перевести в доказательство, а только такой говнокод, который при переводе на язык логики не будет являться невыполнимой формулой, потому что такие формулы невыводимы. А невыполнимая формула это то же самое, что противоречие, а противоречие то же самое, что и бесконечная рекурсия. Получается, что изоморфизм Карри-Говарда применим только к тем программам, которые terminating? Любую terminating программу можно интерпретировать как некоторое конструктивное доказательство?
>>1402720>⊥ -> AНу тока тут Empty -> A, а ⊥ его экземляр, с другой стороны он по идее экземляр любого типа должен быть или я хз.
>>1402642Слушай, анон, а если мы модифицируем определение вывода как некоторой счётной последовательности формул, что получится? Тогда while(true){} уже будет легитимно? И если оно будет легитимно, то оно любая хуета будет выводима? Или нет?
>>1402642>деревья выводаДля обычного исчисления высказываний хотелось бы пример всё же, это что-то вроде того, что получается, когда мы ищем(и не находим) контрпример в Генценовском исчислении секвенций?
>>1402527> Релевантная часть в книге, на которую ссылка, -- это 7.2.3.Там нет параграфа 7.2.3> Арность -- это какая-то внешняя по отношению к логической системе конструкция. Нельзя внутри языка написать высказывание про все операторы заданной арности.> Здесь же речь об отношениях типизации3.6-3.9 в той же книге, где нет 7.2.3.
>>1402792Он банальнейшей хуйни понаписал в общем то, и даже при этом умудрился дристануть немножка. Ничто не мешает написать функцию берущую состояние МТ и возвращающую следующее состояние. Проблема только если мы хотим завернуть эту функцию перехода в цикл "двигать до терминального состояния" поскольку coq пошлет нас нахуй т.к. нельзя наверняка сказать что такое состояние будет вообще достигнуто.Нахуя он в синтаксисе coq написал пример с которым coq его очевидно пошлет нахуй - для меня тоже великая загадка. Горюшко объясняльщики на метр объяснят, на два еще запутают.
>>1403023> Проблема только если мы хотим завернуть эту функцию перехода в цикл "двигать до терминального состояния" поскольку coq пошлет нас нахуй т.к. нельзя наверняка сказать что такое состояние будет вообще достигнуто.Lazy evaluation отменили? Чем-то мне эти ваши описания машины Тьюринга на коке неуловимо напоминают separation logic или хотя бы логику Хоара. Там есть правила вывода в виде циклов while, if-else и что-то кок ничего против не имеет.
>>1403338Не знаю где ты всего этого говна понабрался, но у тебя безнадежная каша в голове, не вижу даже смысла дискутировать.
>>1402701> Я овердохуя понаписал про кучу пруверов свои первые ощущения от знакомства и подводные с которыми может столкнуться вкатывальщик.Я ничего не имею против тебя: хорошо, что ты рассказываешь о том, что узнаёшь. Это был просто пример того, что тут тред не очень содержательный: если бы это было не так, то кто-то обязательно пришёл бы и разъяснил, что на Coq без Emacs тоже писать не принято, но и в Agda Emacs необязателен; что в быту Coq, который тебе понравился больше всех, лучше не использовать, потому что он очень хиленький. На Coq нельзя написать даже функцию merge из merge sort, чтобы не напороться на неприятности, в отличие от той же Agda. В общем, кто-то бы ответил каким-то опытом из индустрии. Но этого не произошло.> Одному только тебе хую что то все пекло на ровном месте. И до сих пор не отпустило похоже.Я в этот тред только что-то писал, там с тобой кто-то другой спорил.>>1402709> нооо, непонятно немного как теперь получать какой-то выводТут уже нужно понимать, как работает само соответствие Карри-Говарда. И лучше тут начать с Хаскелля и исчисления высказываний. В качестве \/ можно взять Either, в качестве /\ можно взять пару. Стрелка -- импликация.Тогда высказывание (A -> B -> A) из логики высказываний -- это функция const из Haskell. Аппликация -- это то же, что modus ponens в исчислении высказываний. Аксиомы интуиционистского исчисления высказываний можно в Haskell вывести. Тогда, например, можно взять вывод формулы A -> A из исчисления высказываний:1. A -> (A -> A) -> A -- аксиома 12. A -> (A -> A) -- аксиома 13. (A -> (A -> A) -> A) -> (A -> (A -> A)) -> A -> A -- аксиома 24. (A -> (A -> A)) -> A -> A (MP(1, 3))5. A -> A (MP(2, 4))ему будет соответствовать такая функция:id' :: a -> aid' = a2 a1 a1В Coq добавляются зависимые типы -- они просто ещё дают кванторы.>>1402720> Любую terminating программу можно интерпретировать как некоторое конструктивное доказательство?Любую тотальную и типизируемую -- да.>>1402726В такой записи можно считать, что Empty = ⊥. За ⊥ обозначают и расходимость как значение, и пустой тип.>>1402732> Слушай, анон, а если мы модифицируем определение вывода как некоторой счётной последовательности формул, что получится?Тогда можно вывести что угодно, да. Выше я дал вывод (id' :: A -> A). Тогда если мы позволяем счётный вывод, то A можно доказать как id' (id' (id' (id' ... То есть t = a2 a1 a1 t -- это доказательство любого A.>>1402750Ну почти. В исчислении секвенций много правил вывода с посылками и одна "аксиома" -- правило вывода без посылок. В исчислении высказываний наоборот. Выше я вывел A -> A, это можно записать как дерево, где узлы -- это modus ponens, а листья -- аксиомы.>>1402832> Там нет параграфа 7.2.3Да, прости, перепутал. 7.3.2.>>1403023> Ничто не мешает написать функцию берущую состояние МТ и возвращающую следующее состояние. Проблема только если мы хотим завернуть эту функцию перехода в цикл "двигать до терминального состояния" поскольку coq пошлет нас нахуй т.к. нельзя наверняка сказать что такое состояние будет вообще достигнуто.Это всё правда, только ты упустил, что там речь шла о доказательстве программ, так что там полезно вводить многошаговую редукцию как отношение. Можно, конечно, ввести вычислимую функцию n-шаговой редукции и доказывать достижимость и недостижимость терминального состояния как "существует n..." и "не существует n...", но ведь, во-первых, так неудобно, во-вторых, невменяемо сложно выразить недетерминизм, хотя иногда хотелось бы.> Нахуя он в синтаксисе coq написал пример с которым coq его очевидно пошлет нахуй - для меня тоже великая загадка.Я думаю, ты не очень внимательно прочитал. Все примеры, кроме того, где 2 + 2 = 5, я копипастил из Coq, а тот пример я привёл, чтобы ответить на вопрос, почему незавершающиеся функции нельзя считать доказательствами.> Он банальнейшей хуйни понаписал в общем тоА вот с этим я согласен. Моё исходное утверждение как раз то, что этот тред обречён, так как вместо того, чтобы засесть и хотя бы Software Foundations прорешать, все тут обсуждают глубокомысленно какую-то философию интуиционизма. Вообще я пришёл сюда потому, что тут пошли какие-то совсем далёкие от правды высказывания.
>>1403436>Тогда если мы позволяем счётный выводНо ведь понятие алгоритма тогда тоже нужно осчетинить, получается. Нет?>это можно записать как дерево, где узлы -- это modus ponens, а листья -- аксиомы.А, ну понятно.По остальному большое спасибо, оче пролил свет ты мне на всё это.
>>1403450>осчетинитьА, или не нужно, в алгоритме же должна быть конечная последовательность инструкций, так что bottom = bottom или while(true){} или t = a2 a1 a1 t сюда попадают. Ну ок тогда, вопросов больше нет, огромное спасибо.
>>1403436>если бы это было не так, то кто-то обязательно пришёл бы и разъяснил, что на Coq без Emacs тоже писать не принято, но и в Agda Emacs необязателен; что в быту Coq, который тебе понравился больше всех, лучше не использовать, потому что он очень хиленький. На Coq нельзя написать даже функцию merge из merge sort, чтобы не напороться на неприятности, в отличие от той же Agda. В общем, кто-то бы ответил каким-то опытом из индустрии. Но этого не произошло.Мог бы тогда так и написать вместо того чтобы пердеть в лужу. Только впредь постарайся свой понос из порванной сраки не выдавать за "мнение экспертов из индустрии", ладненько.
Вопрос экспертам из индустрии. Поясните за рекурсивные функции MLTT - natrec, treerec, listrec итд. Что они вообще делают, зачем они нужны? Пример их практического применения?
>>1403604Ещё раз тебе говорю: в том треде я не появлялся. Моё первое в жизни сообщение на /pr/ -- это вот это:>>1401957>>1403619> Поясните за рекурсивные функции MLTT - natrec, treerec, listrec итд. Что они вообще делают, зачем они нужны? Пример их практического применения?Почему все читают MLTT? Это же довольно старый материал, который слабо отражает современное положение дел.Так ведь там же нет другой рекурсии. listrec -- это почти что foldr из Haskell. Вот хочешь ты, например, написать какую-нибудь рекурсивную функцию -- например, reverse:reverse :: [a] -> [a]reverse xs = reverse' xs []reverse' [] ac = acreverse' (x:xs) ac = reverse' xs (x:ac)В MLTT у тебя просто нет способа это так выразить. Вместо этого надо извернуться и выразить reverse через foldr.reverse' [] = idreverse' (x:xs) = \ac -> (reverse' xs) (x:ac)reverse' = foldr (\x f ac -> f (x:ac)) idreverse xs = foldr (\x f ac -> f (x:ac)) id xs []Вот итоговое определение как раз можно переписать в MLTT.reverse xs = listrec xs id (\x _ f ac -> f (x:ac)) []И так нужно изощряться для любого рекурсивного определения.На самом деле рекурсия в Coq -- это почти то же самое, не считая синтаксического сахара и нескольких модификаций для возможности взаимно рекурсивных определений.
>>1404021> Почему все читают MLTT? Это же довольно старый материал, который слабо отражает современное положение дел.Современное положение дел это разве не расширения и надстройки над MLTT? В агде во всяком случае? Как вариант - PTS + удобства для использования этой хуйни как ЯП в коке. Или ты про всякие cubicaltt? Так опять же агда - единственный нормальный прувер, где это завезли. Или все не так?
Ещё вопрос, навеянный https://2ch.hk/math/res/50442.html#54650 Вот смотрите, у нас есть конструктивное определение множества N, есть конструктивное определение функций сложения и умножения, заданных на элементах этого множества. Есть возможность задать умножение через сложение. Но. Почему тогда ABC-гипотезу нельзя задать как простую функцию? Почему нужны изьебства уровня мочидзукиного аутизма - IUTeich, которые никто толком не понимает, чтобы просто связать умножение со сложением, причём в простейший примерах уровня 1+1? Как так-то, кто виноват и что делать?
Поясните за cedille. Тоже прувер жи, как я понял из описания, основан на лямбда исчислении по Карри, а не по Чёрчу как кок, идрис и агда, например.
>>1417389С этим тебе конструктивный петушок должен помочь, очень странно что он еще не прилетел на запах нубья.
>>1417308> Диссертация Браузера, а вообще лучше хуй соси.>>1417471> С этим тебе конструктивный петушок должен помочь, очень странно что он еще не прилетел на запах нубья.
>>1418003> даже своих любимых обосраных школьников достал.Ты в этой "дискуссии" именно обосранного школьника из себя и представляешь. Да и по жизни ты петух. Горишь на ровном месте, меня постоянно вспоминаешь неизвестно зачем. Хотя бы минимально вменяемый человек так себя вести не будет.
>>1418026>>1418098Сап петушок, смотрю ты и аватарку прикрепил, найс.Ну давай налетай видишь же нубье ждет когда же ты начнешь его кормить историями про Браузера и приобщать к вере в швятой Интуиционизм.
>>1418499Это кто-то из долбоебов-основальщиков, которые не знают, куда присунуть свою хуйню. Это не программисты и не математики, а опущенцы.
>>1382928 (OP)Вы ебанутые? Ручки с бумагами в руки и доказывать леммы!!!Компудахтор за вас не докажет теорему пифагора.
>>1418727> Компудахтор за вас не докажет теорему пифагора.Чё несёт. Даже в Идрисе это несколько строк кода.
>>1418514Как искать? Фамилия такая, что гуглится нифига.>>1382945>СохацкiйКстати, что с ним? ЖЖ удален, инфы нигде.
Там еще один прувер зарелизили Arend https://arend-lang.github.io/ на основе НоТТ. Что интересно, он в виде плагина к IntelliJ IDEA, ставится в пару кликов. Есть и как отдельный jar. >>1444522>>1444378>>1441823<---
>>1451351Добавлю, что пример очень показательный - НоТТ и зависимые типы на джяве, причем в виде простого плагина к ide. Ещё один шаг к тому, чтобы просто интегрировать их в джяву, как лямбду. Корректный софт и зависимые типы это будущее программирования, и то что сейчас есть только в 1,5 экспериментальных пруверах, через 20 лет будет стандартом в яп общего назначения.
>>1422717>Брауэр доказал теорему о неподвижной точке, хуй соси. Всего лишь через 7 лет после доказательства Болем..
>>1451351Зашел в чатик тележный этого прувера, увидел безынициативность автора к предложениям и вышел.што ш... arend говно и моча
