Куча говна / Говнокод #19677 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  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 j123123, (Updated )

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

  • ava j123123 # Ссылка на оригинал 0

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

  • ava kipar # Ссылка на оригинал 0

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

  • ava kurwa # Ссылка на оригинал 0

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

    • ava guest # Ссылка на оригинал 0 ⇈

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

    • ava j123123 # Ссылка на оригинал 0 ⇈

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

    • ava j123123 # Ссылка на оригинал 0 ⇈

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

  • ava roman-kashitsyn # Ссылка на оригинал 0

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

    • ava j123123 # Ссылка на оригинал 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 j123123 # Ссылка на оригинал 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 # Ссылка на оригинал 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 # Ссылка на оригинал 0 ⇈

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

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

Где здесь C++, guest?!

    А не использовать ли нам bbcode?

    ↑
    8
    ↓