Qual é a contribuição do cálculo lambda para o campo da teoria da computação?

Estou apenas lendo o cálculo lambda para "conhecê-lo". Eu vejo isso como uma forma alternativa de computação, em oposição à Máquina de Turing. É uma maneira interessante de fazer coisas com funções / reduções (falando grosseiramente). Algumas perguntas continuam me incomodando:

• Qual é o objetivo do cálculo lambda? Por que passar por todas essas funções / reduções? Qual é o propósito?
• Como resultado, fico pensando: o que exatamente o cálculo lambda fez para avançar a teoria da CS? Quais foram as contribuições que me permitiram ter um momento "aha" de entender a necessidade de sua existência?
• Por que o cálculo lambda não é abordado nos textos sobre a teoria dos autômatos? A rota comum é passar por vários autômatos, gramáticas, máquinas de Turing e classes de complexidade. O cálculo Lambda é incluído apenas no currículo dos cursos no estilo SICP (talvez não?). Mas raramente vi isso como parte do currículo principal do CS. Isso implica que não é tão valioso? Talvez não e talvez eu esteja perdendo alguma coisa aqui?

Estou ciente de que as linguagens de programação funcionais são baseadas no cálculo lambda, mas não estou considerando isso como uma contribuição válida, pois foi criada muito antes de termos linguagens de programação. Então, qual é realmente o sentido de conhecer / entender o cálculo lambda, escrever suas aplicações / contribuições à teoria?

$\lambda$ -calculus tem duas funções principais.

• É uma base matemática simples de comportamento computacional seqüencial, funcional e de ordem superior.

• É uma representação de provas na lógica construtiva.

Isso também é conhecido como correspondência de Curry-Howard . Em conjunto, a visão dupla do -calculus como prova e como linguagem de programação (seqüencial, funcional e de ordem superior), reforçada pela sensação algébrica de -calculus (que não é compartilhada pelas máquinas de Turing), levou a uma enorme transferência de tecnologia entre lógica, fundamentos da matemática e programação. Essa transferência ainda está em andamento, por exemplo, na teoria dos tipos de homotopia . Em particular, o desenvolvimento de linguagens de programação em geral, e de disciplinas de digitação em particular, é inconcebível sem λ λ λ $\lambda$$\lambda$$\lambda$-cálculo. A maioria das linguagens de programação deve algum grau de dívida ao Lisp e ao ML (por exemplo, a coleta de lixo foi inventada para o Lisp), que são descendentes diretos do -calculus. Uma segunda linha de trabalho fortemente influenciada pelo -calculus são assistentes de prova interativos .$\lambda$$\lambda$

É preciso saber -calculus para ser um programador competente, ou mesmo um teórico da ciência da computação? Não. Se você não está interessado em tipos, linguagens de verificação e programação com recursos de ordem superior, provavelmente é um modelo de computação que não é muito útil para você. Em particular, se você está interessado na teoria da complexidade, -calculus provavelmente não é um modelo ideal, porque a etapa básica de redução é poderosa: pode faça um número arbitrário de cópias em , então λ ( λ x . M ) N → p H [ N / X ] N → p λ λ H N H $\lambda$$\lambda$

$$(\lambda x.M) N \rightarrow_{\beta} M[N/x]$$ $N$$\rightarrow_{\beta}$é uma noção básica irrealista na contabilização do custo microscópico da computação. Penso que esta é a principal razão pela qual a Teoria A não é tão apaixonada por -calculus. Por outro lado, as máquinas de Turing não são muito inspiradoras para o desenvolvimento da linguagem de programação, porque não existem noções naturais de composição de máquinas, enquanto no -calculus, se e são programas, o mesmo ocorre com . Essa visão algébrica da computação se relaciona naturalmente às linguagens de programação usadas na prática, e muito desenvolvimento da linguagem pode ser entendido como a pesquisa e investigação de novos operadores de composição de programas.$\lambda$$\lambda$$M$$N$$MN$

Para uma visão geral enciclopédica da história do -calculus, consulte História do cálculo lambda e lógica combinatória de Cardone e Hindley .$\lambda$

