Por que é importante que as funções sejam anônimas no cálculo lambda?

19

Eu estava assistindo a palestra de Jim Weirich, intitulada ' Aventuras em programação funcional '. Nesta palestra, ele introduz o conceito de combinadores Y, que essencialmente encontra o ponto fixo para funções de ordem superior.

Uma das motivações, como ele menciona, é ser capaz de expressar funções recursivas usando o cálculo lambda, para que a teoria de Church (qualquer coisa que seja efetivamente computável possa ser computada usando o cálculo lambda) permaneça.

O problema é que uma função não pode se chamar simplesmente, porque o cálculo lambda não permite funções nomeadas, ou seja,

n(x,y)=x+y

não pode ostentar o nome ' ', deve ser definido anonimamente:n

(x,y)x+y

Por que é importante que o cálculo lambda tenha funções que não são nomeadas? Qual princípio é violado se houver funções nomeadas? Ou será que eu apenas entendi errado o vídeo de jim?

Rohan Prabhu
fonte
4
Isso não parece importante. Você pode atribuir a uma variável e atribuir um nome à função. n(x,t)x+yn
Yuval Filmus
@YuvalFilmus sim, você pode vincular um nome a uma função. Penso que a verdadeira questão aqui, a perplexidade, é por que (no cálculo lambda) uma função não pode se chamar por esse nome? Por que precisamos de uma técnica como o operador Y para executar funções recursivas? Espero que minha resposta abaixo ajude.
Jerry101
1
@ Jerry101 A razão histórica para a ausência de autoaplicação é que -calculus foi planejado para ser uma base da matemática, e a capacidade de se auto-aplicar torna essa base imediatamente inconsistente. Portanto, essa aparente incapacidade (que sabemos agora pode ser contornada) é um recurso de design do -calculus. λλλ
Martin Berger
@MartinBerger, por favor, diga mais. Inconsistente pelo motivo da minha resposta? Ou por outro motivo?
Jerry101
1
@ Jerry101 Inconsistente no sentido de que você pode provar 0 = 1 em tal fundamento da matemática. Depois de Kleene e Rosser mostrou a inconsistência dos puros, sem tipo -calculus, a simplesmente tipado -calculus foi desenvolvido como uma alternativa que não permite-nos definir combintors ponto-fix como . Mas se você adicionar recursão ao -calculus de digitação simples, ele novamente se tornará inconsistente, porque todo tipo é habitado por um programa não-terminador. λ Y λλλYλ
Martin Berger

Respostas:

24

O principal teorema sobre esse assunto é devido a um matemático britânico do final do século XVI, chamado William Shakespeare . Seu artigo mais conhecido sobre o assunto, intitulado " Romeu e Julieta ", foi publicado em 1597, embora o trabalho de pesquisa tenha sido realizado alguns anos antes, inspirado, mas precursores como Arthur Brooke e William Painter.

Seu principal resultado, afirmado no Ato II. Cena II , é o famoso teorema :

O que há em um nome? o que chamamos de rosa
Por outro nome, teria um cheiro tão doce;

Esse teorema pode ser entendido intuitivamente como "nomes não contribuem para o significado".

A maior parte do artigo é dedicada a um exemplo que complementa o teorema e mostra que, embora os nomes não contribuam com significado, eles são a fonte de problemas sem fim.

Conforme apontado por Shakespeare, os nomes podem ser alterados sem alterar o significado, uma operação que mais tarde foi chamada de conversão por Alonzo Church e seus seguidores. Como conseqüência, não é necessariamente simples determinar o que é indicado por um nome. Isso levanta uma variedade de questões, como o desenvolvimento de um conceito de ambiente em que a associação nome-significado é especificada e regras para saber qual é o ambiente atual quando você tenta determinar o significado associado a um nome. Isso confundiu os cientistas da computação por um tempo, dando origem a dificuldades técnicas, como o infame problema de Funargα. Os ambientes continuam sendo um problema em algumas linguagens de programação populares, mas geralmente é considerado fisicamente inseguro mais específico, quase tão letal quanto o exemplo elaborado por Shakespeare em seu artigo.

Essa questão também se aproxima dos problemas levantados na teoria da linguagem formal , quando alfabetos e sistemas formais precisam ser definidos até um isomorfismo , de modo a ressaltar que os símbolos dos alfabetos são entidades abstratas , independentemente de como elas "se materializam". elementos de algum conjunto.

Esse importante resultado de Shakespeare mostra também que a ciência estava divergindo da magia e da religião, onde um ser ou um significado pode ter um nome verdadeiro .

A conclusão de tudo isso é que, para o trabalho teórico, muitas vezes é mais conveniente não ser sobrecarregado por nomes, embora possa parecer mais simples para o trabalho prático e a vida cotidiana. Mas lembre-se de que nem todo mundo chamado mamãe é sua mãe.

Nota :
A questão foi abordada mais recentemente pelo lógico americano do século 20, Gertrude Stein . No entanto, seus colegas matemáticos ainda estão ponderando as implicações técnicas precisas de seu principal teorema :

Rose é uma rosa é uma rosa é uma rosa.

publicado em 1913 em uma comunicação curta intitulada "Emily Sagrada".

babou
fonte
3
Nota adicional: Nas últimas décadas, "rosa" foi (na ciência da computação) substituída principalmente por "foobar" (e partes dela) como o exemplo canônico de um nome tão bom quanto qualquer outro. Aparentemente, essa preferência foi introduzida por engenheiros ferroviários americanos.
FrankW
Dito isto, nomes canônicos para conceitos frequentemente usados ​​são importantes para uma comunicação eficiente.
Raphael
1
@ Rafael concordou, mas eu colocaria isso na categoria de vida cotidiana. E como sabemos os limites do que é realmente canônico? Ainda assim, muitas vezes sinto preocupação quando vejo os alunos adotando toda terminologia, notação e definição (ou mesmo a maneira como alguns teoremas são declarados) por uma verdade imutável dada por Deus. Mesmo aqui, no SE, os alunos fazem perguntas, sem perceber que podemos não saber suas anotações ou as definições que eles usam nas aulas. A magia dos nomes verdadeiros não morre facilmente.
babou
10

