Почему невозможно объявить индуктивный принцип для церковных цифр

17

Представьте себе, мы определили натуральные числа в лямбда-исчислении с зависимой типизацией как церковные цифры. Они могут быть определены следующим образом:

SimpleNat = (R : Set) → R → (R → R) → R

zero : SimpleNat
zero = λ R z _ → z

suc : SimpleNat → SimpleNat
suc sn = λ R z s → s (sn R z s)

SimpleNatRec : (R : Set) → R → (R → R) → SimpleNat → R
SimpleNatRec R z s sn = sn R z s

Однако, похоже, что мы не можем определить церковные цифры с помощью следующего типа принципа индукции:

NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n)

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

Константин Соломатов
источник

Ответы:

20

Вопрос, который вы задаете, интересен и известен. Вы используете так называемое нечеткое кодирование натуральных чисел. Позвольте мне объяснить немного фона.

Учитывая конструктор типа , нас может заинтересовать «минимальный» тип удовлетворяющий . В терминах теории категорий - функтор, а - начальная -алгебра. Например, если то соответствует натуральным числам. Если то - тип конечных бинарных деревьев.Т ( ) Т Т Т ( Х ) = 1 + Х Т ( Х ) = 1 + Х × Х AT:TYпеTYпеAAT(A)TATT(Икс)знак равно1+ИксAT(Икс)знак равно1+Икс×ИксA

Идея с длинной историей заключается в том, что исходная -алгебра имеет тип (Вы используете нотацию Agda для зависимых продуктов, но я использую более традиционную математическую нотацию.) Почему это должно быть? Итак, существу кодирует принцип рекурсии для начальной алгебры: для любой алгебры со структурным морфизмом мы получаем гомоморфизм алгебр помощью Таким образом , мы видим , что является слабо: = Π Х : Т у р е ( Т ( Х ) Х ) Х . A T T Y f : T ( Y ) Y ϕ : A Y ϕ ( a ) = aT

A:знак равноΠИкс:TYпе(T(Икс)Икс)Икс,
ATTYе:T(Y)Yφ:AYA ϕ A K
φ(a)знак равноaYе,
Aначальный точно. Чтобы он был начальным, мы должны знать, что уникальна. Это не верно без дополнительных предположений, но детали являются техническими и противными и требуют чтения некоторого справочного материала. Например, если мы можем показать удовлетворительную теорему параметричности, то мы победим, но есть и другие методы (такие как массирование определения и допущение -аксиомы и экстенсиональности функции).φAК

Применим вышеприведенное к : Мы получили церковные цифры ! И теперь мы также понимаем, что мы получим принцип рекурсии бесплатно, потому что церковные цифры являются принципом рекурсии для чисел, но мы не получим индукцию без параметризации или подобного устройства.T(Икс)знак равно1+Икс

NaTзнак равноΠИкс:TYпе((1+Икс)Икс)Иксзнак равноΠИкс:TYпе(Икс×(ИксИкс))Иксзнак равноΠИкс:TYпеИкс(ИксИкс)Икс,

Технический ответ на ваш вопрос таков: существуют модели теории типов, в которых тип SimpleNatсодержит экзотические элементы, которые не соответствуют цифрам, и, кроме того, эти элементы нарушают принцип индукции. Тип SimpleNatв этих моделях слишком велик и является лишь слабой начальной алгеброй.

Андрей Бауэр
источник
8
Я согласен, что ответ хороший , но здесь могут быть полезны несколько ссылок: статья Гиверса о не выводимости индукции и статья Нила К и Дерека Дрейера о получении (некоторой) индукции из параметричности . Я не знаю о бумаге, которая полностью исследует отношения, хотя.
Коди
Я не слишком силен в ссылках в этой области, спасибо @cody!
Андрей Бауэр