Что такое конструктор в Coq?

Question

У меня проблемы с пониманием принципов того, что такое конструктор и как он работает.

Например, в Coq нас учили определять натуральные числа следующим образом:

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

И мне сказали, что S это конструктор, но что именно это означает?

Если я тогда сделаю:

Check (S (S (S (S O)))).

Я понял, что это 4 и типа nat.

Как это работает, и как Coq узнает, что (S (S (S (S O)))) представляет 4?

Полагаю, ответом на это является какая-то очень умная фоновая магия в Coq.

Answer 1

Inductive naturals : Type :=
   | Z : naturals
   | N : naturals -> naturals.

говорит следующее:

1. Z - это термин типа naturals

2. при eявляется термином типа naturals, N e является термином типа naturals.

3. Применение Z или N - единственные два способа создания естественного,Когда дано произвольное натуральное выражение, вы знаете, что оно было сделано либо из одного, либо из другого.

4. два члена e1 и e2 типа naturals равны, если итолько если они оба Z или если они соответственно N t1 и N t2 с t1 равными t2.

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

• применение конструктора к аргументам правильных типов дает термин типа t;
• anyтермин типа t является результатом применения одного из конструкторов, которые были связаны с типом t, когда он был определен;другими словами, учитывая член типа t, можно предположить, что он является результатом применения одного из конструкторов t;
• два члена типа t равны только в том случае, если онирезультат применения одинаковых конструкторов к одним и тем же аргументам.

(Примечание: если определение типа предназначено для конструкторов формы Z и N, эти свойства более или менее точно соответствуют Аксиомы Пеано для натуральных чисел, поэтому тип с именем nat предопределен в Coq с конструкторами этих форм, которые будут использоваться для представления натуральных чисел. Этот тип получает специальную обработку, потому что он очень утомляетбыстро манипулировать необработанной формой, но специальные процедуры существуют только для удобства.)

Answer 2

В теории типов конструктор (типа) - это просто способ создания новых типов из существующих (http://en.wikipedia.org/wiki/Type_constructor).

В вашем индуктивном определении nat S является конструктором, потому что(если вы посмотрите на подпись), он берет nat и производит другой nat.

Например, конструктор типа для пары nats будет:

Inductive pair : Type := P: nat->nat->pair.

Check P (S (O)) (S(S(O))).