Size: a a a

Теория категорий

2019 June 23

EP

Emelian Piker (Евгений) in Теория категорий
Ну давайте найду текст
источник

ЕО

Евгений Омельченко in Теория категорий
Давай
источник

EP

Emelian Piker (Евгений) in Теория категорий
For example, a military general who knows that he will be attacked from either the east or the north must divide his forces between both fronts, even if the attack will only come from one direction; thus what he has is “attack from east ⅋ attack from north”. (If he had spies out that would be able to inform him in advance where the attack was coming from so that he could concentrate his forces there, then he would instead have an additive disjunction “attack from east ⊕ attack from north”.)
источник

EP

Emelian Piker (Евгений) in Теория категорий
источник

EP

Emelian Piker (Евгений) in Теория категорий
Щяс там ещё было про &
источник

EP

Emelian Piker (Евгений) in Теория категорий
Emelian Piker (Евгений)
For example, a military general who knows that he will be attacked from either the east or the north must divide his forces between both fronts, even if the attack will only come from one direction; thus what he has is “attack from east ⅋ attack from north”. (If he had spies out that would be able to inform him in advance where the attack was coming from so that he could concentrate his forces there, then he would instead have an additive disjunction “attack from east ⊕ attack from north”.)
Вот сдесь проясняется про +
источник

ЕО

Евгений Омельченко in Теория категорий
Emelian Piker (Евгений)
Ну давайте найду текст
Мне кажется, что нельзя напрямую линейную логику проектировать в обычные вычисления. Особенно классическую линейную логику, а не интуитивисткую
источник

NI

Nick Ivanych in Теория категорий
Евгений Омельченко
Мне кажется, что нельзя напрямую линейную логику проектировать в обычные вычисления. Особенно классическую линейную логику, а не интуитивисткую
Напрямую будет, попросту, некорректно.
А про именно логику, можно посоветовать Шульмана что-то типа линейная логика для интуииониста.
Если интересно, вспомню точнее название и ссылка найдётся с ходу, скорее всего.
источник

EP

Emelian Piker (Евгений) in Теория категорий
Additive conjunction (“with”) 1 & 2 has the neutral element T. It
expresses that only one of the actions described by 1 and 2 will be
performed. But we can deduce or anticipate from an environment which
of them will be performed. This formula can be considered as an analogy
with the statements if-then-else and case in programming languages.
Somethimes it is called external nondeterminism (dependent choice);
источник

Oℕ

Oleg ℕizhnik in Теория категорий
Вопрос в семантике мультипликативной дизъюнкции?
источник

NI

Nick Ivanych in Теория категорий
Изначально, вопрос в том, есть ли строгое определение "аддитивного" и "мультипликативного".
Вопрос начался с бинарных операций.
источник

EP

Emelian Piker (Евгений) in Теория категорий
Бартоз называет Either a b почемуто суммой, это не мультипликативная дизюнкция случайно ? Мне кажется тут путаница
источник

ЕО

Евгений Омельченко in Теория категорий
Ну Either a b это прямая сумма
источник

NI

Nick Ivanych in Теория категорий
Emelian Piker (Евгений)
Бартоз называет Either a b почемуто суммой, это не мультипликативная дизюнкция случайно ? Мне кажется тут путаница
Копроизведение (обычный интуиционистский вариантный тип) принято называть суммой.
источник

Oℕ

Oleg ℕizhnik in Теория категорий
Either - это декартова сумма, она обладает большей силой, чем линейные варианты дизъюнкции
источник

EP

Emelian Piker (Евгений) in Теория категорий
Emelian Piker (Евгений)
Additive conjunction (“with”) 1 & 2 has the neutral element T. It
expresses that only one of the actions described by 1 and 2 will be
performed. But we can deduce or anticipate from an environment which
of them will be performed. This formula can be considered as an analogy
with the statements if-then-else and case in programming languages.
Somethimes it is called external nondeterminism (dependent choice);
Вот про case. В haskell case какбы некомутативен если его попытаться представить как оператор. Можно даже написать бинарную функцию которая собирает свой case
источник

EP

Emelian Piker (Евгений) in Теория категорий
Евгений Омельченко
Ну Either a b это прямая сумма
А мультипликативная дизюнкция это что тогда ?
источник

Oℕ

Oleg ℕizhnik in Теория категорий
Некоммутативность хаскельного кейс исчезает, если говорить про паттерн матчинг типа сумы
источник

Oℕ

Oleg ℕizhnik in Теория категорий
Т.е. если сузить паттернматчинг до суммы морфизмов, он будет коммуиативен
источник

EP

Emelian Piker (Евгений) in Теория категорий
Oleg ℕizhnik
Некоммутативность хаскельного кейс исчезает, если говорить про паттерн матчинг типа сумы
Ну да, а если говорить про обычный, nо он адитивен чтоли ? Тоесть это некомутативно и аддитивно ?
источник