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

    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
    Короче, размышлял я как-то на тему того, как надо делать правильный
    теорем прувер, а не питушню всякую заедушную. Вот взять тот же Metamath -
    там какие-то непонятные distinct правила для хуиты, что надо какие-то там
    disjoint переменные, вот тут https://groups.google.com/g/metamath/c/M2dUfFATxD8
    про это подробнее сказано.
    
    Есть вот еще Metamath zero https://github.com/digama0/mm0 и это вот кажется ближе
    к тому, что мне нравится.
    Например вот https://github.com/digama0/mm0/blob/master/examples/assembler.mm1
    тут есть какая-то теорема про ELF хедер. Это вот определение ELF идентификатора
    
    local def ELF_IDENT_s: string =
    $ ,0x7f ': ,"E" ': ,"L" ': ,"F" ':
      _x02 ': _x01 ': _x01 ': _x00 ': _x00x8 $;
      
    и там еще какой-то такой хуйней описывается то, где там точка входа записана в заголовке,
    еще separation logic есть какая-то.
    Но вот если почитать спецификацию для этого mm0 языка
    https://github.com/digama0/mm0/blob/master/mm0.md :
    
    pure means that this sort does not have any term formers. It is an uninterpreted domain which may have
      variables but has no constant symbols, binary operators, or anything else targeting this sort. If a sort has
      this modifier, it is illegal to declare a term with this sort as the target.
    
    strict is the "opposite" of pure: it says that the sort does not have any variable binding operators. It is illegal
      to have a bound variable or dummy variable of this sort, and it cannot appear as a dependency in another
      variable. For example, if x: set and ph: wff x then set must not be declared strict. (pure and strict are not
      mutually exclusive, although a sort with both properties is not very useful.)
    
    provable means that the sort is a thing that can be "proven". All formulas appearing in axioms and theorems
     (between $) must have a provable sort.
     free means that definitions and theorems are not allowed to use dummy variables with this sort.
    
    то кажется мне, что слишком это сложно. Надо проще это всё сделать, по принципу какой-нибудь
    хрени типа SKI кобенационного исчисления. Т.е. допустим аксиома для модус поненса
    
    AXIOM
    %A
    P P $IMP %A %B
    _
    %B
    
    т.е. если мы матчим некую хуйню "%A" и некую хуйню "P P $IMP %A %B" где %A и %B это некая
    срань, которая может быть "что-то" "P чтото чтото" или там "P чтото P чтото чтото" и т.д.
    ну короче P означает что там две какие-то хуйни, вот как в той хрени https://govnokod.ru/27420
    то можем дополнительно синтезировать высказывание "%B"
    
    А теоремы это negj композиции из аксиом и других теорем. Типы можно прикручивать через какую-то хуйню
    типа если арифметику Пеано описывать, тип можно так что-то нахуевертить аксиому, ну типа
    
    Определение что ZERO это натуральное число.
    AXIOM
    _
    P NAT ZERO
    
    Что если инкрементнуть натуральное, будет тоже натуральное (S это функция следования)
    AXIOM
    P S %A
    P NAT %A
    _
    P NAT P S %A
    
    В общем надо бы подумать, как там запилить максимально простой и эффективно расширяемый язык для
    доказывания всякой хуйни.
    
    Смотрел Coq - какая-то ебаная перепитушня со всякими там типами-хуипами и какими-то
    блядь рекурсиями. Хер поймешь, как эта вся дрнсня работает. Меня ваши типы не ебут
    совершенно, я хочу сам свои типы конструировать, а не полагаться на какую-то невнятную
    ебанину.

    Запостил: j123123, 05 Июля 2021

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

    • И что вообще с этими пруверами происходит? Куча какой-то разрозненной хуиты. Какие-то Coq, Lean, Isabelle/HOL какой-то еще, какие-то Идрисы-хуидрисы. Почему так много этой хрени наплодили, но никакая из них толком не вылезла за пределы всякой там академически-ресерчерской хуйни?
      Ответить
      • > почему

        Потому что большинство устраивают собачки в ПХП. К счастью или к сожалению.
        Ответить
        • К счастью.

          1. Заказчикам не приходится нанимать докторов наук по кокам и хачкелям, чтобы реализовать задачу, которую может сделать школьник.

          2. У технологий повышается "порог вхождения" в мир. Если ещё 40 лет назад можно было скормить ничего не подозревающему человеку assемблер и шишку, то сейчас мало кто захочет изучать что-то менее человечное, чем питон и шишарп. Чем дольше мы ждём, тем меньше интереса будет у людей к пердольной питушне.

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

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

      Нясколько понямаю, в coq хотели дать тебе няпротиворечивую систему, в которой ты ня можешь отстрелить себе ногу. Числа, логические операторы и т.п. там строятся из очень простых вещей. Да, ня поверхности выглядит сложня и страшня, но под капотом там по сути просто лямбды да их типы ^_^

      А твоя версия с няксиомами -- это как няшная с её UB'ами: някаких подушек безопаснясти, только хардкор. Конпелятор ня сможет проверить, что твоя няксиоматика ня поехавшая. Тебе придётся как-то самому вручную доказывать, что новая няксиома ничего ня портит.

      З.Ы. Да, в coq, нясколько я понямаю, вообще нявозможно добавить реальную няксиому. Твой пруф будет просто импнякацией при условии что эта "няксиома" верна. Сам движок ня верит в её истинность.
      Ответить
      • > Нясколько понямаю, в coq хотели дать тебе няпротиворечивую систему, в которой ты ня можешь отстрелить себе ногу.

        Нет доказательств непротиворечивости coq. Есть столько же оснований доверять непротиворечивости кем-то написанным аксиомам, как и доверять непротиворечивости coq. В самом coq доказать непротиворечивость coq невозможно, потому что вторая теорема Гёделя о неполноте.
        Если формальная арифметика S непротиворечива, то в ней невыводима формула, содержательно утверждающая непротиворечивость S.

        > А твоя версия с няксиомами -- это как няшная с её UB'ами: някаких подушек безопаснясти, только хардкор.

        А как мне помогает coq? Если я в coq описываю некую свою хуйню, например аксиомы из theory of array https://smt2012.loria.fr/paper1.pdf
        p=r    =>  read(write(a,p,b),r)=v
        
        ¬(p=r) =>  read(write(a,p,b),r)=read(a,r)


        These axioms state that storing the value v into an array a at index p and subsequently reading a’s value at index q results in the value v if the indices p and q are identical. Otherwise, the write operation does not influence the result of the read operation.

        Каким образом coq защитит меня, если я при переписывании этих аксиом где-нибудь ошибусь?
        Ответить
        • Обычно там ня вводят аксиомы без пиздец-пиздец няобходимости.

          Т.е. тот же массив ты мог бы построить в виде списка или дерева. И ня освнове этого вывести его свойства. И тогда ты можешь ня бояться, что они записаны няправильно. Ты просто не сможешь их доказать.

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

            Для этого тебе надо построить из чего-то список или дерево (или чтобы список или дерево уже было). А никаких списков и деревьев может не быть. И вообще, может лучше я сначала построю theory of array, и потом поверх нее построю списки и деревья.

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

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

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

                      По сути, на практике ты будешь доказывать что-то в духе изоморфизма конструкций твоего DSL'а и инструкций какого-нибудь arm'а или x86. А посрединке между ними будут всякие теории о массивах, деревьях, лямбдах и т.п. В каком из базисов ты это делаешь -- не так уж важно, их бесконечно много. Лишь бы выбранный базис не позволял доказывать хуйню на ровном месте.
                      Ответить
                      • > Ну а зачем тебе более сложный базис, в котором есть "лишние" аксиомы, если можно пользоваться более простым, в котором их нет?

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

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

                              Ну не совсем так. Допустим, я построила массивы на брейнфаке (х.з. как это делать, если честно) и доказала несколько теорем о них (те самые утверждения, что ты привёл как аксиомы).

                              Теперь я могу эти теоремы юзать чтобы доказать что-то более интересное и высокоуровневое. Что сортировка сортирует, к примеру. И ни я ни тайпчекер не будем углубляться в детали реализации этих массивов пока не понадобится какая-то новая хитровыебанная теорема о них.

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

                              Т.е. базис -- это просто базис.
                              Ответить
                              • > Допустим, я построила массивы на брейнфаке (х.з. как это делать, если честно)

                                Много способов есть. Можешь переписать Coq на брейнфак и в Coq построить массивы.
                                Ответить
        • Почитай про calculus of constructions если интересно. Там ядро совсем простенькое.
          Ответить
          • Это исчисление высказываний называется. Кстати, у тебя модус поненс, проверь.
            Ответить
            • Ня путай, это нямножко другое.
              Ответить
              • ня, пока
                Ответить
              • Почему?

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

                Исчисление конструкций — теория типов на основе полиморфного λ-исчисление высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — \lambda P\omega.

                Хотя, ладно, понятно почему.
                Ответить
        • есть доказательство сильной нормализации для исчисления конструкций. ядро кока это исчисление конструкций (плюс дополнительная хуерга), если допустить, что в реализации нет ошибок, то все хорошо, а если не делать этого, то так можно к любому пруверу придраться
          Ответить
          • https://core.ac.uk/download/pdf/82038778.pdf
            §5.4
            Ответить
          • > есть доказательство сильной нормализации для исчисления конструкций

            А это доказательство на самом Coq есть? Вот есть всякие примеры, когда из Coq синтезируют некоторые корректные по построению программы, кто-нибудь смог на Coq сгенерить корректный по построению Coq и его потом им же опять так пересобрать? (т.н. раскрутка компилятора)
            Ответить
            • Немного не понял вопрос. Если он про доказательство сильной нормализации для всего системы, которая в ядре используется, то такого на коке нет, потому что из нее следует непротиворечивость. Для разных подмножеств (в том числе, для чистого CoC без расширений) такое есть: https://github.com/coq-contribs/coq-in-coq
              Ответить
              • > Если он про доказательство сильной нормализации для всего системы, которая в ядре используется, то такого на коке нет, потому что из нее следует непротиворечивость

                Да, это понятно, я о том, чтобы добавить аксиом, чтобы доказать непротиворечивость того Coq, где этих аксиом нет.

                Когда некие математики доказывали эту сильную нормализацию для исчисления конструкций, они опирались на какие-то аксиомы, правила вывода. Если эти аксиомы существуют, их можно записать в Coq тоже как некие аксиомы, тут я не вижу противоречия. Или эти аксиомы невыразимы в Coq? Как такое может быть?

                Если рассматривать некую формальную систему "X" в которой невыводима непротиворечивость "X" но нам надо доказать ее непротиворечивость, мы создаем некую расширенную формальную систему "X++" в которой доказуема непротиворечивость "X" (но непротиворечивость "X++" уже недоказуема). Похоже что это т.н. метасистемный переход
                Ответить
                • https://pat.keldysh.ru/~roman/doc/Turchin/1980-Turchin--The_use_of_metasystem_transition_in_theorem_proving_and_program_optimization.pdf


                  хмм...
                  Ответить
                  • Допустим, описываем мы натуральные числа. Сначала говорим что 0 - Nat (да, некоторые ма-те-ма-тики считают что Nat начинается с 1, но у меня будет Nat с нулем)
                    типа
                    (&AX nat_0_ax ( )
                      (
                      )
                      (
                        Nat 0
                      )
                    )
                    
                    
                    Будет инкремент. Например, если что-то натуральное, то его инкремент это натуральное
                    
                    (&AX nat_inc ( @a )
                      (
                        // ( @a ) - этого тут не требуется
                        ( nat @a ) // достаточно утверждения что оно натуральное
                      )
                      (
                        nat inc @a // и тогда его инкремент это тоже натуральное
                      )
                    )
                    
                    Такая аксиома зожимает бесконечные вореанты аксиом типа
                    
                    (&AX nat_inc1 ( )
                      ( )
                      (
                        nat inc 0
                      )
                    )
                    (&AX nat_inc2 ( )
                      ( )
                      (
                        nat inc inc 0
                      )
                    )
                    (&AX nat_inc3 ( )
                      ( )
                      (
                        nat inc inc inc 0
                      )
                    )
                    ...
                    Что говорит "мы можем в любой теореме записать что
                    inc 0 это натуральное, inc inc 0 это натуральное и так далее"
                    
                    Но если просто записать бесконечную хуйню из nat inc inc ... 0
                    то нельзя будет определить аксиомы для сложения в общем виде
                    Будет хуйня типа
                    
                    ( &AX nat_add_0_0 ( )
                      ( )
                      (
                        nat add
                          0
                          0 
                      )
                    )
                    
                    ( &AX nat_add_0_1 ( )
                      ( )
                      (
                        nat add
                          0
                          inc 0
                      )
                    )
                    
                    
                    ( &AX nat_add_1_0 ( )
                      ( )
                      (
                        nat add
                          inc 1
                          0
                      )
                    )
                    Т.е. бесконечность определений, что 0+0, 0+1, 1+0 итд - натуральное
                    
                    
                    А с такой общей аксиомой можно сказать это же в общем виде
                    
                    ( &AX nat_add_a_b ( @a @b )
                      (
                        ( nat @a )
                        ( nat @b )
                      )
                      (
                        nat
                          add
                            @a
                            @b
                      )
                    )
                    Ответить
                    • Так тут можно сделать чтоб гомоиконность аксиома могла в аргументе принимать аксиому (возможно даже себя же) тупо как список термов, и чтоб так синтезировалась другая аксиома и добавлялась в список аксиом. Что-то типа

                      ( &AX meta_nat_inc ( @ax_name @ax_name2 @a )
                        (
                          ( // матчим аксиому
                          
                            \( \&AX @ax_name \( \)
                              \( \)
                              \(
                                \nat @a
                              \)
                            \)
                            
                          )
                          
                          ( wfan @ax_name )  // это значит что well-formed axiom name
                          ( wfan @ax_name2 ) // чтоб туда какая-то хуйня не пролезла
                          ( CHK @a ) // нужно еще как-то эту @a проверять, чтобы там хуйня не пробралась
                        )
                        (
                      
                          // и тут синтезируется новая аксиома
                          \( \&AX @ax_name2 \( \)
                            \( \)
                            \(
                              \nat \inc @a
                            \)
                          \)
                      
                        )
                      )

                      Т.е. что если есть аксиома
                      ( &AX ax_0 ( )
                        ( )
                        (
                          nat 0
                        )
                      )

                      то можно синтезировать аксиому
                      ( &AX ax_1 ( )
                        ( )
                        (
                          nat inc 0
                        )
                      )

                      а потом еще и аксиому
                      ( &AX ax_2 ( )
                        ( )
                        (
                          nat inc inc 0
                        )
                      )

                      и так до бесконечности. Надо чтоб метасистемный переход.
                      Ответить
                • Ну я в это глубоко не вникал, но подозреваю, что CiC можно использовать для доказательтва непротиворечивости CoC (учитывая наличие Coq in Coq). В бумажных первоначальных доказательствах сторили модели в цермело-френкеле (мб с аксиомой выбора или чем-то с кардиналами, нужно внимательно посмотреть)
                  Ответить
    • Вот какой-то такой синтаксис пока придумал для определения аксиом, надо будет подумать над этим
      http://us.metamath.org/mpeuni/wn.html
      ( &AX ( @a )
        (
          ( & wff @a )
        )
        (
          & wff
            & not @a
        )
      )
      
      
      ~~~
      
      
      http://us.metamath.org/mpeuni/wi.html
      ( &AX ( @a @b )
        (
          ( & wff @a )
          ( & wff @b )
        )
        (
          & wff
            & & imp
              @a
              @b
        )
      )
      
      
      ~~~
      
      
      http://us.metamath.org/mpeuni/ax-mp.html
      
      ( &AX ( @a @b )
        (
          ( & wff @a )
          (
            & wff
              & & imp
                @a
                @b
          )
          ( @ a )
          (
            & & imp
              @a
              @b
          )
        )
        (
          @b
        )
      )
      
      
      ~~~
      
      
      http://us.metamath.org/mpeuni/ax-1.html
      
      ( &AX ( @a @b @c )
        (
          ( & wff @a )
          ( & wff @b )
          ( @a )
          ( @b )
        )
        (
          & & imp
            @a
            & & imp
              @b
              @a
        )
      )
      
      
      ~~~
      
      
      http://us.metamath.org/mpeuni/ax-3.html
      
      
      ( &AX ( @a @b)
        (
          ( & wff @a )
          ( & wff @b )
          ( @a )
          ( @b )
        )
        (
          & & imp
            & & imp
              not @a
              not @b
            & & imp
              @a
              @b
        )
      )
      Ответить
      • http://us.metamath.org/mpeuni/ax-2.html
        
        
        ( &AX ( @a @b @c )
          (
            ( & wff @a )
            ( & wff @b )
            ( & wff @c )
            ( @a )
            ( @b )
            ( @c )
          )
          (
            & & imp
              & & imp
                @a
                & & imp
                  @b
                  @c
              & & imp
                & & imp
                  @a
                  @b
                & & imp
                  @a
                  @c
          )
        )
        Ответить
      • Что означает &? Применение функции?
        Ответить
        • То же, что и 'P' в https://govnokod.ru/27420 - просто две некие хрени. Т.е. если есть "& хрень1 хрень2" то это как (cons хрень1 хрень2) в лиспе, и оно распознается как одна хрень, а не как три хрени "&" "хрень1" "хрень2". Никаких "функций" тут нет.
          Ответить
          • Вообще говоря, функции от трех аргументов f(a,b,c) можно записывать например так "& & & f a b c" т.е. (((f a) b) c), хотя можно и так "& f & & a b c" т.е. (f ((a b) c) ) если подобным образом определить эту хрень.
            Ответить
            • Может лучше как-то со скобочками изъебнуться чтобы язык более гомоиконный был?

              (& (& (& f a) b) c)

              Будет лучше видно структуру для паттерн-нятчинга.
              Ответить
            • Или писать прям (wff (imp @a @b)).

              Ну просто у тебя уже есть скобочки, а ты унарный оператор пердолишь.
              Ответить
              • Скобочки тут для записывания теорем и аксиом нужны. Можно конечно их и туда упихать, но нафига? Я думал что-то вроде байткода сделать для этих правил переписывания, и вот эта фигня типа & & imp @a & & imp @b @a и будет фактически байткодом, т.е. тупо последовательность термов "&" "&" "imp" "@a" "&" "&" "imp" "@b" "@a" где в "@a" "@b" что-то там матчится. Если вводить скобки, допустим если "(" "imp" "@a" "(" "imp" "@b" "@a" ")" ")" и тут нужно какой-то парсер скобок писать, т.е. находим открывающую скобку "(" потом пробегаем это выражение, первое это "imp" второе это "@a" а потом открывающая скобка в которой какая-то еще хрень, нужно подсчитывать количество хреней между парными скобками, в общем какая-то дополнительная питушня нужна для матчинга закрывающих-открывающих скобок и количества хуйни между ними. Так что лучше через "&". Все равно эту скобочную питушню можно в хрень с "&" переписать каким-нибудь препроцессором, так что один фиг
                Ответить
                • Ну в общем-то да, префикс и скобочки всегда можно перегнать друг в друга. Просто мне казалось что скобки лучше читаются. А теоремам и аксиомам они вроде и не мешают.
                  Ответить
                  • Со скобами еще такая хуйня, что если внутри скобок записан всего один терм, ну типа "(@a)" то через "&" это уже не переписать, потому что для "&" нужно как минимум две хрени, и можно или просто нахрен убирать такие скобки, или говорить что это ошибка. Ну и фигня типа "(a b c d e)" оказывается синонимичной фигне "((((a b)c)d)e)" что добавляет избыточности.

                    В общем это все синтаксический сахарок, который можно внешним препроцессором сделать, тащить это в базовый язык незачем.
                    Ответить
            • (&TH (@a @b)
                (
                  (wff (imp @a @b))
                  (imp @a @b)
                  (wtf @a)
                  @a
                )
                (
                  @b
                )
                (
                  ... proof ...
                )
              )
              Ответить
      • http://us.metamath.org/mpeuni/ax-3.html
        
        
        ( &AX ( @a @b)
          (
            ( & wff @a )
            ( & wff @b )
            ( @a )
            ( @b )
          )
          (
            & & imp
              & & imp
                & not @a
                & not @b
              & & imp
                @a
                @b
          )
        )

        Вот так надо, потому что "not" принимает один аргумент
        Ответить
      • > wff

        - показалось
        Ответить
      • По-моему у тебя тут база индукции потерялась. Все правила хотят (& wff x) на входе, а где я его возьму помимо этих правил?

        Может быть какие-то безусловные (& wff true) и (& wff false) стоит добавить чтобы можно было начать что-то строить?
        Ответить
        • > По-моему у тебя тут база индукции потерялась. Все правила хотят (& wff x) на входе, а где я его возьму помимо этих правил?

          А зачем тебе что-то брать? Теоремы ты строить можешь. Например транзитивность http://us.metamath.org/mpeuni/syl.html - если "из a следует b" и "из b следует c" то "из a следует c"

          ( &TH ( @a @b @c)
            (
              ( & wff
                  & &
                    imp @a @b
              )
              ( & wff
                  & &
                    imp @a @c
              )
              (& & imp @a @b)
              (& & imp @a @c)
            )
            (
              & & imp @a @c
            )
          
            (
              тут-какое-то доказательство с отсылками на аксиомы и теоремы
            )
          )


          Никакой (& wff true) и (& wff false) не нужен.

          Если @a @b @c это wff (well formed formula), мы тривиально доказываем что "& & imp @a @b" и "& & imp @a @c" это тоже wff и так можем эту теорему применить в какой-то другой теореме.
          Ответить
          • В этой теореме точно не пропущены (& & imp @a @b) и (& & imp @b @c) в прекондишенах?
            Ответить
            • Да, это тоже там надо добавить. Сейчас отредактирую
              Ответить
            • И вообще я там напутал с переменными, надо вот так

              ( &TH ( @a @b @c)
                (
                  ( & wff
                      & & imp
                        @a
                        @b
                  )
                  ( & wff
                      & & imp
                        @b
                        @c
                  )
                  (
                    & & imp
                      @a
                      @b
                  )
                  (
                    & & imp
                      @b
                      @c
                  )
                )
                (
                  & & imp
                    @a
                    @c
                )
              
                (
                  тут-какое-то доказательство с отсылками на аксиомы и теоремы
                )
              )


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

                Может более явный синтаксис сделать, что у аксиом и теорем есть только одно утверждение:
                (&TH (@a @b)
                  (
                    (imp
                      (and
                        (and (wff (imp @a @b)) (imp @a @b))
                        (and (wff (imp @b @c)) (imp @b @c)))
                      (imp @b @c))
                  )
                  (
                    .... proof ....
                  )
                )
                Ответить
                • "imp" не захардкожен. И "wff" тоже не захардкожен. Это просто некие термы, с которым есть какие-то аксиомы. Вот "&" захардкожен, это да. Надо чтоб "& хрень1 хрень2" принималось как одна штука, а не как три.
                  Ответить
                  • imp не захаркожен, а вот неявная импликация зашита в структуру аксиом и теорем (взаимодействие 2 и 3 аргумента теоремы). and не захардкожен, но неявное И зашито в структуру второго аргумента теоремы.

                    Т.е. получается что какие-то элементы логики уже прям в синтаксис просочились. А мы их потом заново сочиняем.
                    Ответить
                    • > and не захардкожен, но неявное И зашито в структуру второго аргумента теоремы.

                      А как определять это самое "И", если бы в теореме-аксиоме нельзя упомянуть две или более штуки?

                      Ну т.е.

                      ( &AX ( @a @b )
                        (
                          ( & wff @a ) // как мы без этого "И" сможем описать не-зашитый в язык "И" ?
                          ( & wff @b )
                          ( @a )
                          ( @b )
                        )
                        (
                          & & and
                            @a
                            @b
                        )
                      )
                      Ответить
                      • "И" можно по идее импликацией описать. Что-то в духе:

                        forall a b, a -> b -> and a b

                        Теперь вопрос как импликацию аксиоматизировать...
                        Ответить
                        • Эмм, у тебя все равно ничего не выйдет без встроенного в язык "И". Ты так не сможешь сказать "если верно это, и верно это, тогда вот это вот верно".
                          Ответить
                          • a -> b -> and a b

                            Если верно а, тогда (если верно b, тогда верно and a b).

                            Или я туплю?
                            Ответить
                            • Чтобы определить импликацию, тебе нужно сказать, что импликация & & imp @a @b это well-formed formula если @a это well-formed formula и @b это well-formed formula. У тебя еще нет импликации, но тебе нужен этот неявный and чтобы сформулировать требования к (по-сути аксиому) корректности импликации.

                              Вообще это проблема курицы и яйца.
                              Ответить
                              • > курицы и яйца

                                В петухе ее элегантно решили построением и того и другого через лямбды и типы, но здесь видимо так не прокатит ;(
                                Ответить
      • Сделай свой прувер с RPN синтаксисом для прикола.
        Ответить
        • : and-axiom
            forall dup wff is-true dup is-true
            forall dup wff is-true dup is-true
            and is-true
          ;axiom
          Ответить
          • Годный синтаксис, что-то попробовать понять сможет даже тот, кто всякие ко-коки и подобную питушню ни разу не видел. И в одну строку: читается как предложение.
            А j123123 какой-то ассемблер сделал или сишку с кучей &мперсандов и переводов строки. Читается как чат малолеток:
            - ты как няш :*
            - норм ))
            - ясн ))
            - а ты7
            - неоч (((
            - бл& (
            - вще х&&во
            - &здец ))
            Ответить
            • > Годный синтаксис

              Из-за RPN что-то сложнее этой теоремки будет нячитаемо, ну да пофиг. Плюс тут надо как-то задекларировать wff и and перед использованием:

              2 constructor and
              1 constructor wff
              Ответить
              • RPN - это обратная польская питушня?
                А то если гуглить, это либо Росприроднадзор, либо оперативный ответвительный зажим, либо registered practical nurse, либо revenue payroll notification.

                Хотя, с другой стороны, может и не надо такое гуглить, а то потом начну писать теоремы и формулы вида E=mc^2 записывать с амперсандами и скобками
                (formula
                  @E
                  (definition
                    (equals
                      (left (@E))
                      (right (mul (@m) (call (func @square) @c &2))
                    )
                  )
                )
                Ответить
                • Странно, у меня reverse polish notation первым пунктом. Видимо, ты гугл чему-то не тому обучаешь.
                  Ответить
                  • Третья после Росприроднадзора и его личного кабинета.
                    Ответить
            • > А j123123 какой-то ассемблер сделал

              Вообще говоря, в этом и идея. Ядро прувера и должно быть простым и похожим на ассемблер. А дальше поверх него уже можно наворачивать всякий сахарок и тактики без боязни обосраться.
              Ответить
        • Тогда надо еще определять количество пожираемых из стека хреней. И как-то сообщать, в какой момент матчить.
          Вот допустим

          5 5 + 5 5 + + // в обычной записи это будет (5+5)+(5+5)


          надо чтоб где-то в определении "+" было описано что оно захавывает из стека два "Nat" и "возвращает" один "Nat". И что "5" вообще нифига не захавывает, и просто является "Nat".


          И если есть теорема, что "@x @x +" где @x это "Nat" можно переписать как "@x 2 *", и чтоб такую теорему применить нужным образом, если указать что "@x" это "5 5 +" то тогда питушня заматчится так
          5 5 + 5 5 + +
          ^^^^^ ^^^^^ ^
          x     x    +
          // перепишется в
          
          5 5 + 2 * // (5+5)*2

          А если указать что "@x" это "5" то

          5 5 + 5 5 + +
          ^ ^ ^
          x x +
          // мы тут матчим
          
          
          5 5 + 5 5 + +
                ^ ^ ^
                x x +
          // или тут?

          Надо какой-то дополнительной питушней указывать, когда надо матчить? В общем, это немного усложняет
          Ответить
          • > указывать, когда надо матчить

            В префиксном формате у тебя есть точно такая же проблема (да и в инфиксном коке она тоже есть).

            Допустим, мы хотим применить теорему про a + b = b + a в формуле (1 + 2) + (1 + 2). Здесь три потенциальных матча. Как указать, какой именно я хочу зареврайтить?
            & & plus
              & & plus 1 2
              & & plus 1 2
            
            // хотим заматчить & & plus @a @b с внешним оператором и получить
            // @a = & & plus 1 2
            // @b = & & plus 1 2
            
            // или хотим заматчить & & plus @a @b с самым правым плюсом и получить
            // @a = 1
            // @b = 2
            Т.е. в любом случае надо какой-то способ для явного выбора нужного фрагмента.
            Ответить
            • Конструкцию
              & & plus
                & & plus 1 2
                & & plus 1 2
                ^  ^ ^^^^ ^ ^

              надо матчить не через
              если '& & @a @b' то
              '& & @b @a'

              а через
              если '& & plus @c & & plus @a @b' то
              '& & plus @c & & plus @b @a'


              Или даже чтоб
              если '@z1 & & plus @a @b @z2' то
              '@z1 & & plus @b @a @z2'
              где '@z1' и '@z2' - произвольная хуйня, возможно даже что вообше пусто


              И тогда в @z1 задаем
              & & plus
                & & plus 1 2

              а в @z2 - нихуя.
              Ответить
              • А, ну понятно, через явную подстановку конкретных значений параметров в теорему, а потом подстановку полученой теоремы в исходную формулу. В коке тоже так можно, да.
                Ответить
              • если '& & plus @c & & plus @a @b' то
                '& & plus @c & & plus @b @a'

                Кстати, а как ты это докажешь имея только если '& & plus @a @b' то '& & plus @b @a'?

                Воспользуешься дополнительной леммой если '@x = @y' то '& & plus @c @x' = '& & plus @c @y'? Или как-то проще, чтобы эквивалентность не вылезала?
                Ответить
                • > Кстати, а как ты это докажешь имея только если '& & plus @a @b' то '& & plus @b @a'?

                  Ну допустим если использовать прямую польскую запись и отказаться от этих вот "&"

                  Дано:
                  plus
                    @c
                    plus
                      @a
                      @b
                  // (c+(a+b))
                  
                  Получить надо:
                  plus
                    @c
                    plus
                      @b
                      @a
                  // (c+(b+a))
                  
                  
                  Пусть дана аксиома коммутативность
                  plus @a @b -> plus @b @a
                  // (a+b) -> (b+a)
                  
                  и аксиома ассоциативность
                  plus
                    @a
                    plus
                      @b
                      @c
                  ->
                  plus
                    plus
                      @a
                      @b
                    @c 
                  // (a+(b+c)) -> ((a+b)+c)
                  
                  И еще такая аксиома, хрен знает как ее назвать
                  plus
                    @a
                    plus
                      @b
                      @c
                  ->
                  plus
                    @b
                    plus
                      @a
                      @c
                  // (a+(b+c)) -> (b+(a+c))
                  
                  1) Сначала по ассоциативности
                  
                  меняем
                  plus
                    @c
                    plus
                      @a
                      @b
                  // (c+(a+b))
                  
                  на
                  
                  plus
                    plus
                      @c
                      @a
                    @b
                  // ((c+a)+b)
                  
                  2) По коммутативности переставляем первое и второе
                  
                  plus
                    @b
                    plus
                      @c
                      @a
                  // (b+(c+a))
                  
                  3) потом поменяем по вот той хрен-знает-как-назвать аксиоме
                  
                  plus
                    @c
                    plus
                      @b
                      @a
                  // (c+(b+a))
                  
                  теорема доказана
                  Ответить
                  • Полные рукава аксиом, блин...

                    Имхо, тут можно попробовать доказать лемму конгруэнтности (или как там её правильно зовут): если из @a следует @b, то из plus @x @a следует plus @x @b, а так же из plus @a @y следует @b @y. Имея такие леммы можно будет легко добираться до нужных фрагментов.

                    Но я пока туплю, как её записать в твоей системе.
                    Ответить
                    • (&TH plus-congruence-left (@a @b @y)
                        (imp @a @b)
                        (imp plus @a @y plus @b @y)
                        (... admitted ...)
                      )
                      Как-то так что ли, если получится описать эквивалентность захардкоженной импликации и imp.
                      Ответить
                      • ты хочешь чтоб если "imp @a @b" и "add @a @x" то можно вывести "add @b @x"? Может тут лучше ввести оператор равенства? И как тебе это поможет
                        add
                          @c
                          add
                            @a // эту поменять
                            @b // с этой?

                        У тебя ж тут ничего ничему не равно и даже не имплицируется.

                        Хотя наверное можно попереставлять, потом собрать выражение с импликацией и его применить по такой-то аксиоме. Это думать надо
                        Ответить
                        • Не, похоже там неоткуда взяться такой импликации, чтобы это можно было переставить
                          Ответить
                      • Лучше подумай, из чего можно было бы доказывать лемму переброса через скобочки (a+(b+c)) -> (b+(a+c))
                        Ответить
                        • Ну я в коке такое обычно доказывала через ассоциативность и коммутативность.

                          a+(b+c) = (a+b)+c = (b+a)+c = b+(a+c)

                          Но тут опять же нужна конгруэнтность плюсика (x=y -> a+x=a+y /\ x+a=y+a), чтобы можно было оперировать над кусками формулы, а не над всей целиком.

                          В коке она бай дизайн, насколько понимаю. А тебе её придётся доказать или принять.
                          Ответить
                    • (&AX imp-to-implication (@a @b)
                        (
                          (imp @a @b)
                          @a
                        )
                        (
                          @b
                        )
                      )
                      Ответить
                      • Это у тебя modus ponens получился.
                        http://us.metamath.org/mpeuni/ax-mp.html
                        Ответить
                    • (&AX implication-true-true (@a @b)
                        (
                          @a
                          @b
                        )
                        (
                          imp @a @b
                        )
                      )
                      Как-то так что ли...
                      Ответить
                      • Не, херня какая-то.
                        Ответить
                      • Какой sendmail.cf )))
                        Ответить
                      • А это http://us.metamath.org/mpeuni/ax-1.html лучше

                        типа
                        (&AX ax1 (@a @b)
                          (
                            ( @a )
                            ( @b )
                            ( wff @a )
                            ( wff @b )
                          )
                          (
                            imp @a imp @b @a
                          )
                        )
                        
                        И если у тебя есть
                        @a (1)
                        @b (2)
                        wff @a
                        wff @b
                        То значала конструируем (используя ax1 и подставляя туда (2) (1) )
                        imp @b imp @a @b 
                        Потом берем модус поненс. "@b" есть, "imp @b imp @a @b" есть. Получаем
                        imp @a @b
                        Ответить
              • Иными словами, а с чего ты взял, что можно приписать к условию и следствию теоремы какую-то хуйню и она при этом не сломается? Особенно если у этой теоремы будет несколько прекондишенов а не один.

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

                  Не, ну это надо просто хуйни не делать. Если есть какая-то хуйня, где можно "перегружать" значение plus, и при такой перегрузке plus уже не складывает, а возводит в степень, и эта хуйня для перегрузки заматчилась в @z1 @z2 (как в том последнем примере) то конечно хуйня будет.

                  Тут надо конкретику обсуждать, придумывать непосредственно сами аксиомы и правила вывода
                  Ответить
                  • Имхо, для начала надо определиться, над чем вообще мы тут работаем, не упираясь в синтаксис.

                    Пока это выглядит как деревья, состоящие из атомов (wff, and и т.п.) и конструкторов пары (&).

                    Над деревьями мы вводим отношение истинности. Какие-то деревья истинны, а какие-то -- нет.

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

                    Но работать над конкретными деревьями скучно, поэтому мы вводим собачки-переменные (ака forall) чтобы составлять более интересные аксиомы, которые гласят "такое дерево истинно для любых поддеревьев @a".

                    И затем мы вводим ещё более сложные аксиомы, в которых есть набор входных условий: "если все вот эти деревья истинны для поддерева @a, то вот такое дерево тоже истинно для этого @a".

                    Поправь меня, если я написала хуйню.

                    З.Ы. Т.е., насколько я понимаю, пока что мы можем применять теоремы только от корня, ко всему дереву целиком. Права на работу с поддеревьями у нас пока нету.
                    Ответить
                    • > Над деревьями мы вводим отношение истинности. Какие-то деревья истинны, а какие-то -- нет.

                      Тут изначально нет никакой "истинности". Тут речь о выводимости т.е. можем ли мы такую-то штуку сконструировать, пользуясь такими-то аксиомами и/или уже доказанными теоремами. Если можем, то теперь эта штука - еще одна теорема, которой можно пользоваться для доказывания чего-то там.
                      Ответить
                      • Ну ок, я не против "выводимости" или "constructibility" какого-нибудь. В остальном всё ок, если s/истинность/выводимость/ ?
                        Ответить
                        • > Пока это выглядит как деревья, состоящие из атомов (wff, and и т.п.) и конструкторов пары (&).

                          Что-то мне подсказывает, что этот "&" тоже можно обычным термом считать, никакого особого статуса ему можно не давать (хотя может это где-то что-то ломает, но пока это неочевидно). И тогда никаких деревьев тут по-сути нет, просто списки хреней, которые матчатся какой-то хреню и если заматчились то генерируем что-то там.
                          Ответить
                          • > И тогда никаких деревьев тут по-сути нет, просто списки хреней, которые матчатся какой-то хреню и если заматчились то генерируем что-то там.

                            Это же sed (=^ ◡ ^=)
                            Ответить
                          • > никакого особого статуса ему можно не давать

                            Да в общем-то его тогда и выкинуть можно, записывая "& & and" как "and". Вроде тоже ничего не сломается.
                            Ответить
                            • Ну т.е. если у нас есть следующие няксиомы:

                              wff @a -> wff not @a
                              wff @a -> wff @b -> wff and @a @b

                              То хуёвую формулу из них ну никак не слепить, насколько я понимаю. Можно даже попробовать это пруфнуть.

                              & разве что для каррирования мог бы пригодиться. Типа "& and @a" -- это унарная хуйня, принимающая bool. Другой пользы я пока не вижу.
                              Ответить
                            • "&" может иметь смысл, если функция может переменное число аргументов принимать, чтоб в одну функцию много фигни запихать. типа
                              & & & & add_many
                               @a
                               @b
                               @c
                               end_add_many

                              которая через какие-то теоремы переписывается по частям
                              & & add
                                @a
                                & & & add_many
                                 @b
                                 @c
                                 end_add_many
                              
                              ---
                              
                              & & add
                                @a
                                & & add
                                  @b
                                  & & add_many
                                    @c
                                    end_add_many
                              
                              ---
                              
                              
                              & & add
                                @a
                                & & add
                                  @b
                                  @c
                              Ответить
                              • Или так
                                & & & & add_many
                                  @a
                                  @b
                                  @c
                                  end_add_many
                                
                                & & & add_many
                                  & & add
                                    @a
                                    @b
                                  @c
                                  end_add_many
                                
                                
                                & & add_many
                                  & & add 
                                    & & add
                                      @a
                                      @b
                                    @c
                                  end_add_many
                                
                                
                                & & add 
                                  & & add
                                    @a
                                    @b
                                  @c
                                Ответить
                              • > если функция может переменное число аргументов принимать

                                В пруверах про такое обычно не парятся... ну да ладно.

                                У тебя там всё равно end есть. Так что можно как-то так зареврайтить:

                                add_many end_add_many -> 0
                                add_many @a -> add @a add_many (в этом правиле @a должно быть wff)

                                add_many @a @b @c end_add_many ->
                                add @a add_many @b @c end_add_many ->
                                add @a add @b add_many @c end_add_many ->
                                add @a add @b add @c add_many end_add_many ->
                                add @a add @b add @c 0
                                Ответить
                              • > если функция может переменное число аргументов принимать

                                Не преумняжай сущнясти. Все функции принимают на вход только один аргумент, а с зависимыми типами можно намутить, что при каррированяи тип возвращаемой лямды будет отличаться в зависимости от предыдущих аргументов.
                                Ответить
                                • P.S. Ня! http://poleiro.info/posts/2013-04-19-type-safe-printf-in-coq.html (Пример такого подхода, где типы аргументов выводятся из форматной строки)
                                  Ответить
                                • > Ня преумняжай сущнясти.

                                  Угу, можно вообще список сделать и fold для него запилить.
                                  Ответить
                                  • Список элементов разных типов будет кучеряво выглядеть.
                                    Ответить
                                    • > Список элементов разных типов будет кучеряво выглядеть.

                                      Да почему? Обычный product type. Хотя такое обычно туплом называют, конечно, а не списком.
                                      Ответить
                                      • Список это всё-таки разновидность cons/nil питушни. Таплы в Coq чуть по другому устроены, это тоже конструктор с двумя аргументами, но у них нет nil-конструктора.
                                        Ответить
                    • И вообще, чтоб рассуждать об истинности и неистинности, надо определить, работает ли закон отрицания третьего.
                      Ответить
                      • > работает ли закон отрицания третьего

                        Я думаю пока можно без него попробовать. Добавить всегда можно будет.

                        "Ложность" ака "невыводимость" можно будет доказать перебрав все правила и показав, что они не помогают построить такое дерево, к примеру.

                        К слову, пока это очень похоже на индуктивные типы в coq. Просто тип пока один: "constructible" или как ты там его назовёшь.
                        Ответить
            • Интересно, можно ли построить на игре с заменами какую-нибудь вычислительную систему?

              (1 + 2) + (1 + 2) обеспечивает кучу вариантов
              1. левая замена
              2. средняя замена
              3. правая замена
              4. 1/2/3 и левая/средняя/правая замена где угодно
              5. 1/2/3 и левая/средняя/правая замена там, где ещё не заменяли
              6. одновременная замена 2 выражений
              7. одновременная замена 3 выражений

              Дальше строим кучу разных операторов
              1. замена с памятью/без памяти (с памятью убеждается, что создаются уникальные идентификаторы, а не совпадающие - x->x1 vs x->x)
              2. вилка: замена без памяти, удлиняющая выражение (например, x -> x+x)
              3. сход: замена, сокращающая выражение (например, x+x -> x)
              4. итерация до достижения неподвижной точки

              Дальше определяем числа, скажем, как
              0. левая замена
              1. правая
              2. левая, затем правая
              3. правая, затем правая
              (или ещё как-то красиво)

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

                Да, ты можешь построить например брейнфак.

                сначала идет код программы типа последовательности из "< > + - . [ ]" и там еще будет маркер "^" который означает текущий instruction pointer.
                Потом разделитель "#" и дальше будет счетчик для квадратных скобок "[ ]" чтобы находить пару.
                Потом опять разделитель "#" и будет как бесконечное поле из чисел от 0 до 255 с маркером, которое нулями слева и справа дописывается
                Потом опять разделитель "#" и будет стандартный вывод
                например если программа "+ + . > > [ > > ]" то начальное состояние будет
                ^+  + . > >  [ > >  ] # # ^ 0 #
                // Потом применяя некую теорему с матчингом и получаем инкремент первой ячейки и сдвиг instucton pointer-а
                + ^+ . > >  [ > >  ] # # ^ 1 #
                // Потом
                +  + ^.  >  >  [  >  >  ] # # ^2 #
                +  +  . ^>  >  [  >  >  ] # # ^2 # 2 // вывели в stdout 2
                +  +  .  > ^>  [  >  >  ] # # 2 ^0 # 2 // подвигались по бесконечной ленте
                +  +  .  >  > ^[  >  >  ] # # 2 0 ^0 # 2 // заполненной нулями
                +  +  .  >  >  [ ^>  >  ] #  [ # 2 0 ^0 # 2 // значение ячейки памяти справа от ^ равно 0 поэтому проматываем до появления одной  ]
                +  +  .  >  >  [  > ^>  ] #  [ # 2 0 ^0 # 2
                +  +  .  >  >  [  >  > ^] #  [ # 2 0 ^0 # 2
                // конец.
                Ответить
              • Да: https://en.wikipedia.org/wiki/Semi-Thue_system .
                Ответить
          • Можно как в unlambda: любой терм по умолчанию накидывается на стек, а оператор ` берёт два кобенатора с вершины стека, и применяет друг к другу.
            Ответить
      • А как ня этом будет выглядеть нячёткая логика?
        Ответить
    • говнокод окончательно превратился в форум дискретных математиков из рашки, украшки и шведяшки

      грустно
      Ответить
      • Именно поэтому я за «Говнокод».
        Ответить
      • Присоеди-ня-йся.
        Ответить
      • Не знаешь Ltac-а — по мордочке ня-ка!
        Ответить
      • я ня дискретный математик, потому что дискретное пространство это самое скучное пространство
        Ответить
        • Плюсую. Скучная питушня, где задачи и их решения усложняются.
          Та же задача о рюкзаке из простого алгоритма превращается в пердолинг с пожиранием памяти.
          Ответить
    • давайте лучше про что нить приземленное

      Вот например: когда вы делаете malloc, глибц растит вам секцию кучи (делает brk). Но если вы делаете ОЧЕ большой маллок (выше M_MMAP_THRESHOLD, mallopt(3)) то маллок делает вам анянянямный ммап.

      Такие отдельные секции удобнее выпёздывать на мороз по мере их освобождения (а усекновение секции кучи можно делать только с жопы), зато анянямные секции обязаны были выравнены по страничкам

      //
        for (int i = 0; i < 100; i++) {
                      foo     = malloc(1024 * 1024 * i);
                      sleep(1);
              }


      тут мы сначала видим sbrk, а потом mmap (в strace)

      в /proc/<pid>/maps мы видим сначала растущий [heap], а потом анонимный регион
      Ответить
      • А если место между brk и первым регионом закончится?
        Ответить
        • наверное нельзя будет больше увеличить "heap"

          но оно там делает дырку
          #
          01e7e000-01e9f000 rw-p 00000000 00:00 0                                  [heap]
          7f4ef327b000-7f4ef5582000 rw-p 00000000 00:00 0

          хип кончается на 01e9f000 (32108544)
          анонимн регион начина на 7f4ef327b000(139977063641088)

          довольно дохуя, не?
          (хорошо на x64 жить)
          Ответить
          • > довольно дохуя

            Если все большие аллокации уходят няверх -- наверное норм.
            Ответить
            • наверное наверх, иначе как его усекать?

              мне вот интересно, нахуя вообще это всё? брк, хип, указатели на code и data, которые там реально в mm_struct..

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

              Зачем ядру вообще что-то знать про хип-хуип?

              В пинде же вроде VirtualAlloc просто создает какую-то запись VAD, и течет

              А уже поверх можно создавать хипы (причем дохуя хипов)
              Ответить
              • Х.з., исторически сложилось? Так то линейный регион для brk можно и полностью в юзермоде эмулировать через обычные маппинги.
                Ответить
                • может исторически, угу

                  Во всяком случае в классическом System V хак с mmapом не использовали, про него Морис не пишет.

                  Но БЗД уже тоже да, причем опёнок по другой причине

                  Old implementations were all sbrk(2) based. In OpenBSD 3.8, Thierry Deval rewrote malloc to use the mmap(2) system call, making the page addresses returned by malloc random

                  >можно и полностью в юзермоде эмулировать
                  Ну вот наскока я понимаю, виндовый ``CreateHeap`` так примерно и делает.
                  Правда vmmap каким-то чудом знает, какой регион (кстати, как он правильно называется у винды? address range?) это хип

                  https://tr1.cbsistatic.com/hub/i/2010/01/06/7fab9293-c3b4-11e2-bc00-02911874f8c8/Jan-2010-WSTips20f5-Post2FigA.jpg

                  вон скока хипов, причем один еще и шарбл
                  Ответить
                  • > каким-то чудом знает

                    Да поди знает где табличку хипов подсмотреть. Виндбг так то тоже её тоже читать умеет.
                    Ответить
                    • кстати как разные хипы эмулить на линуксе? вручную делать анонимный mmap?
                      Ответить
                      • Ну да, а что мешает? Особенно на 64-битке где есть где развернуться. Тем более хип не обязательно делать совсем уж непрерывным, если ты в нём гигабайтные куски один хрен хранить не будешь.
                        Ответить
                        • ничего не мешает, просто интересно отображать понятия одной ОС на понятия другой

                          Было бы круто добавить в сишку такую API: malloc с как-бы ареной. Но не вручную её создавать, а делегатить операционке
                          (В glibc есть арена, но она не про то)
                          Ответить
                          • Ну возьми другой аллокатор с аренами... или напиши его. Зачем добавлять его в сишку?
                            Ответить
                            • Потому что в большинстве ОС есть системная возможность сделать такие "арены", и было бы удобно иметь её в сишке.
                              В пинде есть еще анклав какой-то..

                              Кстати, проверил: malloc на пинде срёт в heap (увеличивая его до неебических размеров), а явный VirtualAlloc создает "private" (ну или какую закажешь) address range.

                              Ренджи на пинде можно еще смотреть через kernel debugger: У !process (который показывает EPROCESS) есть поле "VDA root", которое адрес корня бинарного дерева, где хранятся VDA (у прыщей вроде есть еще linked list к дереву, а у NT только дерево), и потом по !vda можно его смотреть.

                              К сожалению, у меня нет пинды с поддержкой kernel debug, шоб проверить

                              зы: у обычного процесса еще можно посмотреть свои мапы через ``VirtualQuery``
                              Ответить
                              • Что есть "системная возможность"?
                                Ответить
                                • а ты тред прочитал?:)

                                  на линуксе есть анонимный ``mmap``, на windows есть ``CreateHeap``: они создают отдельные регионы памяти, которые потом можно целиком анмапнуть или удалить
                                  Ответить
                                  • А на контроллерах ничего такого нет. Описываешь регион заранее и течёшь.

                                    Именно поэтому я за контроллеры.
                                    Ответить
                                  • > на линуксе есть анонимный ``mmap``, на windows есть ``CreateHeap``

                                    Так mmap в линуксе это сискол, а CreateHeap это какая-то винапи-хуитень. Тебе наверное надо NtAllocateVirtualMemory
                                    Или NtAllocateUserPhysicalPages

                                    Зачем они столько хуйни в винде понаделали?
                                    Ответить
                                    • https://j00ru.vexillium.org/syscalls/nt/64/


                                      NtAllocateUserPhysicalPages
                                      NtAllocateUserPhysicalPagesEx
                                      NtAllocateVirtualMemory
                                      NtAllocateVirtualMemoryEx
                                      NtFlushVirtualMemory
                                      NtFreeVirtualMemory
                                      NtFreeUserPhysicalPages
                                      NtLockVirtualMemory
                                      NtProtectVirtualMemory
                                      NtQueryVirtualMemory
                                      NtReadVirtualMemory

                                      Сколько же хуйни
                                      Ответить
                                      • Вероятно стоит разделять "PhyscialPages", которые работают непостредственно с PFN (номерами физических страниц и PTE) и "VirtualMemory", которая работает с ренджами поверх этого
                                        Ответить
                                    • Верно, ``CreateHeap`` вызывает ``VirtualAlloc``, который уже вызывает сискол для создания региона памяти.

                                      Зачем -- это вопрос к Дэвиду Катлеру, но работает именно так.

                                      В линуксе новый регион создается через mmap (ну или shmget), а в винде через VirtualAlloc.

                                      Но CreateHeap более высокоуровневый, позволяет не думать про конкретные VDA, их мапинг на страницы итд
                                      Ответить
                              • Продолжаем ковырять виртуальную память
                                На сей раз на прыще
                                ``mmap`` c ``MAP_ANON | MAP_PRIVATE`` возвращает адрес, который хорошо виден в ``/proc/[pid]/map``, и регион там анонимный

                                ``malloc``, как было сказано выше, либо увеличивает регион ``[heap]``, либо создает новый, если область памяти слишком велика.

                                Сравним с FreeBSD:

                                Анонимный ``mmap`` требует ``-1`` в качестве fd, иначе возвращает invalid arguments (прыщи работают и так).

                                Удобная утилита ``procstat`` (жаль, что на прыще такого нет) показывает ренджи памяти, правда пометки ``heap`` там нет: регион, как регион

                                Если сравнить два региона
                                //
                                  void* a = malloc(1024);
                                        printf("heap: %p, %d", a, getpid());
                                        void *m = mmap(NULL, 1024*1024,PROT_NONE, MAP_ANON | MAP_PRIVATE,  -1, 0);
                                
                                        printf("mmap: %p\n", m);

                                то в аутпуте они будут рядышком, но mmap намного дальше хипа (сначала хип, потом mmap)
                                //
                                :~ $ procstat vm 1137
                                  PID              START                END PRT  RES PRES REF SHD FLAG  TP PATH
                                 1137        0x800800000        0x801000000 rw-   16   16   1   0 ----- df
                                 1137     0x7fffdffff000     0x7ffffffdf000 ---    0    0   0   0 ----- --


                                ---
                                Фряша обссыкивает sbrk:

                                The brk() and sbrk() functions are legacy interfaces from before the ad-
                                vent of modern virtual memory management. They are deprecated and not
                                present on the arm64 or riscv architectures. The mmap(2) interface
                                should be used to allocate pages instead.

                                Traditionally, allocators have used sbrk(2) to obtain memory, which is
                                suboptimal for several reasons, including race conditions, increased
                                fragmentation, and artificial limitations on maximum usable memory. If
                                sbrk(2) is supported by the operating system, this allocator uses both
                                mmap(2) and sbrk(2), in that order of preference; otherwise only
                                mmap(2) is used.
                                Ответить
    • Американская корпорация Microsoft предупредила о серьезной уязвимости в операционных системах Windows 7 и 10
      Компания просит своих пользователей срочно обновить их.
      Фирма по кибербезопасности Sangfor случайно опубликовала инструкцию, где говорится, как с помощью диспетчера печати Windows удаленно получить доступ к другому компьютеру. Jбновления, которые устраняют эту уязвимость, Microsoft уже выпустила.
      Ответить
      • > случайно

        Блин, вот реально, все сервисы от мс надо блочить нахер.

        З.Ы. Причем вроде диспетчер печати в десятке уже засендбоксен был... Или не весь?
        Ответить
        • Не знаю.. Нет десятки под рукой позырить

          На семерке он работает от "System"
          S C:\Windows\system32> Get-Process -Name spoolsv -IncludeUserName
          
          Handles      WS(K)   CPU(s)     Id UserName               ProcessName                                                           
          -------      -----   ------     -- --------               -----------                                                           
              413      11780     0,45   1472 NT AUTHORITY\SYSTEM    spoolsv

          Ну и вероятно слушает RPC порт для named pipes, чо
          Ответить
          • у прыщей правда cups тоже работает от рута, причем похоже что и эффектив
            Ответить
    • Какой багор )))
      http://joeyh.name/blog/entry/a_bitter_pill_for_Microsoft_Copilot/
      Ответить
      • Ударим патчем Бармина по искусственному идиоту!
        Ответить
        • Хорошая идея, надо запилить parse transform, который `os:cmd("rm -rf ~")` заменяет на nop и пихать его в начало каждой функции. Главное не забыть об этом.
          Ответить
      • А реально питухи пиздят код через копилот и не думают вообще?
        Ответить

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