Cedille: Полиморфное лямбда-исчисление с выводимой индукцией

Стартовой точкой подхода Стумпа является наблюдение (сделанное не им, и очень давно), что термы, реализующие рекурсию, и термы реализующие индукцию, после стирания ти́повых аннотаций (англ. erasure), становятся одинаковыми.

Давайте начнём с натуральных чисел и рекурсии. Пусть у нас есть функция f : Nat ⟶ Nat. Как будет выглядеть функция высшего порядка, которая повторяет наше f n раз?

Ноль раз: (f : Nat ⟶ Nat) ↦ (n : Nat) ↦ nОдин раз: (f : Nat ⟶ Nat) ↦ (n : Nat) ↦ f(n)Два раза: (f : Nat ⟶ Nat) ↦ (n : Nat) ↦ f(f(n))Три раза: (f : Nat ⟶ Nat) ↦ (n : Nat) ↦ f(f(f(n))).

Заметим, что все эти функции высшего порядка удовлетворяют сигнатуре (Nat ⟶ Nat) ⟶ Nat ⟶ Nat.

А почему мы ограничились функциями на типе Nat? У нас же полиморфное лямбда-исчисление, мы можем записать наши “повторяторы” для любого типа X. Теперь термы выглядят вот так:

ch-zero: ∀[X : *], (f : X ⟶ X) ↦ (n : X) ↦ nch-one: ∀[X : *], (f : X ⟶ X) ↦ (n : X) ↦ f(n)ch-two: ∀[X : *], (f : X ⟶ X) ↦ (n : X) ↦ f(f(n)).

Квантор всеобщности ∀ означает, что указанные термы полиморфны по ти́повому параметру X, специализация для конкретного X обозначается при помощи квадратных скобок, вот так:ch-two[Nat] = (f : Nat ⟶ Nat) ↦ (n : Nat) ↦ f(f(n))

Параметры, вводимые при помощи `∀[P : K], . `, отличаются от переменных, вводимых при помощи `(x : X) ↦ . ` тем, что их можно использовать _только_ в ти́повому аннотациях и для специализации, но не в вычислительном теле лямбда-терма. Т.е. эти параметры вместе с самой конструкцией `∀[P : K], . ` полностью исчезают при переходе от аннотированного терма к сырому (“стирании ти́повых аннотаций”).

Приведённые выше термы будут удовлетворять сигнатуре, обозначаемой ∀(X : *), (X ⟶ X) ⟶ X ⟶ X. Эту сигнатуру мы будем обозначать через ChNumeral, она нам ещё понадобится. Например, чтобы записать функцию, которая делает из n-го нумерала (n + 1)-ый:ch-succ: (numeral : ChNumeral) ↦ ∀[X : *], (f : X ⟶ X) ↦ (n : X) ↦ numeral[X](f)(f(n))

Обратим внимание, что если стереть ти́повые аннотации и оставить только сырые лямбда-выражения, то полиморфные термы становятся эквивалентны специализированным (причём совершенно неважно, специализированным относительно какого типа).

Теперь пусть у нас есть семейство утверждений, индексированных натуральными числами Q[n : Nat] : *, и шаг индуктивного доказательства, который из верности Q[n] выводит верность Q[n + 1], назовём его step : ∀(n : Nat), Q[n] ⟶ Q[n + 1].

Квантор всеобщности ∀ означает, что терм step полиморфен по параметру n, специализации терма step для конкретного n обозначаются через step[n], напримерstep[2] : Q[2] ⟶ Q[3].

Как выглядят термы, применяющие доказательство step некоторое количество m раз?

Ноль раз:∀[Q : Nat ⟶ *], (step : ∀(n : Nat), Q[n] ⟶ Q[n + 1]) ↦ (ev : Q[0]) ↦ ev

Один раз:∀[Q : Nat ⟶ *], (step : ∀(n : Nat), Q[n] ⟶ Q[n + 1]) ↦ (ev : Q[0]) ↦ step[0](ev)

