TermWare: система символьных вычислений

 Руслан Шевченко. Киев, ГрадСофт

http://www.gradsoft.ua





Приятное совпадение — сам проект (TermWare) был анонсирован 5 лет назад на OSDN-2003. Готовясь к написанию этой статьи для OSDN-2008, я только что обнаружил, что TermWare входит в 10-ку лучших систем встраиваемых правил с открытым кодом по версии Business Review Online.

Немного истории

Наверное, сначала надо рассказать о том, что такое символьные вычисления и переписывающие правила. Мы стоим на плечах гигантов: рассказывать придется издалека. Пожалуй, рассказ о Думающей Машине Лувилля мы опустим, начнем сразу с Глушкова:

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

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

Это цитата из программной статьи Глушкова «Кибернетика и управление производством» в газете «Правда», 1962 г. Прошу прощения за столь длинную цитату — не могу удержаться, сейчас такой стилистики и такого слога уже не встретишь. Так вот: именно в институте кибернетики, кроме всего прочего, занимались автоматизацией математических исследований и ввели в обиход само понятие символьных вычислений и правил переписывания. В отличие от «обычных» вычислений, символьные вычисления работают не с цифрами, а с символами, а правила переписывания моделируют основные паттерны мышления математика. Это просто преобразования, виду x y, где x и у — какие-то математические выражения. К примеру, можно вспомнить школу и правила дифференцирования:

Δ(f*g) Δ(f)*g+f*Δ(g)

 
Или институт и правила интегрирования:
I(f*Δ(g))f*g-I(g*Δ(f))
 

Каждая отрасль математического знания состоит из таких вот правил переписывания и знаний о том, как и когда их применять (стратегии применения). Глушков представлял себе систему поддержки математического творчества как некоторые средства логического вывода и математических правил, с которыми может интерактивно работать математик. В [1] [2] был определен язык АНАЛИТИК, в который были включены элементы символьных преобразований. Как бы сказали сейчас, «killer application» для этой среды выступали алгоритмы символьного интегрирования. В дальнейшем этот язык поддерживался, был перенесен на современные архитектуры ЭВМ и эволюционировал в сторону системы компьютерной алгебры. Последнее упоминание о работе над системой Аналитик в литературе относятся к 2002 г. [3]

В 90-ых один из авторов языка Аналитик (Александр Адольфович Летичевский) начал говорить о концепции «Алгебраического программирования», как основной парадигмы, где сущностная часть решения какой-либо алгоритмической задачи полностью описывается в терминах символьного преобразования, а процедурное описание используется только для порядка применения правил. Так появилась система APS [4], состоящая из библиотеки организации термов на С и интерфейса языка высокого уровня. Мне посчастливилось работать в Институте Кибернетики именно в этой группе в самом начале моей профессиональной деятельности, и язык TermWare многое унаследовал от APS. Кстати, сама система APS развивается до сих пор, и там тоже с тех пор появилось довольно много интересного.

Зачем потребовалась новая система?  Там решались три основных вопроса:

И в 2002 году, при поддержке Анатолия Ефимовича Дорошенко, началась разработка TermWare [5] и ее использование в Институте Программных Систем.

В целях полноты картины надо еще упомянуть о дальнейшем развитии APS и еще одном отвлетвлении Аналитика:






Про APS — система продолжает развиваться, правда, уже в основном вне стен института кибернетики. Там вырабатали довольно-таки своеобразный подход к проблеме с динамическим окружением времени выполнения: в termware окружение как бы внешнее по отношению к системе, которую мы описываем; они же строят метаописание агентской среды (так называемую алгебру поведения), включающее взаимодействия, для чего придумали новую парадигму: инсерционное программирование. [6]

Наконец, существует еще ветка САД (Система Автоматизации Дедукции). Это развитие работ о «компьютерном помощнике» работающего математика. Эти работы ведутся на кафедре теоретического программирования Киевского Университета, и у них есть реально работающая система, позволяющая при соблюдении ряда не очень обременительных условий пропускать статьи в TeX-е через систему верификации доказательств. Это, кстати, тоже свободное ПО, распространяющееся по лицензии GPL: http://nevidal.org/sad.ru.html

