Что такое индукция-индукция?

11

Что такое индукция-индукция ?

Ресурсы, которые я нашел:

Первые две ссылки слишком кратки для меня, а последние две слишком технические. Кто-нибудь может объяснить это в терминах непрофессионала? Было бы лучше, если бы был код Агды.

盛安安
источник
В вашей четвертой цитате есть код Агды.
Жиль "ТАК - перестать быть злым"
Конечно, но было бы очень трудно прочитать этот огромный объем кода. И (я думаю) супер просто, увидев 1 или 2 примера.
盛安安

Ответы:

13

Дополнение 2016-10-03: Я перепутал индукцию-индукцию и индукцию-рекурсию (не первый раз, когда я это сделал!). Мои извинения за беспорядок. Я обновил ответ, чтобы покрыть оба.

Я нахожу объяснения в статье Форсберга и Сетцера. Конечная аксиоматизация индуктивно-индуктивных определений освещает.

Индукция-рекурсия

Индуктивно-рекурсивное определение - это определение, в котором мы определяем тип A и семейство типов B:AType одновременно особым образом:

  1. A определяется как индуктивный тип.
  2. B определяется рекурсии наA .
  3. Важно отметить , что определение A может использовать B .

Без третьего требования, мы могли бы сначала определить A , а затем отдельно B .

Вот детский пример. Определим A индуктивно, чтобы иметь следующие конструкторы:

  • a:A
  • :(x:AB(x))A

Семейство типов B определяется как

  • B(a)=bool
  • B((x,f))=nat

A

a:A.
B(a)bool
(a,false)
(a,true)
AB((a,false))=B((a,true))=natn:nat
((a,false),n):A
((a,true),n):A
B(((a,true),n))=nat
m:nat
(((a,true),n),m):A
(((a,false),n),m):A
A

Индукция индукции

AB:AType

  1. A
  2. BA
  3. AB

B

B(c())=
c()ABB

A

  • a:A
  • :(x:AB(x))A

B

  • Tru:B(a)
  • Fal:B(a)
  • x:Ay:B(x)Zer:B((x,y))
  • x:Ay:B(x)z:B((x,y))Suc(z):B((x,y))

BB(a)B((x,y))

Андрей Бауэр
источник
почему, черт возьми, кто-то может определять такие типы данных D:
盛安安
7
Для того, чтобы научить, что такое индуктивно-индуктивный тип. Я мог бы привести вам реальный пример, а именно тип вселенной, но это может сбить с толку.
Андрей Бауэр
3
@AndrejBauer Для меня это больше похоже на индукцию-рекурсию. Индукция-индукция - это когда типовое семейство определяется как индуктивный тип .
Gallais
2
Ой, ты абсолютно прав. Я исправлю это.
Андрей Бауэр