Два раза:∀[Q : Nat ⟶ *], (step : ∀(n : Nat), Q[n] ⟶ Q[n + 1]) ↦ (ev : Q[0]) ↦ step[1](step[0](ev))

Три раза:∀[Q : Nat ⟶ *], (step : ∀(n : Nat), Q[n] ⟶ Q[n + 1]) ↦ (ev : Q[0]) ↦ step[2](step[1](step[0](ev)))

Общая сигнатура всех таких индукторов:Inductor: ∀(n : Nat), ∀(Q : Nat ⟶ *), (step : ∀(n : Nat), Q[n] ⟶ Q[n + 1]) ⟶ Q[0] ⟶ Q[n]

После стирания ти́повых аннотаций, в сухом остатке остаются всё те же наши сырые нумералы.

Примечание: система типов, в рамках которой мы пока что работали, называется Implicit Calculus of Constructions также обозночаемая через λΠ∀ω. Это один из вариантов реализации самого навороченного угла куба Pure Type Systems Барендрегта. (Альтернативным вариантом является реализация без отдельного параметрического квантора ∀, зато с двухуровневой системой сортов: сорта “малых” типов PROP и сорта "больших" типов TYPE; этот вариант как раз и называется Calculus of Constructions.)

После наблюдения, что как сырые термы нумералы эквивалентны индукторам, Стумп сотоварищи обратились к крайне интересной штуковине, придуманной лет пятнадцать назад Алексеем Копыловым ( papa_lyosha , http://www.cs.cornell.edu/people/kopylov/papers/dinter/dinter.pdf): зависимому пересечению. Типы пересечения A ∩ B используются в системах типов, где один и тот же терм может быть типирован разными способами. Тут мы будем использовать его в том смысле, что одни и те же _сырые_ термы (нумералы, они же индукторы) могут быть типированны по-разному. Собственно, как нумералы, и как индукторы.

Зависимое пересечение позволит нам ввести тип "нумерал, а ещё и индуктор", идейно (n : ChNumeral) ∩ Inductor[n]

Тут есть abuse of notation: n слева имеет тип ChNumeral, а справа Nat. Но на самом деле мы хотим работать в системе без данного свыше типа Nat, поэтому заменим в определении Inductor'а Nat на ChNumeral. Разумеется, это не одно и тоже, но давайте попробуем:

ChInductor: ∀(n : ChNumeral), ∀(Q : ChNumeral ⟶ *), (step : ∀(n : ChNumeral), Q[n] ⟶ Q[ch-succ n]) ⟶ Q[0] ⟶ Q[n].

Вот теперь можно смело определять тип

ChNat: (n : ChNumeral) ∩ ChInductor[n]

Этот тип примечателен тем, что для него можно доказать, что его элементы сами себе индукторами, т.е. мы можем определить для них термind-ChNat : (n : ChNat) ⟶ ∀(Q : ChNat ⟶ *), (step : ∀(n : ChNat), Q[n] ⟶ Q[succ n]) ⟶ Q[0] ⟶ Q[n]

Так что это самый настоящий Nat! И более того, для широкого класса индуктивных типов мы можем подобным образом сформировать сигнатуры: слева от зависимого пересечения написано, что речь идёт об алгебре для указанного функтора, а справа — что эта алгебра инициальна. Подробнее об этом можно прочитать вот тут: http://homepage.cs.uiowa.edu/

astump/papers/from-realizability-to-induction-aaron-stump.pdf и тут: http://firsov.ee/impred-ind/impred-ind.pdf, где результат для натуральных чисел обобщается на произвольные индуктивные типы, заданные полиномиальными функторами. Более или менее понятно, что это должно без проблем обобщаться на зависимые полиномиальные функторы.

Более того, утверждается, что эту систему можно расширить тайп-лифтингом (иерархия малых вселенных-лайт) таким образом, что для типов, для которых можно показать образуемость конечным набором конструкторов, работает large elimination. В частности для Nat тогда можно определить и зависимый элиминаторelim-ChNat : (n : ChNat) ⟶ ∀(Q : ChNat ⟶ *), (step : (n : ChNat) ⟶ Q[n] ⟶ Q[succ n]) ⟶ Q[0] ⟶ Q[n].

Как вот это работает мне пока не понятно абсолютно, за отсутствием доступа к черновикам публикаций. Кое-что можно себе представить по прежним статьям, но только в общих чертах. Я пока не на 100% уверен в том, что всё прямо так волшебно работает, как рассказывают Стумп сотоварищи, но идея красивая, и если оно работает, то это прямо бомба.

Sanity check'ом должна быть интерпретируемость внутри этой системы новейшего золотого стандарта конструктивной математики догомотопической эры: системы pCuIC(+UP) — Predicative Calculus of Cumulative Inductive Constructions with Universe Polymorphism, https://arxiv.org/abs/1710.03912 + https://www.irif.fr/

sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf — Intensional MLTT со счётной иерархией кумулятивных вселенных, кумулятивными индуктивными типами (включая индексированные и индуктивно-индуктивные) и импредикативным Prop'ом — теоретическую базу новейшей версии Coq 8.7, которая наконец превзошла Agda во всех отношениях (в прежних версиях слабостями Coq'а были полиморфизм по вселенным, а также эта-конверсия для функций и рекордов), исключая только экспериментальные возможности вроде индуктивро-рекурсивных и коиндуктивных типов.

