Что значит «модель у множества»?
Модель бывает у теории.
У теории множеств первого порядка — есть счетная модель, да.
Но в тот момент, когда мы рассматриваем модель теории второго порядка — уже ниоткуда, вроде, счётность получиться не может.
В Расте — когнитивной сложностью базовых операций (да и самой концепции владения и заимствования (ownership/borrow)).
Если их понять — собрать безопасное низкоуровневое приложение становится относительно просто.
В С — базовые операции гораздо более простые, но собрать безопасное приложение поверх них — очень сложная задача.
Так именно в эту же: если инструмент «тонкий», то пользоваться им сложно (или тяжело, что с точки зрения пользователя почти одно и то же).
Нужны абстракции правильной толщины — если абстракция слишком бедная, то ей пользоваться сложно (не с точки зрения предсказания, какой получится результат выполнения этой одной строчки, а с точки зрения того, как эта одна строчка влияет на всю программу), потому что она позволяет слишком большим количеством способов отстрелить себе ногу.
А если слишком богатая, то оказывается сложно предсказать поведение системы «под капотом» (например, в случае управления памятью это будет сборщик мусора, который добавляет новые задержки, над которыми нет контроля).
Вопрос в том, как измерять сложность.
Каждая отдельная команда управление памятью — проще, конечно, в С.
Но для не-тривиальной программы на С, следить (руками) за всеми инвариантами (чтобы не получить use after free, double free, etc) уже сложнее (хотя каждый отдельный примитив по-прежнему проще).
Один из первых примеров не работает: fn main() {
let alice = Person { name: String::from("Alice"), age: 30 };
baz(&alice); // работает
bin(&alice); // ошибка!
bin(&mut alice); // а это работает
}
видимо, должно быть
let mut alice = Person { name: String::from("Alice"), age: 30 };
Не возможно получить мутабельную ссылку на немутабельный объект (и дальше это тоже упоминается).
Так проблема с тем, что значит «задаваться формулой».
Если мы говорим «задаётся формулой» = «перечислим снизу», то начинается беда: разность двух перечислимых снизу чисел уже не обязательно перечислима снизу.
Ну, например, есть невычислимые числа, которые можно перечислить снизу. То есть есть бесконечная последовательность, такая что её сумма не больше единицы, но при этом, нет алгоритма, который бы давал эту сумму с наперед заданной точностью.
Проблема с размером аккумулятора для фолда.
Если мы не разрешаем менять внешний (для цикла) контекст, то в аккумуляторе должен быть вся изменяющаяся часть контекст (и возникает проблема с аллокацией, о которой уже упомянали).
А если разрешаем мутации внешнего контекста — то уже не возможна замена на фолд.
Добавим каждому муравью бусинку своего цвета.
При столкновении будем не только отражать муравья, но и менять бусинки у муравьев.
Тогда у каждого муравья всегда есть ровно одна бусинка.
Каждая бусинка двигается равномерно и прямолинейно (никуда не отражается).
Все бусинки упадут за 1 секунду, значит и все муравьи тоже.
Ну, если подходить аккуратнее, то статистический анализ может быть и на разрешающих алгоритмах.
Но тогда у него будут фолс-позитиврешы (какие-то алгоритмы, которые на самом деле разрешающие, будут считаться не-разрешающими).
Перечислимые (а не разрешимые) множества с точки зрения программирования (и теоретического CS) гораздо более правильная абстракция.
Хотя бы потому, что множество программ перечисляющих множества — разрешимо (это, примерно, все программы правильной сигнатуры), а множество программ разрешающих множество — нет (и даже не перечислимо).
Да, конечно, diag(S) наследует перечислимость или разрешимость от S.
Если S разрешимо, то и diag(S) разрешимо.
Если S перечислимо, то и diag(S) станет перечислимым.
Это даже распространяется дальше, например, на перечислимость снизу или сверху (которая нужна для полумер и колмогоровской сложности соответственно).
Конечно, задача разрешить diag от перечислимого множества — не разрешима (и для конкретного перечислимого множества может являться просто проблемой остановки).
Но сам diagonal(S) — вполне конструктивен (настолько же, насколько S конструктивно. Например, если в S вычислимы все клетки, то и diagonal(S) вычислим ровно в том же смысле).
И даже diagonal(S) != S_i тоже вычислимо проверяется. После этого возникает проблема с переходом к бесконечности — достаточно ли, эффективно по i доказывать X != S_i, или нужно больше, чтобы сказать X \not in S. Насколько я помню классическую конструктививную логику — этого достаточно, но я не полностью уверен.
Чистый ассемблер уже является тьюринг-полным.
Модель бывает у теории.
У теории множеств первого порядка — есть счетная модель, да.
Но в тот момент, когда мы рассматриваем модель теории второго порядка — уже ниоткуда, вроде, счётность получиться не может.
И, насколько я помню, там как-то очень нехорошо с полнотой.
Если их понять — собрать безопасное низкоуровневое приложение становится относительно просто.
В С — базовые операции гораздо более простые, но собрать безопасное приложение поверх них — очень сложная задача.
Нужны абстракции правильной толщины — если абстракция слишком бедная, то ей пользоваться сложно (не с точки зрения предсказания, какой получится результат выполнения этой одной строчки, а с точки зрения того, как эта одна строчка влияет на всю программу), потому что она позволяет слишком большим количеством способов отстрелить себе ногу.
А если слишком богатая, то оказывается сложно предсказать поведение системы «под капотом» (например, в случае управления памятью это будет сборщик мусора, который добавляет новые задержки, над которыми нет контроля).
Каждая отдельная команда управление памятью — проще, конечно, в С.
Но для не-тривиальной программы на С, следить (руками) за всеми инвариантами (чтобы не получить use after free, double free, etc) уже сложнее (хотя каждый отдельный примитив по-прежнему проще).
Один из первых примеров не работает:
fn main() {let alice = Person { name: String::from("Alice"), age: 30 };
baz(&alice); // работает
bin(&alice); // ошибка!
bin(&mut alice); // а это работает
}
видимо, должно быть
Не возможно получить мутабельную ссылку на немутабельный объект (и дальше это тоже упоминается).
Если мы говорим «задаётся формулой» = «перечислим снизу», то начинается беда: разность двух перечислимых снизу чисел уже не обязательно перечислима снизу.
Если мы не разрешаем менять внешний (для цикла) контекст, то в аккумуляторе должен быть вся изменяющаяся часть контекст (и возникает проблема с аллокацией, о которой уже упомянали).
А если разрешаем мутации внешнего контекста — то уже не возможна замена на фолд.
При столкновении будем не только отражать муравья, но и менять бусинки у муравьев.
Тогда у каждого муравья всегда есть ровно одна бусинка.
Каждая бусинка двигается равномерно и прямолинейно (никуда не отражается).
Все бусинки упадут за 1 секунду, значит и все муравьи тоже.
Дополнительно, не пересекаются скрещивающиеся, но это не отменяет того, что параллельные не пересекаются по определению.
Но тогда у него будут фолс-позитиврешы (какие-то алгоритмы, которые на самом деле разрешающие, будут считаться не-разрешающими).
Хотя бы потому, что множество программ перечисляющих множества — разрешимо (это, примерно, все программы правильной сигнатуры), а множество программ разрешающих множество — нет (и даже не перечислимо).
Если S разрешимо, то и diag(S) разрешимо.
Если S перечислимо, то и diag(S) станет перечислимым.
Это даже распространяется дальше, например, на перечислимость снизу или сверху (которая нужна для полумер и колмогоровской сложности соответственно).
Конечно, задача разрешить diag от перечислимого множества — не разрешима (и для конкретного перечислимого множества может являться просто проблемой остановки).
Но сам diagonal(S) — вполне конструктивен (настолько же, насколько S конструктивно. Например, если в S вычислимы все клетки, то и diagonal(S) вычислим ровно в том же смысле).
И даже diagonal(S) != S_i тоже вычислимо проверяется. После этого возникает проблема с переходом к бесконечности — достаточно ли, эффективно по i доказывать X != S_i, или нужно больше, чтобы сказать X \not in S. Насколько я помню классическую конструктививную логику — этого достаточно, но я не полностью уверен.
Только диоганальный метод — он вполне себе конечный.
Он по индексу i возвращает значение ячейки (i,i) (возможно как-то модифицированное).
Он же явно строит двумерной бесконечной матрице «не-диагональ».