Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

Определение [ править ]

Формально (односортированная) сигнатура может быть определена как тройка σ = ( S func , S rel , ar), где S func и S rel - непересекающиеся множества, не содержащие никаких других основных логических символов, которые называются соответственно

  • функциональные символы (примеры: +, ×, 0, 1) и
  • символы отношений или предикаты (примеры: ≤, ∈),

и функция ar: S func  S rel →, которая присваивает натуральное число, называемое арностью, каждой функции или символу отношения. Символ функции или отношения называется n -арным, если его арность равна n . Нулевой ( 0- мерный) функциональный символ называется постоянным символом . 

Сигнатура без функциональных символов называется реляционной сигнатурой , а сигнатура без символов отношения называется алгебраической сигнатурой . [1] конечная подписи является такой , что подпись S FUNC и S отн является конечными . В более общем смысле мощность сигнатуры σ = ( S func , S rel , ar) определяется как | σ | = | S func | + | S отн |.

Языком подпись является множеством всех хорошо сформированных предложений , построенных из символов в этой подписи вместе с символами в логической системе.

Другие соглашения [ править ]

В универсальной алгебре слово тип или тип подобия часто используется как синоним слова «подпись». В теории моделей сигнатуру σ часто называют словарем или отождествляют с языком L (первого порядка), которому она предоставляет нелогические символы . Однако мощность языка L всегда будет бесконечной; если σ конечно, то | L | будет ℵ 0 .

Поскольку формальное определение неудобно для повседневного использования, определение конкретной подписи часто сокращается неформальным образом, например:

«Стандартная сигнатура для абелевых групп - σ = (+, -, 0), где - унарный оператор».

Иногда алгебраическая подпись рассматривается как просто список арностей, например:

«Тип подобия абелевых групп равен σ = (2,1,0)».

Формально это определило бы функциональные символы подписи как нечто вроде f 0  (нулевой), f 1  (унарный) и f 2  (двоичный), но на самом деле обычные имена используются даже в связи с этим соглашением.

В математической логике очень часто символы не могут быть нулевыми, [ необходима цитата ], поэтому постоянные символы должны обрабатываться отдельно, а не как нулевые функциональные символы. Они образуют множество S const, не пересекающееся с S func , на котором функция арности arне определен. Однако это только усложняет дело, особенно при доказательствах индукцией по структуре формулы, когда необходимо рассматривать дополнительный случай. Любой символ нулевого отношения, который также не разрешен таким определением, может быть эмулирован символом унарного отношения вместе с предложением, выражающим, что его значение одинаково для всех элементов. Этот перевод не работает только для пустых структур (которые часто исключаются по соглашению). Если разрешены нулевые символы, то каждая формула логики высказываний также является формулой логики первого порядка .

Пример для бесконечной сигнатуры использует S func = {+} ∪ {f a : a ∈ F } и S rel = {=} для формализации выражений и уравнений о векторном пространстве над бесконечным скалярным полем F , где каждое f a обозначает унарная операция скалярного умножения на a . Таким образом, подпись и логика могут быть отсортированы по отдельности, причем сортировка выполняется только по векторам. [2]

Использование подписей в логике и алгебре [ править ]

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

В структуре , А.Н. интерпретация связь функции и символы отношений к математическим объектам , которые оправдывают их имена: Интерпретация из п -ичного символа функции F в структуру А с доменом А является функцией F A :  A п  →  A , и интерпретация n -арного символа отношения - это отношение R A  ⊆  A n . Здесь A n = A × A × ... × A обозначаетn -кратное декартово произведение области A на себя, поэтому f на самом деле является n -арной функцией, а R - n -арным отношением.

Многосортные подписи [ править ]

Для многосортированной логики и для многосортированных структур сигнатуры должны кодировать информацию о сортировках. Самый простой способ сделать это - использовать типы символов, которые играют роль обобщенных арностей. [3]

Типы символов [ править ]

Пусть S - некоторое (своего рода) множество, не содержащее символов × или →.

Типы символов над S - это определенные слова в алфавите : типы реляционных символов s 1 ×… × s n и функциональные типы символов s 1 ×… × s n → s ′ для неотрицательных целых чисел n и . (При n = 0 выражение s 1 ×… × s n обозначает пустое слово.)

Подпись [ править ]

Подпись (многосортная) - это тройка ( S , P , тип), состоящая из

  • своего рода набор S ,
  • набор P символов, и
  • тип карты , который ассоциируется с каждым символом в P A Тип символа над S .

Заметки [ править ]

  1. ^ Мокадем, Риад; Литвин, Витольд; Риго, Филипп; Шварц, Томас (сентябрь 2007 г.). «Быстрый поиск строки на основе nGram по данным, закодированным с использованием алгебраических подписей» (PDF) . 33-я Международная конференция по очень большим базам данных (VLDB) . Проверено 27 февраля 2019 . CS1 maint: обескураженный параметр ( ссылка )
  2. ^ Джордж Гретцер (1967). «IV. Универсальная алгебра». В Джеймсе С. Эбботе (ред.). Тенденции в теории решеток . Принстон / Нью-Джерси: Ван Ностранд. С. 173–210. CS1 maint: discouraged parameter (link) Здесь: с.173.
  3. ^ Многосортная логика , первая глава в конспектах лекции по процедурам принятия решений , написанная Калоджеро Г. Зарба .

Ссылки [ править ]

  • Burris, Stanley N .; Санкаппанавар, HP (1981). Курс универсальной алгебры . Springer . ISBN 3-540-90578-2. Бесплатное онлайн-издание .
  • Ходжес, Уилфрид (1997). Более короткая модельная теория . Издательство Кембриджского университета . ISBN 0-521-58713-1.

Внешние ссылки [ править ]

  • Стэнфордская энциклопедия философии : « Теория моделей » - Уилфред Ходжес .
  • PlanetMath: Запись « Подпись » описывает концепцию для случая, когда не вводятся никакие сортировки.
  • Бэйли, Джин , " Введение в алгебраическую спецификацию абстрактных типов данных ".