4.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.

На каждой строке этого примера вводится одно или несколько имен (до двоеточия) и специфицируется их тип (после двоеточия). Выделенное слово тип указывает, что введенные на данной строке имена обозначают какие-то типы данных. Выделенное слово функция обозначает некоторый тип функции, задающей отображение из области определения (аргументов) в область результата. Все остальные имена (true, false, zero, empty) будем называть константами. Для единства записи определений имен эти константы будем рассматривать как функции без аргументов. Заметим, что в приведенных определениях указываются только имена типов и ничего не сообщается, что они собой представляют (биты, ячейки, массивы или что-либо еще). Не приводятся также тела функций. Все это на данном (синтаксическом) уровне рассмотрения имен не имеет значения.

В соответствии с терминологией, принятой в математике, будем употреблять термин «основа» вместо «тип» и «знак операции» вместо «имя функции». Тогда можно ввести понятие сигнатуры , как пары  S,  , состоящей из множества S имен основ и множества  знаков операций, для каждого из которых указываются имена основ операндов и основы результата, например:

 {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} .

Основы и знаки операций выделены в отдельные множества, поэтому необходимость применения терминов «тип» и «функция» отпала. Второй компонент пары можно рассматривать как отображение различных последовательностей имен основ операндов и основы результата на множество знаков операций, что подчеркивается введением знака  вместо скобок. Это приводит к понятию I – индексированного семейства множеств. Будем считать, что I – индексированное семейства множеств – это функция из I в множества. Предположим для примера, что nat обозначает множество {0, 1, 2, …}. Тогда функция, отображающая 0 в {a, b}, 1 в {a, c, d}, 2 в пустое множество и т.д. представляет nat – индексированное семейство множеств букв, изображаемое кратко следующим образом: {a, b}₀, {a, c, d}₁, ₂, … . Теперь можно сказать, что второй компонент сигнатуры является по сути дела семейством множеств знаков операций, индексированных своей «арностью», т.е. своей последовательностью имен основ операндов и основы результата. Например, {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}.

Определение 1.1. Сигнатура  есть пара  S, , где S – множество (имен основ),  - (S^* S) – индексированное семейство множеств (знаков операций), а S^* - множество всех последовательностей элементов множества S (включая пустую последовательность).

Непосредственным следствием данного определения сигнатуры, важным для языков программирования, является то, что в одной сигнатуре (и тем более в разных) допускаются одинаковые имена знаков операций при условии их разной индексации (т.е. разных типов операндов и/или результатов). Например, {+}_{целое,целое,целое}, {+}_{вещественное,вещественное,вещественное}, {+}_{строка,строка,строка} и т.д.

Далее под обозначением  будет пониматься пара  S,  . Для двух сигнатур  и  ^ запись    ^ означает, что S  S^ и    ^. В этом случае  называется редуктом сигнатуры  ^, а  ^ - расширением сигнатуры . Совокупность основ и знаков операций, преобразующих  в  ^ будем называть  ^ - приращением сигнатуры .