Многосортная алгебра

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

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

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

* каждому сорту "s " ∈ "S " интерпретация приписывает его носитель — множество "A_s " ⊆ "A " объектов сорта "s ", при этом каждому объекту алгебры должен быть приписан некоторый сорт (может быть, не один);
* каждому функциональному символу "f " типа "1,…,s_n,s_n+1> " интерпретация приписывает некоторую функцию "f_I " : A₁×…×A_n → A_n+1, где A_i — носитель сорта s_i. Функции могут быть частичными, то есть не всюду определёнными на "A₁×…×A_n ". В этом случае алгебра называется частичной. Если же все функции тотальны (то есть, всюду определены на "A₁×…×A_n "), алгебра называется тотальной.

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

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

Ω-термом сорта s называется любая переменная или константа сорта "s ", а также любое конечное (то есть, состоящее из конечного числа символов) выражение вида "f(t₁,…,t_n) ", где "f " ∈ "F ", "σ(f) = < s₁,…,s_n,s> " и "t_i " — Ω-терм сорта "s_i " для каждого 1 ≤ "i " ≤ n.

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

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

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

Ссылки

* [http://public.uic.rsu.ru/~skritski/scourses/Transl/ С.П.Крицкий. Трансляция языков программирования: синтаксис, семантика, перевод]