Pull to refresh

Comments 31

С inline-формулами, наверное, ничего особо не сделаешь, это нужно как-то делать на уровне движка Хабра, так? Кастануть бы кого-нибудь вроде Boomburum


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


UPD Перерендерил часть формул в картинки, теперь на мобилке смотреть немного удобней.

Хм… В алгоритме Евклида вообще-то фигурирует деление с остатком, а не вычитание.
Хотя с вычитанием тоже будет работать, но уж больно долго.
Хм… В алгоритме Евклида вообще-то фигурирует деление с остатком, а не вычитание.
Ну да… именно поэтому, — «на наши деньги»- его оригинальное название значит что-то типа «пропорциональное вычитание». Если, конечно, мой склероз меня не обманывает. :-)
Хмм, это ведь языки для разработки аппаратных схем, а TLA+ — средство логической верификации/моделирования алгоритмов (которые потом да, могут воплощаться в конкретную реализацию в железе и моделироваться уже в Verilog/VHDL)
Что-то меня всегда не улыбало смотреть на условия.
Зачем проверять какое из чисел больше, когда можно найти разницу (меньшее число) и из суммы чисел вычесть разницу и поделить это на два (большее число)?
x = abs(a - b);
y = (a + b - x) / 2;
С точки зрения алгоритма, замена равнозначная. А с точки зрения практики применения — нет, т.к. в зависимости от реализации a+b может вызвать переполнение. Поэтому и начинаются упомянутые пляски поверх алгоритма:
у M и N будет определенный тип, BigInteger или что-то в таком роде; нужно будет определить поведение программы в случае, если M и N неположительные; и так далее и тому подобное
Даны два бесконечных числа:
11110110101010101…
11110010101110111…
Какое из них больше легко найти, а время на поиск полной разницы составит бесконечность.
Похоже на туториал по рисованию совы.
Сначала для примера рассмотрим алгоритма Евклида, а затем вы и сами легко поймёте, как это всё применяется на сложных распределённых и параллельных программах.
А так всегда — долго-долго мусолим концепцию на простом примере и переходим к следующей не задерживаясь на сложных практических случаях. Но у этого есть совершенно определенный смысл: понять концепцию гораздо проще если не приходится продираться через сложный алгоритм. С другой стороны, разбор чего-то сложного займет на порядок или два больше места — такой разбор просто не получится сделать в рамках доклада на конференции или статьи на хабре (или в аналогичном месте). Это можно сделать в учебнике или в серии статей конечно.
λ-исчисления придуманы уже давно. Функциональные языки тоже. А машина состояний и логическое программирование — даже не тьюринг-полны и имеют предельно узкое применение.
Примеры с рекуррентным алгоритмом это хорошо, но создается впечатление что TLA для них только и заточен. Вот например как на TLA выразить алгоритм, который в файл выводит Hello world? Как написать какой-нибудь fizzbuzz?

Наверное у них есть монады, что-то вроде Next = “fizz” + Next’

Вы далеки от темы и вас пугают языки программирования? Предикаты и лямбда-функции решат вашу проблему.

Они вас пугают куда больше? Не понимаю. Я 20 лет работаю профессором математики и меня они не пугают.
Ну так языки надо учить, а новое учить тяжело) А математика уже знакома.
Даже программисты часто считают что математика рулит. Что сейчас вот мы возьмем монады и забудем о всей низкоуровневой мелочи.

На работе хаскель — каждую вторую программу приходится профилировать по памяти, для приемлемой скорости добавили битовые векторы, недавно был баг с переполнением переменной.

Но зилоты не устают повторять что хаскель дает нам невероятно абстрактный код и надежные бинарники.
Сорри, не туда) Вот-вот. Я думаю что некоторым хочется в это верить) В программирование она привнесла только отсутствие пробела перед вводом аргументов функции, и нумерацию массивов с нуля (ибо в математике с какой-то стати это диапазон, а не группа элементов).
На работе хаскель — каждую вторую программу приходится профилировать по памяти, для приемлемой скорости добавили битовые векторы, недавно был баг с переполнением переменной

напишите статью об этом
Дело в том, что этот алгоритм нельзя увидеть, если ваше мышление сосредоточено на коде, на типах, исключениях, циклах while и прочем, а не на математических свойствах чисел.

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

То, что я прочитал, похоже на глоток свежего воздуха. Спасибо!

«Не используйте языки программирования, вот вам ещё один язык программирования»

UFO landed and left these words here
Все написанное в статье действительно очень здорово, и тот, кто начнет писать программы, основываясь на мат аппарате изменит индустрию, но тут мне приходит на ум аналогия со строительством, сопромат как наука зародился в XVIII веке, но это не значит, что до этого момента люди не строили никаких сооружений, причем не плохо так строили. То, что предлагается в статье — это будущее, но программы нужны уже сегодня. Просто мы еще в начале пути.
Четкой разницы между алгоритмами и программами нет,

ИМХО четкая разница в формуле Вирта:
Алгоритмы + структуры данных = программы,
Нпр.,
у M и N будет определенный тип, BigInteger

алгоритм Евклида м.б. реализован на языке, где нет типа BigInteger.
А LaTeX — великая вещь! Респект.
что-то мне напомнило анекдот про лису: «только бухгалтерии добавилось»
«В каждой большой программе живет алгоритм, который пытается выбраться наружу»

Скорее, каждая программа создана пытаться завершиться, но постоянно мешают циклы.
Было бы интересно узнать о производительности TLA+ и его сравнении с прологом. Или же в вопросах верификации производительность роли не имеет?
Only those users with full accounts are able to leave comments. Log in, please.

Information

Founded
Location
Россия
Website
jugru.org
Employees
51–100 employees
Registered

Habr blog