Cálculo lambda fora da programação funcional?

21

Sou estudante universitário e atualmente estamos estudando o Lambda Calculus. No entanto, ainda tenho dificuldade em entender exatamente por que isso é útil para mim. Sei que, se você faz muita programação funcional, isso pode ser útil, mas acho que não é realmente necessário para aprender programação funcional, o que você acha?

Em segundo lugar, existe alguma utilidade para o Lambda Calculus no âmbito da Ciência da Computação, mas fora das linguagens de programação funcional?

Jacob
fonte

Respostas:

15

O cálculo lambda é fundamental em lógica, teoria de categorias, teoria de tipos, verificação formal, ... Basicamente, qualquer coisa relacionada à semântica da linguagem de programação e à lógica formal. É um formalismo tão fundamental que as pessoas que trabalham nesses campos nem sequer questionam seus benefícios.

Eu acho que é extremamente útil para entender a programação funcional, porque fornece a essência da programação funcional. Funções, aplicação, substituição. Com base nisso, você pode desenvolver suas habilidades de raciocínio sobre programas funcionais e transformações deles. Funções de ordem superior são fáceis.

Claro que você poderia aprender programação funcional sem o cálculo lambda, mas nunca entenderia verdadeiramente a programação funcional sem ele.

Dave Clarke
fonte
Muito obrigado pela sua resposta Dave. Acho que a verificação formal é a melhor razão até agora, por que o cálculo lambda é útil para eu aprender e, curiosamente, farei um curso sobre verificação formal no próximo semestre. Você também usaria o cálculo lambda para fazer uma verificação formal de um software escrito em qualquer idioma, por exemplo, imperativo ou orientado a objetos?
27412 Jacob
1
Você não pode usar o cálculo lambda diretamente ao fazer a verificação formal, mas ele aparecerá nas bases da verificação formal. As especificações de escrita geralmente envolvem a escrita em uma linguagem funcional, mesmo para códigos imperativos / OO.
Dave Clarke
Ok, isso é interessante, muito obrigado, agora eu tenho um pouco mais de razão para estudar isso. Você sabe se o cálculo lambda é usado para projetar idiomas não funcionais (em níveis mais baixos)?
Jacob
1
ALGOL. Scala. Por fim, sua pergunta é difícil de responder. O cálculo lambda tornou-se parte do conhecimento comum para a maioria dos designers de linguagem e, portanto, influencia o design de linguagem, mesmo que não seja explicitamente usado. Considere blocos no Smalltalk ou Ruby, classes anônimas em Java. Esses são fechamentos, que estão intimamente ligados a funções de ordem superior no cálculo lambda.
21812 Dave Clarke
Ok, muito obrigado Dave, isso é muito apreciado.
Jacob
17

Você está solicitando um aplicativo fora da ciência e da lógica da computação. Isso é facilmente encontrado, por exemplo, na topologia algébrica, é conveniente ter uma categoria de espaços fechados cartesianos; consulte a categoria conveniente de espaços topológicos no nLab. A linguagem formal correspondente às categorias fechadas cartesianas é precisamente o λ cálcio. Deixe-me ilustrar com um exemplo muito simples como isso é útil.

Primeiro, como um exercício de aquecimento, suponha que alguém lhe pergunte se a função definida por f ( x ) = x 2 e x + log ( 1 + x 2 ) é diferenciável. Na verdade, você não precisa provar que é, apenas observa que é uma composição de funções diferenciáveis, portanto diferenciáveis. Em outras palavras, você concluiu facilmente com base no formuláriof:RRf(x)=x2ex+registro(1+x2) de definição.

Agora, o exemplo real. Suponhamos que alguém pergunta se a função definido por F ( x ) = ( λ f : C ( R ) . x - x f ( 1 + t 2 ) d t ) ( λ y : I . Max ( x , pecado ( y + 3 ) )f:RR

f(x)=(λf:C(R).-xxf(1+t2)dt)(λy:R.max(x,pecado(y+3))
é contínuo. Novamente, podemos responder imediatamente "yes" porque a função é definida usando o calcculus e partindo de mapas contínuos max , , sin , etc.λmaxpecado

Várias extensões do cálcio tornam possível fazer o mesmo tipo de coisa em outras áreas. Por exemplo, como topos suaves é uma categoria fechada cartesiana, qualquer mapa que é definido usando o cálcio λ , a partir de derivadas e da estrutura de anéis dos reais (e você pode ativar a função exponencial, se desejar) é automaticamente suave . (Na verdade, o principal impulso dos topos suaves é a existência de infinitesimais nilpotentes, que permitem dizer coisas significativas como "dissecamos um disco em triângulos isósceles infinitamente finos".)λλ

Andrej Bauer
fonte
1
Obrigado por sua resposta elaborada. Na verdade, eu estava tentando encontrar um uso para o cálculo lambda na ciência da computação, mas fora da programação funcional, desculpas se isso não estivesse claro. Mudei a questão para declarar isso mais claramente.
27412 Jacob
Ah, que pena, eu teria escrito uma resposta elaborada sobre isso.
21312 Andrej Bauer
Desculpas por isso. Sinta-se livre para adicionar qualquer comentário, se você quiser adicionar outras informações :)
Jacob
2
λ
7

λλ -calculus é tão simples, os pontos em comum entre muitas linguagens de programação que permitem parametrizar o código são destacados de maneira especialmente clara.

λ

Martin Berger
fonte
5

λ

λ

λ

Peter Wone
fonte