May 18th, 2015

Vash

Суммы и произведения

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