Добавил:
Upload Опубликованный материал нарушает ваши авторские права? Сообщите нам.
Вуз: Предмет: Файл:
A04_Types.doc
Скачиваний:
5
Добавлен:
12.11.2019
Размер:
376.32 Кб
Скачать

Контрольные вопросы

1) Что такое алгебра слов и как она конструируется?

2) Чем характерна алгебра на множестве переменных и чем она отличается от обычной алгебры слов?

3) Сформулируйте определение терма алгебры слов.

4.4. Теории

Пусть имеется сигнатура = S, . Тогда сигнатуре можно сопоставить две различные алгебры А и А, с носителями, соответственно,А , А и функциями сопоставления us, us для каждого символа операции. В общем случае таких алгебр может быть бесчисленное множество. Различные алгебры одной и той же сигнатуры получили название подобных алгебр.

При наличии множества подобных алгебр естественно возникает необходимость выделения среди них таких алгебр, которые отвечают требованиям полезности, отвечают определенным законам. Эти законы могут быть выражены в виде равенств. Равенство на множестве переменных в данной сигнатуре представляет собой не что иное, как пару термов с переменными. Например, равенство plus(x, y) = plus(y, x) на множестве переменных {x, y} может рассматриваться как тройка {x, y}, plus(x, y), plus(y, x).

Определение 1.4. - равенство – это тройка Х, t1, t2, где Х есть S – индексированное множество (переменных), а t1, t2W (X) суть термы одной основы на множестве (переменных) Х (обычно уравнение имеет вид: «для всех Х, t1 = t2»).

Равенства дают основу для классификации алгебр. Если в алгебре выполняется, скажем, равенство e1(x, y) = e2(x, y), то это означает, что, каковы бы ни были значения, приданные переменным x и y, вычисление выражения левой части дает тот же результат, что и вычисление выражения правой части. Таким образом, если А есть алгебра и v : {x, y} A есть функция привязки переменных, тогда требуется, чтобы расширение v # этой функции подчинялось закону v #(e1(x, y)) = v #(e2(x, y)).

Пусть теперь Е будет множеством равенств. Некоторая алгебра называется моделью Е, если она удовлетворяет каждому из равенств Е. Множество всех моделей будем обозначать Е*.

При наличии некоторого множества моделей мы можем рассматривать множество равенств, выполняющихся в каждой модели этого множества. Обозначим через Е** такое множество равенств. Е** называется замыканием Е.

Рассмотрим пример теории:

основы {государственное_лицо};

операции {президент, хранитель_ядерного_чемоданчика: государственное_лицо};

равенства {президент = хранитель_ядерного_чемоданчика }.

Если в государстве есть президент и если государство обладает ядерным оружием, то всегда можно построить модель, в которой указанное равенство выполняется. Следовательно, в этом случае мы имеем множество моделей Е* и замыкание Е**множества равенств.

Рассмотрим еще один пример:

основы {должностное_лицо};

операции {начальник_отдела, главный_инженер, главный_конструктор: должностное_лицо};

равенства {начальник_отдела = главный инженер, главный_инженер = главный_конструктор}.

Предположим теперь, что имеются алгебры с различными значениями для указанных констант (примером такой алгебры может служить малое предприятие с сотрудниками Иванов, Петров, Сидоров и т.д.). В тех алгебрах, в которых начальник_отдела и главный инженер имеют одно и то же значение, а главный_инженер и главный_конструктор также имеют одно и то же значение, выполняются приведенные равенства. Но если в алгебре выполняется данная пара равенств, то в ней выполняется и равенство начальник_отдела = главный_конструктор.

Если мы выделим из всего множества предприятий такие, в которых предусматривается совмещение рассмотренных должностных обязанностей, то на этом подмножестве мы будем иметь модель Е*

и замыкание Е**. В общем случае замыкание в этом примере не существует. В этом и заключается смысл введения равенств: получение полезных подмножеств.

Сигнатура с множеством равенств называется представлением.

Определение 1.5. Представление – это пара , Е, где есть сигнатура, а Е - множество равенств.

Определение 1.6. Теория – это такое представление , Е, в котором Е замкнуто.

Будем обозначать Т Т , если  и Е Е. В этом случае Т называется редуктом теории Т, а Т - расширением Т. Совокупность основ, знаков операций и равенств, преобразующих Т в Т, будем называть Т - приращением теории Т.

Следует обратить внимание, что теория и представление являются синтаксическими объектами, в то время как алгебры – это уже семантические объекты. У каждой теории может быть несколько удовлетворяющих ей алгебр.

В качестве примера рассмотрим теорию множества натуральных чисел, соответствующую приведенной в разделе 1.1 сигнатуре:

основы: {bool, nat, setofnat};

операции: {true, false : bool;

not : bool bool;

or, and : bool, bool bool;

zero : nat;

succ : nat nat;

, : nat, nat bool;

empty : setofnat;

insert : setofnat, nat setofnat;

has : setofnat, nat bool};

равенства: { not(true) = false;

not(false) = true;

p : bool and(false, p) = false;

and(true, p) = p;

or(false, p) = p;

or(true, p) = true;

m, n : nat zero n = true;

succ(m) zero = false;

succ(m) succ(n) = m n;

m n = and(m n, n m);

x, y : nat, s : setofnat

has(empty, x) =false;

has(insert(s, x), y) = or(x y, has(s, y)) }.

Алгебрами данной теории будут все алгебры, в которых выполняется каждое из приведенных равенств. Заметим, что вследствие ограничений, накладываемых равенствами, множество этих алгебр будет уже, чем множество алгебр соответствующей сигнатуры. Алгебры некоторой теории часто называют моделями этой теории.

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

Соседние файлы в предмете [НЕСОРТИРОВАННОЕ]