Eu acho que -calculus contribuiu de várias maneiras para esse campo e ainda contribui para ele. Seguem três exemplos, e isso não é exaustivo. Como não sou especialista em -calculus, certamente sinto falta de alguns pontos importantes.$\lambda$$\lambda$

• Primeiro, acho que ter diferentes modelos de computação que acabam por representar exatamente o mesmo conjunto de funções estava na origem da tese de Church-Turing , e -calculus desempenhou um papel importante, juntamente com as máquinas de Turing e -recursive funções.$\lambda$$\mu$

• Segundo, em relação à linguagem de programação funcional, não entendo como uma contribuição não válida : Basicamente, todos os nossos modelos de computação foram inventados muito antes de qualquer coisa acontecer na Ciência da Computação! Assim, -calculus trouxe outra visão da computação, em certo sentido ortogonal às máquinas de Turing, que é muito proveitosa no campo das linguagens de programação (que faz parte do campo da teoria da computação).$\lambda$

• Finalmente, e como um exemplo mais específico, penso em Complexidade Computacional Implícita, que visa caracterizar classes de complexidade por meio de linguagens dedicadas. Os primeiros resultados, como o Teorema de Bellantoni-Cook, foram declarados em termos de funções recursivas , mas resultados mais recentes usam o vocabulário e as técnicas do . Consulte esta breve introdução à complexidade computacional implícita para obter mais informações, ou os procedimentos dos workshops da DICE .$\mu$$\lambda$

Além do papel fundamental do -calculus, mencionado em todas as outras respostas, eu gostaria de acrescentar algo sobre$\lambda$

O que exatamente o cálculo lambda fez para avançar a teoria do CS?

Acredito que a teoria da concorrência é um campo de CS que foi tremendamente influenciado pela visão composicional mencionada por Martin Berger. Certamente, o -calculus em si não é uma linguagem concorrente, mas seu "espírito algébrico" permeia a definição e o desenvolvimento de cálculos de processos modernos . Eu acho que é justo dizer que álgebras de processo são descendentes do -calculus mais do que são de autômatos e máquinas de Turing e, em geral, a teoria da concorrência não seria o que é hoje sem a importação do - cálculo.λ $\lambda$$\lambda$$\lambda$

Além da simultaneidade, fico feliz em ver a complexidade computacional implícita (ICC) mencionada em uma das respostas (é um campo no qual estou pessoalmente envolvido). No entanto, deve-se dizer que, até o momento, o ICC não tem uso na teoria de CS fora das linguagens de programação e, de maneira muito limitada, na verificação de software. Este é apenas um exemplo de uma situação mais geral: a visão modular, composicional e altamente estruturada da computação subjacente ao e predominante na "Teoria B" parece trazer pouca compreensão dos problemas profundos de interesse na "Teoria A". . Por que isso é assim é, para mim, um assunto interessante e ao mesmo tempo frustrante de reflexão. (Veja esta pergunta para uma discussão relacionada).$\lambda$

(Como uma observação lateral, deixe-me mencionar que, graças às suas profundas conexões com a teoria da prova (Curry-Howard), o -calculus tem aplicações interessantes também fora do CS "apropriado", em particular na teoria dos conjuntos. aludindo a trabalhos recentes sobre realizabilidade clássica, um programa de pesquisa desenvolvido a partir do início dos anos 2000 por Jean-Louis Krivine (e várias outras pessoas agora, como Alexandre Miquel, as palestras encontradas em sua página na web são uma excelente introdução ao assunto). Do ponto de vista teórico do modelo, a realização clássica pode ser vista como uma generalização "não comutativa" da forçante de Cohen, produzindo modelos da teoria dos conjuntos impossíveis de serem obtidos com a forçante).$\lambda$

Suas perguntas podem ser abordadas de vários lados. Gostaria de deixar de lado os aspectos históricos e filosóficos e abordar sua principal questão, que considero ser esta:

Qual é o objetivo do cálculo lambda? Por que passar por todas essas funções / reduções?

