Derivação clara e intuitiva do combinador de ponto fixo (combinador Y)?

28

O combinador de ponto fixo FIX (também conhecido como combinador Y) no cálculo lambda (sem tipo) ( ) é definido como: $\lambda$

FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. x~x~y))$

Entendo sua finalidade e posso rastrear perfeitamente a execução de seu aplicativo; Gostaria de entender como derivar o FIX dos primeiros princípios .

Aqui está o que eu vejo quando tento derivar isso sozinho:

CORRECÇÃO é uma função: CORRECÇÃO $\triangleq \lambda_\ldots$
O FIX utiliza outra função, , para torná-la recursiva: FIX $f$ $\triangleq \lambda f._\ldots$
O primeiro argumento da função é o "nome" da função, usado onde um aplicativo recursivo se destina. Portanto, todas as aparências do primeiro argumento para devem ser substituídas por uma função, e essa função deve esperar o restante dos argumentos de (vamos supor que use um argumento): FIX $f$ $f$ $f$ $f$ $\triangleq \lambda f._\ldots f~(\lambda y. _\ldots y)$

É aqui que eu não sei "dar um passo" no meu raciocínio. As pequenas elipses indicam onde meu FIX está faltando alguma coisa (embora eu só possa saber disso comparando-o com o FIX "real").

Eu já li Tipos e Linguagens de Programação , que não tentam derivá-lo diretamente e, em vez disso, encaminha o leitor para The Little Schemer para uma derivação. Também li isso e sua "derivação" não foi tão útil. Além disso, é menos uma derivação direta e mais um uso de um exemplo muito específico e uma tentativa ad-hoc de escrever uma função recursiva adequada em . $\lambda$

computability logic programming-languages lambda-calculus combinatory-logic BlueBomber
fonte

11

Esta postagem pode ser útil. Em geral, acho que apenas analisar e computar várias iterações do combinador é útil para descobrir por que ele funciona.

Xodarap

2

Existem vários combinadores de pontos fixos diferentes. Talvez as pessoas apenas brincassem com combinadores até que tropeçassem neles.

Yuval Filmus

@YuvalFilmus, é isso que minha pesquisa e a resposta a esta pergunta estão começando a me fazer pensar. Mas ainda acho que seria instrutivo "ver" como os combinadores são formados logicamente, uma habilidade que seria especialmente útil quando, por exemplo, tentando construir um novo combinador.

BlueBomber 09/02

Leia o capítulo 9 em "The Little Lisper", de Daniel P. Friedman (ou "The Little Schemer").

user18199

2

O PO parece indicar que eles já leram isso.

Raphael

29

Eu não li isso em nenhum lugar, mas é assim que acredito que poderia ter sido derivado: $Y$

Vamos ter uma função recursiva , talvez um fatorial ou qualquer outra coisa assim. Informalmente, definimos como termo pseudo-lambda onde ocorre em sua própria definição: $f$ $f$ $f$

f = \dots f \dots f \dots

$f = \ldots f \ldots f \ldots$

Primeiro, percebemos que a chamada recursiva pode ser fatorada como um parâmetro:

f = \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} f

$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} f$

Agora poderíamos definir se tivéssemos uma maneira de passar isso como argumento para si mesmo. Isso não é possível, é claro, porque não temos em mãos. O que temos em mãos é . Como contém tudo o que precisamos para definir , podemos tentar passar como argumento em vez de e tentar reconstruir mais tarde. Nossa primeira tentativa é assim: $f$ $f$ $M$ $M$ $f$ $M$ $f$ $f$

f = \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}}

$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}$

No entanto, isso não está completamente correto. Antes, foi substituído por no interior . Mas agora passamos vez. Temos de corrigir alguma forma todos os lugares onde usamos para que eles reconstruir de . Na verdade, isso não é nada difícil: agora que sabemos que , em todos os lugares que usamos , simplesmente o substituimos por . $f$ $r$ $M$ $M$ $r$ $f$ $M$ $f = M M$ $r$ $(r r)$

f = \underset{M^{'}}{\underset{⏟}{(λ r . (\dots (r r) \dots (r r) \dots))}} \underset{M^{'}}{\underset{⏟}{(λ r . (\dots (r r) \dots (r r) \dots))}}

