Нашли или выдавили из себя код, который нельзя назвать нормальным,
на который без улыбки не взглянешь?
Не торопитесь его удалять или рефакторить, — запостите его на
говнокод.ру, посмеёмся вместе!
(set-logic UF)
; https://smtlib.cs.uiowa.edu/logics.shtml
; UF for the extension allowing free sort and function symbols
(set-option :produce-proofs true)
(declare-sort M_wff)
; AND2
(declare-fun M_a2 (M_wff M_wff) M_wff)
; AND3
(declare-fun M_a3 (M_wff M_wff M_wff) M_wff)
; (AND2 a b) <=> (AND2 b a)
(assert
(forall ( (a M_wff) (b M_wff) )
(=
(M_a2 a b)
(M_a2 b a)
)
)
)
; (AND2 a a) <=> a
(assert
(forall ( (a M_wff) )
(=
(M_a2 a a)
a
)
)
)
; (AND2 a (AND2 b c)) <=> (AND3 a b c)
(assert
(forall ( (a M_wff) (b M_wff) (c M_wff) )
(=
(M_a2 a (M_a2 b c))
(M_a3 a b c)
)
)
)
; (AND3 a b c) <=> (AND3 b a c)
(assert
(forall ( (a M_wff) (b M_wff) (c M_wff) )
(=
(M_a3 a b c)
(M_a3 b a c)
)
)
)
; IMPL - implication
(declare-fun M_impl (M_wff M_wff) M_wff)
; http://us.metamath.org/ileuni/ax-1.html
; Axiom Simp
; (IMPL a (IMPL b a)) <=> (AND2 a b)
(assert
(forall ( (a M_wff) (b M_wff) )
(=
(M_impl a (M_impl b a))
(M_a2 a b)
)
)
)
...
Надо еще пруфануть что этот плагин правильно всё конвертит.
И даже если правильно, реализациии Gallina-интерпретатора на SMT-языке нет. Да и вообще, какие там есть реализации Gallina-интерпретатора, сколько есть таких реализаций и на каких языках?
> Надо еще пруфануть что этот плагин правильно всё конвертит.
А нафига. Он же от SMT сольвера пруф получает. И если этот пруф проходит проверку, то в общем-то пофиг и на корректность плагина и на корректность сольвера.
З.Ы. Сорок тысяч обезьян, рандомно стучащих по клаве -- тоже вполне валидный способ доказывать теоремы.
А корректность перевода из одного языка в другой язык кто проверять будет?
Если некая хрень неправильно переводит из одного языка в другой, получает некое доказательство которое оно тоже неправильно переводит, но которое по случайному стечению обстоятельств оказывается правильным для той теоремы (баги аннигилировались как-то, хуй знает) - это тоже не очень хорошая ситуация.
Еще одна попытка сделать формально доказанный компилятор сишечки - это в рамках Metamath Zero пытаются какой-то компилятор MMC сделать https://youtu.be/CxS0ONDfWJg?t=218
Я не спец по CompCert, но краям уха слышал, что register allocation там и правда на Ocaml, но выхлоп всё равно верифицируется. Многие стрелочки над пунктиром упираются в validate.
Потому что чтобы правильня распарсить код ня крестах — нядо решить проблему останова!
https://stackoverflow.com/a/14589567
> Line 21 is syntactically correct if and only if the N in IsPrime<N> is prime. Otherwise, typen is an integer, not a template, so typen<1>() is parsed as (typen<1)>() which is syntactically incorrect because () is not a syntactically valid expression.
Почему? В итоге ведь всё нормально получилось, обезьянки наебашили правильный пруф для конкретной задачи вопреки теории вероятности. Пруф от этого не стал каким-то зашкваренным, он ведь проходит проверку.
Ну в каких-то других ситуациях, где звёзды не так удачно лягут, ты увидишь багу и пофиксишь.
> которая кажется мне ... ммм ... неэлегантной ...
Мне, наоборот, metamath коммьюнити претит. Бегают с лозунгами, прямо как растоманы: "у нас самая большая библиотека в 100500 лемм!!!" А на самом деле, у них тупо нет тактик, и они в библиотеку высрали все промежуточные леммы, большая часть которых никакого интереса не представляет.
Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
> Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numbers start with 0x or 0X. bigint are integers; numbers without fractional nor exponent parts. bignat are non-negative integers. Underscores embedded in the digits are ignored, for example 1_000_000 is the same as 1000000.
Какие такие числа? Я ни про какие числа не знаю. Какая там аксиоматика? Арифметика Пеано или Пресбургера?
> integer and natural are limited to the range that fits into an OCaml integer (63-bit integers on most architectures). bigint and bignat have no range limitation.
OCaml? Я не хочу знать ни про какой OCaml и мне совершенно не должно быть важно, какие там в нем лимиты для каких-то чисел.
Ладно, читаем дальше.
>Keywords
> The following character sequences are keywords defined in the main Coq grammar that cannot be used as identifiers (even when starting Coq with the -noinit command-line flag):
_ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
SProp Set Theorem Type Variable as at cofix else end
fix for forall fun if in let match return then where with
Эмм, че? Что такое Fixpoint? А что такое CoFixpoint? Зачем это нужно?
Допустим я хочу свой интерпретатор Gallina имплементнуть, в каком месте мне надо читать о точном семантическом смысле Fixpoint и CoFixpoint? Зачем вводить подобную питушню на уровне базового языка??? Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются. Почему не начинать с более базовых вещей?
> Какие такие числа? Я ни про какие числа не знаю. Какая там аксиоматика? Арифметика Пеано или Пресбургера?
И та, и другая там есть в стандартной либе. Тактика `lia` работает с последней.
> Что такое Fixpoint?
Структурная рекурсия.
> А что такое CoFixpoint?
Структурная ко-рекурсия.
> Зачем это нужно?
Ну а зачем нужна рекурсия?
> Почему не начинать с более базовых вещей?
Это и есть базовые вещи в CoC.
> Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются.
В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню. Короче, попробуй сам и поймёшь.
И определил Питуз базовую питулю переписывания термов, и научил различать правильное и неправильное доказательство, и сказал, что всё остальное человек должен сделать своими руками
> Ну а зачем нужна рекурсия?
У меня на контроллерах не нужна, от нее стек быстро кончается. В Metamath тоже нет никакой рекурсии как базового понятия, и ничего, работает вроде. Зачем ее вводить как базовую сущность?
> Это и есть базовые вещи в CoC.
Зачем надо делать так, если можно начать с простого, а потом через простое выразить исчисление конструкций?
> В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню.
Ну хорошо, есть функции и термы. А где это это формально определено? Предположим я упоролся и хочу написать свою альтернативную реализацию Gallina на сишечке - что мне прочитать, чтоб по мотивам прочитанного я мог написать питушню на сишке, которая будет полностью соответствовать семантике той Gallina которая в доверенном ядре этого Coq?
> У меня в Coq никаких брадобреев нет, поэтому я за Coq.
Мы это вроде уже обсуждали. Брадобреи возникают в наивной теории множеств. В ZFC и IZF они не возникают, но могут быть другие парадоксы, это да. Но формальная система в Coq от каких-либо парадоксов тоже не застрахован, так что тут условия равны.
Metamath это чисто механическа хрень на переписывании, суть доказательства заключается в том, что есть "Hypotheses" и "Assertion" и надо из одного синтезировать другое, пользуясь какой-то там хренью (леммы доказанные из аксиом, или сами аксиомы) и критерий правильности или неправильности - это что применяя такие-то шаги у нас получается или не получается "Hypotheses" переписать в "Assertion".
Я более-менее в курсе, как он устроен. Проблема в аксиомах, с ними ситуация такая же, как с фотоном зашквара: если одна из них противоречит какой-либо другой, то на любое доказанное утверждение может няйтись контрпример. В итоге от возни с доказательствами в такой формальной системе смысла нят.
Теория типов, как считается, изолирует систему от попадания зашкваренных частиц.
Ну так если в Metamath грузануть некую систему аксиом, которая будет противоречивой, и можно будет доказать что ⊤⇔⊥, ну да и хрен бы с ним, в таком наборе аксиом это действительно так и доказательство действительно верно, раз у нас такие хуевые аксиомы. Выбери другую аксиоматику, где такой хуйни не будет.
> А на самом деле, у них тупо нет тактик, и они в библиотеку высрали все промежуточные леммы, большая часть которых никакого интереса не представляет.
Тактики - дело наживное. Меня больше волнует тот факт, что написать свой Gallina-интерпретатор (альтернативное доверенное ядро проверки питушни) - нихуя не просто, какие-то неподвижные точки прямо в сам язык встроены. Зачем? Зачем? Почему это не теоремы-аксиомы? Почему не сделать максимально простое доверенное ядро, а там уж на него навешивать всякие неподвижные точки, кванторы-шманторы, типы и прочую такую питулю?
> Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
"Теория типов хуйня потому что медленно" - хуёвая доебка, согласен. Я до теорий типов могу доебаться намного лучше.
Ты путаешь куритсу с яйтсом. Ключевое слово Theorem в Coq — синоним определения функции. Axiom — примерно тоже, но без определеления. В Coq довольно много заумных ключевых слов, которые зачастую несут чисто декоративную функцию, но ядро языка при этом весьма простое.
И такую примитивную хуйню, что "если (φ → ψ) и (ψ → χ) то тогда (φ → χ)" оно доказывает хер знает сколько и высирает какое-то дниннющее нечитаемое доказательство. Я б посмотрел, как Coq его будет проверять, если его сконвертить.
> А как тогда вообще эти авто-пруверы юзать, если они на такой тривиальной теореме сливаются?
Я думаю что авто-пруверы под такую питушню не затачивались, никто не придумывал специальных эвристик под ситуации когда там реализовывали через ассерты систему Гильберта и через эту внутреннюю систему Гильберта доказывали хуиту описанную через эту систему Гильберта. Быть может, если как-нибудь переформулировать эту хуиту в более удобоваримую форму, всякие другие SMT-решатели тоже будут что-то там доказывать.
А так вообще, можешь почитать https://sat-smt.codes/SAT_SMT_by_example.pdf - там очень много интересных применений описано, и SMT решатели - достаточно мощная штука. Там через них можно сапёр решать, передавая состояние игрового поля.
Так-то вообще суть такова, что Гильбертову систему можно через uninterptreted function хрень с двусторонним переписыванием реализовать. Вот так можно описать исчисление высказываний
(<=>
(& a b)
(& a (-> a b))
)
(<=>
(& a b c)
(&
(& a b c)
(-> a (-> b a))
)
)
(<=>
(& a b c)
(&
(& a b c)
(->
(-> a (-> b c))
(-> (-> a b) (-> a c))
)
)
)
(<=> a b) это значит что для доказывания можно свободно переписывать "b" на "a", и переписывать "a" на "b"
Т.е. выходит что любая хрень, кроме модус поненса, описанного как
(<=>
(& a b)
(& a (-> a b))
)
не убирает ничего лишнего, а лишь нарашивает питушню в списке. И доказательство что из "x" выводимо "y" это когда из питушни "x" можно сконструировать "(& y ... некаяхуйня ... )" или когда из "(& y ... некаяхуйня ...)" можно сконструировать x
> что любая хрень, кроме модус поненса, ... не убирает ничего лишнего
Тут конечно надо заметить, что модус поненс от этого не становится неинвертируемым. Т.е. если есть (& a b) то из него можно синтезнуть (& a (-> a b), и из (& a (-> a b)) можно тоже обратно синтезнуть (& a b). Это я лишь к тому, что не было b, а теперь он появился.
И да, такую вот переписывающую питушню реализовать достаточно просто. А сколько надо проебать времени, чтобы реализовать свою альтернативную Gallina из этого Coq, чтоб это был standalone executable компилирующийся из сишки?
И да, такой вот ассемблер реализовать достаточно просто. А сколько надо проебать времени, чтобы реализовать свою альтернативную сишку?
Это я к тому, что курица -- это всё-таки компроммисс между практичностью и минимальностью, чтобы и в кресты не скатиться и на голом переписывании термов не ебашить.
> Это я к тому, что курица -- это всё-таки компроммисс между практичностью и минимальностью
Любую хуитень можно назвать каким-то компромиссом. Для кого-то сишка -- "компромисс между практичностью и минимальностью", для кого-то кресты -- "компромисс между практичностью и минимальностью", для кого-то еще - ассемблер (а есть еще машинные коды, которые в HEX-редакторе можно руками вбивать). И как определить, чей компромисс более компромиссный?
Ну это ж только если некая питуля с бесконечными списками. А если конечносписочная, то всё развернется в (M_a2 var1 (M_a2 var2 (M_a2 var3 (M_a2 var4 (....... питушню, которая конечна.
Вроде Снаут упоминал какой-то плагин, который курицу конвертит в SMT для сольвера, а потом пруф обратно импортирует?
Какое прелестное название! А какие ассоциации возникают )))
И даже если правильно, реализациии Gallina-интерпретатора на SMT-языке нет. Да и вообще, какие там есть реализации Gallina-интерпретатора, сколько есть таких реализаций и на каких языках?
А нафига. Он же от SMT сольвера пруф получает. И если этот пруф проходит проверку, то в общем-то пофиг и на корректность плагина и на корректность сольвера.
З.Ы. Сорок тысяч обезьян, рандомно стучащих по клаве -- тоже вполне валидный способ доказывать теоремы.
Если некая хрень неправильно переводит из одного языка в другой, получает некое доказательство которое оно тоже неправильно переводит, но которое по случайному стечению обстоятельств оказывается правильным для той теоремы (баги аннигилировались как-то, хуй знает) - это тоже не очень хорошая ситуация.
Там, имхо, очень далеко до "почти". https://www.absint.com/compcert/structure.htm
https://www.absint.com/compcert/compcert_diagram.png - всё что выше пунктира - не доказано, а просто запрограммировано на OCaml.
Еще одна попытка сделать формально доказанный компилятор сишечки - это в рамках Metamath Zero пытаются какой-то компилятор MMC сделать https://youtu.be/CxS0ONDfWJg?t=218
https://stackoverflow.com/a/14589567
> Line 21 is syntactically correct if and only if the N in IsPrime<N> is prime. Otherwise, typen is an integer, not a template, so typen<1>() is parsed as (typen<1)>() which is syntactically incorrect because () is not a syntactically valid expression.
Ой мама, как же весело наверное писать для крестов полноценный IDE с кодинсайтом
Почему? В итоге ведь всё нормально получилось, обезьянки наебашили правильный пруф для конкретной задачи вопреки теории вероятности. Пруф от этого не стал каким-то зашкваренным, он ведь проходит проверку.
Ну в каких-то других ситуациях, где звёзды не так удачно лягут, ты увидишь багу и пофиксишь.
Но надо б конечно себя переосилить и разобраться в этом Coq чтоб более обоснованно его раскритиковать
Мне, наоборот, metamath коммьюнити претит. Бегают с лозунгами, прямо как растоманы: "у нас самая большая библиотека в 100500 лемм!!!" А на самом деле, у них тупо нет тактик, и они в библиотеку высрали все промежуточные леммы, большая часть которых никакого интереса не представляет.
Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
Я не на комьюнити смотрю, а на свойства языка. Язык Metamath для меня выглядит куда более понятным, чем язык Gallina, и проверятель пруфов для Metamath написать явно проще. Вот взять например этот мануал:
https://coq.github.io/doc/master/refman/language/core/basic.html#lexical-conventions
Читаем:
> Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numbers start with 0x or 0X. bigint are integers; numbers without fractional nor exponent parts. bignat are non-negative integers. Underscores embedded in the digits are ignored, for example 1_000_000 is the same as 1000000.
Какие такие числа? Я ни про какие числа не знаю. Какая там аксиоматика? Арифметика Пеано или Пресбургера?
> integer and natural are limited to the range that fits into an OCaml integer (63-bit integers on most architectures). bigint and bignat have no range limitation.
OCaml? Я не хочу знать ни про какой OCaml и мне совершенно не должно быть важно, какие там в нем лимиты для каких-то чисел.
Ладно, читаем дальше.
>Keywords
> The following character sequences are keywords defined in the main Coq grammar that cannot be used as identifiers (even when starting Coq with the -noinit command-line flag):
Эмм, че? Что такое Fixpoint? А что такое CoFixpoint? Зачем это нужно?
Допустим я хочу свой интерпретатор Gallina имплементнуть, в каком месте мне надо читать о точном семантическом смысле Fixpoint и CoFixpoint? Зачем вводить подобную питушню на уровне базового языка??? Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются. Почему не начинать с более базовых вещей?
И та, и другая там есть в стандартной либе. Тактика `lia` работает с последней.
> Что такое Fixpoint?
Структурная рекурсия.
> А что такое CoFixpoint?
Структурная ко-рекурсия.
> Зачем это нужно?
Ну а зачем нужна рекурсия?
> Почему не начинать с более базовых вещей?
Это и есть базовые вещи в CoC.
> Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются.
В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню. Короче, попробуй сам и поймёшь.
> Структурная ко-рекурсия.
В Metamath ничего этого нет.
И определил Питуз базовую питулю переписывания термов, и научил различать правильное и неправильное доказательство, и сказал, что всё остальное человек должен сделать своими руками
> Ну а зачем нужна рекурсия?
У меня на контроллерах не нужна, от нее стек быстро кончается. В Metamath тоже нет никакой рекурсии как базового понятия, и ничего, работает вроде. Зачем ее вводить как базовую сущность?
> Это и есть базовые вещи в CoC.
Зачем надо делать так, если можно начать с простого, а потом через простое выразить исчисление конструкций?
> В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню.
Ну хорошо, есть функции и термы. А где это это формально определено? Предположим я упоролся и хочу написать свою альтернативную реализацию Gallina на сишечке - что мне прочитать, чтоб по мотивам прочитанного я мог написать питушню на сишке, которая будет полностью соответствовать семантике той Gallina которая в доверенном ядре этого Coq?
[[citation needed]] Емнип, в metamаth можно запилить теорию Фреге, и он её сожрёт и не подавится.
У меня в Coq никаких брадобреев нет, поэтому я за Coq.
Не слышал про теорию Фреге. Знаю что есть теорема Фреге (P → (Q→R)) → ((P→Q) → (P→R)), и в metamath она есть http://us.metamath.org/ileuni/ax-2.html
> У меня в Coq никаких брадобреев нет, поэтому я за Coq.
Мы это вроде уже обсуждали. Брадобреи возникают в наивной теории множеств. В ZFC и IZF они не возникают, но могут быть другие парадоксы, это да. Но формальная система в Coq от каких-либо парадоксов тоже не застрахован, так что тут условия равны.
Я про наивную теорию множеств. Он её придумал.
> Но формальная система в Coq от каких-либо парадоксов тоже не застрахован
Теория типов как раз именно от этого и страхует.
> так что тут условия равны
Так что нет.
Эмм, но ведь нет же. Разве теория типов позволяет доказать непротиворечивость теории типов? Чем доказывается непротиворечивость теории типов?
См "вторая теорема Гёделя"
Ничем, но парадоксов в ней ещё не нашли.
Теория типов, как считается, изолирует систему от попадания зашкваренных частиц.
"как считается", да. Четкого доказательства этому нет, да и не может быть.
Верно. Но это ещё не повод переходить на PHP.
Тактики - дело наживное. Меня больше волнует тот факт, что написать свой Gallina-интерпретатор (альтернативное доверенное ядро проверки питушни) - нихуя не просто, какие-то неподвижные точки прямо в сам язык встроены. Зачем? Зачем? Почему это не теоремы-аксиомы? Почему не сделать максимально простое доверенное ядро, а там уж на него навешивать всякие неподвижные точки, кванторы-шманторы, типы и прочую такую питулю?
> Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
"Теория типов хуйня потому что медленно" - хуёвая доебка, согласен. Я до теорий типов могу доебаться намного лучше.
Ты путаешь куритсу с яйтсом. Ключевое слово Theorem в Coq — синоним определения функции. Axiom — примерно тоже, но без определеления. В Coq довольно много заумных ключевых слов, которые зачастую несут чисто декоративную функцию, но ядро языка при этом весьма простое.
Ещё бы не застревать на задачах со звёздочками... Сраный перфекционизм почему-то не даёт забить на них и идти дальше, а решить ума не хватает.
вот вроде бы пофиксил немного...
Доказательство там конечно совершенно нечитаемый пиздец, выглядит оно вот так:
1005:(resolution ((not (= (M_a2 (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_a2 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2))))) (not (= (M_a2 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2))) (M_a2 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1)))) (not (= (M_a3 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1) (M_impl @sk0 @sk1)) (M_a2 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_a2 (M_impl @sk0 @sk1) (M_impl @sk0 @sk1))))) (not (= (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1)) (M_a3 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1) (M_impl @sk0 @sk1)))) (not (= (M_a2 (M_impl @sk0 @sk1) (M_a2 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1))) (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1)))) (not (= (M_a2 (M_impl @sk0 @sk1) (M_a2 (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk1 @sk2))) (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk1 @sk2)))) (not (= (M_a3 (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk1 @sk2)))) (not (= (M_a2 (M_impl (M_impl @sk1 @sk2)...
> не осиливают
А как тогда вообще эти авто-пруверы юзать, если они на такой тривиальной теореме сливаются?
Я думаю что авто-пруверы под такую питушню не затачивались, никто не придумывал специальных эвристик под ситуации когда там реализовывали через ассерты систему Гильберта и через эту внутреннюю систему Гильберта доказывали хуиту описанную через эту систему Гильберта. Быть может, если как-нибудь переформулировать эту хуиту в более удобоваримую форму, всякие другие SMT-решатели тоже будут что-то там доказывать.
Разворачивается в... барабанная дробь...
SMT солверы нужны для байтоёбства, зачем их юзать для абстрактной питушни?
А если я ему какое-нибудь sha в виде системы уравнений запишу, он найдёт что было на входе у хеша?
> SMT солверы нужны для байтоёбства, зачем их юзать для абстрактной питушни?
Байтоебство изоморфно абстрактной питушне.
(<=> a b) это значит что для доказывания можно свободно переписывать "b" на "a", и переписывать "a" на "b"
не убирает ничего лишнего, а лишь нарашивает питушню в списке. И доказательство что из "x" выводимо "y" это когда из питушни "x" можно сконструировать "(& y ... некаяхуйня ... )" или когда из "(& y ... некаяхуйня ...)" можно сконструировать x
Тут конечно надо заметить, что модус поненс от этого не становится неинвертируемым. Т.е. если есть (& a b) то из него можно синтезнуть (& a (-> a b), и из (& a (-> a b)) можно тоже обратно синтезнуть (& a b). Это я лишь к тому, что не было b, а теперь он появился.
лучше так.
И да, такую вот переписывающую питушню реализовать достаточно просто. А сколько надо проебать времени, чтобы реализовать свою альтернативную Gallina из этого Coq, чтоб это был standalone executable компилирующийся из сишки?
Это я к тому, что курица -- это всё-таки компроммисс между практичностью и минимальностью, чтобы и в кресты не скатиться и на голом переписывании термов не ебашить.
Любую хуитень можно назвать каким-то компромиссом. Для кого-то сишка -- "компромисс между практичностью и минимальностью", для кого-то кресты -- "компромисс между практичностью и минимальностью", для кого-то еще - ассемблер (а есть еще машинные коды, которые в HEX-редакторе можно руками вбивать). И как определить, чей компромисс более компромиссный?
https://www.youtube.com/watch?v=FtcQrFvnZxs
Понятно.
Настоящий сишник даже под "SMT" пишет как на няшной.
Но придётся принять ислам аксиому индукции?
M_a2 это ж по сути хрень для выражений, которые являются истинными в данном контексте. См. https://en.wikipedia.org/wiki/Hilbert_system