1.4. Алгебра термов

Многосортные алгебры.

Под алгеброй понимают некоторое множество объектов с определёнными на нём операциями (функциями). Объекты могут быть разнотипными, тогда каждому объекту приписывают так называемый сорт - некоторое имя (или символ), характеризующий тип объекта. Для работы с объектами используются термы - выражения, построенные из переменных и функций алгебры. Дадим точные определения.

Сигнатурой алгебры (т.е. системой обозначений) называется тройка W = (S,F,s), где S - множество сортов, F - множество функциональных символов, s  - типовая функция, приписывающая каждому функциональному символу его тип - список сортов всех аргументов и результата соответствующей функции. Таким образом, для каждого f О F определён его тип s(f) = < s₁,...,s_n,s_n+1>, где s₁, ..., s_n - сорта аргументов, s_n+1 - сорт результата функции f, n ³ 0 - число аргументов функции, т.е. её арность (говорят n-арная или n-местная функция). 0-арная функция называется константой.

W-алгеброй называется пара (A,I), где A - множество объектов алгебры, её носитель, а I  - интерпретация сигнатуры W на A:

• каждому сорту s О S интерпретация приписывает его носитель - множество A_s Í A объектов сорта s, при этом каждому объекту алгебры должен быть приписан некоторый сорт (может быть, не один); 
• каждому функциональному символу f типа < s₁,...,s_n,s_n+1> интерпретация приписывает некоторую функцию f_I : A₁ґ...ґA_n ® A_n+1, где A_i - носитель сорта s_i. Функции могут быть частичными, т.е. не всюду определёнными на A₁ґ...ґA_n. В этом случае алгебра называется частичной. Если же все функции тотальны (т.е., всюду определены на A₁ґ...ґA_n), алгебра называется тотальной.

На одном носителе A можно определить множество W-алгебр. Если определенная интерпретация подразумевается, то будем обозначать алгебру (A,W), а если подразумевается и сигнатура, то обозначаем её просто A.

Для определения понятия терм будем считать, что с каждым сортом s связано счётное множество символов V_s - переменных сорта s. Множество всех переменных обозначим V. Каждая переменная имеет только один сорт.

W-термом сорта s называется любая переменная или константа сорта s, а также любое конечное (т.е., состоящее из конечного числа символов) выражение вида f(t₁,...,t_n), где f О F, s(f) = < s₁,...,s_n,s > и t_i - W-терм сорта s_i для каждого 1 Ј i Ј n. 

Терм t, содержащий переменные x₁, ..., x_k, будем обозначать t(x₁,...,x_k) или t(x). На каждой W-алгебре  (A,I) такой терм определяет некоторую k-местную функцию. Пусть задана некоторая тотальная (т.е. всюду определённая) функция g: V ® A такая, что g(x) О A_s, если x О V_s. Эта функция называется оценкой (или интерпретацией) переменных на A. Значение терма t на W-алгебре (A,I) при оценке g обозначается t_I[g] или t_I(a₁,...,a_k), если t = t(x₁,...,x_k) и g(x_i) = a_i. Оно определяется следующим образом (индекс I будем опускать):

• x[g] = g(x) для x О V;
• c[g] = c_I , если определена интерпретации константы c;
• f(t₁,...,t_n)[g] = f_I (a₁,...,a_n), если определены все значения a_i = t_i[g];
• в противном случае значение терма не определено.

В силу тотальности оценки значение любого W-терма на тотальной W-алгебре определено при любой оценке.

Алгебры термов.

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

Обычно используются алгебры термов. Носителем такой алгебры являются термы определённых сортов, а её операциями - функции, образующие сложные термы из более простых. Эти операции называются конструкторами. Перейдём к точным определениям.

Алгебра термов почти полностью определяется её сигнатурой W = (S,F,s), которая должна удовлетворять следующим условиям:

• S = S_p И S_c, где S_p - множество первичных сортов, S_c - множество конструируемых сортов,  S_p З S_c = Ж ;
• F - множество конструкторов; если f О F и s(f) = < s₁,...,s_n,s >, то s₁,..., s_n О S, а s О S_c; при этом f называется конструктором сорта s.

Для полного задания W-алгебры термов необходимо ещё задать носители первичных сортов A_s для всех s О S_p (если S_p № Ж ). Предполагается, что каждый объект первичного сорта добавляет в W соответствующую константу того же сорта, которая может использоваться для образования термов конструируемого сорта. 

Носитель любого конструируемого сорта s О S_c есть множество T_s основных термов сорта s, т.е. термов сорта s, состоящих только из объектов первичных сортов и конструкторов из F. Переменных и других функций основные термы не содержат. 

Операции алгебры (соответствующие конструкторам) определяются следующим образом. Пусть f О F, тогда:

• если s(f) = < s >, то значением константы f является основной терм f;
• если s(f) = < s₁,...,s_n,s > и для каждого 1 Ј i Ј n задан t_i - основной терм сорта s_i, то значением операции f от термов t₁,...,t_n является основной терм f(t₁,...,t_n).

Из данного определения непосредственно следует

У т в е р ж д е н и е  1.10. 

• Алгебра термов тотальна.
• Каждый основной терм конструируемого сорта однозначно определяет конструктор, значением которого он является, и его аргументы.

Ђ

Пример 1.5. Натуральные числа:

первичных сортов нет;
N - конструируемый сорт натуральных чисел;
0 - константа сорта N (нуль);
S - конструктор типа < N,N >, образующий следующее число.

Число  n > 0 представляется термом S(...S(0)...), где S повторяется n раз.
Ђ

Пример 1.6. Последовательности:

E - первичный сорт элементов последовательности;
Q - конструируемый сорт последовательностей;
[] - константа сорта Q (пустая последовательность);
[_|_] - конструктор типа < E,Q,Q >, присоединяющий элемент к началу (голове) последовательности.

Последовательность < e₁,e₂,e₃ > представляется термом [e1|[e2|[e3|[]]]]. Вместо [e1|[e2|...]] разрешается писать [e1,e2|...], а также разрешается опускать |[] в конце списка. Тогда получим запись [e1,e2,e3].
Ђ

Пример 1.7. Списки:

E - первичный сорт элементов, не являющихся списками;
L - конструируемый сорт списков;
[] - константа сорта L (пустой список);
[_|_]1 - конструктор типа < E,L,L >, присоединяющий элемент к голове списка.;
[_|_]2 - конструктор типа < L,L,L >, присоединяющий список в качестве элемента к голове списка.

Разрешается опускать индексы конструкторов, а также применять сокращения, используемые для последовательностей. Тогда список < e₁,< >,<e₂,e₃> > представляется термом [e1,[],[e2,e3]]. 
Ђ

Алгоритм унификации.

В алгебре термов часто возникает задача решения уравнения  t₁ = t₂ (или даже системы таких уравнений), где t₁, t₂ - термы, возможно содержащие переменные. Под решением понимаются такие значения переменных, при которых термы t₁ и t₂ становятся одинаковыми, унифицированными. Например, в алгебре списков уравнение [e1,X,[e2,Y]]=[X|Z] имеет решение X=e1, Z=[e1,[e2,Y]]. Дадим точную формулировку задачи.

Подстановкой называется система уравнений вида

q = {x₁ = u₁, ..., x_n = u_n},

где x_i  - переменные, u_i  - термы, не содержащие переменных x₁, ..., x_n. Такая подстановка определяет переменные x₁, ..., x_n. Будем рассматривать также пустую подстановку { }.

Пусть q - произвольная система уравнений (возможно, пустая) или терм. Обозначим qq  результат применения подстановки q  к q, т.е. результат замены в q всех вхождений каждой переменной x_i на соответствующий терм u_i. Пусть q  и  q ' - подстановки. Очевидно, что qq ' будет снова подстановкой, если переменные, определяемые подстановкой q, не входят в q '.

