Зависимые типы

В этом разделе мы познакомимся с основами Rzk, позволяющими нам работать с зависимыми типам.

Источники

Эта страница основана почти целиком на введении в зависимые типы в «Гомотопической теории типов»^{1 2} (Sections 1.2–1.6), и сразу вводит соответствующие формализации на Rzk, указывая на некоторые различия между "книжной" теорией и решателем Rzk.

Этот раздел является литературным файлом Rzk:

#lang rzk-1

Функции

Запись (x : A) → B x представляет тип (зависимых) функций с аргументом типа A и, для каждого входа x, результат типа B x.

В качестве простого примера зависимой функции, рассмотрим тождественную функцию:

#define identity
  : ( A : U) → (x : A) → A
  := \ A x → x

Поскольку мы не используем переменную x в типе функции identity, мы можем упростить тип функции, указав для второго аргумента только тип (без имени аргумента):

#define identity₁
  : ( A : U) → A → A
  := \ A x → x

Мы можем записать это же определение по-другому, переместив (A : U) в параметры определения (до :), при этом опуская этот аргумент в теле определения (после :=):

#define identity₂
  ( A : U)
  : A → A
  := \ x → x

В принципе, мы могли бы также переместить x в параметры, но вряд ли бы это повысило читаемость:

#define identity₃
  ( A : U)
  ( x : A)
  : A
  := x

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

#define swap
  ( A B C : U)
  : ( A → B → C) → (B → A → C)
  := \ f → \ b a → f a b

Типы-произведения

Rzk не предоставляет встроенных типов-произведений, поскольку они являются частным случаем Σ-типов (зависимых пар), о которых мы поговорим в следующем подразделе. Но пока мы просто дадим определение типов-произведений:

#define prod
  ( A B : U)
  : U
  := Σ (_ : A) , B

Запись prod A B соответствует типу-произведению \(A \times B\). Запись Unit соответствует единичному типу \(\mathbf{1}\).

Элементами типа prod A B предполагаются только пары (a, b) : prod A B где a : A и b : B. Аналогично, единственным элементом Unit предполагается unit. Технически, теория типов не гарантирует, что эти типы состоят только из упомянутых элементов, но скоро мы сможем доказать, что это так.

Заметка о конструкторах типов

Формально, каждый новый тип (конструктор типов) состоит из следующих компонентов. Мы показываем примеры для типов-произведений и функций для сравнения:

1. Правила формирования (конструирования) типов:

   • prod A B — это тип, если A и B типы
   • A → B — это тип, если A и B типы

2. Конструкторы (правила введения):

   • (x , y) является термом (выражением) типа prod A B, если x : A и y : B
   • \ x → y является термом (выражением) типа A → B, если для любых x : A верно, что y : B (y здесь — это произвольное выражение, возможно, содержащее x)

3. Правила устранения:

   • Если z : prod A B, то мы можем использовать проекцию чтобы получить первый или второй компоненты:
   • first z : A и second z : B

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

     #define swap-prod₁
       ( A B : U)
       : prod A B → prod B A
       := \ (x , y) → (y , x)
     
     #define swap-prod₂
       ( A B : U)
       ( (x , y) : prod A B)
       : prod B A
       := ( y , x)
     

   • в общем случае, правила устранения записываются как принцип индукции, который мы обсудим ниже, и может быть определён в Rzk через сопоставление с образцом или first и second:

     #define ind-prod
       ( A B : U)
       ( C : prod A B → U)
       ( f : (a : A) → (b : B) → C (a , b))
       : (z : prod A B) → C z
       := \ (a , b) → f a b
     

   • Если f : A → B, мы можем применить функцию к аргументу a : A:

   • f a : B

   Встроенные проекции в Rzk

   Встроенные проекции и правила устранения в Rzk должны быть применены ко всем аргументам (например, first без аргумента считается невалидным синтаксисом!). Технически, это ограничение схоже со "вторым представлением" теории типов в Приложении A.2 книги ^{1 2}. На практике, это не всего удобно, поскольку часто хочется исползовать каррированные варианты, поэтому пользователи часто вводят обёртки над встроенными проекциями, например:

   #define pr₁
     ( A B : U)
     : prod A B → A
     := \ p → first p
   

4. Правила вычисления:

   • Проекция из пары вычисляется следующим образом для любых x : A and y : B:
   • first (x , y) ≡ x
   • second (x , y) ≡ y
   • Применение лямбда-функции к аргументу вычисляется при помощи подстановки аргумента в тело функции:
   • (\ x → y) a ≡ y{x ↦ a} when a : A and for all x : A, y : B.

5. Принцип уникальности (опционально):

   • Для любых z : prod A B, верно z ≡ (first z, second z)
   • В Rzk это выполняется по определению для типов-произведений и Σ-типов, но в книге^{1 2} это можно доказать только в слабой (пропозициональной) форме.
   • Для любой функции f : A → B верно, что f ≡ \ x → f x

