В большинстве вузовских учебников эта традиция продолжается.
Если учитывать англоязычные, то в большинстве учебников (а также научных статей, и так далее) ноль таки включается.
Понятие натурального числа вводится в начальной школе. В любом школьном учебнике (кроме, возможно, каких-нибудь маргинальных вариантов) ряд натуральных чисел начинается с единицы.
В начальной школе и отрицательных чисел нет, и корень из минус единицы брать нельзя.
А при чем тут 0? А при том что 0 в такой парадигме это не часть натуральных чисел, а нулл - маркер отсутствия числа, единица тоже спец маркер граничного случая, и только все остальные числа это числа.
Так я запутался, единицу в итоге тоже вычёркиваем из натуральных чисел?
А на самом деле всё проще:
Затем, что каждый вариант имеет свой АПИ. Из пустого контейнера ничего нельзя читать, а можно только мутировать/добавлять.
Тип функции для чтения
read : Fin n → Vec n a → a
гарантирует отсутствие чтений из пустого контейнера (и многое другое) без каких-либо крайних случаев.
Единичный контейнер это опшионал который в том числе можно трактовать и как массив, т.е. должен поддерживать оба АПИ
Оба — это какие?
Монадический API он уже поддерживает, и для одноэлементного массива он ведёт себя как надо. Можно вообще взять индексированные монады и получить
(>>=) : Vec n a → (a → Vec m b) → Vec (n × m) b
или, если хочется максимальной точности,
(>>=) : {out-count : a → Nat}
→ (xs : Vec n a)
→ ((x : a) → Vec (out-count x) b)
→ Vec (sum (map out-count xs)) b
после чего предыдущий вариант сводится к этому при out-count ↦ const m. С таким >>= изоморфизм Maybe a ≅ Vec 1 a строится (и доказывается) тривиально.
Не всегда наличие группы это благо, а даже может быть и явным косяком - нулл ошибка на миллиард - как раз пример того, что расширение домена не всегда удачный выбор.
Потому что групповая структура не у самих адресов, а у оффсетов/индексов, а адреса — это множество, на котором действует эта группа. Group action, все дела. И, кстати, для того, чтобы это действие было определённым, и чтобы вы не поехали кукухой в слоях изоморфизмов, в группе индексов должен быть обычный арифметический ноль.
У многих древних народов понятие 0 не было, а вот нул был как естественное представление отсутствия, и точно также в языке таких народов можно часто увидеть отдельно слово для 1 и отдельное понятие больше единицы - много. Нисколько, один, много - это естественное представление мозга о натуральных числах
Тут проблема не в том, что код сложный, а в том, что код явно завязан на внешний мир. И тут есть варианты — либо делать модель файловой системы и доказывать все свойства на ней (и проверять её соответствие реальной ФС через какой-нибудь квикчек), либо формализовывать всю ОС и экстрагировать из этого формализма реализацию (доверяя компилятору, но вы ему и так всегда доверяете), например.
…и оно не имеет смысла (то есть, никогда не выполняется для любого производного типа), если в языке есть операторы вроде typeid, dynamic_cast и тому подобных, позволяющие сформулировать предикат вроде φ x = typeid x ≡ typeid T.
Как известно, любая система, обладающая полнотой по Тьюрингу не имеет логических преимуществ перед другой, так как может вычислить любой алгоритм.
«Логические преимущества» у вас не определены достаточно однозначно.
О разных системах можно рассуждать с разной. Например, C++, и язык ассемблера тьюринг-полны, но где процесс сборки кода в бинарник выявляет больше ошибок до запуска?
В математике не существует конвенции -- включать или не включать ноль в натуральные числа. Поэтому многими предлагается вообще не использовать их, а говорить: позитивные целые числа.
Дело не в конвенции, а в том, какие умолчания более часто распространены. И, опять же, личный опыт — умолчание «ноль включается» распространено больше, особенно в англоязычной литературе. В data N = Z | S Nу вас Z интерпретируется как ноль, в начальной алгебре [zero, suc] : 1 + N → N zero интерпретируется тоже как ноль, в произвольных топосах «треугольная часть» natural numbers object интерпретируется как ноль, и так далее.
Но логичнее всего было бы не включать, ибо натуральные числа используются для счёта объектов.
Они используются далеко не только для этого. Но, впрочем, чем «ноль объектов» плох?
Но с «человеческой» точки зрения нумерация с единицы действительно удобнее, что нашло своё отражение, например, в классической математике.
А где в классической математике это нашло отражение?
Натуральные числа в большинстве математических школ начинаются с нуля (а там, где не начинаются — так только ради того, чтобы опустить слово «не равный нулю знаменатель» при определении рациональных чисел). Я, если честно, не вспомню книгу, в которой ноль не подразумевался бы входящим во множество натуральных чисел.
Конкретно для самих массивов длины n объектов типа T, упрощая, денотация — это функция I → T, где I — индексное множество (например, фактор-группа ℤ/nℤ, или тип Fin n, смотря какой формализм вам приятнее). И чем больше структуры на индексном множестве, тем с ним приятнее работать. И, в частности, включение нейтрального элемента в это множество делает его группой, удобным типом, и так далее.
Только подавляющее большинство (виденного мной, по крайней мере) ООП-кода оверинжинирнуто, и при всём этом его тяжело поддерживать (потому что оно оверинжинирнуто «не туда», и с направлением развития или эволюции требований не угадали, а рефакторить его больно). Возможно, именно поэтому ООП вас
кормило верой и правдой более 15 лет
точно так же, как меня C++ кормил верой и правдой много лет, и может кормить ещё, если я начну снова ненавидеть себя достаточно сильно, чтобы в него окунуться. Отвратительный, переусложнённый язык (хотя база тоже тупая как полено), на котором практически невозможно писать надёжный код и который совсем невозможно знать, за счёт чего и кормит. Жоп секурити, все дела.
А вот на реальный мир он натягивается с оговорками, как и прочие модели.
Это не модель, это метод рассуждения. И натягивается он вполне успешно, без каких-либо оговорок.
Единую физику-то полезную и непротиворечивую не изобрели, а вы на куда более неопределённую этику замахиваетесь.
«Физики пока не осилили совместить ОТО и квантмех (что, впрочем, не ведёт к наблюдаемым неконсистентностям), но поэтому я не то что не буду пытаться вывести непротиворечивую систему воззрений в основе своего поведения, но я активно буду отражать попытки это сделать или хотя бы даже намёки на то, что это достойная цель.»
Довольно странный аргумент.
Я, конечно, понимаю, что когда в руках учебник по матлогике, всё вокруг кажется формальными моделями, которые можно поверить алгеброй.
И я снова так могу!
Когда в руках учебник по обществознанию, всё вокруг кажется вопросами, которые можно решить демократией. Когда в руках учебник по психологии, всё вокруг кажется акцентуациями поведенческих категорий, которые можно объяснить этими категориями.
В частности, воздыхание по абстракциям характерно для шизоидного спектра.
Не очень понял, причём тут это, но мы, конечно, можем начать обсуждать разные спектры, расстройства-нерасстройства, и так далее. Вам, правда, результат скорее всего не понравится.
Но всё-таки полезно осознавать, что другие люди вовсе не обязаны разделять ваши ценности
Это не ценности, это снова способ рассуждения о них, не более: не надо смешивать язык и метаязык. И, собственно, непротиворечивая логика — это единственный способ рассуждать об этих ценностях и обмениваться ими. Если вы выкидываете этот способ, то у вас остаются только эмоции: кто громче и пламеннее говорит, тот и победил. Хотите ли вы жить в таком мире?
и вашу конфигурацию нейросеточки, и убеждать их в правильности вашей картины мира, оперируя исключительно ограниченными ей понятиями, малоперспективно.
Я разве против? Я, например, кроме того осознаю, что некоторые люди воруют (а я нет) и им норм, или насилуют (а я нет) и им норм. Но что мы делаем с такими людьми? Мы не допускаем их до управления финансами и не разрешаем им работать воспитателями в детских садах.
Вот так и тут: если люди воинственно не хотят думать и рассуждать, то допускать их, например, до процесса принятия затрагивающих кого-то ещё решений тоже нельзя.
Конечно, в интернетах всегда остаётся вариант самоутвердиться
Но, конечно, куда лучше вариант — регулярно намекать на личность собеседника (что он шизоид, или что ему лишь бы самоутвердиться) вместо того, чтобы говорить по существу.
Ну и притаскивать какие-то статейки, конечно. Когда в руках буковки, поддерживающие приятное вам высказывание, всё в них кажется истинным.
Ну естественно — сила статистики стала важна только тогда, когда выводы для вас получаются неудобные. Покуда выводы удобные, то можно не заморачиваться не то что статистической силой, но и самим наличием статистики, а просто говорить как факт «цифры будут не в вашу сторону». Почему? Потому, что вы в это верите.
Тогда это уж точно не обязанно быть истинным. Я-то брал самую оптимистичную интерпретацию, где «плохо» дефиниционально равно «не хорошо» (или это пессимистичная интерпретация? хз)
Если вы программист, то нельзя говорить, что a ∨ ¬a заведомо верно, поэтому глубокое понимание логического оператора «ИЛИ» как раз к такому ответу не приводит (или, можно сказать, скорее даже от него уводит).
Хуже: всего лишь компилируемость этих выражений. Для соответствия типов надо использовать синтаксис с { ... } ->.
В оригинальном пропозале на концепты из нулевых было понятие аксиом (откуда и закомментированная часть), но даже их компилятор не проверял. Это были именно аксиомы, а не теоремы.
Представители самой мирной религии цивилизованно вступили в диалог о том, что они от этого расстроились, и цивилизованно попросили так больше не делать, используя доступные им демократические инструменты политически свободной Швеции.
Ну тут уже на несколько пунктов набралось, например конкретно по данной теме:
Притаскивание статистики по SF вместо того упомянутого мной пригорода с выдачей этого как опровержения моих слов.
Указание, что я про Даллас писал «потом».
Указание, что «культурно» SF называют Frisco.
Или, по соседней:
4. Что моя позиция по оружию сформирована на голливудских фильмах.
Тем более агрессивное?
Да, сорян (вот видите, это совсем несложно!) — мне стоило написать «агрессивно сформулированное враньё». «Агрессивное враньё» действительно непонятно, что такое.
Слюной брызжете здесь как раз вы
Откалибруйте эмоциометр: у меня довольно базовая эмоция презрения, и я всего лишь не стесняюсь её открыто выражать.
Ок, не заметил видимо. Ваши посты слишком многословны
Ещё один, не осиливший ничего толще букваря. Гермиона Хабр сильно изменился за лето.
большинство из них здесь по этой причине я не читал в принципе
Но отвечать вам это не мешает! Равно как и утверждать, что и где я писал или не писал.
Ну слушайте, после того как вы сравнили статистику одного малого города со статистикой по другой стране в целом
Население Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) — где-то 200 тысяч человек. Это был бы четвёртый по размеру город в Швеции.
Это характерная статистика для такого рода городов (на что я тоже указывал).
Более того, граница между Далласом и Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) — довольно воображаемая: попробуйте открыть google maps и найти там Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе). При этом в Далласе с преступностью всё очень плохо, а в Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) — хорошо, притом, что в Далласе ментов на душу населения в разы больше. Почему? Потому, что там правоприменительная практика, да и само сильно более левое/синее/либеральное/демократическое население в целом, сильно больше боятся оружия.
Сторонниками госраспределения, социального государства, и так далее, постулируется, что это всё сглаживает социальные конфликты и что-то там ещё, поэтому флуктуации в странах околоскандинавского околосоциализма сильно меньше.
Учитывая вышесказанное, сравнение вполне обосновано.
Примерно с таким же успехом можно сравнить статистику по вашему Фриско с какой-н Кируной за полярным кругом в Швеции, только оно не в вашу пользу окажется
Было бы интересно найти реальную статистику (скажем, kiruna murder rate), но по Kiruna, Sweden её не нашёл за 10 минут ни я, ни chatgpt, ни deepseek.
Ладно, придётся использовать Numbeo:
Притом, что в Kiruna на порядок меньше население, а рядом со Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) криминогенный Даллас, во Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) существенно безопаснее. Люди в последнем чуть больше переживают за машины (вероятно, потому, что без машины в США жить тяжело), а всё остальное — заметно безопаснее.
Отдельно прокекал с worries being insulted в 2.5 раза ниже. Вооружённое общество — вежливое общество.
не в вашу пользу
Lol. Lmao even.
Обожаю, когда люди выдают какие-то свои предубеждения без попыток их минимально проверить, а потом садятся с ними в лужу.
Зачем с ним так? Он же не занимается враньём через умалчивание, не спорит с соломенными чучелами, не притаскивает левые анонимные источники и не обижается, когда ему говорят, что источники врут, и вообще отличный человек (а я весь в него!).
Потому что депортации нелегалов и членов банд, и прекращение государственных распилов — не беспредел.
Если учитывать англоязычные, то в большинстве учебников (а также научных статей, и так далее) ноль таки включается.
В начальной школе и отрицательных чисел нет, и корень из минус единицы брать нельзя.
Так я запутался, единицу в итоге тоже вычёркиваем из натуральных чисел?
А на самом деле всё проще:
Тип функции для чтения
гарантирует отсутствие чтений из пустого контейнера (и многое другое) без каких-либо крайних случаев.
Оба — это какие?
Монадический API он уже поддерживает, и для одноэлементного массива он ведёт себя как надо. Можно вообще взять индексированные монады и получить
или, если хочется максимальной точности,
после чего предыдущий вариант сводится к этому при out-count ↦ const m. С таким
>>=изоморфизмMaybe a ≅ Vec 1 aстроится (и доказывается) тривиально.Потому что групповая структура не у самих адресов, а у оффсетов/индексов, а адреса — это множество, на котором действует эта группа. Group action, все дела. И, кстати, для того, чтобы это действие было определённым, и чтобы вы не поехали кукухой в слоях изоморфизмов, в группе индексов должен быть обычный арифметический ноль.
А как у древних народов дела с понятием массивов?
Тут проблема не в том, что код сложный, а в том, что код явно завязан на внешний мир. И тут есть варианты — либо делать модель файловой системы и доказывать все свойства на ней (и проверять её соответствие реальной ФС через какой-нибудь квикчек), либо формализовывать всю ОС и экстрагировать из этого формализма реализацию (доверяя компилятору, но вы ему и так всегда доверяете), например.
…и оно не имеет смысла (то есть, никогда не выполняется для любого производного типа), если в языке есть операторы вроде
typeid,dynamic_castи тому подобных, позволяющие сформулировать предикат вродеφ x = typeid x ≡ typeid T.«Логические преимущества» у вас не определены достаточно однозначно.
О разных системах можно рассуждать с разной. Например, C++, и язык ассемблера тьюринг-полны, но где процесс сборки кода в бинарник выявляет больше ошибок до запуска?
Дело не в конвенции, а в том, какие умолчания более часто распространены. И, опять же, личный опыт — умолчание «ноль включается» распространено больше, особенно в англоязычной литературе. В
data N = Z | S Nу васZинтерпретируется как ноль, в начальной алгебре[zero, suc] : 1 + N → Nzero интерпретируется тоже как ноль, в произвольных топосах «треугольная часть» natural numbers object интерпретируется как ноль, и так далее.Они используются далеко не только для этого. Но, впрочем, чем «ноль объектов» плох?
А где в классической математике это нашло отражение?
Натуральные числа в большинстве математических школ начинаются с нуля (а там, где не начинаются — так только ради того, чтобы опустить слово «не равный нулю знаменатель» при определении рациональных чисел). Я, если честно, не вспомню книгу, в которой ноль не подразумевался бы входящим во множество натуральных чисел.
Конкретно для самих массивов длины
nобъектов типа T, упрощая, денотация — это функция I → T, где I — индексное множество (например, фактор-группа ℤ/nℤ, или типFin n, смотря какой формализм вам приятнее). И чем больше структуры на индексном множестве, тем с ним приятнее работать. И, в частности, включение нейтрального элемента в это множество делает его группой, удобным типом, и так далее.Только подавляющее большинство (виденного мной, по крайней мере) ООП-кода оверинжинирнуто, и при всём этом его тяжело поддерживать (потому что оно оверинжинирнуто «не туда», и с направлением развития или эволюции требований не угадали, а рефакторить его больно). Возможно, именно поэтому ООП вас
точно так же, как меня C++ кормил верой и правдой много лет, и может кормить ещё, если я начну снова ненавидеть себя достаточно сильно, чтобы в него окунуться. Отвратительный, переусложнённый язык (хотя база тоже тупая как полено), на котором практически невозможно писать надёжный код и который совсем невозможно знать, за счёт чего и кормит. Жоп секурити, все дела.
Это не модель, это метод рассуждения. И натягивается он вполне успешно, без каких-либо оговорок.
«Физики пока не осилили совместить ОТО и квантмех (что, впрочем, не ведёт к наблюдаемым неконсистентностям), но поэтому я не то что не буду пытаться вывести непротиворечивую систему воззрений в основе своего поведения, но я активно буду отражать попытки это сделать или хотя бы даже намёки на то, что это достойная цель.»
Довольно странный аргумент.
И я снова так могу!
Когда в руках учебник по обществознанию, всё вокруг кажется вопросами, которые можно решить демократией.
Когда в руках учебник по психологии, всё вокруг кажется акцентуациями поведенческих категорий, которые можно объяснить этими категориями.
Не очень понял, причём тут это, но мы, конечно, можем начать обсуждать разные спектры, расстройства-нерасстройства, и так далее. Вам, правда, результат скорее всего не понравится.
Это не ценности, это снова способ рассуждения о них, не более: не надо смешивать язык и метаязык. И, собственно, непротиворечивая логика — это единственный способ рассуждать об этих ценностях и обмениваться ими. Если вы выкидываете этот способ, то у вас остаются только эмоции: кто громче и пламеннее говорит, тот и победил. Хотите ли вы жить в таком мире?
Я разве против? Я, например, кроме того осознаю, что некоторые люди воруют (а я нет) и им норм, или насилуют (а я нет) и им норм. Но что мы делаем с такими людьми? Мы не допускаем их до управления финансами и не разрешаем им работать воспитателями в детских садах.
Вот так и тут: если люди воинственно не хотят думать и рассуждать, то допускать их, например, до процесса принятия затрагивающих кого-то ещё решений тоже нельзя.
Но, конечно, куда лучше вариант — регулярно намекать на личность собеседника (что он шизоид, или что ему лишь бы самоутвердиться) вместо того, чтобы говорить по существу.
Ну и притаскивать какие-то статейки, конечно. Когда в руках буковки, поддерживающие приятное вам высказывание, всё в них кажется истинным.
Я не плохо играю в шахматы, я просто не согласен с правилами.
Вы так говорите, будто все люди одинаково хороши во всём и одинаково способны ко всему.
Ну естественно — сила статистики стала важна только тогда, когда выводы для вас получаются неудобные. Покуда выводы удобные, то можно не заморачиваться не то что статистической силой, но и самим наличием статистики, а просто говорить как факт «цифры будут не в вашу сторону». Почему? Потому, что вы в это верите.
Предельно ожидаемо, предельно скучно.
Тогда это уж точно не обязанно быть истинным. Я-то брал самую оптимистичную интерпретацию, где «плохо» дефиниционально равно «не хорошо» (или это пессимистичная интерпретация? хз)
Если вы программист, то нельзя говорить, что a ∨ ¬a заведомо верно, поэтому глубокое понимание логического оператора «ИЛИ» как раз к такому ответу не приводит (или, можно сказать, скорее даже от него уводит).
За конечное время нельзя автоматически доказать. Проверить доказательство — можно.
Но для этого, да, нужны зависимые типы.
Хуже: всего лишь компилируемость этих выражений. Для соответствия типов надо использовать синтаксис с
{ ... } ->.В оригинальном пропозале на концепты из нулевых было понятие аксиом (откуда и закомментированная часть), но даже их компилятор не проверял. Это были именно аксиомы, а не теоремы.
Это «семантика» языка типов (который при компиляции стирается и после запуска не очень интересен), а не языка термов.
Представители самой мирной религии цивилизованно вступили в диалог о том, что они от этого расстроились, и цивилизованно попросили так больше не делать, используя доступные им демократические инструменты политически свободной Швеции.
Скрытый текст
На самом деле нет, конечно же:
https://www.lemonde.fr/en/international/article/2023/09/04/violent-riot-breaks-out-in-sweden-at-koran-burning-protest_6122393_4.html
https://news.sky.com/story/violent-riot-lasts-through-the-night-in-sweden-after-koran-burning-12954816
https://news.sky.com/story/iraqi-man-who-sparked-riots-with-koran-burnings-shot-dead-in-sweden-13299458
Ну тут уже на несколько пунктов набралось, например конкретно по данной теме:
Притаскивание статистики по SF вместо того упомянутого мной пригорода с выдачей этого как опровержения моих слов.
Указание, что я про Даллас писал «потом».
Указание, что «культурно» SF называют Frisco.
Или, по соседней:
4. Что моя позиция по оружию сформирована на голливудских фильмах.
Да, сорян (вот видите, это совсем несложно!) — мне стоило написать «агрессивно сформулированное враньё». «Агрессивное враньё» действительно непонятно, что такое.
Откалибруйте эмоциометр: у меня довольно базовая эмоция презрения, и я всего лишь не стесняюсь её открыто выражать.
Ещё один, не осиливший ничего толще букваря.
ГермионаХабр сильно изменился за лето.Но отвечать вам это не мешает! Равно как и утверждать, что и где я писал или не писал.
Население Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) — где-то 200 тысяч человек. Это был бы четвёртый по размеру город в Швеции.
Это характерная статистика для такого рода городов (на что я тоже указывал).
Более того, граница между Далласом и Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) — довольно воображаемая: попробуйте открыть google maps и найти там Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе). При этом в Далласе с преступностью всё очень плохо, а в Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) — хорошо, притом, что в Далласе ментов на душу населения в разы больше. Почему? Потому, что там правоприменительная практика, да и само сильно более левое/синее/либеральное/демократическое население в целом, сильно больше боятся оружия.
Сторонниками госраспределения, социального государства, и так далее, постулируется, что это всё сглаживает социальные конфликты и что-то там ещё, поэтому флуктуации в странах околоскандинавского околосоциализма сильно меньше.
Учитывая вышесказанное, сравнение вполне обосновано.
Было бы интересно найти реальную статистику (скажем, kiruna murder rate), но по Kiruna, Sweden её не нашёл за 10 минут ни я, ни chatgpt, ни deepseek.
Ладно, придётся использовать Numbeo:
Притом, что в Kiruna на порядок меньше население, а рядом со Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) криминогенный Даллас, во Frisco (НЕ Сан-Франциско, который в Калифорнии, США, а Frisco, который НЕ Сан-Франциско и в Техасе) существенно безопаснее. Люди в последнем чуть больше переживают за машины (вероятно, потому, что без машины в США жить тяжело), а всё остальное — заметно безопаснее.
Отдельно прокекал с worries being insulted в 2.5 раза ниже. Вооружённое общество — вежливое общество.
Lol. Lmao even.
Обожаю, когда люди выдают какие-то свои предубеждения без попыток их минимально проверить, а потом садятся с ними в лужу.
Зачем с ним так? Он же не занимается враньём через умалчивание, не спорит с соломенными чучелами, не притаскивает левые анонимные источники и не обижается, когда ему говорят, что источники врут, и вообще отличный человек (а я весь в него!).
Вторая. Пукпук и всё.