Combinador de ponto fixo - Fixed-point combinator

Na matemática e na ciência da computação em geral, um ponto fixo de uma função é um valor mapeado para si mesmo pela função.

Na lógica combinatória para ciência da computação , um combinador de ponto fixo (ou combinator fixpoint ) é uma função de ordem superior que retorna algum ponto fixo de sua função argumento, se houver.

Formalmente, se a função f tem um ou mais pontos fixos, então

e, portanto, por aplicação repetida,

Combinador Y

No cálculo lambda clássico sem tipo , cada função tem um ponto fixo.

Uma implementação particular de correção é o combinador Y paradoxal de Curry , representado por

Na programação funcional , o combinador Y pode ser usado para definir formalmente funções recursivas em uma linguagem de programação que não oferece suporte à recursão.

Este combinador pode ser usado na implementação do paradoxo de Curry . O cerne do paradoxo de Curry é que o cálculo lambda não tipado é incorreto como sistema dedutivo, e o combinador Y demonstra isso ao permitir que uma expressão anônima represente zero, ou mesmo muitos valores. Isso é inconsistente na lógica matemática.

Aplicado a uma função com uma variável, o combinador Y geralmente não termina. Resultados mais interessantes são obtidos aplicando o combinador Y a funções de duas ou mais variáveis. A segunda variável pode ser usada como contador ou índice. A função resultante se comporta como um loop while ou for em uma linguagem imperativa.

Usado dessa forma, o combinador Y implementa recursão simples. No cálculo lambda não é possível referir-se à definição de uma função em um corpo de função. A recursão só pode ser alcançada passando uma função como parâmetro. O combinador Y demonstra esse estilo de programação.

Combinador de ponto fixo

O combinador Y é uma implementação de um combinador de ponto fixo no cálculo lambda. Os combinadores de ponto fixo também podem ser facilmente definidos em outras linguagens funcionais e imperativas. A implementação no cálculo lambda é mais difícil devido às limitações do cálculo lambda. O combinador de ponto fixo pode ser usado em várias áreas diferentes:

Os combinadores de ponto fixo podem ser aplicados a uma gama de funções diferentes, mas normalmente não terminarão a menos que haja um parâmetro extra. Quando a função a ser corrigida se refere ao seu parâmetro, outra chamada para a função é invocada, de forma que o cálculo nunca seja iniciado. Em vez disso, o parâmetro extra é usado para acionar o início do cálculo.

O tipo de ponto fixo é o tipo de retorno da função que está sendo corrigida. Este pode ser um real, uma função ou qualquer outro tipo.

No cálculo lambda não tipado, a função para aplicar o combinador de ponto fixo pode ser expressa usando uma codificação, como a codificação de Church . Nesse caso, termos lambda específicos (que definem funções) são considerados valores. "Executando" (redução beta) o combinador de ponto fixo na codificação fornece um termo lambda para o resultado que pode então ser interpretado como valor de ponto fixo.

Alternativamente, uma função pode ser considerada como um termo lambda definido puramente no cálculo lambda.

Essas diferentes abordagens afetam como um matemático e um programador podem considerar um combinador de ponto fixo. Um matemático de cálculo lambda pode ver o combinador Y aplicado a uma função como sendo uma expressão que satisfaz a equação de ponto fixo e, portanto, uma solução.

Em contraste, uma pessoa que deseja apenas aplicar um combinador de ponto fixo a alguma tarefa de programação geral pode vê-lo apenas como um meio de implementar recursão.

Valores e domínios

Cada expressão tem um valor. Isso é verdade na matemática geral e deve ser verdade no cálculo lambda. Isso significa que, no cálculo lambda, a aplicação de um combinador de ponto fixo a uma função fornece uma expressão cujo valor é o ponto fixo da função.

No entanto, este é um valor no domínio do cálculo lambda , ele pode não corresponder a nenhum valor no domínio da função, então em um sentido prático não é necessariamente um ponto fixo da função, e apenas no domínio do cálculo lambda é é um ponto fixo da equação.

Por exemplo, considere

A divisão de números assinados pode ser implementada na codificação da Igreja, portanto, f pode ser representado por um termo lambda. Esta equação não tem solução nos números reais. Mas no domínio dos números complexos i e -i são soluções. Isso demonstra que pode haver soluções para uma equação em outro domínio. No entanto, o termo lambda para a solução da equação acima é mais estranho do que isso. O termo lambda representa o estado em que x pode ser i ou -i , como um valor. A informação que distingue estes dois valores foi perdida, na mudança de domínio.

