Интересно, а каких ещё клёвых штук можно на грудах наформализовывать? Я никогда всерьёз не интересовался грудами, привык думать о них как “те же торсоры, только в профиль”, а тут вот пример, когда использование груд очень украшает аксиоматику.
1) Вы не пробовали записать удобную аксиоматику для иных геометрий, основываясь на грудах? Наверное, для афинной напрашивается, а вот как со сферической, эвклидовой, гиперболической, проективной и конформной - априори непонятно.
2) А вы что-нибудь знаете про Planar ternary rings? Они могут быть описаны как equational theories, или они ближе к полям и соответственно слишком “жесткие”, чтобы быть алгебраическими теориями?
Не пробовал, но вот человек пробовал для аффинной и у него не получилось https://dxdy.ru/topic122315.html Там ведь не только сдвиги, там гомотетии нужны. В эллиптическом пространстве любое движение (сохраняющее ориентацию) есть композиция левого и правого сдвигов. Я это всё (написание программы) затеял с тройной целью: 1) Поучиться программировать; 2) Разобраться в геометрии (что с детства хотел сделать, но всё никак); 3) В перспективе написать пруфчекер, чтобы понять, как пишутся пруфчекеры. Соответственно, выбрал самую простую геометрию. Аксиоматика из книги Бахмана, если её расшифровать (а это нелегко было, посмотрите стр. 165-170, из которых я выжал доказательства), сбывает вековую мечту - свести геометрию к алгебре и доказательства к тупым вычислениям! В результате научился рисовать OpenGL и сейчас учусь сглаживать края, а до пруфчекера дойду ещё не скоро.
https://dxdy.ru/topic135617.html
Reply
Интересно, а каких ещё клёвых штук можно на грудах наформализовывать? Я никогда всерьёз не интересовался грудами, привык думать о них как “те же торсоры, только в профиль”, а тут вот пример, когда использование груд очень украшает аксиоматику.
Reply
2) А вы что-нибудь знаете про Planar ternary rings? Они могут быть описаны как equational theories, или они ближе к полям и соответственно слишком “жесткие”, чтобы быть алгебраическими теориями?
Reply
https://dxdy.ru/topic122315.html
Там ведь не только сдвиги, там гомотетии нужны. В эллиптическом пространстве любое движение (сохраняющее ориентацию) есть композиция левого и правого сдвигов. Я это всё (написание программы) затеял с тройной целью:
1) Поучиться программировать;
2) Разобраться в геометрии (что с детства хотел сделать, но всё никак);
3) В перспективе написать пруфчекер, чтобы понять, как пишутся пруфчекеры.
Соответственно, выбрал самую простую геометрию. Аксиоматика из книги Бахмана, если её расшифровать (а это нелегко было, посмотрите стр. 165-170, из которых я выжал доказательства), сбывает вековую мечту - свести геометрию к алгебре и доказательства к тупым вычислениям! В результате научился рисовать OpenGL и сейчас учусь сглаживать края, а до пруфчекера дойду ещё не скоро.
Reply
Reply
Leave a comment