Специализни шаблонца!

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

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

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

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

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

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

Edited at 2015-05-18 17:08 (UTC)

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

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

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

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

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

Так, Y - это сумма нескольких типов, если в Y существуют стрелки изо всех типов, на которые "опирается" коконус. Можно было бы стрелки (инъекции) пронумеровать, но в общем виде их индексируют некоторым сетоидом. Соответственно, запись Σx:AB(x) однозначным образом описывает тип и все возможные стрелки в него. Символ суммы Σ по той причине, что любой объект A можно представить в виде суммы с 0: A ≡ A+0, поскольку в любой объект есть стрелка из себя и из инициального объекта 0.


data Stream a = S {head :: a} {tail :: Stream a} -- произведение типов a и Stream a, описываемое стрелками head :: Stream a -> a и tail :: Stream a -> Stream a

Тогда Π-тип - это функция, позволяющая выбрать либо head, либо tail с помощью некоторого типа-индекса (и скрывает Stream a "внутри").


data Nat = Zero | Succ Nat -- сумма типов () и Nat, описываемая стрелками Zero : () -> Nat и Succ : Nat -> Nat

Тогда Σ-тип - это результат функции, которая некоторым образом выбрала одну из инъекций - один из конструкторов, и передала этому конструктору значение нужного типа.

Разложение Σ на проекции - вопрос чисто технический; это тупль на уровне, на котором категория не оперирует, т.е. произведение не в том же смысле, в каком произведением является A×B. Это всего-лишь 2×Y, никакого произвола с выбором индекса проекций.

Edited at 2015-05-18 22:30 (UTC)

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

(Удалённый комментарий)
А там вообще плохие курсы пока, они же только начали. Если товарищ слушал что-то по математике столь же омерзительное, как их курсы по С++, то я могу его понять.

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

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

Например, элемент типа ∏(x : A) B(x) - это кортеж из A значений типов семейства B, по одному B(x) на каждое x:A - декартово произведение B(x) для всех x:A. Эквивалентно выражается в виде проекций кортежа для каждого индекса x:A - функция π:(x:A)→B x.

Тогда элемент типа ∑(x : A) B(x) - это элемент disjoint union значений типов семейства B. Если вспомнить, как пишется disjoint union, ∏ вверх ногами, ∐, и как он определяется - как тупль из значения и индекса, указывающего, из какого множества семейства значение взято, то это и есть сигма, ∑. Disjoint union иногда так и записывают, через ∑, а не ∐. Грубо говоря, для просто union достаточно было бы указать значение типа B(x) для некоторого x:A. А для disjoint union нужно ещё и указать само x:A, индексирующее тип из семейства B - "номер" инъекции, индекс конструктора. Так что, это сумма в том же смысле, в каком disjoint union можно было бы назвать суммой множеств.

  • 1
?

Log in

No account? Create an account