Qual é o objetivo da Álgebra Booleana, ou Álgebra Relacional, ou Lógica de Primeira Ordem, ou Teoria dos Tipos, ou algum outro formalismo / teoria matemática? A resposta é que eles não têm um propósito inerente a eles, mesmo que seus designers os tenham criado para um propósito ou outro. Leibniz, ao erguer os fundamentos da Álgebra Booleana, tinha um certo projeto filosófico em mente; Boole estudou por suas próprias razões. o trabalho de Morgan sobre Álgebra relacional também foi motivado por vários projetos dele; Peirce e Frege tinham suas próprias motivações para criar a lógica moderna.

A questão é: qualquer que seja o motivo que a Igreja tenha tido ao criar o cálculo lambda, o ponto do cálculo lambda varia de um praticante para outro.

• Para alguém, é uma notação conveniente para falar sobre cálculos; uma alternativa para as máquinas de Turing e assim por diante.

• Para outro, é uma base matemática sólida sobre a qual construir uma linguagem de programação mais sofisticada (por exemplo, McCarthy, Stanley).

• Para uma terceira pessoa, é uma ferramenta rigorosa para fornecer a semântica das linguagens naturais e de programação (por exemplo, Montague, Fitch, Kratzer).

Eu acho que o cálculo Lambda é uma linguagem formal que vale a pena estudar por si só. Você pode aprender o fato de que, no cálculo lambda sem tipo, temos essas pequenas bestas chamadas 'combinadores Y' e como elas nos ajudam a definir funções recursivas e tornar a prova de indecidibilidade tão elegante e simples. Você pode aprender o fato surpreendente de que existe uma correspondência íntima entre o cálculo lambda simplesmente digitado e um tipo de lógica intuicionista . Existem muitos outros tópicos interessantes a serem explorados (por exemplo, como devemos fornecer a semântica do cálculo lambda? Como podemos transformar o cálculo lambda em um sistema dedutivo como o FOL?)

---

Confira Introdução aos combinadores de Hindley & Seldin e λ – Calculus para obter uma introdução. O Lambda Calculus de Barendregt é a bíblia, então se você é viciado em Hindley & Seldin, há muitos tópicos de natureza semântica e sintática para explorar.

Turing argumentou que a matemática pode ser reduzida a uma combinação de símbolos de leitura / escrita, escolhidos a partir de um conjunto finito, e alternando entre um número finito de "estados" mentais. Ele reificou isso em suas Máquinas de Turing, onde símbolos são gravados nas células de uma fita e um autômato monitora o estado.

No entanto, as máquinas de Turing não são uma prova construtiva dessa redução. Ele argumentou que qualquer 'procedimento eficaz' pode ser implementado por alguma máquina de Turing e mostrou que uma máquina universal de Turing pode implementar todas essas outras máquinas, mas ele não forneceu um conjunto de símbolos, estados e regras de atualização que implementam a matemática. da maneira que ele argumentou. Em outras palavras, ele não propôs uma 'Máquina de Turing padrão', com um conjunto padrão de símbolos que podemos usar para escrever nossa Matemática.

O cálculo Lambda, por outro lado, é precisamente isso. Church estava especificamente tentando unificar as notações usadas para escrever nossa Matemática. Uma vez demonstrado que LC e TMs são equivalentes, poderíamos usar a LC como nossa 'Máquina de Turing padrão' e todos seriam capazes de ler nossos programas (bem, em teoria;)).

Agora, poderíamos perguntar por que tratar a LC como primitiva, e não como um dialeto da MT? A resposta é que a semântica de LC é denotacional : os termos de LC têm um significado "intrínseco". Existem números da Igreja, existem funções para adição, multiplicação, recursão, etc. Isso torna o LC muito bem alinhado com o modo como a Matemática (formal) é praticada, razão pela qual muitos algoritmos (funcionais) ainda são apresentados diretamente no LC.

