Cálculo lambda
Na lógica matemática e na ciência da computação, lambda cálculo , também escrito como cálculo-λ é um sistema formal que estuda funções recursivas computáveis, no que se refere a 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.
A parte relevante de lambda cálculo para computação ficou conhecida como lambda cálculo não-tipado. O lambda cálculo tipado e o não-tipado tem suas ideias aplicadas nos campos da lógica, teoria da recursão (computabilidade) e linguística, e tem tido um grande papel no desenvolvimento da teoria de linguagens de programação (com a versão não-tipada sendo a inspiração original para programação funcional, em particular Lisp, e a versão tipada contribuindo para fundamentar modernos sistemas de tipos e linguagens de programação). Neste artigo, a versão não-tipada será discutida largamente.
Índice
1 História
2 Descrição informal
2.1 Motivação
2.2 O Cálculo Lambda
2.2.1 Termos lambda
2.2.2 Funções que operam em funções
2.2.3 Alfa-equivalência
2.2.4 Variáveis livres
2.2.5 Substituição de variáveis
2.2.6 Redução Beta
3 Definição formal
3.1 Definição
3.2 Notação
3.3 Variáveis livres e ligadas
4 Redução
4.1 α-conversão
4.1.1 Substituição
4.2 β-redução
4.3 η-conversão
5 Forma normal e confluência
6 Codificando tipos de dados
6.1 Aritmética no lambda cálculo
6.2 Lógica e predicados
6.3 Pairs
6.4 Recursão e pontos fixos
6.5 Termos padrão
7 Outras linguagens puras
8 Ver também
9 Referências
História |
Lambda cálculo foi apresentada por Alonzo Church na década de 1930 como parte da investigação dos fundamentos da matemática.[1][2] 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 lambda cálculo não-tipado.[3] Em 1940, ele também apresentou uma versão computacionalmente mais fraca, mas com um sistema lógico consistente, conhecido como lambda cálculo simplesmente tipado.[4]
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.
Descrição informal |
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
I(x) = x
recebe uma única entrada, x, e imediatamente retorna x (ou seja, a identidade não faz nada com sua entrada), enquanto a função
sqsum(x, y) = x*x + y*y
recebe um par de entradas, x e y e retorna a soma de seus quadrados, x*x + y*y. Usando estes 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
sqsum(x, y) = x*x + y*y
pode ser reescrita na forma anônima como
(x, y) ↦ x*x + y*y
(leia-se “a tupla x e y é mapeada em x*x + y*y”). Similarmente,
I(x) = x
pode ser reescrita em sua forma anônima para x ↦ x, onde a entrada é simplesmente mapeada para si mesma.
A segunda observação é que a escolha do nome para os argumentos de uma função é totalmente irrelevante. Isto é,
x ↦ xey ↦ y
expressam a mesma função: a identidade. De forma similar,
(x, y) ↦ x*x + y*ye(u, v) ↦ u*u + v*v
também expressam a mesma função.
Finalmente, qualquer função que recebe duas entradas, como a função sqsum do exemplo, pode ser reelaborada numa função equivalente que recebe uma única entrada e tem, como saída, uma outra função, que por sua vez também aceita uma única entrada. Por exemplo,
(x, y) ↦ x*x + y*y
pode ser reelaborada para
x ↦ (y ↦ x*x + y*y)
Esta transformação é chamada currying, e pode ser generalizada para funções que aceitam um número arbitrário de argumentos.
Currying pode ser entendido de forma mais clara através de um exemplo. Compare a função
(x, y) ↦ x*x + y*y
com sua forma "curryficada",
x ↦ (y ↦ x*x + y*y)
Dado dois argumentos, temos:
((x, y) ↦ x*x + y*y)(5, 2)= 5*5 + 2*2 = 29
No entanto, usando currying, temos:
((x ↦ (y ↦ x*x + y*y))(5))(2)= (y ↦ 5*5 + y*y)(2)= 5*5 + 2*2 = 29
e assim vemos que as versões com ou sem currying computam o mesmo resultado. Perceba que x*x se transformou numa constante.
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 lambda cálculo 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 lambda cálculo 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 equivalência-alpha e que demonstra este princípio.
Termos lambda |
A sintaxe de termos lambda é particularmente simples. Existem três maneiras de obtê-las:
- um termo lambda pode ser uma variável,
x; - se
té um termo lambda, exé uma variável, entãoλx.té um termo lambda (chamado abstração lambda); - se
tessão termos lambda, entãotsé um termo lambda (chamado aplicação).
Nada mais é termo lambda, apesar de que parenteses podem ser usados para tirar ambiguidades entre termos.
Uma abstração lambda λx.t{displaystyle lambda x.t}
Uma aplicação ts{displaystyle ts}
Em lambda cálculo não existe o conceito de declaração de variáveis. Em uma definição tal qual λx.x+y{displaystyle lambda x.x+y}
Parenteses podem ser usados para distinguir termos. Por exemplo, λx.((λx.x)x){displaystyle lambda x.((lambda x.x)x)}
Funções que operam em funções |
Em lambda cálculo , funções são consideradas como valores, então elas podem servir de entrada para outras funções, e funções podem retornar funções como saída.
Por exemplo, λx.x representa a função identidade, x ↦ x, e (λx.x)y representa a função identidade aplicada a y. E assim, (λx.y) representa a função constante x ↦ y, uma função que sempre retorna, independentemente da entrada. É importante ressaltar que a aplicação de funções é associativa à esquerda, então (λx.x)y z = ((λx.x)y)z.
O que torna os termos ainda mais interessantes são as várias noções de equivalência e redução que podem ser definidas sobre eles.
Alfa-equivalência |
Uma forma básica de equivalência, definida para termos lambda, é chamada de alfa-equivalência.
Ela determina que a escolha da variável ligada, na abstração lambda, não importa (normalmente).
Por exemplo, λx.x e λy.y são termos lambda alfa-equivalentes, representando a mesma função identidade.
Perceba que os termos x e y não são alfa-equivalentes, porque eles não estão ligados por uma abstração lambda.
Em muitos casos, é fácil de identificar termos lambda equivalentes.
As próximas definições serão necessárias para que a definição de beta-redução seja possível.
Variáveis livres |
As variáveis livres de um termo são aquelas variáveis que não são ligadas por uma abstração lambda.
Isto é, as variáveis livres de x são apenas x; as variáveis livres de λx.t são as variáveis livres de t, com x removido, e as variáveis livres de ts são a união das variáveis livres de t e s.
Por exemplo, o termo lambda representando a função identidade λx.x não tem variáveis livres, mas a função constante λx.y tem uma única variável livre, y.
Substituição de variáveis |
Suponha que t{displaystyle t}
![{displaystyle t[x:=r]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/18e1a37baab228f8a6915d5f6b1cf94c48188a2a)
x[x:=r]=r{displaystyle x[x:=r]=r};
y[x:=r]=y{displaystyle y[x:=r]=y}se x≠y{displaystyle xneq y}
;
(ts)[x:=r]=(t[x:=r])(s[x:=r]){displaystyle (ts)[x:=r]=(t[x:=r])(s[x:=r])};
(λx.t)[x:=r]=λx.t{displaystyle (lambda x.t)[x:=r]=lambda x.t};
(λy.t)[x:=r]=λy.(t[x:=r]){displaystyle (lambda y.t)[x:=r]=lambda y.(t[x:=r])}se x≠y{displaystyle xneq y}
Exemplos:
(λx.x)[y:=y]=λx.(x[y:=y])=λx.x{displaystyle (lambda x.x)[y:=y]=lambda x.(x[y:=y])=lambda x.x},
((λx.y)x)[x:=y]=((λx.y)[x:=y])(x[x:=y])=(λx.y)y{displaystyle ((lambda x.y)x)[x:=y]=((lambda x.y)[x:=y])(x[x:=y])=(lambda x.y)y}.
Redução Beta |
A regra de redução beta afirma que uma aplicação da forma (λx.t)s{displaystyle (lambda x.t)s}
![{displaystyle t[x:=s]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c69396d99d4f60dbe54641cf62b9864b0a2251e1)
![{displaystyle (lambda x.t)sto t[x:=s]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8b3ec6af9a3a97d2362dd9473b3b00f414b5323e)
![{displaystyle (lambda x.x)sto x[x:=s]=s}](https://wikimedia.org/api/rest_v1/media/math/render/svg/02262c02953e5da0468ebf98f4b38327229bd4c9)
![{displaystyle (lambda x.y)sto y[x:=s]=y}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de42f8231c1e95fb1556e6aee11c40d0000ea008)
O lambda cálculo pode ser visto como uma linguagem de programação funcional idealizada. Como Haskell ou Standard ML. Sob este ponto de vista beta redução corresponde a um passo de computação. Este passo pode ser repetido por conversões beta adicionais até que não haja mais reduções beta. Em lambda cálculo não tipado, como este apresentado aqui, este processo pode não terminar em alguns casos. Um exemplo é o seguinte, considere o termo Ω=(λx.xx)(λx.xx){displaystyle Omega =(lambda x.xx)(lambda x.xx)}
![{displaystyle (lambda x.xx)(lambda x.xx)to (xx)[x:=lambda x.xx]=(x[x:=lambda x.xx])(x[x:=lambda x.xx])=(lambda x.xx)(lambda x.xx)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ba84bd0baf6c5c33e59226aa42474b36e3046231)
Outro aspecto do lambda cálculo não tipado é que ele não faz distinção entre diferentes tipos de dados. Por exemplo, ele pode não ter interesse em escrever uma função que apenas opera com números. Contudo, em um lambda cálculo não tipado, não há nenhuma maneira de impedir uma função de ser aplicadas a valores de verdade, strings ou outros objetos não-numéricos.
Definição formal |
Definição |
Expressões lambda são compostas por
- variáveis v1, v2, …, vn
- símbolos abstratos λ (lambda) e. (ponto)
- parênteses ()
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:
- <expressão>::= <identificador>
- <expressão>::= (λ<identificador>. <expressão>)
- <expressão>::= (<expressão> <expressão>)
O conjunto das expressões lambda, Λ, podem ser definidas indutivamente:
- se x é uma variável, então x ∈ Λ
- se x é uma variável e M ∈ Λ, então (λx.M) ∈ Λ
- se M, N ∈ Λ, então (M N) ∈ Λ
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.
- Parenteses mais externos são removidos: M N é usado ao invés de (M N)
- Aplicação assume associatividade mais a esquerda: M N P deve ser escrito ao invés de ((M N) P)[5]
- A variável ligada de uma abstração abrange o máximo para a direita quanto possível: λx.M N Significa λx.(M N) e não (λx.M) N
- Uma sequencia de abstrações é contraída: λx.λy.λz.N é contraída para λxyz.N[6][7]
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:
- FV(x) = {x}, Onde x é uma variável.
- FV(λx.M) = FV(M) {x} (o conjunto das variáveis livres de M menos a variável x se existi-se em M)
- FV(M N) = FV(M) ∪ FV(N)[8]
Uma expressão que não contém nenhuma variável livre é dita ser fechada. Expressão lambda fechada são também conhecidas como combinadores e são equivalentes para termos em combinatory logic.
Redução |
O significado de expressões lambda é definido por como expressões pode ser reduzidas.[9]
Existem três tipos de reduções.
α-conversão: trocar variáveis ligadas (alpha);
β-redução: aplicando funções aos seus argumentos (beta);
η-conversão: que capta a noção de extensionalidade (eta).
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,[10] 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 lambda cálculo , 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.
Em segundo lugar, alfa-conversão não é possível se isto iria resultar em uma variável sendo capturada por uma abstração diferente. Por exemplo, se substituirmos x com y em λx.λy.x, nós obteríamos λy.λy.y, que tem um significado diferente da expressão anterior.
Em linguagens de programação com escopo estático, alfa-conversão pode ser usado para fazer name resolution garantindo que nenhum nome de variável masks um nome em um determinado escopo (veja alpha renaming to make name resolution trivial).
Na notação De Bruijn index, quaisquer dois termos alfa-equivalente são literalmente idênticos.
Substituição |
Substituição, escrito E[V := R], é o processo de substituição de todas as ocorrências da variável livre V na expressão E pela expressão R. Substituição de termos em λ-cálculo é definido por recursão sobre a estrutura de termos, do seguinte modo (note: x e y são apenas as variáveis enquanto M e N são alguma λ expressão).
x[x := N] ≡ N
y[x := N] ≡ y, se x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N] ≡ λx.M
(λy.M)[x := N] ≡ λy.(M[x := N]), se x ≠ y, e y ∉ FV(N)
Para substituir em uma abstração lambda, às vezes é necessário algo converter α-expressão. Por exemplo, não é correto para (λx.y) [y = x:] para resultar em (λx.x), porque o x substituído era suposto ser livre, mas acabou sendo ligado. A substituição correta neste caso é (λz.x), pela α-equivalência. Observe que a substituição é definida exclusivamente até a α-equivalência.
β-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.
Forma normal e confluência |
Para o lambda cálculo n/tipado, β-redução como uma rewriting rule não é nem strongly normalising nem weakly normalising.
No entanto, se puder ser demonstrado que a β-redução é confluent. (É 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 único. 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.
Codificando tipos de dados |
O lambda cálculo 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 lambda cálculo |
Existem várias formas possíveis para definir os números naturais no lambda cálculo, mas, de longe, os mais comuns são os Church numerals,, que podem ser definidos da seguinte forma:
0 := λf.λx.x1 := λf.λx.f x2 := λf.λx.f (f x)3 := λf.λx.f (f (f x))
e assim por diante. Ou usando a sintaxe alternativa representada anteriormente na Notação:
0 := λfx.x1 := λfx.f x2 := λfx.f (f x)3 := λfx.f (f (f x))
Um numeral de Church é uma higher-order function 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-exima composição de f, i.e 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 de identidade. Essas composições repetidas (de uma única função f) obedece à laws of exponents, razão pela qual estes numerais pode ser usado para aritmética. (No lambda cálculo originais 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).
Podemos definir uma função sucessor, o que leva um número n e retorna n + 1 pela adição de outra aplicação de f, onde '(mf)x" significa que a função f é aplicado m vezes em x:
SUCC := λn.λf.λx.f (n f x)
Porque o m-exima composição de f composto com a n-exima composição de f dá a m+n-exima composição de f, Adicionalmente pode ser definido como se segue:
PLUS := λm.λn.λf.λx.m f (n f x)
PLUS pode ser pensada como tendo uma função de dois números naturais como argumentos e devolver um número natural; pode-se verificar que
PLUS 2 3
and
5São lambda expressões β-equivalentes . desde que acrescentandompara um númeronpode ser realizado adicionando 1mvezes, uma definição equivalente é:
PLUS := λm.λn.m SUCC n[11]
De forma simular, multiplicação pode ser definida da seguinte forma:
MULT := λm.λn.λf.m (n f)[12]
Alternativamente:
MULT := λm.λn.m (PLUS n) 0
desde multiplicando m e n é o mesmo que repetir a adicionar n funções m vezes e, em seguida, aplicando a zero. Exponenciação tem uma realização bastante simples em numerais de Church , ou seja:
POW := λb.λe.e b
A função predecessor definida por PRED n = n − 1 para um inteiro positivo n e PRED 0 = 0 é consideravelmente mais difícil. A formula
PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
pode ser validado, mostrando indutivamente que se T representa (λg.λh.h (g f)), então T(n)(λu.x) = (λh.h(f(n−1)(x))) para n > 0. Duas outras definições de PRED são apresentadas a seguir, uma usando conditionals e a outra usando pairs. Com a função predecessor , subtração é simples. Definida por:
SUB := λm.λn.n PRED m,
SUB m n produz m − n quando m > n e 0 caso contrario.
Lógica e predicados |
Por convenção, as duas definições seguintes (conhecidas como Church booleans) serão utilizadas para os valores booleanos TRUE eFALSE:
TRUE := λx.λy.x
FALSE := λx.λy.y
- (Note que
FALSEé equivalente ao numeral de Church zero definido anteriormente).
- (Note que
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):
AND := λp.λq.p q pOR := λp.λq.p p qNOT := λp.λa.λb.p b aIFTHENELSE := λp.λa.λb.p a b
Estamos agora em condições de calcular algumas funções lógicas, por exemplo:
AND TRUE FALSE
≡ (λp.λq.p q p) TRUE FALSE →β TRUE FALSE TRUE≡ (λx.λy.x) FALSE TRUE →β FALSE
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:
ISZERO := λn.n (λx.FALSE) TRUE
Os seguintes predicados testa se o primeiro argumento é menor que ou igual a segundo:
LEQ := λm.λn.ISZERO (SUB m n),
e desde m = n, se LEQ m n e LEQ n m, é muito simples para construir um predicado de igualdade numérica.
Da disponibilidade de predicados e na definição acima de TRUE eFALSE torná-lo conveniente para escrever "if-then-else" expressões. Por exemplo,a função predecessor pode ser definida como:
PRED := λn.n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0
que pode ser verificada, mostrando indutivamente que n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) é a função adicionar n − 1 para n > 0.
Pairs |
Um par (2-tupla) pode ser definida em termos de TRUE e FALSE, usando o Church encoding for pairs. Por exemplo, PAIR encapsula o par (x,y), FIRST retorna o primeiro elemento do par, e SECOND retorna o segundo.
PAIR := λx.λy.λf.f x yFIRST := λp.p TRUESECOND := λp.p FALSENIL := λx.TRUENULL := λp.p (λx.λy.FALSE)
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:
Φ := λx.PAIR (SECOND x) (SUCC (SECOND x))
O que nos permite dar talvez a versão mais transparente da função predecessor :
PRED := λn.FIRST (n Φ (PAIR 0 0)).
Recursão e pontos fixos |
Ver artigo principal: Fixed-point combinatorRecursão é a definição de uma função que invoca a própria função; em face do que, lambda cálculo não permitir isto (nós não podemos nos referir a um valor que ainda está para ser definido, dentro do lambda termo define esse mesmo valor, como todas as funções são anônimos em lambda cálculo). Contudo, esta impressão é enganosa: dentro de (λx.x x) y ambos x referem-se ao mesmo lambda termo , 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, o factorial funçãoF(n) recursivamente definido por:
F(n) = 1, se n = 0; então n × F(n − 1).
Na expressão lambda que é representar esta função, um parametro (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 a 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:
G := λr. λn.(1, se n = 0; então n × (r r (n−1)))
- com
r r x = F x = G r xpara manter, assimr = Ge
- com
F := G G = (λx.x x) G
A auto-aplicação alcança replicação aqui, passando a função como expressão lambda para a próxima invocação como um valor de argumento, tornando-o disponível para ser referenciado e invocou ali.
Isto resolve, mas necessita de reescrever cada chamada recursiva como auto-aplicação. Gostaríamos de ter uma solução genérica, sem necessidade de quaisquer re-escrita:
G := λr. λn.(1, se n = 0; então n × (r (n−1)))
- com
r x = F x = G r xpara manter, assimr = G r =: FIX Ge
- com
F := FIX GondeFIX g := (r onde r = g r) = g (FIX g)
- de modo que
FIX G = G (FIX G) = (λn.(1, se n = 0; então n × ((FIX G) (n−1))))
- de modo que
Dado um lambda termo com o primeiro argumento representando chamada recursiva (i.e. G aqui), o combinador de ponto-fixo FIX irá retornar uma expressão lambda auto-replicante que representa a função recursiva (aqui, F). A função não necessita de ser passado explicitamente a si mesma em qualquer ponto, a auto-replicação é providenciado com antecedência, quando ele é criado, para ser feito cada vez que é chamado. Assim, a expressão lambda inicial (FIX G) é recriado dentro de si, no ponto de chamada, alcançando self-reference.
Na verdade, há muitas definições possíveis para este operador FIX, o mais simples delas é:
Y := λg.(λx.g (x x)) (λx.g (x x))
Em lambda cálculo, Y g é um ponto-fixo de g, a medida que se expande a:
Y gλh.((λx.h (x x)) (λx.h (x x))) g(λx.g (x x)) (λx.g (x x))g ((λx.g (x x)) (λx.g (x x)))g (Y g)
Agora, para executar nossa chamada recursiva para a função fatorial, teríamos simplesmente que chamar (Y G) n, onde n é o número que estamos a calcular o fatorial de n . Dado n = 4, por exemplo, isto dá:
(Y G) 4G (Y G) 4(λr.λn.(1, se n = 0; então n × (r (n−1)))) (Y G) 4(λn.(1, se n = 0; então n × ((Y G) (n−1)))) 41, se 4 = 0; então 4 × ((Y G) (4−1))4 × (G (Y G) (4−1))4 × ((λn.(1, se n = 0; então n × ((Y G) (n−1)))) (4−1))4 × (1, se 3 = 0; então 3 × ((Y G) (3−1)))4 × (3 × (G (Y G) (3−1)))4 × (3 × ((λn.(1, se n = 0; então n × ((Y G) (n−1)))) (3−1)))4 × (3 × (1, se 2 = 0; então 2 × ((Y G) (2−1))))4 × (3 × (2 × (G (Y G) (2−1))))4 × (3 × (2 × ((λn.(1, se n = 0; então n × ((Y G) (n−1)))) (2−1))))4 × (3 × (2 × (1, se 1 = 0; então 1 × ((Y G) (1−1)))))4 × (3 × (2 × (1 × (G (Y G) (1−1)))))4 × (3 × (2 × (1 × ((λn.(1, se n = 0; então n × ((Y G) (n−1)))) (1−1)))))4 × (3 × (2 × (1 × (1, se 0 = 0; então 0 × ((Y G) (0−1))))))4 × (3 × (2 × (1 × (1))))24
Cada função definida recursivamente pode ser vista como um ponto fixo de alguma função adequadamente definida através da chamada recursiva com um argumento extra, e, por conseguinte, utilizando Y, cada função pode ser definida recursivamente expressa como uma expressão lambda. Em particular, podemos agora definir claramente a subtração, multiplicação e predicados de comparação dos números naturais de forma recursiva.
Termos padrão |
Alguns termos têm nomes comumente aceitos:
I := λx.x
K := λx.λy.x
S := λx.λy.λz.x z (y z)
B := λx.λy.λz.x (y z)
C := λx.λy.λz.x z y
W := λx.λy.x y y
U := λx.λy.y (x x y)
ω := λx.x x
Ω := ω ω
Y := λg.(λx.g (x x)) (λx.g (x x))
Outras linguagens puras |
- Haskell
Ver também |
- lambda cálculo simplesmente tipificado
Referências
↑ A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
↑ Para saber a história completa, veja "History of Lambda-calculus and Combinatory Logic" (2006), de Cardone e Hindley.
↑ A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (Apr., 1936), pp. 345-363.
↑ A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, Volume 5 (1940).
↑ «Example for Rules of Associativity». Lambda-bound.com. Consultado em 18 de junho de 2012
↑ Selinger, Peter (2008), Lecture Notes on the Lambda Calculus (PDF), 0804 (class: cs.LO), Department of Mathematics and Statistics, University of Ottawa, p. 9, Bibcode:2008arXiv0804.3434S, arXiv:0804.3434
↑ «Example for Rule of Associativity». Lambda-bound.com. Consultado em 18 de junho de 2012
↑ Barendregt, Henk; Barendsen, Erik (março de 2000), Introduction to Lambda Calculus (PDF)
↑ de Queiroz, Ruy J.G.B. "A Proof-Theoretic Account of Programming and the Role of Reduction Rules." Dialectica 42(4), pages 265-282, 1988.
↑ Turbak, Franklyn; Gifford, David (2008), Design concepts in programming languages, ISBN 978-0-262-20175-9, MIT press, p. 251
↑ Felleisen, Matthias; Flatt, Matthew (2006), Programming Languages and Lambda Calculi (PDF), p. 26
↑ Selinger, Peter (2008), Lecture Notes on the Lambda Calculus (PDF), 0804 (class: cs.LO), Department of Mathematics and Statistics, University of Ottawa, p. 16, Bibcode:2008arXiv0804.3434S, arXiv:0804.3434
Controle de autoridade |
|
|---|
: 
