Corecursion - Corecursion

Na ciência da computação , a correcursão é um tipo de operação que é dual para a recursão . Enquanto a recursão funciona analiticamente, começando com dados mais distantes de um caso base e quebrando-os em dados menores e repetindo até chegar a um caso base, a correcursão funciona sinteticamente, começando a partir de um caso base e construindo-o, produzindo iterativamente dados ainda mais removidos de um caso base. Simplificando, os algoritmos correcursivos usam os dados que eles próprios produzem, pouco a pouco, à medida que se tornam disponíveis e são necessários para produzir mais bits de dados. Um conceito semelhante, mas distinto, é a recursão generativa, que pode carecer de uma "direção" definida inerente à correcursão e à recursão.

Onde a recursão permite que os programas operem em dados arbitrariamente complexos, desde que possam ser reduzidos a dados simples (casos de base), a correcursão permite que os programas produzam estruturas de dados arbitrariamente complexas e potencialmente infinitas, como fluxos , desde que possam ser produzidos de dados simples (casos básicos) em uma sequência de etapas finitas . Onde a recursão pode não terminar, nunca alcançando um estado de base, a correcursão começa a partir de um estado de base e, portanto, produz etapas subsequentes deterministicamente, embora possa prosseguir indefinidamente (e, portanto, não terminar sob avaliação estrita), ou pode consumir mais do que produz e assim tornar-se não produtivo . Muitas funções tradicionalmente analisadas como recursivas podem, alternativamente, e de forma mais natural, ser interpretadas como funções co-cursivas que são encerradas em um determinado estágio, por exemplo, relações de recorrência como o fatorial.

A correcursão pode produzir estruturas de dados finitas e infinitas como resultados e pode empregar estruturas de dados autorreferenciais . A correcursão é freqüentemente usada em conjunto com a avaliação preguiçosa , para produzir apenas um subconjunto finito de uma estrutura potencialmente infinita (em vez de tentar produzir uma estrutura infinita inteira de uma vez). A correcursão é um conceito particularmente importante na programação funcional , onde a correcursão e a codata permitem que linguagens totais trabalhem com estruturas de dados infinitas.

Exemplos

A correcursão pode ser entendida em contraste com a recursão, que é mais familiar. Embora a correcursão seja principalmente de interesse na programação funcional, ela pode ser ilustrada usando a programação imperativa, que é feita a seguir usando o gerador em Python. Nestes exemplos, variáveis ​​locais são usadas e valores atribuídos imperativamente (destrutivamente), embora estes não sejam necessários em correcursão em programação funcional pura. Na programação funcional pura, em vez de atribuir a variáveis ​​locais, esses valores calculados formam uma sequência invariável e os valores anteriores são acessados ​​por auto-referência (os valores posteriores na sequência fazem referência aos valores anteriores na sequência a ser computada). As atribuições simplesmente expressam isso no paradigma imperativo e especificam explicitamente onde os cálculos acontecem, o que serve para esclarecer a exposição.

Fatorial

Um exemplo clássico de recursão é computar o fatorial , que é definido recursivamente por 0! : = 1 e n! : = n × (n - 1)! .

Para calcular recursivamente seu resultado em uma determinada entrada, uma função recursiva chama (uma cópia de) a si mesma com uma entrada diferente ("menor" de alguma forma) e usa o resultado dessa chamada para construir seu resultado. A chamada recursiva faz o mesmo, a menos que o caso base tenha sido alcançado. Assim, uma pilha de chamadas se desenvolve no processo. Por exemplo, para calcular fac (3) , isso chama recursivamente, por sua vez, fac (2) , fac (1) , fac (0) ("encerrando" a pilha), ponto em que a recursão termina com fac (0) = 1 , e então a pilha se desenrola na ordem inversa e os resultados são calculados no caminho de volta ao longo da pilha de chamadas para o quadro de chamada inicial fac (3) que usa o resultado de fac (2) = 2 para calcular o resultado final como 3 × 2 = 3 × fac (2) =: fac (3) e finalmente retornar fac (3) = 6 . Neste exemplo, uma função retorna um único valor.