Para o matemático de cálculo lambda, isso é uma consequência da definição de cálculo lambda. Para o programador, significa que a redução beta do termo lambda fará um loop para sempre, nunca alcançando uma forma normal.

Função versus implementação

O combinador de ponto fixo pode ser definido em matemática e então implementado em outras linguagens. A matemática geral define uma função com base em suas propriedades extensionais . Ou seja, duas funções são iguais se executam o mesmo mapeamento. O cálculo lambda e as linguagens de programação consideram a identidade da função como uma propriedade intensional . A identidade de uma função é baseada em sua implementação.

Uma função de cálculo lambda (ou termo) é uma implementação de uma função matemática. No cálculo lambda, há vários combinadores (implementações) que satisfazem a definição matemática de um combinador de ponto fixo.

O que é um "combinador"?

A lógica combinatória é uma teoria das funções de ordem superior . Um combinador é uma expressão lambda fechada , o que significa que não possui variáveis ​​livres. Os combinadores podem ser combinados para direcionar os valores para seus lugares corretos na expressão, sem nunca nomeá-los como variáveis.

Uso na programação

Os combinadores de ponto fixo podem ser usados ​​para implementar a definição recursiva de funções. No entanto, eles raramente são usados ​​na programação prática. Sistemas de tipo fortemente normalizados , como o cálculo lambda simplesmente tipado, não permitem a não terminação e, portanto, combinadores de ponto fixo geralmente não podem ser atribuídos a um tipo ou requerem recursos de sistema de tipo complexo. Além disso, os combinadores de ponto fixo são frequentemente ineficientes em comparação com outras estratégias para implementar recursão, uma vez que requerem mais reduções de função e constroem e desmontam uma tupla para cada grupo de definições mutuamente recursivas.

A função fatorial

A função fatorial fornece um bom exemplo de como o combinador de ponto fixo pode ser aplicado. O resultado demonstra recursão simples, como seria implementado em um único loop em uma linguagem imperativa. A definição dos números usados ​​é explicada em Church encoding .

A função que se assume como parâmetro é

Isso dá YF n como

Configuração dá

Esta definição coloca F no papel de corpo de um loop a ser iterado e é equivalente à definição matemática de fatorial:

Combinadores de ponto fixo em cálculo lambda

O combinador Y , descoberto por Haskell B. Curry , é definido como

A redução beta disso dá:

(por definição de Y )
(por β-redução de λf: aplicado Y a g)
(por β-redução de λx: função esquerda aplicada à função direita)
(por segunda igualdade)

A aplicação repetida desta igualdade dá:

(A igualdade acima deve ser pensada como uma sequência de reduções β de várias etapas da esquerda para a direita. O termo lambda não pode, em geral, reduzir β ao termo . Em vez disso, pode-se interpretar os sinais de igualdade como equivalências β de reduções β de várias etapas para permitir ir em ambas as direções.)

Definição equivalente de um combinador de ponto fixo

Este combinador de ponto fixo pode ser definido como y , como em

Uma expressão para y pode ser derivada usando regras da definição de uma expressão let . Em primeiro lugar, usando a regra

Além disso, usando

E então, usando a regra de redução eta ,

Derivação do combinador Y

O combinador Y de Curry pode ser facilmente obtido a partir da definição de y .

Começando com,

Uma abstração lambda não suporta referência ao nome da variável, na expressão aplicada, então x deve ser passado como um parâmetro para x . Podemos pensar nisso como substituir x por xx , mas formalmente isso não é correto. Em vez de definir y por dá

A expressão let pode ser considerada como a definição da função y , onde z é o parâmetro. A instanciação z como y na chamada dá

E, como o parâmetro z sempre passa pela função y ,

Usando a regra de redução eta ,

Uma expressão let pode ser expressa como uma abstração lambda ; usando

Esta é possivelmente a implementação mais simples de um combinador de ponto fixo no cálculo lambda. No entanto, uma redução beta dá a forma mais simétrica do combinador Y de Curry:

Consulte também Traduzindo entre expressões let e lambda .

Outros combinadores de ponto fixo

No cálculo lambda não tipado, os combinadores de ponto fixo não são especialmente raros. Na verdade, existem infinitamente muitos deles. Em 2005, Mayer Goldberg mostrou que o conjunto de combinadores de ponto fixo do cálculo lambda não tipado é recursivamente enumerável .

O combinador Y pode ser expresso no cálculo SKI como

O combinador de ponto fixo mais simples no cálculo SK, encontrado por John Tromp , é

