Стандартные конструктивные определения целых, рациональных и действительных?

10

Натуральные числа определяются индуктивно как (используя синтаксис Coq в качестве примера)

Inductive nat: Set :=
| O: nat
| S: nat -> nat.

Существует ли стандартный способ конструктивного определения целых чисел (и, возможно, других множеств, таких как рациональные и действительные)?

Alex
источник
1
Что такое конструктивное определение?
Трисмегистос

Ответы:

12

Есть несколько способов определить математическую структуру, в зависимости от того, какие свойства вы считаете определением. Между эквивалентными характеристиками, какая из них вы принимаете за определение, а какая за альтернативную характеристику, не важна.

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

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

Например, чтобы определить , математик может быть доволен приравниванием разностей натуральных чисел: Z : = N 2 / { ( ( x , y ) , ( x , y ) ) x + y = x + у }Z

Zзнак равноN2/{((Икс,Y),(Икс',Y'))|Икс+Y'знак равноИкс'+Y}
Несмотря на то, что это выглядит аккуратно (без «того или иного»), для конструктивных рассуждений проще, если равенство объектов совпадает с равенством представлений, поэтому мы можем определить относительные целые числа как натуральное число или отрицание натуральное число минус один:
Inductive Z1 :=
  | Nonnegative : nat -> Z1   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Negative : nat -> Z1.     (* ⟦Negative x⟧ = -⟦x⟧-1 *)

Однако это определение странно асимметрично, что может сделать предпочтительным допустить два различных представления для нуля:

Inductive Z2 :=
  | Nonnegative : nat -> Z2   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Nonpositive : nat -> Z2.  (* ⟦Nonpostitive x⟧ = -⟦x⟧ *)

Или мы можем построить относительные целые числа, не используя натуральные числа в качестве строительного блока:

Inductive Pos3 :=
  | I : Pos3                  (* ⟦I⟧ = 1 *)
  | S3 : Pos3 -> Pos3         (* ⟦S3 x⟧ = ⟦x⟧+1 *)
Inductive Z3 :=
  | N3 : Pos3 -> Z3           (* ⟦N3 x⟧ = -⟦x⟧ *)
  | O3 : Z3                   (* ⟦O3⟧ = 0 *)
  | P3 : Pos3 -> Z3           (* ⟦P3 x⟧ = ⟦x⟧ *)

Стандартная библиотека использует Coq еще одно определение: он создает положительные целые числа от их обозначений является базой 2, как цифра 1 , за которым следует последовательность цифр 0 или 1. Затем он строит , Zкак Z3из Pos3выше. Это определение также имеет уникальное представление для каждого целого числа. Выбор использования двоичной записи делается не для упрощения рассуждений, а для создания более эффективного кода, когда программы извлекаются из доказательств.

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

NQN×N*=?=Q

Реальные числа - это совершенно другой котелок рыбы, потому что они не конструируемы. Невозможно определить действительные числа как индуктивный тип (все индуктивные типы являются счетными). Вместо этого любое определение действительных чисел должно быть аксиоматическим, то есть неконструктивным. Можно построить счетные подмножества действительных чисел; способ сделать это зависит от того, какое подмножество вы хотите построить.

Жиль "ТАК - перестань быть злым"
источник
1
В вычислимых действительных чисел , как представляется, наиболее разумным кандидатом, так как большинство использования действительных чисел связаны с их обычным упорядочением в некотором роде.
dfeuer
5
Что значит «конструктивный»? Я знаю только о «конструктивных множествах» в виде теории множеств, но теперь вы это имеете в виду. Кроме того, несмотря на то, что это реал, это совершенно другой котелок рыбы, это неправда, что «любое определение действительных чисел должно быть аксиоматическим, то есть неконструктивным». И в теории гомотопического типа существует более высокое индуктивно-индуктивное определение вещественных чисел.
Андрей Бауэр
15

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

Неверно, что все индуктивные типы являются счетными. Например, индуктивный тип

Inductive cow := 
   | nose : cow
   | horn : (nat -> cow) -> cow.

не является счетным, поскольку для любой последовательности, которую c : nat -> cowмы можем сформировать, horn cкоторая не входит в последовательность по обоснованности крупного рогатого скота. Если вы хотите правильно сформулировать форму «все индуктивные типы являются исчисляемыми», вы должны строго ограничить допустимые конструкции.

Вещественные числа не могут быть легко построены как индуктивный тип, за исключением того, что в теории гомотопического типа они могут быть построены как более высокий индуктивно-индуктивный тип , см. Главу 11 книги HoTT . Можно утверждать, что это обман.

Существует ряд конструктивных определений и конструкций действительных, вопреки утверждению Жиля. Их можно широко разделить на два класса:

  1. Конструкции типа Коши, в которых вещественные числа рассматриваются как метрическое пополнение рациональных чисел. Такая конструкция часто требует частных, хотя можно уйти с коиндуктивным определением, зависящим от того, как относиться к равенству. Наивное построение, как правило, также требует счетного выбора, но Фред Ричман дал процедуру завершения, которая работает конструктивно без выбора, см. Его Действительные числа и другие дополнения .

  2. λΣ

Что касается реализации, у нас есть различные конструктивные формализации реалов (но не те, что в стандартной библиотеке Coq, которые просто ужасны), например, сертифицированные компьютером Роберта Кребберса и Баса Спиттерса эффективные точные реалы в Coq .

Для фактической реализации точных действительных чисел я указываю на iRRAM Норберта Мюллера .

NN

Андрей Бауэр
источник
Вы можете предположительно аксиоматизировать теорию реальных замкнутых полей в Coq ...
Псевдоним
Да, вы могли бы, и Кирилл Коэн сделал это, см. Hal.inria.fr/hal-00671809v1/document . Какова ваша позиция?
Андрей Бауэр
1
У меня нет смысла, это была просто презумпция.
Псевдоним