Combinador de ponto fixo

Em ciência da computação, um combinador de ponto fixo  é uma função y de alta ordem que satisfaz a equação

$y\ f=f\ (y\ f)\ \ {\text{ para todo }}f$

ou em palavras: y, quando aplicado a uma função arbitrária f, produz o mesmo resultado que f aplicada para o resultado da aplicação f para y. É assim chamado porque, por definição $x=y\ f$, representa uma solução para a equação de ponto fixo

$x=f\ x$

Um ponto fixo de uma função f é um valor que não é alterado sob a aplicação da função f.

Funções que satisfazem a equação para y expandir como,

$y\ f=f\ (\ldots f\ (y\ f)\ldots )$

A implementação particular de y é um combinador paradoxal Y de Curry, representado no cálculo lambda por

$Y=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

Este combinador pode ser utilizado na implementação do paradoxo de Curry. O coração do paradoxo de Curry é que o cálculo lambda não tipado não é sólido como um sistema dedutivo, e o combinador Y demonstra que, ao permitir uma expressão anônima para representar zero, ou até mesmo muitos valores é inconsistente na lógica matemática.

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

Usado desta forma o combinador Y implementa recursão simples. No cálculo lambda não é possível remeter para a definição de uma função de um corpo da função. Recursão só pode ser alcançada por passagem de uma função como um parâmetro. O combinador Y demonstra esse estilo de programação.

Introdução

O combinador Y é uma implementação do combinador de ponto fixo em cálculo lambda. 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 no cálculo lambda.

O combinador de ponto fixo pode ser usado em diferentes áreas,

• Matemática Geral 
• Cálculo lambda não tipado 
• Cálculo lambda tipado 
• Programação funcional 
• Programação imperativa 

Combinadores de ponto fixo podem ser aplicados a uma gama de diferentes funções, mas normalmente não irão terminar a menos que exista um parâmetro adicional. Mesmo com avaliação preguiçosa quando a função fixada refere-se ao seu parâmetro, outra chamada para a função é invocada. O cálculo nunca é iniciado. O parâmetro adicional é necessário para provocar o início do cálculo.

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

No cálculo lambda não tipado, a função de aplicar o combinador de ponto fixo pode ser expressa utilizando uma codificação, como a codificação Curry. Neste caso particular, lambda (termos que definem as funções) são considerados como valores. "Running" (beta redução) o combinador de ponto fixo sobre a codificação dá 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 puramente lambda definido no cálculo lambda.

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

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

Valores e domínios

Toda expressão tem um valor. Em geral isto é verdade em matemática e deve ser verdade em cálculo lambda. Isto significa que no cálculo lambda, aplicando um combinador de ponto fixo para uma função dá uma expressão cujo valor é o ponto fixo da função.

No entanto, este é um valor no domínio do cálculo lambda, não pode corresponder a qualquer valor no domínio da função, de modo que, em termos práticos, 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,

$x^{2}=-1\Rightarrow x={\frac {-1}{x}}\Rightarrow f\ x={\frac {-1}{x}}\land Y\ f=x$

Divisão de números com sinal podem ser implementados na codificação Church, então f pode ser representada por um termo de lambda. Esta equação não tem solução em números reais. Mas, no domínio dos números complexos i e -i são soluções. Isto demonstra que pode haver soluções para uma equação em outro domínio. No entanto, o termo lambda para a solução para a equação acima é estranho. O termo lambda Y f representa o estado em que x pode ser ou 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 no cálculo lambda, esta é uma consequência da definição do cálculo lambda. Para o programador, isso significa que a redução beta do termo lambda entra em loop para sempre, nunca chegando a uma forma normal.

Função versus implementação

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

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

O que é um "combinador"?

Um combinador é um tipo especial de função de alta ordem que pode ser usado na definição de funções sem a utilização de variáveis. Os combinadores podem ser combinados com os valores para seus lugares corretos na expressão sem nunca nomeá-los como variáveis.

Uso

Normalmente, quando aplicado às funções de um parâmetro, as implementações do combinador de ponto fixo não conseguem terminar. Funções com parâmetros extras são mais interessantes.

O combinador Y é um exemplo do que faz o cálculo lambda inconsistente. Por isso, deve ser considerado com reserva. No entanto, é seguro considerar o combinador Y quando definido em apenas lógica matemática. A definição é,

$y\ f=f\ (y\ f)$

É fácil de ver como f pode ser aplicada a uma variável. A sua aplicação a duas ou mais variáveis requer adicionar à equação,

$y\ f\ x=f\ (y\ f)\ x$

Esta versão da equação deve ser mostrada consistente com a anterior, a definição para a igualdade de funções,

$(\forall xf\ x=g\ x)\equiv f=g$

Esta definição permite que as duas equações de y para ser considerado como equivalente, desde que o domínio de x está bem definido. Assim, se f tem múltiplos parâmetros o y f ainda pode ser considerado como um ponto fixo, com algumas restrições.

A função fatorial

