МБ
Так с Haskell проблем нет. Там не нужны такие изыски. А вот с каким-нибудь ACL - проблема от энергичности
Size: a a a
2019 November 23
МБ
И может быть, как раз нужно нечто не банальное в качестве hom. Вот, кстати. Enriched categorical semantics for distributed calculi
NI
Надо будет заценить. Вроде, выглядит несложно.
2019 November 24
B
В логике (логике) ⊥ обозначает противоречие, т.е. произвольную формулу и её отрицание, и если мы не допускаем true contradictions, то это тривиально переводится в одноимённую константу, означающую тождественную ложь. Если мы занимаемся экзотикой и допускаем true contradictions, мы должны менять нотацию.
B
В теории типов ⊥ имеет другое содержание.
B
Кроме того, значения T и F -- это алгебра логики, а не логика.
B
В самой логике значений нет. Там модельная семантика для решения проблем с истиной, так как это решает проблемы семантических парадоксов по типу парадокса лжеца. Считать же, что истина или ложь -- такие же объекты, как и любые другие вещи, в логике некорректно. Но это допускается в алгебре.
B
В логике вместо значений, как в алгебре, и отношений выполнения (satisfaction relations), как обычно в логике, можно попробовать, что допускал и сам Тарский, аксиоматическое определение истины, где истина становится характерным предикатом.
B
ЕО
Brenoritvrezorkre
В самой логике значений нет. Там модельная семантика для решения проблем с истиной, так как это решает проблемы семантических парадоксов по типу парадокса лжеца. Считать же, что истина или ложь -- такие же объекты, как и любые другие вещи, в логике некорректно. Но это допускается в алгебре.
Мне кажется, что это не совсем корректное утверждение, это более зависит от подхода к формализации логики и металогических рассуждений.
B
Нет, это полностью корректное утверждение. В логике нет таких значений. В алгебре логики, которой логики тоже занимаются, они есть.
B
Либо если мы работаем с алгебраической семантикой (которая непопулярна, но была популярна в начале XX века), то там это следует просто в алгебраическом порядке.
ЕО
Ну просто "логика" это у вас что? Секвенциальное исчисление предикатов? Или раздел математики, изучающие формализации логических рассуждений?
B
Логика -- это логика. Набор характерных исчислений, теория моделей и теория доказательств.
ЕО
Ну вот вы взяли, например, и категориальную логику вычеркнули искусственно. Да и теория типов это раздел логики
B
Теория типов немного отделилась от логики, хотя если расширять определение, она туда входит, как и алгебра логики.
Категориальная логика дополняет логику категорными конструкциями, производя интерпретацию теории категорий в логику. Остальное то же самое.
Категориальная логика дополняет логику категорными конструкциями, производя интерпретацию теории категорий в логику. Остальное то же самое.
KV
Brenoritvrezorkre
Теория типов немного отделилась от логики, хотя если расширять определение, она туда входит, как и алгебра логики.
Категориальная логика дополняет логику категорными конструкциями, производя интерпретацию теории категорий в логику. Остальное то же самое.
Категориальная логика дополняет логику категорными конструкциями, производя интерпретацию теории категорий в логику. Остальное то же самое.
Вроде ж наоборот, там суть в том, что категорные конструкции проще строить не явно, а при помощи языка, например, логики
B
В логику как некоторое исчисление добавляются некоторые proof theoretic элементы и на базе этого понятия теории категорий. Затем мы переводим категории в это.
B
Алгебра логики и логика довольно близки. Например, о валентности некоторой логики как исчисления судят через алгебраические исследования. И квантовую логику ту же нельзя было построить без перевода в алгебру, а потом обратно, просто потому, что менялись алгебраические свойства операторов. Но всё же это разные области.