Заткнись и покажи код.

Да — что такое переписывающие правила, мы объяснили. Теперь покажем несколько примеров:

Преобразование числа из цифр в текст:



domain(examples, 
 system(Number2String,default, 
  ruleset( 
     import(general), 

     numberToString($x) -> p($x), 

     p(0) -> "zero", 
     p(1) -> "one", 
     p(2) -> "two", 
     p(3) -> "three", 
     p(4) -> "four", 
     p(5) -> "five", 
     p(6) -> "six", 
     p(7) -> "seven", 
     p(8) -> "eight", 
     p(9) -> "nine", 
     p(10) -> "ten", 
     p(11) -> "eleven", 
     p(12) -> "twelve", 
     p(13) -> "thirteen", 
     p(14) -> "fourteen", 
     p(15) -> "fifteen", 
     p(16) -> "sixteen", 
     p(17) -> "seventeen", 
     p(18) -> "eighteen", 
     p(19) -> "nineteen", 
     p($x) [ $x > 19 && $x < 100 ] ->   $x % 10 == 0 ? pd($x / 10) : 
                                       l([pd($x/10),p($x % 10)]) 
       | 
        [ $x >= 100 && $x < 1000 ] -> 
                $tens == 0 ? 
                      l([p($handreds),sIfNotOne($handreds,"handred")]) 
                       : 
                      l([p($handreds),sIfNotOne($handreds, "handred"),p($tens)]) 
                  where ( 
                    $handreds <- $x/100, $tens <- $x % 100 
                  ) 
       | 
        [ $x >= 1000 && $x < 1000000 ] -> 
                   $handreds == 0 ? 
                        l([p($thousands),sIfNotOne($thousands,"thousand")]) 
                                     : 
                        l([p($thousands),sIfNotOne($thousands,"thousand"), p($handreds)]) 
                    where ( 
                       $thousands <- $x/1000, 
                       $handreds <- $x % 1000 
                    ) 
       | 
        [ $x >= 1000000 && $x <= 1000000000 ] -> 
                      $thousands == 0 ? 
                             l([p($millions),sIfNotOne($millions,"million")]) 
                                   : 
                             l([p($millions), 
                                sIfNotOne($millions,"million"),p($thousands)]) 
                      where ( 
                       $millions <- $x/1000000, 
                       $thousands <- $x % 1000000 
                      ) 
       | 
        [ $x > 100000000 ] -> l([ "number", "is", "too", "big" ]), 

       sIfNotOne(1,$x) -> $x, 
       sIfNotOne($x,$y) [ isNumber($x) ] -> String.concat($y,"s"), 

       pd(2) -> "twenty", 
       pd(3) -> "thirdy", 
       pd(4) -> "fourty", 
       pd(5) -> "fifty", 
       pd(6) -> "sixty", 
       pd(7) -> "seventy", 
       pd(8) -> "eighty", 
       pd(9) -> "ninty", 
       l([$x:$y]) -> String.concat(reduce($x)," ",reduce(l($y))), 
       l([$x]) -> l($x), 
       l($x) -> $x, 
       l([]) -> "" 

  ), 
  FirstTop 
 ) 
); 

Игра Жизнь

domain(examples, 

  system(Life1,javaFacts(Life1DB,"ua.gradsoft.termwaredemos.life.Life1Facts"), 
         ruleset( 
             # $T - set of pairs to test. 


        { l($i,$j) : $T} [ n($i,$j) == 3 ] -> $T [ putCell($i,$j) ] , 

        { l($i,$j) : $T} [ n($i,$j) == 2 ] -> $T [ existsCell($i,$j) ? putCell($i,$j) : removeCell($i,$j) ], 

        { l($i,$j) : $T} [ n($i,$j) > 3 || n($i,$j) < 2 ] -> $T [ removeCell($i,$j) ] , 


        { } -> $T [ [ showGeneration() , generateNextTestSet($T) ] ], 

        checkEmpty({$x:$Y}) -> { $x:$Y }, 
       checkEmpty({}) -> END 

                ), 
         FirstTop) 

); 

