TermWare: Описание Семантики
DocumentId:GradSof-TermWare-r-Sm-20.06.2001-4


August 18, 2008

Contents

1 Введение (Introduction)
2 Формальная модель (Formal Model)
 2.1 Алфавит (ABC)
 2.2 Термы (Terms)
 2.3 Операции (Operations)
 2.4 Упорядоченные множества правил
 2.5 Действия (Actions)
 2.6 Терминальная система со взаимодействием (term system with actions)
3 Язык TermWare (Language)
 3.1 Иерархическая система имен
 3.2 Встраиваемые парсеры других языков
4 Java API
 4.1 Работа с термами
  4.1.1 Term
  4.1.2 TermFactory
  4.1.3 ITermTransformer
  4.1.4 ITermRewritingStrategy
  4.1.5 IFacts
  4.1.6 IEnv
  4.1.7 TermSystem
 4.2 Воспомогательные классы
  4.2.1 TermWare
  4.2.2 TermWareInstance
  4.2.3 IParser, IParserFactory
  4.2.4 IPrinter, IPrinterFactory
5 Перечень изменений

1 Введение (Introduction)

Termware - система компьютерной алгебры, предназначенная для встраивания в системы языковой обработки. В этой статье определяется формальная модель, лежащая в основании семантики языка, бегло описывается синтаксис языка TermWare и внутреннее строение Java API. Текст рассчитан на знакомство читателя как с практикой объектно - ориентированного и функционального программирования, так и с основами математической логики. Впрочем, если Вы — программист, думающий использовать TermWare в своих проектах, то чтение первой части можно заменить чтением ее первого параграфа.

2 Формальная модель (Formal Model)

Здесь построена обычная терминальная алгебра, где объектами языка являются термы (выражения вида fi(x1xn), переменные и элементарные типы данных, такие-же как во всех языках функционального программирования) с одним отличием от стандартного подхода: конструктор упорядоченного множества является выделенным термом и операции подстановки на этих термах сохраняют порядок.

Остаток раздела посвятим обычному утомительному построению:

2.1 Алфавит (ABC)

  1. Множество примитивных типов (внимание, это не многосортная алгебра)

    Σpt = {CHAR,SHORT,INT,BigDecimal,BigInteger,BOOL,STRING,ATOM}

  2. Множество типизированных констант Σcpt = {cipt}, с каждой константой связанно значение, на множестве соответствующего примитивного типа, т. е. val : Σcpt- > Dompt, где
  3. Множество терминальных символов Σt = {ti}
  4. Множество подстановочных символов Σx = {xi}
  5. Скобки ’(’ и ’)’ и знак зяпятой ’,’
  6. Множество модельных функциональных символов Σf = {fi}

2.2 Термы (Terms)

Определим множество конкретных термов Tc :

И множество подстановочных термов Tv

Терм, принадлежащий Tv∕Tc будем называть термом со свободными переменными, для каждого терма T множество входящих в него подстановочных символов будем называть множеством свободных переменных этого терма и обозначать как v(T).

2.3 Операции (Operations)

Определим на нашей системе термов следующие модельные функции:

Правило переписывания это тройка: (X,tin,tout) где:

Семантика действия переписывания определяется следующим выражением:

apply(t,tin,tout) = subst(tout,free_unify(tin,t))

Расширим действия переписывания на множество правил:

apply(t,{r1...rn}) = {apply(t,r1)...apply(t,rn)}

и на множество свободных термов1 :

apply({t1...tn},R) = ∪apply(ti,R )

Естественно, само правило может быть представленно в виде терма: rule(vars,tin,tout) где:

Будем говорить, что множество термов x переписывается в множество термов y, если существует цепочка z1zn такая, что

z1 = x∧ zn = y ∧ ∀i ∈ {1...n}zn+1 ∈ apply(zn,R)

Наконец, будем говорить что множество термов T сходится относительно множества правил R если существует неподвижная точка уравнения:

Множество правил R называется сходящимся, относительно конечного множества термов T, если apply*(T,R) - конечно.

Множество правил обладает свойством нетеровости если

∀t ∈ T;r1,r2 ∈ Rapply(t,r1)! = apply(t,r2)∃R * ∈ R :
apply(apply(t,r1),R*) = apply(apply(t,r2),R*)∧ apply(t1,R*)

Таким образом мы приходим к широко известной теории переписывающих правил, с некоторыми отличиями от канонических формулировок:

Эти отличия не добавляют ничего существенного нового к математическим свойствам алгебры кроме того, что чисто технически с нею удобно работать.