Este desenrolar da pilha pode ser explicado, definindo o fatorial correcursivamente , como um iterador , onde se começa com o caso de , a partir desse valor inicial constrói-se valores fatoriais para números crescentes 1, 2, 3 ... como na definição recursiva acima com "seta do tempo" invertida, por assim dizer, ao ser lida de trás para frente como . O algoritmo correcursivo assim definido produz um fluxo de todos os fatoriais. Isso pode ser implementado concretamente como um gerador . Simbolicamente, observando que o cálculo do próximo valor fatorial requer o acompanhamento de n e f (um valor fatorial anterior), isso pode ser representado como:

ou em Haskell ,

  (\(n,f) -> (n+1, f*(n+1))) `iterate` (0,1)

significando, "começando de , em cada etapa os próximos valores são calculados como ". Esta é matematicamente equivalente e quase idêntica à definição recursiva, mas a enfatiza que os valores fatoriais estão sendo construídas para cima , indo para a frente a partir do caso de começar, em vez de ser calculado após a primeira indo para trás, para baixo para o caso base, com um decréscimo. A saída direta da função correcursiva não contém simplesmente os valores fatoriais , mas também inclui para cada valor os dados auxiliares de seu índice n na sequência, de modo que qualquer resultado específico possa ser selecionado entre todos eles, como e quando necessário.

Existe uma conexão com a semântica denotacional , em que as denotações de programas recursivos são construídas corecursivamente dessa maneira.

Em Python, uma função fatorial recursiva pode ser definida como:

def factorial(n):
    """Recursive factorial function."""
    if n == 0:
        return 1
    else:
        return n * factorial(n - 1)

Isso poderia ser chamado, por exemplo, factorial(5) para calcular 5! .

Um gerador corecursivo correspondente pode ser definido como:

def factorials():
    """Corecursive generator."""
    n, f = 0, 1
    while True:
        yield f
        n, f = n + 1, f * (n + 1)

Isso gera um fluxo infinito de fatoriais em ordem; uma porção finita dele pode ser produzida por:

def n_factorials(k):
    n, f = 0, 1
    while n <= k:
        yield f
        n, f = n + 1, f * (n + 1)

Isso poderia então ser chamado para produzir os fatoriais de até 5! através da:

for f in n_factorials(5):
    print(f)

Se estamos interessados ​​apenas em um determinado fatorial, apenas o último valor pode ser obtido, ou podemos fundir a produção e o acesso em uma função,

def nth_factorial(k):
    n, f = 0, 1
    while n < k:
        n, f = n + 1, f * (n + 1)
    yield f

Como pode ser facilmente visto aqui, isso é praticamente equivalente (apenas substituindo return o único yield lá) à técnica de argumento do acumulador para recursão de cauda , desfeita em um loop explícito. Assim, pode-se dizer que o conceito de correcursão é uma explicação da incorporação de processos de computação iterativa por definições recursivas, quando aplicável.

Sequência de Fibonacci

Da mesma forma, a sequência de Fibonacci pode ser representada como:

Como a sequência de Fibonacci é uma relação de recorrência de ordem 2, a relação corecursiva deve rastrear dois termos sucessivos, com o correspondente a avançar um passo e o correspondente a calcular o próximo termo. Isso pode então ser implementado da seguinte forma (usando atribuição paralela ):

def fibonacci_sequence():
    a, b = 0, 1
    while True:
        yield a
        a, b = b, a + b

Em Haskell,

 map fst ( (\(a,b) -> (b,a+b)) `iterate` (0,1) )

Travessia de árvore

A travessia da árvore por meio de uma abordagem em primeiro lugar é um exemplo clássico de recursão. Dualmente, a travessia em amplitude pode ser implementada naturalmente por meio de correcursão.

