JUG Ru Group corporate blog
Programming
Algorithms
Conferences
Distributed systems
Comments 31
+4

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


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


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

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

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

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

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

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

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

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

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

+6

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

+2

Статья называется "Если вы не пишете программу...". Если вы пишете программу, вам нужна другая статья. Еще там сказано:


В докладе пойдёт речь о формальных методах, применяемых в разработке сложных и критичных систем вроде космического зонда Rosetta или движков Amazon Web Services.

Если разрабатываемая вами система не настолько сложна/критична вам опять нужна другая статья.

+1
Все написанное в статье действительно очень здорово, и тот, кто начнет писать программы, основываясь на мат аппарате изменит индустрию, но тут мне приходит на ум аналогия со строительством, сопромат как наука зародился в XVIII веке, но это не значит, что до этого момента люди не строили никаких сооружений, причем не плохо так строили. То, что предлагается в статье — это будущее, но программы нужны уже сегодня. Просто мы еще в начале пути.
0
Четкой разницы между алгоритмами и программами нет,

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

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

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