O Lambda Calculus é puramente sintático?

29

Eu leio há algumas semanas sobre o Cálculo Lambda, mas ainda não vi nada que seja materialmente diferente das funções matemáticas existentes e quero saber se é apenas uma questão de notação ou se há alguma novidade. propriedades ou regras criadas pelos axiomas do cálculo lambda que não se aplicam a todas as funções matemáticas. Então, por exemplo, eu li o seguinte:

"Pode haver funções anônimas" : as funções do Lambda não são anônimas, são todas chamadas de lambda. É permitido em notação matemática usar a mesma variável para funções diferentes se o nome não for importante. Por exemplo, as duas funções em uma conexão de Galois são frequentemente chamadas *.

"Funções podem aceitar funções como entradas" : Não é novo, você pode fazer isso com funções comuns.

"Funções são caixas pretas" : apenas entradas e saídas também são descrições válidas de funções matemáticas ...

Isso pode parecer uma discussão ou pergunta opinativa, mas acredito que deve haver uma resposta "correta" para essa pergunta. Quero saber se o cálculo lambda é apenas uma convenção notacional ou sintática para trabalhar com funções matemáticas, ou se existem diferenças substanciais ou semânticas entre lambdas e funções comuns.

Neil
fonte
2
Não quero obter uma resposta completa, mas as funções não podem aceitar funções como entradas. Eu posso escrever f (g (0)), mas não posso escrever f (g, 0). O último é chamado de "funcional" e exige regras diferentes.
Cort Ammon - Restabelecer Monica
Os funcionais do @CortAmmon são funções. Uma função é apenas um conjunto de pares (embora, estritamente falando, seja um triplo (D, R, G) onde D é o domínio R é o intervalo e G é o gráfico (conjunto de pares), outro pequeno problema que tenho com a resposta aceita, mas que não está aqui nem ali). Portanto, se D é um conjunto de funções e você pega pares onde o primeiro elemento é uma função em D, então você tem uma função. Verifique a Wikipedia: "Um funcional é um mapeamento [função] ..."
Neil
Ou seja, todos os funcionais são funções, nem todas as funções são funcionais. Mas todas as regras que se aplicam a funções se aplicam a funcionais
Neil

Respostas:

63

Ironicamente, o título está no ponto, mas não da maneira que você parece querer dizer, que é "o cálculo lambda é apenas uma convenção notacional" que não é precisa.

Os termos do Lambda não são funções 1 . São partes da sintaxe, ou seja, coleções de símbolos em uma página. Temos regras para manipular essas coleções de símbolos, mais significativamente a redução beta. Você pode ter várias distintas termos lambda que correspondem à mesma função. 2

Vou abordar seus pontos diretamente.

Primeiro, lambda não é um nome que está sendo reutilizado. Isso não seria extremamente confuso, mas não escrevemos λ(x) (ou (λ x) ), o que faríamos se λ fosse o nome de uma função, assim como escrevemos f(x) . Em f(x) , poderíamos substituir f (se definido por um termo lambda) pelo termo lambda produzindo algo como (λy.y)(x) significa (λy.y) é uma expressão que pode representar uma função, não uma declaração declarando uma função (chamadaλ ou qualquer outra coisa). De qualquer forma, quando sobrecarregamos a terminologia / notação, é (espera-se) feita de uma maneira que possa ser desambiguada via contexto, que certamente não pode ser o caso dos termos lambda.

Seu próximo ponto é bom, mas um pouco irrelevante. Não é uma competição em que há termos e funções da equipe Lambda, e apenas um pode vencer. Uma aplicação principal dos termos lambda é estudar e entender certos tipos de funções. Um polinômio não é uma função, embora geralmente os identifiquemos desleixadamente. Estudar polinômios não significa que se pense que todas as funções devam ser polinômios, nem é o caso de que os polinômios tenham que "fazer" algo "novo" para valer a pena estudar.

As funções teóricas dos conjuntos não são caixas pretas, embora sejam inteiramente definidas por sua relação entrada-saída. (Eles literalmente são sua relação de entrada-saída.) Termos Lambda também não são caixas pretas e eles são não definidos por sua relação de entrada-saída. Como mencionei antes, você pode ter termos lambda distintos que produzem a mesma relação entrada-saída. Isso também ressalta o fato de que os termos lambda não podem ser funções, embora possam induzir funções. 2

F2 F2F24F2F2F2F22N2N

