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

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

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

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

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

Пример

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

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

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

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

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

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

{\ displaystyle {\ textit {собака}} \ substeq {\ textit {carnivore}}}

,

{\ Displaystyle {\ textit {собака}} \ substeq {\ textit {млекопитающее}}}

,

{\ displaystyle {\ textit {carnivore}} \ substeq {\ textit {животное}}}

,

{\ displaystyle {\ textit {млекопитающее}} \ substeq {\ textit {животное}}}

,

{\ Displaystyle {\ textit {животное}} \ substeq {\ textit {организм}}}

,

{\ Displaystyle {\ textit {растение}} \ substeq {\ textit {организм}}}

,

и так далее; ср. картина.

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

Логика с сортировкой по порядку может быть преобразована в логику без сортировки, используя унарный предикат для каждой сортировки и аксиому для каждого объявления подсортировки . Обратный подход оказался успешным в автоматическом доказательстве теорем: в 1985 году Кристоф Вальтер смог решить тогдашнюю задачу эталонного теста, переведя ее в логику с упорядоченной сортировкой, тем самым уменьшив ее на порядок, поскольку многие унарные предикаты превратились в сортировки. ${\ Displaystyle p_ {я} (х)}$ ${\ displaystyle s_ {i}}$ ${\ Displaystyle \ forall x (p_ {i} (x) \ rightarrow p_ {j} (x))}$ ${\ displaystyle s_ {i} \ substeq 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 \ {х_ {1} = х, \; х_ {2} = х \}}$ ${\ displaystyle x: s_ {1} \ cap s_ {2}}$

Обобщенная логика Smolka с сортировкой по порядку для параметрического полиморфизма . В его структуре объявления подсортировки распространяются на сложные выражения типов. В качестве примера программирования, параметрического рода может быть объявлен (с является параметром типа , как в шаблоне C ++ ), а также из декларации subsort отношения автоматически выводится, а это означает , что каждый список целых чисел также список поплавков. ${\ Displaystyle {\ textit {список}} (X)}$ ${\ displaystyle X}$ ${\ displaystyle {\ textit {int}} \ substeq {\ textit {float}}}$ ${\ displaystyle {\ textit {список}} ({\ textit {int}}) \ substeq {\ textit {list}} ({\ textit {float}})}$

Schmidt-Schauß обобщенная логика упорядоченной сортировки, позволяющая декларировать термины. В качестве примера, предполагая объявления подсортировки и , объявление термина, например, позволяет объявить свойство целочисленного сложения, которое не может быть выражено обычной перегрузкой. ${\ Displaystyle {\ textit {даже}} \ substeq {\ textit {int}}}$ ${\ displaystyle {\ textit {odd}} \ substeq {\ textit {int}}}$ ${\ displaystyle \ forall i: {\ textit {int}}. \; (i + i): {\ textit {even}}}$