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

    0

    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
    Fixpoint mint_add0 {N} (i k : Fin.t N) te_i te' t0 vec
                 (Ht : MInt nonCommRel N k vec (te' :: t0))
                 (Hik : k < i)
                 (Hcomm0 : trace_elems_commute te_i te')
                 {struct Ht} :
          exists t' : list TE,
              MInt nonCommRel N k (vec_append i te_i vec) (te' :: t') /\
              Permutation trace_elems_commute (te_i :: te' :: t0) (te' :: t').
        Proof with eauto.
          (* Welcome to the hell proof! *)
          remember (te' :: t0) as t_.
          destruct Ht as [k
                         |k j vec te_k t Hij Ht
                         |k j vec te_k te_j t Hij Hcomm Ht
                         ];
            [discriminate
            |replace te' with te_k in * by congruence; clear Heqt_..
            ].
          2:{ destruct (trace_elems_commute_dec te_i te_j).
              - apply mint_add0 with (te_i := te_i) (i := i) in Ht; [|lia|assumption].
                destruct Ht as [t' [Ht' Hperm']].
                exists (te_j :: t'). split.
                + swap_vec_append.
                  eapply mint_cons2...
                + apply permut_cons with (a := te_k) in Hperm'.
                  eapply permut_trans...
                  now apply permut_head'.
              - exists (te_i :: te_j :: t). split.
                + swap_vec_append.
                  apply mint_cons1 with (j0 := i); [lia|].
                  apply mint_cons2 with (j0 := j); [lia|auto..].
                + now apply permut_head'.
          }
          { inversion_ Ht.
            - exists [te_i]. split.
              + swap_vec_append.
                apply mint_cons1 with (j0 := i); [lia|].
                apply mint_cons1 with (j0 := i); [lia|].
                constructor.
              + now apply permut_head'.
            - rename te into te_j.
              destruct (PeanoNat.Nat.lt_ge_cases j i).
              2:{ exists (te_i :: te_j :: t1). split.
                  - swap_vec_append.
                    apply mint_cons1 with (j1 := i); [lia|].
                    apply mint_cons1 with (j1 := j); [lia|assumption].
                  - now apply permut_head'.
              }
              { destruct (trace_elems_commute_dec te_i te_j) as [Hte_ij|Hte_ij].
                - apply mint_add0 with (i := i) (te_i := te_i) in Ht; [|lia|assumption].
                  destruct Ht as [t' [Ht' Hperm']].
                  exists (te_j :: t'). split.
                  + swap_vec_append.
                    eapply mint_cons1...
                  + apply permut_cons with (a := te_k) in Hperm'.
                    now apply permut_head.
                - exists (te_i :: te_j :: t1). split.
                  + swap_vec_append.
                    apply mint_cons1 with (j1 := i); [lia|].
                    apply mint_cons2 with (j1 := j); [lia|assumption..].
                  + apply permut_head; [assumption|constructor].
              }
            - rename j0 into i0. cbn in H0.
              destruct (PeanoNat.Nat.lt_ge_cases j i).
              2:{ exists (te_i :: te_i0 :: te_j :: t1). split.
                  + swap_vec_append.
                    apply mint_cons1 with (j0 := i); [lia|].
                    apply mint_cons1 with (j0 := j); [lia|assumption].
                  + now apply permut_head'.
              }
              { destruct (trace_elems_commute_dec te_i te_i0).
                - apply mint_add0 with (i := i) (te_i := te_i) in Ht; [|lia|assumption].
                  destruct Ht as [t' [Ht' Hperm']].
                  exists (te_i0 :: t'). split.
                  + swap_vec_append.
                    eapply mint_cons1...
                  + apply permut_cons with (a := te_k) in Hperm'.
                    now apply permut_head.
                - exists (te_i :: te_i0 :: te_j :: t1). split.
                  + swap_vec_append.
                    apply mint_cons1 with (j0 := i); [lia|].
                    apply mint_cons2 with (j0 := j); [lia|assumption..].
                  + apply permut_head.
                    * assumption.
                    * constructor.
              }
          }
        Qed.

    Мой magnum opus. Часть доказательства про выкидывание из рассмотрения коммутирующих системных вызовов.

    Запостил: CHayT, 17 Ноября 2020

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

    • Разворецивается всего в 600 строк Gallina. Тут прекрасно всё: и копипаста, и автоматическое именование переменных с последующим переименовыванием, и сама идея хуйнуть троекратно вложенный кейз-анализ.
      Ответить
      • Ня, привет.
        Ответить
      • > троекратно вложенный кейз-анализ

        Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.

        Теорему про раскраску графа вообще чуть ли не брутфорсом доказывали...

        З.Ы. Ня, привет.
        Ответить
        • > Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.

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

        т.е. есть генератор стратегий, ему дают теорему, он выплевывает стратегию gen_strateg(theorem) -> strategy

        и есть бесконечно генерирующая теоремы херня, допустим gen_theorem(0) - одна теорема, gen_theorem(1) - другая, и так далее.

        А потом надо доказать что
        /forall (Nat x) {do_proof(gen_theorem(x), gen_strateg(gen_theorem(x))) == TRUE}
        Так делают?
        Ответить
        • Какой тип у `стратегии'?
          Вопрос я, конечно, не понял, но ответ на него скорее всего – нет. Дело в том, что стратегий в Coq нет, есть тактики, и они пишутся на совершенно другом метаязыке (Ltac), нежели теоремы (Gallina). (В Lean не так, кстати. Там по слухам гомоиконность) Поэтому написать теорему про тактику в Coq – это как написать функцию, принимающую как аргумент макрос, в C.
          Ответить
          • Почему у тебя такие кавычки? Ты что, на m4 пишешь?
            Ответить
          • > Какой тип у `стратегии'?

            У `стратегии' тип это список правил, по которым некая питушня что-то набрасывает в качестве пруфа теоремы, пытаясь это доказать. Ну ок, пусть будет `тактики', а не `стратегии'. Почему б не доказывать, что такие-то тактики, генерируемые на основе конкретных теорем, всегда успешно доказывают теоремы, сгенеренные таким-то способом? Т.е. доказать что генератор тактик всегда для такого семейства теорем, генерируемых таким способом, генерит такие тактики, которые всегда доказывают соотв. теорему
            Ответить
            • См. пост ниже. Ты сейчас индукцию изобрёл. Если упростить, то `теорема' – это тип, а доказательство – это терм, имеющий данный тип. И то, и другое можно параметризовать числом (т.к. в Coq нет особой разницы между типами и термами), и тогда получится твоя питушня.
              Ответить
          • > Дело в том, что стратегий в Coq нет, есть тактики, и они пишутся на совершенно другом метаязыке (Ltac), нежели теоремы (Gallina).

            А почему не сделать это одним языком? Чтобы можно было доказывать доказуемость некоего множества теорем такими-то генеренными из теорем тактиками.
            Ответить
            • > А почему не сделать это одним языком?

              Нянужно! Gallina имеет крайне строгую семантику, поскольку она является доверенной по принципу де Бройля. Поэтому в ней не может быть никаких свистелок и перделок, и всё крайне ограничено и консервативно. А Ltac – не доверенный язык, в нём можно сколько угодно фич пилить и ломать семантику как хочешь. Поэтому его используют для автоматизации, т.к. удобно.
              Ответить
              • > Gallina имеет крайне строгую семантику, поскольку она является доверенной по принципу де Бройля. Поэтому в ней не может быть никаких свистелок и перделок, и всё крайне ограничено и консервативно. А Ltac – не доверенный язык, в нём можно сколько угодно фич пилить и ломать семантику как хочешь.

                Ну так почему б не написать транспилер из Ltac в Gallina? В самой Gallina сделать тьюринг-полноту с гомоиконами, и пусть само с собой там метушится, доказывая доказуемость.
                Ответить
                • > Ну так почему б не написать транспилер из Ltac в Gallina?

                  Принципиально нявозможно. Ltac – Тьюринг полный, Gallina – нят.
                  Ответить
                  • > Gallina – нят.

                    Зачем? Зачем? Я могу описать функцию, принимающую стейт брейнфака возвращающую новый стейт брейнфака плюс номер шага, и через Ltac я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота. Ради чего это?
                    Ответить
                    • Зачем? Зачем?

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

                      > я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота

                      Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
                      Ответить
                      • > Зачем? Зачем?

                        Чтобы доказывать применимость таких-то стратегий (стратегий, построенных по определенному шаблону) к доказыванию таких-то теорем, построенных по определенному шаблону. Сделать еще какую-то алгебру стратегий, что такие-то стратегии можно упростить, сведя их к таким-то, а вот такие стратегии это частные случаи таких стратегий. Более высокий уровень абасракции короче.

                        > Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.

                        Почему не будет? Так мы пробуем доказать небесконечность цикла, и раз мы так можем делать, это и есть тьюринг-полнота, мы интерпретируем брейнфак. Какая разница, зависнет ли у меня Ltac генерящий питушню для Gallina, или Gallina само себе питушню генерить будет и зависнет?
                        Ответить
                        • > Какая разница, зависнет ли у меня Ltac генерящий питушню для Gallina, или Gallina само себе питушню генерить будет и зависнет?

                          Огромная. [1] [2]

                          [1] https://govnokod.ru/26981#comment579147
                          [2] https://govnokod.ru/27333#comment620156

                          Поднимаю говно-Хирш
                          Ответить
            • Например, если у меня есть генератор теорем, он их генерирует бесконечное множество (теорема1, теорема2, теорема3 и так далее). Есть генератор тактик, тактика1 доказывает теорему1, тактика2 доказывает теорему2 и так далее. И надо доказать, что все такие генеретные тактики доказывают все такие генеренные теоремы. Можно конечно как-нибудь обобщить само множество теорем в некую одну теорему, и сделать одну общую тактику, которая б доказывала эту одну теорему, но это как-то неправильно. Почему это не в рамках единого языка?
              Ответить
              • > Например, если у меня есть генератор теорем, он их генерирует бесконечное множество (теорема1, теорема2, теорема3 и так далее).

                В переводе на петушиный: у меня есть функция F(n : nat), возвращающая термы в универсуме U + 1.

                > Есть генератор тактик, тактика1 доказывает теорему1, тактика2 доказывает теорему2 и так далее.

                В переводе на петушиный: у меня есть функция G от nat, которая возвращает терм типа F(n) в универсуме U.

                > И надо доказать, что все такие генеретные тактики доказывают все такие генеренные теоремы.

                В переводе на петушиный: надо найти определение G.

                > Почему это не в рамках единого языка?

                Просто переформулировав пробему как показано выше, ты и сделаешь это в рамках одного языка.
                Ответить
                • Нужно просто понять, что в Coq на самом деле нет ни теорем, ни доказательств. И то, и другое – функции.
                  А тактики – это макроязык такой.
                  Ответить
                • > Просто переформулировав пробему как показано выше, ты и сделаешь это в рамках одного языка.

                  Переформулировать-то можно, это понятно. Но так не выйдет доказать что-то относительно неких свойств стратегий, применимости определенных стратегий к доказыванию определенных типов теорем и так далее. Окажись стратегий частью самого языка для описания теорем, это можно было бы делать.
                  Ответить
                  • Тактики в Coq сугубо опциональны, и можно доказывать всё вообще без них (Agda2 братишки так и делают). Поэтому доказывать какие-то свойства про них — занятие довольно бесполезное. Есть некое подобие "стратегий", называется induction scheme. (Например: https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#rectS) Ну так это просто функция высшего порядка. Про неё да, в теории что-то можно доказать.
                    Ответить
                    • Но вообще, есть ли смысл доказывать нечто о том, что какие-то штуки доказываются такими-то подходами? Т.е. что если теорема (или множества теорем, которые таким-то образом механически конструируются) так-то и так-то устроена, то доказать, что доказательства, конструируемые вот по такому шаблону эту теорему (или множество теорем) будут доказывать.
                      Ответить
                      • > есть ли смысл доказывать

                        В этом вроде и идея ltac. Нет никакого смысла доказывать, что он правильно работает в общем случае или для каких-то классов теорем. Достаточно просто проверять сгенерённые им пруфы для конкретных теорем которые тебе и нужно доказать.
                        Ответить
                        • А зачем тогда специальный язык ltac? Тогда можно и через какой-то питон пруфы кодогенерировать. Какие преимущества у ltac по сравнению с условным питоном, если его прикрутить к этому coq чтобы питон там что-то набрасывал в качестве пруфа?
                          Ответить
                          • Основное преимущество, я так понимаю, в нотациях. Что можно невозбранно лепить на нём DSL и математику косплеить.

                            А технически и питон и даже пхп сойдут, конечно.
                            Ответить
                            • На любой тьюринг-полной скриптушне можно налепить всяких нотаций, сделать DSL и косплеить математику.
                              Ответить
                              • На большинстве тьюринг-полной скриптушни DSL выглядят как говно, если честно.
                                Ответить
                                • +++++
                                  Ответить
                                • Говорят, самая лучшая скриптушня для DSL - LISP. Почему вместо ltac не взяли LISP?
                                  Ответить
                                  • Ты ещё спроси, зачем линкер GHC работает с помощью своего собственного стековрого языка.
                                    Причина: ты что, пёс, я Computer Scientist.

                                    Ну а на деле: люди бы ебанулись на LISP паттерн-матчинг типов пилить. Да в нём и нету нормального паттерн-матчинга.
                                    Ответить
                            • Нотации — они в Vernacular, а не в Ltac, ЕМНИП. Основное преимущество, что в нём есть backtracking a la Prolog, и он знает всё про термы Gallina, в т.ч. умеет их красиво матчить. Некоторые требовательные к производительности тактики на Ocaml там написаны. В теории можно и питон звать, наверно.
                              Ответить
                              • А этот Ltac знает Gallina на уровне некоего AST, или он в своем составе содержит парсер синтаксиса этой Gallina и потом текстушню какую-то набрасывает для пруфанья, которая прогоняется потом через парсер для Gallina в самом Gallina-интерпретаторе и там как-то верифицируется?
                                Ответить
                                • Как я понимаю, он её знает прямо-таки на уровне термов, а не анскилльного AST. По крайней мере, информация о типах в нём есть.
                                  Ответить
                                  • P.S. И это делается без парсера, ибо coqtop умеет в holes. Т.е., грубо говоря, компилятор посреди компиляции останавливается и передаёт тактике управление, чтобы она там что-то догенерила. Это вам не анскилльные макросы.
                                    Ответить
                                    • > Т.е., грубо говоря, компилятор посреди компиляции останавливается и передаёт тактике управление, чтобы она там что-то догенерила.

                                      Тогда еще больше причин делать всю петушню в рамках одного языка, а не разграничивать на две хрени, которые там еще как-то перепихиваются в процессе.
                                      Ответить
                                      • С чего такой вывод? Компилятор Coq не написан на Coq, just sayin'.
                                        Ответить
                                        • > Компилятор Coq не написан на Coq, just sayin'.

                                          Я ведь тогда не могу в Coq доказать что Coq(Coq(x)) проверяет x и считает этот пруф верным или не верным тогда же, когда, когда это делает Coq(Coq(Coq(x))), даже не смогу это объявить как аксиому(если это недоказуемо из-за какой-то там неполноты), да? И что в этом хорошего?
                                          Ответить
                                          • И вообще, взять например идею с partial evaluation, futamura projection. Говоря простым языком, можно рассматривать Тьюринг-полные языки как некие математически формализуемые питули, и можно сделать декларативное описание одного языка lang1, и декларативное описание другого языка lang2, и придумать функцию gen_transl(dst, src, target) т.е. gen_transl(lang1, lang2, lang1) сгенерит код на языке lang1 который транслирует (или компилирует) язык lang2 в lang1, и все это доказать. Вот https://habr.com/ru/post/47418/ там про это немного побольше написано. Так вот, можно таким вот образом расширять возможности некоторого языка, добавляя в него новые фичи. И если допустим язык gallina формализуем и формализован в gallina, можно взять какой-нибудь другой язык для теорем-прувинга и сделать его транслятор в gallina, и наоборот.
                                            Ответить
                                            • Конечно же нужен язык с гомоикнностью. Нужно сделать на самом языке систему символьных вычислений (ССВ) над его же кодом/AST и используя эту ССВ иметь возможность например выводить определенные свойства реализации (для проведения формальной верификации, доказательства корректности, как например с использованием Frama-C с применением SMT-решателей, Coq, HOL и всякого такого), использовать эту ССВ для целей вроде суперкомпиляции/супероптимизации. Или чтобы циклы например анроллить, типа вот мы задаем каким-то там макаром, что вот тут у нас цикл, и говорим нашей ССВ что вот наанроль его вот таким образом, и потом будет там наанроленный цикл. Или реализовывать свои domain-specific оптимизации для каких-нибудь бигинтов. Или эту же ССВ можно попросить, чтобы например она трансформировала код некой функции таким образом, чтобы она вместо int принимала long long int, чтобы это было еще в IDE интегрировано нормально, и чтобы такую кодогенерацию при желании даже в рантайме можно было бы делать, если с собой в рантайм тащить еще JIT с VM (т.е. тащить какую-то жирную хрень типа JVM) и AST, удобный для трансформации. Можно сделать что-то вроде тех же Java оптимизаций в рантайме, рантайм-профилирование и трансформация кода в процессе...
                                              Ответить
                                              • Или даже profile-guided optimisation (PGO) потом сделать на основе собранной статистики, т.е. вот типа набрали мы статистики при выполнении кода в VM и потом использовали ее чтобы полностью четко скомпилировать в бинарник, чтоб без VM все выполнялось. Чтобы можно было бы вводить свои правила приведения типов, и на основе этого ССВ могла бы выводить тип. Или чтоб можно было сделать язык с нестрогой типизацией поверх существующего AST и чтоб в рантайме при каких-нибудь тестовых прогонах производился мониторинг того, что с какими типами вызывается (т.е. к каким фактически типам там приводится все в динамике) и потом чтобы на основе этого можно было бы расставить эти самые типы в реальном коде. Т.е. если у нас будет функция без указания типа, и эта функция в одном месте вызывается допустим с типом int, а в другом с типом float, то можно сделать две специализированные под этот тип реализации, которые бы вызывались конкретно в тех местах, где собственно и происходит вызов той функции с таким-то там типом.
                                                Ответить
                                              • Остапа понесло.
                                                Ответить
                                                • > Остапа понесло.

                                                  Это копипаста, которую я хуй знает когда написал.
                                                  Ответить
                                                  • > Это копипаста, которую я хуй знает когда написал.

                                                    Это вореции?
                                                    Ответить
                                                    • > Это вореции?

                                                      Нет. Это одна моя старая идея метаязыка для конструирования языков, который будет сам на себе написан, и чтоб всё через частичные вычисления, проекции Футамуры и формальные доказательства там работало, и чтобы это был один единый язык с Тьюринг-полнотой, самомодифицирующийся в процессе исполнения (система переписывающих правил чтоб, грубо говоря запуск языка это самопереписывание графа, полученного из AST с чтением из STDIN выплевыванием чего-то из STDOUT). И на этой алгебре самопереписывания уже б вводились всякие теории типов.
                                                      Ответить
                                                      • "<...> И на этой алгебре самопереписывания уже б вводились всякие теории типов" -- сказал j123123, докуривая косяк, и начал писать код на сишке под микроконтроллеры.
                                                        Ответить
                                                        • > и начал писать код на сишке под микроконтроллеры.

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

                                          Раз у Gallina нет тьюринг-полноты и в нем нельзя написать Gallina-интерпретатор, в рамках Gallina нельзя что-то доказывать о том, как что-либо делается самой Gallina для доказывания чего-либо, верно? И нельзя делать эти проекции Футамуры, о которых я выше написал.
                                          Ответить
                                          • https://www.youtube.com/watch?v=06dNw_tsv_c

                                            Т.к. Gallina не Тьюринг-полна, в теории может и можно написать её интерпретатор на не-Тьюринг полном языке. Напиши, проверишь.
                                            Ответить
                                            • > не-Тьюринг полном языке

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

                                                https://github.com/orangeduck/CPP_COMPLETE


                                                https://github.com/pfultz2/Cloak/wiki/Is-the-C-preprocessor-Turing-complete%3F

                                                >Now this example is limited to 10 repeats, because of limitations of the counter. Just like a repeat counter in a computer would be limited by the finite memory. Multiple repeat counters could be combined together to workaround this limitation, just like in a computer. Furthermore, we could define a FOREVER macro:

                                                #define FOREVER() \
                                                    ? \
                                                    DEFER(FOREVER_INDIRECT) () ()
                                                #define FOREVER_INDIRECT() FOREVER
                                                // Outputs question marks forever
                                                EVAL(FOREVER())


                                                >This will try to output ? forever, but will eventually stop because there are no more scans being applied. Now the question is, if we gave it an infinite number of scans would this algorithm complete? This is known as the halting problem, and Turing completeness is necessary to prove the undecidability of the halting problem. So as you can see, the preprocessor can act as a Turing complete language, but instead of being limited to the finite memory of a computer it is instead limited by the finite number of scans applied.
                                                Ответить
                                                • Ну не... Проги на препроцессоре всё-таки всегда ограничены каким-то заранее известным числом шагов. Вечный цикл там пильнуть невозможно.

                                                  Т.е. это явно более узкий класс программ чем в типичном "тьюринг-полном" языке, который ограничен только памятью.
                                                  Ответить
                                                  • > Т.е. это явно более узкий класс программ чем в типичном "тьюринг-полном" языке, который ограничен только памятью.

                                                    Ну как бы смотря как ты определяешь"класс программ". Если "тьюринг-полный" язык органичен конечной памятью, доказательство зависания для него можно всегда доказать через https://ru.wikipedia.org/wiki/Нахождение_цикла

                                                    Рассмотрим функцию "шаг интерпретатора"
                                                    state step(state from)
                                                    {
                                                      делаем некую питушню в зависимости от state,
                                                      и вернем новый state
                                                    }

                                                    Если state это некая хуита, занимающая конечный кусок в оперативной памяти (нет никаких указателей и выделений памяти) то если бесконечный вызов хуйни в хуйню
                                                    state st = {someshit};
                                                    while(true)
                                                    {
                                                      st = step(st);
                                                    }

                                                    То значение `st' обязательно будет повторяться т.к. количество состояний конечно.
                                                    И если такая программа выводит что-то в stdout допустим(но ничего не получает извне), то она сводима к:
                                                    printf(некая_хуйня);
                                                    {
                                                      while(true)
                                                      {
                                                        printf(еще_какая-то_хуйня);
                                                      }
                                                    }
                                                    Ответить
                                                    • Т.е. что тут получается. Результат работы зависающей программы на "тьюринг-полном языке с конечной памятью", которая что-то выводит в stdout и ничего не принимает в stdin (или принимает конечную известно какую строку, тогда такая программа сводима к программе, где эта строка тупо в сам код вшита) может быть описана как две конечные строки - строка начальной хуйни, и строка повторяющейся хуйни. Строка начальной хуйни и/или строка конечной хуйни может естественно быть пустой. А две строки конечной длины всегда можно вывести за конечное число шагов.
                                                      Ответить
                                                      • > (или принимает конечную известно какую строку, тогда такая программа сводима к программе, где эта строка тупо в сам код вшита)

                                                        или принимает бесконечную периодическую строку, такую строку тоже можно в код вшить.
                                                        Ответить
                                            • > Т.к. Gallina не Тьюринг-полна, в теории может и можно написать её интерпретатор на не-Тьюринг полном языке.

                                              Некий условный 1 шаг интерпретатора Gallina однозначно можно написать на Gallina т.к. 1 шаг брейнфака написать там точно можно. А вот "вызывать" интерпретатор бесконечное количество раз в Gallina нельзя, и это может сделать только некая внешняя хрень, которая что-то доказывает в терминах Gallina. Как-то так
                                              Ответить
                                    • > Это вам не анскилльные макросы.

                                      https://archive.jlongster.com/Lisp--It-s-Not-About-Macros,-It-s-About-Read
                                      Ответить
                                      • Как было на самом деле: протоцепепе - ЛИСП 50-80 гг. C++ 80-90 гг. Haskell - новая версия цепепе. 90-00 гг. С точки зрения лиспопетушка сначала был Хаскель, в следующей версии он деградировал до цепепе, а в лиспопетушином будущем цепепе деградирует до лиспа.

                                        А я все ломал голову, как человек может так ненавидеть будущее, так привязаться к прошлому, что пишет на лиспе? Но для лиспопетушка-контрамота лисп - это и есть будущее. А дальше ВВ2, индустриальная контрреволюция, религиозные войны, рабовладельческий строй, отрастание хвостов и подъем на деревья. Скай из зе лимит!



                                        На самом деле в Lisp и Scheme всё очень печально с pattern-matching'ом, и всякие CSшни в современном мире без него пилить никому не охота.
                                        Ответить
                                        • > На самом деле в Lisp и Scheme всё очень печально с pattern-matching'ом

                                          В чем именно заключается печальность? Что мешает сделать DSL для pattern-matching'а?
                                          Ответить
                                          • > В чем именно заключается печальность?

                                            Его там нет. (Ну может в современных диалектах появился)

                                            > Что мешает сделать DSL для pattern-matching'а?

                                            Так сделали, само собой. Но когда я открываю доки по pcase, я плачу, настолько он уродливый.
                                            Ответить
                                            • > когда я открываю доки по pcase, я плачу, настолько он уродливый.

                                              https://docs.racket-lang.org/reference/match.html такой паттерн матчинг норм? Покажи реальный пример хорошего паттерн-матчинга в каком-то язычке.
                                              Ответить
                        • > Нет никакого смысла доказывать, что он правильно работает в общем случае

                          Более того, с его помощью легко запилить что-то неправильное. Ключевые слова Qed. и Defined. потом всё перепроверяют.
                          Особенный багор, когда ты ltac'ом запилил огромный fixpoint, а он оказался не структурным, т.к. auto где-то подхватило рекуррентный вызов ))) Приходится во избежание этого гипотезы чистить вилкой.
                          Ответить
        • Вообще, похоже на простую индукцию по x, только с кучей бессмысленных врапперов каких-то. `Стратегия' и есть доказательство.
          Ответить
          • А индукцию по стратегиям генеренным такой-то метушней можно сделать?
            Ответить
            • Индукция – это тупо структурно-рекурсивая функция в Gallina. Поэтому нет, метушню в неё не засунуть.
              Ответить
        • Как ты попал в этот тред?
          Ответить
          • Смотрел список говнокодов снаута, нашел этот говнокод.
            Ответить
    • Это на каком язычке?
      Ответить
    • Давно вуз окончил?
      Ответить
    • А были ли успешные попытки прикручивания к Coq нейросетей, чтоб оно само там применяло стратегии и как-нибудь доказывалось?
      Ответить
      • Попытки были (coqhammer, gamepad), насколько успешные не знаю, мне они не помогли. +Я знаю, что сейчас несколько исследовательских групп что-то новое ковыряет.
        Ответить
        • Вообще, на мой взгляд, самое трудное — это правильные определения. Если в них есть баг или они недостаточно специфичны, то нейросеть просто в какой-то момент встанет или натворит непонятной херни. И потом фиг поймёшь, то ли искуственный идиот что-то напутал, то ли твои определения говно. Ручное доказательство это конечно долго, но зато когда приходишь к какой-то неразрешимой херне, понимаешь, что к чему. Поэтому в данном случае я даже тактику induction не использовал, чтобы она какой-нибудь ненужной херни в гипотезу индукции не подхватила, и запилил индукцию вручную.
          Ответить
          • Но ты ведь тоже нейросеть.
            Ответить
            • Да, но я та же нейросеть, которая ставит задачу и которая будет это дебажить.
              Ответить
              • Ну так разреши нейросети формулировать задачу и оценивать результат.
                Ответить
        • tactician ещё из нового. Правда мне он всегда подсказывает: "юзай firstorder, bro", а потом, "ну хер знает". Какой AI )))
          Ответить
          • У него с самого начала была какая-то тактика.
            Ответить
            • Гроссмейстер вошел в зал. Он чувствовал себя бодрым и твердо знал, что первый ход e2 — e4 не грозит ему никакими осложнениями. Остальные ходы, правда, рисовались в совершенном уже тумане, но это нисколько не смущало великого комбинатора.
              Ответить
    • Ебать поехавший.
      Ответить

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