А мне не понятно, почему вы оба говорите именно про алгорифмы, а не про λ-исчисление или комбинаторную логику. По моему мнению, после λ и CL работать с алгорифмами — боль и страдание. Может, поэтому все известные мне современные (кто-то ещё использует Рефал?) системы, которые пробовали в том или ином виде реализовывать определяемые пользователем алгорифмы, обмазываются императивщиной и побочными эффектами: Wolfram, TeX, sed.
Поскольку вопрос был лично мне, то отвечу, причём честно.
Ещё 10 лет назад, когда мои представления о сетевых технологиях ограничивались знанием о существовании аббревиатуры ISO/OSI и «я тебя по IP вычислю», я считал, что - маршрутизаторы — это такие устройства, которые используют серьёзные фирмы для организации локальных сетей, а также провайдеры для поддержки Интернета, чтобы я мог за установленную плату смотреть там котиков, - а роутер — это то, что мне знакомый поставил дома, чтобы я могу не таскать провода по всей квартире.
Так что ответ таков: 10 лет назад я бы однозначно сказал, что используют только роутер. Зачем мне в быту такая дорогостоящая и сложная вещь, как маршрутизатор?
Сейчас — одинаково, синонимы.
Теперь о другом: безусловно, язык меняется, слова входят и выходят в употребление, меняют свой смысл. И конечно, наивно считать, что современная речь замкнута и более никакие новые слова в язык не войдут, и что нужно бороться с новыми заимствованиями. Но таким же образом неверно считать, что все языки одинаковы, что различаются они несущественными деталями. У каждого языка, а точнее, у каждой культуры, в рамках которой язык развивается, имеется определённый дух, стиль. Это отражается в том, как происходит работа со словом, как обычно выстраивается и ведётся мысль. Например, если у некоторого слова есть три смысла и я использую это слово в первом смысле, почему я и собеседник увидят ассоциацию со вторым смыслом, а с третьим — нет? Если я хочу донести некоторую мысль, какое слово мне выбрать, чтобы у читателя возникли нужные мне ассоциации, и не возникли лишние? Какие заимствования нам стоит брать, чтобы обогатить речь, а каких стоит избегать, потому что они делают речь более убогой?
Кстати, в ЯП всё то же самое.
В общем, я считаю, что тема сложная, надо чётко обозначить 1) как работает язык, 2) какую задачу мы хотим решить, 3) какими методами мы хотим достичь цели. Без этого обсуждение бесполезно.
P.S. отдельно замечу, что мне печально от того, что слово «планшет» поменял свой смысл и сейчас необходимо уточнять, о чём именно я говорю. Но это вопрос моего личного вкуса.
Какие маршруты? По Золотому кольцу России или по Алтайским горам?
Вообще-то, именно в этом смысле и используется слово. Была как-то статья (не нашел ссылку) на хабре, что власти РФ озаботились тем, что пакеты из одного русского города бегают в другой русский град через то ли Голландию, то ли другую европейскую страну.
А если бы предмет, строящий маршруты, назвали "маршрутер", вы бы тоже задали этот вопрос?
Для русского уха такое словообразование было бы странным и, вероятно, вопросы бы задавались. Вероятно, предложили бы использовать «маршрутчик» или «маршрутник». Я думаю, что «маршрутизатор» появился после того, как устоялся термин «маршрутизация», потому его и используем.
"маршрутизитор" считается государственным языком
одно из них типа наше родное
Дело не в государственности, а в том, подходит ли для носителей обсуждаемого языка и культуры или нет. Сравните с поговоркой: «программист на Фортране на любом ЯП пишет код на Фортране». В случае с живой речью человеку нужны правильные ассоциации и естественный способ изложения мысли. В противном случае возникает чувство, что присутствует инородный элемент. Можно также сравнить с проблемой архитектурной целостностью города: никто же не говорит, что строить надо только в партийно одобренном стиле (японский контрпример с последствиями), эклектика тоже хорошо, но когда в меру, разумно.
Это модель Пуанкаре в круге. Геометрия определённо неевклидовая, о чём можно судить хотя бы по «догонялкам», когда два субъекта (игрок+монстр, монстр+монстр) бегут параллельно и от этого расходятся.
Тем не менее, в этой игре, как и в Hyperbolica, мне представляется нечестным показывать игроку мир в виде круга (впрочем, это хороший выбор для слоя модели), а не экспоненциальную карту. В частности, в Hyperbolica меня раздражал батут: ну не может «житель» эвклидового мира видеть горизонт бытия.
Да, есть системы типов с модальностями (напр., R. Davies et al. A Modal Analysis of Staged Computation), есть кучная куча систем с линейными типами и т.п.
Одна из важных особенностей теории типов в традиционном её понимании в том, что она соответствует proof-relevant логикам, т.е. в теории типов терм/доказательство M:A принципиально может обладать свойствами, отличными от другого терма/доказательства N:A того же типа/высказывания A. Соответственно, все логики, в которых «плевать на само доказательство, лишь бы оно было», плохо интерпретируются в терминах программ и типов.
Другая особенность — это вычислительная семантика термов/доказательств. В HoTT, например, на каждый тип приходятся правила вывода, среди которых помимо стандартных для логики правил (англ. терминология) Formation, Introduction, Exclusion есть ещё Evaluation (соответствует β-редукции) и Uniqueness (соответствует η-редукции). Если в логике нет аналога β-редукции, сложно доказательства интерпретировать как программы.
Offtop к сообщению @Underskyer1. Теория категория зародилась как обобщения безудержно плодящихся топологических теорий и, как было почти сразу обнаружено тогда же в середине XX века, алгебраических систем ввиду сходства типичных конструкций и построений, а также применимости алгебраических методов в геометрии и наоборот. Теория типов жила и развивалась весь XX век независимо и только в самом конце начали пытаться натянуть её на инструменты теории категорий.
Ух ты, поражен до глубины. Я пропустил первые абзацы и бегло прочитал остальное. Подумал, что «функция пола» так называется из-за специфики предметной области — тогдашних гендерных исследований. Мол, мальчик-девочка-мальчик-девочка-… — вот вам n%2 = n - 2 * floor(n/2) для определения пола (правда, почему-то написано только floor(n/2), но да бог с ним, подумал я). Всё оказалось гораздо прозаичнее.
Спасибо. Ваш ответ оказался короче, чем ожидал, потому что мне видится здесь благодатное поле для сравнения и обнаружения уникальных свойств Вашей теории.
1.1) если я правильно понял, под сжатыми структурами Вы понимаете символы * (весь домен) и 0 (пустое множество), в то время как в реляционной алгебре необходимо прописывать отношение перечислением элементов. Верно?
1.2) алгебраическая система состоит из набора объектов, алгебраических операций и законов, которым они удовлетворяют. Алгоритмы не являются частью алгебраических систем, это часть реализации системы поддержки / СУБД.
2) доказана связь между реляционной алгеброй и реляционным исчислением, которое обладает теми же свойствами, которые Вы описали в упомянутом разделе. Я тут увидел в вики, что реляционное исчисление близкородственно (или эквивалентно?) исчислению кортежей. Ваша логика, соответствующая АК, и реляционное исчисление — это одно и то же или разные логические системы?
Пробежался по тексту и по крайним главам Вашей книги, и не нашел упоминания реляционной алгебры и Кодда. Кажется, что это прямо первый кандидат на сравнение с Вашей теорией.
Борьба с мракобесием основывается на использовании рационального мышления и, в частности, логики, на культуре именования, на культуре ведения мысли, на использовании фактов. Печально, что текст, направленный против мракобесия вообще и ИТ в частности, в первой половине неаккуратно работает как с понятиями, так и с фактами.
Вместо слова «религия» лучше использовать слово «секта», которое в контексте статьи подходит в широком и в узком смысле, в историческом и в современном.
Как отмечали выше другие, наклеивание ярлыка «религиозный фанатик» на всех несогласных — тоже форма сектантства.
По-моему, аргументы, логика, факт-чекинг и обоснованная методология — вакцина против дури, применения инструментов не по назначению и не в соответствии с поставленной целью.
В случае систем вроде Coq работает принцип де Брёйна: система верификации может быть сколь угодно сложной и позволять компактно записывать сложные доказательства теорем и брать на себя заботу о доказательстве «скучного формализма», но она должна для порождать для каждого «компактного» доказательства некий «протокол» — «длинное» доказательство на простом языке (как правило, подмножество исходного), реализацию которого можно под пивко написать за вечер.
Это как с подписью транзакций в блокчейне: задача решается долго, а решение проверяется быстро.
При наличии этого принципа не важно, одна там реализация Coq или их несколько, ведь всегда можно проверить, что порождаемый ею результат корректен.
Даже если не брать во внимание время на составление таблицы результатов, предложенное решение всё же сомнительное, потому что время на случайный доступ зависит от максимального размера накопителя: чем он больше, тем больше времени требуется на извлечение данных. Так что Вам осталось доказать, что физически возможно сконструировать носитель, чтение с которого будет быстрее разового вычисления cado-nfs.
P.S. Я тут быстро пробежался по документации cado-nfs и не увидел принципиальных ограничений на размер входного числа. Упоминается «маленький» режим (< 2^32) и есть режим больших чисел. Без ограничений таблицу результатов нельзя составить в принципе. Так что не зачёт.
Оно использует несколько множителей и пытается оценить количество внеземных разумных цивилизаций, существующих в нашей Галактике в любой момент [точнее, числа внеземных цивилизаций в Галактике, с которыми у человечества есть шанс вступить в контакт / прим. перев.].
Иначе удивительно читать, что Лионель Дрико из Бельгии знает и находит нужным упомянуть, что организация Meta запрещена в России.
Если клиентское приложение имеет большое количество своих реализаций несвязанных между собой общим кодом (пишутся на разных технологиях), то вероятность существования ошибок будет увеличиваться.
Почему так? Если есть только одна реализация, и в ней присутствует уязвимость, то она наследуется всеми клиентами.
Если в описании безопасности приложения часто уделяется внимание названиям общеизвестных криптографических алгоритмов и протоколов, то реальная безопасность приложения скорее скрывается, чем описывается.
Как это сочетается с тем, что писалось ранее:
Криптография — наука консервативная, когда существует что-то старое и рабочее, проверенное временем и большим количеством криптографов, то оно будет выбрано в приоритете.
Я контекст обсуждения понял таким образом: вместо нативных компилируемых приложений пишут веб-приложения или на JS, или на чём-то компилируемом в JS.
Wasm не курил, но это вроде как обычный байткод. Если я правильно представляю, концептуально wasm ничем не отличается от других виртуальных машин. Беглый гуглёж сообщил, что есть LLVM IR → wasm. Мне представляется, что сам по себе wasm не даёт ничего принципиально нового в сравнении с другими VM. @Nipherisвроде такого же мнения. Но за слова не отвечаю.
Язык ассемблера или байткод какой-нибудь виртуальной машины выполняется непосредственно на машине. В случае с JS вычислительная среда (движок браузера) пытается угадать/восстановить типизацию переменных и контекста для более эффективной компиляции в байткод перед исполнением (как пример, выявление скрытых классов).
В итоге получается, что программист пишет, скажем, на TypeScript, PureScript или Idris свой код (типы проставлены и согласованы), который компилируется в JavaScript (типы стираются), после чего движок пытается угадать, какие типы использовались. Логично же?
У пользователя уже есть ОС и это её (или входящих в дистрибутив системных приложений) задача обеспечивать пользователя новой песочницей по требованию и нужными мерами изоляции — cgroup там всякие и иже с ним. Осталось обеспечить пользователя удобными инструментами, которые позволят «выполнять приложения без ритуала скачивания, установки и без риска». ИМХО, в связи с этим Docker обрёл популярность.
Мне тоже кажется странным использовать JS в качестве низкоуровневого языка виртуальной машины, на котором запускаются пользовательские приложения, к которым предъявляются требования надёжности (пишутся тесты), стандартизации (код транспилируется под конкретный стандарт), изоляции (Worker, WASM) и т.п. JS разрабатывался совсем для других нужд (низкие требования к коду, некая совместимость с нестандартными реализациями, отложенное падение программ, выживание любой ценой) и сейчас это выглядит как натягивание совы на глобус.
Во времена детства, когда трава была зеленее, а руки ещё не из того места росли, одного полного здоровья было категорически мало для комфортного времяпрепровождения со сватами и прочими серьёзными дядями в форме.
А мне не понятно, почему вы оба говорите именно про алгорифмы, а не про λ-исчисление или комбинаторную логику. По моему мнению, после λ и CL работать с алгорифмами — боль и страдание. Может, поэтому все известные мне современные (кто-то ещё использует Рефал?) системы, которые пробовали в том или ином виде реализовывать определяемые пользователем алгорифмы, обмазываются императивщиной и побочными эффектами: Wolfram, TeX, sed.
Поскольку вопрос был лично мне, то отвечу, причём честно.
Ещё 10 лет назад, когда мои представления о сетевых технологиях ограничивались знанием о существовании аббревиатуры ISO/OSI и «я тебя по IP вычислю», я считал, что
- маршрутизаторы — это такие устройства, которые используют серьёзные фирмы для организации локальных сетей, а также провайдеры для поддержки Интернета, чтобы я мог за установленную плату смотреть там котиков,
- а роутер — это то, что мне знакомый поставил дома, чтобы я могу не таскать провода по всей квартире.
Так что ответ таков: 10 лет назад я бы однозначно сказал, что используют только роутер. Зачем мне в быту такая дорогостоящая и сложная вещь, как маршрутизатор?
Сейчас — одинаково, синонимы.
Теперь о другом: безусловно, язык меняется, слова входят и выходят в употребление, меняют свой смысл. И конечно, наивно считать, что современная речь замкнута и более никакие новые слова в язык не войдут, и что нужно бороться с новыми заимствованиями. Но таким же образом неверно считать, что все языки одинаковы, что различаются они несущественными деталями. У каждого языка, а точнее, у каждой культуры, в рамках которой язык развивается, имеется определённый дух, стиль. Это отражается в том, как происходит работа со словом, как обычно выстраивается и ведётся мысль. Например, если у некоторого слова есть три смысла и я использую это слово в первом смысле, почему я и собеседник увидят ассоциацию со вторым смыслом, а с третьим — нет? Если я хочу донести некоторую мысль, какое слово мне выбрать, чтобы у читателя возникли нужные мне ассоциации, и не возникли лишние? Какие заимствования нам стоит брать, чтобы обогатить речь, а каких стоит избегать, потому что они делают речь более убогой?
Кстати, в ЯП всё то же самое.
В общем, я считаю, что тема сложная, надо чётко обозначить 1) как работает язык, 2) какую задачу мы хотим решить, 3) какими методами мы хотим достичь цели. Без этого обсуждение бесполезно.
P.S. отдельно замечу, что мне печально от того, что слово «планшет» поменял свой смысл и сейчас необходимо уточнять, о чём именно я говорю. Но это вопрос моего личного вкуса.
Вообще-то, именно в этом смысле и используется слово. Была как-то статья (не нашел ссылку) на хабре, что власти РФ озаботились тем, что пакеты из одного русского города бегают в другой русский град через то ли Голландию, то ли другую европейскую страну.
Для русского уха такое словообразование было бы странным и, вероятно, вопросы бы задавались. Вероятно, предложили бы использовать «маршрутчик» или «маршрутник». Я думаю, что «маршрутизатор» появился после того, как устоялся термин «маршрутизация», потому его и используем.
Дело не в государственности, а в том, подходит ли для носителей обсуждаемого языка и культуры или нет. Сравните с поговоркой: «программист на Фортране на любом ЯП пишет код на Фортране». В случае с живой речью человеку нужны правильные ассоциации и естественный способ изложения мысли. В противном случае возникает чувство, что присутствует инородный элемент. Можно также сравнить с проблемой архитектурной целостностью города: никто же не говорит, что строить надо только в партийно одобренном стиле (японский контрпример с последствиями), эклектика тоже хорошо, но когда в меру, разумно.
Это модель Пуанкаре в круге. Геометрия определённо неевклидовая, о чём можно судить хотя бы по «догонялкам», когда два субъекта (игрок+монстр, монстр+монстр) бегут параллельно и от этого расходятся.
Тем не менее, в этой игре, как и в Hyperbolica, мне представляется нечестным показывать игроку мир в виде круга (впрочем, это хороший выбор для слоя модели), а не экспоненциальную карту. В частности, в Hyperbolica меня раздражал батут: ну не может «житель» эвклидового мира видеть горизонт бытия.
Легко. Вот первая.
Оригинал:
Здесь:
Там:
Кто из этих переводчиков знает, о чём пишет?
Да, есть системы типов с модальностями (напр., R. Davies et al. A Modal Analysis of Staged Computation), есть кучная куча систем с линейными типами и т.п.
Одна из важных особенностей теории типов в традиционном её понимании в том, что она соответствует proof-relevant логикам, т.е. в теории типов терм/доказательство M:A принципиально может обладать свойствами, отличными от другого терма/доказательства N:A того же типа/высказывания A. Соответственно, все логики, в которых «плевать на само доказательство, лишь бы оно было», плохо интерпретируются в терминах программ и типов.
Другая особенность — это вычислительная семантика термов/доказательств. В HoTT, например, на каждый тип приходятся правила вывода, среди которых помимо стандартных для логики правил (англ. терминология) Formation, Introduction, Exclusion есть ещё Evaluation (соответствует β-редукции) и Uniqueness (соответствует η-редукции). Если в логике нет аналога β-редукции, сложно доказательства интерпретировать как программы.
Offtop к сообщению @Underskyer1. Теория категория зародилась как обобщения безудержно плодящихся топологических теорий и, как было почти сразу обнаружено тогда же в середине XX века, алгебраических систем ввиду сходства типичных конструкций и построений, а также применимости алгебраических методов в геометрии и наоборот. Теория типов жила и развивалась весь XX век независимо и только в самом конце начали пытаться натянуть её на инструменты теории категорий.
Ух ты, поражен до глубины. Я пропустил первые абзацы и бегло прочитал остальное. Подумал, что «функция пола» так называется из-за специфики предметной области — тогдашних гендерных исследований. Мол, мальчик-девочка-мальчик-девочка-… — вот вам n%2 = n - 2 * floor(n/2) для определения пола (правда, почему-то написано только floor(n/2), но да бог с ним, подумал я). Всё оказалось гораздо прозаичнее.
Спасибо. Ваш ответ оказался короче, чем ожидал, потому что мне видится здесь благодатное поле для сравнения и обнаружения уникальных свойств Вашей теории.
1.1) если я правильно понял, под сжатыми структурами Вы понимаете символы * (весь домен) и 0 (пустое множество), в то время как в реляционной алгебре необходимо прописывать отношение перечислением элементов. Верно?
1.2) алгебраическая система состоит из набора объектов, алгебраических операций и законов, которым они удовлетворяют. Алгоритмы не являются частью алгебраических систем, это часть реализации системы поддержки / СУБД.
2) доказана связь между реляционной алгеброй и реляционным исчислением, которое обладает теми же свойствами, которые Вы описали в упомянутом разделе.
Я тут увидел в вики, что реляционное исчисление близкородственно (или эквивалентно?) исчислению кортежей. Ваша логика, соответствующая АК, и реляционное исчисление — это одно и то же или разные логические системы?
Пробежался по тексту и по крайним главам Вашей книги, и не нашел упоминания реляционной алгебры и Кодда. Кажется, что это прямо первый кандидат на сравнение с Вашей теорией.
Чем отличаются Ваша алгебра и реляционная?
Борьба с мракобесием основывается на использовании рационального мышления и, в частности, логики, на культуре именования, на культуре ведения мысли, на использовании фактов. Печально, что текст, направленный против мракобесия вообще и ИТ в частности, в первой половине неаккуратно работает как с понятиями, так и с фактами.
Вместо слова «религия» лучше использовать слово «секта», которое в контексте статьи подходит в широком и в узком смысле, в историческом и в современном.
Как отмечали выше другие, наклеивание ярлыка «религиозный фанатик» на всех несогласных — тоже форма сектантства.
По-моему, аргументы, логика, факт-чекинг и обоснованная методология — вакцина против дури, применения инструментов не по назначению и не в соответствии с поставленной целью.
В случае систем вроде Coq работает принцип де Брёйна: система верификации может быть сколь угодно сложной и позволять компактно записывать сложные доказательства теорем и брать на себя заботу о доказательстве «скучного формализма», но она должна для порождать для каждого «компактного» доказательства некий «протокол» — «длинное» доказательство на простом языке (как правило, подмножество исходного), реализацию которого можно под пивко написать за вечер.
Это как с подписью транзакций в блокчейне: задача решается долго, а решение проверяется быстро.
При наличии этого принципа не важно, одна там реализация Coq или их несколько, ведь всегда можно проверить, что порождаемый ею результат корректен.
Для Rust такого нет, AFAIK.
Даже если не брать во внимание время на составление таблицы результатов, предложенное решение всё же сомнительное, потому что время на случайный доступ зависит от максимального размера накопителя: чем он больше, тем больше времени требуется на извлечение данных. Так что Вам осталось доказать, что физически возможно сконструировать носитель, чтение с которого будет быстрее разового вычисления cado-nfs.
P.S. Я тут быстро пробежался по документации cado-nfs и не увидел принципиальных ограничений на размер входного числа. Упоминается «маленький» режим (< 2^32) и есть режим больших чисел. Без ограничений таблицу результатов нельзя составить в принципе. Так что не зачёт.
del
В любом случае, в приличном обществе принято помечать отсебятину переводчика.
Например, https://habr.com/ru/articles/471870/
Или https://habr.com/ru/articles/412093/
Иначе удивительно читать, что Лионель Дрико из Бельгии знает и находит нужным упомянуть, что организация Meta запрещена в России.
Почему так? Если есть только одна реализация, и в ней присутствует уязвимость, то она наследуется всеми клиентами.
Как это сочетается с тем, что писалось ранее:
Спасибо, интересная идея.
Хочу на практике попробовать с кривыми Безье и эллипсами. Кстати, они не имеют обсуждаемых выше проблем массового поражения.
Я контекст обсуждения понял таким образом: вместо нативных компилируемых приложений пишут веб-приложения или на JS, или на чём-то компилируемом в JS.
Wasm не курил, но это вроде как обычный байткод. Если я правильно представляю, концептуально wasm ничем не отличается от других виртуальных машин. Беглый гуглёж сообщил, что есть LLVM IR → wasm. Мне представляется, что сам по себе wasm не даёт ничего принципиально нового в сравнении с другими VM. @Nipherisвроде такого же мнения. Но за слова не отвечаю.
Как бы да, но «это другое» (с).
Язык ассемблера или байткод какой-нибудь виртуальной машины выполняется непосредственно на машине. В случае с JS вычислительная среда (движок браузера) пытается угадать/восстановить типизацию переменных и контекста для более эффективной компиляции в байткод перед исполнением (как пример, выявление скрытых классов).
В итоге получается, что программист пишет, скажем, на TypeScript, PureScript или Idris свой код (типы проставлены и согласованы), который компилируется в JavaScript (типы стираются), после чего движок пытается угадать, какие типы использовались. Логично же?
У пользователя уже есть ОС и это её (или входящих в дистрибутив системных приложений) задача обеспечивать пользователя новой песочницей по требованию и нужными мерами изоляции — cgroup там всякие и иже с ним. Осталось обеспечить пользователя удобными инструментами, которые позволят «выполнять приложения без ритуала скачивания, установки и без риска». ИМХО, в связи с этим Docker обрёл популярность.
Мне тоже кажется странным использовать JS в качестве низкоуровневого языка виртуальной машины, на котором запускаются пользовательские приложения, к которым предъявляются требования надёжности (пишутся тесты), стандартизации (код транспилируется под конкретный стандарт), изоляции (Worker, WASM) и т.п. JS разрабатывался совсем для других нужд (низкие требования к коду, некая совместимость с нестандартными реализациями, отложенное падение программ, выживание любой ценой) и сейчас это выглядит как натягивание совы на глобус.
Это бронька. Никак не заменяет аспирин.
Во времена детства, когда трава была зеленее, а руки ещё не из того места росли, одного полного здоровья было категорически мало для комфортного времяпрепровождения со сватами и прочими серьёзными дядями в форме.