Sem usar recursão ou correcursão especificamente, pode-se atravessar uma árvore começando no nó raiz, colocando seus nós-filhos em uma estrutura de dados e, em seguida, iterando removendo nó após nó da estrutura de dados, enquanto coloca cada filho do nó removido de volta nessa estrutura de dados . Se a estrutura de dados for uma pilha (LIFO), isso resultará em uma travessia em profundidade, e se a estrutura de dados for uma fila (FIFO), isso resultará em uma travessia em largura primeiro.

Usando a recursão, uma passagem de profundidade (pós-ordem) pode ser implementada começando no nó raiz e percorrendo recursivamente cada subárvore filha por vez (a subárvore baseada em cada nó filho) - a segunda subárvore filha não começa o processamento até que a primeira subárvore filho está concluída. Uma vez que um nó folha é alcançado ou os filhos de um nó de ramificação foram esgotados, o próprio nó é visitado (por exemplo, o valor do próprio nó é enviado). Nesse caso, a pilha de chamadas (das funções recursivas) atua como a pilha que é iterada.

Usando correcursão, uma travessia em largura pode ser implementada começando no nó raiz, emitindo seu valor e, em seguida, percorrendo em largura as subárvores - ou seja, passando toda a lista de subárvores para a próxima etapa (nem uma única subárvore, como na abordagem recursiva) - na próxima etapa, emitir o valor de todos os seus nós raiz e, em seguida, passar suas subárvores filhas etc. Nesse caso, a função geradora, na verdade a própria sequência de saída, atua como a fila. Como no exemplo fatorial (acima), onde as informações auxiliares do índice (em qual etapa um estava, n ) foram empurradas para frente, além da saída real de n !, Neste caso, as informações auxiliares das subárvores restantes são empurrado para a frente, além da saída real. Simbolicamente:

o que significa que em cada etapa, uma saída da lista de valores de nós raiz e, em seguida, prossegue para as subárvores filhas. Gerar apenas os valores de nó desta sequência simplesmente requer descartar os dados auxiliares da árvore filha e, em seguida, achatar a lista de listas (os valores são inicialmente agrupados por nível (profundidade); achatar (desagrupar) produz uma lista linear plana). Em Haskell,

 concatMap fst ( (\(v, t) -> (rootValues v t, childTrees t)) `iterate` ([], fullTree) )

Eles podem ser comparados da seguinte maneira. A travessia recursiva lida com um nó folha (na parte inferior ) como o caso base (quando não há filhos, apenas imprima o valor) e analisa uma árvore em subárvores, percorrendo cada uma por sua vez, resultando em apenas nós folha - folha real nós e nós de ramificação cujos filhos já foram tratados (corte abaixo ). Em contraste, a travessia corecursiva trata um nó raiz (no topo ) como o caso base (dado um nó, primeiro produza o valor), trata uma árvore como sendo sintetizada de um nó raiz e seus filhos, em seguida, produz como saída auxiliar um lista de subárvores em cada etapa, que são então a entrada para a próxima etapa - os nós filhos da raiz original são os nós raiz na próxima etapa, pois seus pais já foram tratados (corte acima ). Na travessia recursiva há uma distinção entre nós folha e nós de ramos, enquanto na travessia corecursiva não há distinção, já que cada nó é tratado como o nó raiz da subárvore que define.

Notavelmente, dada uma árvore infinita, a travessia corecursiva em largura primeiro percorrerá todos os nós, assim como em uma árvore finita, enquanto a travessia recursiva em profundidade descerá um galho e não percorrerá todos os nós, e de fato se percorrer pós-ordem , como neste exemplo (ou na ordem), ele não visitará nenhum nó, porque nunca alcançará uma folha. Isso mostra a utilidade da correcursão em vez da recursão para lidar com estruturas de dados infinitas.

Em Python, isso pode ser implementado da seguinte maneira. A travessia de profundidade normal pós-ordem pode ser definida como:

def df(node):
    """Post-order depth-first traversal."""
    if node is not None:
        df(node.left)
        df(node.right)
        print(node.value)

Isso pode então ser chamado por df(t) para imprimir os valores dos nós da árvore na ordem de profundidade inicial pós-ordem.

