Goodstein, Hydra, a question
Nov. 12th, 2019 09:58 pmhttp://math.andrej.com/2008/02/02/the-hydra-game/
My question actually is this: can Goodstein sequence to be proven to stop in a lambda calculus? Naively, it should be.
And another question: can set theory be modeled in lambda? (Or should I reread Dana Scott's works?)
My question actually is this: can Goodstein sequence to be proven to stop in a lambda calculus? Naively, it should be.
And another question: can set theory be modeled in lambda? (Or should I reread Dana Scott's works?)
дошла до меня еще одна вещь
Jul. 11th, 2019 10:00 amМы привыкли, что вот всякие ресурсы в программе - они внешние, их может быть дефицит (коннекшены, файл-хендлы, память).
А надо. Время. Рассматривать тоже как ресурс. Время - это ресурс. Не знаю, линейная логика справится с этим или чо. Но если мы вообразим, что вот наше вычисление захватывает определенный кусок времени и им пользуется - как в расте, то, может быть, и код будет выглядеть по-другому. А то все таймауты, таймауты, ой, так получилось. И т.д.
Время - это ресурс.
А надо. Время. Рассматривать тоже как ресурс. Время - это ресурс. Не знаю, линейная логика справится с этим или чо. Но если мы вообразим, что вот наше вычисление захватывает определенный кусок времени и им пользуется - как в расте, то, может быть, и код будет выглядеть по-другому. А то все таймауты, таймауты, ой, так получилось. И т.д.
Время - это ресурс.
фигня какая-то
Jan. 26th, 2019 09:41 amПару лет назад интервьюировался в Кариус, это такая генетическая контора. Мне там подбросили задачку на дом, на спарке чтобы искать патогены в сиквенсе. Ну т.е. подстроки. Я, будучи знаком с алгоритмом Укконена, не видел смысла использовать спарк, распараллелил все в одной программе, и все дела, 10 минут, готово. Но им не понравилось.
А вот сейчас у меня два таких вопроса уже возникает:
- При чем тут нахер спарк, если нужно искать подстроку в строке;
- Каким образом патоген холеры вообще вдруг оказывается в генах человека? Это вообще что, они не ебанулись часом? Это ж лысенковщина. - Тут я неправ. Они ищут не в генах человека, а в супе из генов, который получается, если просто взять капельку крови. (Кстати, а почему оно sequence?)
Ну и заодно хотелось бы вообще понять, что у людей в головах; но я не врач.
А вот сейчас у меня два таких вопроса уже возникает:
- При чем тут нахер спарк, если нужно искать подстроку в строке;
- Каким образом патоген холеры вообще вдруг оказывается в генах человека? Это вообще что, они не ебанулись часом? Это ж лысенковщина. - Тут я неправ. Они ищут не в генах человека, а в супе из генов, который получается, если просто взять капельку крови. (Кстати, а почему оно sequence?)
Ну и заодно хотелось бы вообще понять, что у людей в головах; но я не врач.
жопа с классом Set
Dec. 21st, 2018 04:53 am Я-то думал сейчас приплету ZFC, и роль C в этом деле, эндофунктор powerset, что там два функтора на самом деле; и монада из него; потом на топосы перейти, и все такое, потом посмотреть, а как оно в софтверной категории типов...
Все фигня. Ничего не работает. powerset нету, вообще-то говоря.
Все фигня. Ничего не работает. powerset нету, вообще-то говоря.
Вообще, стоит задуматься, а в типизированной лямбде... да и бестиповой, set можно задать, как adt? А хрен там. И знаете почему? а в бестиповой лямбде нет же равенства. Ну не эквациональная теория, как я понимаю. В том смысле, что равенство в виде лямбды не записывается. Не совсем определение эквациональной, скорее что-то вроде внутренней эквациональности.
Поэтому что? Поэтому надо, как Бартош и предложил, впендюрить какое-нибудь отношение эквивалентности. Вместо равенства сойдет. И "множество", как adt, задается через это отношение. На лямбде это можно навалять; будет много лямбд, но выразить можно.
А смысл? Как-то очень неуклюже, очень.
Статей не нашел на эту тему никаких, одни благоглупости, вроде того, что в википедии написано.
Короче, серьезная тема, да? Приехали.the book I am reading these days
Dec. 7th, 2010 05:45 pmyosefk.com - an infinite source of knowledge and inspiration.