дыбр

[juan_gandhi]

 Утром проснулся-то рано, да мы как-то подзатянули, зарядка там всякая - и выехали уже в девятом часу.

Приезжаем на работу - а там хоп, завтраки отменили. Окей... буду позже ездить. 

Проверил у студентов домашку, написал новую им. Пускай.

Вдруг дошло до меня, что в теории множеств ZFC нет, вообще говоря, способа выразить такую вещь как y = f(x). Есть только {f(x)} - но способа вынуть контент из {} не существует; про этот контент можно только утверждения писать, типа ∀y∈{f(x)}...

Не знаю, понятно ли изложил. Но, короче, теория множеств вдруг бац - и это. Конечно, когда вы пишете функцию синус, вы знаете, что за f(x) - но в целом в ZFC функции задаются как их графики, а не как "способ вычислить". Вот так вот мы где-то, философски, касаемся невычислимых функций, да? Но речь не о них.

Ладно. Надо было еще зафигачить в гитхаб ихний апдейт книжки и главы, но вот не дошли руки.

Дома меня подобрали у станции. Так-то мы собирались приехать и пойти гулять на закате, но что-то лень стало. И интернета нету. 

Выключать и включать модем, как это советует суппорт, я умею. Не помогает. Стал на сайт комкаста лазить (ну у меня же телефон еще есть); там сайт половина чота не работает. Стал им звонить. Робот такой говорит - выключите, включите, и мы через 10 минут вам позвоним. Поужинал, не позвонили. Звоню снова. Робот, конечно, ничего про меня не помнит, и говорит, выключите-включите. Я говорю - не хочу. А, так вы уже выключали-включали. У вас модем не подключен. Подключите. И какой у вас адрес. Да бля. Удалось от роботихи наконец добиться, чтобы "агента" подключила. Агент такой - выключите и включите. Шесть раз, говорю, это делал. Ну и так далее. Но он упорный, ну бля, ну вот, еще раз пойду выключу и включу. Сделал. Он там чота потыкал, говорит - да у вас модем не работает. Дык, говорю. Короче, с агентом, веселым филиппинским парнем, расстались друзьями, а я поехал, в семь вечера, темень, в офис комкаста.

Комкаст теперь назывется Xfinity, офис у них как у Эпла, и куча всяких полезных штучек рекламируется, надо будет жену привезти, может, чего и купим. На входе суровый негр спросил типа "чо надо", сказал ему, вот модем, и он не работает. Взял модем, посканил код, спросил мое имя, дал бумажку, велел сидеть и ждать. Потом одна мучача вызвала меня и выдала новый модем. Все!

Приехал домой, включил новый модем, а он сука даже знает, как мои вайфаи раньше назывались, и какие у них пароли! Короче, вжик-вжик, и все заработало. Вот уважаю, да.

И уже после этого пошел, усталый и довольный, в душ.

И обсуждать меры по выживанию в грядущей чуме. Все стремно. Жора правильно написал, а Миша как-то мутит. Ну Миша профессионал, ему нельзя панику гнать населению.

Не, нам-то чо в субарбии, мы внеплановые близкие контакты можем вообще прекратить, а в магазин в перчатках (да и на работу тоже). Вот городским херово придется. 

Comments

[punk_floyd]

>Приезжаем на работу - а там хоп, завтраки отменили
кризис?

>Жора правильно написал, а Миша как-то мутит.

кто это Жора и Миша?

[juan_gandhi]

https://gxachaturov.dreamwidth.org/
https://nsn.fm/society/epidemiolog-shansy-zarazitsya-koronavirusom-v-rf-prakticheski-ravny-nulu

[66george]

Мучача кукарача. Можно добавить дескриптор (йота-термы, "такой единственный икс, что верно фи(икс)"). Тогда с логикой будут проблемы, потому что он не всегда определён. Но это сделано давно многими разными способами ("свободная логика", позволяет работать с не везде определёнными термами). А вот я нашёл на линкедине Тодда Вилсона, который в 2001 году написал убойную статью про интуиционистской доказательство теоремы Цермело. И больше никаких его статей интернет не знает, кроме диссертации 94-го года. Спрашиваю, Вы тот самый Тодд Вилсон? А где ещё статьи? Да, говорит, тот самый, но на эту тему больше не пишу, завязал. Притом он на профессорской должности (computer science), но и компьютерных статей тоже не видно. Рассказал историю Куклеву, но Куклев только стиральными машинами интересуется, будет ли в космосе работать стиральная машина.