O gerador correcursivo de amplitude pode ser definido como:

def bf(tree):
    """Breadth-first corecursive generator."""
    tree_list = [tree]
    while tree_list:
        new_tree_list = []
        for tree in tree_list:
            if tree is not None:
                yield tree.value
                new_tree_list.append(tree.left)
                new_tree_list.append(tree.right)
        tree_list = new_tree_list

Isso pode ser chamado para imprimir os valores dos nós da árvore na ordem de largura:

for i in bf(t):
    print(i)

Definição

Os tipos de dados iniciais podem ser definidos como sendo o menor ponto fixo ( até isomorfismo ) de algum tipo de equação; o isomorfismo é então dado por uma álgebra inicial . Dualmente, os tipos de dados finais (ou terminais) podem ser definidos como sendo o maior ponto de fixação de uma equação de tipo; o isomorfismo é então dado por uma coalgebra final .

Se o domínio do discurso é a categoria de conjuntos e funções totais, os tipos de dados finais podem conter valores infinitos e não bem fundamentados, ao passo que os tipos iniciais não. Por outro lado, se o domínio do discurso é a categoria de ordens parciais completas e funções contínuas , que corresponde aproximadamente à linguagem de programação Haskell , então os tipos finais coincidem com os tipos iniciais, e a coalgebra final correspondente e a álgebra inicial formam um isomorfismo.

A corecursão é, então, uma técnica para definir recursivamente funções cujo intervalo (codomínio) é um tipo de dados final, dual do modo como a recursão comum define recursivamente funções cujo domínio é um tipo de dados inicial.

A discussão abaixo fornece vários exemplos em Haskell que distinguem a correcursão. Grosso modo, se alguém tivesse que transportar essas definições para a categoria de conjuntos, elas ainda seriam correcursivas. Este uso informal é consistente com os livros existentes sobre Haskell. Os exemplos usados ​​neste artigo são anteriores às tentativas de definir correcursão e explicar o que ela é.

Discussão

A regra para a correcursão primitiva em codata é dual para a recursão primitiva em dados. Em vez de descer no argumento por correspondência de padrões em seus construtores (que foram chamados antes , em algum lugar, então recebemos um dado pronto e obtemos suas subpartes constituintes, ou seja, "campos"), ascendemos no resultado preenchendo seus "destruidores" (ou "observadores", que serão chamados depois , em algum lugar - então, na verdade, estamos chamando um construtor, criando outra parte do resultado a ser observada mais tarde). Assim, a correcursão cria codata (potencialmente infinita), enquanto a recursão ordinária analisa dados (necessariamente finitos). A recursão ordinária pode não ser aplicável aos codados porque pode não terminar. Por outro lado, a correcursão não é estritamente necessária se o tipo de resultado for dados, porque os dados devem ser finitos.

Em "Programação com fluxos em Coq: um estudo de caso: a peneira de Eratóstenes" encontramos

hd (conc a s) = a               
tl (conc a s) = s

(sieve p s) = if div p (hd s) then sieve p (tl s)
              else conc (hd s) (sieve p (tl s))

hd (primes s) = (hd s)          
tl (primes s) = primes (sieve (hd s) (tl s))

onde os primos "são obtidos aplicando a operação de primos ao fluxo (Enu 2)". Seguindo a notação acima, a sequência de primos (com um zero descartável prefixado a ele) e os fluxos de números sendo peneirados progressivamente podem ser representados como

ou em Haskell,

(\(p, s@(h:t)) -> (h, sieve h t)) `iterate` (0, [2..])

Os autores discutem como a definição de sieve nem sempre é garantida como produtiva e pode ficar presa, por exemplo, se chamada com [5,10..] como o fluxo inicial.

Aqui está outro exemplo em Haskell. A seguinte definição produz a lista de números de Fibonacci em tempo linear:

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

Essa lista infinita depende de avaliação preguiçosa; os elementos são calculados conforme a necessidade e apenas prefixos finitos são explicitamente representados na memória. Esse recurso permite que algoritmos em partes de codata sejam encerrados; tais técnicas são uma parte importante da programação Haskell.

