Математик объясняет, как доказывать уравнения с помощью диаграмм
How to prove equations using diagrams, part 1
Evan Patterson из Topos Institute показывает, как доказывать уравнения, манипулируя диаграммами, а не перебирая термы. Ключевой инструмент — начальные функторы: они сохраняют пределы, а значит, и множества решений уравнений, заданных диаграммой. На конкретных примерах — склейка коммутативных квадратов и задание моноида — автор выстраивает механический стиль доказательств, который позже ляжет в основу категориальной семантики e-graphs и системы egglog.
В обычной математической практике никто не утруждает себя тем, чтобы сформулировать эти правила. Мы же намерены действовать более систематично.
- henearkr
Очень интересно!!
Придирка: для J-образной диаграммы D, J — это «индексная категория» или «схема» D, а не «форма», как написано в статье.
- boldslogan
чувак, я недавно наткнулся на концепцию функтора или несимволической логики и в таком духе. не думаешь, что у тебя есть какие-нибудь предложения, на что посмотреть?