Oℕ
Emelian Piker (Евгений)
Ну да, а если говорить про обычный, nо он адитивен чтоли ? Тоесть это некомутативно и аддитивно ?
Какой обычный?
Size: a a a
2019 June 23
ЕО
Emelian Piker (Евгений)
А мультипликативная дизюнкция это что тогда ?
Вы смешиваете понятия разных отраслей математики и получается каша, вот и всё. В хаскеле нет поддержки линейной логики, там классическая теория типов
Oℕ
Мне сложно понять, что такое аддитивность в данном контексте
EP
Какой обычный?
Ну да, вот я например написал некую функцию композиции case, они какбы добавляются друг к другу
ЕО
Есть понятия "произведение" и "сумма" типов. (A,B) — произведение, Either A B — сумма
EP
Есть понятия "произведение" и "сумма" типов. (A,B) — произведение, Either A B — сумма
Ну да, произведение это мультипликативная Конъюнкция. Вопрос что есть мультипликативная дизъюнкция ?
ЕО
Да ничего, нету в хаскеле линейной логики
Oℕ
Произведение имеет свойства и мультипликативной и аддитивной конъюнкций
ЕО
Из-за того, что тензорное произведение декартово, то мультипликативная и аддиктивная конъюкция совпадут
ЕО
Разделение имеет смысл только для недекартовых категорий
EP
Я согласен что haskell не самый самый. Хочу понять как надо было бы
EP
What about Linear Logic in Computer Science? Daniel Mihályi, Valerie Novitzká https://www.uni-obuda.hu/journal/Mihalyi_Novitzka_42.pdf
Oℕ
Emelian Piker (Евгений)
Ну да, произведение это мультипликативная Конъюнкция. Вопрос что есть мультипликативная дизъюнкция ?
Можно, как и написано в вики понять её через дуальность с тензорным
EP
Я вот например прочитал вики про пи исчисление, там есть оператор P = (A | B). Похоже что это именно мультипликативная дизюнкция
EP
A + B = ! (A * C) | ! (B * C) | C^⊥
__
левый и правый нейтральный элементы ввести да и всио
ЕО
У вас тут диалог за теорию типов и вычислений пошёл
NI
Emelian Piker (Евгений)
https://image2.slideserve.com/4188309/the-p-calculus-syntax-n.jpg https://www.slideserve.com/damian/lecture-1-the-pi-calculus-and-the-asynchronous-pi-calculus-catuscia-palamidessi
Прочитайте про моноидальные категории ;-)
EP
Ок, с композицией морфизмов всё понятно, это мультипликативная партиальная группа (группоид) с единицей. Морфизм можно понять как пермутацию, мы берём начальную пермутацию и применяем к ней пермутации.