Формализация теории конечных множеств в теории типов

10

Большинство помощников по доказательству имеют формализацию понятия «конечное множество». Эти формализации, однако, сильно отличаются (хотя можно надеяться, что все они по существу эквивалентны!). Что я не понимаю на данном этапе, так это пространство проектирования и каковы плюсы и минусы каждой формализации.

В частности, я хотел бы понять следующее:

  • Могу ли я аксиоматизировать конечные множества (т.е. типы, населенные конечным числом жителей) в простой теории типов? Система F? Каковы недостатки такого способа?
  • Я знаю, что это можно сделать «элегантно» в зависимо типизированной системе. Но с классической точки зрения полученные определения кажутся крайне чуждыми. [Я не говорю, что они не правы, это далеко не так!]. Но я тоже не понимаю, почему они «правы». Я понимаю, что они выбирают правильную концепцию, но более глубокую причину «говорить так» я не совсем понимаю.

По сути, я хотел бы получить аргументированное введение в пространство проектирования формализаций понятия «конечное множество» в теории типов.

Жак Каретт
источник

Ответы:

8

Я знаю, что это можно сделать «элегантно» в зависимо типизированной системе. Но с классической точки зрения полученные определения кажутся крайне чуждыми.

Можете ли вы объяснить, что вы подразумеваете под "чужой"? Мне кажется, что вы точно так же формализуете понятие конечного множества в теории типов и в теории множеств.

В теории множеств вы продолжаете, определяя множество как Затем вы определяете предикат конечности как: где означает изоморфизм множеств.Fin(n)

Fin(n){kN|k<n}
Finite(X)nN.XFin(n)
AB

В теории типов вы можете сделать то же самое! Обратите внимание, что является типом с элементами (поскольку второй компонент пары не имеет отношения к доказательствам). Затем вы можете определить конструктор типа конечности следующим образом: где означает изоморфизм типов.

Fin(n)Σk:N.ifk<nthenUnitelseVoid
Fin(n)n
Finite(X)Σn:N.XFin(n)
AB
Нил Кришнасвами
источник
Чужой, потому что я только когда-либо видел необработанные определения без сопровождающего теста, который объясняет, как читать эти определения. Плюс тот факт, что обычное определение Fin, сделанное индуктивно, затемняет вещи дальше. Ваше короткое объяснение - это то, что мне нужно, чтобы оно щелкнуло.
Жак Каретт
5

Дай посмотреть, смогу ли я добавить что-нибудь полезное к ответу Нила. «Пространство дизайна» для конечных множеств конструктивно намного больше, чем классически, потому что различные определения «конечного» не обязательно должны согласовываться конструктивно. Различные определения в теории типов дают несколько разные понятия. Вот несколько возможностей.

Конечные множества Куратовского ( -конечные) можно охарактеризовать как свободные -полрешетки: для данного множества, типа или объекта элементы свободной -полурешетки могут быть как конечные подмножества , Действительно, каждый такой элемент генерируется:KXK(X)X

  • нейтральный элемент , который соответствует пустому набору, или0
  • генератор , который соответствует синглтону , илиxX{x}
  • соединение из двух элементов, которое соответствует объединению.ST

Эквивалентная формулировка такова: является конечным тогда и только тогда, когда существует и сюръекция .K(X)SXKnN e:{1,,n}S

Если сравнить это с определением Нееля мы видим , что он требует биекция . Это равносильно тому, что мы принимаем те -конечные подмножества которые имеют разрешимое равенство: . Будешь использовать для сбора разрешим -конечных подмножеств .e:{1,,n}SKSXx,yS.x=yxyD(X)KX

Очевидно, что замкнуто относительно конечных объединений, но это не нужно быть замкнутым в конечных пересечениях. И не закрывается ни при каких операциях. Поскольку люди ожидают, что конечные множества ведут себя немного как «булева алгебра без вершины», можно также попытаться определить их как свободную обобщенную булеву алгебру ( , , и относительные дополнения ), но я на самом деле никогда слышал о таких усилиях.K(X)D(X)0

Решая, что такое «правильное» определение, вы должны обратить внимание на то, что вы хотите сделать с конечными множествами. И нет единого правильного определения. Например, в каком смысле «конечный» является множеством комплексных корней многочлена конечного ?

Видите Конструктивно конечно? Thierry Coquand и Arnaud Spiwack для подробного обсуждения конечности. Урок в том, что конечность конструктивно далека от очевидности.

Андрей Бауэр
источник
Да, я знал это достаточно, чтобы знать, что мой вопрос не был тривиальным. Теперь я могу перечитать части библиотек Coq, Isabelle и Agda, которые имеют дело с конечными наборами, и у меня есть надежда понять, какой выбор (каламбур) они сделали.
Жак Каретт
Интересно, насколько осведомлены авторы библиотек о выборе. Они, вероятно, просто вошли в одно из определений. Естественно предположить, что имеет разрешимое равенство, потому что тогда совпадает с и все идет гладко и во многом как в классическом случае. Проблема начинается, как только у нет решаемого равенства. AK(A)D(A)A
Андрей Бауэр
Чтобы быть справедливым, часто используют конечные множества для формализации аспектов верификации программы, и в этом случае вы обычно можете предполагать, что имеет место разрешимое равенство.
Коди