Como derivar eliminadores de tipo dependente?

10

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.DEDDED

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.NatList

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?

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
3
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

Respostas:

8

A referência canônica para isso é Peter Dybjer, Famílias Indutivas , que oferece um tratamento bastante abrangente de famílias indutivas baseadas em eliminadores.

cody
fonte
6

Você pode encontrar alguns de nossos artigos recentes sobre isso úteis, pois derivamos eliminadores para tipos de dados codificados por lambda. Por exemplo, veja este um para derivação genérico de eliminadores, e este um para a técnica básica aplicada apenas para o tipo Nat.

Aaron Stump
fonte