Принцип рекурсии

Следуя книге^{1 2}, для каждого конструктора типов мы можем сформулировать принцип рекурсии. Принцип рекурсии для типа T — это способ построить функцию в произвольный тип C из типа T:

#define rec-T
  ( C : U)
  -- ... (параметры принципа рекурсии)
  : T → C

Например, для типа-произведения prod A B, принцип рекурсии выглядит следующим образом:

#define rec-prod
  ( A B : U)
  ( C : U)
  ( f : A → B → C)
  : prod A B → C
  := \ (a , b) → f a b

Для типа Unit, принцип рекурсии тривиален:

#define rec-Unit
  ( C : U)
  ( c : C)
  : Unit → C
  := \ unit → c

Принцип индукции

Чтобы определить зависимую функцию из типа, необходим принцип индукции, который можно рассматривать как зависимый вариант принципа рекурсии. Принцип индукции для типа T — это способ (функция), позволяющий построить функцию в тип C z для каждого входа z : T:

#define ind-T
  ( C : T → U)
  -- ... (параметры принципа индукции)
  : (z : T) → C z

Например, для типа-произведения prod A B, принцип индукции выглядит так:

#define ind-prod
  ( A B : U)
  ( C : prod A B → U)
  ( f : (a : A) → (b : B) → C (a , b))
  : ( z : prod A B) → C z
  := \ (a , b) → f a b

Мы можем использовать ind-prod для доказательства принципа уникальности. Тут мы используем тип-тождество, который обсудим позже. Пока нам достаточно знать, что для любого x : A всегда можно построить элементrefl_{x} типа x =_{A} x.

#define uniq-prod
  ( A B : U)
  ( z : prod A B)
  : ( first z , second z) =_{prod A B} z
  := ind-prod A B
      ( \ z' → (first z' , second z') =_{prod A B} z') -- C
      ( \ a b → refl_{(a , b)})
        -- C (a, b)
        -- ≡ ( \ z' → (first z', second z') =_{prod A B} z') (a, b)
        -- ≡ (first (a, b), second (a, b)) =_{prod A B} (a, b)
        -- ≡ (a, second (a, b)) =_{prod A B} (a, b)
        -- ≡ (a, b) =_{prod A B} (a, b)
      z

Поскольку принцип уникальности уже встроен в Rzk, более простое доказательство также подойдёт:

#define uniq-prod'
  ( A B : U)
  ( z : prod A B)
  : ( first z , second z) =_{prod A B} z
  := refl_{z} -- работает в Rzk, но не в книжном HoTT, поскольку в Rzk верно (first z, second z) ≡ z

Для единичного типа Unit принцип индукции выглядит просто:

#define ind-Unit
  ( C : Unit → U)
  ( c : C unit)
  : ( z : Unit) → C z
  := \ unit → c

В отличие от rec-Unit, принцип индукции для Unit не бесполезен, поскольку он позволяет доказать принцип уникальности для единичного типа:

#define uniq-Unit
  ( z : Unit)
  : unit =_{Unit} z
  := ind-Unit
      ( \ z' → unit =_{Unit} z')
      ( refl_{unit})
      z

Опять же, поскольку принцип уникальности уже встроен в Rzk, более простое доказательство также сработает:

#define uniq-Unit'
  ( z : Unit)
  : unit =_{Unit} z
  := refl_{z} -- работает в Rzk, но не в книжном HoTT, поскольку в Rzk верно unit ≡ z

Зависимые пары (Σ-типы)

Σ-типы являются обобщением типов-произведений и позволяют типу второго элемента зависеть от значения первого. Запись Σ (a : A), B a соответствует типу зависимых пар, где A тип и B : A → U семество типов, индексируемое в типе A.

Предполагаемыми элементами типа Σ (a : A), B a являются пары (a , b) термов a : A и b : B a. Заметьте, что тип второго терма может зависеть от значения первого. Если семейство типов B константное, например (\ _ → C), то Σ (a : A), B a становится в точности типов-произведением prod A C.

Для устранения зависимых пар, мы используем first, second, или сопоставление с образцом для пар. Однако, типы проекций в этом случае не такие очевидные, как для типов-произведений.

Проекции

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

#define pr₁
  ( A : U)
  ( B : A → U)
  : ( Σ ( a : A) , B a) → A
  := \ (a , _) → a

Однако, для определения второй проекции нужна осторожность. В частности, следующее определение не сработает:

-- NOTE: incorrect definition
#define pr₂
  ( A : U)
  ( B : A → U)
  : (Σ (a : A), B a) → B a  -- ОШИБКА ТИПОВ!
  := \ (_ , b) → b