embora note que não está na forma normal, que é mais longa. Este combinador corresponde à expressão lambda

O seguinte combinador de ponto fixo é mais simples do que o combinador Y, e β-reduz no combinador Y; às vezes é citado como o próprio combinador Y:

Outro combinador de ponto fixo comum é o combinador de ponto fixo de Turing (nomeado após seu descobridor, Alan Turing ):

Sua vantagem é que beta reduz para , enquanto que e somente beta reduz para um termo comum.

também tem um formulário simples de chamada por valor:

O análogo para recursão mútua é um combinador de ponto fixo polivariadico , que pode ser denotado Y *.

Combinador de ponto fixo estrito

Em uma linguagem de programação estrita, o combinador Y se expandirá até o estouro da pilha ou nunca parará no caso de otimização de chamada final. O combinador Z funcionará em linguagens restritas (também chamadas de linguagens ansiosas, onde a ordem de avaliação do aplicativo é aplicada). O combinador Z tem o próximo argumento definido explicitamente, evitando a expansão de Z g no lado direito da definição:

e no cálculo lambda é uma eta-expansão do combinador Y :

Combinadores de ponto fixo não padrão

No cálculo lambda não tipado, existem termos que têm a mesma árvore de Böhm que um combinador de ponto fixo, ou seja, têm a mesma extensão infinita λx.x (x (x ...)). Eles são chamados de combinadores de ponto fixo não padrão . Qualquer combinador de ponto fixo também é não padrão, mas nem todos os combinadores de ponto fixo não padrão são combinadores de ponto fixo porque alguns deles falham em satisfazer a equação que define os "padrão". Esses estranhos combinadores são chamados de combinadores de ponto fixo estritamente não padronizados ; um exemplo é o seguinte combinador:

Onde

O conjunto de combinadores de ponto fixo não padrão não é recursivamente enumerável.

Implementação em outras línguas

(O combinador Y é uma implementação particular de um combinador de ponto fixo no cálculo lambda. Sua estrutura é determinada pelas limitações do cálculo lambda. Não é necessário ou útil usar essa estrutura na implementação do combinador de ponto fixo em outras linguagens. )

Exemplos simples de combinadores de ponto fixo implementados em alguns paradigmas de programação são fornecidos abaixo.

Implementação funcional preguiçosa

Em uma linguagem que suporta avaliação preguiçosa , como em Haskell , é possível definir um combinador de ponto fixo usando a equação de definição do combinador de ponto fixo convencionalmente denominado fix. Como Haskell tem tipos de dados preguiçosos, esse combinador também pode ser usado para definir pontos fixos de construtores de dados (e não apenas para implementar funções recursivas). A definição é fornecida aqui, seguida de alguns exemplos de uso. No Hackage, a amostra original é:

fix, fix' :: (a -> a) -> a
fix f = let x = f x in x         -- Lambda dropped. Sharing.
                                 -- Original definition in Data.Function.
-- alternative:
fix' f = f (fix' f)              -- Lambda lifted. Non-sharing.

fix (\x -> 9)                    -- this evaluates to 9

fix (\x -> 3:x)                  -- evaluates to the lazy infinite list [3,3,3,...]

fact = fix fac                   -- evaluates to the factorial function
  where fac f 0 = 1
        fac f x = x * f (x-1)

fact 5                           -- evaluates to 120

Implementação funcional estrita

Em uma linguagem funcional estrita, o argumento para f é expandido de antemão, produzindo uma sequência de chamadas infinita,

.

Isso pode ser resolvido definindo correção com um parâmetro extra.

let rec fix f x = f (fix f) x (* note the extra x; here fix f = \x-> f (fix f) x *)

let factabs fact = function   (* factabs has extra level of lambda abstraction *)
   0 -> 1
 | x -> x * fact (x-1)

let _ = (fix factabs) 5       (* evaluates to "120" *)

Implementação de linguagem imperativa

Este exemplo é uma implementação ligeiramente interpretativa de um combinador de ponto fixo. Uma classe é usada para conter a função de correção , chamada fixer . A função a ser corrigida está contida em uma classe que herda do fixador. A função de correção acessa a função a ser corrigida como uma função virtual. Quanto à definição funcional estrita, fix recebe explicitamente um parâmetro extra x , o que significa que a avaliação preguiçosa não é necessária.

template <typename R, typename D>
class fixer
{
public:
    R fix(D x)
    {
        return f(x);
    }
private:
    virtual R f(D) = 0;
};

class fact : public fixer<long, long>
{
    virtual long f(long x)
    {
        if (x == 0)
        {
            return 1;
        }
        return x * fix(x-1);
    }
};