Подстановка называется решением (или унификатором) системы уравнений E, если Eq  является тождеством, т.е. выполняется при любых значениях переменных в данной алгебре. Решение q  называется наиболее общим (НОР), если любое другое решение получается из q  применением некоторой подстановки q '. Предыдущий пример решения является наиболее общим.

Т е о р е м а  1.3. Система уравнений имеет решение тогда и только тогда, когда она имеет НОР. Следующий алгоритм находит НОР, если решение существует, в противно случае сообщает об отсутствии решения.

Алгоритм 1.2 (унификации). Система уравнений E решается рекурсией по структуре системы.

1. E имеет вид {t = t}. НОР={ }.
2. E имеет вид {x = t}, где t не содержит x. НОР={x = t}.
3. E имеет вид {x = t}, где t содержит x, но не совпадает с x. Решения не существует, т.к. для любой подстановки q  термы xq  и tq  имеют разную длину.
4. E имеет вид {f(t₁,...,t_n) = g(s₁,...,s_m)}. Она имеет решение тогда и только тогда, когда f = g и, следовательно, n = m, а также имеет решение система E' = {t₁ = s₁, ..., t_n = s_n}. При этом НОР E и E' совпадают. 
5. E имеет вид {t = s}И E', где E'  - непустая система уравнений. НОР E равен qq ' И q ', где q  есть НОР уравнения t = s, а q ' есть НОР системы E'q.

Доказательство. Остаётся доказать, что алгоритм никогда не зацикливается. Зациклиться он может из-за того, что на шаге 4 увеличивает число уравнений, а на шаге 5, при переходе от системы E' к системе E'q, удлиняет уравнения (в случае непустой подстановки q ). Но зацикливания не происходит, т.к. на шаге 4 уменьшается общее число символов в системе уравнений, а на шаге 5 при непустой q  уменьшается число переменных в системе, а при пустой подстановке система E' не меняется (при переходе от E к E' число символов уменьшается) . Таким образом, при решении системы число её переменных монотонно уменьшается (число символов в уравнениях может при этом возрастать), а в промежутках между изменением числа переменных монотонно уменьшается число символов в системе, что в конечном итоге приводит к завершению алгоритма.
Ђ

Машины Тьюринга.

Машины Тьюринга представляют собой простой формально определённый рекурсивно полный класс алгоритмов (это недоказуемое утверждение называется тезисом Чёрча-Тьюринга). Каждая машина Тьюринга представляет один алгоритм. Она состоит из 

• ленты - конечной последовательности ячеек, в каждой из которых записано по одному символу некоторого конечного алфавита S, 
• головки - устройства, которое в каждый момент обозревает некоторую ячейку, может находиться в одном из конечного множества состояний Q, читать и писать символ в обозреваемой ячейке, перемещаться вдоль ленты и добавлять при необходимости к её концам новые ячейки,
• программы - конечного множества правил P, управляющих поведением головки.

Машина Тьюринга

Правило имеет вид (q,a) ® (q',a',S), где q и q' - состояния, a и a' - символы алфавита, S - сдвиг головки, принимающий значение L (сдвиг влево на одну ячейку), R (сдвиг вправо на одну ячейку) или N (отсутствие сдвига). Правило может применяться, когда головка находится в состоянии q и обозревает ячейку с символом a. Если оно применяется, то головка переходит в состояние q', в обозреваемую ячейку записывается символ a', а затем выполняется сдвиг S. Если сдвиг невозможен из-за выхода за границу ленты, то к ней с соответствующей стороны добавляется ячейка с записанным в неё специальным символом LОS . Множество состояний обязательно содержит одно начальное состояние q₀ и одно заключительное состояние q_f. При этом предполагается, что для каждой пары (q,a), где q № q_f, в P есть хоть одно правило, а для q_f нет ни одного правила. Таким образом, машина Тьюринга останавливается тогда и только тогда, когда она попадает в заключительное состояние.

Конфигурацией машины Тьюринга называется цепочка вида aqab, где aab - содержимое ленты, q - текущее состояние головки, а её позиция указывает обозреваемую ячейку между a и b (см. рисунок). Предполагается, что начальная конфигурация всегда имеет вид q₀ab, т.е. головка в этих конфигурациях всегда сдвинута к левому концу ленты.

Формально, машина Тьюринга определяется набором M = (S,Q,P,q₀,q_f), где
S = {L,a₁,...,a_n} - конечный ленточный алфавит, n ³ 1,
Q = {q₀,...,q_f} - конечное множество состояний,
P Í QґSґQґSґS, где S = {L,R,N}, - множество правил, записываемых в виде (q,a) ® (q',a',S), где (q,a) принимает все значения из (Q \ {q_f})ґS  и только такие значения,
q₀, q_f - начальное и заключительное состояния, соответственно,
K = {aqb | qОQ, aОS ^*, bОS ⁺} - множество конфигураций (обозначения S ^* и S ⁺ см. в п. 2.1),
I = {q₀a | aОS ⁺} - множество начальных конфигураций.
Отношение перехода T Í KґK формально определяется следующим образом:
если q,q'ОQ, a,a',bОS, a,bОS ^*, то
правилу (q,a) ® (q',a',N) соответствует переход aqab ®_T aq'a'b ,
правилу (q,a) ® (q',a',L) соответствуют переходы abqab ®_T aq'ba'b  (для всех b) и qab ®_T q'La'b,
правилу (q,a) ® (q',a',R) соответствуют переходы aqabb ®_T aa'q'bb  (для всех b) и aqa ®_T aa'q'L.

На самом деле, рекурсивно полным будет класс всех машин Тьюринга с произвольным фиксированным алфавитом S, например, с S = {L,1}. Разные алфавиты мы используем только для удобства программирования.

Назовём L-выходом (выходом с пустым входом) машины Тьюринга любую цепочку a = bg, не начинающуюся и не кончающуюся символом L, если есть вычисление q₀L ®_T^* L^mb q_f g Lⁿ (m, n ³ 0). С помощью тезиса Чёрча-Тьюринга можно доказать следующее утверждение (доказательство опускаем).

У т в е р ж д е н и е  1.9. Пусть задан произвольный конечный алфавит A. Произвольное множество цепочек B в алфавите A рекурсивно перечислимо тогда и только тогда, когда оно совпадает с множеством L-выходов некоторой машины Тьюринга.

Очевидно, что при |B|>1 машина должна быть недетерминированной.

Пример 1.4. Пусть A = {a, b}. Множество A^* всех цепочек в алфавите A рекурсивно перечислимо, т. к. совпадает с множеством L-выходов машины Тьюринга с правилами

(q₀,L) ® (q₀,a,R),
(q₀,L) ® (q₀,b,R),
(q₀,L) ® (q_f ,L,N).

Вычисление для такой машины имеет вид q₀L ® aq₀L ® abq₀L ® abbq₀L ® abbq_f L.
Ђ

Машины Тьюринга дают ещё классические примеры нерекурсивных множеств. Ограничимся классом машин с одним фиксированным ленточным алфавитом. Рассматривая программу машины как последовательность символов, можно закодировать её в этом ленточном алфавите и подать на вход любой машине из этого класса. Точно также можно программу машины подать на вход ей самой. Машина, для которой её собственная программа является допустимым входом, называется самоприменимой. В противном случае она называется несамоприменимой. Известно, что множество самоприменимых машин Тьюринга нерекурсивно, но рекурсивно перечислимо, а множество несамоприменимых машин не является рекурсивно перечислимым (и, следовательно, нерекурсивно). Таким образом, проблемы самоприменимости и несамоприменимости машин Тьюринга неразрешимы (но в разной степени)..