abstract
| - Под многосортной алгеброй понимают некоторое множество объектов с определёнными на нём операциями (функциями). Объекты могут быть разнотипными, тогда каждому объекту приписывают так называемый сорт — некоторое имя (или символ), характеризующий тип объекта. Для работы с объектами используются термы — выражения, построенные из переменных и функций алгебры. Сигнатурой многосортной алгебры (то есть системой обозначений) называется тройка Ω = (S,F,σ), где S — множество сортов, F — множество функциональных символов, σ — типовая функция, приписывающая каждому функциональному символу его тип — список сортов всех аргументов и результата соответствующей функции. Таким образом, для каждого f ∈ F определён его тип σ(f) = 1,…,sn,sn+1>, где s1,…, sn — сорта аргументов, sn+1 — сорт результата функции f, n ≥ 0 — число аргументов функции, то есть её арность (говорят n-арная или n-местная функция). 0-арная функция называется константой. Ω-алгеброй называется пара (A,I), где A — множество объектов алгебры, её носитель, а I — интерпретация сигнатуры Ω на A:
* каждому сорту s ∈ S интерпретация приписывает его носитель — множество As ⊆ A объектов сорта s, при этом каждому объекту алгебры должен быть приписан некоторый сорт (может быть, не один);
* каждому функциональному символу f типа 1,…,sn,sn+1> интерпретация приписывает некоторую функцию fI : A1×…×An → An+1, где Ai — носитель сорта si. Функции могут быть частичными, то есть не всюду определёнными на A1×…×An. В этом случае алгебра называется частичной. Если же все функции тотальны (то есть, всюду определены на A1×…×An), алгебра называется тотальной. На одном носителе A можно определить множество Ω-алгебр. Если определенная интерпретация подразумевается, то будем обозначать алгебру (A,Ω), а если подразумевается и сигнатура, то обозначаем её просто A. Для определения понятия терм будем считать, что с каждым сортом s связано счётное множество символов Vs — переменных сорта s. Множество всех переменных обозначим V. Каждая переменная имеет только один сорт. Ω-термом сорта s называется любая переменная или константа сорта s, а также любое конечное (то есть, состоящее из конечного числа символов) выражение вида f(t1,…,tn), где f ∈ F, σ(f) = < s1,…,sn,s> и ti — Ω-терм сорта si для каждого 1 ≤ i ≤ n. Терм t, содержащий переменные x1,…,xk, будем обозначать t(x1,…,xk) или t(x). На каждой Ω-алгебре (A,I) такой терм определяет некоторую k-местную функцию. Пусть задана некоторая тотальная (то есть всюду определённая) функция γ: V → A такая, что γ(x) ∈ As, если x ∈ Vs. Эта функция называется оценкой (или интерпретацией) переменных на A. Значение терма t на Ω-алгебре (A,I) при оценке γ обозначается tI[γ] или tI(a1,…,ak), если t = t(x1,…,xk) и γ(xi) = ai. Оно определяется следующим образом (индекс I будем опускать):
* x[γ] = γ(x) для x ∈ V;
* c[γ] = cI, если определена интерпретация константы c;
* f(t1,…,tn)[γ] = fI (a1,…,an), если определены все значения ai = ti[γ];
* в противном случае значение терма не определено. В силу тотальности оценки значение любого Ω-терма на тотальной Ω-алгебре определено при любой оценке.
|