Cálculo lambda
Na lógica matemática e na ciência da computação, o cálculo lambda, também escrito como cálculo-λ é um sistema formal que estuda funções recursivas computáveis, no que se refere à teoria da computabilidade, e fenômenos relacionados, como variáveis ligadas e substituição. Sua principal característica são as entidades que podem ser utilizadas como argumentos e retornadas como valores de outras funções.
Imagem: Aztlek · BY-SA · Openverse
O cálculo lambda foi apresentada por Alonzo Church na década de 1930 como parte da investigação dos fundamentos da matemática. O sistema original foi demonstrado ser logicamente inconsistente em 1935 quando Stephen Kleene e J. Barkley Rosser desenvolveram o paradoxo Kleene-Rosser. Em seguida, em 1936, Church isolou e publicou apenas a computação e que depois ficou conhecida como cálculo lambda não tipado. Em 1940, ele também apresentou uma versão computacionalmente mais fraca, mas com um sistema lógico consistente, conhecido como cálculo lambda simplesmente tipado. Alonzo Church foi orientador de Alan Turing. De certa forma, o trabalho de Church está para o conceito de software assim como o de Turing relaciona-se muito diretamente ao conceito de Hardware.
Motivação
Funções recursivas são um conceito fundamental dentro da ciência da computação e da matemática. O cálculo-λ provê uma semântica simples para computações, permitindo que propriedades da computação fossem estudadas formalmente. Considere os dois exemplos a seguir. A função identidade recebe uma única entrada, x, e imediatamente retorna x (ou seja, a identidade não faz nada com sua entrada), enquanto a função recebe um par de entradas, x e y e retorna a soma de seus quadrados, x*x + y*y. Usando esses dois exemplos, podemos fazer algumas observações úteis que motivam as principais ideias em cálculo-λ. A primeira observação é que funções não precisam ser nomeadas explicitamente. Isto é, a função
O Cálculo Lambda
O cálculo lambda consiste de uma linguagem de termos lambda junto com uma teoria equacional (que pode também ser entendida operacionalmente). Como os nomes de funções são uma mera conveniência, o cálculo lambda não tem interesse em nomear uma função. Já que todas as funções esperando mais de um argumento podem ser transformadas em funções equivalentes recebendo uma única entrada (via currying), o cálculo lambda não tem interesse em criar funções que aceitam mais de um argumento. E como os nomes dos argumentos são irrelevantes, a noção nativa de igualdade entre termos lambda se chama alfa-equivalência e que demonstra este princípio. A sintaxe de termos lambda é particularmente simples. Existem três maneiras de obtê-las:
Definição
Considerando um número infinito de identificadores: {a, b, c, …, x, y, z, x1, x2, …}, o conjunto de todas as expressões do lambda pode então ser descrito pela seguinte gramática livre de contexto na forma normal de Backus: O conjunto das expressões lambda, Λ, podem ser definidas indutivamente: Instâncias da regra 2 são conhecidas como abstrações e instâncias de regra 3 são conhecidas como aplicações.
Notação
Para manter a notação das expressões lambda organizada, as seguintes convenções são geralmente aplicados.
Variáveis livres e ligadas
O operador de abstração λ, é dito para ligar suas variáveis sempre que elas ocorrem no corpo da abstração. Variáveis que caem dentro do âmbito de uma abstração são ditos ser ligado. Todas as outras variáveis são chamadas de livres. Por exemplo, na seguinte expressão y é uma variável ligada e x é uma variável livre: λy.x x y. Observe também que uma variável está vinculada pela sua abstração "mais próximo". No exemplo a seguir a única ocorrência de x na expressão está ligada pela segunda lambda : λx.y (λx.z x). O conjunto das variáveis livres de uma expressão lambda M é denotado como FV(M) e é definido por recursão na estrutura de termos. Como se segue:
O significado de expressões lambda é definido por como expressões podem ser reduzidas. Nós também falamos das equivalências resultantes: duas expressões são β-equivalente, se elas podem ser β-convertidos em uma mesma expressão, e α/η-equivalência são definidas de forma semelhante. O termo redex, significa expressão redutível. refere-se a sub-termos que podem ser reduzidos por uma das regras de redução. Por exemplo, (λx.M) N é uma beta-redex que expressa a substituição de x por N em M; se x não é variável livre em M, λx.M x é uma eta-redex. A expressão para o qual uma REDEX reduz é chamado de seu reduto; usando o exemplo anterior, os redutos destas expressões são, respectivamente, M[x:=N] e M.
α-conversão
Alpha-conversão, às vezes é conhecida como alfa-renomeação, permite alterar nomes de variáveis ligadas. Por exemplo, alpha-conversão de λx.x pode produzir λy.y. Termos que diferem apenas por alfa-conversão são chamados α-equivalente. Freqüentemente, no cálculo lambda, termos alfa-equivalente são considerados equivalentes. As regras para a alfa-conversão não são completamente triviais. Primeiro, quando alfa-conversão atua em uma abstração, as únicas ocorrências de variáveis que podem ser renomeados são aqueles que são vinculados a esta mesma abstração. Por exemplo, um alfa-conversão de λx.λx.x poderia resultar em λy.λx.x, mas não pode resultar em λy.λx.y. Este último tem um significado diferente do original.
β-redução
Beta-redução capta a ideia de aplicação de função. Beta-redução é definida em termos de substituição: a beta-redução de ((λV.E) E′) é E[V := E′]. Por exemplo, assumindo alguns codificação de 2, 7, ×, temos a seguinte β-redução: ((λn.n×2) 7) → 7×2.
η-conversão
Eta-conversão expressa a ideia de extensionalidade, que neste contexto é que duas funções são as mesmas se e somente se eles dão o mesmo resultado para todos os argumentos. Eta-conversão converte entre λx.(f x) e f sempre que x não aparece livre em f.
Para o cálculo lambda n/tipado, β-redução como uma rewriting rule não é nem fortemente normalizada nem fracamente normalizada. No entanto, se puder ser demonstrado que a β-redução é confluente. (É claro que estamos a trabalhar livre α-conversão, ou seja, nós consideramos duas formas normais para ser igual, se é possível α-converter um para o outro.) Portanto, ambos os termos fortemente normalizados e termos fracamente normalizados tem uma forma normal única. Para termos fortemente normalizáveis, qualquer estratégia de redução é garantida para alcançar a forma normal, enquanto que para termos fracamente normalizáveis, algumas estratégias de redução pode não conseguir encontrá-lo.
O cálculo lambda básico pode ser usado para modelar booleano, aritmética, estruturas de dados e a recursividade, como ilustrado nas subsecções seguintes.
Aritmética no cálculo lambda
Existem várias formas possíveis para definir os números naturais no cálculo lambda, mas, de longe, os mais comuns são os numerais de Church, que podem ser definidos da seguinte forma: e assim por diante. Ou usando a sintaxe alternativa representada anteriormente na Notação: Um numeral de Church é uma função de ordem superior. Ela toma um função de um único argumento f, e retorna outra função de um único argumento. O numeral de Church n é uma função que toma uma função f como argumento e retorna a n-ésima composição de f, isto é, a função f composta com ela mesma n vezes. Isto e representado por f(n) e é de fato a n-exima potencia de f (considerado como um operador); f(0) é definido como sendo a função identidade. Essas composições repetidas (de uma única função f) obedece à leis de exponenciação, razão pela qual estes numerais pode ser usado para aritmética. (No cálculo lambda original da Church, o parâmetro formal de uma expressão lambda era necessária ter pelo menos uma ocorrência no corpo da função, o que fez a definição acima de 0 impossível).
Lógica e predicados
Por convenção, as duas definições seguintes (conhecidas como booleanos de Church) serão utilizadas para os valores booleanos TRUE eFALSE: Então, com esses dois termos λ, podemos definir alguns operadores lógicos (estes são apenas possíveis formulações; outras expressões são igualmente correto): Estamos agora em condições de calcular algumas funções lógicas, por exemplo: e vemos que AND TRUE FALSE é equivalente a FALSE. Um predicado é uma função que retorna um valor booleano. O predicado mais fundamental é ISZERO, que retorna TRUE se o seu argumento é o numeral de Church 0, e FALSE se seu argumento for qualquer outro numeral de Church: Os seguintes predicados testa se o primeiro argumento é menor que ou igual a segundo:
Pares
Um par (2-tupla) pode ser definida em termos de TRUE e FALSE, usando a pares de Church. Por exemplo, PAIR encapsula o par (x,y), FIRST retorna o primeiro elemento do par, e SECOND retorna o segundo. Uma lista ligada pode ser definida como qualquer NIL para a lista vazia, ou o PAIR de um elemento e uma lista menor. o predicado NULL testa se o valor é NIL. (Alternativamente, com NIL := FALSE, a construção l (λh.λt.λz.lidar_com_cabeça_h_e_calda_t) (lidar_com_nil) obviamente e necessidade de um teste para NULL). Como um exemplo da utilização de PAIR, a função de deslocamento-e-incremento que mapeia (m, n) to (n, n + 1) pode ser definida da seguinte forma:
Recursão e pontos fixos
Recursão é a definição de uma função que invoca a própria função; em face do que, cálculo lambda não permitir isto (nós não podemos nos referir a um valor que ainda está para ser definido, dentro do termo lambda que define esse mesmo valor, como todas as funções são anônimas em cálculo lambda). Contudo, esta impressão é enganosa: dentro de (λx.x x) y ambos x referem-se ao mesmo termo lambda, y, por isso, é possível que uma expressão lambda – y – ser preparada para receber-se como o seu argumento, através da auto-aplicação. Considere, por exemplo, a função fatorialF(n) recursivamente definida por: Na expressão lambda que é representar esta função, um parâmetro (tipicamente o primeiro) será presumido para receber em si a expressão lambda como o seu valor, de modo que é chamando – aplicando-o a um argumento – será equivalente à recursão. Assim, para alcançar a recursividade, o argumento destinado-como-auto-referência (chamador aqui) sempre deve ser passada para si mesmo dentro do corpo da função, em um ponto de chamada:
Termos padrão
Alguns termos têm nomes comumente aceitos:
