AT
Size: a a a
2020 December 06
TT
Это какой-то тонкий йумор?
VM
показывают на собесе и спрашивают "что вы видите на этой картинке"?
AG
а всякие пруф ас ис тенты же помогают в познании учоным?
смотря каким ученым
AG
пока в основном PL теоретикам
AG
Антон, можно ли обобщить чего-нибудь так, чтобы с лёгкостью переиспользовать в разных доказательствах. Например, диагональный метод Кантора используется и при доказательстве несчётности действительных чисел, и при доказательстве несуществования универсальной МТ, и (кажется) при доказательстве теоремы Гёделя.
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
ну как правило такие переиспользуемые вещи это или какие то технические тактики или солверы для какой то разрешимой теории типа той же арифметики пресбургера
NL
ну как правило такие переиспользуемые вещи это или какие то технические тактики или солверы для какой то разрешимой теории типа той же арифметики пресбургера
Да, Антон уже ответил. Меня слегка напрягает, что такие тактики или солверы -- это сущности не первого класса.
B
кто что знает про компанию люксофт?
λ
если такие вопросы задаешь, то иди
AT
если такие вопросы задаешь, то иди
bad dog
B
если такие вопросы задаешь, то иди
кек, а как верно сформулировать вопрос?
AT
кек, а как верно сформулировать вопрос?
"насколько ужасен люксофт как галера?"
B
"насколько ужасен люксофт как галера?"
тогда можно ответ на этот вопрос?)
AT
Да, Антон уже ответил. Меня слегка напрягает, что такие тактики или солверы -- это сущности не первого класса.
Мне кажется, что фундаментальная система не должна иметь такие вещи как сущности 1-го класса. Уже сейчас "ядра" систем довольно сложны.
Хотя может в далеком будущем что-то мы узнаем про это.
Хотя может в далеком будущем что-то мы узнаем про это.
AG
Да, Антон уже ответил. Меня слегка напрягает, что такие тактики или солверы -- это сущности не первого класса.
ну так это метапрограммирование
KS
/get tldr
VM
понв куда будут выкладывать (если будут) видосы/доклады с прошлой конфы? и че там было годного а что вода/гавно?
R
V. M.
понв куда будут выкладывать (если будут) видосы/доклады с прошлой конфы? и че там было годного а что вода/гавно?
Записи понвоференции доступны