[juan_gandhi]

Спасибо. Но я этой его теоремы не понимаю. Известно, что в обычной ZF упорядочиваемость эквивалентно AC. В его тексте начинаем с "мы в элементарном топосе, давайте возьмем множества, да заодно определим типы". Выглядит бредом, в моих глазах. IZF я еще не смотрел. и что конкретно Фрейд в 87-м году доказал, тоже не смотрел. Посмотрю потом.

[66george]

Есть "глобальный" вариант теоремы Цермело (из аксиомы выбора следует вполне-упорядочиваемость всех множеств), а есть локальный: работаем без аксиомы выбора, предполагаем, что для какого-то множества А есть функция выбора (по каждому непустому подмножеству А выдающая некоторый его элемент) и доказываем, что множество А можно вполне-упорядочить. Глобальный вариант легко доказывается интуиционистски, но по неожиданной причине: из аксиомы выбора следует закон исключённого третьего! Локальный вариант доказал Фрейд в длинной сложной статье на языке топосов. В конце статьи бахвалился примерно так "Теоретически, можно перевести доказательство на язык теории типов, но вряд ли кому под силу". И вот Тодд Вилсон дал доказательство на две странички, используя кванторы по высказываниям.

[juan_gandhi]

А, понял. Да, логично.

Из AC следует булевость, знамо дело.

Бахвальство Фрейда

[66george]

It is the author's estimation that such an 'elementary proof' will be extracted from this proof only by machine translation using machines not yet in existence. It is the author's further estimation that such a proof will be verifiable only via further machines not yet even in theoretical existence.

[alexander_panin]

>> Комкаст теперь назывется infinity

Xfinity?

[juan_gandhi]

О, Xfinity, конечно. Пойду поправлю.

[twilightshade]

За свою жизнь я подключал интернет через: простой модем, сотовый телефон как модем, асинхронно через спутниковую тарелку и мобильный телефон, adsl-модем, теперь вот через простой wifi-роутер.

[malobukov]

> меры по выживанию в грядущей чуме

Если речь про nCoV-2019, так он к маю должен пойти на спад. Но к следующей чуме готовиться всё равно полезно, это да.

[juan_gandhi]

Дай бы бог.

[cyrill_999]

И интернета нету.
Ну так... в первых числах ниже ноля было, ничего удивительного.
...олово в бессвинцых припоях, после перехода в в-фазу, не умеет себя назад "правильно-собирать"

[kondybas]

Собсно, в базах данных давно по этим граблям топчутся. И, ввиду невычислимости фунций, фетчат f{x} перебором - более или менее быстрым. Для унимодальных еще туда-сюда, а если нет - то опачьки. Эн пополам.

[juan_gandhi]

Базы данных - это прикладная модель теория множеств, ограниченный сегмент в смысле (без powerset).

Но поразительно, как народ не понимает этой простой вещи про {f(x)}. Да и я только на той неделе понял.

Аксиома выбора дает иллюзию, но это иллюзия.

[kondybas]

Все БД, вообще говоря, это куцые и кривые эмуляции множеств списками, со всеми вытекающими. Разница колоссальна, но ее тоже ухитряются не видеть.

[juan_gandhi]

B-trees, может быть?

Потом, не забываем про мутабельность и ее проблемы.

[kondybas]

Мы не умеем и даже не знаем, как реализовать множества, иначе, как посредством тюринговского итератора. Шаг вслепую, обмацали, либо сунули в мешок, либо сразу шаг дальше. Это приводит к разным пакостям, вроде вложенных циклов, и невозможности выполнить теоретически безупречную операцию за разумное время. Отсюда растет довольно позорная концепция денормализации. Ну, и у К.Дж.Дейты на тысячестраничный талмуд индексам отведен всего один абзац, да.


Как можно сделать сет-машину, я примерно догадываюсь, нечто вроде тотального параллелизма, где ячейка стораджа одновременно есть и процессинг-юнит, и всякий "объект" обрабатывается занятым им набором PU. Чтобы можно было рявкнуть: агнцы направо, козлища налево, к конъюнкции товсь! И шоб все завертелось. Но как оно там внутре будет устроено - хз, фантазии не хватает.