Por outro lado, a semântica dos programas de MT é operacional : o significado é definido como o comportamento da máquina. Nesse sentido, não podemos cortar uma parte da fita e dizer "isso é adição", porque depende do contexto. O comportamento da máquina, quando atinge essa seção da fita, depende do estado da máquina, dos comprimentos / compensações / etc. dos argumentos, quanta fita será usada para o resultado, se alguma operação anterior corrompeu essa seção da fita etc. Essa é uma maneira horrível de trabalhar ("Ninguém quer programar uma máquina de Turing"), e é por isso que muitos algoritmos (imperativos) são apresentados como pseudocódigo.

outras respostas são boas, eis um outro ângulo / motivo de consideração que se mescla com outras pessoas, mas que pode ser ainda mais definitivo; no entanto, pode ser mais difícil ter em mente claramente, pois as antigas origens se perdem um pouco nas areias do tempo:

precedência histórica!

O cálculo Lambda foi introduzido pelo menos desde 1932 na seguinte ref:

• A. Church, "Um conjunto de postulados para o fundamento da lógica", Annals of Mathematics, Série 2, 33: 346–366 (1932).

a máquina de Turing foi introduzida em ~ 1936 ; portanto, o Lambda Calculus é anterior à aparência da TM há vários anos!

• Turing, AM (1936). "Em números computáveis, com uma aplicação ao problema de Entscheidungs". Anais da London Mathematical Society. 2 (1937) 42: 230-265. doi: 10.1112 / plms / s2-42.1.230

portanto, em outras palavras, uma resposta básica é que o Lambda Calculus é, sob muitos aspectos, o sistema legado final do TCS. ele ainda existe da mesma maneira que o Cobol é, apesar de não haver tanto desenvolvimento na linguagem! parece ser o sistema de computação Turing Complete mais antigo introduzido e até antecede a idéia fundamental da completude de Turing. apenas uma análise retrospectiva posterior mostrou que o cálculo de Lambda, as máquinas de Turing e o problema pós-correspondência eram equivalentes e introduziu o conceito de equivalência de Turing e a tese de Church-Turing .

O cálculo lambda é simplesmente a maneira de estudar a computação a partir de um ponto de vista mais centralizado na lógica em termos de representá-la como teoremas matemáticos e derivações de fórmulas lógicas, etc. também mostra a profunda relação entre computação e recursão e o acoplamento ainda mais estreito com a indução matemática .

esse é um fato bastante notável, porque sugere que, de muitas maneiras, as origens (pelo menos teóricas ) da computação eram fundamentalmente na lógica / matemática , uma tese avançada / ampliada em detalhes por Davis em seu livro Engines of Logic / Mathematicians e as origens de o computador . (é claro que as origens e o papel fundamental da álgebra booleana também reforçam ainda mais essa estrutura histórica conceitual.)

portanto, dramaticamente, pode-se até dizer que o cálculo Lambda é um pouco como uma máquina do tempo pedagógica para explorar as origens da computação!

Acabei de me deparar com este post e, apesar de meu post estar bastante atrasado no dia (ano!), Pensei que talvez meu "valor de centavo" possa ser útil.

Enquanto estudava o assunto na universidade, tive um pensamento semelhante sobre o assunto; então, coloquei a questão do "porquê" para o palestrante e a resposta foi: "compiladores". Assim que ela mencionou, o poder por trás da redução e a arte de avaliar a melhor forma de manipulá-la subitamente fizeram todo o propósito de por que era e ainda é uma ferramenta potencialmente útil.

Bem, esse foi o meu momento "aha".

Na minha opinião, geralmente consideramos linguagens, padrões, autômatos, complexidade de algoritmos etc. de alto nível úteis porque podemos relacioná-los à "tarefa" em questão; enquanto o cálculo lamdba parece um pouco abstrato demais. No entanto, ainda existem aqueles que trabalham com linguagens em um nível baixo - e imagino que o cálculo lambda, o cálculo de objetos e outras formalizações relacionadas os ajudaram a entender e talvez desenvolver novas teorias e tecnologias das quais o programador médio pode se beneficiar. De fato, provavelmente não é um módulo básico por esse motivo, mas (pelos motivos que afirmei) haverá alguns poucos - além dos acadêmicos - que podem achar que é parte integrante de sua carreira profissional escolhida na computação.