Многосортная логика

Иерархическая типизированная логика

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

Существуют различные способы формализовать указанное выше намерение; многосортная логика — это любой пакет информации, который ее выполняет. В большинстве случаев даны следующие:

• набор сортов, S
• соответствующее обобщение понятия подписи , позволяющее обрабатывать дополнительную информацию, поступающую с сортировками.

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

Пример

Рассуждая о биологических организмах, полезно различать два вида: и . В то время как функция имеет смысл, подобная функция обычно не имеет. Многосортная логика позволяет иметь термины типа , но отбрасывать термины типа как синтаксически неправильно сформированные. ${\displaystyle \mathrm {plant} }$ ${\displaystyle \mathrm {animal} }$ ${\displaystyle \mathrm {mother} \colon \mathrm {animal} \to \mathrm {animal} }$ ${\displaystyle \mathrm {mother} \colon \mathrm {plant} \to \mathrm {plant} }$ ${\displaystyle \mathrm {mother} (\mathrm {lassie} )}$ ${\displaystyle \mathrm {mother} (\mathrm {my\_favorite\_oak} )}$

Алгебраизация

Алгебраизация многосортной логики объясняется в статье Калейру и Гонсалвеша ^[1] , которая обобщает абстрактную алгебраическую логику на многосортный случай, но может также использоваться в качестве вводного материала.

Логика сортировки по порядку

Пример иерархии сортировки

В то время как логика многосортности требует, чтобы два различных сорта имели непересекающиеся наборы вселенных, логика упорядоченной сортировки позволяет объявить один сорт подсортом другого сорта , обычно с помощью записи или похожего синтаксиса. В приведенном выше примере биологии желательно объявить ${\displaystyle s_{1}}$ ${\displaystyle s_{2}}$ ${\displaystyle s_{1}\subseteq s_{2}}$

${\displaystyle {\text{dog}}\subseteq {\text{carnivore}}}$,

${\displaystyle {\text{dog}}\subseteq {\text{mammal}}}$,

${\displaystyle {\text{carnivore}}\subseteq {\text{animal}}}$,

${\displaystyle {\text{mammal}}\subseteq {\text{animal}}}$,

${\displaystyle {\text{animal}}\subseteq {\text{organism}}}$,

${\displaystyle {\text{plant}}\subseteq {\text{organism}}}$,

и т. д.; см. рисунок.

Везде, где требуется термин некоторого вида , вместо него может быть предоставлен термин любого подвида ( принцип подстановки Лисков ). Например, если предположить объявление функции и объявление константы , то термин будет совершенно допустимым и будет иметь вид . Чтобы предоставить информацию о том, что мать собаки — собака, в свою очередь, может быть выдано другое объявление; это называется перегрузкой функций , аналогично перегрузке в языках программирования . ${\displaystyle s}$ ${\displaystyle s}$ ${\displaystyle {\text{mother}}:{\text{animal}}\longrightarrow {\text{animal}}}$ ${\displaystyle {\text{lassie}}:{\text{dog}}}$ ${\displaystyle {\text{mother}}({\text{lassie}})}$ ${\displaystyle {\text{animal}}}$ ${\displaystyle {\text{mother}}:{\text{dog}}\longrightarrow {\text{dog}}}$

Логику с сортировкой по порядку можно перевести в несортированную логику, используя унарный предикат для каждой сортировки и аксиому для каждого объявления подсортировки . Обратный подход оказался успешным в автоматизированном доказательстве теорем: в 1985 году Кристоф Вальтер смог решить тогдашнюю эталонную задачу, переведя ее в логику с сортировкой по порядку, тем самым сведя ее на порядок, поскольку многие унарные предикаты превратились в сортировки. ^[2] ${\displaystyle p_{i}(x)}$ ${\displaystyle s_{i}}$ ${\displaystyle \forall x(p_{i}(x)\rightarrow p_{j}(x))}$ ${\displaystyle s_{i}\subseteq s_{j}}$

