Реализация числа Пеано в Coq

Question

Я изучал основы программного обеспечения, чтобы изучить Coq, и застрял в Numbers. В этом определении типа

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

Как O становится 0 когда мы используем его в определении

Definition pred (n : nat) : nat :=
  match n with
    | O => O
    | S n' => n'
  end.

Я только понял что O представляет собой натуральные числа и S принимает натуральное число и возвращает другое натуральное число. Чего я не понимаю, так это когда наш nat тип данных используется в pred определение как O представлять 0? И как S n' скороговорка дает нам предшественника n,

Answer 1

Числа Пеано

nat представляет натуральные числа через унарную систему счисления. Жители (ценности) nat тип являются O, S O, S (S O), S (S (S O)),..., S (S (S (S ... O)...),

Мы интерпретируем символ O как натуральное число ноль. А также S представляет одну "галочку" в унарном представлении, т.е. мы интерпретируем S как конструктор (он не имеет ничего общего с объектно-ориентированным программированием), который принимает натуральное число и выдает следующее натуральное число.

Функция предшественника

pred на самом деле это не очень хорошая функция в некотором смысле.

Прежде всего, не существует предшественника нуля, когда мы говорим о натуральных числах. Но все функции в Coq должны возвращать значение, поэтому, если мы хотим сохранить тип pred (который nat -> nat) мы должны что-то сделать с pred O, Кажется естественным просто вернуться O и покончим с этим. Это дает нам первую ветвь выражения pattern-mathing (O => O).

Далее, что мы возвращаем, когда звоним pred на число, представляющее 1? Давайте вспомним, что мы пишем 1 в Coq как S O, Это просто -- pred (S O) должен вернуться O, Теперь давайте попробуем 2: pred (S (S O)) должен вернуться S O, Вы видите образец здесь? Если у нас есть куча Sперед Oмы раздеваемся S выкл - просто так. Вторая ветвь выражения сопоставления с образцом (S n' => n') делает именно это: он принимает (ненулевое) число вида S n' и превращает его в n' (без изменения оригинала, конечно).

Позвольте мне привести пример. Давайте вычислим предшественника числа 3 пошагово:

pred (S (S (S O)))

Разверните определение pred, замена S (S (S O)) за n:

match S (S (S O)) with
| O => O
| S n' => n'
end

S (S (S O)) имеет форму S n' (начинается с S), поэтому мы берем 2-ю ветку, привязку n' в S (S O), Как мы можем проверить, что мы здесь не ошиблись? Если мы подставим определение n' в S n' мы должны вернуть оригинал n: S n' знак равно S (S (S O)) знак равно n,

Теперь мы просто вернемся n':

S (S O)

Как и ожидалось, мы получили 2 в результате!

нотации

Есть различие между 0, 0, а также O, Первый ноль (0) - это цифра мета-уровня для натурального числа ноль (именно так мы обозначаем ноль в нашем метаязыке, например, в нашем случае английский). 0 это обозначение для O, другими словами 0 является синтаксическим сахаром для O, Как сказано в справочном руководстве Coq ( §1.2.4):

Числа не имеют определенной семантики в исчислении. Это простые обозначения, которые могут быть связаны с объектами посредством механизма обозначений (подробности см. В главе 12). Первоначально, цифры связаны с представлением Пеано натуральных чисел (см. 3.1.3).

Это легко проиллюстрировать:

Check 0.                     (* 0 : nat *)
Check 5.                     (* 5 : nat *)
Unset Printing Notations.    (* Print terms as is, no syntactic sugar *)
Check 0.                     (* O : nat *)
Check 5.                     (* S (S (S (S (S O)))) : nat *)

Вы можете перегрузить цифры, вот пример с целыми числами:

Set Printing Notations.
Require Import Coq.ZArith.ZArith.
Open Scope Z.
Check 0.                            (* 0 : Z *)
Check 5.                            (* 5 : Z *) 
Unset Printing Notations.
Check 0.                            (* Z0 : Z *)
Check 5.                            (* Zpos (xI (xO xH)) : Z *)

Upshot: одни и те же обозначения могут быть связаны с разными терминами. Coq определяет некоторые нотации по умолчанию, например, для таких вездесущих вещей, как числа.

Если вы хотите определить свой собственный тип для представления натуральных чисел (my_nat) с возможно разными именами для O а также S (лайк stop а также tick), вам нужно написать плагин для сопоставления чисел Coq с условиями my_nat (см. здесь).