Я наткнулся на противоречивое разногласие между Агдой и Коком, которое, очевидно, не связано с наиболее известными различиями между их теориями типов (например, (im) предсказуемость, индукция-рекурсия и т. Д.).
В частности, Агда принимает следующее определение:
data Ty : Set0 -> Set0 where
c1 : Ty ℕ
c2 : Ty (Ty ℕ)
в то время как эквивалентное определение Coq отклонено, поскольку появление [Ty _] в качестве индекса самого себя в c2 считается нарушением строгой положительности.
Inductive Ty : Set -> Set :=
| c1 : Ty nat
| c2 : Ty (Ty nat).
Фактически, этот случай является почти дословным примером из раздела 14.1.2.1 Coq'Art о нарушении строгой позитивности:
Inductive T : Set -> Set := c : (T (T nat)).
Но я не вижу причин такого различия между теориями типов. Мне понятен классический пример доказательства того, что False использует отрицательное вхождение типа в аргументе конструктора, но я не могу понять, как можно извлечь противоречие из этого стиля индексации (независимо от других строго положительных аргументов конструктора).
Обращаясь к литературе, в ранней статье «Индуктивные семьи» Дайбжера делается необоснованный комментарий о том, что решение Полина-Моринга в статье CID имеет несколько иные ограничения, и смутно предполагает, что различия могут быть связаны с непредсказуемостью, но не будем подробно останавливаться на этом. Бумага Дайберса, кажется, позволяет это, в то время как бумага Полина-Моринга явно запрещает это.
Очевидно, я не первый, кто заметил эту разницу во мнениях, и некоторые считают, что это определение не должно быть разрешено ни в одной из систем ( https://lists.chalmers.se/pipermail/agda/2012/004249.html ), но Я не нашел никаких объяснений того, почему это звучит в одной системе, а не в другой, или просто нет различий во мнениях.
Итак, я полагаю, у меня есть несколько вопросов:
- Это пример монотонного, но не строго положительного типа? (В Coq; явно Агда считает это строго положительным)
- Почему Agda разрешает это, в то время как Coq отклоняет это? Это просто своеобразное различие в интерпретации «строго положительного», есть ли тонкая разница между Coq и Agda, которая делает его звучащим в Agda, и несостоятельным в Coq, или это вопрос вкуса, обусловленный конкретными теоретическими предпочтениями?
- Есть ли существенная разница между первым определением выше и эквивалентным индуктивно-рекурсивным определением ниже?
Индуктивно-рекурсивное определение:
mutual
data U : Set0 -> Set0 where
c : (i : Fin 2) -> U (T i)
T : Fin 2 -> Set0
T zero = ℕ
T (suc zero) = U ℕ
Я счастлив иметь указатели на соответствующую литературу.
Заранее спасибо.
источник
Ty is not strictly positive, because it occurs in an index of the target type of the constructor c2 in the definition of Ty.
Ответы:
Похоже, проблема заключается в путанице, вызванной слиянием двух факторов:
Это более близкое прочтение, конечно, согласуется с проверкой, которую выполняют Coq и (последние версии) Agda, которые запрещают любое появление T в его собственных индексах.
источник
Как подсказывают ваши собственные замечания, возможной причиной такой разницы является непредсказуемость. Исторически у Coq был непредсказуемый набор (все еще доступный как флаг, я верю!)
Цитирую книгу Адама Члипалы http://adam.chlipala.net/cpdt/html/Universes.html
источник