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

    +2

    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
    (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_list)
    
    (declare-fun m_node (M_list M_list) M_list)
    
    ; один хер какой порядок, можно переписать (a, b) на (b, a)
    (assert
      (forall ( (a M_list) (b M_list) )
        (=
          (m_node a b)
          (m_node b a)
        )
      )
    )
    
    ; если есть (a (b c)) то можно переписать на (с (a b))
    (assert
      (forall ( (a M_list) (b M_list) (c M_list) )
        (=
          (m_node a (m_node b c) )
          (m_node c (m_node a b) )
        )
      )
    )
    
    ; Можно создавать или удалять повторы, (a a) <=> a
    (assert
      (forall ( (a M_list))
        (=
          (m_node a a)
          a
        )
      )
    )
    
    
    ; Чтоб узнать, выводима ли такая-то хернь
    (declare-fun m_node_select (M_list M_list) Bool)
    
    
    (assert
      (forall ( (a M_list) (b M_list) )
        (m_node_select
          a (m_node a b)
        )
      )
    )
    
    ; проверяем, можно ли сконструировать (a a) из (c ((b d) a))
    (assert
      (not (forall ( (a M_list) (b M_list) (c M_list) (d M_list) )
        (m_node_select
          (m_node a a)
          (m_node c (m_node (m_node b d) a) )
        )
      ))
    )
    
    
    (check-sat)
    (get-proof)

    Вот вам немного гомоикон SMT-солвера. Эта вот хренотень сама доказывает, не то что какой-то там Coq.

    Понятно что по тем вот говноправилам можно чтоб всплыло 'a' и потом его удвоить "(a a) <=> a"
    потом через m_node_select вытащить этот дубликат

    Запостил: j123123, 01 Марта 2021

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

    • На этой хуите с uninterpreted functions кстати можно попробовать свой гильберт-стайл прувер написать, и чтоб оно там само всякие вореции доказательств перебирало.
      Ответить
    • Что-то мне намекает, что "сама доказывает" она не больше чем какой-нибудь auto в петухе.
      Ответить
      • Конкретно в этом случае может быть какие-то автоматические тактики Coq и осилят (пусть снаут проверит, если не лень), но в общем случае эти SMT-решатели сами по себе доказывают намного лучше (т.к. специально под это затачивались) чем какая-то auto-хрень в Coq (в котором же еще надо понимать, какие тактики в каком порядке к какой питушне и как применять)
        Ответить
        • > доказывают намного лучше

          А что делать, если они не осиливают? Какой-то способ вручную пнуть в нужном направлении есть?
          Ответить
          • Да, вот в том же z3 есть тактики и стратегии какие-то https://rise4fun.com/z3/tutorial/strategies но я ими не пользовался
            Ответить
        • > пусть снаут проверит, если не лень

          Блин, я вот кстати х.з. как в петухе записать a и b -- неведомая хуйня одного сорта. Походу тут совсем другая логика юзается.
          Ответить
        • А всё, разобрался:
          Variable M_list: Set.
          
          Variable m_node: M_list -> M_list -> M_list.
          Hypothesis H1: forall a b: M_list, m_node a b = m_node b a.
          Hypothesis H2: forall a b c: M_list, m_node a (m_node b c) = m_node c (m_node a b).
          Hypothesis H3: forall a: M_list, m_node a a = a.
          
          Variable m_node_select: M_list -> M_list -> Prop.
          Hyphotesis H4: forall a b: M_list, m_node_select a (m_node a b).
          
          Theorem T: forall a b c d: M_list,
              m_node_select (m_node a a) (m_node c (m_node (m_node b d) a)).
          Вручную доказал, автоматом не прувит ;(
          Ответить
          • Я думаю что тут лучше использовать 'Prop' а не 'Set'
            Ответить
            • Почему?
              Ответить
              • 'Prop' - proposition - высказывание. Ну и тут делаются преобразования над какими-то высказываниями. А что такое 'Set' - некие вычислимые множества или че вообще такое?
                https://cs.stackexchange.com/a/80737

                > Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if p1,p2:P then p1=p2. This allows terms that are only used for proof to be erased in any code generated by Coq.

                > Set is meant for computation. It's predicative, and doesn't have proof irrelevance, which lets you do nice things like not assuming 1=2. The Set parts remain during code extraction.

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

                Я вообще ненастоящий сварщик(пусть снаут прокомментирует).
                Ответить
                • Х.з., в изначальном коде ведь о каком-то абстрактном сорте говна рассуждалось, а не об утверждениях. Поэтому я и взял Set.
                  Ответить
                  • Там рассуждалось о том, что такую-то хуитень можно на такую-то хуитень заменить в обе стороны, т.е. вполне себе некие операции над высказываниями. Если "Set" понимать как множества в математическом смысле (ZFC там, или еще чего), то тут тоже мимо.
                    Ответить
                    • Ну я представлял, что m_node -- это какая-то функция над множествами, обладающая определёнными свойствами. И вот мы можем воспользоваться этими свойствами чтобы трансформировать выражение не меняя его смысл.
                      Ответить
                    • Т.е., к примеру, мы взяли какое-то множество, определили на нём операцию сложения, пруфнули что она обладает вот этими вот описанными в твоём коде свойствами. И теперь мы можем юзать это для оптимизации кода, в котором юзается сложение.

                      И вот эта фраза "The Set parts remain during code extraction" становится очень полезной.
                      Ответить
                • > Я вообще ненастоящий сварщик(пусть снаут прокомментирует).

                  Будто я настоящий, лол. Set к ZFC и вычислимым множествам отношения не имеет, это просто название
                  самого низкого уровня в иерархии вселенных.
                  Ответить
    • > Эта вот хренотень сама доказывает, не то что какой-то там Coq.

      Питух умеет юзать что Z3, что CVC4 через coqhammer. Шах и мат, аметисты.
      Ответить
      • Так-то еще есть OpenTheory project чтоб из одних пруверов в другие переводить. http://www.gilith.com/opentheory/
        Там вот https://groups.google.com/g/metamath/c/b9k2nWOWJ-A напимер пишут

        > Yes. https://arxiv.org/abs/1412.8091 details a translation from OpenTheory to Metamath, and https://arxiv.org/abs/1910.10703 has a translation from Metamath -> MM0 -> Lean + HOL. You have to map every axiom and inference rule of the source system to a theorem of the target system, and since most of these systems have a similar idea about what math is this is usually possible, modulo some axiomatic strength mismatches, which can usually be addressed by adding (reasonable, idiomatic) axioms to the target system to make up the difference.
        Ответить
        • Почему Google Groups такое тормознутое?
          Ответить
          • В фаерфоксовой багзилле пишут, что это из-за синхронной(!) загрузки по одному(!) комменту за запрос.

            Вы все ещё хотите работать в гугле?
            Ответить
            • Достойно отдельного ГК
              Ответить
            • вангую, было так: в 2001-м году гугл купил deja news, который питухи вообще на коленке написали в 1995-м. Потом какой-то питух чото там подмандил чутка, и с тех пор так оно и работает. Внутри там ад, израиль, черти ебуца и код 2001-го года
              Ответить
              • GG это ж по сути mailing list

                У красноглазых они во все поля и грузятся из архивов мгновенно

                Pozor
                Ответить
                • Там вроде есть шлюзы к юзнету, фидо и еще всякому говну, так что возможно там отдельно хранится каждое сообщение в каком-то своем формате.

                  Понятное дело, что в 2021 нужно грузить все сообщения сразу, да еще и загзипованные (или за бротлинные даже)
                  Ответить
                  • Хм, а как это работает? Оно в реальном времени стучится куда-то, парсит ответ и рендерит страницу?
                    Ответить
                    • )я не думаю, что в реальном времени. Скорее всего они связываются с новостными серверами, и сливают данные оттуда.

                      Фидо
                      https://groups.google.com/g/fido7.ru.fidonet.today
                      Юзнет
                      https://groups.google.com/g/alt.unix
                      Ответить
              • > черти ебутся

                устали поди за двадцать пять лет-то
                Ответить
      • SMT-солверы ж не обязаны конструктивистское доказательство выплевывать, так что Coq его может не принять.
        Ответить
        • SMT-солверы работают в логике первого порядка, её Coq сожрёт, думаю даже без дополнительных аксиом. Хотя, как именно доказательство адаптируется, вопрос интересный.
          Ответить
          • А питушня с distinct variables в этом Coq как-то нативно записывается по аналогии с metamath? http://us.metamath.org/mpegif/mmset.html#distinct
            Ответить
    • Cock
      Ответить
      • Coq -- это питух по-французски.
        Ответить
        • сказал bormand
          Ответить
          • Тренируешься оформлять прямую речь?
            Ответить
            • Взял тебя в "кавычки". Проверь
              Ответить
              • Заэкранировать не забыл?
                Ответить
                • я кстати недавно гитару сам экранировал - лучше бы не экранировал.
                  Ответить
                  • Клава, неси дихлофос, опять музыканты полезли!
                    Ответить
                    • кстати да, midi-Клаву тоже заказал себе.
                      Ответить
                      • Человек-оркестр?
                        Ответить
                      • Хуйня, лучше нормальное пиано возьми, на 88 клавеш с миди-выходом.
                        Ответить
                        • А зачем? Миди клавы в пару октав вполне хватит, чтобы набросать мелодию и потом подтюнить в проге.
                          Ответить
                          • Да даже тюниьь не надо. Поставил забугорнвй синт1 наколдавал всяких генераторов залуп синусоидой и другой хуеты.
                            Ответить
                        • Потом возьму Яхама пьянину, сначало побаловаться и почему сразу хуйня.
                          Ответить
                        • У пианинки, к слову, не будет "лишних" кнопочек и крутилок, которые есть на миди клавах и синтах.

                          Всё-таки цели у этих инструментов немного разные.
                          Ответить
                          • Это и на компе можно сделать, зато играть удобно.
                            Ответить
                            • А почему миди клава не удобно играть когда у неё полноценное количество клавиш?
                              Ответить
                              • Фидбека у клавиш нету, слишком мягкие. Ну и на дешёвых реакции на силу скорость нажатия нету.

                                А у пианино кусок механики от настоящего пианино.
                                Ответить
                                • взвешенные (молоточковые), полувзвешенные и ненастоящие (не помню как правильно называются)
                                  Ответить
                                • Лол что. У миди Клавы есть фидбек и скорость нажатия. Если бы этого небыло - нахуй они нужны. Погугли про взвешенные и не взвешенные клавиши + у каждой невзвншеноц клавиши разрабатывается свой фидбек у разных фирм под своим потентом. Если бы силы нажатия небыло - нахуй тогда вообще миди клава нужна - это был бы наверное прекрасный подарок для ребенка который любит музыцировать - но ты как родитель ненавидишь всеми нервами его музыцирования. По этому для программной части именно - миди клава будет лучше, для анал-огово пианина, синты, и другая аналоговая громкая хуйня
                                  Ответить
                                  • Ты сейчас ямахи описал. У дешевой срани есть только сила нажатия.
                                    Ответить
                                    • Не совсем так. Даже у невзвешеных клавиш есть фидбек, но он конечно не молоточковый так как у разных фирм - своя технология. Да и в чем от этого плюс даёт? Только у самой дешёвой пали китайской за 3к рубасов нет фидбека, а силы нажатия ну это вообще пиздец детское сломанное пианино или самопал на ардуики от китайского долбоеба
                                      Ответить
                                  • Ну и сколько там миди клав со взвешенными?
                                    Ответить
                            • > Это и на компе можно сделать

                              Да ну... Медленно и неудобно же. А народ в реалтайме эти крутилки вертит, чтобы из потока не выходить.

                              Это как тебя заставить хоткеи мышкой прожимать.
                              Ответить
                • у него \\\\\\\\\\"мэджик квоц\\\\\\\", не ссы
                  Ответить
                • mysql_real_escape_bormand
                  Ответить
      • сказал guest6
        Ответить
    • Насколько всё-таки лисп выразительный язык
      Ответить
      • Это не лисп, этот язык называется SMT-LIB
        http://smtlib.cs.uiowa.edu/language.shtml
        Если некий язык в качестве синтаксиса испольует S-expression, это не делает его лиспом.
        Ответить
        • простите, Варвара Андреевна, завтра с родителями приду
          Ответить

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