Isso também se aplica aos termos lambda. Podemos interpretá-los como outras coisas que não funções. Eles também são objetos muito mais tratáveis ​​para trabalhar do que os conjuntos de funções tipicamente incontáveis ​​e infinitas. Ambos são muito mais computacionais que funções arbitrárias. Posso escrever um programa para manipular polinômios (com coeficientes que sejam pelo menos representáveis ​​computacionalmente) e termos lambda. De fato, termos lambda não tipados são um dos modelos originais de funções computáveis. Essa perspectiva mais simbólica / sintática, calculadora / computacional é geralmente mais enfatizada, especialmente para o cálculo lambda sem tipo, do que as interpretações mais semânticas do cálculo lambda. DigitadoOs termos lambda são coisas muito mais gerenciáveis ​​e geralmente (mas nem sempre) podem ser facilmente interpretados como funções teóricas definidas, mas também podem geralmente ser interpretados em uma classe de coisas ainda mais ampla, além das funções, do que o cálculo lambda não tipado. Eles também têm uma rica teoria sintática própria e uma conexão muito profunda com a lógica .

1 É possível que o problema ocorra de outra maneira. Talvez você tenha uma má compreensão sobre o que é uma função.

DDDDDD, e para a categoria de conjuntos, não há objetos reflexivos não triviais. A história é um pouco diferente para termos lambda digitados , mas ainda pode ser não trivial.

3 Se você é claro sobre essa distinção, a analogia deve ser bastante informativa.

4 Esse problema não ocorre com os campos da característica 0, como números complexos, reais, racionais ou números inteiros; portanto, a distinção não é tão nítida, embora ainda exista.

Derek Elkins
fonte
8
Esta é uma resposta incrível, só tenho a dizer. Realmente esclarece alguns longos mal-entendidos para mim. Obrigado!
the0ther
4
Eu gostaria de poder responder a isso em detalhes! Muitas coisas que eu gostaria de acompanhar. No geral, embora isso tenha sido muito útil para mim, e aparentemente para algumas outras pessoas, também, obrigado pela resposta completa e ponderada.
Neil
1
Há apenas um ponto em que discutirei aqui: sua afirmação de que os polinômios não precisam "fazer" algo "novo" para valer a pena estudar. Claro que sim! Obviamente, dependendo do seu campo, "novo" pode ter significados diferentes (por exemplo, um matemático puro não fará distinção entre vetores de coluna e vetores de linha porque são isomórficos, mas um estatístico pode considerar a distinção útil para fins de computação). Qualquer novo formalismo deve se justificar.
Neil
2
@ Neil: A nota de rodapé 2, em particular, oferece algumas evidências muito claras de que o cálculo lambda "faz algo novo" que funções "regulares" "não podem fazer". Para um exemplo mais concreto de uma expressão lambda não bem fundamentada, consulte combinadores de ponto fixo . Os números da Igreja também contribuem para uma leitura fascinante, especialmente a função predecessora.
Kevin
1
Eu acrescentaria que as lambdas como funções não fazem nada útil. A única coisa que você pode fazer com um lambda é passar um lambda e ele retorna um lambda. Você não tem como testar o que o lambda resultante faz. Você só pode passar outro lambda para obter outro lambda em troca. Como funções, o conjunto de "funções lambda" se comporta exatamente como um conjunto singleton contendo apenas a função de identidade. É apenas considerando a entrada e a saída de um lambda como expressões que você pode diferenciar os lambdas.
Florian F
0

Pense no conceito de variáveis. Em idiomas antigos, como o básico, você não tinha alocação dinâmica e precisava de um nome para cada variável. (Isso não é perfeitamente preciso porque você tinha matrizes, mas a idéia é que ...) em muitos problemas, você precisa alocar quantas variáveis ​​desejar, sem se limitar ao número de nomes que seu programa define.

As funções do Lambda permitem livrar-se da mesma limitação sobre os nomes das funções, permitindo que o seu programa defina quantas funções forem necessárias e as "armazene" nas mesmas estruturas de dados complexas que outras variáveis. Isso não é algo que você poderia fazer com funções nomeadas convencionais.

Camion
fonte
Por que não consigo fazer isso com funções nomeadas convencionais? Se eu escrever f(x)=let g(y)=x+y in g, todo matemático saberá instantaneamente o que se entende e concorda que esse é um objeto matemático sensato (talvez até algumas queixas sobre ser claro sobre o domínio de f). Eles também ficarão perfeitamente felizes se eu escrever o conjunto {f(n) | n ∈ ℕ}, que contém infinitas funções e, em particular, não é limitado por ter apenas um número finito de nomes para usar.
Daniel Wagner
A questão é sobre o cálculo lambda. Embora relacionado, isso não é a mesma coisa que funções lambda em linguagens de programação.
Andy Dent