Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Равенство Лейбница как кодирование Чёрча и Cedille

А вот все говорят, что равенство Лейбница это импредикативное кодирование равенство Мартин-Лёфа.

А вот Cedille получается кодировать индуктивные типы через зависимые пересечения соответствующего им типа импредикативного кодирования, и принципа индукции. Разберём на примере натуральных чисел.

Вот тип алгебр над сигнатурой натуральных чисел:
```
NatAlg := ∀[T : ∗], (succ : T -> T, zero : T)
```

Сами натуральные числа Nat — алгебра, свободно порождённая succ и nat, её можно также охарактеризовать как инициальную среди всех таких алгебр, т.е. из неё существует уникальный гомоморфизм в любую такую алгебру: т.е. в частности это означает, что берём элемент `n : Nat`, берём алгебру `A : NatAlg`, замешиваем их и получаем некий элемент A.T. Можно попробовать сказать, что элементы `Nat` это и есть такие “черные ящики”, превращающие всякую Nat-алгебру в её элемент:
```
Nat-ish := ∀[T : ∗], (T -> T) -> T -> T
```

Это и есть нумералы Чёрча, несложно показать что этот тип имеют выражения следующего вида:
```
zero := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ n
one := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(n)
two := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(f(n))
three := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(f(f(n)))
...
```

А следующая функция превращает нумерал в следующий нумерал:
```
succ(m : Nat-ish) := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ (m(f))(f(n))
```

Все синтаксически-выразимые объекты типа Nat-ish суть натуральные числа. Но, ежели у подлежащей теории есть теоретикомножественные модели, то в этих моделях тип Nat-ish неизбежно будут населять ещё и бестии, невыразимые синтаксически. Однако можно ведь попытаться выделить среди них “настоящие”, т.е. те, для которых работает математическая индукция. Давайте запишем тип, выражающий математическую индукцию, т.е. позволяющий доказать предикат P(n : Nat) для всех n, обладая доказательствами базы индукции P(0) и шага индукции P(n) -> P(succ(n)):

Nat-ly := (n : Nat-ish) ↦ ∀[P : Nat-ish -> ∗], (step : ∀[n : Nat-ish], P(n) -> P(succ n)) -> (base : P(zero)) -> P(n)

В Cedille есть способ выделить среди типа Nat-ish элементы, которые сами себе доказательство индукции (термы n, которые могут быть типизированны одновременно как элементы Nat-ish и как элементы Nat-ly(n) для самого себя):
```
Nat := (n : Nat-ish, n : Nat-ly(n))
```

Вот для этого типа в Cedille можно показать, что это в самом деле тип натуральных чисел.

* * *

Теперь давайте попробуем проделать то же самое для типа равенства. Равенство-лейбница термов `x y : T` записывается как тип
```
Id-ish[T : ∗](x y : T) := ∀[P : T -> ∗], P(x) -> P(y)
```

Запишем также терм
```
refl[T : ∗](x : T) : ∀(P : T -> ∗), (\p : P(x)) ↦ p
```
и обратим внимание, что `refl[T](x) : Id-ish[T](x, x)`.

Теперь давайте вспомним как устроена индукция для равенства Мартин-Лёфа:
```
Id-ly[T : ∗](x y : T) := (p : Id-ish[T](x, y)) ↦ (∀[P : Id[T] -> ∗], P(refl)) -> P(p)
```

Кто-нибудь уже изучал тип `Id-ish[T : ∗](x y : T) := (p : Id-ish[T](x, y), p : Id-ly[T](x, y)(p))` в Cedille?
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 8 comments