Что такое индукция-индукция ?
Ресурсы, которые я нашел:
- книга HoTT , в конце главы 5.7.
- статья nLab
- статья под названием индуктивно-индуктивные определения
- этот блог также упоминает индуктивно-индуктивные типы
Первые две ссылки слишком кратки для меня, а последние две слишком технические. Кто-нибудь может объяснить это в терминах непрофессионала? Было бы лучше, если бы был код Агды.
Ответы:
Дополнение 2016-10-03: Я перепутал индукцию-индукцию и индукцию-рекурсию (не первый раз, когда я это сделал!). Мои извинения за беспорядок. Я обновил ответ, чтобы покрыть оба.
Я нахожу объяснения в статье Форсберга и Сетцера. Конечная аксиоматизация индуктивно-индуктивных определений освещает.
Индукция-рекурсия
Индуктивно-рекурсивное определение - это определение, в котором мы определяем типA и семейство типов B:A→Type одновременно особым образом:
Без третьего требования, мы могли бы сначала определитьA , а затем отдельно B .
Вот детский пример. ОпределимA индуктивно, чтобы иметь следующие конструкторы:
Семейство типовB определяется как
Индукция индукции
источник