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

    −1

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    (* basic power axiom
    safe_comp_power x y =
        case
            (x = 0) and (y <> 0) -> 1
            (x = 1) -> x
            ((x <> 0) and (y >= 0)) or ((x = 0) and (y > 0)) -> x * (safe_comp_power x (y - 1))
    *)
    
    logic safe_comp_pow : int, int -> int
    
    axiom safe_comp_pow_int_A_1 : forall x : int. (x <> 0) -> safe_comp_pow(x, 0) = 1
    
    axiom safe_comp_pow_int_A_2 : forall x : int. safe_comp_pow(x, 1) = x
    
    axiom safe_comp_pow_int_A_3 : forall x,y : int. ((x <> 0) and (y >= 0)) or ((x = 0) and (y > 0)) -> safe_comp_pow(x, y) = x*(safe_comp_pow(x,y-1))
    
    
    goal g_1 :
      forall a,n : int.
      a <> 0 -> n >= 0 ->
      safe_comp_pow(a,n+1) = safe_comp_pow(a,n)*a

    Язык для SMT солвера alt-ergo https://alt-ergo.ocamlpro.com/try.php . Аксиомы для возведения в степень. Возводить в отрицательную степень нельзя. Ноль в степени ноль - нельзя. Логика первого порядка. Должна быть справедлива для целых. Правда в одной аксиоме я допустил баг. Я его уже нашел. Можете тоже попробовать найти его

    Запостил: j123123, 22 Марта 2016

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

    • Хотя не, немного не так. В отрицательные степени можно возводить только единицу. Единицу вообще во что ни возведи - будет единица (бесконечностей не существует кокок)
      Ответить
    • > Логика первого порядка.
      > int, int -> int
      Ясно.
      Ответить
    • Заведи себе гитхаб, твитор и бложек. Зачем хвастаться кодом на непрофильных ресурсах?
      Ответить
      • почему непрофильный?
        Годкод.ру это же лучший ресурс, круче чем РСДН
        Ответить
      • Очень даже профильный. Тут говно в аксиоме, если вы еще не заметили
        Ответить
      • Надо сделать GovnHub и чтоб там цель была не исправлять код и улучшить читаемость, а вносить в него новые баги, делать нечитаемым и разводить побольше копипаста
        Ответить
      • Творожек
        Ответить
    • > try.php
      Ответить
      • Сам солвер написан на ocaml и оттранслинован в джаваскрипт
        Ответить
    • Вот это условие в третьей аксиоме смущает:
      > (x <> 0) and (y >= 0)
      Там точно включительно должно быть? С первой аксиомой пересечение получается. Решатель по порядку аксиомы пробует?
      Ответить
      • Да, проблема в этой аксиоме. Надо или так
        axiom safe_comp_pow_int_A_3 : forall x,y : int. ((x <> 0) and (y > 0)) or ((x = 0) and (y > 0)) -> safe_comp_pow(x, y) = x*(safe_comp_pow(x,y-1))

        или так:
        axiom safe_comp_pow_int_A_3 : forall x,y : int. ((x <> 0) and (y >= 0)) or ((x = 0) and (y > 0)) -> safe_comp_pow(x, y+1) = x*(safe_comp_pow(x,y))
        Ответить
        • > ((x <> 0) and (y > 0)) or ((x = 0) and (y > 0))
          (y > 0) and (x >= 0)
          Ответить
          • > ((x <> 0) and (y > 0)) or ((x = 0) and (y > 0))

            y>0
            Ответить
          • Да, оказывается так нельзя:
            axiom safe_comp_pow_int_A_3 : forall x,y : int. ((x <> 0) and (y > 0)) or ((x = 0) and (y > 0)) -> safe_comp_pow(x, y) = x*(safe_comp_pow(x,y-1))

            Потому что если подставить сюда x = 0 и y = 1 то оно проходит по условию (x = 0) and (y > 0) и исходя из этой аксиомы должно быть верно что safe_comp_pow(0, 1) = x*(safe_comp_pow(0,1-1))
            Получается 0^0 - нельзя.
            Ответить
          • Вот вроде нормальная аксиома
            axiom safe_comp_pow_int_A_3 : forall x,y : int. ((x <> 0) and (y >= 1)) or ((x = 0) and (y > 1))
             -> safe_comp_pow(x, y) = x*(safe_comp_pow(x,y-1))

            доказательство того, что x*x = safe_comp_pow(x, 2):
            Proof:
               (a * a) <> safe_comp_pow(a,2)
               a = 0
               a <> 0
               safe_comp_pow(a,2) = (a * safe_comp_pow(a,(2 - 1)))
               safe_comp_pow(a,1) = a
              ( a = 0 \/  1 > 2)
              ( a <> 0 \/  1 > (2 - 1))
              (( a = 0 \/  1 > 2) \/
               safe_comp_pow(a,2) = (a * safe_comp_pow(a,(2 - 1))))
              (( a <> 0 \/  1 > (2 - 1)) \/
               safe_comp_pow(a,2) = (a * safe_comp_pow(a,(2 - 1))))
            Ответить
      • > Решатель по порядку аксиомы пробует?
        Там если собрать через opam этот alt-ergo то можно врубить логгирование, какие аксиомы и как он пытается
        применять. Порядок объявления аксиом не важен
        Ответить

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