Isso também pode ser feito em Python:

from itertools import tee, chain, islice, imap

def add(x, y):
    return x + y

def fibonacci():
    def deferred_output():
        for i in output:
            yield i
    result, c1, c2 = tee(deferred_output(), 3)
    paired = imap(add, c1, islice(c2, 1, None))
    output = chain([0, 1], paired)
    return result

for i in islice(fibonacci(), 20):
    print(i)

A definição de zipWith pode ser embutida, levando a isto:

fibs = 0 : 1 : next fibs
  where
    next (a: t@(b:_)) = (a+b):next t

Este exemplo emprega uma estrutura de dados autorreferencial . A recursão comum faz uso de funções autorreferenciais , mas não acomoda dados autorreferenciais. No entanto, isso não é essencial para o exemplo de Fibonacci. Ele pode ser reescrito da seguinte forma:

fibs = fibgen (0,1)
fibgen (x,y) = x : fibgen (y,x+y)

Isso emprega apenas uma função autorreferencial para construir o resultado. Se fosse usado com o construtor de lista estrita, seria um exemplo de recursão descontrolada, mas com o construtor de lista não estrita, essa recursão protegida produz gradualmente uma lista definida indefinidamente.

A correcursão não precisa produzir um objeto infinito; uma fila correcursiva é um exemplo particularmente bom desse fenômeno. A definição a seguir produz uma travessia em largura de uma árvore binária em tempo linear:

data Tree a b = Leaf a  |  Branch b (Tree a b) (Tree a b)

bftrav :: Tree a b -> [Tree a b]
bftrav tree = queue
  where
    queue = tree : gen 1 queue

    gen  0   p                 =         []           
    gen len (Leaf   _     : s) =         gen (len-1) s 
    gen len (Branch _ l r : s) = l : r : gen (len+1) s

Esta definição pega uma árvore inicial e produz uma lista de subárvores. Essa lista tem um duplo propósito como fila e como resultado ( gen len p produz seus len entalhes de saída após seu ponteiro de retorno de entrada,, p junto com queue ). É finito se e somente se a árvore inicial for finita. O comprimento da fila deve ser rastreado explicitamente para garantir o encerramento; isso pode ser eliminado com segurança se essa definição for aplicada apenas a árvores infinitas.

Outro exemplo particularmente bom dá uma solução para o problema da rotulagem em primeiro lugar. A função label visita cada nó em uma árvore binária em uma amplitude primeiro e substitui cada rótulo por um inteiro, cada inteiro subsequente é maior que o último por um. Esta solução emprega uma estrutura de dados autorreferencial e a árvore binária pode ser finita ou infinita.

label :: Tree a b -> Tree Int Int 
label t = t
    where
    (t, ns) = go t (1:ns)

    go :: Tree a b    -> [Int]  -> (Tree Int Int, [Int])
    go   (Leaf   _    ) (n:ns) = (Leaf   n       , n+1 : ns  )
    go   (Branch _ l r) (n:ns) = (Branch n l r , n+1 : ns′′)
                                where
                                  (l, ns ) = go l ns
                                  (r, ns′′) = go r ns

Um apomorfismo (como um anamorfismo , como desdobrar ) é uma forma de correcursão da mesma forma que um paramorfismo (como um catamorfismo , como dobra ) é uma forma de recursão.

O assistente de prova Coq suporta correcursão e coindução usando o comando CoFixpoint.

História

A correcursão, conhecida como programação circular, data pelo menos de ( Bird 1984 ), que credita John Hughes e Philip Wadler ; formas mais gerais foram desenvolvidas em ( Allison 1989 ) . As motivações originais incluíam a produção de algoritmos mais eficientes (permitindo uma passagem de dados em alguns casos, em vez de exigir várias passagens) e a implementação de estruturas de dados clássicas, como listas e filas duplamente vinculadas, em linguagens funcionais.

Veja também

Notas

Referências