Введение

rzk — это экспериментальный решатель теорем для синтетических ∞-категорий. rzk-1 — это ранняя версия языка, поддерживаемая rzk. Язык основан на «Теории типов для синтетических ∞-категорий» Рил и Шульмана¹. В этом разделе мы вводим синтаксис, обсуждаем возможности и некоторые текущие ограничения решателя теорем.

В целом, программа в rzk-1 состоит из прагмы языка (указывающей, что мы используем rzk-1, а не один из других языков²), за которой следует последовательность команд. Пока мы будем использовать только команду #define.

Вот небольшая формализация в подмножестве MLTT rzk-1:

#lang rzk-1
-- Перестановка аргументов функции.
#define flip
    ( A B : U)                         -- Для любых типов A и B
    ( C : (x : A) → (y : B) → U)     -- и семейства типов C
    ( f : (x : A) → (y : B) → C x y) -- при заданной функции f : A -> B -> C
  : ( y : B) → (x : A) → C x y       -- мы строим функцию типа B -> A -> C
  := \ y x → f x y    -- путём перестановки аргументов

-- Двойная перестановка функции — это то же самое, что ничего не делать
#define flip-flip-is-id
    ( A B : U)                         -- Для любых типов A и B
    ( C : (x : A) → (y : B) → U)     -- и семейства типов C
    ( f : (x : A) → (y : B) → C x y) -- при заданной функции f : A -> B -> C
  : f = flip B A (\ y x → C x y)
          ( flip A B C f)              -- двойная перестановка f — это то же самое, что f
  := refl                             -- доказательство рефлексивностью

Обсудим основные части этого кода:

1. #lang rzk-1 указывает, что мы используем язык rzk-1;
2. -- начинает строку комментария (до конца строки);
3. #define «name» : «type» := «term» определяет имя «name» равным «term»; решатель теорем проверит тип «term» относительно типа «type»;
4. Мы определяем здесь два терма — flip и flip-flip-is-id;
5. flip — это функция, которая принимает 4 аргумента и возвращает функцию двух аргументов.
6. flip-flip-is-id — это функция, которая принимает два типа, семейство типов и функцию f и возвращает значение типа тождества flip ... (flip ... f) = f, указывая, что двойная перестановка функции f возвращает нас к f.

Аналогично трём слоям в теории типов Рил и Шульмана, rzk-1 имеет 3 вселенные:

• CUBE — это вселенная кубов, соответствующая слою кубов;
• TOPE — это вселенная топов, соответствующая слою топов;
• U — это вселенная типов, соответствующая слою типов и термов.

Начиная с v0.8, Rzk также поддерживает экспериментальное модальное расширение (модальности _b, _# и _op) для Триангулированной теории типов; см. Модальности (экспериментально).

Они объясняются в следующих разделах.

Корректность

rzk-1 предполагает "тип-в-типе", то есть U имеет тип U. Известно, что это делает систему типов некорректной (из-за парадоксов в стиле Рассела и Карри), однако, это иногда считается приемлемым в решателях теорем. И, поскольку это упрощает реализацию, rzk-1 принимает это предположение, по крайней мере, пока.

Более того, rzk-1 не предотвращает зависимость кубов или топов от типов и термов. Например, следующее определение проходит проверку типов:

#define weird
    ( A : U)
    ( I : A → CUBE)
    ( x y : A)
  : CUBE
  := I x × I y

Это, вероятно, приводит к ещё одной несогласованности, но, скорее всего, не приведёт к ошибкам в реальных доказательствах, представляющих интерес, поэтому текущая версия принимает это свободное обращение с вселенными.

---

1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442 ↩

2. В версии :octicons-tag-24: v0.1.0, rzk поддерживал просто типизированное лямбда-исчисление, PCF и MLTT. Однако эти языки были удалены. ↩