2.4 Упорядоченные множества правил

Мы можем расширить семантику применения правил не ненетеровы системы, фиксируя порядок применения правил в несводимых критических парах. Т. е. правила p, s образуют критическую пару, если существует такой терм t, что apply(p,t)apply(s,t). Для сходящихся систем для любого терма t существует общая редукция apply(p,t) и apply(s,t). Однако много практически интересных вещей лучше описываются с помощью локально-неконфлюэнтных правил с фиксированным порядком применения.

Введем частичное упорядочивания переписывающих правил по ’степени конкретности’ их входных образцов. Будем писать t1ct2 когда t1 ’более конкретно’ чем t2. А что такое ’более конкретно’ ? - это означает что t1 может быть представлен как частичный случай t2, т. е. существует подстановка переменных s такая, что subst(t2,s) t1. Эквивалентное определение: t : free_unify(t,t1) free_unify(t,t2).

Далее, пусть p = (inp outp) и s = (ins outs) два правила, формирующие критическую пару. Мы говорим, что p cs if inpcins, и определим порядок применения как "более конкретный образец применяется первым", т. е.

              (
              {  apply(p,t)             p ≤c s
apply({p,s},t) =   apply(s,t)             s ≤c p
              (  ι{apply(p,t),apply(s,t)}  p ~c s
где ι – операторо недерменисткого выбора, зависящий от стратегии переписывания.

Легко показать что для каждого набора правил r1rn, где i,j : ij ⇒⁄ ri ~crj может быть построена эквивалентная система правил без ограничений на порядок применения.

2.5 Действия (Actions)

Следующий вопрос, который следует рассмотреть - это представление вычислений над термами. Обычный подход (множество правил, преобразующих входное множество термов в выходное) нас не устраивает, так как в реальном мире нам нужно несколько больше:

Примерами таких применений могут быть: набор правил для определения следуйщих действий в каком-либо бизнес-процессе, зависящий от переменных этого процесса, или процесс генерации кода, зависящий от конкретной архитектуры, или правила вывода, представляемые фактами в дедуктивной базе данных.

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

Терминальная машина это четверка: < S,E,ϕse > где:

Поведение терминальной машины определяется следующим преобразованием за единицу дискретного времени:

< S,E, X > - >< ϕs(X,E, S)|S,ϕe(ϕs(X,E, S)|Y)

(тут x|Y обозначает проекцию x на координату Y в обычном теоретико-множественном смысле).

Нижеприведенная диаграмма может быть более ясна для понимания.

          phi_s  
 <S,E,X> ----------> <S’,Y’>   phi_e  
    |                       ----------> E’  
    ---------------------E

2.6 Терминальная система со взаимодействием (term system with actions)

Какие изменения нам требуются внести для отражения требований операционной семантики в систему переписывания термов - просто добавить некоторый синтаксис взаимодействия со средой :

Пара вход/выход (X : x y) заменяется на четверку (X : (x,ein) (y,eout), где

Будем обозначать эту четверку как x[ein] y[eout]. Выражение x[ein] для терма t можно интерпретировать как сопоставление с образцом x при выполнении subst(ein,snd(free_unify(t,x))) (пусть snd(free_unify(t,x)) = s), y[eout] - как подстановка унификации в y и выполнения subst(eout,s).

3 Язык TermWare (Language)

Лексемы:

Синтаксис:

см. также BNF синтаксис

Полное описание встроенных систем содержиться в описании TermWareAPI

Примеры систем, определенных с помощью Языка TermWare:

 
System(BooleanAlgebra,default,  
ruleset(  
 $x && ($x => z) -> $z ,  
 not($x && $y) -> not($x) || not($y) ,  
 not($x || $y) -> not($x) && not($y) ,  
 $x && ($y || $z) -> ($x && $y) || ($x & $z) ,  
 not(not($x)) -> $x ,  
),  
FirstTop);  
 
System(BooleanLogic,general,  
 ruleset( import(BooleanAlgebra),  
          true => $x -> $x,  
          false => $x -> not($x),  
          true  || $x -> true,  
          false || $x -> $x,  
          true && $x -> $x,  
          false && $x -> false,  
          not(true) -> false,  
          not(false) -> true  
        ), FirstTop);  
 

Здесь, как вы видите все правила сокращенные (без действий и базы данных).

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

Поэтому ниже мы приведем терминальную систему “из реальной жизни” 2, а семантику фактов и действий опишем неформально:

System(BugFixing,DevelopmentProcess,  
 ruleset(  
 
 received($bug_id) -> check_confirmation($bug_id)  
                                 [ human_task(check_bug($bug_id)) ],  
 
 check_confirmation($bug_id) [ confirmed($tester,$bug_id) ]  
                          -> known($bug_id)  
                                 [ human_task(fix_bug($bug_id),  
                                               write_regression($bug_id)  
                                              ) ],  
 
 check_confirmation($bug_id) [ not_confirmed($tester,$bug_id) ]  
                          -> true [ send_not_confirmed($bug_id,$tester) ],  
 
 
 known($bug_id) [  
                  fixed($developer1, $bug_id) &&  
                  added_regression($developer2,$bug_id)  
                 ]  
                          -> true [ send_closed($bug_id,$developer1) ]  
 ),  
 FirstTop)

Этот пример описывает применение TermWare в системе организации бизнес-процессов. Как вы уже догадались, описываемый пример - обработка сообщения об ошибке в ПО.

Здесь база фактов (внешняя среда) может дать ответы на вопросы:

И воспринимать сообщения:

Обратите внимание на передачу в систему данных из внешнего мира с помощью пропозициональных выражений в условиях. Более подробно этот пример описан в [1]

3.1 Иерархическая система имен

С точки зрения организации программирования терминальных систем удобно использовать иерархический механизм именования, похожий на модули в idl, пространства имен в C++ или пакеты в Java.

В TermWare такой механизмы организации предоставляется термом domain. Синтаксис: domain(name,def1,defn), где defi - термы определения систем или поддоменов.

Пример:

domain(algebra,  
  System(Semigroup),  
  domain(LiGroups,  
    System ..  
  )  
)

Также реализована автоматическая загрузка определений систем из файлов: при интерпретации встроенных преобразований в любом контексте, где встречается полное имя системы (например:x.y.z, т. е. система с именем z, находящейся в домене x/y) автоматически загружается файл из соответствующего местоположения в файловой системе относительно свойства Java окружения termware.path. (в случае обращения к системе x.y.z будет сделана попытка чтения файла <termware.path>/x/y/z.def).

3.2 Встраиваемые парсеры других языков

Синтаксис TermWare, как таковой, не всегда удобен для ввода данных: иногда нам хочеться использовать более естественный проблемно-ориентированный язык для ввода исходной информации.

C этой целью TermWare предоставляет возможность расширения - пользователи могут добавлять синтаксические анализаторы своих языков, реализуя в своих классах Java интерфейсы IParser и IParserFactory и регистрируя имена этих классов в общем словаре.

4 Java API

4.1 Работа с термами

4.1.1 Term

Основная сущность TermWare - ITerm. (Описание API)

Как видите, Term это класс в котором определены:

В отличие от большинства систем компьютерной алгебры система термов тут построенна не “снизу-вверх”, от атомарных типов данных, а “сверху-вниз” - термом может быть объявлен любой класс, наследующийся от ITerm.

Естественно, существует предопределенный набор типов термов (описанный в формальной модели). Соответствующая диаграмма наследования:

 ITerm  
  |  
  *---AbstractPrimitiveTerm  
  |     |  
  |     *--AtomTerm  
  |     |  
  |     *--BooleanTerm  
  |     |  
  |     *--DoubleTerm  
  |     |  
  |     *--IntTerm  
  |     |  
  |     *--NILTerm  
  |     |  
  |     *--StringTerm  
  |  
  *---AbstractComplexTerm  
  |   |  
  |   *--SetTerm  
  |  
  *---XTerm  
  |  
  *---JTerm  

Однако с точки зрения программиста прямое использование этих классов не необходимо: лучше для этой цели воспользоваться интерфейсом ITermFactory.

4.1.2 TermFactory

TermFactory - класс, предоставляющий методы для создания термов. (Описание API)

Примеры использования:

 Term term=TermWare.getInstance().getTermFactory().createAtom("qqq");

Создаст

 TermFactory termFactory = TermWare.getInstance().getTermFactory();  
 Term term=termFactory.createComplexTerm3("f_3",  
                                  termFactory.createInt(3),  
                                  termFactory.createComplexTerm2("f",  
                                            termFactory.createAtom("a1"),  
                                            termFactory.createAtom("a2")  
                                                                 ),  
                                  termFactory.createX(1)  
                                                     );

создаст нам терм f3(3,f(a1,a2),x1) с одной свободной переменной x1.

4.1.3 ITermTransformer

Это просто преобразователь терма: (Описание API)

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

Как преобразователи термов связаны с правилами переписывания - очень просто: мы можем по правилу переписывания создать соответствующий преобразователь.

4.1.4 ITermRewritingStrategy

Наконец, стратегия переписывания: (Описание API) Это достаточно сложный объект, который содержит в себе набор правил (преобразователей термов) и алгоритм применения этих правил.

Конечный пользователь, как правило, не работает прямо с переписывающими стратегиями, но прикладные программисты могут создавать свои стратегии переписывания, наследуя свой класс от AbstractTermRewritingStrategy. (Описание API)

Само понятие стратегии заимствовано из APS [3], похожий подход принят в Stratego [2].

4.1.5 IFacts

IFacts (Описание API) - образ базы знананий терминальной системы, играющей роль внешней среды (или оракула) в нашей логике.

Что мы можем сделать с фактом:

Естественно, семантика базы знаний полностью определяется предметной областью, реализация создается отдельно для каждой задачи и может включать в себя запросы к реляционной БД либо к операторам ввода/вывода.

Правило вида x[condition] rule[action] интерпритируется следующим образом:

Одна реализация, с именем default определена непосредственно в библиотеке TermWare в классе DefaultFact.

Там методы check и set определены следующим образом: они интерпритируют логические и арифметические выражения и, если встречают функциональный символ, совпададающий с именем публичного метода своего класса, то вызывают этот метод, при необходимости производя преобразование типов входных аргументов, с помощью Java Reflection API.

Т. е. для того, что бы можно было вызывать методы БД фактов непосредственно из переписывающих правил, нужно просто унаследовать класс БД фактов от DefaultFacts (Описание API)

4.1.6 IEnv

Кроме “логической” внешней среды, определенной в логике у нас еще есть “программная” или “физическая” среда выполнения, которая определяет:

Эта среда инкапсулируестся в интерфейсе IEnv (Описание API)

4.1.7 TermSystem

Теперь мы можем сказать, что такое терминальная система: - это совокупность правил переписывания со стратегиями, базы данных фактов и интерфейса програмного окружения. (Описание API)

Зная все это мы можем определить и собственно операции преобразования термов: reduce.

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

Типичный код для создания терминальной системы выглядит следующим образом:

   IEnv env =  new SystemLogEnv();  
 
   ITermRewritingStrategy strategy=new TopDownStrategy();  
 
   IFacts facts=new AttributeFacts();  
 
   ITermSystem system=new ITermSystem(strategy,facts,env);

4.2 Воспомогательные классы

4.2.1 TermWare

TermWare - это просто синглетон для набора экзкмпляров.

4.2.2 TermWareInstance

Экземпляр TermWareInstance (Описание API) - это, образно говоря, стержень, который содержит в себе иерархическую систему доменов (см. класс Domain, (Описание API), метод getDomain() ), пользовательские словари имен парсеров языков и принтеров.

4.2.3 IParser, IParserFactory

С помощью этих интерфейсов определяется подключение к системе TermWare пользовательских разборщиков языков.

Общий паттерн использования следующий:

4.2.4 IPrinter, IPrinterFactory

Интерфейсы, определяющие подключение собственного вывода термов. Все точно так-же, как и в предыдущей части, только вместо входного потока у нас выходной. Описание API:

5 Перечень изменений

  1. 28.06.2007 - добавлено описание порядка выполнения критических пар.
  2. 28.03.2007 - добавлено описание внутреннего API. Приведен в соответствие с версией 2.0.0
  3. 08.10.2005 - приведен в соответствие с версией 2.0.RC0
  4. 07.03.2004 - косметические правки.
  5. 07.02.2004 - описана реализация БД фактов по умолчанию.
  6. 12.01.2003 - первая внешняя редакция.
  7. 06.11.2002 - первая внутренняя редакция.
  8. 20.06.2001 - создан.

References

[1]   Ruslan Shevchenko. Anatoliy Doroshenko. Managing business logic with symbolic computations. Lecture Notes in Informatics V. 30 - Proceeding of Information Systems Technology and its Applications 2003, pages 143–152, 2003.

[2]   Visser E. Stratego: A language for program transformation based on rewriting strategies. system description of stratego 0.5. Rewriting Techniques and Applications (RTA 01), 2051.:357–361, 2001.

[3]   J.V.Kapitonova A.A.Letichevsky M.S.L’vov and V.A.Volkov. Tools for solving problems in the scope of algebraic programming. LNCS, 958, 1995.