schwatchingizя решал проблему поле рациональных - кольцо целых -
кто из них подтип кого.
тут дошло что в натуральных - целых таже проблема.

можно сначала с этой парой разобраться.
Ну кольцо оно. Целые со сложением и умножением -
ассоциативное коммутативное кольцо.
может я что-то не так понял, но разве может быть определено кольцо, элементами которого будут только натуральные числа? ведь для них внутри N нет обратного по сложению.
в нормальном смысле нельзя. просто еще до кольца не добрались

softwarertchingizОсталось только с обратными к натуральным разобраться
Тоже не проблема. x+x=1 => x=1-x
тоже нифига не понял.
Сначала добавляем обратный

потом разбираемся с x + x = 1.
По рассмотренному выше x может быть только обратным.
Тогда существует натуральное y такое что -(y) = x// minus(y) = x
заменяем

plus (minus(y), minus(y)) = 1 // (-(y)) + (-(y)) = 1
по аксиоме plus_minus2
minus(plus(y, y))) = 1 // -(y+y) = 1

plus (y, y) должен получатся натуральным, то есть последовательностью
единиц
тоесть plus (y, y) = plus(1, plus(1, ..., plus(1,1)...)) =
plus(1, z) = 1 ---где z натуральное.

тогда succ(z) = 1
но это противоречит аксиоме first_is_zero

Шото в таком духе.
фух,

нет, лучше от той аксиомы отказаться.

plus(1,z) = 1 = plus(1, zero)
тогда
z = zero
тогда zero можно представить в виде последовательности единиц.
а это не так. противоречие.

во первых, взятие обратного унарная операция


minus : N >< N -> N
еще не вводили.
во вторых,
для того чтобы выполнялось следует
x+x = 1 => x = 1-x
надо добавить операция взятие обратного -x,
аксиому возможности замены порядка при выполнения суммы и взятия обратного
и аксиому c нулем.
что я и добавил в схему z

x + x + (-x) = 1 + (-x) => -- аксиома о скобках
x + (x +(-x) ) = 1 + (-x) => -- plus_minus2
x + 0 = 1 + (-x) => -- аксиома о сложении с нулем
x = 1 + (-x)

в третьих, заменим x на натуральный y и шо?

x = 1 + (-(-(y))) => по аксиоме о двух взятиях обратного minus_minus
x = 1 + y
а ну да. предположили что x не натуральное,
получается не натуральное равно сумме натуральных.
Да. так понятнее, но используется две новых аксиомы.

не надо с этим succ мозг напрягать

По аналогии с парой (Real, Int) по поводу обратного для умножения,
можно проследить пару (Int , UInt) по поводу обратного для сложения.

похоже вся мистика ооп в позднем связывании.
Если пронаследовать UInt от Int, и использовать
позднее связывание операции отнимания при присваивании b = a
То попадаем в нарушение того принципа, который пыталась
сформулировать Лисков. Наследовать нельзя.
Без позднего связывания отнимания - можно.
Если наследовать Int от UInt то будет нарушена аксиома
first_is_zero. Поэтому наследовать тоже нельзя.
Int не подтип UInt-a. Нет subtyping- а
короче, все педерасты, а я дъартаньян в белом плаще

а всю ооп мифологию можно записать в функциональном стиле.
чуть ли не левой задней ногой.

для записи спецификаций использовался язык спецификаций RSL
http://agp1.hx0.ru/arts/report249.pdf

и тока я могу написать оопшную на лямбда исчислении,
с сохранением прямых аналогов объектов

на любом функциональном.
в связи с тем, что класс это абстрактный автомат
то есть, пара (множество значений, множество функций)
и наследование на абстрактных автоматах я уже сделал

iv_an_rutchingiz,

На лямбда это так, разминка. А слабо на нормальных алгорифмах?
ааа. сории.
на частично рекурсивных функциях