undefined variable: a

Мы получили ошибку undefined variable (неизвестная переменная), поскольку переменная a не видна снаружи определения Σ-типа. Для доступа к первой компоненте зависимой пары, нам нужно использовать первую проекцию:

#define pr₂
  ( A : U)
  ( B : A → U)
  : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
  := \ (_ , b) → b

Иногда о Σ-типах удобнее говорить как о тотальных (общих?) типах (аналогично "total spaces"):

#define total-type
  ( A : U)
  ( B : A → U)
  : U
  := Σ (a : A) , B a

Мы можем переписать более компактно определение второй проекции, используя сопоставление с образцом в параметрах, и используя total-type:

#define pr₂'
  ( A : U)
  ( B : A → U)
  ( ( a , b) : total-type A B)
  : B a
  := b

Принципи рекурсии и индукции

Принцип рекурсии для Σ-типов простым образом общает соответствующий принцип для типов-произведений:

#define rec-Σ
  ( A : U)
  ( B : A → U)
  ( C : U)
  ( f : (a : A) → B a → C)
  : total-type A B → C
  := \ (a , b) → f a b

Аналогично с принципом индукции:

#define ind-Σ
  ( A : U)
  ( B : A → U)
  ( C : total-type A B → U)
  ( f : (a : A) → (b : B a) → C (a , b))
  : ( z : total-type A B) → C z
  := \ (a , b) → f a b

Как и раньше, мы можем использовать ind-Σ для доказательства принципа уникальности, теперь для Σ-типов:

#define uniq-Σ
  ( A : U)
  ( B : A → U)
  ( z : total-type A B)
  : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
  := ind-Σ A B
      ( \ z → (pr₁ A B z , pr₂ A B z) =_{total-type A B} z)
      ( \ a b → refl_{(a , b)})
      z

И опять же, Rzk допускает более простое доказательство, поскольку уникальность для Σ-типов встроена в решатель:

#define uniq-Σ'
  ( A : U)
  ( B : A → U)
  ( z : total-type A B)
  : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
  := refl_{z} -- работает в Rzk, но не в книжном HoTT

Теоретико-типовая "аксима" выбора

Используя принцип индукции ind-Σ мы можем доказать версию аксиомы выбора в теории типов:

#define AxiomOfChoice
  : U
  := (A : U)
    → ( B : U)
    → ( R : A → B → U)
    → ( ( x : A) → Σ (y : B) , R x y)
    → ( Σ ( f : A → B) , (x : A) → R x (f x))

Читалю предлагается попробовать доказать это утверждение самостоятельно:

#define axiom-of-choice
  : AxiomOfChoice
  := ...

При возникновении проблем с доказательством, вы можете обратиться к разделу 1.6 (стр. 32) в книге^{1 2}.

Если всё ещё остануться проблемы при формализации доказательства в Rzk, можете подсмотреть решение здесь:

Доказательство теоретико-типовой аксиомы выбора

#define ac : AxiomOfChoice
  := \ A B R g → ( \ a → first (g a) , \ x → second (g x))
  -- g    : (x : A) → Σ (y : B), R x y
  -- x    : A
  -- g x  : Σ (y : B), R x y
  -- second (g x) : R x (first (g x))

  -- f : A → B
  -- f := \ a → first (g a)
  --
  -- R x (f x)
  -- == R x ((\ a → first (g a)) x)
  -- == R x (first (g x))

Копроизведения (суммы типов)

Для типов \(A\) и \(B\), тип \(A + B\) соответствует (интуитивно) дизъюнктивному объединению \(A\) и \(B\) (при интерпретации в теории множеств). Для полноты также разумно предположить наличие пустого типа: \(\mathbf{0}\).

В Rzk, пустой тип и типы-копроизведения объявляются как индуктивные типы с помощью команды #data.

Пустой тип

Пустой тип — это индуктивный тип без конструкторов:

#data Void

Объявление порождает принцип индукции ind-Void и его простую (не зависимую) версию rec-Void:

#check ind-Void : (C : Void → U) → (z : Void) → C z
#check rec-Void : (C : U) → Void → C

Поскольку в пустом типе Void нет элементов, принцип индукции соответсвует принципу абсурности (из лжи следует что угодно).

Тип-копроизведение

Тип-копроизведение — это индуктивный тип с двумя конструкторами — один вводит терм из типа A, другой из типа B:

#data coprod
  ( A B : U)
  :=
    inl (a : A)
  | inr (b : B)

Чтобы устранить копроизведение, порождённый принцип индукции требует два обработчика — один на случай, если в копроизведении хранится левое значение, и один на случай правого значения:

#check ind-coprod
  : ( A : U) → (B : U)
  → ( C : coprod A B → U)
  → ( ( a : A) → C (inl A B a))
  → ( ( b : B) → C (inr A B b))
  → ( z : coprod A B) → C z