Правило выставления инвойса:

(из конфигурации бизнес-приложения)



domain(examples, 
  system(Invoicing,default, 
         ruleset( 
           # import general operations. 
           import(general), 

           # handle new invoice and set one to paid if possible. 
           @class("ua.gradsoft.termwaredemos.invoicing.Invoice", $invoice) 
                        [ ! $invoice.isPayed() 
                           && 
                            $invoice.getCustomer().getAccountBalance() - $invoice.getAmount() + $invoice.getCustomer().getCreditLimit() > 0 
                        ] 
                          -> true 
                             [ $invoice.getCustomer().decrementAccount($invoice.getAmount()) 
                               && 
                               $invoice.setPayed(true) ], 


           # set credit limit in depend from summary payments. 
           @class("ua.gradsoft.termwaredemos.invoicing.Customer", $customer) 
                        [ $customer.getAccountBalance() > 0 && $customer.getSummaryPayments() > 2000 ] -> true [ $customer.setCreditLimit(500) ] 

         ), 
         FirstTop) 
);



Где и как такие системы применяются:



Два самых очевидных случая — системы управления бизнес-процессами (с помощью настраиваемых правил описывается, в каком состоянии может быть какой-то процесс) в духе [7] и экспертные системы. Подобная подсистема есть чуть ли не в каждой крупной корпоративной системе; мы сами встраивали ее несколько раз.

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

Известно, что наша система применяется также в приложениях автоматизации домашней электроники и в системах моделирования той же электроники.

Второй большой слой применения — это инструментальные средства (и вообще работа с формальными моделями). Cобственно, ради этого TermWare и создавалась. Тут есть еще особенность — в архитектуре termware есть слой подключения моделей других языков через plugin-ы, поэтому встроить какой-либо язык так, что бы его AST можно было рассматривать как объект termware, не составляет труда. В качестве примера вместе с дистрибутивом распространяются такие драйвера для языков java и graphviz.



На их основе построены средства анализа языка Java, которые умеют делать довольно широкий спектр задач: от слежения за соблюдением стандартов кодирования до контроля соблюдения дисциплины работы с ресурсамито есть мы можем «частично» проанализировать пути выполнения программы и определить места, где ресурсы выделяются, но не освобождаются. [8] (см. JavaChecker: http://www.gradsoft.kiev.ua/products/javachecker_rus.html)

Одним из «больших» применений является использование построенных таким образом средств анализа Java кода как промежуточного уровня — JavaChecker--- может экспортировать API для семантической (а не синтаксической) модели программ. Это тоже свободное ПО. Вещи, которые относительно легко сделать, используя наше инфраструктурное ПО - визуализация структуры зависимостей или поиск уязвимостей.

Следующий шаг — это т. н. символьные вычисления на уровне трансформации программ, когда мы можем преобразовать одну программу в другую. Это может иметь смысл при портировании ПО на устройства с ограниченной мощностью либо наоборот, на кластеры с другими структурными характерстиками (автоматическая параллелизация).

Для Java мы сделали небольшой проект по ограниченной специализации програм — когда на входе у нас пакет исходного кода и набор значений переменных, а на выходе — этот же код, но «вычисленный и оптимизированный» по отношению к этим переменным. (cм JPE: http://www.gradsoft.kiev.ua/products/jpe_eng.html) Мы думаем, этим могут заинтересоваться люди, пишущие для мобильных телефонов (правда, на этом проекте мы будем опробовать бизнес-модель «сада с платным входом», так что это ПО открытое, но не бесплатное).

Исследованиями в области автоматического распараллеливания исходного кода занимается группа в ИПС НАНУ. Там сделан входной драйвер для схем алгебр Цейтлина, к которым применяются преобразования. [9]

Там же было проведено моделирование с помощью TermWare протоколов связи сенсорной сети. Описание протоколов сенсорной сети (наподобие ZigBee) на TermWare (которое обошлось в 123 правила, в то время, когда их реализация на не-декларативных языках занимает несколько тысяч строк) было встроенно в систему имитационного моделирования AnyLogic, с тем, чтобы можно было быстро посмотреть, как те или иные параметры протокола влияют на устойчивость и время жизни сети, не прибегая к дорогостоящим экспериментам) [10]

Ну и еще одна большая область применений — инфраструктура ПО. Если коротко, то всюду, где есть потенциальные таблицы переходов, применение termware вместо них будет и удобнее, и документированнее.

Поработаем вместе ?



В 90 годы был довольно популярен одесский стиль ведения бизнеса, иллюстрирующийся сделками, когда контрагенты договариваются, скажем, о покупке/продаже вагона апельсинов за деньги, после чего первый участник сделки идет искать деньги, а второй — апельсины. Менеджмент OSS проекта немного труднее: надо одновременно искать и деньги, и апельсины.

То есть, нам нужны участники проекта со всех сторон.

Сначала продаем:

Пользуясь случаем, обращаюсь к представителям украинских оффшорных компаний: если вам заказывают экспертные системы или системы правил бизнес-процессов, а вы вместо нас используете какой-то Drool или Jess — вы много теряете. Кроме того бесспорного факта, что наш наш язык лучше ;), мы еще и находимся рядом и можем помочь с интеграцией (или самим провести ее), обучением и доработкам. Кстати, большинство документации есть как на английском, так и на русском языке.

