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

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

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

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

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

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

Пример

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

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

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

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

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

{\text{dog}}\subseteq {\text{carnivore}}

,

{\text{dog}}\subseteq {\text{mammal}}

,

{\text{carnivore}}\subseteq {\text{animal}}

,

{\text{mammal}}\subseteq {\text{animal}}

,

{\text{animal}}\subseteq {\text{organism}}

,

{\text{plant}}\subseteq {\text{organism}}

,

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

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

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

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

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

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

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

Ссылки

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

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

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

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