Правила вычисления определительные: ind-coprod A B C l r (inl A B a) вычисляется в l a автоматически. Например, следующее равенство доказывается через refl:

#define compute-ind-coprod-inl
  ( A B : U)
  ( C : coprod A B → U)
  ( l : (a : A) → C (inl A B a))
  ( r : (b : B) → C (inr A B b))
  ( a : A)
  : ind-coprod A B C l r (inl A B a) = l a
  := refl

Принцип рекурсии для копроизведений — это порождённая не зависимая версия:

#check rec-coprod
  : ( A : U) → (B : U)
  → ( C : U)
  → ( ( a : A) → C)
  → ( ( b : B) → C)
  → coprod A B → C

Принцип уникальности для копроизвдений гласит, что любое значение в типе-копроизведении должно быть либо inl, либо inr. Доказательство принципа уникальности относительно простое, однако Rzk требует явно расписать все промежуточные типы:

#define uniq-coprod
  ( A B : U)
  ( z : coprod A B)
  : coprod
      ( Σ ( a : A) , inl A B a = z)
      ( Σ ( b : B) , inr A B b = z)
  := ind-coprod A B
      ( \ z' → coprod
          ( Σ ( a : A) , inl A B a = z')
          ( Σ ( b : B) , inr A B b = z'))
      ( \ a' → inl
          ( Σ ( a : A) , (inl A B a = inl A B a'))
          ( Σ ( b : B) , (inr A B b = inl A B a'))
          ( a' , refl))
      ( \ b' → inr
          ( Σ ( a : A) , (inl A B a = inr A B b'))
          ( Σ ( b : B) , (inr A B b = inr A B b'))
          ( b' , refl))
      z

Booleans

Булев тип — это индуктивный тип с двумя конструкторами без полей:

#data Bool := false | true

Порождённые принципы индукции и рекурсии имеют ожидаемые типы:

#check ind-Bool
  : ( C : Bool → U)
  → C false
  → C true
  → ( z : Bool) → C z

#check rec-Bool : (C : U) → C → C → Bool → C

#define uniq-Bool
  ( z : Bool)
  : coprod (z = false) (z = true)
  := ind-Bool
      ( \ z' → coprod (z' = false) (z' = true))
      ( inl (false = false) (false = true) refl)
      ( inr (true = false) (true = true) refl)
      z

#define not
  : Bool → Bool
  := rec-Bool Bool true false

Поскольку правила вычисления индуктивных типов определительные, not (not false) вычисляется в false, а not (not true) — в true, и следующее доказательство проходит индукцией с двумя случаями refl:

#define not-not-is-identity
  : ( z : Bool) → not (not z) = z
  := ind-Bool
      ( \ z → not (not z) = z)
      ( refl)
      ( refl)

Индуктивные типы и симплициальная структура

Индуктивный тип приходит ровно со своим принципом индукции. Как тип взаимодействует с симплициальной структурой Rzk — отдельный вопрос, и, вообще говоря, это взаимодействие невыводимо. В частности, принцип индукции Bool не доказывает дискретность Bool: дискретность Bool эквивалентна предположению, что существует тип с двумя точками, не соединёнными стрелкой, а без дополнительных аксиом теория не может доказать это предположение. Таким образом, чтобы Bool был дискретным, всё ещё необходима аксиома несвязности; объявление #data Bool не доказывает ничего нового о 2 → Bool.

Natural numbers

Натуральные числа — рекурсивный индуктивный тип: конструктор succ хранит натуральное число. Порождённый принцип индукции предоставляет гипотезу индукции для рекурсивного поля:

#data ℕ := zero | succ (n : ℕ)

#check ind-ℕ
  : ( C : ℕ → U)
  → C zero
  → ( ( n : ℕ) → C n → C (succ n))
  → ( n : ℕ) → C n

#check rec-ℕ : (C : U) → C → ((n : ℕ) → C → C) → ℕ → C

#define double-ℕ
  : ℕ → ℕ
  := rec-ℕ ℕ zero (\ _ m → succ (succ m))

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

#define double-two
  : double-ℕ (succ (succ zero)) =_{ℕ} succ (succ (succ (succ zero)))
  := refl

---

1. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. 2013. https://homotopytypetheory.org/book/ ↩↩↩↩↩

2. Международный коллектив авторов. Гомотопическая теория типов: унивалентные основания математики. ИНСТИТУТ ПЕРСПЕКТИВНЫХ ИССЛЕДОВАНИЙ. Перевод и редактирование: ГЕННАДИЙ ЧЕРНЫШЕВ. https://henrychern.files.wordpress.com/2022/10/hott2.pdf ↩↩↩↩↩