Definindo funções recursivas primitivas sobre tipos de dados gerais

9

As funções recursivas primitivas são definidas sobre os números naturais. No entanto, parece que o conceito deve generalizar para outros tipos de dados, permitindo falar sobre funções recursivas primitivas que mapeiam listas para árvores binárias, por exemplo. Por analogia, funções recursivas parciais sobre os números naturais generalizam bem para funções computáveis ​​em qualquer tipo de dados, e eu gostaria de entender como fazer o mesmo tipo de generalização para funções recursivas primitivas.

Intuitivamente, se eu definisse uma linguagem imperativa simples que permitisse operações básicas, digamos listas (como concatenação, aceitação e comparação, comparação de elementos) e uma forma de iteração que requer saber antecipadamente quantas iterações ocorrerão ( como iterar sobre os elementos em uma lista imutável), essa linguagem deve, no máximo, ser capaz de calcular as funções recursivas primitivas nas listas. Mas como posso entender isso formalmente, e mais especificamente, como eu provaria que minha linguagem calcula todas as funções recursivas primitivas em listas e não apenas um subconjunto delas?

Para ser claro, estou interessado em entender as funções recursivas primitivas como uma classe bem definida de funções (se é que elas são), em vez de apenas na operação da recursão primitiva em si, o que parece direto. Eu estaria interessado em apontadores para qualquer coisa que tenha sido escrita sobre recursão primitiva sobre estruturas de dados gerais, ou mesmo em qualquer contexto que não seja o número natural.

atualização: Talvez eu tenha encontrado uma resposta, em um artigo chamado Walther Recursion , de McAllester e Arkoudas. (Procedimentos do CADE 1996. ) Isso parece conter uma versão generalizada da recursão primitiva, bem como a recursão mais poderosa de Walther. Pretendo escrever uma resposta automática depois de digeri isso, mas, enquanto isso, essa nota pode ser útil para outras pessoas com a mesma pergunta.

Nathaniel
fonte
11
Não está claro para mim o que exatamente você está procurando. Parece que você está apenas tentando encontrar tipos W , mas pode não ser isso.
Andrej Bauer
3
Provavelmente, é útil observar que tipos de dados "comuns" (semelhantes a árvores) podem ser codificados de maneira bastante direta em números naturais e, em seguida, as funções de PR sobre os naturais são uma representação muito boa do que você pode querer. Como alternativa, você pode usar o System T da Gödel estendido aos tipos de dados estritamente positivos de primeira ordem com os recursores "usuais".
Cody
11
Você pode restringir os tipos de saída dos eliminadores a tipos básicos, se desejar eliminar esse "recurso".
Cody
11
Ainda me parece que uma forma restrita de tipos W é o que você está procurando. Algo como os tipos W com ramificação finita e os recursores limitados à eliminação para outros tipos W restritos.
Andrej Bauer
11
Visite a conferência do CADE em 1996 aqui: dblp.org/db/conf/cade/cade96
John Fisher

Respostas:

5

Em geral, em uma linguagem com tipos de dados (como listas, árvores etc.), é fácil descrever uma linguagem de funções que se comporta exatamente como esperamos que a recursão primitiva se comporte.

Por exemplo, se o tipo de dados for e os construtores c 1 , , c n tiverem o tipoDc1,,cn

cEu:T1 1EuT2Eu...Tk1 1EuD...D

o recursor para o tipo de saída terá o tipo OrecDOO

recDO:(T1 11 1...Tk1 11 1D...DO...O)...DO

e a semântica operacional será:

recDO f1 1 ... fn (cEu t1 1...tkEu d1 1...dm)fEu t1 1...tkEu (recDO f1 1... fn d1 1)...(recDO f1 1...fn dm)

para cada .Eu

Algo de boca cheia! Pelo menos para números naturais, realmente obtemos

recNO:(NOO)ONO

r e c O N f 0 f 1 (Sn) f 0 n( r e c O N f 0 f 1 n)

recNO f0 0 f1 1 0 0f1 1 0 0
e
recNO f0 0 f1 1 (S n)f0 0 n (recNO f0 0 f1 1 n)

como esperado (observe que o construtor zero tem zero argumentos!).

Se agora permitimos funções e projeções constantes e utilizações arbitrárias de para tipos não funcionais , então você tem uma recursão exatamente primitiva. OrecDOO

De forma tranquilizadora, se todos os também não são funcionais, a codificação Gödel usual do tipo de dados fornece as mesmas funções recursivas primitivas.TEuj


Seria bom ter uma descrição mais elegante desse processo. Foi aí que a resposta de Carlos entrou: esses tipos de dados podem ser descritos com mais elegância na teoria das categorias como as álgebras iniciais de certos functores, geralmente chamados de polinomiais . O recursor é então apenas (uma variante) do morfismo inicial dessa álgebra, às vezes chamado de catamorfismo por pessoas que tentam confundir as coisas. Esse morfismo existe pela construção da álgebra inicial.

Um paramorfismo é apenas a variante específica que descrevi acima.

cody
fonte
Receio que isso esteja um pouco além de mim. Por que esperávamos obter como o tipo assinatura? Isso significa automaticamente que representa recursividade primitiva? (Não consigo imaginar como isso poderia ser lido apenas do tipo de uma função.) Conheço a teoria dos tipos na medida em que posso programar em Haskell, mas não conheço o formalismo que você tem ' re usando aqui. Onde posso ler antecedentes suficientes para entender o que você escreveu? recNO:(NOO)ONO
Nathaniel
O tipo de segue o esquema mais geral acima. Representa a recursividade primitiva porque a semântica operacional representa a operação de recursão a partir da definição de funções de PR. Não expliquei a semântica operacional, portanto, expandirei meu comentário. recN
Cody
Não tenho nenhuma referência elementar de antemão, embora eu ache que esses slides sejam uma boa introdução, e o capítulo 3 da tese de Ralph Mattes entra em enormes detalhes técnicos, embora permita tipos indutivos não de "primeira ordem".
Cody
2

Recentemente, eu estava fazendo essa mesma pergunta e encontrei vários artigos de interesse:

Lógicas Apresentadas Indutivamente Finitárias : (a) define uma lógica que fornece uma noção genérica de recursão primitiva sobre qualquer tipo de dados que satisfaça certos requisitos (b) prova que essa lógica é uma extensão conservadora da aritmética recursiva primitiva.

A complexidade dos programas de loop : prova que sua noção de programa de loop é equivalente às funções recursivas primitivas.

Programas lógicos para conjuntos recursivos primitivos : prova que sua classe de programas lógicos é equivalente a funções recursivas primitivas.

Uma caracterização teórica da prova das funções primitivas do conjunto recursivo : prova que todas as funções recursivas primitivas de um determinado conjunto são exatamente aquelas definíveis em uma teoria muito fraca dos conjuntos.

Stephen Skeirik
fonte
0

Talvez você esteja pensando no conceito de um paramorfismo ?

Da programação funcional com bananas, lentes, envelopes e arame farpado :

h=(b,)

h0 0=bh(n+1 1)=n(hn)

b=1 1nm=(n+1 1)×m

h

hnada=bh(contrasumab)=uma(b,hb)
user76284
fonte