Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Category:

Арифметика жопы

Вот обещанная теория арифметики с насыщением при переполнении для Prover9. Mace4 говорит, что для каждого размера модели от 3 (0, 1, Bot) до 15 с точностью до изоморфизма существует ровно одна модель (как и задумывалось). При этом ручной просмотр моделей показывает, что они обладает необходимым свойством: таблички операций и отношения a + b, a * b и a > b совпадают с точностью до перестановки с оными для чисел, за исключением некоторых больших значений, начиная с которых стоит _|_ (происходит переполнение).

Также интересно, что все аксиомы кольца по-прежнему выполняются, несмотря на наличие _|_. Вопрос залу: имеет ли это кольцо какое-то название? C моими минимальными познаниями в абстрактной алгебре я нашел только, что это http://en.wikipedia.org/wiki/Integral_domain

(x + y) + z = x + (y + z).
(exists x x + 1 = y) <-> y != 0.
-(x > x).
x * 0 = 0.
x * (y + 1) = (x * y) + x.  
x > y & y > z -> x > z.

x + 1 != x <-> x != Bot.
x + 1 > x <-> x != Bot.

x + 0 = x.
x + y = y + x.
x * y = y * x.
(x * y) * z = x * (y * z).
Tags: fp, programming
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 16 comments