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

В этом разделе мы познакомимся с основами 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, пустой тип и типы-копроизведения не встроены, но мы, тем не менее, можем постулировать их в более слабой форме.

Пустой тип (постулированный)

Например, мы можем постулировать пустой тип следующим образом:

#postulate Void
  : U
#postulate ind-Void
  ( C : Void → U)
  : ( z : Void) → C z

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

#define rec-Void
  ( C : U)
  : Void → C
  := ind-Void (\ _ → C)

Тип-копроизведение (постулированный)

Постулированный тип

В этом подразделе представлен только постулированный тип без достаточных пояснений. Как только Rzk обзаведётся поддержой пользовательстких (высших) индуктивных типов или встроенными типами-копроизведениями, этот подраздел будет обновлён.

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

#postulate coprod
  ( A B : U)
  : U

Существует два способа построить элемент типа coprod A B — ввести терм из типа A или из типа B:

#postulate inl
  ( A B : U)
  : A → coprod A B
#postulate inr
  ( A B : U)
  : B → coprod A B

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

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

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

#postulate 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

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

Теперь мы можем определить принцип рекурсии для копроизведений как частный случай индукции:

#define rec-coprod
  ( A B : U)
  ( C : U)
  ( l : A → C)
  ( r : B → C)
  : coprod A B → C
  := ind-coprod A B (\ _ → C) l r

Принцип уникальности для копроизвдений гласит, что любое значение в типе-копроизведении должно быть либо 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

Постулированный тип

В этом подразделе представлен только постулированный тип без достаточных пояснений. Как только Rzk обзаведётся поддержой пользовательстких (высших) индуктивных типов или встроенным булевым типом, этот подраздел будет обновлён.

#postulate Bool
  : U
#postulate false
  : Bool
#postulate true
  : Bool

#postulate ind-Bool
  ( C : Bool → U)
  ( f : C false)
  ( t : C true)
  : ( z : Bool) → C z

#postulate ind-Bool-false
  ( C : Bool → U)
  ( f : C false)
  ( t : C true)
  : ind-Bool C f t false = f
#postulate ind-Bool-true
  ( C : Bool → U)
  ( f : C false)
  ( t : C true)
  : ind-Bool C f t true = t

#define rec-Bool
  ( C : U)
  ( f t : C)
  : Bool → C
  := ind-Bool (\ _ → C) f t

#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

К сожалению, поскольку правила вычисления постулированы только в слабой форме, они не вычисляются автоматически и нам необходимо использовать их явно. Поэтому, следующее доказательство не работает в Rzk:

#define not-not-is-identity
  : (z : Bool) → not (not z) = z
  := ind-Bool
      ( \ z → not (not z) = z)
      ( refl) -- ОШИБКА ТИПОВ! не работает из-за отсутствия "сильных" правил вычисления
      ( refl) -- ОШИБКА ТИПОВ! не работает из-за отсутствия "сильных" правил вычисления

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

Natural numbers

Постулированный тип

В этом подразделе представлен только постулированный тип без достаточных пояснений. Как только Rzk обзаведётся поддержой пользовательстких (высших) индуктивных типов или встроенным типом натуральных чисел, этот подраздел будет обновлён.

#postulate ℕ
  : U
#postulate zero
  : ℕ
#postulate succ (n : ℕ)
  : ℕ

#postulate ind-ℕ
  ( C : ℕ → U)
  ( base : C zero)
  ( step : (n : ℕ) → C n → C (succ n))
  : ( n : ℕ) → C n

#postulate ind-ℕ-zero
  ( C : ℕ → U)
  ( base : C zero)
  ( step : (n : ℕ) → C n → C (succ n))
  : ind-ℕ C base step zero = base
#postulate ind-ℕ-succ
  ( C : ℕ → U)
  ( base : C zero)
  ( step : (n : ℕ) → C n → C (succ n))
  ( n : ℕ)
  : ind-ℕ C base step (succ n) = step n (ind-ℕ C base step n)

#define rec-ℕ
  ( C : U)
  ( base : C)
  ( step : (n : ℕ) → C → C)
  : ℕ → C
  := ind-ℕ (\ _ → C) base step

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

#define compute-ind-ℕ-zero
  ( C : ℕ → U)
  ( base : C zero)
  ( step : (n : ℕ) → C n → C (succ n))
  : C zero
  := base

#define compute-ind-ℕ-one
  ( C : ℕ → U)
  ( base : C zero)
  ( step : (n : ℕ) → C n → C (succ n))
  : C (succ zero)
  := step zero (compute-ind-ℕ-zero C base step)

#define compute-ind-ℕ-two
  ( C : ℕ → U)
  ( base : C zero)
  ( step : (n : ℕ) → C n → C (succ n))
  : C (succ (succ zero))
  := step (succ zero) (compute-ind-ℕ-one C base step)

#compute compute-ind-ℕ-two (\ _ → ℕ) zero (\ _ m → succ (succ m))

---

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 ↩↩↩↩↩