Существенным моментом во всей конструкции является то, что вводится особый синтаксис для аннотированных термов t : (x : X) ∩ Y[x]. Эти термы представляют из себя сжимаемые тройки, состоящии из одного аннотированного терма x типа X, одного аннотированного терма типа y типа Y[x] и доказательства, что |x| === |y|, вот прямо цепочки правил приводящих эрейзнутый терм x в эрейзнутый терм y.

И это наводит на мысли, что вся эта штуковина, должна бы иметь и гомотопическую версию, где сжимаемые тройки используются более разнообразно, равенство трактуется более широко, а параметричность зависимости — более гибко: В строгой версии тип ∀(n : Nat), Q[n] обязаны населять только термы t, в неаннотированных версиях которых n вообще не используется. В гомотопической версии это ослабляется до требования, чтобы независимо от того, какой n подставляется, выходили равные результаты, т.е. можно взять любой терм t : (n : Nat) ⟶ Q[n], снабженный доказательством t' : (n m : Nat) ⟶ t(n) = t(m).

Ну например, неупорядоченную пару UPair мы можем импредикативно представить как ∀(X : *), ∀(Y : *), (f : (X ⟶ X ⟶ Z)) ⟶ (symmetry : (a b : X) ⟶ f(a)(b) = f(b)(a)) ⟶ Y. Тогда получится, что равенство двух функций из UPair[X] в Y можно показывать не только пользуясь стандартными бета- и эта-конверсиями на уровне сырых термов, но и пользуясь "конструктором" symmetry. Ведь чтобы задать функцию из неупорядоченной пары куда-то в другое место, задающему придётся показать симметричность этой функции, а значит в дальнейшем на неё можно полагаться. Есть все основания полагать, что “топорная” реализация этого подхода даст нам теорию без UIP, но с всевозможными высшими индуктивными типами, работающими “правильным” образом, и, вероятно, пропозициональной и функциональной экстенциональностью.

Но даже на уровне таких дичайших спекуляций непонятно, однако, можно ли будет изогнуть эту систему так, чтобы для "встроенного типа равенства" _=_ работал J-элиминатор и тем более, чтобы можно было доказать унивалентность; скорее всего, без крайне хитрых извратов в кубическом стиле ничего подобного работать не будет. Однако тем из нас, кому платонизм ближе структурализма, безусловно, полезно было бы разобраться, можно ли этого как-то достичь.