Многосортная логика - Many-sorted logic

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

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

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

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

Пример

Рассуждая о биологических организмах, полезно различать два вида: ${displaystyle mathrm {plant} }$ и ${displaystyle mathrm {animal} }$. Хотя функция ${displaystyle mathrm {mother} colon mathrm {animal} o mathrm {animal} }$ имеет смысл, аналогичная функция ${displaystyle mathrm {mother} colon mathrm {plant} o 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 { extit {dog}}subseteq { extit {carnivore}}}$,

${displaystyle { extit {dog}}subseteq { extit {mammal}}}$,

${displaystyle { extit {carnivore}}subseteq { extit {animal}}}$,

${displaystyle { extit {mammal}}subseteq { extit {animal}}}$,

${displaystyle { extit {animal}}subseteq { extit {organism}}}$,

${displaystyle { extit {plant}}subseteq { extit {organism}}}$,

и так далее.

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

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

Чтобы включить логику с сортировкой по порядку в автоматическое средство доказательства теорем на основе предложений, соответствующий упорядоченное объединение необходим алгоритм, требующий для любых двух объявленных сортов ${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}}$.

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

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

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

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

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

Рекомендации

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

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

• Ван, Хао (1952). «Логика разноплановых теорий». Журнал символической логики. 17: 105–116. Дои:10.2307/2266241., собранные в авторской Вычисление, логика, философия. Сборник сочинений, Пекин: Science Press; Дордрехт: Kluwer Academic, 1990.
• Гилмор, П. (1958). «Дополнение к» Логике разноплановых теорий."" (PDF). Compositio Mathematica. 13: 277–281.
• А. Обершельп (1962). "Untersuchungen zur mehrsortigen Quantorenlogik". Mathematische Annalen. 145 (4): 297–333. Дои:10.1007 / bf01396685. Архивировано из оригинал на 2015-02-20. Получено 2013-09-11.
• Ф. Джеффри Пеллетье (1972). «Сортировочная количественная оценка и ограниченная количественная оценка» (PDF). Философские исследования. 23: 400–404. Дои:10.1007 / bf00355532.

внешняя ссылка

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