A função fatorial fornece um bom exemplo de como o combinador de ponto fixo pode ser aplicado para as funções de duas variáveis. O resultado demonstra recursão simples, como seria implementado num único loop, em uma linguagem imperativa. A definição de números usados é explicada na codificação Church. A função de ponto fixo é,

$F\ f\ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (f\ (\operatorname {pred} \ n)))$

assim y F é,

$y\ F\ n=F\ (y\ F)\ n$

ou

$y\ F\ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ ((y\ F)\ (\operatorname {pred} \ n)))$

Reformulando $y\ F=\operatorname {fact}$ dá,

$\operatorname {fact} \ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\operatorname {pred} \ n)))$

esta definição é equivalente para a definição matemática do fatorial,

$\operatorname {fact} \ n=\operatorname {if} n=0\operatorname {then} 1\operatorname {else} n*\operatorname {fact} \ (n-1)$

Esta definição coloca F no papel do corpo de um ciclo para ser iterado.

Combinador de ponto fixo no cálculo lambda

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

$Y=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

Com redução beta temos,

$Y\ g$ $=(\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))\ g$	(por definição de Y)
$=(\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x))$	(por β-redução de λf: aplicando Y para g)
$=g((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))$	(por β-redução de λx: aplicando a função esquerda para a função direita)
$=g\ (Y\ g)$	(por segunda igualdade)

Ao aplicar repetidamente essa igualdade ficamos,

$Y\ g=g\ (Y\ g)=g\ (g\ (Y\ g))=g\ (\ldots g\ (Y\ g)\ldots )$

Definição equivalente de um combinador de ponto fixo

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

$x=f\ x\land y\ f=x$

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

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

dá,

$\operatorname {let} x=f\ x\operatorname {in} y\ f=x$

Também usando,

$x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\to \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)$

dá

$y\ f=\operatorname {let} x=f\ x\operatorname {in} x$

Em seguida, usando a regra de redução eta,

$f\ x=y\iff f=\lambda x.y$

dá,

$y=\lambda f.\operatorname {let} x=f\ x\operatorname {in} x$

Derivação do combinador Y

O combinador Y de Curry pode ser prontamente obtido a partir da definição de Y. Começando com,

$\lambda f.\operatorname {let} x=f\ x\operatorname {in} x$

A 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 substituindo x por xx, mas formalmente isso não é correto. Em vez disso definir y por $\forall z,y\ z=x$ temos,

$\lambda f.\operatorname {let} y\ z=f\ (y\ z)\operatorname {in} y\ z$

A expressão let poderá ser considerada como a definição da função y, em que z é o parâmetro. Instanciando z como y na chamada dá,

$\lambda f.\operatorname {let} y\ z=f\ (y\ z)\operatorname {in} y\ y$

E porque o parâmetro z sempre passa a função y.

$\lambda f.\operatorname {let} y\ z=f\ (z\ z)\operatorname {in} y\ y$

Usando a regra redução eta,

$f\ x=y\equiv f=\lambda x.y$

dá,

$\lambda f.\operatorname {let} y=\lambda z.f\ (z\ z)\operatorname {in} y\ y$

A expressão let pode ser expressa como uma abstração lambda usando,

$n\not \in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda n.L)\ E)$

dá,

$\lambda f.(\lambda y.y\ y)\ (\lambda z.f\ (z\ z))$

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.

$\lambda f.(\lambda z.f\ (z\ z))\ (\lambda z.f\ (z\ z))$

Veja também translating between let and lambda expressions.

Outros combinadores de ponto fixo

Em cálculo lambda não tipado 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 no cálculo lambda não tipado é recursivamente enumerável. 

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

Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))))

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

Y' = S S K (S (K (S S (S (S S K)))) K)))

que corresponde à expressão lambda

Y' = (λx. λy. x y x) (λy. λx. y (x y x))))

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

X = λf.(λx.x x) (λx.f (x x))

Outro combinador de ponto fixo comum é o combinador de ponto fixo Turing (em homenagem a seu descobridor, Alan Turing):

Θ = (λx. λy. (y (x x y))) (λx. λy. (y (x x y)))

Ele também tem uma forma simples call-by-value:

Θ_v = (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))

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

Combinador de ponto fixo estrito

O combinador Z irá trabalhar em linguagens estritas (ou onde a ordem normal é aplicada). O combinador Z tem o seguinte argumento definido explicitamente, impedindo a expansão do Z g no lado direito da definição:

Z g v = g (Z g) v

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

Z = λf.(λx.f (λv.((x x) v))) (λx.f (λv.((x x) v)))

Combinadores de ponto fixo não-padrão

Em cálculo lambda não tipado existem termos que têm a mesma árvore Böhm como um combinador de ponto fixo, que são aqueles que têm a mesma extensão infinita λx.x (x (x ...)). Estes são chamados de combinadores de ponto fixo não-padrão. Qualquer combinador de ponto fixo é também um 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 não conseguem satisfazer a equação que define os "padrão". Estes combinadores estranhos são chamados de combinadores de ponto fixo estritamente não-padrão; um exemplo é a seguinte combinador.

