Como derivar eliminadores de tipo dependente?

Na programação de tipo dependente, existem duas maneiras principais de decompor dados e executar recursão:

Correspondência de padrões dependentes : as definições de funções são fornecidas como várias cláusulas. A unificação garante que todos os casos omitidos sejam impossíveis e um solucionador externo garante que a recursão seja bem fundamentada.
Eliminadores : Cada indutivo tipo de dados tem uma constante associado , que actua como um princípio de indução, e como função recursiva que se decompõe valores do tipo . Eles são mais detalhados, mas têm a vantagem de serem totais (todos os casos são cobertos por ) e finalizados por construção. $D$ $E_D$ $D$ $E_D$

Eu já vi eliminadores para tipos de dados comuns, como , onde o eliminador é basicamente indução matemática, ou , onde o eliminador é basicamente uma dobra. $Nat$ $List$

Eu tenho lido vários artigos sobre correspondência de padrões dependentes, e muitos se referem a teorias de tipos nas quais tipos de dados podem ser definidos e eliminadores são fornecidos pela teoria. Por exemplo, Eliminando Dependente Matching Padrão descreve como UTT é baseado em eliminadores, e como padrão de correspondência pode ser convertido para eliminação na presença de axioma . Meu entendimento é que, uma vez definido um tipo de dados, a teoria fornece o eliminador. $K$

O que eu não encontrei (ou pelo menos não reconheci se o vi) é uma boa descrição de como se pode derivar os eliminadores, tanto seus tipos quanto suas semânticas.

Alguém pode me indicar uma referência que descreva como se pode obter um eliminador a partir da definição de um tipo de dados?

reference-request recursion type-theory dependent-types inductive-datatypes jmite
fonte

Tenho certeza de que há uma descrição no cálculo de construções ou na literatura Coq (para tipos estritamente positivos - os eliminadores de Coq em tipos mais complexos não são totalmente gerais).

Gilles 'SO- stop be evil'

@Gilles Meu entendimento era que a Coq não usava eliminadores, mas sim operadores separados de correspondência e de correção (protegidos).

jmite

A linguagem principal não usa eliminadores, mas quando você define um tipo, o Coq gera um eliminador, definido em termos de fixe match. Não tenho uma referência em mãos, mas sei que li algo sobre como esse eliminador é gerado. cs.stackexchange.com/questions/104/… pode ser de seu interesse.

Gilles 'SO- stop be evil'

Para qualquer tipo indutivo T, a Coq define um princípio de indução T_indque é um eliminador dependente. Isso é definido em termos de recursão e correspondência de padrões, mas você pode, em princípio, assumi-la como uma nova constante, tendo o mesmo tipo (com a mesma semântica).

chi

Como derivar eliminadores de tipo dependente?

Respostas: