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.

A parte relevante do cálculo lambda para computação ficou conhecida como cálculo lambda não tipado. O cálculo lambda 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).

História

O cálculo lambda 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 cálculo lambda 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 cálculo lambda 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 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

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 ↦ x e

y ↦ y

expressam a mesma função: a identidade. De forma similar,

(x, y) ↦ x*x + y*y e

(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 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.

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, e x é uma variável, então λx.t é um termo lambda (chamado abstração lambda);
se t e s são termos lambda, então ts é 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 $\lambda x.t$ é uma definição de uma função não nomeada que é capaz de receber uma entrada $x$ e substitui-la em sua expressão $t$ . Define, assim, uma função anônima que recebe $x$ e retorna $t$ . Por exemplo, $\lambda x.(x^{2}+2)$ é uma abstração lambda para a função $f(x)=x^{2}+2$ usando o termo $(x^{2}+2)$ para $t$ . A definição de uma função com a abstração lambda meramente "configura" a função, mas não a invoca. A abstração liga a variável $x$ no termo $t$ .

Uma aplicação $ts$ representa a aplicação de uma função $t$ com um argumento $s$ , ou seja, ela representa o ato de chamar a função $t$ com entrada $s$ para produzir $t(s)$ .

Em cálculo lambda não existe o conceito de declaração de variáveis. Em uma definição tal qual $\lambda x.(x+y)$ (i.e. $f(x)=x+y$ ), cálculo lambda trata $y$ como uma variável que ainda não foi definida.A abstração lambda $\lambda x.(x+y)$ é sintaticamente valida, e representa uma função que soma a entrada com o valor ainda não conhecido $y$ .

Parenteses podem ser usados para distinguir termos. Por exemplo, $\lambda x.((\lambda x.x)x)$ e $(\lambda x.(\lambda x.x))x$ representam diferentes termos (embora eles coincidentemente possam ser reduzidos para o mesmo termo normal). Aqui o primeiro exemplo define uma função que define outra função e retorna o resultado de aplicar x para a função-filha (aplicar a função e então retornar), enquanto o segundo exemplo define uma função que retorna uma função para qualquer entrada e então retorna a aplicação dela a x (retorna uma função e então aplica).

Funções que operam em funções

Em cálculo lambda, 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$ , $s$ e $r$ são lambda termos e $x$ e $y$ são variáveis. A notação $t[x:=r]$ indica a substituição de $x$ por $r$ em $t$ . Isto é definido de modo que:

$x[x:=r]=r$ ;
$y[x:=r]=y$ se $x\neq y$ ;
$(ts)[x:=r]=(t[x:=r])(s[x:=r])$ ;
$(\lambda x.t)[x:=r]=\lambda x.t$ ;
$(\lambda y.t)[x:=r]=\lambda y.(t[x:=r])$ se $x\neq y$ e $y$ não é variável livre de $r$ . A variável $y$ é chamada de "fresh" para $r$ .

Exemplos:

$(\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x$ ,
$((\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 $(\lambda x.t)s$ reduz para o termo $t[x:=s]$ . A notação $(\lambda x.t)s\to t[x:=s]$ é usada para indicar que $(\lambda x.t)s$ beta reduz para $t[x:=s]$ . Por exemplo, para todo $s$ , $(\lambda x.x)s\to x[x:=s]=s$ . Isto demostra que $\lambda x.x$ realmente é a função identidade. De forma semelhante, $(\lambda x.y)s\to y[x:=s]=y$ , Que demonstra que $\lambda x.y$ e uma função constante.

O cálculo lambda 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 cálculo lambda não tipado, como este apresentado aqui, este processo pode não terminar em alguns casos. Um exemplo é o seguinte, considere o termo $\Omega =(\lambda x.xx)(\lambda x.xx)$ . Assim temos $(\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)$ . Isto é, o termo reduz para ele mesmo em um passo da beta redução, e portanto o processo de redução nunca termina.

Outro aspecto do cálculo lambda 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 cálculo lambda 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 v₁, v₂, …, v_n

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 a mesma existe 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 podem ser reduzidas.^[9]

Existem três tipos de reduções.

α-conversão: trocar variáveis ligadas (alfa);
β-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 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.

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.

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
(M₁ M₂)[x := N]  ≡ (M₁[x := N]) (M₂[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 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.

Codificando tipos de dados

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:

0 := λf.λx.x

1 := λf.λx.f x

2 := λ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.x

1 := λfx.f x

2 := λfx.f (f x)

3 := λfx.f (f (f x))

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⁽ⁿ⁾ e é de fato a n-exima potencia de f (considerado como um operador); f⁽⁰⁾ é 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).

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

e

5

são expressões lambda β-equivalentes, desde que acrescentando m para um número n pode ser realizado adicionando 1 m vezes, 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 predecessora definida por PRED n = n − 1 para um inteiro positivo n e PRED 0 = 0 é consideravelmente mais difícil. A fórmula

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⁽ⁿ⁾(λu.x) = (λh.h(f⁽ⁿ⁻¹⁾(x))) para n > 0. Duas outras definições de PRED são apresentadas a seguir, uma usando condicionais e a outra usando pares. Com a função de predecessor, a subtração é simples. Definida por:

SUB := λm.λn.n PRED m,

SUB m n produz m − n quando m > n e 0 caso contrário.

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:

TRUE := λx.λy.x

FALSE := λx.λy.y

(Note que FALSE é equivalente ao numeral de Church zero definido anteriormente).

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 p

OR := λp.λq.p p q

NOT := λp.λa.λb.p b a

IFTHENELSE := λ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 e FALSE torná-lo conveniente para escrever expressões "if-then-else". Por exemplo, a função predecessora 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.

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.

PAIR := λx.λy.λf.f x y

FIRST := λp.p TRUE

SECOND := λp.p FALSE

NIL := λx.TRUE

NULL := λ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

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:

F(n) = 1, se n = 0; então n × F(n − 1).

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:

G := λr. λn.(1, se n = 0; então n × (r r (n−1)))

com r r x = F x = G r x para manter, assim r = G e

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 reescrita:

G := λr. λn.(1, se n = 0; então n × (r (n−1)))

com r x = F x = G r x para manter, assim r = G r =: FIX G e

F := FIX G onde FIX 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))))

Dado um termo lambda com o primeiro argumento representando chamada recursiva (i.e. G aqui), o combinador de ponto-fixo FIX irá retornar uma expressão lambda autorreplicante que representa a função recursiva (aqui, F). A função não necessita ser passada explicitamente a si mesma em qualquer ponto, a autorreplicação é providenciado com antecedência quando ela é criada para ser feita cada vez que é chamada. Assim, a expressão lambda inicial (FIX G) é recriada dentro de si, no ponto de chamada, alcançando a autorreferência.

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 cálculo lambda, 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) 4

G (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)))) 4

1, 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))

Ver também

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

[1] A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).

[2] Para saber a história completa, veja "History of Lambda-calculus and Combinatory Logic" (2006), de Cardone e Hindley.

[3] A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (Apr., 1936), pp. 345-363.

[4] A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, Volume 5 (1940).

[5] «Example for Rules of Associativity». Lambda-bound.com. Consultado em 18 de junho de 2012

[Selinger-6] 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

[7] «Example for Rule of Associativity». Lambda-bound.com. Consultado em 18 de junho de 2012

[BarendregtBarendsen-8] Barendregt, Henk; Barendsen, Erik (março de 2000), Introduction to Lambda Calculus (PDF)

[9] Queiroz, Ruy J.G.B. "A Proof-Theoretic Account of Programming and the Role of Reduction Rules." Dialectica 42(4), pages 265-282, 1988.

[10] Turbak, Franklyn; Gifford, David (2008), Design concepts in programming languages, ISBN 978-0-262-20175-9, MIT press, p. 251

[11] Felleisen, Matthias; Flatt, Matthew (2006), Programming Languages and Lambda Calculi (PDF), p. 26

[12] 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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]