Mostrar código-fonte de 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ção (matemática)|funções]] [[recursão|recursivas]] [[função computável|computáveis]], no que se refere à [[teoria da computabilidade]], e fenômenos relacionados, como variáveis ligadas e [[substituição (lógica)|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 computabilidade|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 [[Sistema de tipos|sistemas de tipos]] e [[Linguagem de programação|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]].<ref>A. Church, "A set of postulates for the foundation of logic", ''Annals of Mathematics'', Series 2, 33:346–366 (1932).</ref><ref>Para saber a história completa, veja "History of Lambda-calculus and Combinatory Logic" (2006), de Cardone e Hindley.</ref> O sistema original foi demonstrado ser [[Consistência|logicamente inconsistente]] em 1935 quando [[Stephen Kleene]] e [[:en:J._Barkley_Rosser|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.<ref>A. Church, "An unsolvable problem of elementary number theory", ''American Journal of Mathematics'', Volume 58, No. 2. (Apr., 1936), pp. 345-363.</ref> 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]].<ref>A. Church, "A Formulation of the Simple Theory of Types", ''Journal of Symbolic Logic'', Volume 5 (1940).</ref>

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 ===
[[Recursividade|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]]
:<code>I(x) = x</code>
recebe uma única entrada, <code>x</code>, e imediatamente retorna <code>x</code> (ou seja, a identidade não faz nada com sua entrada), enquanto a função
:<code>sqsum(x, y) = x*x + y*y</code>
recebe um par de entradas, <code>x</code> e <code>y</code> e retorna a soma de seus quadrados, <code>x*x + y*y</code>. 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
:<code>sqsum(x, y) = x*x + y*y</code>
pode ser reescrita na forma anônima como
:<code>(x, y) ↦ x*x + y*y</code>
(leia-se “a [[Énuplo|tupla]] <code>x</code> e <code>y</code> é mapeada em <code>x*x + y*y</code>”). Similarmente,
:<code>I(x) = x</code>
pode ser reescrita em sua forma anônima para <code>x ↦ x</code>, 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 é,
:<code>x ↦ x</code> e
:<code>y ↦ y</code>
expressam a mesma função: a identidade. De forma similar,
:<code>(x, y) ↦ x*x + y*y</code> e
:<code>(u, v) ↦ u*u + v*v</code>
também expressam a mesma função.

Finalmente, qualquer função que recebe duas entradas, como a função <code>sqsum</code> 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,
:<code>(x, y) ↦ x*x + y*y</code>
pode ser reelaborada para
:<code>x ↦ (y ↦ x*x + y*y)</code>
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
:<code>(x, y) ↦ x*x + y*y</code>
com sua forma "curryficada",
:<code>x ↦ (y ↦ x*x + y*y)</code>
Dado dois argumentos, temos:
:<code>((x, y) ↦ x*x + y*y)(5, 2)</code>
:<code> = 5*5 + 2*2 = 29</code>
No entanto, usando currying, temos:
:<code>((x ↦ (y ↦ x*x + y*y))(5))(2)</code>
:<code> = (y ↦ 5*5 + y*y)(2)</code>
:<code> = 5*5 + 2*2 = 29</code>
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, <code>x</code>;
* se <code>t</code> é um termo lambda, e <code>x</code> é uma variável, então <code>λx.t</code> é um termo lambda (chamado ''abstração lambda'');
* se <code>t</code> e <code>s</code> são termos lambda, então <code>ts</code> é 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'' <math>\lambda x.t</math> é uma definição de uma função não nomeada que é capaz de receber uma entrada <math>x</math> e substitui-la em sua expressão <math>t</math>. Define, assim, uma função anônima que recebe <math>x</math> e retorna <math>t</math>. Por exemplo, <math>\lambda x.(x^2+2)</math> é uma abstração lambda para a função <math>f(x) = x^2 + 2</math> usando o termo <math>(x^2+2)</math> para <math>t</math>. 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 [[Variáveis livres e ligadas|liga]] a variável <math>x</math> no termo <math>t</math>.

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

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

Parenteses podem ser usados para distinguir termos. Por exemplo, <math>\lambda x.((\lambda x.x)x)</math> e <math>(\lambda x.(\lambda x.x)) x</math> 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, <code>λx.x</code> representa a função identidade, <code>x ↦ x</code>, e <code>(λx.x)y</code> representa a função identidade aplicada a <code>y</code>. E assim, <code>(λx.y)</code> representa a ''função constante'' <code>x ↦ y</code>, uma função que sempre retorna, independentemente da entrada. É importante ressaltar que a aplicação de funções é associativa à esquerda, então <code>(λx.x)y z = ((λx.x)y)z</code>.

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, <code>λx.x</code> e <code>λy.y</code> são termos lambda alfa-equivalentes, representando a mesma função identidade.

Perceba que os termos <code>x</code> e <code>y</code> ''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 <code>x</code> são apenas <code>x</code>; as variáveis livres de <code>λx.t</code> são as variáveis livres de <code>t</code>, com <code>x</code> removido, e as variáveis livres de <code>ts</code> são a união das variáveis livres de <code>t</code> e <code>s</code>.

Por exemplo, o termo lambda representando a função identidade <code>λx.x</code> não tem variáveis livres, mas a função constante <code>λx.y</code> tem uma única variável livre, <code>y</code>.

==== Substituição de variáveis ====
Suponha que <math>t</math>, <math>s</math> e <math>r</math> são lambda termos e <math>x</math> e <math>y</math> são variáveis. A notação <math>t[x := r]</math> indica a substituição de <math>x</math> por <math>r</math> em <math>t</math>. Isto é definido de modo que:
* <math>x[x := r] = r</math>;
* <math>y[x := r] = y</math> se <math>x \neq y</math>;
* <math>(ts)[x := r] = (t[x := r])(s[x := r])</math>;
* <math>(\lambda x.t)[x := r] = \lambda x.t</math>;
* <math>(\lambda y.t)[x := r] = \lambda y.(t[x := r])</math> se <math>x \neq y</math> e <math>y</math> não é variável livre de <math>r</math>. A variável <math>y</math> é chamada de "fresh" para <math>r</math>.
Exemplos:
* <math>(\lambda x.x)[y := y] = \lambda x.(x[y := y]) = \lambda x.x</math>,
* <math>((\lambda x.y)x)[x := y] = ((\lambda x.y)[x := y])(x[x := y]) = (\lambda x.y)y</math>.

==== Redução Beta ====
A regra de redução beta afirma que uma aplicação da forma <math>( \lambda x . t) s</math> reduz para o termo <math> t [ x := s]</math>. A notação <math>( \lambda x . t ) s \to t [ x := s ] </math> é usada para indicar que <math>( \lambda x .t ) s </math> beta reduz para <math> t [ x := s ] </math>. Por exemplo, para todo <math>s</math>, <math>( \lambda x . x ) s \to x[ x := s ] = s </math>. Isto demostra que <math> \lambda x . x </math> realmente é a função identidade. De forma semelhante, <math>( \lambda x . y ) s \to y [ x := s ] = y </math>, Que demonstra que <math> \lambda x . y </math> e uma função constante.

O cálculo lambda pode ser visto como uma linguagem de programação funcional idealizada. Como [[Haskell (linguagem de programação)|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 <math>\Omega = (\lambda x . xx)( \lambda x . xx )</math>. Assim temos <math>( \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 )</math>. 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 [[Tipo de dado|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<sub>1</sub>, v<sub>2</sub>, …, v<sub>n</sub>
: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 [[Formalismo de Backus-Naur|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)<ref>{{citar web|url = http://www.lambda-bound.com/book/lambdacalc/node27.html|título= Example for Rules of Associativity|publicado= Lambda-bound.com|data= |acessodata= 2012-06-18}}</ref>
* 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<ref name="Selinger">{{Citation
 |primeiro = Peter|último = Selinger|título= Lecture Notes on the Lambda Calculus|ano= 2008|página= 9|local= |publicado= Department of Mathematics and Statistics, University of Ottawa|url = http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf|bibcode = 2008arXiv0804.3434S|volume = 0804|arxiv = 0804.3434|número= class: cs.LO}}</ref><ref>{{citar web|url = http://www.lambda-bound.com/book/lambdacalc/node25.html|título= Example for Rule of Associativity|publicado= Lambda-bound.com|data= |acessodata= 2012-06-18}}</ref>

=== 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: <code>λ''y''.''x'' ''x'' ''y''</code>. 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 : <code>λ''x''.''y'' (λ''x''.''z'' ''x'')</code>.

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)<ref name="BarendregtBarendsen">{{Citation
 |último = Barendregt|primeiro = Henk|último2 = Barendsen|primeiro2 = Erik|título= Introduction to Lambda Calculus|local= |publicado= |data=março de 2000|edição= |url = ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf}}</ref>
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 [[:en:Combinatory logic|combinatory logic]].

== Redução ==
O significado de expressões lambda é definido por como expressões podem ser reduzidas.<ref>[[Ruy de Queiroz|de Queiroz, Ruy J.G.B.]] "[[doi:10.1111/j.1746-8361.1988.tb00919.x|A Proof-Theoretic Account of Programming and the Role of Reduction Rules.]]" ''Dialectica'' '''42'''(4), pages 265-282, 1988.</ref>

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, <code>(λ''x''.M) N</code> é uma beta-redex que expressa a substituição de x por N em M; se <code>''x''</code> não é variável livre em <code>M</code>, <code>λ''x''.M ''x''</code> é 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, <code>M[''x'':=N]</code> e <code>M</code>.

=== α-'''conversão''' ===
Alpha-conversão, às vezes é conhecida como alfa-renomeação,<ref>{{Citation |título= Design concepts in programming languages|último1 = Turbak|primeiro1 = Franklyn|último2 = Gifford|primeiro2 = David|ano= 2008|publicado= MIT press|página= 251|isbn = 978-0-262-20175-9}}</ref> permite alterar nomes de variáveis ligadas. Por exemplo, alpha-conversão de <code>λ''x''.''x''</code> pode produzir <code>λ''y''.''y''</code>. 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 <code>λ''x''.λ''x''.''x''</code> poderia resultar em <code>λ''y''.λ''x''.''x''</code>, mas não pode resultar em <code>λ''y''.λ''x''.''y''</code>. 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 <code>''x''</code> com <code>''y''</code> em <code>λ''x''.λ''y''.''x''</code>, nós obteríamos <code>λ''y''.λ''y''.''y''</code>, 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 [[:en:Name resolution (programming languages)|name resolution]] garantindo que nenhum nome de variável [[:en:Variable shadowing|masks]] um nome em um determinado [[Escopo (computação)|escopo]].

Na notação [[:en:De Bruijn index|De Bruijn index]], quaisquer dois termos alfa-equivalente são literalmente idênticos.

==== Substituição ====
Substituição, escrito {{mono|1 = ''E''[''V'' := ''R'']}}, é o processo de substituição de todas as ocorrências da variável livre {{mono|''V''}} na expressão {{mono|''E''}} pela expressão {{mono|''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] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x2261; N
 ''y''[''x'' := N] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x2261; ''y'', se ''x'' ≠ ''y''
 (M<sub>1</sub> M<sub>2</sub>)[''x'' := N]&nbsp; &#x2261; (M<sub>1</sub>[''x'' := N]) (M<sub>2</sub>[''x'' := N])
 (λ''x''.M)[''x'' := N] &nbsp;&#x2261; λ''x''.M
 (λ''y''.M)[''x'' := N] &nbsp;&#x2261; λ''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.

=== &#x3B2;-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 <code>((λ''V''.''E'') ''E&#x2032;'')&nbsp;</code> é <code>''E''[''V'' := ''E&#x2032;'']</code>.

Por exemplo, assumindo alguns codificação de <code>2, 7, &#xD7;</code>, temos a seguinte β-redução: <code>((λ''n''.''n''&#xD7;2) 7) </code>→<code> 7&#xD7;2</code>.

=== &#x3B7;-conversão ===
Eta-conversão expressa a ideia de [[:en:Extensionality|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 <code>λ''x''.(''f'' ''x'')</code> e <code>''f''</code> sempre que <code>''x''</code> não aparece livre em <code>''f''</code>.

== Forma normal e confluência ==
Para o cálculo lambda n/tipado, β-redução como uma ''[[Sistema de redução|rewriting rule]]'' não é nem [[Forma normal|fortemente normalizada]] nem fracamente normalizada.

No entanto, se puder ser demonstrado que a β-redução é [[Confluência (sistemas de reescrita de termos)|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, [[Estrutura de dados|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úmero natural|números naturais]] no cálculo lambda, mas, de longe, os mais comuns são os [[Codificação de Church|numerais de Church]], que podem ser definidos da seguinte forma:
: <code>0 := λ''f''.λ''x''.''x''</code>
: <code>1 := λ''f''.λ''x''.''f'' ''x''</code>
: <code>2 := λ''f''.λ''x''.''f'' (''f'' ''x'')</code>
: <code>3 := λ''f''.λ''x''.''f'' (''f'' (''f'' ''x''))</code>
e assim por diante. Ou usando a sintaxe alternativa representada anteriormente na Notação:
: <code>0 := λ''fx''.''x''</code>
: <code>1 := λ''fx''.''f'' ''x''</code>
: <code>2 := λ''fx''.''f'' (''f'' ''x'')</code>
: <code>3 := λ''fx''.''f'' (''f'' (''f'' ''x''))</code>
Um numeral de Church é uma [[função de ordem superior]]. Ela toma um função de um único argumento <code>''f''</code>, e retorna outra função de um único argumento. O numeral de Church <code>''n''</code> é uma função que toma uma função <code>''f''</code> como argumento e retorna a n-ésima composição de <code>''f''</code>, isto é, a função f composta com ela mesma <code>''n''</code> vezes. Isto e representado por <code>''f''<sup>(''n'')</sup></code> e é de fato a <code>''n''</code>-exima potencia de <code>''f''</code> (considerado como um operador); <code>''f''<sup>(0)</sup></code> é definido como sendo a [[função identidade]]. Essas composições repetidas (de uma única função <code>''f''</code>) obedece à [[Exponenciação|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 <code>0</code> impossível).

Podemos definir uma função sucessor, o que leva um número <code>''n''</code> e retorna <code>''n'' + 1</code> pela adição de outra aplicação de <code>''f''</code>, onde '<code>''(mf)x''</code>" significa que a função <code>''f''</code> é aplicado <code>''m''</code> vezes em <code>''x''</code>:
: <code>SUCC := λ''n''.λ''f''.λ''x''.''f'' (''n'' ''f'' ''x'')</code>
Porque o <code>''m''</code>-exima composição de <code>''f''</code> composto com a <code>''n''</code>-exima composição de <code>''f''</code> dá a <code>''m''+''n''</code>-exima composição de <code>''f''</code>, Adicionalmente pode ser definido como se segue:
: <code>PLUS := λ''m''.λ''n''.λ''f''.λ''x''.''m'' ''f'' (''n'' ''f'' ''x'')</code>
<code>PLUS</code> 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
: <code>PLUS 2 3</code>
e
: <code>5</code>
são expressões lambda β-equivalentes, desde que acrescentando <code>''m''</code> para um número <code>''n''</code> pode ser realizado adicionando 1 <code>''m''</code> vezes, uma definição equivalente é:
: <code>PLUS := λ''m''.λ''n''.''m'' SUCC ''n&#x2009;''</code><ref>{{Citation
 |último1 = Felleisen|primeiro1 = Matthias|último2 = Flatt|primeiro2 = Matthew|título= Programming Languages and Lambda Calculi|publicado= |ano= 2006|local= |página= 26|url = http://www.cs.utah.edu/plt/publications/pllc.pdf}}</ref>
De forma simular, multiplicação pode ser definida da seguinte forma:
: <code>MULT := λ''m''.λ''n''.λ''f''.''m'' (''n'' ''f'')</code><ref>{{Citation
 |primeiro = Peter|último = Selinger|título= Lecture Notes on the Lambda Calculus|ano= 2008|página= 16|local= |publicado= Department of Mathematics and Statistics, University of Ottawa|url = http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf|bibcode = 2008arXiv0804.3434S|volume = 0804|arxiv = 0804.3434|número= class: cs.LO}}</ref>
Alternativamente:
: <code>MULT := λ''m''.λ''n''.''m'' (PLUS ''n'') 0</code>
desde multiplicando <code>''m''</code> e <code>''n''</code> é o mesmo que repetir a adicionar <code>''n''</code> funções <code>''m''</code> vezes e, em seguida, aplicando a zero. Exponenciação tem uma realização bastante simples em numerais de Church, ou seja:
: <code>POW := λ''b''.λ''e''.''e'' ''b''</code>
A função predecessora definida por <code>PRED ''n'' = ''n'' − 1</code> para um inteiro positivo <code>''n''</code> e <code>PRED 0 = 0</code> é consideravelmente mais difícil. A fórmula
: <code>PRED := λ''n''.λ''f''.λ''x''.''n'' (λ''g''.λ''h''.''h'' (''g'' ''f'')) (λ''u''.''x'') (λ''u''.''u'')</code>
pode ser validado, mostrando indutivamente que se ''T'' representa <code>(λ''g''.λ''h''.''h'' (''g'' ''f''))</code>, então <code>T<sup>(''n'')</sup>(λ''u''.''x'') = (λ''h''.''h''(''f''<sup>(''n''−1)</sup>(''x'')))</code> para <code>''n'' > 0</code>. Duas outras definições de <code>PRED</code> 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:
: <code>SUB := λ''m''.λ''n''.''n'' PRED ''m''</code>,
<code>SUB ''m'' ''n''</code> produz <code>''m'' − ''n''</code> quando <code>''m'' > ''n''</code> e <code>0</code> 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 <code>TRUE</code> e<code>FALSE</code>:
: <code>TRUE := λ''x''.λ''y''.''x''</code>
: <code>FALSE := λ''x''.λ''y''.''y''</code>
:: (Note que <code>FALSE</code> é 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):
: <code>AND := λ''p''.λ''q''.''p'' ''q'' ''p''</code>
: <code>OR := λ''p''.λ''q''.''p'' ''p'' ''q''</code>
: <code>NOT := λ''p''.λ''a''.λ''b''.''p'' ''b'' ''a''</code>
: <code>IFTHENELSE := λ''p''.λ''a''.λ''b''.''p'' ''a'' ''b''</code>
Estamos agora em condições de calcular algumas funções lógicas, por exemplo:
: <code>AND TRUE FALSE</code>
:: <code>≡ (λ''p''.λ''q''.''p'' ''q'' ''p'') TRUE FALSE →<sub>β</sub> TRUE FALSE TRUE</code>
:: <code>≡ (λ''x''.λ''y''.''x'') FALSE TRUE →<sub>β</sub> FALSE</code>
e vemos que <code>AND TRUE FALSE</code> é equivalente a <code>FALSE</code>.

Um predicado é uma função que retorna um valor booleano. O predicado mais fundamental é <code>ISZERO</code>, que retorna <code>TRUE</code> se o seu argumento é o numeral de Church <code>0</code>, e <code>FALSE</code> se seu argumento for qualquer outro numeral de Church:
: <code>ISZERO := λ''n''.''n'' (λ''x''.FALSE) TRUE</code>
Os seguintes predicados testa se o primeiro argumento é menor que ou igual a segundo:
: <code>LEQ := λ''m''.λ''n''.ISZERO (SUB ''m'' ''n'')</code>,
e desde <code>''m'' = ''n''</code>, se <code>LEQ ''m'' ''n''</code> e <code>LEQ ''n'' ''m''</code>, é muito simples para construir um predicado de igualdade numérica.

Da disponibilidade de predicados e na definição acima de <code>TRUE</code> e <code>FALSE</code> torná-lo conveniente para escrever expressões "if-then-else". Por exemplo, a função predecessora pode ser definida como:
: <code>PRED := λ''n''.''n'' (λ''g''.λ''k''.ISZERO (''g'' 1) ''k'' (PLUS (''g'' ''k'') 1)) (λ''v''.0) 0</code>
que pode ser verificada, mostrando indutivamente que <code>''n'' (λ''g''.λ''k''.ISZERO (''g'' 1) ''k'' (PLUS (''g'' ''k'') 1)) (λ''v''.0)</code> é a função adicionar <code>''n''</code> − 1 para <code>''n''</code> > 0.

=== Pares ===
Um par (2-tupla) pode ser definida em termos de <code>TRUE</code> e <code>FALSE</code>, usando a [[Codificação de Church#Pares de Church|pares de Church]]. Por exemplo, <code>PAIR</code> encapsula o par (<code>''x''</code>,<code>''y''</code>), <code>FIRST</code> retorna o primeiro elemento do par, e <code>SECOND</code> retorna o segundo.
: <code>PAIR := λ''x''.λ''y''.λ''f''.''f'' ''x'' ''y''</code>
: <code>FIRST := λ''p''.''p'' TRUE</code>
: <code>SECOND := λ''p''.''p'' FALSE</code>
: <code>NIL := λ''x''.TRUE</code>
: <code>NULL := λ''p''.''p'' (λ''x''.λ''y''.FALSE)</code>
Uma [[lista ligada]] pode ser definida como qualquer <code>NIL</code> para a lista vazia, ou o <code>PAIR</code> de um elemento e uma lista menor. o predicado <code>NULL</code> testa se o valor é <code>NIL</code>. (Alternativamente, com <code>NIL := FALSE</code>, a construção <code>''l'' (λ''h''.λ''t''.λ''z''.lidar_com_cabeça_''h''_e_calda_''t'') (lidar_com_nil)</code> obviamente e necessidade de um teste para NULL).

Como um exemplo da utilização de <code>PAIR</code>, a função de deslocamento-e-incremento que mapeia <code>(''m'', ''n'')</code> to <code>(''n'', ''n'' + 1)</code> pode ser definida da seguinte forma:
: <code>Φ := λ''x''.PAIR (SECOND ''x'') (SUCC (SECOND ''x''))</code>
O que nos permite dar talvez a versão mais transparente da função predecessor :
: <code>PRED := λ''n''.FIRST (''n'' Φ (PAIR 0 0)).</code>

=== Recursão e pontos fixos ===
{{Artigo principal|Combinador de ponto fixo}}{{VT|Combinadores SKI}}
[[Recursividade|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 <code>(λ''x''.''x'' ''x'') ''y''</code> &#x2002;ambos <code>''x''</code>&#x2009;‍ referem-se ao mesmo termo lambda, <code>''y''</code>, por isso, é possível que uma expressão lambda &#x2013; <code>''y''</code> &#x2013; ser preparada para receber-se como o seu argumento, através da auto-aplicação.

Considere, por exemplo, a função [[fatorial]]<code>F(''n'')</code> recursivamente definida por:
: <code>F(''n'') = 1, se ''n'' = 0; então ''n'' &#xD7; F(''n'' − 1)</code>.
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 &#x2013; aplicando-o a um argumento &#x2013; será equivalente à recursão. Assim, para alcançar a recursividade, o argumento destinado-como-auto-referência (chamado<code>''r''</code> aqui) sempre deve ser passada para si mesmo dentro do corpo da função, em um ponto de chamada:
: <code>G := λ''r''. λ''n''.(1, se ''n'' = 0; então ''n'' &#xD7; (''r'' ''r'' (''n''−1)))</code>
::: com&#x2002; <code>''r'' ''r'' ''x'' = F ''x'' = G ''r'' ''x''</code> &#x2002;para manter, assim <code>''r'' = G</code> &#x2002;e
: <code>F := G G = (λ''x''.''x'' ''x'') G</code>
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:
: <code>G := λ''r''. λ''n''.(1, se ''n'' = 0; então ''n'' &#xD7; (''r'' (''n''−1)))</code>
::: com&#x2002; <code>''r'' ''x'' = F ''x'' = G ''r'' ''x''</code> &#x2002;para manter, assim&#x2002; <code>''r'' = G ''r'' =: FIX G</code> &#x2002;e
: <code>F := FIX G</code> &#x2002;onde&#x2002; <code>FIX ''g'' := (''r'' onde ''r'' = ''g'' ''r'') = ''g'' (FIX ''g'')</code>
::: de modo que&#x2002; <code>FIX G = G (FIX G) = (λ''n''.(1, se ''n'' = 0; então ''n'' &#xD7; ((FIX G) (''n''−1))))</code>
Dado um termo lambda com o primeiro argumento representando chamada recursiva (i.e. <code>G</code> aqui), o combinador de ponto-fixo <code>FIX</code> irá retornar uma expressão lambda autorreplicante que representa a função recursiva (aqui, <code>F</code>). 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 <code>(FIX G)</code> é recriada dentro de si, no ponto de chamada, alcançando a [[autorreferência]].

Na verdade, há muitas definições possíveis para este operador <code>FIX</code>, o mais simples delas é:
: <code>'''Y''' := λ''g''.(λ''x''.''g'' (''x'' ''x'')) (λ''x''.''g'' (''x'' ''x''))</code>
Em cálculo lambda, <code>'''Y''' ''g''</code>&#x2009; é um ponto-fixo de <code>''g''</code>, a medida que se expande a:
: <code>'''Y''' ''g''</code>
: <code>λ''h''.((λ''x''.''h'' (''x'' ''x'')) (λ''x''.''h'' (''x'' ''x''))) ''g''</code>
: <code>(λ''x''.''g'' (''x'' ''x'')) (λ''x''.''g'' (''x'' ''x''))</code>
: <code>''g'' ((λ''x''.''g'' (''x'' ''x'')) (λ''x''.''g'' (''x'' ''x'')))</code>
: <code>''g'' ('''Y''' ''g'')</code>
Agora, para executar nossa chamada recursiva para a função fatorial, teríamos simplesmente que chamar <code>('''Y''' G) ''n''</code>,&nbsp; onde <code>''n''</code> é o número que estamos a calcular o fatorial de <code>''n''</code> . Dado ''n'' = 4, por exemplo, isto dá:
: <code>('''Y''' G) 4</code>
: <code>G ('''Y''' G) 4</code>
: <code>(λ''r''.λ''n''.(1, se ''n'' = 0; então ''n'' × (''r'' (''n''−1)))) ('''Y''' G) 4</code>
: <code>(λ''n''.(1, se ''n'' = 0; então ''n'' × (('''Y''' G) (''n''−1)))) 4</code>
: <code>1, se 4 = 0; então 4 × (('''Y''' G) (4−1))</code>
: <code>4 × (G ('''Y''' G) (4−1))</code>
: <code>4 × ((λ''n''.(1, se ''n'' = 0; então ''n'' × (('''Y''' G) (''n''−1)))) (4−1))</code>
: <code>4 × (1, se 3 = 0; então 3 × (('''Y''' G) (3−1)))</code>
: <code>4 × (3 × (G ('''Y''' G) (3−1)))</code>
: <code>4 × (3 × ((λ''n''.(1, se ''n'' = 0; então ''n'' × (('''Y''' G) (''n''−1)))) (3−1)))</code>
: <code>4 × (3 × (1, se 2 = 0; então 2 × (('''Y''' G) (2−1))))</code>
: <code>4 × (3 × (2 × (G ('''Y''' G) (2−1))))</code>
: <code>4 × (3 × (2 × ((λ''n''.(1, se ''n'' = 0; então ''n'' × (('''Y''' G) (''n''−1)))) (2−1))))</code>
: <code>4 × (3 × (2 × (1, se 1 = 0; então 1 × (('''Y''' G) (1−1)))))</code>
: <code>4 × (3 × (2 × (1 × (G ('''Y''' G) (1−1)))))</code>
: <code>4 × (3 × (2 × (1 × ((λ''n''.(1, se ''n'' = 0; então ''n'' × (('''Y''' G) (''n''−1)))) (1−1)))))</code>
: <code>4 × (3 × (2 × (1 × (1, se 0 = 0; então 0 × (('''Y''' G) (0−1))))))</code>
: <code>4 × (3 × (2 × (1 × (1))))</code>
: <code>24</code>
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 <code>'''Y'''</code>, 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:
: {{anchor|I}} <code>'''I''' := λ''x''.''x''</code>
: {{anchor|K}} <code>'''K''' := λ''x''.λ''y''.''x''</code>
: {{anchor|S}} <code>'''S''' := λ''x''.λ''y''.λ''z''.''x'' ''z'' (''y'' ''z'')</code>
: {{anchor|B}} <code>'''B''' := λ''x''.λ''y''.λ''z''.''x'' (''y'' ''z'')</code>
: {{anchor|C}} <code>'''C''' := λ''x''.λ''y''.λ''z''.''x'' ''z'' ''y''</code>
: {{anchor|W}} <code>'''W''' := λ''x''.λ''y''.''x'' ''y'' ''y''</code>
: {{anchor|U}} <code>'''U''' := λ''x''.λ''y''.''y'' (''x'' ''x'' ''y'')</code>
: {{anchor|omega}} <code>'''ω''' := λ''x''.''x'' ''x''</code>
: {{anchor|Omega}} <code>'''Ω''' := '''ω''' '''ω'''</code>
: {{anchor|Y}} <code>'''Y''' := λ''g''.(λ''x''.''g'' (''x'' ''x'')) (λ''x''.''g'' (''x'' ''x''))</code>

== Ver também ==
* [[Cálculo lambda simplesmente tipado]]
* [[Haskell (linguagem de programação)|Haskell]]

{{Referências}}

{{Controle de autoridade}}

{{DEFAULTSORT:Calculo Lambda}}
[[Categoria:Teoria da computação]]
[[Categoria:Métodos formais]]