Contents

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

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

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

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

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

2.1 Алфавит (ABC)

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

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

2. Множество типизированных констант Σ_c^pt = {c_i^pt}, с каждой константой связанно значение, на множестве соответствующего примитивного типа, т. е. val : Σ_c^pt- > Dom^pt, где
   • Dom^{<PrimitiveType>} - множество примитивных типов, представляемое соответствующими константами
   • Dom^ATOM - множество атомарных неинтерпритируемых значений. Среди атомов выделим атом NIL, играющий специальную роль.
3. Множество терминальных символов Σ_t = {t_i}
4. Множество подстановочных символов Σ_x = {x_i}
5. Скобки ’(’ и ’)’ и знак зяпятой ’,’
6. Множество модельных функциональных символов Σ_f = {f_i}

2.2 Термы (Terms)

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

• ∀c_i Σ_c, c_i T_c
• ∀t Σ_t,∀r T_c⁺ = {T₁,…T_n} t(T₁,…T_n) T_c

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

• ∀t T_c{t T_v}
• ∀x Σ_x, x T_v
• ∀t Σ_t,r T_v⁺ = {T₁,…T_n} t(T₁,…T_n) T_v

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

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

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

• typename0 : T_v → INT, отображающий различные типы в различные целые константы.
• name : T_v → STRING
  • name(c_i) = STRING(c_i)
  • name(x_i) = STRING(x_i)
  • name(t_i(1₁,…r_n)) = STRING(t_i)
• arity : T_v → INT
  • arity(c_i) = 0
  • arity(x_i) = 0
  • arity(t(x₁,…x_n)) = n
• subterm : T_v ×{INT}→ T_v
  • ∀j {INT} : subterm(c_i,j) = NIL
  • ∀j {INT} : subterm(x_i,j) = NIL
  • ∀t T_v,j {INT} : j < 1 → subterm(t,j) = NIL
  • если считать, что на j-том месте находится подтерм t_j.
  • ∀t T_v,j {INT} : j >= arity(t) → subterm(t,j) = NIL
• equalT_v × T_v → BOOL (Введем для equal(x,y) сокращение x == y
  • c_i == c_j, если c_i и c_j представляют один и тот-же модельный объект.
  • x_i == x_j, всегда.
  • t₁(r₁,…,r_n) == t₂(q₁,…q_k), если t₁ и t₂ тот-же терминальный символ, r == n и ∀i 1…nr_i == q_i
• less : T_v × T_v → BOOL (Введем для less(x,y) сокращение x << y)
  • ∀x! = NIL,NIL << x
  • ∀c_i,c_j,typename(c_i) == typename(c_j) → c_i < c_j ⇔ c_i << c_j, где < - естественное упорядочивание модельной области.
  • ∀t₁,t₂ : typename0(t₁) = ′atom′,typename0(t₂)! = ′atom′t₁ << t₂
  • ∀t₁,t₂ : typename0(t₁) = ′string′,typename0(t₂)! = ′atom′ ∧ typename0(t₂)! = ′string′ : t₁ << t₂
  • ∀t₁,t₂ : typename0(t₁) = ′boolean′,typename0(t₂)! = ′atom′ ∧ typename0(t₂)! = ′string′∧ typename(0,t₂)! = ′boolean′ : t₁ << t₂
  • ∀t₁,t₂ : typename0(t₁) = ′int′,typename0(t₂)! = ′atom′ ∧ typename0(t₂)! = ′string′ ∧ typename0(t₂)! = ′boolean′ ∧ typename0(t₂)! = ′int′ : t₁ << t₂
  • ∀t₁,t₂ T_v : arity(t₁) < arity(t₂) → t₁ < t₂
  • ∀t₁(t₁1,…,t₁n),t₂(t₂1,…,t₂n) T_v,t₁.getName() < t2.getName() → t1 << t2
  • ∀t₁(t₁1,…,t₁n),t₂(t₂1,…,t₂n),T_v,t₁.getName() = t2.getName() : t₁1 << t₂1 → t1 << t2
  • ∀t₁(t₁1,…,t₁n),t₂(t₂1,…,t₂n),T_v,t₁.getName() = t2.getName() ∧ t₁1 = t₂1 : t₁(t₁2…t₁n) << t₂(t₂2…t₂n) → t1 << t2
  • ∀t₁,t₂ : t₁ == t₂ ⇔⁄ (t₁ << t2)∧⁄ (t₂ << t₁))

  т. е. множество термов просто частично-упорядоченно. Зачем - это позволяет нам выделить конструктор упорядоченного множества.

• set_n(t₁,…,t_n) - терм, обозначающий упорядоченное множестов из n элементов.
• Теперь мы можем определить fv(T_v) → T_v - множество свободных переменных t.
  • fv(c_i) = NIL
  • fv(x_i) = set₁(x_i)
  • fv(f(t₁,…,t_n)) = set(x_i) ∪ freeset(f(t₂,…,t_n))

  И fvi(x) - множество индексов термов.

• Каждый подтерм в терме однозначно идентифицируется последовательностью цифр - пути от головы терма. Т. е. существует subterm^* : T_v ×INT^*→ T_v
  • subterm^*(x_i,k) = NIL
  • subterm^*(c_i,k) = NIL
  • 
• Как обычно, подстановка свободных переменных - это множество пар (x_i,t_i), которые мы будем обозначать как substitution([x₁,t₁]…[x_n,t_n]) S В случае, когда это не будет вызывать неоднозначности, мы будем также обозначать ее как s([x₁,t₁]…[x_n,t_n]) или просто как s[x_i,t_i]
• Сам процесс подстановки subst(t,s) определяется следующим образом:
  • 
  • subst(NIL,s) = NIL
  • subst(c_i,s) = c_i
  • 
  • 
• Определим связную унификацию как bound_unify : T_v,×T_v ×S → T_v ×S - мы по существующей подстановке и двум термам получаем унификатор и уточненную подстановку.
  • bound_unify(NIL,x,S) = NIL
  • bound_unify(x,NIL,S) = NIL
  • 
  • bound_unify(x_i,t,S) = t,S ∧ [x_i,t]
  • bound_unify(t,x_i,S) = t,S ∧ [x_i,t]
  • bound_unify(x_i,x_j,S) = x_i,S ∧ [x_i,x_j]
  • 
• И несвязную унификацию как free_unify : T_v,×T_v → T_v × S - мы по двум термам получаем унификатор и уточненую подстановку, при этом предполагая, что термы не связаны общим набором переменных. т. е.
  • free_unify(t₁,t₂) = bound_unify(t₁,free_fv(t₂,fv(t₁)))
  • free_fv(c_i,(x₁…x_n)) = c_i
  • free_fv(x_i,(x₁…x_n)) =

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

• X = x_i - множество свободных переменных.
• t_in T_v входной терм, такой-что fv(t_in) = X
• t_out T_v выходной терм, такой-что fv(t_out) X

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

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

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

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

• vars - множество переменных, терм вида set(x₁,…x_n)
• t_in и t_out - соответственно входной и выходной термы.

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

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

• apply^*(T,R) = X : X = apply(X,R)

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

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

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

• мы работаем с множествами, а не с единичными термами - это уеличивает общность формулировок (например apply^*(X,R) существует всегда) за ту плату, что основное определение не конструктивно
• рефлексивные определения этого исчисление непосредственно встроенны в само исчисление.
• Операции работы с упорядоченными множествами включены непосредственно в исчисление термов, а не эмулируются набором нормализирующих правил, как обычно.

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

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

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

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

Далее, пусть p = (in_p → out_p) и s = (in_s → out_s) два правила, формирующие критическую пару. Мы говорим, что p ≤_cs if in_p≤_cin_s, и определим порядок применения как "более конкретный образец применяется первым", т. е.

Легко показать что для каждого набора правил r₁…r_n, где ∀i,j : i≠j ⇒⁄ r_i ~_cr_j может быть построена эквивалентная система правил без ограничений на порядок применения.

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

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

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

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

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

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

• S =< S_t,S_r > - состояние, пара из
  • S_t - множество термов.
  • S_r - множество активных правил переписывания.

  Заметим, что это разделение - довольно условно, так как правила переписывания представлены терминами специального вида.

• E - представление среды в системе
• ϕ_s : S × X × E → S × Y - функция преобразования системы.
• ϕ_e : E × Y - > E - функция реакции среды.

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

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

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

• ϕ_s - операция применения S_r к S_f в соответствии с некоторой стратегией, продуцирующая влияние на среду Y как побочный эффект. (с точки зрения программирования - операции вывода) Будем говорить, что система нормальна, если ϕ_s определяет неподвижную точку применения S_r к S_f
• ϕ_e - интерпритация env(y) окружающей средой.

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

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

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

• x, y - входной и выходной терм, как и раньше.
• e_in - запрос состояния среды.
• e_out - операция воздействия на среду.

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

3 Язык TermWare (Language)

Лексемы:

• Константы - числа и строки с обычной семантикой
• Переменные - $x
• Идентификаторы. -
• Конструкторы термов: f(x₀…x_n)
• Set-Образцы : термы вида set_pattern(