Gostaria de arriscar uma opinião diferente da de @babou e @YuvalFilmus: é vital que o -calculus puro tenha funções anônimas. O problema de ter apenas funções nomeadas é que você precisa saber com antecedência quantos nomes precisará. Mas no -calculus puro, você não tem um limite a priori do número de funções usadas (pense em recursão); portanto, você usa (1) funções anônimas ou (2) segue a rota -calculus e fornece um novo combinador de nomes ( in -calculus) que fornece um suprimento inesgotável de novos nomes em tempo de execução.λλπνx.Pπ

A razão pela qual -calculus puro não possui um mecanismo explícito de recursão é que o -calculus puro foi originalmente planejado para ser um fundamento da matemática por A. Church, e a recursão torna esse fundamento trivialmente doentio. Então, foi um choque quando Stephen Kleene e JB Rosser descobriram que o puro é inadequado como fundamento da matemática ( paradoxo Kleene-Rosser ). Haskell Curry analisou o paradoxo de Kleene-Rosser e percebeu que sua essência é o que hoje conhecemos como Y-Combinator.λλλ

Adicionado após o comentário de @ babou: não há nada errado em ter nomeado funções. Você pode fazer o seguinte: é uma abreviação de na chamada por valor -calculus.letf=MinN(λf.N)Mλ

Martin Berger
fonte
1
Eu acho que o OP queria a capacidade de nomear funções, não proibir as anônimas. Dito isto, eu pensaria que qualquer requisito de cálculo λ em relação à necessidade de funções anônimas também aparecesse em linguagens como Lisp / Scheme ou ML. No caso do Lisp / Scheme, a meta-circularidade dos avaliadores deve possibilitar a criação de novos nomes, conforme necessário, embora eu não tenha certeza se gostaria que fosse assim em um sistema formal. O uso de um número ilimitado de funções não é necessariamente um problema quando a recursão permite a reutilização local de nomes já usados.
babou
O @babou Scheme e o ML têm letrec, para que possam viver facilmente com um número finito de funções nomeadas. Eu estaria interessado em ver uma apresentação do -calculus puro com um esquema explícito para reutilizar nomes. E sim, a capacidade de nomear funções (e outros termos) é perfeitamente compatível com o -calculus puro . λλλ
Martin Berger
A última linha deve ler (lambda f. N) M?
Joe the Person
@JoethePerson Sim, bem localizado. Fixo. Obrigado.
Martin Berger
4

Acredito que a ideia é que nomes não sejam necessários. Tudo o que parece exigir nomes pode ser escrito como funções anônimas.

Você pode pensar no cálculo lambda como linguagem assembly. Alguém em uma palestra sobre montagem pode dizer "Não há árvores de herança orientadas a objetos na linguagem assembly". Você pode então pensar em uma maneira inteligente de implementar árvores de herança, mas esse não é o ponto. O ponto é que as árvores de herança não são necessárias no nível mais básico de como um computador físico é programado.

No cálculo lambda, o ponto é que os nomes não são necessários para descrever um algoritmo no nível mais básico.

Real John Connor
fonte
4

Estou gostando das três respostas aqui até agora - principalmente a análise de Shakespearen de @bouou -, mas elas não esclarecem o que eu acho que é a essência da pergunta.

O cálculo λ liga nomes a funções sempre que você aplica uma função a uma função. A questão não é a falta de nomes.

"O problema é que uma função não pode se chamar simplesmente" referindo-se ao seu nome.

(No Lisp puro, a ligação name -> function não está no escopo dentro do corpo da função. Para que uma função se chame por seu nome, a função precisaria se referir a um ambiente que se refere à função. Pure Lisp não tem estruturas de dados cíclicas. O Impure Lisp o faz mutando o ambiente ao qual a função se refere.)

Como @MartinBerger apontou, a razão histórica pela qual o λ-cálculo não permite que uma função se chame pelo nome foi uma tentativa de descartar o paradoxo de Curry ao tentar usar o λ-cálculo como base da matemática, incluindo a lógica dedutiva. Isso não funcionou, já que técnicas como o combinador Y permitem recursão mesmo sem auto-referência.

Da Wikipedia:

Se podemos definir a função r = (λ.x x x ⇒ y)então r r = (r r ⇒ y).

Se r ré verdade, então yé verdade. Se r ré falso, então r r ⇒ yé verdade, o que é uma contradição. Então, yé verdade e, como ypode ser qualquer afirmação, qualquer afirmação pode ser comprovada.

r ré um cálculo não final. Considerada como lógica r ré uma expressão para um valor que não existe.

Jerry101
fonte
Eu sou muito novo no cálculo lambda, então eu tinha uma pergunta, que eu tenho há quase uma eternidade até agora. O que significa ? Tenho certeza que isso não significa multiplicar por . Isso significa aplicar a expressão a si mesma? Além disso, o que a parte => y significa? x x xλ.x xxxxx
Rohan Prabhu 14/03
@RohanPrabhu λ.x x xtraduz para Lisp como (lambda (x) (x x))e para JavaScript como function (x) {return x(x);}. x⇒ysignifica x implies y, aproximadamente o mesmo que (NOT x) OR y. Veja en.wikipedia.org/wiki/Lambda_calculus
Jerry101
Obrigado por responder a essa pergunta embaraçosa de novato!
Rohan Prabhu