На выучение всех этих дебильных правил тратиться 8 лет[...], которое можно было бы потратить с большей пользой.
Недавно мне джун примерно такими же словами ругался, что время тратится на удовлетворение правил линтера. Я же объяснял, что линтер — это всего лишь инструмент, а правила помогают обнаружить места, которые, вероятно, вызовут у читателя кода затруднение. Надо снижать когнитивную нагрузку на читателя, даже если это потребует чуть больше времени от писателя.
В украинском языке нет правила тся/ться, и ничего страшного не случилось.
Потому что в украинском -и в инфинитиве не сократилось до -ь:
«Він має пишатися і він пишається»
Заметим, что здесь форма инфинитива и 3 лица различны.
Выше @nronnieпривёл формальное определение O-нотации, из которого видно, что время работы T(n) может одновременно относиться к нескольким разным функциям f(n), если соблюдаются упомянутые условия. Так, если T(n) = O(n), то всегда можно сказать, что T(n) = O(n^2), хотя и бесполезно. Аналогично, если T(n) = O(n (log n)^2), то T(n) = O(n sqrt(n)).
В сущности, вопрос может быть сведён к тому, насколько точную оценку мы хотим предоставить в O-нотации. Если мы хотим сказать «ну, время растёт быстрее n log n, но всяко медленнее n sqrt(n)», то пишем O(n sqrt(n)). Если хотим сказать «время растут не быстрее n (log n)^2 и это хорошая оценка», то пишем O(n (log n)^2). Собственное имя есть не у каждого класса функция (что очевидно, ведь имён конечное количество, а классов функций несчётно много).
Я мог ошибиться, описал субъективное видение из далёкого прошлого. Когда я покинул НИИ и у меня кончилась действующая лицензия, решил купить у них. Единственная подходящая лицензия стоила за год как 1/4 моей месячной зарплаты. Естественно я не стал её приобретать.
Когда на одном из мест работы встал вопрос, а не использовать ли нам Вольфрам, начальство посмотрело и сказало, что потенциальная выгода от языка и стандартной библиотеки не покрывает стоимость и риски, связанные с длительным сопровождением будущих программных компонент на Вольфраме. Деталей не знаю.
Для ЯП общего назначения он не подходит просто по определению.
В текущем виде — да. Впрочем, я на нём и XML-файлы парсил и анализировал, и с файловой системой работал, и строил иллюстрации к статьям, и числодробилку писал. У языка есть потенциал стать вполне хорошим скриптовым языком.
Ну так я и не утверждал, что на WL невозможно такое написать. Можно, но для этого надо выработать определённую дисциплину: на каждый символ приходится не более одного определения (Set, SetDelayed), все определение должны идти строго перед запуском вычислений и быть строго на верхнем уровне программы, нельзя использовать никакие «опасные» функции (Print, Set, Function, Module) в качестве комбинаторов и т.д. и т.п.
Проблема в том, действительно ли перед нами комбинатор или это выражение мимикрирует под комбинатор, но таковым не является. WM принципиально не позволяет ответить на подобные вопросы; из ниоткуда может в любой момент вычислений вылезти побочный эффект (самый неприятный для отладки — доопределение символов более специфичными правилами, которые не соответствуют семантике основного правила). Ставится крест на принципе Черча-Россера (результат вычисления не зависит от стратегии) и на ссылочной прозрачности (любое выражение может быть заменено на эквивалентное, полученное в результате вычисления).
P.S. моё предыдущее сообщение относилось к обсуждению алгорифмов Маркова, которые я считаю достаточно плохим формализмом по сравнению с другими. Те же λ-исчисление или комбинаторную логику можно использовать вот прямо как есть, это не «Тьюрингова трясина», хотя сложные программы на них не напишешь. Писать алгорифмы Маркова для решения хотя бы простой практической задачи нереально. «Change my mind»
По теме: можете сами поискать «композиция алгорифмов маркова» — это алгоритм переписывания алгорифма так, чтобы к нему можно было дописать другой алгорифм.
Возьмём к примеру CL. В ней выражения (комбинаторы) применяются к другим выражениям, применение всегда одноаргументно. У каждого комбинатора есть комбанаторное свойство, которое определяет, как он будет вычисляться. Например, есть комбинатор I со свойством I[x] = x; или комбинатор K со свойством K[x][y] = x, или S[x][y][z] = x[z][y[z]].
Объекты, свойства, понятия, процессы в предметной области соответствуют своим комбинаторам. Какие-то комбинаторы просто постулируются вместе со своими свойствами, какие-то можно определить через другие (но определение должно сохранять комбинаторное свойство!), какие-то мы оставляем «неопределёнными», то есть рассматриваем их как переменные. Последние в будущем будут заменены на конкретные выражения, когда данные подъедут. Или нет.
Возьмём алгорифм Маркова. Если я работаю с матрицами, какая подстрока или какое правило соответствует понятию «матричное умножение двух неких матриц A*B»? Если я к программе добавлю ещё какие-то правила, будет ли это же (правило или подстрока) соответствовать ровно тому же понятию? Едва ли. Посмотрите, как всю программу приходится переписывать ради того, чтобы дописать другую подпрограмму.
WL (точнее, WM) был популярен среди учёных. В широкие массы он не вышел из-за 1) конской цены, по которой он большую часть времени распространялся, когда народ присматривался к этому инструменту, ну и упомянутая другими проприетарная лицензия, и 2) рекламы и позиционирования: Стив его пиарил как шайтан-машинку, которая и тайны мироздания моделирует, или около-человеческую речь понимает, а ещё крестиком вышивать умеет, в то время как рядовому пользователю нужен обычный ЯП общего назначения с низким порогом входа и с хорошей библиотекой для решения его, пользователя, задач (собственно, поэтому Fortran и Python заимели популярность в своё время). Причём WL является таким ЯП, но чтобы Стив так сказал, нужно гордостью подавиться. Посмотри на переводные статьи про WL на хабре — много ли желания возникает использовать его для решения частных бытовых задач?
Костыли, конечно, есть, но это не квадратные скобки. К слову, WL один из немногих языков, в которых группировочные скобки для разбора выражений с инфиксными операторами и скобки, входящие в состав синтаксического выражения (список аргументов, кортеж и т.п.), различаются графически. К примеру, в JS скобки в x = (a, b) и x = f(a, b) выполняют разную роль.
Также // не проблема, ведь всегда можно использовать префиксную запись.
К костылям я бы отнёс императивность интерпретатора, которая вынуждает внимательно следить за тем, в каком состоянии находится ядро (kernel), в т.ч. какие правила записаны в *Values
А мне не понятно, почему вы оба говорите именно про алгорифмы, а не про λ-исчисление или комбинаторную логику. По моему мнению, после λ и 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) и есть режим больших чисел. Без ограничений таблицу результатов нельзя составить в принципе. Так что не зачёт.
Категорически не соглашусь со сказанным.
Недавно мне джун примерно такими же словами ругался, что время тратится на удовлетворение правил линтера. Я же объяснял, что линтер — это всего лишь инструмент, а правила помогают обнаружить места, которые, вероятно, вызовут у читателя кода затруднение. Надо снижать когнитивную нагрузку на читателя, даже если это потребует чуть больше времени от писателя.
Потому что в украинском -и в инфинитиве не сократилось до -ь:
«Він має пишатися і він пишається»
Заметим, что здесь форма инфинитива и 3 лица различны.
Выше @nronnieпривёл формальное определение O-нотации, из которого видно, что время работы T(n) может одновременно относиться к нескольким разным функциям f(n), если соблюдаются упомянутые условия. Так, если T(n) = O(n), то всегда можно сказать, что T(n) = O(n^2), хотя и бесполезно. Аналогично, если T(n) = O(n (log n)^2), то T(n) = O(n sqrt(n)).
В сущности, вопрос может быть сведён к тому, насколько точную оценку мы хотим предоставить в O-нотации. Если мы хотим сказать «ну, время растёт быстрее n log n, но всяко медленнее n sqrt(n)», то пишем O(n sqrt(n)). Если хотим сказать «время растут не быстрее n (log n)^2 и это хорошая оценка», то пишем O(n (log n)^2). Собственное имя есть не у каждого класса функция (что очевидно, ведь имён конечное количество, а классов функций несчётно много).
Встречный вопрос:
1) Дифференцируемые и, в частности, гладкие функции — непрерывные.
2) Дикая функция Вейерштрасса не дифференцируемая и тем более не гладкая.
Вопрос: непрерывна ли дикая функция Вейерштрасса?
Пример про медведей корректный, но вопрос про Лондон в статье «Без логики сложно» звучит немножко издевательски.
Я мог ошибиться, описал субъективное видение из далёкого прошлого. Когда я покинул НИИ и у меня кончилась действующая лицензия, решил купить у них. Единственная подходящая лицензия стоила за год как 1/4 моей месячной зарплаты. Естественно я не стал её приобретать.
Когда на одном из мест работы встал вопрос, а не использовать ли нам Вольфрам, начальство посмотрело и сказало, что потенциальная выгода от языка и стандартной библиотеки не покрывает стоимость и риски, связанные с длительным сопровождением будущих программных компонент на Вольфраме. Деталей не знаю.
В текущем виде — да. Впрочем, я на нём и XML-файлы парсил и анализировал, и с файловой системой работал, и строил иллюстрации к статьям, и числодробилку писал. У языка есть потенциал стать вполне хорошим скриптовым языком.
Ну так я и не утверждал, что на WL невозможно такое написать. Можно, но для этого надо выработать определённую дисциплину: на каждый символ приходится не более одного определения (Set, SetDelayed), все определение должны идти строго перед запуском вычислений и быть строго на верхнем уровне программы, нельзя использовать никакие «опасные» функции (Print, Set, Function, Module) в качестве комбинаторов и т.д. и т.п.
Проблема в том, действительно ли перед нами комбинатор или это выражение мимикрирует под комбинатор, но таковым не является. WM принципиально не позволяет ответить на подобные вопросы; из ниоткуда может в любой момент вычислений вылезти побочный эффект (самый неприятный для отладки — доопределение символов более специфичными правилами, которые не соответствуют семантике основного правила). Ставится крест на принципе Черча-Россера (результат вычисления не зависит от стратегии) и на ссылочной прозрачности (любое выражение может быть заменено на эквивалентное, полученное в результате вычисления).
P.S. моё предыдущее сообщение относилось к обсуждению алгорифмов Маркова, которые я считаю достаточно плохим формализмом по сравнению с другими. Те же λ-исчисление или комбинаторную логику можно использовать вот прямо как есть, это не «Тьюрингова трясина», хотя сложные программы на них не напишешь. Писать алгорифмы Маркова для решения хотя бы простой практической задачи нереально. «Change my mind»
@BoomburumУ нас проблема. Я вставляю в decoded-формате, а хабр автоматом конвертирует в не-пойми-что.
По теме: можете сами поискать «композиция алгорифмов маркова» — это алгоритм переписывания алгорифма так, чтобы к нему можно было дописать другой алгорифм.
Возьмём к примеру CL. В ней выражения (комбинаторы) применяются к другим выражениям, применение всегда одноаргументно. У каждого комбинатора есть комбанаторное свойство, которое определяет, как он будет вычисляться. Например, есть комбинатор I со свойством I[x] = x; или комбинатор K со свойством K[x][y] = x, или S[x][y][z] = x[z][y[z]].
Объекты, свойства, понятия, процессы в предметной области соответствуют своим комбинаторам. Какие-то комбинаторы просто постулируются вместе со своими свойствами, какие-то можно определить через другие (но определение должно сохранять комбинаторное свойство!), какие-то мы оставляем «неопределёнными», то есть рассматриваем их как переменные. Последние в будущем будут заменены на конкретные выражения, когда данные подъедут. Или нет.
Возьмём алгорифм Маркова. Если я работаю с матрицами, какая подстрока или какое правило соответствует понятию «матричное умножение двух неких матриц A*B»? Если я к программе добавлю ещё какие-то правила, будет ли это же (правило или подстрока) соответствовать ровно тому же понятию? Едва ли. Посмотрите, как всю программу приходится переписывать ради того, чтобы дописать другую подпрограмму.
WL (точнее, WM) был популярен среди учёных. В широкие массы он не вышел из-за 1) конской цены, по которой он большую часть времени распространялся, когда народ присматривался к этому инструменту, ну и упомянутая другими проприетарная лицензия, и 2) рекламы и позиционирования: Стив его пиарил как шайтан-машинку, которая и тайны мироздания моделирует, или около-человеческую речь понимает, а ещё крестиком вышивать умеет, в то время как рядовому пользователю нужен обычный ЯП общего назначения с низким порогом входа и с хорошей библиотекой для решения его, пользователя, задач (собственно, поэтому Fortran и Python заимели популярность в своё время). Причём WL является таким ЯП, но чтобы Стив так сказал, нужно гордостью подавиться. Посмотри на переводные статьи про WL на хабре — много ли желания возникает использовать его для решения частных бытовых задач?
Костыли, конечно, есть, но это не квадратные скобки. К слову, WL один из немногих языков, в которых группировочные скобки для разбора выражений с инфиксными операторами и скобки, входящие в состав синтаксического выражения (список аргументов, кортеж и т.п.), различаются графически. К примеру, в JS скобки в
x = (a, b)иx = f(a, b)выполняют разную роль.Также
//не проблема, ведь всегда можно использовать префиксную запись.К костылям я бы отнёс императивность интерпретатора, которая вынуждает внимательно следить за тем, в каком состоянии находится ядро (kernel), в т.ч. какие правила записаны в
*ValuesА мне не понятно, почему вы оба говорите именно про алгорифмы, а не про λ-исчисление или комбинаторную логику. По моему мнению, после λ и 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) и есть режим больших чисел. Без ограничений таблицу результатов нельзя составить в принципе. Так что не зачёт.