Tipo de dados recursivos - Recursive data type

Em linguagens de programação de computador , um tipo de dados recursivo (também conhecido como tipo de dados definido recursivamente , indutivamente definido ou indutivo ) é um tipo de dados para valores que podem conter outros valores do mesmo tipo. Dados de tipos recursivos são geralmente vistos como gráficos direcionados .

Uma aplicação importante da recursão na ciência da computação é a definição de estruturas de dados dinâmicas, como listas e árvores. Estruturas de dados recursivas podem crescer dinamicamente até um tamanho arbitrariamente grande em resposta aos requisitos de tempo de execução; em contraste, os requisitos de tamanho de um array estático devem ser definidos em tempo de compilação.

Às vezes, o termo "tipo de dados indutivo" é usado para tipos de dados algébricos que não são necessariamente recursivos.

Exemplo

Um exemplo é o tipo de lista , em Haskell :

data List a = Nil | Cons a (List a)

Isso indica que uma lista de a's é uma lista vazia ou uma célula cons contendo um 'a' (a "cabeça" da lista) e outra lista (a "cauda").

Outro exemplo é um tipo semelhante com link único em Java:

class List<E> {
    E value;
    List<E> next;
}

Isso indica que a lista não vazia do tipo E contém um membro de dados do tipo E e uma referência a outro objeto List para o resto da lista (ou uma referência nula para indicar que este é o fim da lista).

Tipos de dados mutuamente recursivos

Os tipos de dados também podem ser definidos por recursão mútua . O exemplo básico mais importante disso é uma árvore , que pode ser definida mutuamente recursivamente em termos de uma floresta (uma lista de árvores). Simbolicamente:

f: [t[1], ..., t[k]]
t: v f

Uma floresta f consiste em uma lista de árvores, enquanto uma árvore t consiste em um par de um valor v e uma floresta f (seus filhos). Esta definição é elegante e fácil de trabalhar abstratamente (como ao provar teoremas sobre propriedades de árvores), pois expressa uma árvore em termos simples: uma lista de um tipo e um par de dois tipos.

Esta definição mutuamente recursiva pode ser convertida em uma definição recursiva única ao in-line a definição de uma floresta:

t: v [t[1], ..., t[k]]

Uma árvore t consiste em um par de um valor v e uma lista de árvores (seus filhos). Essa definição é mais compacta, mas um pouco mais confusa: uma árvore consiste em um par de um tipo e uma lista de outro, que exigem o desemaranhamento para comprovar os resultados.

No ML padrão , os tipos de dados de árvore e floresta podem ser recursivamente definidos mutuamente da seguinte forma, permitindo árvores vazias:

datatype 'a tree = Empty | Node of 'a * 'a forest
and      'a forest = Nil | Cons of 'a tree * 'a forest

Em Haskell, os tipos de dados de árvore e floresta podem ser definidos de forma semelhante:

data Tree a = Empty
            | Node (a, Forest a)

data Forest a = Nil
              | Cons (Tree a) (Forest a)

Teoria

Na teoria dos tipos , um tipo recursivo tem a forma geral μα.T onde a variável de tipo α pode aparecer no tipo T e representa o próprio tipo inteiro.

Por exemplo, os números naturais (consulte a aritmética de Peano ) podem ser definidos pelo tipo de dados Haskell:

data Nat = Zero | Succ Nat

Em teoria de tipos, diríamos: onde os dois braços do tipo soma representam os construtores de dados Zero e Succ. Zero não leva nenhum argumento (portanto, representado pelo tipo de unidade ) e Succ leva outro Nat (portanto, outro elemento de ). ${\ displaystyle nat = \ mu \ alpha .1+ \ alpha}$ ${\ displaystyle \ mu \ alpha .1+ \ alpha}$

Existem duas formas de tipos recursivos: os chamados tipos isorrecursivos e os tipos equirecursivos. As duas formas diferem em como os termos de um tipo recursivo são introduzidos e eliminados.

Tipos isorrecursivos

Com os tipos isorrecursivos, o tipo recursivo e sua expansão (ou desenrolamento ) (onde a notação indica que todas as instâncias de Z são substituídas por Y em X) são tipos distintos (e disjuntos) com construções de termos especiais, geralmente chamados de roll and unroll , que formam um isomorfismo entre eles. Para ser mais preciso: e , e essas duas são funções inversas . ${\ displaystyle \ mu \ alpha .T}$ ${\ displaystyle T [\ mu \ alpha .T / \ alpha]}$ ${\ displaystyle X [Y / Z]}$ ${\ displaystyle roll: T [\ mu \ alpha .T / \ alpha] \ to \ mu \ alpha .T}$ ${\ displaystyle unroll: \ mu \ alpha .T \ to T [\ mu \ alpha .T / \ alpha]}$

Tipos equirecursivos

Sob regras equirecursivas, um tipo recursivo e seu desenrolamento são iguais - ou seja, essas duas expressões de tipo são entendidas como denotando o mesmo tipo. Na verdade, a maioria das teorias de tipos equirecursivos vão além e essencialmente especificam que quaisquer duas expressões de tipo com a mesma "expansão infinita" são equivalentes. Como resultado dessas regras, os tipos equirecursivos contribuem significativamente com mais complexidade para um sistema de tipos do que os tipos isorrecursivos. Problemas de algoritmo como verificação de tipo e inferência de tipo também são mais difíceis para tipos equirecursivos. Como a comparação direta não faz sentido em um tipo equirecursivo, eles podem ser convertidos em uma forma canônica no tempo O (n log n), que pode ser facilmente comparado. ${\ displaystyle \ mu \ alpha .T}$ ${\ displaystyle T [\ mu \ alpha .T / \ alpha]}$

Tipos equirecursivos capturam a forma de definições de tipo autorreferenciais (ou mutuamente referenciais) vistas em linguagens de programação orientadas a objetos e procedurais , e também surgem na semântica teórica de tipos de objetos e classes . Em linguagens de programação funcional, os tipos isorrecursivos (na forma de tipos de dados) são muito mais comuns.

Em sinônimos de tipo

A recursão não é permitida em sinônimos de tipo em Miranda , OCaml (a menos que o -rectypessinalizador seja usado ou seja um registro ou variante) e Haskell; então, por exemplo, os seguintes tipos de Haskell são ilegais:

type Bad = (Int, Bad)
type Evil = Bool -> Evil

Em vez disso, deve ser encapsulado em um tipo de dados algébrico (mesmo que tenha apenas um construtor):

data Good = Pair Int Good
data Fine = Fun (Bool -> Fine)

Isso ocorre porque sinônimos de tipo, como typedefs em C, são substituídos por sua definição em tempo de compilação. (Os sinônimos de tipo não são tipos "reais"; eles são apenas "apelidos" para conveniência do programador.) Mas se isso for tentado com um tipo recursivo, ele fará um loop infinito porque não importa quantas vezes o apelido seja substituído, ele ainda refere-se a si mesmo, por exemplo, "Ruim" aumentará indefinidamente: Bad→ (Int, Bad)→ (Int, (Int, Bad))→ ....

Outra maneira de ver isso é que um nível de indireção (o tipo de dados algébrico) é necessário para permitir que o sistema de tipo isorrecursivo descubra quando rolar e desenrolar .

Veja também

Notas

Este artigo é baseado em material retirado do Dicionário On-line Gratuito de Computação anterior a 1 de novembro de 2008 e incorporado sob os termos de "relicenciamento" do GFDL , versão 1.3 ou posterior.

Languages

In other projects