October 26th, 2010

Book

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

Вот обещанная теория арифметики с насыщением при переполнении для 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).