O cálculo lambda (ou λ-cálculo ) é um sistema formal inventado por Alonzo Church em 1930 , que estabelece a função e aplicação dos conceitos . Manipulamos expressões chamadas de expressões λ, onde a letra grega λ é usada para vincular uma variável. Por exemplo, se M é uma expressão λ, λx.M também é uma expressão λ e representa a função que para x associa M.
O cálculo λ foi o primeiro formalismo a definir e caracterizar funções recursivas : é, portanto, de grande importância na teoria da computabilidade , a par das máquinas de Turing e do modelo de Herbrand-Gödel . Desde então, tem sido aplicada como uma linguagem de programação teórica e como uma metalinguagem para demonstração formal auxiliada por computador . O cálculo lambda pode ser digitado ou não .
O cálculo lambda está relacionado à lógica combinatória de Haskell Curry e é generalizado nos cálculos de substituições explícitas .
A ideia básica do cálculo lambda é que tudo é uma função . Uma função é expressa em particular por uma expressão que pode conter funções que ainda não foram definidas: as últimas são então substituídas por variáveis. Existe uma operação básica, chamada de aplicativo :
Aplicar a expressão (que descreve uma função) à expressão (que descreve uma função) é escrita .
Também podemos fazer funções dizendo que se E for uma expressão, criamos a função que corresponde a x à expressão E; Escrevemos λx.E esta nova função.
O nome da variável não é mais importante do que em uma expressão como ∀x P (x), que é equivalente a ∀y P (y) . Em outras palavras, se E [y / x] é a expressão E na qual todas as ocorrências de x foram renomeadas para y , consideraremos que as expressões λx.E e λy.E [y / x] são equivalentes.
Usando as ferramentas que acabamos de adquirir, obtemos, por aplicativos e abstrações, funções bastante complicadas que podemos querer simplificar ou avaliar. Simplifica aplicação do formulário (λx.E) P retorna para transformá-lo em uma expressão alternativa de E em que cada ocorrência livre de x é substituído por P . Essa forma de simplificação é chamada de contração (ou β- contração, se quisermos lembrar que aplicamos a regra β do cálculo lambda).
Com base nisso, podemos construir algumas funções interessantes, como a função de identidade , que é a função que corresponde , ou seja, a função . Também podemos construir a função constante igual a , viz .
A partir daí podemos construir a função que faz as funções constantes, desde que lhe demos a constante como parâmetro, ou seja, a função , isto é, a função que torna a função constantemente igual para corresponder .
Podemos também, por exemplo, construir uma função que permuta o uso dos parâmetros de outra função, mais precisamente se for uma expressão, gostaríamos que funcionasse assim . Função é função . Se aplicarmos a função para chegarmos que podemos simplificar em .
Até agora temos sido bastante informais. A ideia do cálculo lambda é fornecer uma linguagem precisa para descrever funções e simplificá-las.
O cálculo lambda define entidades sintáticas que são chamadas de termos lambda (ou, às vezes, também expressões lambda ) e que se enquadram em três categorias :
O mapa pode ser visto como segue: se u é uma função e se v é seu argumento, então uv é o resultado do mapa para v da função u .
A abstração λ x . v pode ser interpretado como a formalização da função que, a x , associa v , onde v geralmente contém ocorrências de x .
Assim, a função f que leva o termo lambda x como um parâmetro e adiciona 2 a ele (ou seja, na notação matemática atual, a função f : x ↦ x +2 ) será denotada no cálculo lambda pela expressão λ x . x +2 . A aplicação desta função ao número 3 é escrita ( λ x . X +2) 3 e é “avaliada” (ou normalizada) na expressão 3 + 2 .
Alonzo Church conhecia a relação entre seu cálculo e o dos Principia Mathematica de Russell e Whitehead . Agora, esses usam notação para denotar abstração, mas Church usou, em vez disso, a notação que mais tarde se tornou . Peano também definiu abstração em sua Forma Matemática , ele usa em particular a notação, para notar a função como .
Para delimitar as aplicações, são usados parênteses, mas para maior clareza, alguns parênteses são omitidos. Por exemplo, escrevemos x 1 x 2 ... x n para (( x 1 x 2 ) ... x n ).
Na verdade, existem duas convenções:
Shönfinkel e Curry introduziram a currificação : é um processo para representar uma função com vários argumentos. Por exemplo, a função que ao par ( x , y ) associa u é considerada uma função que, com x , associa uma função que, com y , associa u . Portanto, é denotado: λx. (Λy.u) . Também está escrito λx.λy.u ou λxλy.u ou apenas λxy.u . Por exemplo, a função que, ao par ( x , y ) associa x + y , será denotada λx.λy.x + y ou mais simplesmente λxy.x + y .
Em expressões matemáticas em geral e no cálculo lambda em particular, existem duas categorias de variáveis: variáveis livres e variáveis vinculadas (ou burras ). No cálculo lambda, uma variável é ligada por um λ. Uma variável associada tem um escopo e esse escopo é local. Além disso, você pode renomear uma variável associada sem alterar o significado geral de toda a expressão na qual ela aparece. Uma variável que não é limitada é considerada livre.
Variáveis relacionadas em matemáticaPor exemplo, na expressão , a variável é livre, mas a variável está vinculada (pelo ). Esta frase é "igual" porque era um nome local, exatamente como é . Por outro lado , não corresponde à mesma expressão porque o é gratuito.
Assim como a integral vincula a variável de integração, também vincula a variável que a segue.
Exemplos :
Definimos o conjunto VL (t) de variáveis livres de um termo t por indução:
Um termo que não contém nenhuma variável livre é considerado fechado (ou fechado). Também dizemos que este termo lambda é um combinador (do conceito relacionado de lógica combinatória ).
Um termo que não está fechado é considerado aberto.
A ferramenta mais importante para o cálculo lambda é a substituição que permite substituir, em um termo, uma variável por um termo. Este mecanismo está na base da redução que é o mecanismo fundamental da avaliação das expressões, portanto do “cálculo” dos termos lambda.
A substituição em um termo lambda t de uma variável x por um termo u é denotada por t [x: = u] . Alguns cuidados devem ser tomados para definir corretamente a substituição a fim de evitar o fenômeno de captura de variável que poderia, se não formos cuidadosos, ligar uma variável que estava livre antes da substituição ocorrer.
Por exemplo, se u contém a variável livre y e se x aparece em t como uma ocorrência de um subtermo da forma λy.v , o fenômeno de captura pode aparecer. A operação t [x: = u] é chamada de substituição em t de x por u e é definida por indução em t :
Nota : no último caso, vamos prestar atenção que y não é uma variável livre de u . Na verdade, ele seria então “capturado” pelo lambda externo. Se for esse o caso, renomeamos y e todas as suas ocorrências em v por uma variável z que não aparece em t ou em u .
A conversão α identifica λy.v e λz.v [y: = z] . Dois termos lambda que diferem apenas pela renomeação (sem captura) de suas variáveis vinculadas são considerados α-conversíveis . A conversão α é uma relação de equivalência entre termos lambda.
Exemplos:
Nota: a conversão α deve ser cuidadosamente definida antes da substituição. Assim, no termo λx.λy.xyλz.z , não podemos renomear repentinamente x para y ( obteríamos λy.λy.yyλz.z ) por outro lado, podemos renomear x para z .
Definida assim, a substituição é um mecanismo externo ao lambda-cálculo, também se diz que faz parte da metateoria. Observe que alguns trabalhos visam introduzir a substituição como um mecanismo interno ao cálculo lambda, levando ao que é chamado de cálculos de substituição explícitos .
Uma maneira de ver os termos do cálculo lambda é pensar neles como árvores com nós binários (mapeamentos), nós unários (abstrações-λ) e folhas (variáveis). As reduções têm como objetivo alterar os termos, ou as árvores, se as vermos dessa forma; por exemplo, reduzir (λx.xx) (λy.y) dá (λy.y) (λy.y) .
Chamamos redex um termo da forma (λx.u) v , onde uev são termos e x uma variável. Definimos a contração beta (ou contração β) de (λx.u) v como u [x: = v] . Dizemos que um termo C [u] se reduz a C [u '] se u é um redex que β-se contrai em u' , então escrevemos C [u] → C [u '] , a relação → é chamada de contração .
Exemplo de contração :
(λx.xy) a dá (xy) [x: = a] = ay .
Denotamos → * o fechamento reflexivo transitivo da relação de contração → e o chamamos de redução . Em outras palavras, uma redução é uma sequência finita, possivelmente vazia, de contrações.
Nós definimos = β como o fecho reflexivo simétrico e transitória da contracção e ele é chamado beta-conversão , β- conversão , ou mais comumente beta-equivalência ou β- equivalência .
A β-equivalência permite, por exemplo, comparar termos que não são redutíveis entre si, mas que após uma série de β-contrações chegam ao mesmo resultado. Por exemplo (λy.y) x = β (λy.x) z porque as duas expressões se contraem para dar x .
Formalmente, temos M = β M ' se e somente se ∃ N 1 , ..., N p tal que M = N 1 , M' = N p e, para todo i menor que p e maior que 0 , N i → N i + 1 ou N i + 1 → N i .
Isso significa que em uma conversão podem-se aplicar reduções ou relações inversas de reduções (chamadas expansões ).
Definimos também outra operação, chamada de eta-redução , definida como segue: λx.ux → η u , quando x não aparece livre em u. De fato, ux é interpretado como a imagem de x pela função u . Assim, λx.ux é então interpretado como a função que, ax , associa a imagem de x por u , portanto, como a própria função u .
O cálculo associado a um termo lambda é a sequência de reduções que ele gera. O termo é a descrição do cálculo e a forma normal do termo (se houver) é o resultado.
Diz-se que um termo lambda t está na forma normal se nenhuma contração beta puder ser aplicada a ele, ou seja, se t não contiver redex, ou se não houver nenhum termo lambda u tal que t → u . A estrutura sintática dos termos na forma normal é descrita abaixo.
Exemplo:λx.y (λz.z (yz))
Dizemos que um termo lambda t é normalizável se existe um termo u ao qual nenhuma contração beta pode ser aplicada e tal que t = β u . Esse u é chamado de forma normal de t .
Dizemos que um termo lambda t é fortemente normalizável se todas as reduções de t forem finitas .
Exemplos:Seja Δ ≡ λx.xx definido .
Se um termo for fortemente normalizável, então ele é normalizável.
Teorema de Church-Rosser: sejam t e u dois termos tais que t = β u . Existe um termo v tal que t → * v e u → * v .
Teorema do losango (ou confluência): sejam t , u 1 e u 2 termos lambda tais que t → * u 1 e t → * u 2 . Então existe um termo lambda v tal que u 1 → * v e u 2 → * v .
Graças ao Teorema de Church-Rosser, pode-se facilmente mostrar a singularidade da forma normal , bem como a consistência do cálculo lambda (ou seja, há pelo menos dois termos não beta-conversíveis distintos).
Podemos descrever a estrutura dos termos de forma normal que compõem o conjunto . Para isso, descrevemos os chamados termos neutros que formam o conjunto . Termos neutros são termos nos quais uma variável (por exemplo ) é aplicada a termos na forma normal. Então, por exemplo, é neutro se ... estão na forma normal. Os termos na forma normal são termos neutros precedidos de zero, um ou mais λ, ou seja, abstrações sucessivas de termos na forma normal. Então está na forma normal. Podemos descrever os termos na forma normal por meio de uma gramática.
Exemplos : é neutro, portanto também na forma normal. está na forma normal. é neutro. está na forma normal. Por outro lado, não está na forma normal porque não é neutro e não é uma abstração de um termo na forma normal, mas também porque é ele próprio um β-redex, portanto, β-redutível.
Sobre a sintaxe e a redução do cálculo lambda podemos adaptar diferentes cálculos restringindo mais ou menos a classe de termos. Podemos, portanto, distinguir duas classes principais de cálculos lambda: o cálculo lambda não tipado e os cálculos lambda digitados. Os tipos são anotações dos termos que visam manter apenas os termos normalizáveis, possivelmente adotando uma estratégia de redução. Assim, esperamos ter um cálculo lambda que satisfaça as propriedades de Church-Rosser e de normalização.
A correspondência de Curry-Howard relaciona um cálculo lambda digitado a um sistema de dedução natural. Afirma que um tipo corresponde a uma proposição e um termo corresponde a uma prova e vice-versa.
Codificações simulam objetos de computador comuns, incluindo números naturais, funções recursivas e máquinas de Turing. Por outro lado, o cálculo lambda pode ser simulado por uma máquina de Turing. Graças à tese de Church, deduzimos que o lambda-cálculo é um modelo universal de cálculo.
BooleanosNa parte Sintaxe, vimos que é prático definir primitivas. É isso que vamos fazer aqui.
verdadeiro = λab.a
falso = λab.b
Esta é apenas a definição de uma codificação, e poderíamos definir outras.
Percebemos que: verdadeiro xy → * x e : falso xy → * y
Podemos então definir um termo lambda que representa a alternativa: if-then-else . É uma função com três argumentos, um booleano be dois termos lambda u e v , que retorna o primeiro se o booleano for verdadeiro e o segundo caso contrário.
ifthenelse = λbuv. (buv) .
Nossa função é verificada: se então, xy verdadeiro = (λbuv. (buv)) xy verdadeiro ; se, então, verdadeiro xy → (λuv. (verdadeiro uv)) xy ; se, então, verdadeiro xy → * (verdadeiro xy) ; se, então, verdadeiro xy → * ((λab.a) xy) ; se, então, verdadeiro xy → * x .
Veremos da mesma forma que se, então, falso xy → * y .
A partir daí, também temos um termo lambda para operações booleanas clássicas: não = λb.ifthenelse b false true ; e = λab.ifthenelse ab false (ou então λab.ifthenelse aba ); onde = λab.ifthenelse a true b (ou λab.ifthenelse aab ).
Os inteirosA seguinte codificação de inteiros é chamada de inteiros da Igreja, em homenagem ao seu designer. Nós perguntamos: 0 = λfx.x , 1 = λfx.fx , 2 = λfx.f (fx) , 3 = λfx.f (f (fx)) e em geral: n = λfx.f (f (... (fx) ...)) = λfx.f n x com f iterado n vezes.
Assim, o inteiro n é visto como o funcional que, ao par ≺f, x≻ , associa f n (x) .
Algumas funçõesExistem duas maneiras de codificar a função sucessora , adicionando um f no início ou no final. No início temos n = λfx.f n x e queremos λfx.f n + 1 x . É necessário ser capaz de adicionar um f no início do f ("sob" os lambdas) ou no final.
As outras funções são construídas com o mesmo princípio. Por exemplo, além disso, “concatenando” os dois termos lambda: λnpfx.nf (pfx) .
Para codificar a multiplicação , usamos f para "propagar" uma função ao longo de todo o termo: λnpf.n (pf)
O predecessor e a subtração também não são simples. Falaremos sobre isso mais tarde.
Podemos definir o teste em 0 da seguinte maneira: if0thenelse = λnab.n (λx.b) a , ou então usando os Booleanos λn.n (λx.fal) true .
Os iteradoresVamos primeiro definir uma função de iteração em inteiros: iterates = λnuv.nuv
v é o caso base e u é uma função. Se n for zero, calculamos v , caso contrário, calculamos u n (v) .
Por exemplo, a adição que vem das seguintes equações
pode ser definido como segue. O caso base v é o número p , e a função u é a função sucessora . O termo lambda correspondente ao cálculo da soma é, portanto: add = λnp. iter n sucessor p . Observe que adicione np → * n sucessor p .
CasaisPodemos codificar pares por c = λz.zab onde a é o primeiro elemento eb o segundo. Vamos denotar este par (a, b) . Para acessar as duas partes, usamos π 1 = λc.c (λab.a) e π 2 = λc.c (λab.b) . Reconheceremos os booleanos verdadeiros e falsos nessas expressões e deixaremos que o leitor reduza π 1 (λz.zab) a a .
As listasPodemos notar que um inteiro é uma lista da qual não olhamos para os elementos, considerando apenas o comprimento. Ao adicionar informações correspondentes aos elementos, podemos construir as listas de maneira análoga aos inteiros: [a 1 ; ...; a n ] = λgy. ga 1 (... (ga n y) ...). Então : [] = λgy.y; [a 1 ] = λgy.ga 1 y; [a 1 ; a 2 ] = λgy.ga 1 (ga 2 y).
Os iteradores nas listasDa mesma forma que introduzimos uma iteração sobre inteiros, introduzimos uma iteração sobre listas. a function_list é definida por λlxm.lxm como para inteiros. O conceito é praticamente o mesmo, mas existem pequenas nuances. Veremos por um exemplo.
exemplo: o comprimento de uma lista é definido por
x :: l é a lista de cabeça xe cauda l (notação ML ). A função de comprimento aplicada a uma lista l é codificada por: λl.liste_it l (λym.add (λfx.fx) m) (λfx.x) Ou apenas λl.l (λym.add 1 m) 0.
Árvores bináriasO princípio de construção de inteiros, pares e listas é generalizado para árvores binárias:
Uma árvore é uma folha ou um nó. Neste modelo, nenhuma informação é armazenada no nível do nó, os dados (ou chaves) são mantidos apenas no nível folha. Podemos então definir a função que calcula o número de folhas de uma árvore: nb_feuilles = λa.arbre_it a (λbc.add bc) (λn.1), ou mais simplesmente: nb_feuilles = λa.a add (λn.1)
O predecessorPara definir o predecessor nos inteiros da Igreja, é necessário usar os casais. A ideia é reconstruir o predecessor por iteração: pred = λn.π 1 (itera n (λc. (Π 2 c, sucessor (π 2 c))) (0,0)). Como o predecessor em inteiros naturais não é definido como 0, para definir uma função total, adotamos a convenção aqui de que é igual a 0.
Verificamos, por exemplo, que pred 3 → * π 1 (iter 3 (λc. (Π 2 c, sucessor (π 2 c))) (0,0)) → * π 1 (2,3) → * 2.
Deduzimos que a subtração é definível por: sub = λnp. Itera p pred n com a convenção de que se p é maior que n, então sub np é igual a 0.
RecursãoAo combinar predecessor e iterador, obtemos um recursor . Isso difere do iterador pelo fato de que a função que é passada como um argumento tem acesso ao predecessor.
rec = λnfx.π 1 (n (λc. (f (π 2 c) (π 1 c), sucessor (π 2 c))) (x, 0))
Combinadores de ponto fixo
Um combinador de ponto fixo permite construir para cada F , uma solução para a equação X = FX . Isso é útil para programar funções que não são expressas simplesmente por iteração, como gcd, e é especialmente necessário para programar funções parciais.
O combinador de ponto fixo mais simples, devido ao Curry, é: Y = λf. (Λx.f (xx)) (λx.f (xx)). Turing propôs outro combinador de ponto fixo: Θ = (λx. Λy. (Y (xxy))) (λx. Λy. (Y (xxy))).
Verificamos se tudo o que g. Graças ao combinador de ponto fixo, podemos, por exemplo, definir uma função que recebe uma função como argumento e testa se esta função de argumento retorna verdadeiro para pelo menos um inteiro: teste_annulation = λg.Y (λfn.ou (gn) (f (sucessor n))) 0.
Por exemplo, se definirmos a sequência alternada de booleanos verdadeiros e falsos : alternates = λn.itère n não falso, então, verificamos que: teste_annulation alternates → * or (alternates 0) (Y (λfn.or (alternates n) ( f sucessor n)) (sucessor 0)) → * ou (alterna 1) (Y (λfn. ou (alterna n) (f sucessor n)) (sucessor 1)) → * verdadeiro.
Também podemos definir o mdc: pgcd = Y (λfnp.if0thenelse (sub pn) (if0thenelse (sub np) p (fp (sub np))) (fn (sub pn))).
Conexão com funções parciais recursivasO recursor e o ponto fixo são ingredientes-chave para mostrar que qualquer função parcial recursiva é definível no cálculo λ quando inteiros são interpretados por inteiros de Church. Por outro lado, os termos λ podem ser codificados por inteiros e a redução dos termos λ é definível como uma função recursiva (parcial). O cálculo λ é, portanto, um modelo de calculabilidade .
Anotamos termos com expressões chamadas tipos . Fazemos isso fornecendo uma maneira de digitar um termo. Se esse método for bem-sucedido, dizemos que o termo está bem digitado . Além do fato de dar uma indicação do que a função "faz", por exemplo, ela transforma objetos de um certo tipo em objetos de outro tipo, ajuda a garantir uma normalização forte , ou seja, para todos os termos, todos as reduções resultam em uma forma normal (que é única para cada termo inicial). Ou seja, todos os cálculos realizados neste contexto terminam. Os tipos simples são construídos como tipos de recursos, funções, funções, funções, funções, funções, funções, etc. O que quer que pareça, o poder expressivo desse cálculo é muito limitado (portanto, o exponencial não pode ser definido nele, nem mesmo a função ).
Mais formalmente, os tipos simples são construídos da seguinte forma:
Intuitivamente, o segundo caso representa o tipo de funções que pegam um elemento do tipo e retornam um elemento do tipo .
Um contexto é um conjunto de pares do formulário onde é uma variável e um tipo. Um julgamento de digitação é um trio (então dizemos que está bem digitado ), definido recursivamente por:
Se adicionarmos constantes ao cálculo lambda, devemos dar a elas um tipo (via ).
O cálculo lambda simplesmente digitado é muito restritivo para expressar todas as funções computáveis de que precisamos em matemática e, portanto, em um programa de computador. Uma maneira de superar a expressividade do cálculo lambda simplesmente digitado é permitir que variáveis de tipo e quantizem sobre elas, como é feito no sistema F ou no cálculo de construtos .
Lambda-cálculo forma a base teórica da programação funcional e, portanto, influenciou muitas linguagens de programação. O primeiro deles é o Lisp, que é uma linguagem não tipada. Posteriormente, ML e Haskell , que são linguagens tipadas, serão desenvolvidos.
Os índices de de Bruijn são uma notação do cálculo lambda que permite representar por um termo, cada classe de equivalência para a conversão α. Para isso, de Bruijn propôs substituir cada ocorrência de uma variável por um inteiro natural. Cada número natural denota o número de λ que deve ser cruzado para relacionar a ocorrência ao seu linker.
Assim, o termo λ x. xx é representado pelo termo λ 0 0 enquanto o termo λx. λy. λz .xz (yz) é representado por λ λ λ 2 0 (1 0) , porque no primeiro caso o caminho de x para seu ligante não cruza qualquer λ, enquanto no segundo caso o caminho de x em seu ligante cruza dois λ (ou seja, λy e λz ), o caminho de y para seu ligante cruza um λ (ou seja, λz ) e o caminho de z para seu ligante não cruza qualquer λ.
Como outro exemplo, o termo (λ x λ y λ z λ u. (X (λ x λ y. X))) (λ x. (Λ x. X) x) e um termo que é α equivalente a ele , a saber (λ x λ y λ z λ u. (x (λ v λ w. v))) (λ u. (λ t. t) u) são representados por (λ λ λ λ (3 (λ λ 1 ))) (λ (λ 0) 0) (veja a figura).