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

    • ava j123123 22.03.2016 16:39 # 0

      Хотя не, немного не так. В отрицательные степени можно возводить только единицу. Единицу вообще во что ни возведи - будет единица (бесконечностей не существует кокок)
      Ответить

    • ava kipar 22.03.2016 22:16 # 0

      > Логика первого порядка.
      > int, int -> int
      Ясно.
      Ответить

    • ava kurwa 22.03.2016 22:35 # 0

      Заведи себе гитхаб, твитор и бложек. Зачем хвастаться кодом на непрофильных ресурсах?
      Ответить

      • ava guest 22.03.2016 22:54 # +1

        почему непрофильный?
        Годкод.ру это же лучший ресурс, круче чем РСДН
        Ответить

      • ava j123123 23.03.2016 00:47 # 0

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

      • ava j123123 23.03.2016 00:59 # 0

        Надо сделать GovnHub и чтоб там цель была не исправлять код и улучшить читаемость, а вносить в него новые баги, делать нечитаемым и разводить побольше копипаста
        Ответить

      • ava 3_14dar 23.03.2016 19:43 # −1

        Творожек
        Ответить

    • ava roman-kashitsyn 23.03.2016 09:33 # +1

      > try.php
      Ответить

      • ava j123123 23.03.2016 11:16 # 0

        Сам солвер написан на ocaml и оттранслинован в джаваскрипт
        Ответить

    • ava roman-kashitsyn 23.03.2016 09:47 # 0

      Вот это условие в третьей аксиоме смущает:
      > (x <> 0) and (y >= 0)
      Там точно включительно должно быть? С первой аксиомой пересечение получается. Решатель по порядку аксиомы пробует?
      Ответить

      • ava j123123 23.03.2016 11:15 # 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))
        Ответить

        • ava roman-kashitsyn 23.03.2016 13:45 # 0

          > ((x <> 0) and (y > 0)) or ((x = 0) and (y > 0))
          (y > 0) and (x >= 0)
          Ответить

          • ava kegdan 23.03.2016 13:50 # 0

            > ((x <> 0) and (y > 0)) or ((x = 0) and (y > 0))

            y>0
            Ответить

          • ava j123123 23.03.2016 15:57 # 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 - нельзя.
            Ответить

          • ava j123123 23.03.2016 16:47 # 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))))
            Ответить

      • ava j123123 23.03.2016 11:29 # 0

        > Решатель по порядку аксиомы пробует?
        Там если собрать через opam этот alt-ergo то можно врубить логгирование, какие аксиомы и как он пытается
        применять. Порядок объявления аксиом не важен
        Ответить

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