long result = fact().fix(5);

Em uma linguagem funcional imperativa, como Lisp , Scheme ou Racket , Landin (1963) sugere o uso de uma atribuição de variável para criar um combinador de ponto fixo:

(define Y!
  (lambda (f-maker)
    ((lambda (f)
       (set! f (f-maker (lambda (x) (f x)))) ;; assignment statement
       f)
     'NONE)))

Usando um cálculo lambda com axiomas para instruções de atribuição, pode-se mostrar que Y! satisfaz a mesma lei de ponto fixo que o combinador Y chamada por valor:

Digitando

No Sistema F (cálculo lambda polimórfico), um combinador de ponto fixo polimórfico tem tipo;

∀a. (A → a) → a

onde a é uma variável de tipo . Ou seja, fix pega uma função, que mapeia a → a e a usa para retornar um valor do tipo a.

No cálculo lambda de tipo simples estendido com tipos de dados recursivos , os operadores de ponto fixo podem ser escritos, mas o tipo de operador de ponto fixo "útil" (aquele cujo aplicativo sempre retorna) pode ser restrito.

No cálculo lambda simplesmente digitado , o combinador de ponto fixo Y não pode ser atribuído a um tipo porque em algum ponto ele lidaria com o subtermo de autoaplicação pela regra de aplicação:

onde tem o tipo infinito . Nenhum combinador de ponto fixo pode de fato ser digitado; nesses sistemas, qualquer suporte para recursão deve ser explicitamente adicionado ao idioma.

Digite para o combinador Y

Em linguagens de programação que suportam tipos de dados recursivos , é possível digitar o combinador Y contabilizando apropriadamente a recursão no nível de tipo. A necessidade de autoaplicação da variável x pode ser gerenciada usando um tipo (Rec a), que é definido como sendo isomórfico a (Rec a -> a).

Por exemplo, no código a seguir Haskell, temos Ine outsendo os nomes dos dois sentidos do isomorfismo, com tipos:

In :: (Rec a -> a) -> Rec a
out :: Rec a -> (Rec a -> a)

que nos permite escrever:

newtype Rec a = In { out :: Rec a -> a }

y :: (a -> a) -> a
y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x)))

Ou de forma equivalente em OCaml:

type 'a recc = In of ('a recc -> 'a)
let out (In x) = x

let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))

Alternativamente:

let y f = (fun x -> f (fun z -> out x x z)) (In (fun x -> f (fun z -> out x x z)))

Informação geral

Como combinadores de ponto fixo podem ser usados ​​para implementar recursão, é possível usá-los para descrever tipos específicos de cálculos recursivos, como aqueles em iteração de ponto fixo , métodos iterativos , junção recursiva em bancos de dados relacionais , análise de fluxo de dados , FIRST e FOLLOW conjuntos de não terminais em uma gramática livre de contexto , fechamento transitivo e outros tipos de operações de fechamento .

Uma função para a qual cada entrada é um ponto fixo é chamada de função de identidade . Formalmente:

Em contraste com a quantificação universal em geral , um combinador de ponto fixo constrói um valor que é um ponto fixo de . A propriedade notável de um combinador de ponto fixo é que ele constrói um ponto fixo para uma determinada função arbitrária .

Outras funções têm a propriedade especial de que, depois de serem aplicadas uma vez, outras aplicações não têm efeito. Mais formalmente:

Essas funções são chamadas de idempotentes (ver também Projeção (matemática) ). Um exemplo de tal função é a função que retorna 0 para todos os inteiros pares e 1 para todos os inteiros ímpares.

No cálculo lambda , do ponto de vista computacional, a aplicação de um combinador de ponto fixo a uma função de identidade ou a uma função idempotente normalmente resulta em computação não finalizável. Por exemplo, obtemos

onde o termo resultante pode apenas reduzir a si mesmo e representa um loop infinito.

Os combinadores de ponto fixo não existem necessariamente em modelos de computação mais restritivos. Por exemplo, eles não existem no cálculo lambda simplesmente digitado .

O combinador Y permite que a recursão seja definida como um conjunto de regras de reescrita , sem a necessidade de suporte nativo à recursão na linguagem.

Em linguagens de programação que suportam funções anônimas , os combinadores de ponto fixo permitem a definição e o uso de funções recursivas anônimas , ou seja, sem ter que vincular tais funções a identificadores . Nessa configuração, o uso de combinadores de ponto fixo às vezes é chamado de recursão anônima .

Veja também

Notas

Referências

links externos