M
Нет бы сидеть, хихикать
Size: a a a
2021 March 16
M
А он грустит!
AT
господа логики, расскажите пожалуйста, что такое contraction
это одно из структурных правил в логике, типа ты можешь забивать на одинаковые предпосылки и считать, что она у тебя одна
но если ты это правило убираешь, то получаешь афинную логику (похожа на линейную, но можно 0 раз использовать переменные)
но если ты это правило убираешь, то получаешь афинную логику (похожа на линейную, но можно 0 раз использовать переменные)
(
ой, пардон, не contraction
AG
господа логики, расскажите пожалуйста, что такое contraction
AG
контракция - можно мержить одинаковые предпосылки, викенинг - можно добавлять левые
AG
это в логическом прочтении, в программистском будет снизу вверх
(
почему там можно добавлять левые
AG
контракция - можно копировать переменные, викенинг - можно выбрасывать
(
это типа из контекста какие-то пропозиции?
AG
почему там можно добавлять левые
если из того что "вася негр" и "негры черные" следует что "вася черный"
то из того что "вася негр", "негры черные" и "петя китаец" следует что "вася черный"
то из того что "вася негр", "негры черные" и "петя китаец" следует что "вася черный"
AT
(
если из того что "вася негр" и "негры черные" следует что "вася черный"
то из того что "вася негр", "негры черные" и "петя китаец" следует что "вася черный"
то из того что "вася негр", "негры черные" и "петя китаец" следует что "вася черный"
понял
AG
сейчас у меня идея попробовать привязать линейные сессионные типы через асинхронную игровую семантику к сепарационке
AG
и посмотреть как оно может быть связано с "мета-сепарационкой" контекстов в линейщине