1. Куча / Говнокод #27379

    +1

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 26
    27. 27
    28. 28
    29. 29
    30. 30
    31. 31
    32. 32
    33. 33
    34. 34
    35. 35
    36. 36
    37. 37
    38. 38
    39. 39
    40. 40
    41. 41
    42. 42
    43. 43
    44. 44
    45. 45
    46. 46
    47. 47
    48. 48
    49. 49
    50. 50
    51. 51
    52. 52
    53. 53
    54. 54
    55. 55
    56. 56
    57. 57
    58. 58
    59. 59
    60. 60
    61. 61
    62. 62
    63. 63
    64. 64
    65. 65
    66. 66
    67. 67
    68. 68
    69. 69
    70. 70
    71. 71
    72. 72
    73. 73
    74. 74
    75. 75
    76. 76
    77. 77
    78. 78
    79. 79
    80. 80
    81. 81
    82. 82
    83. 83
    84. 84
    85. 85
    86. 86
    87. 87
    88. 88
    (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)
        )
      )
    )
    
    ...

    Весь код не влазит.

    https://rise4fun.com/Z3/GnfIH
    https://paste.debian.net/hidden/38ef8493/ (запасная ссылка)

    Переписывал Metamath на язык из SMT солверов https://smtlib.cs.uiowa.edu/language.shtml
    Z3 даже умеет доказывать какую-то питушню там.

    Запостил: j123123, 28 Апреля 2021

    Комментарии (72) RSS

    • Перепишите это на Coq теперь!
      Ответить
      • А в чём проблема? Прошлый код ведь удалось переписать и даже доказать (вручную).
        Ответить
        • Вручную это неинтересно. Пусть как-нибудь само там доказывает поиском в ширину всех вореций замены (переписывания) питули.
          Ответить
        • Можно еще Gallina на STM попробовать переписать и через SMT доказывать какую-то питулю на Coq
          Ответить
          • > переписать

            Вроде Снаут упоминал какой-то плагин, который курицу конвертит в SMT для сольвера, а потом пруф обратно импортирует?
            Ответить
            • coqhammer и smtcoq знаю.
              Ответить
              • > coqhammer

                Какое прелестное название! А какие ассоциации возникают )))
                Ответить
            • Надо еще пруфануть что этот плагин правильно всё конвертит.

              И даже если правильно, реализациии Gallina-интерпретатора на SMT-языке нет. Да и вообще, какие там есть реализации Gallina-интерпретатора, сколько есть таких реализаций и на каких языках?
              Ответить
              • > Надо еще пруфануть что этот плагин правильно всё конвертит.

                А нафига. Он же от SMT сольвера пруф получает. И если этот пруф проходит проверку, то в общем-то пофиг и на корректность плагина и на корректность сольвера.

                З.Ы. Сорок тысяч обезьян, рандомно стучащих по клаве -- тоже вполне валидный способ доказывать теоремы.
                Ответить
                • А корректность перевода из одного языка в другой язык кто проверять будет?

                  Если некая хрень неправильно переводит из одного языка в другой, получает некое доказательство которое оно тоже неправильно переводит, но которое по случайному стечению обстоятельств оказывается правильным для той теоремы (баги аннигилировались как-то, хуй знает) - это тоже не очень хорошая ситуация.
                  Ответить
                  • Ну если уж они выгрузку в мышиный код через няшную (почти?) доказали (compcert), то пруф выгрузки в SMT проблемой явно не будет.
                    Ответить
                    • > Ну если уж они выгрузку в мышиный код через няшную (почти?) доказали (compcert)

                      Там, имхо, очень далеко до "почти". 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
                      Ответить
                      • Я не спец по 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.
                        Ответить
                        • Шах и мат, ма-те-ма-тики!
                          Ответить
                        • >Потому что чтобы правильня распарсить код ня крестах — нядо решить проблему останова!


                          Ой мама, как же весело наверное писать для крестов полноценный IDE с кодинсайтом
                          Ответить
                  • Результатом перевода, как я понимаю, является пруф на Coq. Если перевод был неправильный, coqchk его заклюёт.
                    Ответить
                  • > это тоже не очень хорошая ситуация

                    Почему? В итоге ведь всё нормально получилось, обезьянки наебашили правильный пруф для конкретной задачи вопреки теории вероятности. Пруф от этого не стал каким-то зашкваренным, он ведь проходит проверку.

                    Ну в каких-то других ситуациях, где звёзды не так удачно лягут, ты увидишь багу и пофиксишь.
                    Ответить
      • Сам перепиши. Выучить Coq по книжке Пирса ­— много ума не нужно.
        Ответить
        • В Coq какая-то питушня с этими типами, которая кажется мне ... ммм ... неэлегантной ...

          Но надо б конечно себя переосилить и разобраться в этом Coq чтоб более обоснованно его раскритиковать
          Ответить
          • > которая кажется мне ... ммм ... неэлегантной ...

            Мне, наоборот, metamath коммьюнити претит. Бегают с лозунгами, прямо как растоманы: "у нас самая большая библиотека в 100500 лемм!!!" А на самом деле, у них тупо нет тактик, и они в библиотеку высрали все промежуточные леммы, большая часть которых никакого интереса не представляет.
            Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
            Ответить
            • > Мне, наоборот, metamath коммьюнити претит.

              Я не на комьюнити смотрю, а на свойства языка. Язык 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):

              _ 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 ничего этого нет.

                  И определил Питуз базовую питулю переписывания термов, и научил различать правильное и неправильное доказательство, и сказал, что всё остальное человек должен сделать своими руками

                  > Ну а зачем нужна рекурсия?

                  У меня на контроллерах не нужна, от нее стек быстро кончается. В 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 от каких-либо парадоксов тоже не застрахован
                        Теория типов как раз именно от этого и страхует.

                        > так что тут условия равны
                        Так что нет.
                        Ответить
                        • > Теория типов как раз именно от этого и страхует.

                          Эмм, но ведь нет же. Разве теория типов позволяет доказать непротиворечивость теории типов? Чем доказывается непротиворечивость теории типов?

                          См "вторая теорема Гёделя"
                          Ответить
                          • > Чем доказывается непротиворечивость теории типов?

                            Ничем, но парадоксов в ней ещё не нашли.
                            Ответить
                            • В ZFC тоже пока не нашли, как и в IZF и куче других аксиоматизаций теорий множеств. Почему теории типов надо больше доверять?
                              Ответить
                    • Metamath это чисто механическа хрень на переписывании, суть доказательства заключается в том, что есть "Hypotheses" и "Assertion" и надо из одного синтезировать другое, пользуясь какой-то там хренью (леммы доказанные из аксиом, или сами аксиомы) и критерий правильности или неправильности - это что применяя такие-то шаги у нас получается или не получается "Hypotheses" переписать в "Assertion".
                      Ответить
                      • Я более-менее в курсе, как он устроен. Проблема в аксиомах, с ними ситуация такая же, как с фотоном зашквара: если одна из них противоречит какой-либо другой, то на любое доказанное утверждение может няйтись контрпример. В итоге от возни с доказательствами в такой формальной системе смысла нят.
                        Теория типов, как считается, изолирует систему от попадания зашкваренных частиц.
                        Ответить
                        • > Теория типов, как считается, изолирует систему от попадания зашкваренных частиц.

                          "как считается", да. Четкого доказательства этому нет, да и не может быть.
                          Ответить
                          • > Четкого доказательства этому нет, да и не может быть.

                            Верно. Но это ещё не повод переходить на PHP.
                            Ответить
                      • Ну так если в Metamath грузануть некую систему аксиом, которая будет противоречивой, и можно будет доказать что ⊤⇔⊥, ну да и хрен бы с ним, в таком наборе аксиом это действительно так и доказательство действительно верно, раз у нас такие хуевые аксиомы. Выбери другую аксиоматику, где такой хуйни не будет.
                        Ответить
            • > А на самом деле, у них тупо нет тактик, и они в библиотеку высрали все промежуточные леммы, большая часть которых никакого интереса не представляет.

              Тактики - дело наживное. Меня больше волнует тот факт, что написать свой Gallina-интерпретатор (альтернативное доверенное ядро проверки питушни) - нихуя не просто, какие-то неподвижные точки прямо в сам язык встроены. Зачем? Зачем? Почему это не теоремы-аксиомы? Почему не сделать максимально простое доверенное ядро, а там уж на него навешивать всякие неподвижные точки, кванторы-шманторы, типы и прочую такую питулю?

              > Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"

              "Теория типов хуйня потому что медленно" - хуёвая доебка, согласен. Я до теорий типов могу доебаться намного лучше.
              Ответить
              • > Зачем? Зачем? Почему это не теоремы-аксиомы?

                Ты путаешь куритсу с яйтсом. Ключевое слово Theorem в Coq — синоним определения функции. Axiom — примерно тоже, но без определеления. В Coq довольно много заумных ключевых слов, которые зачастую несут чисто декоративную функцию, но ядро языка при этом весьма простое.
                Ответить
        • > много ума не нужно

          Ещё бы не застревать на задачах со звёздочками... Сраный перфекционизм почему-то не даёт забить на них и идти дальше, а решить ума не хватает.
          Ответить
          • А я сразу себе говорю: «я не ма-те-ма-тик, чтобы такое решать, пропускаем...», когда читаю. И книги сразу так легко читаются!
            Ответить
          • Я придерживался принципа полуперфекционизма: уходил дальше, потом возвращался с какой-нибудь новой тактикой, которая их легко вскрывала.
            Ответить
    • Но вообще кажется что я там где-то накосячил и что-то не так понял. Надо б разобраться более детально.
      Ответить
      • https://paste.debian.net/hidden/a8db1767/
        вот вроде бы пофиксил немного...
        Ответить
      • https://paste.debian.net/hidden/1014febf/ вот пофиксил вроде норм теперь. SMT-решатель veriT https://verit.loria.fr/ эту хрень умудряется доказывать, Z3 и CVC4 как-то не осиливают.

        Доказательство там конечно совершенно нечитаемый пиздец, выглядит оно вот так:
        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)...
        Ответить
        • И такую примитивную хуйню, что "если (φ → ψ) и (ψ → χ) то тогда (φ → χ)" оно доказывает хер знает сколько и высирает какое-то дниннющее нечитаемое доказательство. Я б посмотрел, как Coq его будет проверять, если его сконвертить.
          Ответить
          • > доказывает хер знает сколько
            > не осиливают

            А как тогда вообще эти авто-пруверы юзать, если они на такой тривиальной теореме сливаются?
            Ответить
            • > А как тогда вообще эти авто-пруверы юзать, если они на такой тривиальной теореме сливаются?

              Я думаю что авто-пруверы под такую питушню не затачивались, никто не придумывал специальных эвристик под ситуации когда там реализовывали через ассерты систему Гильберта и через эту внутреннюю систему Гильберта доказывали хуиту описанную через эту систему Гильберта. Быть может, если как-нибудь переформулировать эту хуиту в более удобоваримую форму, всякие другие SMT-решатели тоже будут что-то там доказывать.
              Ответить
            • А так вообще, можешь почитать https://sat-smt.codes/SAT_SMT_by_example.pdf - там очень много интересных применений описано, и SMT решатели - достаточно мощная штука. Там через них можно сапёр решать, передавая состояние игрового поля.
              Ответить
          • > Я б посмотрел, как Coq его будет проверять, если его сконвертить.

            Theorem j123123 a b c : (a -> b) -> (b -> c) -> (a -> c).
            Proof.
               eauto.
            Qed.


            Разворачивается в... барабанная дробь...
            fun (a b c : Type) (X : a -> b) (X0 : b -> c) (X1 : a) => X0 (X X1)


            SMT солверы нужны для байтоёбства, зачем их юзать для абстрактной питушни?
            Ответить
            • > для байтоёбства

              А если я ему какое-нибудь sha в виде системы уравнений запишу, он найдёт что было на входе у хеша?
              Ответить
            • Ты кстати не совсем честно сделал. Надо определить и аксиоматизировать импликацию и хуиту "у нас тут и то и это", и поверх этой хуиты уже доказывать.

              > 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, а теперь он появился.
                    Ответить
                • (<=>
                    (& a b)
                    (&
                      (& a b)
                      (-> a (-> b a))
                    )
                  )

                  лучше так.

                  И да, такую вот переписывающую питушню реализовать достаточно просто. А сколько надо проебать времени, чтобы реализовать свою альтернативную Gallina из этого Coq, чтоб это был standalone executable компилирующийся из сишки?
                  Ответить
                  • И да, такой вот ассемблер реализовать достаточно просто. А сколько надо проебать времени, чтобы реализовать свою альтернативную сишку?

                    Это я к тому, что курица -- это всё-таки компроммисс между практичностью и минимальностью, чтобы и в кресты не скатиться и на голом переписывании термов не ебашить.
                    Ответить
                    • Альтернативную сишку может быть реализовать куда проще, чем некоторые виды ассемблера (например x86-64 со всеми существующими говноинструкциями)
                      Ответить
                    • > Это я к тому, что курица -- это всё-таки компроммисс между практичностью и минимальностью

                      Любую хуитень можно назвать каким-то компромиссом. Для кого-то сишка -- "компромисс между практичностью и минимальностью", для кого-то кресты -- "компромисс между практичностью и минимальностью", для кого-то еще - ассемблер (а есть еще машинные коды, которые в HEX-редакторе можно руками вбивать). И как определить, чей компромисс более компромиссный?
                      Ответить
                    • Курица - не птица.
                      Ответить
    • > M_a2 (M_wff M_wff) M_wff

      Понятно.
      Ответить
      • ( (well-formed formula) и (well-formed formula) ) это (well-formed formula)
        Ответить
      • > Понятно

        Настоящий сишник даже под "SMT" пишет как на няшной.
        Ответить
        • Там вроде какая-то херня типа хачкелевого foldl foldr может быть сделана, но мне было лень разбираться
          Ответить
          • > херня типа хачкелевого foldl foldr может быть сделана

            Но придётся принять ислам аксиому индукции?
            Ответить
            • Ну это ж только если некая питуля с бесконечными списками. А если конечносписочная, то всё развернется в (M_a2 var1 (M_a2 var2 (M_a2 var3 (M_a2 var4 (....... питушню, которая конечна.

              M_a2 это ж по сути хрень для выражений, которые являются истинными в данном контексте. См. https://en.wikipedia.org/wiki/Hilbert_system
              Ответить
            • Главное — чтобы ня аксиому выбора. А то так можня нечаяння дублировать шары!
              Ответить

    Добавить комментарий