Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Категорное

Некоторое время назад я в очередной раз занимался категорными моделями линейной логики, где тип A & B (“ящик, из которого можно на выбор взять сущность типа A или сущность типа B, но не обе одновременно”) интерпретируется категорным произведением, и вдруг меня переклинило. Как же это так, подумал я, ведь категорное произведение как-бы означает возможность размножения сущностей, а в линейной логике так быть не должно. Пришлось подумать чуть подробнее.

Итак, из определения категорного произведения следует существование переходов diagA из A в (A & A) для каждого типа A. Но это само по себе это не означает возможности размножения сущностей, потому что из (A & A) законы линейной логики позволяют взять альтернативно только левую или только правую компоненту. Как выразить концепцию альтернативности этого выбора?

Идея довольно проста: в категории не должно быть никаких переходов, “смешивающих” компоненты произведения. Все структурные переходы (т.е. те, чьё существование следует из определения категорного произведения) компоненты не смешивают, они только переставляют их местами, размножают и/или отбрасывают. Отсутствие “смешивающих компоненты переходов” означает, что любой переход из (A & B) должен раскладываться в композицию действующих на компоненты по отдельности fA и fB, и какого-то структурного перехода g.

Это очень ограничительное условие:
– Оно исключает существование каких-либо нетривиальных пределов, не являющихся произведениями.
– Оно исключает декартовую замкнутость в присутствии нетривиальных копределов.

Противоположная крайность: категорное произведение задаёт классический объект пар, если категория контекстуально-замкнута, см. каппа-исчисление.
Subscribe

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments