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

[udpn]

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

Comments

[voidex]

произведение обычное: a × b (первое значение и второе)
обобщение: a₁ × ... × aₙ (для индекса есть значение)
зависимое произведение: ∏ a P (ты ему индекс - (x : a), а он тебе результат - P x)

сумма обычная: a + b (одно или другое)
обобщение: a₁ + ... + aₙ (индекс и какое-то значение)
зависимая сумма: ∑ a P (индекс (x : a) и значение - P x)

[udpn]

Ну это я вообще в рамках юмора.

Так-то понятно, что сигма это что-то типа дискретного интеграла, а интеграл даже несмотря на то, что суммирует площади прямоугольников, является произведением, что в физике сразу видно в размерностях величин.

Просто какая-то накладка с терминологией неприятная.

[sassa_nf]

гм. Не понятно, как тут интегралы помогают.

Категорные лимит и колимит всё объясняют - и что это за обозначения, и каков у них смысл. (Как там размышлял настоящий изобретатель этих обозначений - неважно; но категорное объяснение толкует неплохо.)

Лимит - это такой объект диаграммы, в который есть уникальная стрелка из всех конусов диаграммы, и при этом диаграмма коммутирует. Это обобщение проекций тупля.

Так, X - это произведение нескольких типов, если из X существуют стрелки во все типы, на которые "опирается" конус. По идее можно было бы стрелки (проекции) пронумеровать, но в общем виде их индексируют некоторым сетоидом. Ну и запись Πx:AB(x) однозначным образом описывает такой тип и все возможные стрелки из него. Взят символ произведения Π по той причине, что любой объект A можно представить в виде произведения с 1: A ≡ A×1, поскольку из любого объекта есть стрелка в себя и в терминальный объект 1 (а также A является терминальным среди всех конусов, опирающихся на A и 1

[sassa_nf]

что-то не так :-) и там, и сям индекс от 1 до n.

[sassa_nf]

О, можно ещё так попробовать:

Зависимый тип B : A → Type - это на самом деле семейство типов. Так вот, "произведение ∏" и "сумма ∑" - имеются в виду произведение и сумма всех типов данного семейства