[Перевод] Система типов в математике


Автор: PatientZero
Источник: https://habrahabr.ru/post/347294/
Время от времени мне встречаются вопросы по математике, которые в каком-то смысле можно назвать «грамматически неверными».

Пример. «Интервал $[0, 1]$ является замкнутым или открытым?»

Пример. «Является ли $\{ 1, 2, 3 \}$ группой?»

Пример. «Каков ряд Фурье для $\sin x + \sin \pi x$

А вот ещё более глупые примеры.

Пример. «Является ли прямоугольник простым?»

Пример. "$17 \in 3$?"

Пример. «Каков ряд Фурье для пустого множества?»

Объединяет все эти примеры то, что они являются ошибками типизации: это попытки применения некого математического процесса к математическому объекту, который никак не может быть входными данными для него. Если для ответа на эти вопросы вы попытаетесь написать программу на каком-нибудь высоко математическом языке программирования, то она (я надеюсь!) не скомпилируется.

Математические объекты обычно не воспринимаются явно как имеющие типы в том же смысле, что и объекты в языках программирования с системой типов. Предполагается, что обычная математика должна формализироваться в системе Цермело — Френкеля (ZF), возможно, с аксиомой выбора, а в ZF каждый математический объект конструируется как множество. В этом смысле все эти объекты имеют одинаковый тип. (В частности, вопрос "$17 \in 3$" вполне логичен в ZF! И это одна из причин, по которой стоит не любить ZF в качестве основы для математики.) Однако, мне кажется, что на практике математические объекты неявно воспринимаются, как имеющие типы, и такой образ мышления математики усваивают, но не часто обсуждают.
Читать дальше →


Comments 0