Чтобы включить логику сортировки по порядку в автоматизированную доказательную машину теорем на основе предложений, необходим соответствующий алгоритм объединения сортировки по порядку , который требует для любых двух объявленных сортов также объявить их пересечение : если и являются переменными сорта и , соответственно, уравнение имеет решение , где . ${\displaystyle s_{1},s_{2}}$ ${\displaystyle s_{1}\cap s_{2}}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{2}}$ ${\displaystyle s_{1}}$ ${\displaystyle s_{2}}$ ${\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}}$ ${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$ ${\displaystyle x:s_{1}\cap s_{2}}$

Смолка обобщил логику сортировки по порядку, чтобы разрешить параметрический полиморфизм . ^{[3] [4]} В его фреймворке объявления подсортировки распространяются на выражения сложного типа. В качестве примера программирования можно объявить параметрическую сортировку (с параметром типа, как в шаблоне C++ ), и из объявления подсортировки автоматически выводится отношение , что означает, что каждый список целых чисел также является списком чисел с плавающей точкой. ${\displaystyle {\text{list}}(X)}$ ${\displaystyle X}$ ${\displaystyle {\text{int}}\subseteq {\text{float}}}$ ${\displaystyle {\text{list}}({\text{int}})\subseteq {\text{list}}({\text{float}})}$

Шмидт-Шаус обобщил упорядоченно-отсортированную логику, чтобы разрешить объявления терминов. ^[5] Например, предполагая объявления подсортировки и , объявление термина типа позволяет объявить свойство сложения целых чисел, которое не может быть выражено обычной перегрузкой. ${\displaystyle {\text{even}}\subseteq {\text{int}}}$ ${\displaystyle {\text{odd}}\subseteq {\text{int}}}$ ${\displaystyle \forall i:{\text{int}}.\;(i+i):{\text{even}}}$

Смотрите также

• Философский портал

• Категориальная логика
• Логика_первого_порядка#Многосортная_логика

Ссылки

1. Карлос Калейро, Рикардо Гонсалвес (2006). «Об алгебраизации многосортных логик». Труды 18-й международной конференции по последним тенденциям в методах алгебраического развития (WADT) (PDF) . Springer. стр. 21–36. ISBN 978-3-540-71997-7.
2. Вальтер, Кристоф (1985). «Механическое решение парового катка Шуберта с помощью многосортного разрешения» (PDF) . Artif. Intell . 26 (2): 217–224. doi :10.1016/0004-3702(85)90029-3.
3. Смолка, Герт (ноябрь 1988 г.). «Логическое программирование с полиморфно упорядоченными типами». Международный семинар по алгебраическому и логическому программированию . LNCS. Том 343. Springer. С. 53–70.
4. Смолка, Герт (май 1989), Логическое программирование над полиморфно упорядоченными типами (кандидатская диссертация), Университет Кайзерслаутерн-Ландау , Германия
5. Шмидт-Шаус, Манфред (апрель 1988 г.). Вычислительные аспекты упорядоченно-сортированной логики с декларациями терминов . LNAI. Т. 395. Springer.

Ранние работы по многосортной логике включают в себя:

• Ван, Хао (1952). «Логика многосортных теорий». Журнал символической логики . 17 (2): 105–116. doi :10.2307/2266241. JSTOR  2266241., собранные в книге автора «Вычисления, логика, философия. Сборник эссе» , Пекин: Science Press; Дордрехт: Kluwer Academic, 1990.
• Гилмор, ПК (1958). «Дополнение к «Логике многосортных теорий»» (PDF) . Compositio Mathematica . 13 : 277–281.
• А. Обершельп (1962). «Untersuchungen zur mehrsortigen Quantorenlogik». Математические Аннален . 145 (4): 297–333. дои : 10.1007/bf01396685. S2CID  123363080. Архивировано из оригинала 20 февраля 2015 г. Проверено 11 сентября 2013 г.
• F. Jeffry Pelletier (1972). «Сортовая квантификация и ограниченная квантификация» (PDF) . Philosophical Studies . 23 (6): 400–404. doi :10.1007/bf00355532. S2CID  170303654.

Внешние ссылки

• «Многосортная логика», первая глава в сборнике лекций по процедурам принятия решений Калоджеро Дж. Зарбы