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

[akuklev]

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

Comments

[jahr2]

Прошу прощения за тупость, но что-то cedille не гуглится, не дадите прямую ссылку?)

[akuklev]

https://cedille.github.io/

[jahr2]

Спасибо.)

[anonymous]

Так понятнее - в исходной формуле 2 разных n и непонятно где какая:

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

Я это понимаю так, что для каждого элемента у нас есть доказательство, что цепочка импликаций от нуля через него пройдёт, т.е. это такая красивая кодировка достижимости за конечное число шагов.

> Теперь давайте вспомним как устроена индукция для равенства Мартин-Лёфа

Другое название индукции это dependent eliminator. Ну и в https://homepage.cs.uiowa.edu/~astump/papers/cdle-proofs.pdf рассматриваются J- и K- элиминаторы. Посмотрите на них.

Ещё в https://arxiv.org/pdf/1811.11961.pdf нашёл IdMapping это как раз Ваш Id-Ish

[akuklev]

Я сейчас оформляю содержимое этого поста в англоязычный текст с пробами кода на Cedille: https://github.com/akuklev/QIITs-in-Cedille/

Доделаю - отпишусь.

[nponeccop]

А там коммент мой в спам попал, расспамьте плиз

[66george]

Александер, а вот посоветуйте, как сделать красиво

[66george]

Вот часть вопроса, кажется, решил (как не перерисовывать лишний раз). Если каждый объект будет знать число своих потомков и потомок, обновясь, будет посылать сигнал-подтверждение. Допустим, у объекта А три потомка. Он обновился, послал во все стороны сигнал (широковещание). Потомки его слышат, обновляются сами и шлют сигнал-подтверждение. Пришли три подтверждения - объект А шлёт сигнал рисовальной машинке. Если есть внуки, принцип тот же - сын обновляется сам и ждёт подтверждений от внуков, после чего посылает подтверждение родителю. Фундированное дерево!