В зависимо-типизированном программировании есть два основных способа разложения данных и выполнения рекурсии:
- Зависимое сопоставление с образцом : определения функций приведены в виде нескольких предложений. Унификация гарантирует, что все пропущенные случаи невозможны, а внешний решатель гарантирует, что рекурсия обоснована.
- Сепараторы : Каждый индуктивный тип данных имеет ассоциированный константу Е D , который действует в качестве принципа индукции, а также рекурсивной функции , которые разлагаются значения типа D . Они более многословны, но имеют преимущество в том, что они полные (все случаи охватываются E D ) и заканчиваются конструкцией.
Я видел элиминаторы для распространенных типов данных, таких как , где элиминатор - это в основном математическая индукция, или L i s t , где элиминатор - это в основном сгиб.
Я читал несколько статей о зависимом сопоставлении с образцом, и многие ссылаются на теории типов, в которых могут быть определены типы данных, и теория обеспечивает элиминаторы. Например, устранение зависимого шаблона согласования описывает , как ЕТТ основан на элиминаторах, и как сопоставление с образцом может быть преобразовано в устранение в присутствии аксиомы . Насколько я понимаю, как только тип данных определен, теория обеспечивает элиминатор.
То, что я не нашел (или, по крайней мере, не узнал, видел ли я это), является хорошим описанием того, как можно получить элиминаторы, как их типы, так и их семантику.
Может кто-то указать мне ссылку, которая описывает, как можно получить элиминатор из определения типа данных?
fix
иmatch
. У меня нет под рукой ссылки, но я знаю, что прочитал кое-что о том, как генерируется этот элиминатор. cs.stackexchange.com/questions/104/… может представлять интерес.T
Coq определяет принцип индукции,T_ind
который является зависимым элиминатором. Это определяется с точки зрения рекурсии и сопоставления с образцом, но в принципе вы можете предположить, что это новая константа того же типа (с той же семантикой).Ответы:
Каноническая ссылка на это - Питер Дибджер, « Индуктивные семьи» , который дает довольно всеобъемлющий подход к индуктивным семьям на основе элиминаторов.
источник
Вы можете найти некоторые из наших недавних работ по этому вопросу полезными, поскольку мы выводим элиминаторы для лямбда-кодированных типов данных. Например, см этого один для общего вывода элиминаторов, и это один для основного метода применяются только к Nat типа.
источник