Oℕ
Извините, а какие лекции вы смотрите? В pinned message только тексты вроде, видео-лекций нет. Наверное пропустила, но долистать не могу. Спасибо!
Size: a a a
2019 November 18
Oℕ
Извините, а какие лекции вы смотрите? В pinned message только тексты вроде, видео-лекций нет. Наверное пропустила, но долистать не могу. Спасибо!
Это уже не лекции, а серия митапов
https://www.youtube.com/playlist?list=PLZ6v4yxqn3cRE3YvsSesUHkva_pyMDMEW
https://www.youtube.com/playlist?list=PLZ6v4yxqn3cRE3YvsSesUHkva_pyMDMEW
2019 November 19
LB
Это уже не лекции, а серия митапов
https://www.youtube.com/playlist?list=PLZ6v4yxqn3cRE3YvsSesUHkva_pyMDMEW
https://www.youtube.com/playlist?list=PLZ6v4yxqn3cRE3YvsSesUHkva_pyMDMEW
Спасибо!
2019 November 21
МБ
У меня опять, наверное, специфичный вопрос. Вот берём мы бестиповое lambda-исчисление и строим ДЗК с соответствующим объектом, в котором оно живёт. Что будет стрелками в этом моноиде? И зависит ди определение от того, какая стратегия редуцирования термов выбрана: в естественном порядке или в энергичном?
ЗП
а при чем тут стратегии вычислений к категорной семантике?
NI
а при чем тут стратегии вычислений к категорной семантике?
При том, что некоторые лямбда-термы не будут являться стрелками.
ЗП
При том, что некоторые лямбда-термы не будут являться стрелками.
ну если избавиться от парадоксов возможных?
NI
Бывюат термы, которые в нормализующей стратегии (например, ленивой) редуцируются до нормальной формы, а в строгой нет.
ЗП
Бывюат термы, которые в нормализующей стратегии (например, ленивой) редуцируются до нормальной формы, а в строгой нет.
ну это понятно, но вот ведь это только из-за возможных ботомов, а если в идеальном мире?
NI
Какой-такой идеальный мир, если уже задали условия — бестиповая лямбда, т.е., Тьюринг-полная и рассмотреть разные стратегии редукции?
МБ
А такими проблемами никто не занимался? Есть ли что почитать? Особенно меня интересует декартово произведение. Можно ли его определять для термов, которые определяют функции с разными областями определений? То есть, когда f(v) = u, а g(v) =
undefined для некоторого v.NI
А такими проблемами никто не занимался? Есть ли что почитать? Особенно меня интересует декартово произведение. Можно ли его определять для термов, которые определяют функции с разными областями определений? То есть, когда f(v) = u, а g(v) =
undefined для некоторого v.Декартово произведение для функций с разными областями определений делается.
То есть, (f, g) для функций f : a→b, g : c→d
То есть, (f, g) для функций f : a→b, g : c→d
МБ
А как?
NI
Тут надо решить, речь идёт пр оразную область определения или разную область значений ;-)
NI
А как?
Как функция из произведения (a,c), f и g композицируются с проекциями.
МБ
Пусть будет только область определения разная.
МБ
Это f × g?
NI
Пусть будет только область определения разная.
Область значений произведения всё равно будет (a,a)
МБ
Область значений произведения всё равно будет (a,a)
Ага, но это ok
NI
f : x→z, g : y→z
prod : (x,y) → (z,z)
prod q = (f . fst q, g . snd q)
prod : (x,y) → (z,z)
prod q = (f . fst q, g . snd q)