Комментарии 10
В Латехе.
Латех, латекс… да какая разница?)
Как писал Кнут в TeXBook, "TEX (pronounced tecks) is the admirable Text EXecutive processor developed by Honeywell Information Systems", т.е. совсем другая штука.
Разумеется, сейчас мало кто перепутает, но всё-таки стоит учитывать рекомендации создателя TeX, особенно когда этому посвящена вся первая глава.
English words like ‘technology’ stem from a Greek root beginning with the letters τεχ...; and this same Greek word means art as well as technology. Hence the name TeX, which is an uppercase form of τεχ.
Insiders pronounce the χ of TeX as a Greek chi, not as an ‘x’, so that TeX rhymes with the word blecchhh. It’s the ‘ch’ sound in Scottish words like loch or German words like ach; it’s a Spanish ‘j’ and a Russian ‘kh’. When you say it correctly to your computer, the terminal may become slightly moist.
Не знаю, поможет ли автору мой комментарий, но поскольку сам был вдохновлен подобной идеей когда-то (до практики руки не дошли), накопились некоторые соображения по теме. Я имел неплохой опыт работы с Wolfram Language и большинство замечаний будут так или иначе связаны с ним. Также спешу заметить, что в репозиторий с кодом я так и не заглянул, потому если что-то уже именно так и реализовано, но в статье не отражено (или я не понял) — оно и к лучшему (надеюсь).
Во-первых. Pattern matching — прекрасная концепция функциональных языков. И она же по сути является краеугольным камнем любых символьных манипуляторов. (Может быть дело пойдет проще в F#?) В примере из предыдущей статьи с "уплощением" дерева для операции + (т.е. перевод x + (y + ...) в x + y + ...) автор вынужден был использовать слишком общие паттерны вроде any
, const
, Num(1)
и т.д. Т.е. никак нельзя взять и сопоставить целое поддерево. Было бы куда проще, если бы можно было задавать правила не вида
if expr == plus(const1, any1) && any1 == plus(const2, any2)
а прямо-таки
if expr == plus(any1, plus(any2, any3))
Для сравнения, так оно в Mathematica и реализовано. Сопоставить одно выражение с другим очень и очень просто:
MatchQ[plus[1, plus[2, plus[3, 4]]], plus[x_, plus[y_, z_]]] == True
Несложно и заменить все вхождения данного паттерна в дереве:
plus[1, plus[2, plus[3, 4]]] //. plus[x___, plus[y__], z___] :> plus[x, y, z]
(* prints plus[1, 2, 3, 4] *)
Плюс, поскольку такие общие (x___
в частности) паттерны все-таки довольно накладны, математика из коробки предлагает т.н. атрибуты. Например, атрибут Flat
, будучи присвоен функции plus
, лишает нас необходимости самим ее уплощать.
Если бы можно было писать произвольные паттерны и доставать из них все упоминающиеся переменные (plus(a_, b_) => {a = ..., b = ...}
), все бы существенно упростилось.
Во-вторых. Что касается упрощений, тут дело гораздо сложнее. Расширенный pattern matching, конечно, поможет, но шаблоны могут быть довольно сложные. Опять же, математика решает этот вопрос в Simplify
и FullSimplify
путем перебора всех возможных комбинаций подвыражений данного выражения: к каждой комбинации применяется та или иная упрощающая тактика, оценивается качество упрощения. Про качество тоже отдельный разговор. Например, можно минимизировать количество листов дерева выражения. Или длину максимальной ветви дерева. Играя с этим, можно делать интересные вещи.
В Simplify
применяются некоторые эвристики, так что не все комбинации выражений действительно берутся в расчет. Вот пример вывода шагов упрощения выражения x^2 + 2x + a + 1
до a + (1 + x)^2
(вывод FullSimplify
будет куда длиннее; к сожалению, я не знаю способа вывести это в формате "до-после", тут только "до"):
1 + a + 2 x + x^2
2 x
x^2
1 + 2 x + x^2
(1 + x)^2
1 + x
a + (1 + x)^2
...
Код получения такого вывода:
Simplify[x^2 + 2 x + a + 1, TransformationFunctions -> {Echo, Automatic}]
Как выражать правили замены? Думаю, также, как и сейчас — паттернами. Создается список элементарных упростителей. Далее перебором комбинаций подвыражений (поддеревьев т.е.) производятся попытки упрощения каждым упростителем. Из-за закрытых исходников математики мой интерес в этой области остался неудовлетворенным.
В-третьих. Я, конечно, понимаю, что проект скорее учебный, но все же зашивать упростители и решатели для конкретных функций прямо в код — не дело. Набор гибких паттерн-ориентированных упростителей существенно улучшит качество продукта, да и позволит добавлять новые функции на лету. Может даже для этого какой язык можно придумать простенький.
В-четвертых. Раньше уже упоминали, что можно компилировать выражения прямо в IL-код или в какие-нибудь нативные представления AST (Expressions). Математика тоже так может, плюс она может и в машинный код. Где-то на хабре была статья о компиляции математических функций в IL, но, боюсь, ту, о которой помню, не найду. Вот другая.
В-пятых. Вообще я был вдохновлен подходом интерактивных proof assistant'ов (Coq, The KeY Project, Z3 и т.д.). И прямо-таки горел желанием что-то свое написать. Но не срослось, поскольку я оценил объем работ неподъемным. Идея была в том, чтобы на каждом из этапов упрощения позволять пользователю выбирать ту тактику упрощения, которая бы ему была более приемлема. Из вычислителя-упростителя система тогда превращается в настоящую систему компьютерного доказательства. Мы выдвигаем гипотезу, что \forall x . sin(x)^2 + cos(x)^2 = 1
, доказываем ее как-либо и оформляем в виде теоремы основн_триг_тождество
. Далее уже можно на нее ссылаться, чтобы упростить sqrt(1 - sin^2(x))
, заменив, например, 1. С группировкой тактик и теорем по категориям и с добавлением изрядной доли эвристик можно даже пользователя привлекать минимально к процессу доказательства. Проблем здесь много — чего только стоит контекст (например, теорема верна, если только x \in \Reals
или x \in \Complex
), потому я не буду сильно много здесь размышлять.
В-шестых. Хорошо бы на каком-либо этапе более детально осмотреться. Я имею в виду, например, подсмотреть у Mathematica и у готовых open source продуктов (у Axiom есть прямо-таки теоретические материалы, правда на поверку весьма скудные, где, кроме прочего, есть и аннотированные исходники). К сожалению, по вопросам систем компьютерной алгебры (СКА, CAS) крайне мало подробной информации (во всяком случае мне попадалось).
if expr == plus(any1, plus(any2, any3))
У меня нет такового ужаса, и все ваши комментарии в сторону того, что нельзя хардкодить паттерны не очень уместны, так как я их и не хардкодил. Вот их список: https://github.com/Angourisoft/MathS/blob/master/AngouriMath/Functions/Evaluation/Patterns/Patterns.cs
И вообще, на данный момент simplify более менее нормально работает, ваш пример проработает в том числе.
Простенький язык я придумывать не буду так как смысла в ран-тайме добавлять функционал не вижу. Хотя кто знает, может и понадобится когда-нибудь. Но тогда это нужно очень узкой аудитории.
Насчет компиляции в IL — ок, сделаем.
Пятое: да, действительно умная упрощалка, которая будет работать не за экспоненту — это сложно. Хотя может и в эту сторону будем развиваться.
Чекну Axiom. У mathematica я подсмотреть не смогу по очевидным причинам
Этот "ужас" — просто псевдокод, чуть-чуть приближенный к математике по синтаксису. Демонстрация подхода. Про хардкод скорее относится к фрагментам кода конкретно из этой части статьи, а именно к аналитическим солверам. Вы сами демонстрируете фрагменты с switch (func.Name) { case "sinf" ... }
, собственно, вот. Здесь есть над чем поработать.
У Mathematica прекрасная документация. Так что многие вещи можно вынести оттуда. Есть достаточно много открытых проектов и на ней. В т.ч. всякие пакеты символьных вычислений над тензорами — вот где нужен хороший pattern matching! Я в свое время тоже с этим игрался в математике (маленький самописный тензорный движок) и был почти доволен.
НЛО прилетело и опубликовало эту надпись здесь
Пишем «калькулятор». Часть II. Решаем уравнения, рендерим в LaTeX, ускоряем функции до сверхсветовой