N = B M (B (B M) B)

onde,

B = λx,y,z.x (y z)

M = λx.x x

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

Implementação em outras linguagens

Note que o combinador Y é uma implementação específica de um combinador de ponto fixo em cálculo lambda. A sua estrutura é determinada pelos limites 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 dados abaixo.

Para exemplos de implementações dos combinadores de ponto fixo em várias linguagens ver,

• Rosetta code - Y combinator
• Java code.
• C++ code.

Implementação funcional preguiçosa

IEm uma linguagem que suporta avaliação preguiçosa, como em Haskell, é possível definir um combinador de ponto fixo usando a equação que define o combinador de ponto fixo que é convencionalmente chamado fix. A definição é dada aqui, seguido de alguns exemplos de uso.

 fix :: (a -> a) -> a
 fix f = f (fix f)                -- Lambda lifted
 -- alternative:
 -- fix f = let x = f x in x      -- Lambda dropped

 fix (\x -> 9)                    -- this evaluates to 9
 factabs fact 0 = 1               -- factabs is F from the lambda calculus example
 factabs fact x = x * fact (x-1)
 (fix factabs) 5                  -- evaluates to 120

Implementação funcional estrita

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

$f\ (f...f\ (\operatorname {fix} \ f)...))\ x$.

Isto pode ser resolvido através da definição de fix com um parâmetro adicional.

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 linguagem imperativa

Este exemplo é uma implementação ligeiramente interpretativa de um combinador de ponto fixo. A classe é usada para conter a função fix, chamada fixer. A função fix está contida em uma classe que herda de fixer. A função fix acessa a função fixer em função virtual. Quanto à definição funcional estrito, fix é dado explicitamente um parâmetro x extra, 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);

Tipado

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

∀a.(a → a) → a

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

No cálculo lambda simplesmente tipado estendido com tipos recursivos, operadores de ponto fixo podem ser escritos, mas o tipo de um operador de ponto fixo "útil" (aquele cuja aplicação sempre retorna) pode ser restrito.

No cálculo lambda simplesmente tipado, o combinador de ponto fixo Y não pode ser atribuído um tipo  [9], porque em algum momento ele iria lidar com a auto-aplicação sub-termo x ~ x pela regra de aplicaçãoː

${\Gamma \vdash x\!:\!t_{1}\to t_{2}\quad \Gamma \vdash x\!:\!t_{1}} \over {\Gamma \vdash x~x\!:\!t_{2}}$

onde $x$ tem o tipo infinito $t_{1}=t_{1}\to t_{2}$. Sem combinador de ponto fixo pode de fato ser tipado; nos sistemas para ser suportado deve ser adicionado explicitamente recursão à linguagem.

Tipo para o combinador Y

Em linguagens de programação que suportam tipos recursivos, é possível tipar o combinador Y apropriadamente representando a recursão no nível do tipo. A necessidade de auto-aplicação a variável X pode ser controlada utilizando um tipo (Rec a), (Rec a), o qual é definido de modo a ser isomorfo a (Rec a -> a).

Por exemplo, no código a seguir em Haskell, temos In e Out sendo os nomes das duas direções do isomorfismo, com tipos: 

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

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

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

Informações gerais

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

$\forall xf\ x=x$

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

$\forall xf\ f\ x=f\ x$

Tais funções são chamadas idempotent.  Um exemplo de tal função é a função que retorna 0 para todos os inteiros pares, e 1 para todos os inteiros impares

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

O combinador Y permite recursão para ser definido como um conjunto de regras de reescrita, sem a necessidade de suporte de recursão nativo na linguagem.

O join recursivo em bancos de dados relacionais implementa um ponto fixo, por forma recursiva ao adicionar registros a um conjunto até que não mais pode ser acrescentado.

Em linguagens de programação que suportam funções anônimas, combinadores de ponto fixo permitem a definição e utilização de funções recursivas anônimas, ou seja, sem ter de ligar essas funções para identificadores. Neste cenário, a utilização de combinadores de ponto fixo é, às vezes, chamado recursão anônima.

Veja também

• Iteração de ponto fixo
• Anonymous function
• Cálculo lambda
• Let expression
• Lambda lifting

Referências

• Werner Kluge, Abstract computing machines: a lambda calculus perspective, Springer, 2005, ISBN 3-540-21146-2, pp. 73–77
• Mayer Goldberg, (2005) On the Recursive Enumerability of Fixed-Point Combinators, BRICS Report RS-05-1, University of Aarhus
• Matthias Felleisen. A Lecture on the Why of Y.
• Lambda-Calculus and Combinators: An Introduction, J. Roger Hindley & Jonathan P. Seldin, Cambridge University Press, 2nd edition (August 11, 2008), ISBN 0521898854. (Primeira edição: Introduction to Combinators and Lambda-Calculus, London Mathematical Society Student Texts 1, CUP, 1986.)