Еще нам интересно связаться с теми, кто пишет на Java для мобильных телефонов, - возможно, использование JPE будет вам интересно.

Также имеет смысл позвать нас, если у вас есть проекты, связанные с автоматическим или полуавтоматическим анализом больших массивов кода, - у нас есть соответствующие инструментальные средства, и мы можем покопать в этом направлении.

Естественно, можно нас не звать, а просто использовать наше ПО. Мы будем этому только рады. Если Вы об этом еще и где-то напишете, будем рады вдвойне.



Потом покупаем:

Если вас заинтересовало программирование, основанное на правилах, либо анализ кода, либо что-то еще из применений и приложений — используйте, делайте, пишите. Если просто хочется ознакомиться с termware и есть свободное время — пишите в группу рассылки. Как в любом проекте, есть куча вещей, которые хорошо бы усовершенствовать.

Что было бы интересно и полезно, и не очень трудно сделать:

Что сложнее, но очень интересно:



Спасибо за внимание.



И список URL на память:







Cписок литературы

1: Глушков, Костырко, Летичевский и др., Математичесике методы исследования и оптимизации систем , О языке для записи формальных теорий,

2: В. М. Глушков, Костырко В.Ф. Летичевский А.А. и др, АНАЛИТИК (алгоритмический язык для описания вычислительных процессов с использованием аналитических проебразований), 1971

3: В. П. Фишман Ю. С. и др. Математические системы и машины , Аналитик 2000,

4: Летичевский, Капитонова Ю. В. , Кибернетика , О конструктивном математическом описании предметных областей, 1998

5: Шевченко Р. С. Дорошенко А. Е., Проблемы Программирования , Система символьных вычислений для проектирования динамических выражений, 2003

6: A.Letichevsky, D.Gilbert, Resent Trends in Algebraic Development Techniques. LNCS , Model for Interaction of Agents and Environments, 1999

7: R. Shevchenko, A. Doroshenko, ISTA 2003 , Managing Business Logic with Symbolic Computations , 2003

8: R. Shevchenko, Статический анализ програмного обеспечения с помощью техник переписывания, 2008

9: Дорошенко А.Е. and Жереб К.А. and Яценко О.А, Проблемы программирования , вычислений в многопоточных программах, 2007

10: Дорошенко А.Е. and Жереб К.А. and Шевченко Р.С, УКРПРОГ 2006 , О моделировании сенсорных сетей средствами высокого уровня,