$f = \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'} \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'}$

Esta solução é boa, mas tivemos que alterar dentro. Isso não é muito conveniente. Podemos fazer isso de forma mais elegante sem precisar modificar introduzindo outro que envia a seu argumento aplicado a si mesmo: expressando como obtemos $M$ $M$ $\lambda$ $M$ $M'$ $\lambda x.M(xx)$

f = (λ x . \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} (x x)) (λ x . \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} (x x))

$f = (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx)) (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx))$

Dessa forma, quando é substituído por , é substituído por , que é pela definição igual a . Isso nos dá uma definição não recursiva de , expressa como um termo lambda válido! $M$ $x$ $MM$ $r$ $f$ $f$

A transição para agora é fácil. Podemos usar um termo lambda arbitrário em vez de e executar esse procedimento nele. Para que possamos fatorar e definir $Y$ $M$ $M$

Y = λ m . (λ x . m (x x)) (λ x . m (x x))

$Y = \lambda m . (\lambda x. m(xx)) (\lambda x.m(xx))$

De fato, o reduz a como o definimos. $Y M$ $f$

Nota: Derivei conforme definido na literatura. O combinator você descreveu é uma variante do para chamada por valor línguas, às vezes também chamado de . Veja este artigo da Wikipedia . $Y$ $Y$ $Z$

Petr Pudlák
fonte

11

A-mas-aparentemente óbvia falta intuição de que a sua excelente resposta me deu é que uma função recursiva precisa-se como um argumento, por isso, começar com um pressuposto de que a função terá a forma por algum . Então, quando construímos , usamos a afirmação de que é definido como a aplicação de algo a si próprio internamente em , por exemplo, aplicando a em sua resposta, que por definição é igual a . Fascinante!

f = X (X)

$f = X (X)$

X

$X$

X

$X$

f

$f$

X

$X$

x

$x$

x

$x$

f

$f$

BlueBomber

11

Como Yuval apontou, não há apenas um operador de ponto fixo. Existem muitos deles. Em outras palavras, a equação para o teorema do ponto fixo não possui uma única resposta. Portanto, você não pode derivar o operador deles.

É como perguntar como as pessoas derivam como uma solução para . Eles não! A equação não tem uma solução única. $(x,y)=(0,0)$ $x=y$

Para o caso de você querer saber como foi descoberto o primeiro teorema de ponto fixo. Deixe-me dizer que também me perguntei como eles surgiram com os teoremas de ponto fixo / recursão quando os vi pela primeira vez. Parece tão engenhoso. Particularmente na forma da teoria da computabilidade. Ao contrário do que Yuval diz, não é o caso de as pessoas brincarem até encontrar algo. Aqui está o que eu encontrei:

Tanto quanto me lembro, o teorema é originalmente devido a SC Kleene. Kleene criou o teorema original do ponto fixo ao recuperar a prova de inconsistência do cálculo lambda original da Igreja. O cálculo lambda original da Igreja sofria de um paradoxo do tipo Russel. O cálculo lambda modificado evitou o problema. Kleene estudou a prova de inconsistência provavelmente para ver como se o cálculo lambda modificado sofria de um problema semelhante e transformou a prova de inconsistência em um teorema útil do cálculo lambda modificado. Através de seu trabalho sobre equivalência do cálculo lambada com outros modelos de computação (máquinas de Turing, funções recursivas etc.), ele o transferiu para outros modelos de computação.

Como derivar o operador que você pode perguntar? Aqui está como eu mantenho isso em mente. O teorema do ponto fixo trata da remoção da auto-referência.

Todo mundo conhece o paradoxo do mentiroso:

Eu sou um covil.

Ou na forma mais lingüística:

Esta frase é falsa.

Agora, a maioria das pessoas pensa que o problema com esta frase está na auto-referência. Não é! A auto-referência pode ser eliminada (o problema é com a verdade, uma linguagem não pode falar sobre a verdade de suas próprias sentenças em geral, veja o teorema da indefinibilidade do verbo de Tarski ). O formulário em que a auto-referência é removida é o seguinte:

Se você escrever a seguinte citação duas vezes, na segunda vez entre aspas, a sentença resultante será falsa: "Se você escrever a seguinte citação duas vezes, na segunda vez entre aspas, a sentença resultante será falsa:"

Sem auto-referência, temos instruções sobre como construir uma frase e depois fazer algo com ela. E a frase que é construída é igual às instruções. Observe que em -calculus não precisamos de aspas porque não há distinção entre dados e instruções. $\lambda$

Agora, se analisarmos isso, temos onde é as instruções para construir e fazer alguma coisa. $MM$ $Mx$ $xx$

$Mx = f(xx)$

Então é e temos $M$ $\lambda x. f(xx)$

$MM = (\lambda x. f(xx))(\lambda x. f(xx))$

Isto é para um fixo . Se você deseja torná-lo um operador, basta adicionar e obteremos : $f$ $\lambda f$ $Y$

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

Por isso, lembro o paradoxo sem auto-referência e isso me ajuda a entender o que é o $Y$

Kaveh
fonte

3

Então você precisa definir um combinador de ponto fixo

fix f = f (fix f)
      = f (f (fix f))
      = f (f (f ... ))

mas sem recursão explícita. Vamos começar com o combinador irredutível mais simples

omega = (\x. x x) (\x. x x)
      = (\x. x x) (\x. x x)
      = ...

O xprimeiro lambda é repetidamente substituído pelo segundo lambda. A simples conversão alfa torna esse processo mais claro:

omega =  (\x. x x) (\x. x x)
      =α (\x. x x) (\y. y y)
      =β (\y. y y) (\y. y y)
      =α (\y. y y) (\z. z z)
      =β (\z. z z) (\z. z z)

Ou seja, a variável no primeiro lambda sempre desaparece. Então, se adicionarmos um fao primeiro lambda

(\x. f (x x)) (\y. y y)

o fvai subir

f ((\y. y y) (\y. y y))

Nós nos omegarecuperamos. Agora deve ficar claro que, se adicionarmos um fao segundo lambda, ele faparecerá no primeiro lambda e depois será exibido:

Y f = (\x. x x)     (\x. f (x x))
      (\x. f (x x)) (\x. f (x x)) -- the classical definition of Y

Desde a

(\x. s t) z = s ((\x. t) z), if `x' doesn't occur free in `s'

podemos reescrever a expressão como

f ((\x. x x) (\x. f (x x))

que é apenas

f (Y f)

e nós temos nossa equação Y f = f (Y f). Portanto, o Ycombinador é essencialmente

dobrar o f
fazer o primeiro fbalançar
repetir

user3237465
fonte

2

Você pode ter visto o exemplo clássico de uma equação sem uma forma normal:

(λ x . x x) (λ x . x x) ▹ (λ x . x x) (λ x . x x)

$(\lambda x.xx)(\lambda x.xx) \triangleright (\lambda x.xx)(\lambda x.xx)$

Uma equação semelhante é sugerida por aquela para recursão geral:

\begin{matrix} (A) & \begin{array}{rr} (λ x . R (x x)) (λ x . R (x x)) \\ ▹ & R ((λ x . R (x x)) (λ x . R (x x))) \\ ▹ & R (R ((λ x . R (x x)) (λ x . R (x x)))) \\ ▹ & \dots \end{array} \end{matrix}

$\begin{array} {rr} & (\lambda x.R(xx))(\lambda x.R(xx)) ~\\ \triangleright & R(~ (\lambda x.R(xx))(\lambda x.R(xx))~) \\ \triangleright & R(R(~ (\lambda x.R(xx))(\lambda x.R(xx))~)) \\ \triangleright & \dots \end{array} \tag{A}$

(A) é uma maneira de escrever equações recursivas gerais no cálculo lambda (além da recursiva primitiva). Então, como você resolve a equação ? Conecte para na equação acima para obter: $Yf = f(Yf)$ $f$ $R$

Y f = (λ x . f (x x)) (λ x . f (x x))

$Yf = (\lambda x.f(xx))(\lambda x.f(xx))$

Y = λ f . (λ x . f (x x)) (λ x . f (x x))

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

DanielV
fonte

Derivação clara e intuitiva do combinador de ponto fixo (combinador Y)?

Respostas: